Import anisotropic and classical Carleson formalization

LeanPool/CarlesonLT.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2026 Joris Roos. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joris Roos
+-/
+
+module
+
+/- Adapted for Lean Pool from roos-j/lean-lt-carleson. -/
+
+public import LeanPool.CarlesonLT.Auto.ModelOperator
+public import LeanPool.CarlesonLT.Auto.AnisotropicCarleson
+public import LeanPool.CarlesonLT.Auto.ParametricIntegralContDiff
+public import LeanPool.CarlesonLT.Auto.HardyLittlewoodMaximal
+public import LeanPool.CarlesonLT.Auto.ClassicalCarleson
+public import LeanPool.CarlesonLT.Defs
+public import LeanPool.CarlesonLT.Theorems
+
+/-!
+# Anisotropic Carleson bounds and almost-everywhere Fourier convergence
+
+Source: arxiv:1710.10962, doi:10.1007/s00041-018-09657-7, url:https://github.com/roos-j/lean-lt-carleson
+Authors: Joris Roos
+Status: verified
+Main declarations: `CarlesonLT.anisotropic_carleson`, `CarlesonLT.classical_carleson`
+Tags: harmonic-analysis, fourier-series, time-frequency-analysis, maximal-operators
+MSC: 42A20, 42B20, 42B25
+-/

LeanPool/CarlesonLT/Auto/ParametricIntegralContDiff.lean

@@ -0,0 +1,151 @@
+/-
+Copyright (c) 2026 Joris Roos. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joris Roos
+-/
+module
+
+/- Proofs generated by Claude under Joris Roos’s supervision; adapted for Lean Pool. -/
+
+public import Mathlib.Analysis.Calculus.ContDiff.Comp
+public import Mathlib.Analysis.Calculus.ParametricIntegral
+public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
+
+/-!
+# Smoothness of parametric integrals (the higher-order Leibniz integral rule)
+
+**Theorem (Leibniz integral rule, `C^k` version).** Let `E` be a finite-dimensional real normed
+space and `F` a real normed space, let `Φ : E × ℝ → F` be `C^k` (jointly), and suppose that
+    there is a compact set `K ⊆ ℝ`
+such that `Φ (x, t) = 0` whenever `t ∉ K`. Then the parametric integral
+`x ↦ ∫ t, Φ (x, t) dt` is `C^k` on `E`, and its derivative is obtained by differentiating under
+the integral sign.
+
+The first-order case is Mathlib's `hasFDerivAt_integral_of_dominated_of_fderiv_le`; the general
+case follows by induction on `k`, since the partial derivative `∂ₓΦ` is `C^{k-1}` and vanishes for
+`t ∉ K` as well.
+
+## References
+
+* Leibniz integral rule (differentiation under the integral sign):
+  <https://en.wikipedia.org/wiki/Leibniz_integral_rule>.
+* Mathlib: `hasFDerivAt_integral_of_dominated_of_fderiv_le` in
+  `Mathlib/Analysis/Calculus/ParametricIntegral.lean` (first-order version).
+-/
+
+@[expose] public section
+
+noncomputable section
+
+open MeasureTheory Set Metric
+
+namespace CarlesonLT.Auto
+
+universe u
+
+variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
+
+/-- The partial derivative in the parameter variable: `∂ₓΦ(x, t) = DΦ(x, t) ∘ (v ↦ (v, 0))`. -/
+def partialFst {F : Type u} [NormedAddCommGroup F] [NormedSpace ℝ F] (Φ : E × ℝ → F)
+    (p : E × ℝ) : E →L[ℝ] F :=
+  (fderiv ℝ Φ p).comp (ContinuousLinearMap.inl ℝ E ℝ)
+
+omit [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] in
+theorem integral_eq_setIntegral_of_vanish {F : Type u} [NormedAddCommGroup F] [NormedSpace ℝ F]
+    {Φ : E × ℝ → F} {K : Set ℝ} (hsupp : ∀ x t, t ∉ K → Φ (x, t) = 0) (x : E) :
+    ∫ t, Φ (x, t) = ∫ t in K, Φ (x, t) :=
+  (setIntegral_eq_integral_of_forall_compl_eq_zero fun t ht => hsupp x t ht).symm
+
+/-- Order `0`: the parametric integral of a continuous function vanishing off a compact set is
+continuous. -/
+theorem continuous_integral_of_vanish {F : Type u} [NormedAddCommGroup F] [NormedSpace ℝ F]
+    {Φ : E × ℝ → F} (hΦ : Continuous Φ) {K : Set ℝ} (hK : IsCompact K)
+    (hsupp : ∀ x t, t ∉ K → Φ (x, t) = 0) : Continuous fun x => ∫ t, Φ (x, t) := by
+  have : (fun x => ∫ t, Φ (x, t)) = fun x => ∫ t in K, Φ (x, t) :=
+    funext (integral_eq_setIntegral_of_vanish hsupp)
+  rw [this]
+  exact continuous_parametric_integral_of_continuous (f := fun x t => Φ (x, t))
+    (hΦ.comp continuous_id) hK
+
+omit [FiniteDimensional ℝ E] in
+theorem partialFst_vanish {F : Type u} [NormedAddCommGroup F] [NormedSpace ℝ F]
+    {Φ : E × ℝ → F} {K : Set ℝ} (hK : IsClosed K) (hsupp : ∀ x t, t ∉ K → Φ (x, t) = 0)
+    (x : E) {t : ℝ} (ht : t ∉ K) : partialFst Φ (x, t) = 0 := by
+  have hloc : Φ =ᶠ[nhds (x, t)] fun _ => 0 := by
+    have hopen : IsOpen {p : E × ℝ | p.2 ∉ K} := hK.isOpen_compl.preimage continuous_snd
+    filter_upwards [hopen.mem_nhds ht] with p hp
+    exact hsupp p.1 p.2 hp
+  unfold partialFst
+  rw [hloc.fderiv_eq, fderiv_const_apply, ContinuousLinearMap.zero_comp]
+
+omit [FiniteDimensional ℝ E] in
+theorem hasFDerivAt_partialFst {F : Type u} [NormedAddCommGroup F] [NormedSpace ℝ F]
+    {Φ : E × ℝ → F} (hΦ : Differentiable ℝ Φ) (x : E) (t : ℝ) :
+    HasFDerivAt (fun y => Φ (y, t)) (partialFst Φ (x, t)) x := by
+  have h1 : HasFDerivAt (fun y : E => (y, t)) (ContinuousLinearMap.inl ℝ E ℝ) x :=
+    hasFDerivAt_prodMk_left x t
+  exact (hΦ (x, t)).hasFDerivAt.comp x h1
+
+/-- The inductive step: differentiation under the integral sign. -/
+theorem hasFDerivAt_integral_of_vanish {F : Type u} [NormedAddCommGroup F] [NormedSpace ℝ F]
+    {Φ : E × ℝ → F} (hΦ : ContDiff ℝ 1 Φ) {K : Set ℝ} (hK : IsCompact K)
+    (hsupp : ∀ x t, t ∉ K → Φ (x, t) = 0) (x₀ : E) :
+    HasFDerivAt (fun x => ∫ t, Φ (x, t)) (∫ t, partialFst Φ (x₀, t)) x₀ := by
+  have hdiff : Differentiable ℝ Φ := hΦ.differentiable one_ne_zero
+  have hcont' : Continuous (partialFst Φ) :=
+    ((hΦ.continuous_fderiv one_ne_zero).clm_comp continuous_const)
+  -- a uniform bound for the partial derivative on `closedBall x₀ 1 × K`
+  have hcpt : IsCompact (closedBall x₀ 1 ×ˢ K) := (isCompact_closedBall x₀ 1).prod hK
+  obtain ⟨C, hC⟩ := hcpt.exists_bound_of_continuousOn hcont'.continuousOn
+  have hbound : ∀ t, ∀ x ∈ ball x₀ 1, ‖partialFst Φ (x, t)‖ ≤ K.indicator (fun _ => C) t := by
+    intro t x hx
+    by_cases ht : t ∈ K
+    · rw [indicator_of_mem ht]
+      exact hC (x, t) ⟨ball_subset_closedBall hx, ht⟩
+    · rw [indicator_of_notMem ht, partialFst_vanish hK.isClosed hsupp x ht, norm_zero]
+  have hint : ∀ x, Integrable fun t => Φ (x, t) := by
+    intro x
+    have hc : Continuous fun t => Φ (x, t) := hΦ.continuous.comp (Continuous.prodMk_right x)
+    refine hc.integrable_of_hasCompactSupport (HasCompactSupport.intro hK fun t ht => hsupp x t ht)
+  refine hasFDerivAt_integral_of_dominated_of_fderiv_le (ball_mem_nhds x₀ one_pos)
+    (Filter.Eventually.of_forall fun x => (hint x).aestronglyMeasurable) (hint x₀)
+    (hcont'.comp (Continuous.prodMk_right x₀)).aestronglyMeasurable
+    (Filter.Eventually.of_forall fun t x hx => hbound t x hx)
+    ((integrableOn_const hK.measure_lt_top.ne).integrable_indicator hK.measurableSet)
+    (Filter.Eventually.of_forall fun t x _ => hasFDerivAt_partialFst hdiff x t)
+
+omit [FiniteDimensional ℝ E] in
+theorem contDiff_partialFst {F : Type u} [NormedAddCommGroup F] [NormedSpace ℝ F]
+    {Φ : E × ℝ → F} {n : ℕ} (hΦ : ContDiff ℝ (n + 1) Φ) : ContDiff ℝ n (partialFst Φ) := by
+  unfold partialFst
+  exact (hΦ.fderiv_right (by norm_cast)).clm_comp contDiff_const
+
+/-- **Leibniz integral rule, finite order.** If `Φ : E × ℝ → F` is `C^n` and vanishes for `t`
+outside a compact set `K`, then `x ↦ ∫ Φ(x, t) dt` is `C^n`. -/
+theorem contDiff_integral_of_vanish_nat (n : ℕ) :
+    ∀ {F : Type u} [NormedAddCommGroup F] [NormedSpace ℝ F] {Φ : E × ℝ → F},
+      ContDiff ℝ n Φ → ∀ {K : Set ℝ}, IsCompact K → (∀ x t, t ∉ K → Φ (x, t) = 0) →
+        ContDiff ℝ n fun x => ∫ t, Φ (x, t) := by
+  induction n with
+  | zero =>
+    intro F _ _ Φ hΦ K hK hsupp
+    rw [Nat.cast_zero, contDiff_zero] at hΦ ⊢
+    exact continuous_integral_of_vanish hΦ hK hsupp
+  | succ n ih =>
+    intro F _ _ Φ hΦ K hK hsupp
+    rw [Nat.cast_succ, contDiff_succ_iff_hasFDerivAt]
+    refine ⟨fun x => ∫ t, partialFst Φ (x, t), ?_, fun x =>
+      hasFDerivAt_integral_of_vanish (hΦ.of_le (by exact_mod_cast Nat.le_add_left 1 n)) hK hsupp x⟩
+    exact ih (contDiff_partialFst hΦ) hK fun x t ht => partialFst_vanish hK.isClosed hsupp x ht
+
+/-- **Leibniz integral rule, `C^∞` version.** If `Φ : E × ℝ → F` is smooth and vanishes for `t`
+outside a compact set `K`, then `x ↦ ∫ Φ(x, t) dt` is smooth. -/
+theorem contDiff_integral_of_vanish {F : Type u} [NormedAddCommGroup F] [NormedSpace ℝ F]
+    {Φ : E × ℝ → F} (hΦ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) Φ) {K : Set ℝ}
+        (hK : IsCompact K)
+    (hsupp : ∀ x t, t ∉ K → Φ (x, t) = 0) :
+    ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) fun x => ∫ t, Φ (x, t) :=
+  contDiff_infty.mpr fun n =>
+    contDiff_integral_of_vanish_nat n (hΦ.of_le (by exact_mod_cast le_top)) hK hsupp
+
+end CarlesonLT.Auto

LeanPool/CarlesonLT/Defs.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2026 Joris Roos. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joris Roos
+-/
+module
+
+public import Mathlib.Analysis.Fourier.AddCircle
+public import Mathlib.Analysis.Fourier.FourierTransform
+public import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
+
+/-!
+
+Definition of Fourier partial sums, multiplier class, and Carleson operator.
+
+-/
+
+@[expose] public noncomputable section
+
+namespace CarlesonLT
+
+open Real Complex Finset ENNReal MeasureTheory Set EuclideanSpace
+open scoped InnerProductSpace FourierTransform
+
+/-- The partial sums `S_N f(x) = ∑_{k = -N}^{N} f̂(k) e^{ikx}` of the Fourier series. -/
+def fourierPartialSum (f : ℝ → ℂ) (N : ℕ) (x : ℝ) : ℂ :=
+  ∑ n ∈ Finset.Icc (-(N : ℤ)) N,
+    fourierCoeffOn two_pi_pos f n * fourier n (x : AddCircle (2 * π))
+
+@[inherit_doc EuclideanSpace]
+scoped notation "ℝ^" n:max => EuclideanSpace ℝ (Fin n)
+
+variable {n : ℕ}
+
+/-- The Carleson operator associated with a multiplier `m`. Note
+we use Mathlib's Fourier transform convention here with the `2*π` in the exponent.
+This does not affect boundedness statements. -/
+def carlesonOperator (m : ℝ^n → ℂ) (f : ℝ^n → ℂ) (x : ℝ^n) : ℝ≥0∞ :=
+  ⨆ N : ℝ^n, ‖∫ ξ, 𝓕 f ξ * 𝐞 (⟪x, ξ⟫_ℝ) * m (ξ - N)‖ₑ
+
+/-- The weak `L²` quasinorm `‖g‖_{2,∞} = sup_{t > 0} t |{x : |g(x)| > t}|^{1/2}`. -/
+def weakL2Norm {X : Type*} [MeasurableSpace X] (μ : Measure X) (g : X → ℝ≥0∞) : ℝ≥0∞ :=
+  ⨆ t : ℝ≥0∞, t * μ {x | t < g x} ^ (2⁻¹ : ℝ)
+
+/-- Anisotropic dilations `δ_λ x = (λ^{α₁} x₁, …, λ^{αₙ} xₙ)` -/
+def anisoDil (α : Fin n → ℕ) (t : ℝ) (x : ℝ^n) : ℝ^n :=
+  WithLp.toLp 2 (fun i ↦ t ^ α i * x i)
+
+/-- The anisotropic norm `ρ(x) = max {|xᵢ|^{1/αᵢ} : i = 1, …, n}` -/
+def anisoNorm (α : Fin n → ℕ) (x : ℝ^n) : ℝ := ⨆ i, |x i| ^ ((α i)⁻¹ : ℝ)
+
+/-- Bounded, `ν` times continuously differentiable,
+anisotropically homogeneous multipliers -/
+structure MultiplierClass (α : Fin n → ℕ) (ν : ℕ) (m : ℝ^n → ℂ) : Prop where
+  bounded : ∃ C : ℝ, ∀ ξ, ‖m ξ‖ ≤ C
+  contDiffOn : ContDiffOn ℝ ν m {0}ᶜ
+  homogeneous : ∀ ξ, ξ ≠ 0 → ∀ t : ℝ, 0 < t → m (anisoDil α t ξ) = m ξ
+
+/-- Multiplier norm
+`‖m‖_{𝓜^ν} = sup_{|β| ≤ ν} sup_{ρ(ξ)=1} |∂^β m(ξ)|`, where `∂^β m(ξ)`
+with `|β| = k` is the `k`-th derivative of `m`
+evaluated at standard basis vectors `e_{i₁}, …, e_{i_k}`. -/
+def multiplierNorm (α : Fin n → ℕ) (ν : ℕ) (m : ℝ^n → ℂ) : ℝ≥0∞ :=
+  ⨆ (k ≤ ν) (i : Fin k → Fin n) (ξ : ℝ^n) (_ : anisoNorm α ξ = 1),
+    ‖iteratedFDeriv ℝ k m ξ (fun j ↦ single (i j) 1)‖ₑ
+
+end CarlesonLT
+
+end

LeanPool/CarlesonLT/Imports.lean

@@ -0,0 +1,16 @@
+/-
+Copyright (c) 2026 Lean Pool contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Pool contributors
+-/
+module  -- shake: keep-all --deprecated_module: ignore
+
+-- Generated project imports; run `lake exe mk_all`.
+public import LeanPool.CarlesonLT
+public import LeanPool.CarlesonLT.Auto.AnisotropicCarleson
+public import LeanPool.CarlesonLT.Auto.ClassicalCarleson
+public import LeanPool.CarlesonLT.Auto.HardyLittlewoodMaximal
+public import LeanPool.CarlesonLT.Auto.ModelOperator
+public import LeanPool.CarlesonLT.Auto.ParametricIntegralContDiff
+public import LeanPool.CarlesonLT.Defs
+public import LeanPool.CarlesonLT.Theorems

LeanPool/CarlesonLT/Theorems.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 Joris Roos. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joris Roos
+-/
+module
+
+/- Adapted for Lean Pool from roos-j/lean-lt-carleson. -/
+
+public import LeanPool.CarlesonLT.Defs
+public import Mathlib.Analysis.Distribution.SchwartzSpace.Basic
+import LeanPool.CarlesonLT.Auto.ClassicalCarleson
+
+/-!
+This file contains the statements of the main theorems:
+`anisotropic_carleson` and `classical_carleson`
+-/
+
+@[expose] public section
+
+namespace CarlesonLT
+
+open CarlesonLT
+open MeasureTheory Filter Topology Function Real Set SchwartzMap
+
+variable {n : ℕ}
+
+/-- Theorem 1.1 of `arXiv:1710.10962` proving a weak (2,2) a priori bound for
+Carleson operators associated with anisotropic multipliers on `ℝ^n`. -/
+theorem anisotropic_carleson (α : Fin n → ℕ) (hα : ∀ i, 1 ≤ α i) (hn : 0 < n) (ν₀ : ℕ)
+    (hν₀ : 3 * (∑ i, α i) + 2 ≤ ν₀) :
+      ∃ C : ℝ, 0 < C ∧ ∀ (m : ℝ^n → ℂ), MultiplierClass α ν₀ m → ∀ f : 𝓢(ℝ^n, ℂ),
+        weakL2Norm volume (carlesonOperator m f) ≤
+          ENNReal.ofReal C * (multiplierNorm α ν₀ m) * eLpNorm f 2 volume :=
+  Auto.anisotropic_carleson α hα hn ν₀ hν₀
+
+/-- **Carleson's theorem.** The Fourier series of a `2π`-periodic `L²` function
+on `ℝ` converges pointwise almost everywhere. -/
+theorem classical_carleson (f : ℝ → ℂ) (hper : Periodic f (2 * π))
+    (hf : MemLp f 2 (volume.restrict (Ico 0 (2 * π)))) :
+    ∀ᵐ x, Tendsto (fun N ↦ fourierPartialSum f N x) atTop (𝓝 (f x)) :=
+  Auto.classical_carleson f hper hf
+
+end CarlesonLT

LeanPool/projects/carleson-lacey-thiele.yaml

@@ -0,0 +1,41 @@
+slug: carleson-lacey-thiele
+title: Anisotropic Carleson bounds and almost-everywhere Fourier convergence
+summary: >-
+  Weak (2,2) bounds for maximally modulated anisotropically homogeneous smooth
+  multipliers on Euclidean space, following the Lacey–Thiele time-frequency method,
+  and almost-everywhere convergence of the Fourier series of periodic L² functions.
+branch: harmonic analysis
+entry_module: LeanPool.CarlesonLT
+authors:
+- Joris Roos
+source:
+  url: https://github.com/roos-j/lean-lt-carleson
+  github_repo: roos-j/lean-lt-carleson
+  commit: a83052776113c6417432c594a29b98f3500091a4
+  arxiv: '1710.10962'
+  doi: 10.1007/s00041-018-09657-7
+license: Apache-2.0
+status: verified
+provenance: AI
+main_declarations:
+- CarlesonLT.anisotropic_carleson
+- CarlesonLT.classical_carleson
+main_results:
+- declaration: CarlesonLT.anisotropic_carleson
+  informal: >-
+    For positive integer anisotropies and sufficient multiplier smoothness, the
+    associated maximally modulated multiplier operator obeys a weak L² bound on
+    Schwartz functions, with a constant independent of the multiplier and function.
+- declaration: CarlesonLT.classical_carleson
+  informal: >-
+    The symmetric Fourier partial sums of a 2π-periodic function that is square
+    integrable on one period converge to the function almost everywhere on the real line.
+tags:
+- harmonic-analysis
+- fourier-series
+- time-frequency-analysis
+- maximal-operators
+msc:
+- 42A20
+- 42B20
+- 42B25