TileStructure.Forest.e763

lemma e763 (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 ≤    ∑ k ∈ Finset.Icc ⌊C7_6_3 a n⌋ (2 * S),    (∑ J ∈ (𝓙₆ t u₁).toFinset, (volume (J : Set X))⁻¹ *    (∫⁻ y in J, ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with      ¬Disjoint ↑J (ball (𝔠 p) (8 * D ^ 𝔰 p)) ∧ 𝔰 p = s J - k,    ‖adjointCarleson p f y‖ₑ) ^ 2) ^ (2 : ℝ)⁻¹ := by  calc    _ = _ := btp_expansion hf    _ = (∑ J ∈ (𝓙₆ t u₁).toFinset, (volume (J : Set X))⁻¹ * (∫⁻ y in J,        ‖∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with ¬Disjoint ↑J (ball (𝔠 p) (8 * D ^ 𝔰 p)),          adjointCarleson p f y‖ₑ) ^ 2) ^ (2 : ℝ)⁻¹ := by      congr! 4 with J mJ      refine setLIntegral_congr_fun coeGrid_measurable fun y my ↦ ?_      unfold adjointCarlesonSum; congr 1      rw [filter_mem_univ_eq_toFinset]; refine (Finset.sum_filter_of_ne fun p mp hd ↦ ?_).symm      rw [adjoint_tile_support1] at hd      exact not_disjoint_iff.mpr ⟨_, my,        ball_subset_ball (by gcongr; norm_num) (mem_of_indicator_ne_zero hd)⟩    _ = (∑ J ∈ (𝓙₆ t u₁).toFinset, (volume (J : Set X))⁻¹ * (∫⁻ y in J,        ‖∑ k ∈ Finset.Icc ⌊C7_6_3 a n⌋ (2 * S),        ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with          ¬Disjoint ↑J (ball (𝔠 p) (8 * D ^ 𝔰 p)) ∧ s J - 𝔰 p = k,        adjointCarleson p f y‖ₑ) ^ 2) ^ (2 : ℝ)⁻¹ := by      congr! with J mJ y; simp_rw [← Finset.filter_filter]      refine (Finset.sum_fiberwise_of_maps_to (fun p mp ↦ ?_) _).symm      rw [Finset.mem_filter] at mp; rw [mem_toFinset] at mp mJ; obtain ⟨mp, dp⟩ := mp      have dpJ : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8 * D ^ s J)) := by        contrapose! dp; refine dp.symm.mono_left (Grid_subset_ball.trans (ball_subset_ball ?_))        change (4 : ℝ) * D ^ s J ≤ _; gcongr; norm_num      rw [Finset.mem_Icc]      constructor      · have := thin_scale_impact' hu₁ hu₂ hu h2u mp mJ dpJ        lia      · have : s J ≤ S := scale_mem_Icc.2        have : -S ≤ 𝔰 p := scale_mem_Icc.1        lia    _ ≤ (∑ J ∈ (𝓙₆ t u₁).toFinset, (volume (J : Set X))⁻¹ *        (∫⁻ y in J, ∑ k ∈ Finset.Icc ⌊C7_6_3 a n⌋ (2 * S),        ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with          ¬Disjoint ↑J (ball (𝔠 p) (8 * D ^ 𝔰 p)) ∧ s J - 𝔰 p = k,        ‖adjointCarleson p f y‖ₑ) ^ 2) ^ (2 : ℝ)⁻¹ := by -- Triangle inequality      gcongr with J mJ y      exact (enorm_sum_le _ _).trans (Finset.sum_le_sum fun k mk ↦ enorm_sum_le _ _)    _ = (∑ J ∈ (𝓙₆ t u₁).toFinset, (volume (J : Set X))⁻¹ *        (∑ k ∈ Finset.Icc ⌊C7_6_3 a n⌋ (2 * S), ∫⁻ y in J,        ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with          ¬Disjoint ↑J (ball (𝔠 p) (8 * D ^ 𝔰 p)) ∧ s J - 𝔰 p = k,        ‖adjointCarleson p f y‖ₑ) ^ 2) ^ (2 : ℝ)⁻¹ := by      congr! with J mJ      exact lintegral_finsetSum' _ fun k mk ↦ Finset.aemeasurable_fun_sum _ fun p mp ↦        hf.aestronglyMeasurable.adjointCarleson.aemeasurable.enorm.restrict    _ = (∑ J ∈ (𝓙₆ t u₁).toFinset, (∑ k ∈ Finset.Icc ⌊C7_6_3 a n⌋ (2 * S),        volume (J : Set X) ^ (-2 : ℝ)⁻¹ * ∫⁻ y in J, ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with          ¬Disjoint ↑J (ball (𝔠 p) (8 * D ^ 𝔰 p)) ∧ 𝔰 p = s J - k,        ‖adjointCarleson p f y‖ₑ) ^ (2 : ℝ)) ^ (1 / 2 : ℝ) := by      rw [one_div]; congr! with J mJ      rw [← ENNReal.rpow_neg_one, show (-1 : ℝ) = (-2)⁻¹ * (2 : ℕ) by norm_num, ENNReal.rpow_mul,        ENNReal.rpow_natCast, ← mul_pow, show (2 : ℝ) = (2 : ℕ) by rfl, ENNReal.rpow_natCast,        Finset.mul_sum]      congr! 8 with k mk y p; lia    _ ≤ ∑ k ∈ Finset.Icc ⌊C7_6_3 a n⌋ (2 * S),        (∑ J ∈ (𝓙₆ t u₁).toFinset, (volume (J : Set X) ^ (-2 : ℝ)⁻¹ *        ∫⁻ y in J, ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with          ¬Disjoint ↑J (ball (𝔠 p) (8 * D ^ 𝔰 p)) ∧ 𝔰 p = s J - k,        ‖adjointCarleson p f y‖ₑ) ^ (2 : ℝ)) ^ (1 / 2 : ℝ) := -- Minkowski inequality      ENNReal.Lp_add_le_sum one_le_two    _ = _ := by      rw [one_div]; congr! with k mk J mJ      nth_rw 2 [show (2 : ℝ) = (2 : ℕ) by rfl]      rw [ENNReal.rpow_natCast, mul_pow, ← ENNReal.rpow_natCast, ← ENNReal.rpow_mul,        show (-2)⁻¹ * (2 : ℕ) = (-1 : ℝ) by norm_num, ENNReal.rpow_neg_one]