partialFourierSum_bound

lemma partialFourierSum_bound {g : ℝ → ℂ} (periodic_g : Function.Periodic g (2 * π))  (hg : IntervalIntegrable g volume 0 (2 * π)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) :    ‖S_ N g x‖ₑ ≤      operatorBound g x := by  have intervalIntegrable_g : IntervalIntegrable g volume (-π) (3 * π) := by    apply periodic_g.intervalIntegrable₀ Real.two_pi_pos.ne' hg  have decomposition : S_ N g x      = (  (∫ (y : ℝ) in (x - π)..(x + π),              g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))         + (∫ (y : ℝ) in (x - π)..(x + π),              g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))))        / (2 * π) := by    calc S_ N g x      _ = (∫ (y : ℝ) in (0 : ℝ)..(2 * π), g y * dirichletKernel' N (x - y)) / (2 * π) := by        rw [partialFourierSum_eq_conv_dirichletKernel' (intervalIntegrable_g.mono_set _)]        · ring        rw [Set.uIcc_of_le, Set.uIcc_of_le]        on_goal 1 => apply Set.Icc_subset_Icc        all_goals linarith [pi_pos]      _ = (∫ (y : ℝ) in (x - π)..(x + π), g y * dirichletKernel' N (x - y)) / (2 * π) := by        --Shift domain of integration using periodicity        congr 1        rw [← zero_add (2 * π), Function.Periodic.intervalIntegral_add_eq _ 0 (x - π)]        · congr 1          ring        exact (periodic_g.mul (dirichletKernel'_periodic.const_sub x))      _ = (  (∫ (y : ℝ) in (x - π)..(x + π), g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))           + (∫ (y : ℝ) in (x - π)..(x + π), g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))) / (2 * π) := by        --Split into two parts        rw [← intervalIntegral.integral_add (intervalIntegrable_mul_dirichletKernel'_max hx intervalIntegrable_g) (intervalIntegrable_mul_dirichletKernel'_max' hx intervalIntegrable_g)]        congr with y        ring  calc    _ ≤ (‖∫ y in (x - π)..(x + π), g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖ₑ        + ‖∫ y in (x - π)..(x + π), g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖ₑ) / ENNReal.ofReal (2 * π) := by      rw [decomposition, div_eq_mul_inv, enorm_mul, enorm_inv (by simp [pi_pos.ne']),        ← div_eq_mul_inv]      norm_cast; gcongr      · apply enorm_add_le      · rw [enorm_eq_nnnorm, Complex.nnnorm_real, ENNReal.ofReal_le_coe]        apply le_of_eq        norm_num [abs_eq_self.mpr Real.pi_pos.le]    _ ≤ (T g x + T (⇑conj ∘ g) x          + ENNReal.ofReal π * eLpNorm g 1 (volume.restrict (Set.Ioc 0 (2 * π))))            / ENNReal.ofReal (2 * π) := by      gcongr      · apply le_CarlesonOperatorReal intervalIntegrable_g hx      · apply intervalIntegral.enorm_integral_le_lintegral_enorm_uIoc.trans        rw [Set.uIoc_of_le (by linarith [pi_pos])]        simp_rw [enorm_mul]        calc _          _ ≤ ∫⁻ (y : ℝ) in Set.Ioc (x - π) (x + π), ‖g y‖ₑ * ‖π‖ₑ := by            apply setLIntegral_mono' (measurableSet_Ioc)            intro y hy            gcongr            rw [enorm_le_iff_norm_le, Real.norm_of_nonneg (by linarith [pi_pos])]            rw [Dirichlet_Hilbert_eq]            apply Dirichlet_Hilbert_diff            constructor <;> linarith [hy.1, hy.2]          _ = ENNReal.ofReal π * eLpNorm g 1 (volume.restrict (Set.Ioc 0 (2 * π))) := by            simp_rw [Real.enorm_eq_ofReal pi_pos.le, mul_comm _ (ENNReal.ofReal _)]            rw [lintegral_const_mul' _ _ ENNReal.ofReal_ne_top]            congr            have : x + π = x - π + 2 * π := by linarith            rw [this, Function.Periodic.setLIntegral_Ioc_add_eq _ _ 0, zero_add,              eLpNorm_one_eq_lintegral_enorm]            apply periodic_g.comp    _ = (T g x + T (conj ∘ g) x) / ENNReal.ofReal (2 * π)      + eLpNorm g 1 (volume.restrict (Set.Ioc 0 (2 * π))) / 2 := by      rw [ENNReal.add_div, mul_comm (ENNReal.ofReal _), mul_div_assoc]      congr      rw [← ENNReal.ofReal_div_of_pos Real.two_pi_pos, div_mul_cancel_right₀ Real.pi_pos.ne']      simp