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))