isCancellative_of_norm_integral_exp_le

lemma isCancellative_of_norm_integral_exp_le (τ : ℝ) [CompatibleFunctions ℝ X A]    (h : ∀ {x : X} {r : ℝ} {φ : X → ℂ} (_hr : 0 < r) (_h1 : iLipENorm φ x r ≠ ∞)    (_h2 : support φ ⊆ ball x r) {f g : Θ X},      ‖∫ x in ball x r, exp (I * (f x - g x)) * φ x‖ ≤      A * volume.real (ball x r) * iLipNNNorm φ x r * (1 + dist_{x, r} f g) ^ (-τ)) :    IsCancellative X τ := by  constructor  intro x r φ hr h1 h2 f g  convert ENNReal.ofReal_le_ofReal (h (x := x) (r := r) (φ := φ) hr h1 h2 (f := f) (g := g))  · rw [ofReal_norm]    congr 1    rw [setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)]    have : φ y = 0 := by      apply notMem_support.1      contrapose! hy      exact h2 hy    simp [this]  · rw [ENNReal.ofReal_mul (by positivity), ENNReal.ofReal_mul (by positivity),      ENNReal.ofReal_mul (by positivity)]    congr    · simp    · simp only [Measure.real, ofReal_toReal measure_ball_ne_top]    · simp [iLipNNNorm, coe_toNNReal h1]    · rw [← ENNReal.ofReal_rpow_of_pos (by positivity)]      congr      rw [ENNReal.ofReal_add zero_le_one dist_nonneg]      simp [edist_dist]