Source indexedtheorem · leanprover/lean4:v4.32.0

carleson_hunt_real

Carleson.Classical.CarlesonHunt · Carleson/Classical/CarlesonHunt.lean:146 to 159

Mathematical statement

Exact Lean statement

theorem carleson_hunt_real {f : ℝ → ℂ} (periodic_f : f.Periodic (2 * π))
  {p : ℝ≥0∞} (hp : 1 < p) (hf : MemLp f p (volume.restrict (Set.Ioc 0 (2 * π)))) :
    ∀ᵐ x, Tendsto (S_ · f x) atTop (𝓝 (f x))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem carleson_hunt_real {f : ℝ → ℂ} (periodic_f : f.Periodic (2 * π))  {p : ℝ≥0∞} (hp : 1 < p) (hf : MemLp f p (volume.restrict (Set.Ioc 0 (2 * π)))) :    ∀ᵐ x, Tendsto (S_ · f x) atTop (𝓝 (f x)) := by  -- Reduce to a.e. convergence on [0,2π]  apply @Function.Periodic.ae_of_ae_restrict _ two_pi_pos 0  · rw [Function.Periodic]    intro x    conv => pattern S_ _ _ _; rw [partialFourierSum_periodic]    conv => pattern f _; rw [periodic_f]  apply ae_restrict_of_ae_eq_of_ae_restrict Ico_ae_eq_Icc.symm  rw [zero_add]  -- Show a.e. convergence on [0,2π]  rw [Measure.restrict_congr_set Ioc_ae_eq_Icc.symm]  exact carleson_hunt_interval periodic_f hp hf