hasStrongType_maximalFunction

public theorem hasStrongType_maximalFunction    [BorelSpace X] [IsFiniteMeasureOnCompacts μ] [ProperSpace X] [μ.IsOpenPosMeasure]    {p₁ p₂ : ℝ≥0} (hp₁ : 0 < p₁) (hp₁₂ : p₁ < p₂) :    HasStrongType (maximalFunction (E := E) μ 𝓑 c r p₁) p₂ p₂ μ μ (C2_0_6 A p₁ p₂) := by  by_cases h : Nonempty X; swap  · have := not_nonempty_iff.mp h; intro _ _; simp  intro v mlpv  refine ⟨measurable_maximalFunction.aestronglyMeasurable, ?_⟩  have cp₁p : 0 < (p₁ : ℝ) := by positivity  have p₁n : p₁ ≠ 0 := by exact_mod_cast cp₁p.ne'  conv_lhs =>    enter [1, x]    rw [maximalFunction_eq_maximalFunction_one_rpow cp₁p, ← enorm_eq_self (maximalFunction ..)]  rw [eLpNorm_enorm_rpow _ (by positivity), ENNReal.ofReal_inv_of_pos cp₁p,    ENNReal.ofReal_coe_nnreal, ← div_eq_mul_inv, ← ENNReal.coe_div p₁n]  calc    _ ≤ (CMB A (p₂ / p₁) * eLpNorm (fun y ↦ ‖v y‖ ^ (p₁ : ℝ)) (p₂ / p₁) μ) ^ p₁.toReal⁻¹ := by      apply ENNReal.rpow_le_rpow _ (by positivity)      convert (hasStrongType_maximalFunction_one (μ := μ) _ (fun x ↦ ‖v x‖ ^ (p₁ : ℝ)) _).2      · rw [ENNReal.coe_div p₁n]      · rwa [lt_div_iff₀, one_mul]; exact cp₁p      · rw [ENNReal.coe_div p₁n]; exact mlpv.norm_rpow_div p₁    _ = _ := by      rw [ENNReal.mul_rpow_of_nonneg _ _ (by positivity), eLpNorm_norm_rpow _ cp₁p,        ENNReal.ofReal_coe_nnreal, ENNReal.div_mul_cancel (by positivity) (by simp),        ENNReal.rpow_rpow_inv (by positivity), ← ENNReal.coe_rpow_of_nonneg _ (by positivity),        C2_0_6]