Ks_eq_zero_of_dist_le

lemma Ks_eq_zero_of_dist_le {s : ℤ} {x y : X} (hxy : x ≠ y)    (h : dist x y ≤ defaultD a ^ (s - 1) / 4) :    Ks s x y = 0 := by  rw [Ks_def]  simp only [mul_eq_zero, ofReal_eq_zero]  right  rw [psi_eq_zero_iff (one_lt_realD (X := X)) (dist_pos.mpr hxy),    mem_nonzeroS_iff (one_lt_realD (X := X)) (dist_pos.mpr hxy)]  simp only [mem_Ioo, not_and_or, not_lt]  left  rw [mul_comm]  apply mul_le_of_le_mul_inv₀ (by positivity) (by positivity)  simp only [mul_inv_rev, zpow_neg, inv_inv]  have heq : (D : ℝ)⁻¹ * 4⁻¹ * ↑D ^ s = defaultD a ^ (s - 1) / 4 := by    ring_nf    rw [← zpow_neg_one, zpow_add₀ (by simp)]  exact heq ▸ h