lintegral_globalMaximalFunction_le

lemma lintegral_globalMaximalFunction_le (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q')    (bF : IsBounded F) (mF : MeasurableSet F) (mG : MeasurableSet G) :    ∫⁻ x in G, globalMaximalFunction volume 1 (F.indicator (1 : X → ℝ)) x ≤    C2_0_6 (defaultA a) 1 q * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by  calc    _ = ∫⁻ x, G.indicator 1 x * globalMaximalFunction volume 1 (F.indicator (1 : X → ℝ)) x := by      simp_rw [← indicator_eq_indicator_one_mul]; rw [lintegral_indicator mG]    _ ≤ eLpNorm (G.indicator (1 : X → ℝ≥0∞)) q' *        eLpNorm (globalMaximalFunction volume 1 (F.indicator (1 : X → ℝ))) q := by      apply lintegral_mul_le_eLpNorm_mul_eLqNorm      · rw [holderConjugate_coe_iff]; exact hqq'.symm      · exact aemeasurable_const.indicator mG      · exact measurable_maximalFunction.aemeasurable    _ ≤ volume G ^ (q' : ℝ)⁻¹ *        (C2_0_6 (defaultA a) 1 q * eLpNorm (F.indicator (1 : X → ℝ)) q) := by      gcongr      · rw [Pi.one_def]; convert! eLpNorm_indicator_const_le (1 : ℝ≥0∞) q'        rw [enorm_eq_self, coe_toReal, one_div, one_mul]      · refine (hasStrongType_maximalFunction zero_lt_one hq.1 _ ?_).2        rw [Pi.one_def]; exact memLp_indicator_const _ mF _ (.inr bF.measure_lt_top.ne)    _ ≤ _ := by      rw [← mul_assoc, mul_comm (_ ^ _)]; gcongr      rw [Pi.one_def]; convert! eLpNorm_indicator_const_le (1 : ℝ) q      rw [enorm_one, coe_toReal, one_div, one_mul]