exceptional_set_carleson

theorem exceptional_set_carleson {f : ℝ → ℂ} (periodic_f : f.Periodic (2 * π))  {q : ℝ≥0∞} (hq : 1 < q) (hf : MemLp f q (volume.restrict (Set.Ioc 0 (2 * π))))  {δ ε : NNReal} (δpos : 0 < δ) (εpos : 0 < ε) :    ∃ N₀, distribution (fun x ↦ ⨆ N > N₀, ‖f x - S_ N f x‖ₑ) δ (volume.restrict (Set.Ioc 0 (2 * π))) ≤ ε := by  set p := (min (3 / 2) q).toNNReal with p_def  have : min (3 / 2) q ≠ ⊤ := by    apply ne_of_lt    rw [min_lt_iff]    left    refine div_lt_top (by simp) (by simp)  have hp : p ∈ Set.Ioo 1 2 := by    rw [p_def]    simp only [Set.mem_Ioo]    constructor    · rw [← coe_lt_iff_lt_toNNReal this, lt_min_iff]      simp only [ENNReal.coe_one]      symm      use hq      exact (ENNReal.lt_div_iff_mul_lt (by simp) (by simp)).mpr (by simp; norm_num)    · apply toNNReal_lt_of_lt_coe      simp only [coe_ofNat, inf_lt_iff]      left      refine div_lt_of_lt_mul ?_      norm_num  have hf : MemLp f p (volume.restrict (Set.Ioc 0 (2 * π))) := by    apply MemLp.mono_exponent hf    rw [p_def, coe_toNNReal this]    exact min_le_right _ _  have meas_f : AEStronglyMeasurable f :=    periodic_f.aestronglyMeasurable (t := 0) (by simp [hf.1])  have one_lt_p : (1 : ENNReal) < p := by simp [hp.1]  have δ2pos : 0 < δ / 2 := by positivity  have δ4pos : 0 < δ / 4 := by positivity  have ε2pos : 0 < ε / 2 := by positivity  have ε4pos : 0 < ε / 4 := by positivity  /- Approximate f by a smooth f₀. -/  obtain ⟨f₀, contDiff_f₀, periodic_f₀, hf₀⟩ :=    close_smooth_approx_periodic_Lp one_lt_p.le (by simp) hf      (lt_min (C_distribution_le_of_eLpNorm_le_pos (p := p) δ4pos ε2pos)        (C_control_approximation_effect_pos (p := p) δ2pos ε2pos))  obtain ⟨N₀, hN₀⟩ := fourierConv_ofTwiceDifferentiable periodic_f₀    ((contDiff_infty.mp (contDiff_f₀)) 2) δ4pos  /- This is a classical "epsilon third" argument. -/  use N₀  have : ∀ᶠx in (ae (volume.restrict (Set.Ioc 0 (2 * π)))), ⨆ N > N₀, ‖f x - S_ N f x‖ₑ      ≤ ‖f x - f₀ x‖ₑ + (⨆ N > N₀, ‖f₀ x - S_ N f₀ x‖ₑ) + ⨆ N, ‖S_ N (f₀ - f) x‖ₑ := by    rw [ae_restrict_iff' measurableSet_Ioc]    filter_upwards with x hx    apply iSup_le    intro N    apply iSup_le    intro hN    calc ‖f x - S_ N f x‖ₑ      _ = ‖(f x - f₀ x) + (f₀ x - S_ N f₀ x) + (S_ N f₀ x - S_ N f x)‖ₑ := by ring_nf      _ ≤ ‖(f x - f₀ x) + (f₀ x - S_ N f₀ x)‖ₑ + ‖S_ N f₀ x - S_ N f x‖ₑ := enorm_add_le ..      _ ≤ ‖f x - f₀ x‖ₑ + ‖f₀ x - S_ N f₀ x‖ₑ + ‖S_ N f₀ x - S_ N f x‖ₑ :=        add_le_add_left (enorm_add_le ..) _      _ ≤ ‖f x - f₀ x‖ₑ + (⨆ N > N₀, ‖f₀ x - S_ N f₀ x‖ₑ) + ⨆ N, ‖S_ N (f₀ - f) x‖ₑ := by        gcongr        · exact le_iSup₂_of_le N hN (le_of_eq rfl)        · apply le_iSup_of_le N          rw [partialFourierSum_sub (contDiff_f₀.continuous.intervalIntegrable _ _)]          · rfl          rw [intervalIntegrable_iff_integrableOn_Ioc_of_le two_pi_pos.le]          apply hf.integrable (by simp [hp.1.le])  calc _    _ ≤ distribution        (fun x ↦ ‖f x - f₀ x‖ₑ + (⨆ N > N₀, ‖f₀ x - S_ N f₀ x‖ₑ) + ⨆ N, ‖S_ N (f₀ - f) x‖ₑ)        ((δ / 4) + (δ / 4) + (δ / 2)) (volume.restrict (Set.Ioc 0 (2 * π))) := by      apply distribution_mono      · filter_upwards [this] with x hx        simp [hx]      · norm_cast        ring_nf        rfl    _ ≤ distribution (fun x ↦ ‖f x - f₀ x‖ₑ) (δ / 4) (volume.restrict (Set.Ioc 0 (2 * π)))        + distribution (fun x ↦ ⨆ N > N₀, ‖f₀ x - S_ N f₀ x‖ₑ) (δ / 4) (volume.restrict (Set.Ioc 0 (2 * π)))        + distribution (fun x ↦ ⨆ N, ‖S_ N (f₀ - f) x‖ₑ) (δ / 2) (volume.restrict (Set.Ioc 0 (2 * π))) := by      apply distribution_add_le.trans      gcongr      exact distribution_add_le    _ ≤ ε / 2 + 0 + ε / 2 := by      gcongr      · norm_cast        apply distribution_le_of_eLpNorm_le (p := p) (by positivity) (by positivity [hp.1])          (meas_f.sub contDiff_f₀.continuous.aestronglyMeasurable).enorm.aestronglyMeasurable.restrict        simp only [eLpNorm_enorm]        apply hf₀.trans        simp      · simp only [gt_iff_lt, nonpos_iff_eq_zero]        rw [distribution_eq_zero_iff]        apply essSup_le_of_ae_le _        rw [EventuallyLE, ae_restrict_iff' measurableSet_Ioc]        filter_upwards with x hx        simp only [enorm_eq_self, iSup_le_iff]        intro N hN        rw [enorm_eq_nnnorm, ← nnnorm_norm]        norm_cast        calc _          _ ≤ ‖((δ / 4) : ℝ)‖₊ := by            apply nnnorm_le_nnnorm (by simp)            exact hN₀ N hN x (Set.Ioc_subset_Icc_self hx)          _ = δ / 4 := by simp      · norm_cast        apply control_approximation_effect (ε := ε / 2) δ2pos          (contDiff_f₀.continuous.aestronglyMeasurable.sub meas_f) (periodic_f₀.sub periodic_f) hp        rw [eLpNorm_sub_comm]        apply hf₀.trans        simp    _ = ε := by simp