This file contains the Carleson-Hunt theorem, a generalization of classical_carleson.

theorem instFactLtRealOfNatHMulPi_carleson_5 : Fact (0 < 2 * Real.pi)

theorem exceptional_set_carleson {f : ℝ → ℂ} (periodic_f : Function.Periodic f (2 * Real.pi)) {q : ENNReal} (hq : 1 < q) (hf : MeasureTheory.MemLp f q (MeasureTheory.volume.restrict (Set.Ioc 0 (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_hunt_interval {f : ℝ → ℂ} (periodic_f : Function.Periodic f (2 * Real.pi)) {p : ENNReal} (hp : 1 < p) (hf : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (Set.Ioc 0 (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 carleson_hunt_real {f : ℝ → ℂ} (periodic_f : Function.Periodic f (2 * Real.pi)) {p : ENNReal} (hp : 1 < p) (hf : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi)))) : ∀ᵐ (x : ℝ), Filter.Tendsto (fun (x_1 : ℕ) => partialFourierSum x_1 f x) Filter.atTop (nhds (f x))

theorem classical_carleson_from_carleson_hunt_real : ClassicalCarleson

theorem instFactLtRealOfNatHMulPi_carleson_6 : Fact (0 < 2 * Real.pi)

theorem carleson_hunt_two_pi {f : AddCircle (2 * Real.pi) → ℂ} {p : ENNReal} (hp : 1 < p) (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : ∀ᵐ (x : AddCircle (2 * Real.pi)), Filter.Tendsto (fun (x_1 : ℕ) => (partialFourierSum' x_1 f) x) Filter.atTop (nhds (f x))

theorem carleson_hunt' {T : ℝ} [hT : Fact (0 < T)] {f : AddCircle T → ℂ} {p : ENNReal} (hp : 1 < p) (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : ∀ᵐ (x : AddCircle T), Filter.Tendsto (fun (x_1 : ℕ) => (partialFourierSum' x_1 f) x) Filter.atTop (nhds (f x))

theorem carleson_hunt {T : ℝ} [hT : Fact (0 < T)] {f : AddCircle T → ℂ} {p : ENNReal} (hp : 1 < p) (hf : MeasureTheory.MemLp f p AddCircle.haarAddCircle) : ∀ᵐ (x : AddCircle T), Filter.Tendsto (fun (x_1 : ℕ) => (partialFourierSum' x_1 f) x) Filter.atTop (nhds (f x))

Classical theorem of Carleson and Hunt asserting a.e. convergence of the partial Fourier sums for L^p functions for p > 1. This is a strengthening of classical_carleson, and not officially part of the blueprint.