{"id":"palomar/PALOMAR-2026-10-21-000004","url":"https://github.com/roos-j/lean-dfr/tree/5c7595a83657b6c02f62ebf4f4ae1c02cb4109e4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-21-000004-v1.json","repo":"https://github.com/roos-j/lean-dfr","tags":["math.CA","msc:42B20","harmonic-analysis","hilbert-transform","simplex","lean-formalization"],"score":0,"title":"Formalization of a curved three-dimensional simplex Hilbert transform","trust":"high","domain":"math.CA","source":"palomar","authors":["Polona Durcik","Marco Fraccaroli","Joris Roos"],"reviews":0,"subject":"math.CA","summary":"This is a Lean 4 formalization of the main theorem from the paper \"A curved three-dimensional simplex Hilbert transform\" by P. Durcik, M. Fraccaroli and J. Roos.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-21","reactions":{},"formalized":true,"formalizes":[{"title":"A curved three-dimensional simplex Hilbert transform","identifier":"arXiv:2610.24850, https://arxiv.org/abs/2610.24850","relationship":"formalizes"}]}