Tile.correlation_le_of_nonempty_inter

lemma correlation_le_of_nonempty_inter (ha : 4 ≤ a) {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ}    (hg : Measurable g) (hg1 : ∀ x, ‖g x‖ ≤ G.indicator 1 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  calc    _ ≤ _ := bound_6_2_26 hg hg1    _ ≤ ∫⁻ z in E p' ×ˢ E p,        C6_1_5 a * (1 + edist_(p') (𝒬 p') (𝒬 p)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) /        volume (𝓘 p : Set X) * ‖g z.1‖ₑ * ‖g z.2‖ₑ := by      refine setLIntegral_mono' (measurableSet_E.prod measurableSet_E) fun z hz ↦ ?_      apply (I12_le ha hle hinter ⟨_, hz.1⟩ ⟨_, hz.2⟩).trans      gcongr ?_ * _ * _; exact bound_6_2_29 ha _    _ = _ := by      simp only [mul_assoc]      rw [lintegral_const_mul _ (by fun_prop)]; congr 1      rw [← lintegral_prod_mul (by fun_prop) (by fun_prop), prod_restrict]; rfl