hasWeakType_maximalFunction_equal_exponents

theorem hasWeakType_maximalFunction_equal_exponents [BorelSpace X] [SeparableSpace X]    {p : ℝ≥0} (hp : 0 < p) :    HasWeakType (maximalFunction (E := E) μ 𝓑 c r p) p p μ μ (A ^ ((2 / p : ℝ))) := by  intro v mlpv  constructor; · exact measurable_maximalFunction.aestronglyMeasurable  have cp : 0 < (p : ℝ) := by positivity  have p₁n : p ≠ 0 := by exact_mod_cast cp.ne'  conv_lhs =>    enter [1, x]    rw [maximalFunction_eq_maximalFunction_one_rpow cp]  have hmb_one : wnorm (maximalFunction μ 𝓑 c r 1 (‖v ·‖ ^ (p : ℝ))) 1 μ      ≤ ↑A ^ 2 * eLpNorm (fun x ↦ ‖v x‖ ^ (p : ℝ)) 1 μ := by    apply (hasWeakType_maximalFunction_one (fun x : X ↦ ‖v x‖ ^ (p : ℝ)) _).2    convert! MemLp.norm_rpow_div mlpv p    exact (ENNReal.div_self (coe_ne_zero.mpr p₁n) coe_ne_top).symm  unfold wnorm wnorm' distribution at hmb_one ⊢  simp only [one_ne_top, ↓reduceIte, enorm_eq_self, toReal_one, inv_one, rpow_one, iSup_le_iff,    coe_ne_top, coe_toReal] at hmb_one ⊢  intro t  by_cases ht : t = 0  · rw [ht]; simp  · apply (rpow_le_rpow_iff cp).mp    rw [ENNReal.mul_rpow_of_nonneg _ _ NNReal.zero_le_coe]    convert! hmb_one (t ^ (p : ℝ))    · exact (coe_rpow_of_ne_zero ht p).symm    · rw [rpow_inv_rpow (NNReal.coe_ne_zero.mpr p₁n)]      congr; ext x; rw [coe_rpow_of_ne_zero ht ↑p]; exact (lt_rpow_inv_iff cp)    · rw [eLpNorm_norm_rpow v cp, ENNReal.mul_rpow_of_nonneg _ _ NNReal.zero_le_coe,        div_eq_mul_inv, rpow_mul, rpow_inv_rpow (NNReal.coe_ne_zero.mpr p₁n), rpow_two]; simp