TileStructure.Forest.correlation_near_tree_parts

lemma correlation_near_tree_parts (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂)    (hf₁ : BoundedCompactSupport f₁) (hf₂ : BoundedCompactSupport f₂) :    ‖∫ x, adjointCarlesonSum (t u₁) f₁ x * conj (adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f₂ x)‖ₑ ≤    C7_4_6 a n *    eLpNorm ((𝓘 u₁ : Set X).indicator (adjointBoundaryOperator t u₁ f₁) ·) 2 volume *    eLpNorm ((𝓘 u₁ : Set X).indicator (adjointBoundaryOperator t u₂ f₂) ·) 2 volume := by  set U := (𝓘 u₁ : Set X)  calc    _ = ‖∫ x, conj (adjointCarlesonSum (t u₁) f₁ x) *        adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f₂ x‖ₑ := by      rw [← RCLike.enorm_conj, ← integral_conj]      congr! 3 with x      rw [map_mul, RingHomCompTriple.comp_apply, RingHom.id_apply]    _ = ‖∫ x, conj (U.indicator (adjointCarlesonSum (t u₁) (U.indicator f₁)) x) *        adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f₂ x‖ₑ := by      congr! 5 with x; rw [adjoint_tile_support2_sum hu₁]    _ = ‖∫ x, conj (adjointCarlesonSum (t u₁) (U.indicator f₁) x) *        (U.indicator (adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f₂) x)‖ₑ := by      congr! 3 with x      rw [indicator_eq_indicator_one_mul, map_mul, conj_indicator, map_one, mul_comm _ (conj _),        mul_assoc, ← indicator_eq_indicator_one_mul]    _ = ‖∫ x, conj (U.indicator f₁ x) *        carlesonSum (t u₁) (U.indicator (adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f₂)) x‖ₑ := by      rw [← adjointCarlesonSum_adjoint (hf₂.adjointCarlesonSum.indicator coeGrid_measurable)        (hf₁.indicator coeGrid_measurable)]    _ ≤ C7_2_1 a * eLpNorm (approxOnCube (𝓙 (t u₁))          (‖U.indicator (adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f₂) ·‖)) 2 volume *        eLpNorm (approxOnCube (𝓛 (t u₁)) (‖U.indicator f₁ ·‖)) 2 volume :=      tree_projection_estimate (hf₂.adjointCarlesonSum.indicator coeGrid_measurable)        (hf₁.indicator coeGrid_measurable) hu₁    _ ≤ C7_2_1 a *        (C7_6_2 a n * eLpNorm ((𝓘 u₁ : Set X).indicator (maximalFunction volume 𝓑 c𝓑 r𝓑 1 f₂ ·)) 2 volume) *        eLpNorm (U.indicator f₁ ·) 2 volume := by      rw [cntp_approxOnCube_eq hu₁]; gcongr      · exact bound_for_tree_projection hu₁ hu₂ hu h2u hf₂      · exact eLpNorm_approxOnCube_two_le_self (hf₁.indicator coeGrid_measurable) pairwiseDisjoint_𝓛    _ ≤ _ := by      conv_rhs => rw [mul_comm (C7_4_6 a n : ℝ≥0∞), mul_rotate]      rw [C7_4_6, ENNReal.coe_mul, ← mul_assoc]; gcongr      all_goals        refine eLpNorm_mono_enorm fun x ↦ ?_        simp only [enorm_eq_self, enorm_indicator_eq_indicator_enorm, adjointBoundaryOperator]        apply indicator_le_indicator      · rw [← add_rotate]; exact le_add_self      · exact le_add_self