Tile.correlation_le_of_empty_inter

lemma correlation_le_of_empty_inter {p p' : 𝔓 X} {g : X → ℂ}    (hinter : ¬(ball (𝔠 p') (5 * D ^ 𝔰 p') ∩ ball (𝔠 p) (5 * D ^ 𝔰 p)).Nonempty) :    ‖∫ y, adjointCarleson p' g y * conj (adjointCarleson p g y)‖ₑ ≤    C6_1_5 a * (1 + edist_(p') (𝒬 p') (𝒬 p)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) /    volume (𝓘 p : Set X) * (∫⁻ y in E p', ‖g y‖ₑ) * ∫⁻ y in E p, ‖g y‖ₑ := by  suffices ‖∫ y, adjointCarleson p' g y * conj (adjointCarleson p g y)‖ₑ = 0 by    rw [this]; exact zero_le  simp only [inter_nonempty, not_exists, not_and_or] at hinter  rw [enorm_eq_zero]  apply integral_eq_zero_of_ae (Eq.eventuallyEq _)  ext y  rcases hinter y with hp'y | hpy  · have hp'0 : adjointCarleson p' g y = 0 := by      by_contra hy      exact hp'y (range_support hy)    simp [hp'0, zero_mul]  · have hp'0 : adjointCarleson p g y = 0 := by      by_contra hy      exact hpy (range_support hy)    simp [hp'0, map_zero, mul_zero]