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

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.