theorem exceptional_set_carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : Function.Periodic f (2 * Real.pi)) {ε : ℝ} (εpos : 0 < ε) : ∃ E ⊆ Set.Icc 0 (2 * Real.pi), MeasurableSet E ∧ MeasureTheory.volume.real E ≤ ε ∧ ∃ (N₀ : ℕ), ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, ‖f x - partialFourierSum N f x‖ ≤ ε

theorem carleson_interval {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : Function.Periodic f (2 * Real.pi)) : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 (2 * Real.pi)), Filter.Tendsto (fun (x_1 : ℕ) => partialFourierSum x_1 f x) Filter.atTop (nhds (f x))

theorem Function.Periodic.ae_of_ae_restrict {T : ℝ} (hT : 0 < T) {a : ℝ} {P : ℝ → Prop} (hP : Function.Periodic P T) (h : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Ico a (a + T)), P x) : ∀ᵐ (x : ℝ), P 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))