Source indexedlemma · leanprover/lean4:v4.32.0

dist_mem_Ioo_of_Ks_ne_zero

Carleson.Psi · Carleson/Psi.lean:345 to 351

Mathematical statement

Exact Lean statement

lemma dist_mem_Ioo_of_Ks_ne_zero {s : ℤ} {x y : X} (h : Ks s x y ≠ 0) :
    dist x y ∈ Ioo ((D ^ (s - 1) : ℝ) / 4) (D ^ s / 2)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma dist_mem_Ioo_of_Ks_ne_zero {s : ℤ} {x y : X} (h : Ks s x y ≠ 0) :    dist x y ∈ Ioo ((D ^ (s - 1) : ℝ) / 4) (D ^ s / 2) := by  simp only [Ks, zpow_neg, ne_eq, mul_eq_zero, ofReal_eq_zero] at h  have dist_mem_Ioo := support_ψ (one_lt_realD X) ▸ mem_support.2 (not_or.1 h).2  rwa [mem_Ioo, ← div_eq_inv_mul, lt_div_iff₀ (zpow_realD_pos s),    div_lt_iff₀ (zpow_realD_pos s), mul_inv, mul_assoc, inv_mul_eq_div (4 : ℝ), ← zpow_neg_one,    ← zpow_add₀ (realD_pos a).ne.symm, neg_add_eq_sub, ← div_eq_inv_mul] at dist_mem_Ioo