distribution_carlesonOperatorReal_le

lemma distribution_carlesonOperatorReal_le {δ ε p : ℝ≥0} (δpos : 0 < δ)  (hp : p ∈ Set.Ioo 1 2) {g : ℝ → ℂ}  (g_periodic : g.Periodic (2 * π)) (g_measurable : AEStronglyMeasurable g)  (hg : eLpNorm g p (volume.restrict (Set.Ioc 0 (2 * π))) ≤ C_distribution_carlesonOperatorReal_le δ ε p) :    distribution (T g) δ (volume.restrict (Set.Ioc 0 (2 * π))) ≤ ε := by  apply distribution_le_of_eLpNorm_le δpos (zero_lt_one.trans hp.1)  · apply (carlesonOperatorReal_measurable g_measurable _).aestronglyMeasurable    intro x    have : Set.Ioo x (x + 2) ⊆ Set.Ioc x (x + (2 * π)) := by      apply Set.Ioo_subset_Ioc_self.trans'      apply Set.Ioo_subset_Ioo_right      linarith [Real.two_le_pi]    apply IntegrableOn.mono_set _ this    apply MemLp.integrable (q := p) (by simp [hp.1.le])    use g_measurable.restrict    rw [g_periodic.eLpNorm (s := 0) (by simp), zero_add]    apply hg.trans_lt    simp  · apply (rcarleson'_restrict hp g_periodic _).trans    · calc _        _ ≤ 2 * ↑(C_carleson_hasStrongType 4 p)              * ENNReal.ofNNReal (C_distribution_carlesonOperatorReal_le δ ε p) := by          gcongr        _ = C_distribution_le_of_eLpNorm_le δ ε p := by          unfold C_distribution_carlesonOperatorReal_le          norm_cast          rw [← mul_assoc, mul_inv_cancel₀ (mul_ne_zero (by simp) C_carleson_hasStrongType_pos.ne'),            one_mul]    · use g_measurable.restrict, hg.trans_lt (by simp)