iLipENorm_holderApprox'

lemma iLipENorm_holderApprox' {z : X} {R t : ℝ} (ht : 0 < t) (h't : t ≤ 1)    {C : ℝ≥0} {φ : X → ℂ} (hc : Continuous φ) (hφ : φ.support ⊆ ball z R) (hC : ∀ x, ‖φ x‖ ≤ C) :    iLipENorm (holderApprox R t φ) z (2 * R) ≤      2 ^ (4 * a) * (ENNReal.ofReal t) ^ (-1 - a : ℝ) * C := by  let C' : ℝ≥0 := 2 ^ (4 * a) * (t.toNNReal) ^ (-1 - a : ℝ) * C  have : 2 ^ (4 * a) * (ENNReal.ofReal t) ^ (-1 - a : ℝ) * C = C' := by    simp only [ENNReal.coe_mul, ENNReal.coe_pow, ENNReal.coe_ofNat, C', ENNReal.ofReal]    congr    rw [ENNReal.coe_rpow_of_ne_zero]    simpa using ht  rw [this]  apply iLipENorm_le  · intro x hx    have h'R : 0 < 2 * R := pos_of_mem_ball hx    have hR : 0 < R := by linarith    apply (holderApprox_le hR ht hC x).trans    simp only [NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_ofNat, NNReal.coe_rpow, C', ← mul_assoc]    have : (C : ℝ) = 1 * 1 * C := by simp    conv_lhs => rw [this]    gcongr    · calc        (1 : ℝ)      _ = 2⁻¹ * (2 ^ 1) := by norm_num      _ ≤ 2⁻¹ * (2 ^ (4 * a)) := by        gcongr        · norm_num        · have := four_le_a X          linarith    · apply Real.one_le_rpow_of_pos_of_le_one_of_nonpos (by simp [ht]) (by simp [h't])      linarith  · intro x hx x' hx' hne    have h'R : 0 < 2 * R := pos_of_mem_ball hx    have hR : 0 < R := by linarith    simp only [NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_ofNat, NNReal.coe_rpow,      Real.coe_toNNReal', ht.le, sup_of_le_left, ← mul_assoc, C']    exact norm_holderApprox_sub_le hR ht h't hc hφ hC