Source indexedtheorem · leanprover/lean4:v4.32.0

classical_carleson

Carleson.Classical.ClassicalCarleson · Carleson/Classical/ClassicalCarleson.lean:131 to 143

Mathematical statement

Exact Lean statement

theorem classical_carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π)) :
    ∀ᵐ x, Tendsto (S_ · f x) atTop (𝓝 (f x))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem classical_carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (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_interval' cont_f periodic_f