Tile.correlation_zero_of_ne_subset

lemma correlation_zero_of_ne_subset {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ}    (hp : ¬(𝓘 p' : Set X) ⊆ ball (𝔠 p) (14 * D ^ 𝔰 p)) :    ‖∫ y, adjointCarleson p' g y * conj (adjointCarleson p g y)‖ₑ = 0 := by  contrapose! hp; rw [enorm_ne_zero] at hp  obtain ⟨y, hy⟩ := exists_ne_zero_of_integral_ne_zero hp  rw [mul_ne_zero_iff, map_ne_zero] at hy  refine Grid_subset_ball.trans fun x (mx : x ∈ ball (𝔠 p') (4 * D ^ 𝔰 p')) ↦ ?_  rw [mem_ball] at mx ⊢  calc    _ ≤ dist x (𝔠 p') + dist (𝔠 p') (𝔠 p) := dist_triangle ..    _ < 4 * D ^ 𝔰 p' + (5 * D ^ 𝔰 p' + 5 * D ^ 𝔰 p) := by      gcongr      exact dist_lt_of_not_disjoint_ball        (not_disjoint_iff.mpr ⟨_, range_support hy.1, range_support hy.2⟩)    _ ≤ 4 * D ^ 𝔰 p + (5 * D ^ 𝔰 p + 5 * D ^ 𝔰 p) := by gcongr <;> exact one_le_realD a    _ = _ := by ring