modulated_averaged_projection

lemma modulated_averaged_projection {g : ℝ → ℂ} {n : ℕ} (hmg : AEMeasurable g) :    eLpNorm ((Ioc 0 (2 * π)).indicator (approxHilbertTransform n g)) 2 ≤    eLpNorm ((Ioc 0 (2 * π)).indicator g) 2 := by  unfold approxHilbertTransform  by_cases hn : n = 0  · simp [hn]  rw [funext (indicator_const_mul _ _ _)]  change eLpNorm ((n : ℂ)⁻¹ • _) _ _ ≤ _  rw [eLpNorm_const_smul _ _ _ _, ← Finset.sum_fn, Finset.indicator_sum,    enorm_inv (Nat.cast_ne_zero.mpr hn), ← one_mul (eLpNorm (indicator _ _) _ _),    ← ENNReal.inv_mul_cancel (by simp [hn]) (enorm_ne_top (x := (n : ℂ))), mul_assoc]  refine mul_le_mul_right (le_trans (eLpNorm_sum_le ?_ one_le_two) ?_) _  · refine fun i _ ↦ Measurable.indicator ?_ measurableSet_Ioc |>.aestronglyMeasurable    exact partialFourierSum_uniformContinuous.continuous.measurable.modulationOperator _  trans ∑ i ∈ Finset.Ico n (2 * n), eLpNorm ((Ioc 0 (2 * π)).indicator g) 2 volume; swap  · simp [← ofReal_norm, Nat.sub_eq_of_eq_add (two_mul n)]  refine Finset.sum_le_sum (fun i _ ↦ ?_)  rw [eLpNorm_indicator_modulationOperator, ← eLpNorm_indicator_modulationOperator g (-i)]  exact spectral_projection_bound (hmg.modulationOperator (-i))