theorem exceptional_set_carleson' {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : Function.Periodic f (2 * Real.pi)) {δ ε : NNReal} (δpos : 0 < δ) (εpos : 0 < ε) :
∃ (N₀ : ℕ),
MeasureTheory.distribution (fun (x : ℝ) => ⨆ (N : ℕ), ⨆ (_ : N > N₀), ‖f x - partialFourierSum N f x‖ₑ) (↑δ)
(MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))) ≤ ↑ε
theorem carleson_interval' {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : Function.Periodic f (2 * Real.pi)) :
∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi)), Filter.Tendsto (fun (x_1 : ℕ) => partialFourierSum x_1 f x) Filter.atTop (nhds (f x))
theorem classical_carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : Function.Periodic f (2 * Real.pi)) :
∀ᵐ (x : ℝ), Filter.Tendsto (fun (x_1 : ℕ) => partialFourierSum x_1 f x) Filter.atTop (nhds (f x))