TileStructure.Forest.correlation_distant_tree_parts

lemma correlation_distant_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_5 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  classical  calc    _ ≤ _ := cdtp_le_iHolENorm hu₁ hu₂ hu h2u hf₁ hf₂    _ ≤ ∑ J ∈ 𝓙₅ t u₁ u₂, C2_0_5 a * volume (ball (c J) (8 * D ^ s J)) *        (C7_5_4 a * P7_5_4 t u₁ u₂ f₁ f₂ J) * (1 + C7_5_11 a n) ^ (-(2 * a^2 + a^3 : ℝ)⁻¹) := by      gcongr ∑ _ ∈ _, _ * ?_ * ?_ with J mJ <;> rw [mem_toFinset] at mJ      · rw [← mul_assoc, show (2 : ℝ) * 8 = 16 by norm_num]        exact holder_correlation_tree hu₁ hu₂ hu h2u mJ hf₁ hf₂      · apply ENNReal.rpow_le_rpow_of_nonpos (by rw [Left.neg_nonpos_iff]; positivity)        gcongr; rw [edist_comm, edist_nndist, ENNReal.coe_le_coe]        exact lower_oscillation_bound hu₁ hu₂ hu h2u mJ    _ = C2_0_5 a * C7_5_4 a * (1 + C7_5_11 a n) ^ (-(2 * a^2 + a^3 : ℝ)⁻¹) *        ∑ J ∈ 𝓙₅ t u₁ u₂, volume (ball (c J) (8 * D ^ s J)) * P7_5_4 t u₁ u₂ f₁ f₂ J := by      rw [Finset.mul_sum]; congr! 1 with J mJ; ring    _ ≤ C2_0_5 a * C7_5_4 a *        (2 ^ ((𝕔 / 4) * a ^ 3 + 7) * 2 ^ (-(Z * n : ℝ) / (4 * a ^ 2 + 2 * a ^ 3))) *        ∑ J ∈ 𝓙₅ t u₁ u₂,          2 ^ (6 * a) * volume (ball (c J) (8⁻¹ * D ^ s J)) * P7_5_4 t u₁ u₂ f₁ f₂ J := by      gcongr with J mJ      · exact C7_5_11_binomial_bound (four_le_a X)      · convert! measure_ball_two_le_same_iterate (μ := volume) (c J) (8⁻¹ * D ^ s J) 6 using 2        · rw [← mul_assoc, show (2 : ℝ) ^ 6 * 8⁻¹ = 8 by norm_num]        · unfold defaultA; norm_cast; rw [← pow_mul, mul_comm]    _ = C2_0_5 a * C7_5_4 a * 2 ^ ((𝕔 / 4) * a ^ 3 + 7 + 6 * a) *        2 ^ (-(Z * n : ℝ) / (4 * a ^ 2 + 2 * a ^ 3)) *        ∑ J ∈ 𝓙₅ t u₁ u₂, ∫⁻ x in ball (c J) (8⁻¹ * D ^ s J), P7_5_4 t u₁ u₂ f₁ f₂ J := by      simp_rw [mul_assoc (_ ^ (6 * a)), ← Finset.mul_sum, ← mul_assoc]; congr 1      · ring      · congr! with J mJ; rw [setLIntegral_const, mul_comm]    _ ≤ C7_4_5 a n * ∑ J ∈ 𝓙₅ t u₁ u₂, ∫⁻ x in ball (c J) (8⁻¹ * D ^ s J),        adjointBoundaryOperator t u₁ f₁ x * adjointBoundaryOperator t u₂ f₂ x := by      gcongr ?_ * ∑ _ ∈ _, ?_ with J mJ      · rw [show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl]        simp_rw [← ENNReal.coe_rpow_of_ne_zero two_ne_zero, ← ENNReal.coe_pow, ← ENNReal.coe_mul,          ENNReal.coe_le_coe]        exact le_C7_4_5 (four_le_a X)      · exact setLIntegral_mono' measurableSet_ball fun x mx ↦          P7_5_4_le_adjointBoundaryOperator_mul mx    _ ≤ C7_4_5 a n * ∑ J ∈ 𝓙₅ t u₁ u₂, ∫⁻ x in J,        adjointBoundaryOperator t u₁ f₁ x * adjointBoundaryOperator t u₂ f₂ x := by      gcongr with J mJ; refine (ball_subset_ball ?_).trans ball_subset_Grid      change _ ≤ (D : ℝ) ^ s J / 4; rw [div_eq_inv_mul]; gcongr; norm_num    _ = C7_4_5 a n * ∫⁻ x in 𝓘 u₁,        adjointBoundaryOperator t u₁ f₁ x * adjointBoundaryOperator t u₂ f₂ x := by      simp_rw [← union_𝓙₅ hu₁ hu₂ hu h2u, ← mem_toFinset]      congr 1; refine (lintegral_biUnion_finset ?_ (fun _ _ ↦ coeGrid_measurable) _).symm      rw [coe_toFinset]; exact pairwiseDisjoint_𝓙₅    _ = C7_4_5 a n * ∫⁻ x,        (𝓘 u₁ : Set X).indicator (adjointBoundaryOperator t u₁ f₁) x *        (𝓘 u₁ : Set X).indicator (adjointBoundaryOperator t u₂ f₂) x := by      conv_rhs => enter [2, 2, x]; rw [← inter_indicator_mul _ _ x, inter_self]      rw [lintegral_indicator coeGrid_measurable]    _ ≤ _ := by      rw [mul_assoc]; gcongr      apply ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm inferInstance <;>        refine AEMeasurable.indicator ?_ coeGrid_measurable      · have af₁ := hf₁.aestronglyMeasurable        refine (af₁.adjointCarlesonSum.enorm.add ?_).add af₁.enorm        exact measurable_maximalFunction.aemeasurable      · have af₂ := hf₂.aestronglyMeasurable        refine (af₂.adjointCarlesonSum.enorm.add ?_).add af₂.enorm        exact measurable_maximalFunction.aemeasurable