HolderOnWith.of_iHolENorm_ne_top

lemma HolderOnWith.of_iHolENorm_ne_top (ht : 0 ≤ t) (hφ : iHolENorm φ z R t ≠ ⊤) :    HolderOnWith (iHolNNNorm φ z R t / R.toNNReal ^ t) t.toNNReal φ (ball z R) := by  intro x hx y hy  have hR : 0 < R := by    simp only [mem_ball] at hx    apply dist_nonneg.trans_lt hx  rcases eq_or_ne x y with rfl | hne  · simp  have : (ENNReal.ofReal R) ^ t * (‖φ x - φ y‖ₑ / (edist x y) ^ t) ≤ iHolENorm φ z R t := calc    _ ≤ (ENNReal.ofReal R) ^ t *        ⨆ (x ∈ ball z R) (y ∈ ball z R) (_ : x ≠ y), (‖φ x - φ y‖ₑ / (edist x y) ^ t) := by      gcongr      simp only [ne_eq, le_iSup_iff, iSup_le_iff]      tauto    _ ≤ _ := le_add_self  rw [edist_eq_enorm_sub, ENNReal.coe_div (by simp [hR]), iHolNNNorm, coe_toNNReal hφ,    ← ENNReal.div_le_iff_le_mul (by simp [hne]) (by simp [edist_ne_top]),    ENNReal.le_div_iff_mul_le (by simp [hR]) (by simp)]  apply this.trans_eq'  rw [ENNReal.coe_rpow_of_ne_zero (by simp [hR]), Real.coe_toNNReal t ht, ENNReal.ofReal, mul_comm]