A dimension-free weak-type (1,1) bound for the Gaussian Riesz transforms
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 =…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-30-000009
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-30-000009/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-30-000009/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'