eLpNorm_le_M14

lemma eLpNorm_le_M14 {p : 𝔓 X} (mp : p ∈ 𝔄) {x₀ : X} (hx : x₀ ∈ ball (𝔠 p) (14 * D ^ 𝔰 p))    {r : ℝ} (hr : 0 < r) :    eLpNorm ((ball (𝔠 p) (14 * D ^ 𝔰 p)).indicator (‖g ·‖ₑ)) (ENNReal.ofReal r) volume ≤      volume (ball (𝔠 p) (14 * D ^ 𝔰 p)) ^ r⁻¹ * M14 𝔄 r g x₀ := by  have vpos : 0 < volume (ball (𝔠 p) (14 * D ^ 𝔰 p)) := by    apply measure_ball_pos; unfold defaultD; positivity  rw [mul_comm (_ ^ _), ← ENNReal.div_le_iff_le_mul]; rotate_left  · left    rw [← inv_ne_top, ← ENNReal.rpow_neg]    finiteness  · exact Or.inl <| (by finiteness)  rw [ENNReal.div_eq_inv_mul, ← ENNReal.rpow_neg_one, ← ENNReal.rpow_mul, mul_comm _ (-1),    ENNReal.rpow_mul, ENNReal.rpow_neg_one,    eLpNorm_eq_lintegral_rpow_enorm_toReal (by simpa) (by finiteness)]  simp_rw [ENNReal.toReal_ofReal hr.le, one_div]  rw [← ENNReal.mul_rpow_of_nonneg _ _ (by positivity), M14, maximalFunction]  conv_lhs =>    enter [1, 2, 2, x]    rw [enorm_eq_self, ← Function.comp_apply (f := (· ^ r)),      ← indicator_comp_of_zero (g := fun x ↦ x ^ r) (by simpa using hr)]  rw [lintegral_indicator measurableSet_ball, ← ENNReal.div_eq_inv_mul, ← setLAverage_eq]  simp only [Function.comp_apply]; refine le_trans ?_ (le_iSup₂ p mp); rw [indicator_of_mem hx]