Tile.range_support

lemma range_support {p : 𝔓 X} {g : X → ℂ} {y : X} (hpy : adjointCarleson p g y ≠ 0) :    y ∈ ball (𝔠 p) (5 * D ^ 𝔰 p) := by  simp only [adjointCarleson] at hpy  obtain ⟨x, hxE, hx0⟩ := exists_ne_zero_of_setIntegral_ne_zero hpy  have hxp : dist x (𝔠 p) < 4 * D ^ 𝔰 p := -- 6.2.13    Grid_subset_ball (mem_of_subset_of_mem (fun _ ha ↦ ha.1) hxE)  have hyx : dist y x ≤ 1 / 2 * D ^ 𝔰 p := by -- 6.2.14    have hK : Ks (𝔰 p) x y ≠ 0 := by      by_contra h0      simp only [h0, map_zero, zero_mul, ne_eq, not_true] at hx0    rw [dist_comm]    convert! (dist_mem_Icc_of_Ks_ne_zero hK).2 using 1    ring  have hpos := defaultD_pow_pos a (𝔰 p)  have hle : (9 : ℝ) / 2 < 5 := by norm_num  calc    _ ≤ dist y x + dist x (𝔠 p) := dist_triangle ..    _ ≤ 1 / 2 * D ^ 𝔰 p + 4 * D ^ 𝔰 p := add_le_add hyx hxp.le    _ < _ := by ring_nf; gcongr