TileStructure.Forest.e764_preCS

lemma e764_preCS (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂)    (hf : BoundedCompactSupport f) :    eLpNorm (approxOnCube (𝓙₆ t u₁) (‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f ·‖)) 2 volume ≤    C2_1_3 a * 2 ^ (4 * a) * ∑ k ∈ Finset.Icc ⌊C7_6_3 a n⌋ (2 * S),    (∑ J ∈ (𝓙₆ t u₁).toFinset, (volume (J : Set X))⁻¹ *    (∑ I with s I = s J - k ∧ Disjoint (I : Set X) (𝓘 u₁) ∧      ¬Disjoint ↑J (ball (c I) (8 * D ^ s I)),    ∫⁻ y in J, (ball (c I) (8 * D ^ s I)).indicator 1 y *      maximalFunction volume 𝓑 c𝓑 r𝓑 1 f y) ^ 2) ^ (2 : ℝ)⁻¹ := by  calc    _ ≤ _ := e763 hu₁ hu₂ hu h2u hf    _ = ∑ k ∈ Finset.Icc ⌊C7_6_3 a n⌋ (2 * S),        (∑ J ∈ (𝓙₆ t u₁).toFinset, (volume (J : Set X))⁻¹ *        (∫⁻ y in J, ∑ I, ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with          ¬Disjoint ↑J (ball (𝔠 p) (8 * D ^ 𝔰 p)) ∧ 𝔰 p = s J - k ∧ 𝓘 p = I,        ‖adjointCarleson p f y‖ₑ) ^ 2) ^ (2 : ℝ)⁻¹ := by      congr! with k mk J mJ y      conv_rhs => enter [2, I, 1, 1, p]; rw [← and_assoc]      conv_rhs => enter [2, I]; rw [← Finset.filter_filter]      exact (Finset.sum_fiberwise _ _ _).symm    _ ≤ ∑ k ∈ Finset.Icc ⌊C7_6_3 a n⌋ (2 * S),        (∑ J ∈ (𝓙₆ t u₁).toFinset, (volume (J : Set X))⁻¹ *        (∫⁻ y in J, ∑ I with          s I = s J - k ∧ Disjoint (I : Set X) (𝓘 u₁) ∧ ¬Disjoint ↑J (ball (c I) (8 * D ^ s I)),        ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with          ¬Disjoint ↑J (ball (𝔠 p) (8 * D ^ 𝔰 p)) ∧ 𝓘 p = I,        ‖adjointCarleson p f y‖ₑ) ^ 2) ^ (2 : ℝ)⁻¹ := by      gcongr with k mk J mJ y      nth_rw 1 [← Finset.filter_true (@Finset.univ (Grid X) _) (h := fun _ ↦ instDecidableTrue)]      simp_rw [Finset.sum_finset_product_filter_right]      refine Finset.sum_le_sum_of_subset fun r hr ↦ ?_      obtain ⟨I, p⟩ := r      simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_univ, true_and] at hr ⊢      obtain ⟨mp, h₁, h₂, h₃⟩ := hr; dsimp only [𝔠, 𝔰] at h₁ h₂ h₃ ⊢; rw [h₃] at h₁ h₂ ⊢      refine ⟨mp, ⟨h₂, ?_, h₁⟩, ⟨h₁, rfl⟩⟩      rw [mem_toFinset, Set.mem_sdiff] at mp; obtain ⟨mp₁, mp₂⟩ := mp; contrapose! mp₂      exact overlap_implies_distance hu₁ hu₂ hu h2u (.inr mp₁) (h₃.symm ▸ mp₂)    _ = ∑ k ∈ Finset.Icc ⌊C7_6_3 a n⌋ (2 * S),        (∑ J ∈ (𝓙₆ t u₁).toFinset, (volume (J : Set X))⁻¹ *        (∑ I with s I = s J - k ∧ Disjoint (I : Set X) (𝓘 u₁) ∧          ¬Disjoint ↑J (ball (c I) (8 * D ^ s I)),        ∫⁻ y in J, ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with          ¬Disjoint ↑J (ball (𝔠 p) (8 * D ^ 𝔰 p)) ∧ 𝓘 p = I,        ‖adjointCarleson p f y‖ₑ) ^ 2) ^ (2 : ℝ)⁻¹ := by      congr! with k mk J mJ      exact lintegral_finsetSum' _ fun k mk ↦ Finset.aemeasurable_fun_sum _ fun p mp ↦        hf.aestronglyMeasurable.adjointCarleson.aemeasurable.enorm.restrict    _ ≤ ∑ k ∈ Finset.Icc ⌊C7_6_3 a n⌋ (2 * S),        (∑ J ∈ (𝓙₆ t u₁).toFinset, (volume (J : Set X))⁻¹ *        (∑ I with s I = s J - k ∧ Disjoint (I : Set X) (𝓘 u₁) ∧          ¬Disjoint ↑J (ball (c I) (8 * D ^ s I)),        C2_1_3 a * 2 ^ (4 * a) * ∫⁻ y in J, (ball (c I) (8 * D ^ s I)).indicator 1 y *          maximalFunction volume 𝓑 c𝓑 r𝓑 1 f y) ^ 2) ^ (2 : ℝ)⁻¹ := by      gcongr with k mk J mJ; exact btp_integral_bound    _ = _ := by      nth_rw 2 [← ENNReal.rpow_one (C2_1_3 a * 2 ^ (4 * a))]      rw [show (1 : ℝ) = (2 : ℕ) * 2⁻¹ by norm_num, ENNReal.rpow_mul, Finset.mul_sum]      congr! with k mk      rw [← ENNReal.mul_rpow_of_nonneg _ _ (by positivity), Finset.mul_sum]      congr! 2 with J mJ      rw [← mul_assoc, mul_comm _ (volume (J : Set X))⁻¹, ENNReal.rpow_natCast, mul_assoc,        ← mul_pow, Finset.mul_sum]