TileStructure.Forest.row_correlation

lemma row_correlation (lj : j < 2 ^ n) (lj' : j' < 2 ^ n) (hn : j ≠ j')    (hf₁ : BoundedCompactSupport f₁) (nf₁ : f₁.support ⊆ G)    (hf₂ : BoundedCompactSupport f₂) (nf₂ : f₂.support ⊆ G) :    ‖∫ x, adjointCarlesonRowSum t j f₁ x * conj (adjointCarlesonRowSum t j' f₂ x)‖ₑ ≤    C7_7_3 a n * eLpNorm f₁ 2 volume * eLpNorm f₂ 2 volume := by  classical  let W := ({u | u ∈ t.rowDecomp j} : Finset _) ×ˢ ({u' | u' ∈ t.rowDecomp j'} : Finset _)  let N₁ (w : 𝔓 X × 𝔓 X) := eLpNorm ((𝓘 w.1 ∩ 𝓘 w.2 : Set X).indicator    (adjointBoundaryOperator t w.1 ((𝓘 w.1 : Set X).indicator f₁)) ·) 2 volume  let N₂ (w : 𝔓 X × 𝔓 X) := eLpNorm ((𝓘 w.1 ∩ 𝓘 w.2 : Set X).indicator    (adjointBoundaryOperator t w.2 ((𝓘 w.2 : Set X).indicator f₂)) ·) 2 volume  have N₁_bound : (∑ w ∈ W, N₁ w ^ (2 : ℝ)) ^ (2 : ℝ)⁻¹ ≤ C7_4_3 a * eLpNorm f₁ 2 volume := by    unfold W N₁; rw [Finset.sum_product]    exact row_correlation_aux hf₁ nf₁  have N₂_bound : (∑ w ∈ W, N₂ w ^ (2 : ℝ)) ^ (2 : ℝ)⁻¹ ≤ C7_4_3 a * eLpNorm f₂ 2 volume := by    unfold W N₂; rw [Finset.sum_product, Finset.sum_comm]; dsimp only    conv_lhs => enter [1, 2, u', 2, u]; rw [inter_comm]    exact row_correlation_aux hf₂ nf₂  calc    _ = ‖∫ x, ∑ u with u ∈ rowDecomp t j, ∑ u' with u' ∈ rowDecomp t j',        adjointCarlesonSum (t u) f₁ x * conj (adjointCarlesonSum (t u') f₂ x)‖ₑ := by      congr! with x; unfold adjointCarlesonRowSum      rw [Finset.sum_mul]; congr! with u mu; rw [← Finset.mul_sum, map_sum]    _ = ‖∑ u with u ∈ rowDecomp t j, ∫ x, ∑ u' with u' ∈ rowDecomp t j',        adjointCarlesonSum (t u) f₁ x * conj (adjointCarlesonSum (t u') f₂ x)‖ₑ := by      congr      exact integral_finsetSum _ fun u mu ↦        (BoundedCompactSupport.finset_sum fun u' mu' ↦          hf₁.adjointCarlesonSum.mul hf₂.adjointCarlesonSum.conj).integrable    _ = ‖∑ u with u ∈ rowDecomp t j, ∑ u' with u' ∈ rowDecomp t j', ∫ x,        adjointCarlesonSum (t u) f₁ x * conj (adjointCarlesonSum (t u') f₂ x)‖ₑ := by      congr! with u mu      exact integral_finsetSum _ fun u' mu' ↦        (hf₁.adjointCarlesonSum.mul hf₂.adjointCarlesonSum.conj).integrable    _ ≤ ∑ u with u ∈ rowDecomp t j, ‖∑ u' with u' ∈ rowDecomp t j', ∫ x,        adjointCarlesonSum (t u) f₁ x * conj (adjointCarlesonSum (t u') f₂ x)‖ₑ := enorm_sum_le _ _    _ ≤ ∑ u with u ∈ rowDecomp t j, ∑ u' with u' ∈ rowDecomp t j',        ‖∫ x, adjointCarlesonSum (t u) f₁ x * conj (adjointCarlesonSum (t u') f₂ x)‖ₑ := by      gcongr with u mu; exact enorm_sum_le _ _    _ ≤ ∑ u with u ∈ rowDecomp t j, ∑ u' with u' ∈ rowDecomp t j',        ‖∫ x, adjointCarlesonSum (t u) ((𝓘 u : Set X).indicator f₁) x *        conj (adjointCarlesonSum (t u') ((𝓘 u' : Set X).indicator f₂) x)‖ₑ := by      congr! 5 with u mu u' mu' x      rw [Finset.mem_filter_univ] at mu mu'      rw [adjoint_tile_support2_sum_partial (mem_forest_of_mem mu),        adjoint_tile_support2_sum_partial (mem_forest_of_mem mu')]    _ ≤ ∑ u with u ∈ rowDecomp t j, ∑ u' with u' ∈ rowDecomp t j',        C7_4_4 a n *        eLpNorm ((𝓘 u ∩ 𝓘 u' : Set X).indicator          (adjointBoundaryOperator t u ((𝓘 u : Set X).indicator f₁)) ·) 2 volume *        eLpNorm ((𝓘 u ∩ 𝓘 u' : Set X).indicator          (adjointBoundaryOperator t u' ((𝓘 u' : Set X).indicator f₂)) ·) 2 volume := by      gcongr with u mu u' mu'      rw [Finset.mem_filter_univ] at mu mu'      refine correlation_separated_trees (mem_forest_of_mem mu) (mem_forest_of_mem mu') ?_        (hf₁.indicator coeGrid_measurable) (hf₂.indicator coeGrid_measurable)      exact (pairwiseDisjoint_rowDecomp lj lj' hn).ne_of_mem mu mu'    _ = C7_4_4 a n * ∑ w ∈ W, N₁ w * N₂ w := by      rw [← Finset.sum_product', Finset.mul_sum]; congr! 1 with w mw; rw [mul_assoc]    _ ≤ C7_4_4 a n *        (∑ w ∈ W, N₁ w ^ (2 : ℝ)) ^ (2 : ℝ)⁻¹ * (∑ w ∈ W, N₂ w ^ (2 : ℝ)) ^ (2 : ℝ)⁻¹ := by      rw [← one_div, mul_assoc]; gcongr      exact ENNReal.inner_le_Lp_mul_Lq _ _ _ Real.HolderConjugate.two_two    _ ≤ C7_4_4 a n * (C7_4_3 a * eLpNorm f₁ 2 volume) * (C7_4_3 a * eLpNorm f₂ 2 volume) := by      gcongr    _ = _ := by rw [C7_7_3, sq, ENNReal.coe_mul, ENNReal.coe_mul]; ring