rcarleson'_restrict

lemma rcarleson'_restrict {p : ℝ≥0} (hp : p ∈ Set.Ioo 1 2) {f : ℝ → ℂ}  (f_periodic : f.Periodic (2 * π)) (hf : MemLp f p (volume.restrict (Set.Ioc 0 (2 * π)))) :    eLpNorm (T f) p (volume.restrict (Set.Ioc 0 (2 * π)))      ≤ 2 * (C_carleson_hasStrongType 4 p) * eLpNorm f p (volume.restrict (Set.Ioc 0 (2 * π))) := by  have meas_f : AEStronglyMeasurable f := by    rw [← zero_add (2 * π)] at hf    exact (f_periodic.aestronglyMeasurable hf.1)  have h : eLpNorm ((Set.Ioo (-1) (2 * π + 1)).indicator f) (↑p) volume      ≤ 2 * eLpNorm f (↑p) (volume.restrict (Set.Ioc 0 (2 * π))) := by    calc _        _ ≤ eLpNorm ((Set.Ioc (-1) (-1 + 2 * π)).indicator f) (↑p) volume            + eLpNorm ((Set.Ioc (-1 + 2 * π) (-1 + 2 * π + 2 * π)).indicator f) (↑p) volume := by          apply (eLpNorm_add_le _ _ (by simp [hp.1.le])).trans'          · apply eLpNorm_mono            intro x            rw [← Set.indicator_union_add_inter, Set.Ioc_inter_Ioc, Set.Ioc_union_Ioc_eq_Ioc]            · nth_rw 2 [Set.Ioc_eq_empty_of_le]              · simp only [Set.indicator_empty, Pi.add_apply, add_zero]                rw [norm_indicator_eq_indicator_norm, norm_indicator_eq_indicator_norm]                gcongr                intro x hx                use hx.1                linarith [hx.2, Real.two_le_pi]              · apply le_max_of_le_right                apply min_le_left            · linarith [Real.two_pi_pos]            · linarith [Real.two_pi_pos]          · rw [aestronglyMeasurable_indicator_iff measurableSet_Ioc]            exact meas_f.restrict          · rw [aestronglyMeasurable_indicator_iff measurableSet_Ioc]            exact meas_f.restrict        _ = 2 * eLpNorm f p (volume.restrict (Set.Ioc 0 (2 * π))) := by          rw [two_mul (eLpNorm _ _ _)]          rw [eLpNorm_indicator_eq_eLpNorm_restrict measurableSet_Ioc,            eLpNorm_indicator_eq_eLpNorm_restrict measurableSet_Ioc]          congr 1          · nth_rw 2 [← zero_add (2 * π)]            exact f_periodic.eLpNorm (by simp)          · nth_rw 4 [← zero_add (2 * π)]            exact f_periodic.eLpNorm (by simp)  calc _    _ = eLpNorm (T ((Set.Ioo (0 - 1) (2 * π + 1)).indicator f)) p (volume.restrict (Set.Ioc 0 (2 * π))) := by      apply eLpNorm_congr_ae      rw [Filter.EventuallyEq, ae_restrict_iff' measurableSet_Ioc]      filter_upwards with x hx      exact carlesonOperatorReal_eq_of_restrict_interval (Set.Ioc_subset_Icc_self hx)    _ ≤ eLpNorm (T ((Set.Ioo (-1) (2 * π + 1)).indicator f)) p volume := by      simp only [zero_sub]      exact eLpNorm_mono_measure _ Measure.restrict_le_self    _ ≤ (C_carleson_hasStrongType 4 p) * eLpNorm ((Set.Ioo (-1) (2 * π + 1)).indicator f) p volume := by      apply rcarleson' hp      rw [memLp_indicator_iff_restrict measurableSet_Ioo]      use meas_f.restrict      rw [← eLpNorm_indicator_eq_eLpNorm_restrict measurableSet_Ioo]      apply h.trans_lt      apply ENNReal.mul_lt_top (by simp) hf.2    _ ≤ 2 * (C_carleson_hasStrongType 4 p) * eLpNorm f p (volume.restrict (Set.Ioc 0 (2 * π))) := by      rw [mul_comm 2 (ENNReal.ofNNReal _), mul_assoc]      gcongr