spectral_projection_bound

lemma spectral_projection_bound {f : ℝ → ℂ} {n : ℕ} (hmf : AEMeasurable f) :    eLpNorm ((Ioc 0 (2 * π)).indicator (partialFourierSum n f)) 2 ≤    eLpNorm ((Ioc 0 (2 * π)).indicator f) 2 := by  -- Proof by massaging the statement of `spectral_projection_bound_lp` into this.  by_cases! hf_L2 : eLpNorm ((Ioc 0 (2 * π)).indicator f) 2 = ⊤  · rw [hf_L2]    exact OrderTop.le_top _  rw [← lt_top_iff_ne_top] at hf_L2  have lift_MemLp : MemLp (liftIoc (2 * π) 0 f) 2 haarAddCircle := by    unfold MemLp    constructor    · rw [haarAddCircle_eq_smul_volume]      apply AEStronglyMeasurable.smul_measure      exact hmf.aestronglyMeasurable.liftIoc (2 * π) 0    · rw [haarAddCircle_eq_smul_volume, eLpNorm_smul_measure_of_ne_top (by trivial),        eLpNorm_liftIoc _ _ hmf.aestronglyMeasurable, smul_eq_mul, zero_add]      apply ENNReal.mul_lt_top _ hf_L2      rw [← ENNReal.ofReal_inv_of_pos Real.two_pi_pos]      apply ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg ENNReal.ofReal_ne_top  let F : Lp ℂ 2 haarAddCircle :=    MemLp.toLp (AddCircle.liftIoc (2 * π) 0 f) lift_MemLp  have lp_version := spectral_projection_bound_lp (N := n) F  rw [Lp.norm_def, Lp.norm_def,    ENNReal.toReal_le_toReal (Lp.eLpNorm_ne_top (partialFourierSumLp 2 n F)) (Lp.eLpNorm_ne_top F)]    at lp_version  rw [← zero_add (2 * π), ← eLpNorm_liftIoc _ _ hmf.aestronglyMeasurable,    ← eLpNorm_liftIoc _ _ partialFourierSum_uniformContinuous.continuous.aestronglyMeasurable,    volume_eq_smul_haarAddCircle,    eLpNorm_smul_measure_of_ne_top (by trivial), eLpNorm_smul_measure_of_ne_top (by trivial),    smul_eq_mul, smul_eq_mul, ENNReal.mul_le_mul_iff_right (by simp [Real.pi_pos]) (by finiteness)]  have ae_eq_right : F =ᶠ[ae haarAddCircle] liftIoc (2 * π) 0 f := MemLp.coeFn_toLp _  have ae_eq_left : partialFourierSumLp 2 n F =ᶠ[ae haarAddCircle]      liftIoc (2 * π) 0 (partialFourierSum n f) :=    Filter.EventuallyEq.symm (partialFourierSum_aeeq_partialFourierSumLp 2 n f lift_MemLp)  rw [← eLpNorm_congr_ae ae_eq_right, ← eLpNorm_congr_ae ae_eq_left]  exact lp_version