enorm_holderApprox_sub_le

lemma enorm_holderApprox_sub_le {z : X} {R t : ℝ} (hR : 0 < R) (ht : 0 < t) (h't : t ≤ 1)    {φ : X → ℂ} (hφ : support φ ⊆ ball z R) (x : X) :    ‖φ x - holderApprox R t φ x‖ₑ ≤ ENNReal.ofReal (t/2) ^ τ * iHolENorm φ z (2 * R) τ := by  rcases eq_or_ne (iHolENorm φ z (2 * R) τ) ∞ with h | h  · apply le_top.trans_eq    symm    simp only [defaultτ] at h    simp [h, ENNReal.mul_eq_top, ht]  have : iHolENorm φ z (2 * R) τ = ENNReal.ofReal (iHolNNNorm φ z (2 * R) τ) := by    simp only [iHolNNNorm, ENNReal.ofReal_coe_nnreal, ENNReal.coe_toNNReal h]  rw [ENNReal.ofReal_rpow_of_pos (by linarith), this, ← ENNReal.ofReal_mul (by positivity),    ← ofReal_norm, ← dist_eq_norm]  apply ENNReal.ofReal_le_ofReal  apply dist_holderApprox_le hR ht h't hφ    (by simpa [nnτ_def] using HolderOnWith.of_iHolENorm_ne_top (τ_nonneg X) h) x |>.trans_eq  simp [field, NNReal.coe_div, hR.le]