TileStructure.Forest.correlation_separated_trees

lemma correlation_separated_trees (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)    (hg₁ : BoundedCompactSupport g₁) (hg₂ : BoundedCompactSupport g₂) :    ‖∫ x, adjointCarlesonSum (t u₁) g₁ x * conj (adjointCarlesonSum (t u₂) g₂ x)‖ₑ ≤    C7_4_4 a n *    eLpNorm ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₁ g₁) ·) 2 volume *    eLpNorm ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₂ g₂) ·) 2 volume := by  by_cases hd : Disjoint (𝓘 u₁ : Set X) (𝓘 u₂)  · simp [cst_disjoint hd hu₁ hu₂]  wlog h2u : 𝓘 u₁ ≤ 𝓘 u₂ generalizing u₁ u₂ g₁ g₂  · have hl := (le_or_ge_or_disjoint.resolve_left h2u).resolve_right hd    rw [disjoint_comm] at hd    convert this hu₂ hu₁ hu.symm hg₂ hg₁ hd hl using 1    · rw [← RCLike.enorm_conj (z := ∫ x, adjointCarlesonSum _ g₂ x * _)]      rw [← integral_conj]      congr      simp [mul_comm]    · rw [inter_comm]; ring  exact correlation_separated_trees_of_subset hu₁ hu₂ hu h2u hg₁ hg₂