Harmonic analysis on Euclidean spaces
The Lean Pool projects whose card's first MSC2020 code is in class 42, Harmonic analysis on Euclidean spaces: 5 articles, one per card.
TheoremBoundedness of the trilinear Hilbert transform#
Proves the L³ × L³ × L³ to L¹ bound for the principal-value trilinear Hilbert transform on Schwartz functions, together with its unique bounded extension to L³. Preserves the finite inverse theorem, quantitative quadratic charts, dyadic stopping and projection estimates used by the proof.
Quoted from the card LeanPool/projects/trilinear-hilbert-transform.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
TrilinearHT.trilinear_ht_bound(theorem; a main declaration), declared in LeanPool/TrilinearHilbertTransform/Theorems.lean, line 33: “There is an absolute real constant C such that the L¹ norm of the principal-value integral of f₁(x+t) f₂(x+2t) f₃(x+3t)/t is at most C times the product of the L³ norms, for all complex Schwartz functions.”TrilinearHT.Auto.tht_main(theorem), declared in LeanPool/TrilinearHilbertTransform/Auto/Sec163SummingUpdateLevels/RetainedMinHolds.lean, line 2554: “The truncations converge pointwise for Schwartz inputs, and the transform has a unique bounded complex trilinear extension from three copies of L³ to L¹, agreeing almost everywhere with the Schwartz transform.”
Project
- Authors: Joris Roos.
- Source: Formalization of boundedness of the trilinear Hilbert transform, manuscript.
- Project repository: roos-j/lean-trilinearht, at commit 7b420960.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 42B20, 42B25.
- In Lean Pool: LeanPool/TrilinearHilbertTransform, from the card LeanPool/projects/trilinear-hilbert-transform.yaml.
Sources
TheoremBounds for the centered Hardy-Littlewood maximal constant#
Proves that the weak type (1,1) constant c_2 of the centered maximal operator over axis-parallel squares is at least the explicit radical phi, approximately 1.68551, using a weighted periodic lattice and integrable approximations. Also proves c_d <= 2^d in every natural dimension and 1.685 < phi < 1.686. The operator acts on real-valued integrable functions, with Lebesgue outer measure of strict level sets. Includes the maximal-function API, a Vitali covering argument, lattice witnesses, smearing estimates, and the limiting lower bound. No optimality of phi is claimed.
Quoted from the card LeanPool/projects/centered-maximal-constant.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
LeanPool.CenteredMaximal.ofReal_phi_le_weakTypeConstant_two(theorem; a main declaration), declared in LeanPool/CenteredMaximal.lean, line 63: “The explicit radical phi is a lower bound for c_2, the infimum of all weak type (1,1) bounds for the centered maximal operator over axis-parallel squares in the real plane.”LeanPool.CenteredMaximal.weakTypeConstant_le_two_pow(theorem), declared in LeanPool/CenteredMaximal.lean, line 58: “For every natural number d, including zero, the centered maximal operator over axis-parallel cubes in real d-space has weak type (1,1) constant c_d at most 2^d.”LeanPool.CenteredMaximal.phi_mem_Ioo(theorem), declared in LeanPool/CenteredMaximal/Numerics.lean, line 24: “The explicit radical constant phi lies strictly between 1.685 and 1.686.”
Project
- Authors: Yongxi Lin.
- Source: A lower bound 1.6855 for the planar centred maximal constant over squares by Yongxi Lin.
- The card's note on its source: “First completed publicly on 2026-09-18 at 22:15:07 UTC in commit 06a726f113241d445903f0c0eae1ebe40d8b539f. The lower bound is documented and proved in upstream docs/PROOF.md; the weighted smearing argument adapts Aldaz (2000), Lemma 1.1, and the covering upper bound follows Tao's 245A Notes 5, Exercise 42. Upstream formalization.yaml and docs/HISTORY.md disclose AI generation of the configuration and proofs under Yongxi Lin's direction.”
- Project repository: CoolRmal/centered-maximal-constant, at commit c6a8cb29.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 42B25, 26D15.
- In Lean Pool: LeanPool/CenteredMaximal, from the card LeanPool/projects/centered-maximal-constant.yaml.
Sources
TheoremEndpoint estimates for Stein's purely quadratic Carleson operator#
A Lean 4 formalization of four principal endpoint assertions from Fragkos, Krause, and Lacey's Endpoint Estimates for Stein's Purely Quadratic Carleson Operator: two failures of modular estimates below t log₂ t, a full-modulation L log L endpoint estimate, and a lacunary L (log₂ L)² log₄ L endpoint estimate.
Quoted from the card LeanPool/projects/quadratic-carleson-palomar-submission.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
QuadraticCarleson.StatementSurface.PaperTheorems.lacunary_sub_log2_modular_failure(theorem), declared in LeanPool/QuadraticCarleson/Solution.lean, line 91: “Lacunary purely quadratic modulation fails modular estimates below the specified iterated-logarithmic threshold.”QuadraticCarleson.StatementSurface.PaperTheorems.full_sub_log2_modular_failure(theorem), declared in LeanPool/QuadraticCarleson/Solution.lean, line 96: “Full purely quadratic modulation fails modular estimates below the specified iterated-logarithmic threshold.”QuadraticCarleson.StatementSurface.PaperTheorems.full_LlogL_endpoint(theorem; a main declaration), declared in LeanPool/QuadraticCarleson/Solution.lean, line 101: “The full-modulation operator satisfies the L log L endpoint estimate.”QuadraticCarleson.StatementSurface.PaperTheorems.lacunary_log2_squared_log4_endpoint(theorem), declared in LeanPool/QuadraticCarleson/Solution.lean, line 110: “The lacunary operator satisfies the L (log₂ L)² log₄ L endpoint estimate.”
Project
- Authors: Anastasios Fragkos.
- Project repository: anastasiosfragkosmath/quadratic-carleson-palomar-submission, at commit 3d3cf431.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 42B20.
- In Lean Pool: LeanPool/QuadraticCarleson, from the card LeanPool/projects/quadratic-carleson-palomar-submission.yaml.
Sources
TheoremSquare-function estimates from type IV superorthogonality#
Proves the type IV superorthogonality square-function estimate for finite and countable index sets, including the pointwise combinatorial estimate and unconditional convergence in L^(2r).
Quoted from the card LeanPool/projects/lean-superorthogonality.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
Superorthogonal.sqfct_estimate_of_type_iv_superorthogonal(theorem; a main declaration), declared in LeanPool/Superorthogonality/LeanSuperorthogonality/MainTheorem.lean, line 37: “For an integer r >= 1, a countable type IV superorthogonal family in L^(2r), with almost-everywhere summable squared norms and square function in L^(2r), converges unconditionally in L^(2r) and satisfies the square-function bound with constant C(r).”
Project
- Authors: Joris Roos.
- Project repository: roos-j/lean-superorthogonality, at commit 6d3a3645.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 42B25, 46E30.
- In Lean Pool: LeanPool/Superorthogonality, from the card LeanPool/projects/lean-superorthogonality.yaml.
Sources
TheoremStable phase retrieval for Hermite-Fock expansions#
Formalizes stable phase retrieval for finite Hermite-Fock polynomials and their Gaussian L2 closure in d complex dimensions, together with the quantitative one-dimensional Fock-space local stability estimate that underlies it.
Quoted from the card LeanPool/projects/phaseretrieval.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
DimdPolyShowcaseChallenge.stable_phase_retrieval(theorem; a main declaration), declared in LeanPool/PhaseRetrieval/DimdPoly.lean, line 126: “Proves stable phase retrieval for the Gaussian L2 closure of finite d-dimensional Hermite-Fock polynomials at a fixed level, giving a uniform stability constant bounding the phase-aligned L2 distance by the L2 distance of magnitudes.” Its source, as the card gives it: “R. Balan, P. Casazza, D. Edidin, On signal reconstruction without phase, Appl. Comput. Harmon. Anal. 20 (2006), 345-356, doi:10.1016/j.acha.2005.07.001.”FockSPR.orthogonalReduction_exists_phase(theorem), declared in LeanPool/PhaseRetrieval/Constant.lean, line 61: “Proves the phase-aligned one-dimensional Fock-space local stability estimate, producing a unit phase for which the L2 distance to one is controlled by the magnitude defect.”FockSPR.orthogonalReduction_core(theorem), declared in LeanPool/PhaseRetrieval/Constant.lean, line 49: “Proves the quantitative centered core estimate bounding the Gaussian Fock norm of a polynomial with small norm by the magnitude defect against one.”FockSPR.LocalFockSPR(theorem), declared in LeanPool/PhaseRetrieval/Constant/Internal/MainTheorem.lean, line 784: “Proves the local Fock-space stable phase retrieval coercivity estimate for centered polynomials.”DimdPolyShowcaseChallenge.HermitePoly(def), declared in LeanPool/PhaseRetrieval/DimdPoly.lean, line 60: “Defines the normalized one-variable complex Hermite-Fock basis polynomial.”DimdPolyShowcaseChallenge.TrueHermiteFunctions(def), declared in LeanPool/PhaseRetrieval/DimdPoly.lean, line 116: “Defines the Gaussian L2 closure of finite Hermite-Fock polynomials at a fixed level.”
Project
- Authors: Susanna Bertolini, Jaume de Dios Pont.
- Source: Stable phase retrieval for Hermite-Fock expansions by Susanna Bertolini, Jaume de Dios Pont.
- Project repository: susannabertolini/PhaseRetrieval.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 42C05, 46E22, 94A12.
- In Lean Pool: LeanPool/PhaseRetrieval, from the card LeanPool/projects/phaseretrieval.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.