carleson_hunt'

theorem carleson_hunt' {T : ℝ} [hT : Fact (0 < T)] {f : AddCircle T → ℂ} {p : ℝ≥0∞} (hp : 1 < p)  (hf : MemLp f p) :    ∀ᵐ x, Tendsto (partialFourierSum' · f x) atTop (𝓝 (f x)) := by  set g := fun (x : AddCircle (2 * π)) ↦    f (AddCircle.equivAddCircle (2 * π) T two_pi_pos.ne' hT.out.ne' x)  have hg : MemLp g p := by    unfold g    rw [← memLp_haarAddCircle_iff] at *    apply hf.comp_measurePreserving AddCircle.measurePreserving_equivAddCircle  have h := carleson_hunt_two_pi hp hg  rw [AddCircle.volume_eq_smul_haarAddCircle] at *  rw [Measure.ae_ennreal_smul_measure_eq (ofReal_ne_zero_iff.mpr two_pi_pos)] at h  apply Measure.ae_smul_measure  convert AddCircle.measurePreserving_equivAddCircle.quasiMeasurePreserving.ae h using 4 with x N  · exact partialFourierSum'_comp_equivAddCircle.symm  · unfold g    congr    exact (AddEquiv.symm_apply_eq      (AddCircle.equivAddCircle (2 * π) T (two_pi_pos.ne') (hT.out.ne'))).mp rfl