{"id":"palomar/PALOMAR-2026-10-30-000009","url":"https://github.com/na0b/gaussianriesz-lean/tree/dc16c5de824a20c0164947c3a3e157887d9844c0","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-30-000009-v1.json","repo":"https://github.com/na0b/gaussianriesz-lean","tags":["math.CA","math.FA","msc:42B20","msc:42C10","msc:35J86","msc:47A60","msc:68V20"],"score":0,"title":"A dimension-free weak-type (1,1) bound for the Gaussian Riesz transforms","trust":"high","domain":"math.CA","source":"palomar","authors":["Cristian E. Gutiérrez","Juan J. Manfredi"],"reviews":0,"subject":"math.CA","summary":"A complete Lean 4 / Mathlib formalization of the main results of Gutiérrez and Manfredi, \"A direct obstacle proof of a dimension-free weak-type (1,1) bound for the Gaussian Riesz transforms\" (arXiv:2610.26478). For the Gaussian measure dγₙ = π^{-n/2} e^{-|x|²} dx on ℝⁿ, the Ornstein–Uhlenbeck operator L = -½Δ + x·∇ and the normalized gradient D = 2^{-1/2}∇, the vector Riesz transform R_γ = D L^{-1/2} Π₀ has exactly one linear extension to L¹(γₙ) satisfying t·γₙ{|R_γ f| > t} ≤ 2‖f‖₁ for all t > 0, in every dimension n (Theorem 5.1). The proof goes through a Gaussian obstacle decomposition F =…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-30","reactions":{},"formalized":true,"formalizes":[{"title":"A direct obstacle proof of a dimension-free weak-type (1,1) bound for the Gaussian Riesz transforms","identifier":"arXiv:2610.26478","relationship":"formalizes"}]}