carleson_hunt_two_pi

theorem carleson_hunt_two_pi {f : AddCircle (2 * π) → ℂ} {p : ℝ≥0∞} (hp : 1 < p) (hf : MemLp f p) :    ∀ᵐ x, Tendsto (partialFourierSum' · f x) atTop (𝓝 (f x)) := by  wlog meas_f : Measurable f generalizing f  · rcases hf.1 with ⟨g, meas_g, hfg⟩    have hg : MemLp g p volume := by      rwa [memLp_congr_ae hfg.symm]    have := this hg meas_g.measurable    filter_upwards [hfg, this]    intro x hx    rw [hx]    intro h    convert h using 2 with N    unfold partialFourierSum'    congr with n x    congr 2    have hfg' : f =ᶠ[ae AddCircle.haarAddCircle] g := by      convert hfg using 1      exact (Measure.ae_ennreal_smul_measure_eq (ofReal_ne_zero_iff.mpr two_pi_pos)        AddCircle.haarAddCircle).symm    rw [fourierCoeff_congr_ae hfg']  set g := fun (x : ℝ) ↦ f x  have periodic_g : g.Periodic (2 * π) := by    unfold g    intro x    simp  have hg : MemLp g p (volume.restrict (Set.Ioc 0 (2 * π))) := by    unfold g    nth_rw 2 [← zero_add (2 * π)]    constructor    · apply (hf.1.comp_measurePreserving (AddCircle.measurePreserving_mk _ _))    · rw [eLpNorm_eq_eLpNorm_liftIoc' hf.1]      exact hf.2  apply ae_tendsto_zero_of_distribution_le  intro δ δpos ε εpos  rcases exceptional_set_carleson periodic_g hp hg δpos εpos with ⟨N₀, hN₀⟩  use N₀  apply hN₀.trans'  unfold distribution  rw [Measure.restrict_apply' measurableSet_Ioc,    ← AddCircle.volume_preimage_equivIoc (by exact (measurableSet_superlevelSet (by fun_prop)))]  apply measure_mono  intro x  simp only [gt_iff_lt, enorm_eq_self, Set.mem_setOf_eq]  intro hx  simp only [Set.preimage_setOf_eq, Set.mem_setOf_eq]  convert hx using 5 with N hN  unfold g  simp only [AddCircle.coe_equivIoc]  rw [← partialFourierSum'_eq_partialFourierSum_apply N _]  · simp only [AddCircle.coe_equivIoc]  · nth_rw 1 [← zero_add (2 * π)]    apply Subtype.mem