dist_holderApprox_le

lemma dist_holderApprox_le {z : X} {R t : ℝ} (hR : 0 < R) {C : ℝ≥0} (ht : 0 < t) (h't : t ≤ 1)    {φ : X → ℂ} (hφ : support φ ⊆ ball z R) (h2φ : HolderOnWith C nnτ φ (ball z (2 * R))) (x : X) :    dist (φ x) (holderApprox R t φ x) ≤ (t/2) ^ τ * ((2 * R) ^ τ * C) := by  have φ_cont : Continuous φ := by    apply ContinuousOn.continuous_of_tsupport_subset (h2φ.continuousOn (nnτ_pos X)) isOpen_ball    apply (closure_mono hφ).trans (closure_ball_subset_closedBall.trans ?_)    exact closedBall_subset_ball (by linarith)  have : (∫ y, cutoff R t x y * φ x) / (∫ y, (cutoff R t x y : ℂ)) = φ x := by    rw [      show ∫ y, (cutoff R t x y : ℂ) * φ x = (∫ y, (cutoff R t x y : ℂ)) * φ x from integral_mul_const (φ x) _,      mul_div_cancel_left₀    ]    simpa only [ne_eq, ofReal_eq_zero, integral_complex_ofReal] using (integral_cutoff_pos hR ht).ne'  rw [dist_eq_norm, ← this, holderApprox, integral_complex_ofReal, ← sub_div,    ← integral_sub]; rotate_left  · apply (integrable_cutoff hR ht).ofReal.mul_const  · apply integrable_cutoff_mul hR ht φ_cont hφ  rw [norm_div, norm_real, div_le_iff₀]; swap  · exact ((integral_cutoff_pos hR ht)).trans_le (le_abs_self _)  calc    ‖∫ y, cutoff R t x y * φ x - cutoff R t x y * φ y‖  _ = ‖∫ y, cutoff R t x y * (φ x - φ y)‖ := by simp only [mul_sub]  _ ≤ ∫ y, ‖cutoff R t x y * (φ x - φ y)‖ := norm_integral_le_integral_norm _  _ ≤ ∫ y, cutoff R t x y * (C * (t * R) ^ τ) := by    apply integral_mono_of_nonneg    · filter_upwards with y using (by positivity)    · apply (integrable_cutoff hR ht).mul_const    filter_upwards with y    rcases le_total (dist x y) (t * R) with hxy | hxy    -- Case 1: |x - y| ≤ t * R, then cutoff is non-negative.    · simp only [norm_mul, norm_real, Real.norm_eq_abs, defaultτ, norm_real,        _root_.abs_of_nonneg cutoff_nonneg]      gcongr      · exact cutoff_nonneg      rcases le_or_gt (2 * R) (dist x z) with hx | hx      · have : dist x y ≤ R := by nlinarith        have : dist x z ≤ dist x y + dist y z := dist_triangle _ _ _        have xm : x ∉ support φ := fun h ↦ by linarith [mem_ball.1 (hφ h)]        have ym : y ∉ support φ := fun h ↦ by linarith [mem_ball.1 (hφ h)]        simp only [notMem_support.mp xm, notMem_support.mp ym, sub_self, norm_zero, ge_iff_le]        positivity      rcases le_or_gt (2 * R) (dist y z) with hy | hy      · have : dist x y ≤ R := by nlinarith        have : dist y z ≤ dist x y + dist x z := dist_triangle_left y z x        have xm : x ∉ support φ := fun h ↦ by linarith [mem_ball.1 (hφ h)]        have ym : y ∉ support φ := fun h ↦ by linarith [mem_ball.1 (hφ h)]        simp only [notMem_support.mp xm, notMem_support.mp ym, sub_self, norm_zero, ge_iff_le]        positivity      rw [← dist_eq_norm]      apply h2φ.dist_le_of_le hx hy hxy    -- Case 2: |x - y| > t * R, and cutoff is zero.    · have : cutoff R t x y = 0 := by        simp only [cutoff, sup_eq_left, tsub_le_iff_right, zero_add]        rwa [one_le_div₀ (by positivity)]      simp [this]  _ = ((t / 2) * (2 * R)) ^τ * C * ∫ y, cutoff R t x y := by    rw [integral_mul_const, show (t / 2) * (2 * R) = t * R by ring]    ring  _ ≤ ((t / 2) * (2 * R)) ^ τ * C * ‖∫ (x_1 : X), cutoff R t x x_1‖ := by    gcongr    exact Real.le_norm_self _  _ = (t / 2) ^ τ * ((2 * R) ^ τ * C) * ‖∫ (x_1 : X), cutoff R t x x_1‖ := by    rw [Real.mul_rpow]    · ring    · positivity    · positivity