Plain-language statement
For every continuous, -periodic function , the symmetric partial Fourier sums converge to for almost every .
Exact Lean statement
theorem classical_carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π)) :
∀ᵐ x, Tendsto (S_ · f x) atTop (𝓝 (f x))Formal artifact
Lean source
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- Project
- Carleson formalization
- License
- Apache-2.0
- Commit
- 74ef907d6bdb
- Source
- Carleson/Classical/ClassicalCarleson.lean:131-143
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Adjoint Carleson adjoint
adjointCarleson_adjoint
Plain-language statement
adjointCarleson is the adjoint of carlesonOn.
Source project: Carleson formalization
Person-level attribution pending.
Ae tendsto zero of distribution le
ae_tendsto_zero_of_distribution_le
Plain-language statement
Suppose that, for every error threshold and every measure tolerance , one can choose so that the set where exceeds has measure at most . Then converges to for almost every .
Source project: Carleson formalization
Person-level attribution pending.
Antichain operator
antichain_operator
Plain-language statement
For an antichain of pairwise incomparable tiles, and measurable functions and bounded by the indicators of and , the pairing of with the Carleson sum over is controlled by the norms of and and by positive powers of the two tile-density parameters. Concretely, the bound is
Source project: Carleson formalization
Person-level attribution pending.