TileStructure.Forest.btp_integral_bound

lemma btp_integral_bound :    ∫⁻ y in J, ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with      ¬Disjoint ↑J (ball (𝔠 p) (8 * D ^ 𝔰 p)) ∧ 𝓘 p = I, ‖adjointCarleson p f y‖ₑ ≤    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 := by  calc    _ ≤ ∫⁻ y in J, ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with        ¬Disjoint ↑J (ball (𝔠 p) (8 * D ^ 𝔰 p)) ∧ 𝓘 p = I,          C2_1_3 a * 2 ^ (4 * a) * (volume (ball (𝔠 p) (8 * D ^ 𝔰 p)))⁻¹ * (∫⁻ y in E p, ‖f y‖ₑ) *          (ball (𝔠 p) (8 * D ^ 𝔰 p)).indicator 1 y := by      gcongr with y p mp; exact enorm_adjointCarleson_le_mul_indicator    _ = ∫⁻ y in J, ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with        ¬Disjoint ↑J (ball (c I) (8 * D ^ s I)) ∧ 𝓘 p = I,          C2_1_3 a * 2 ^ (4 * a) * (volume (ball (c I) (8 * D ^ s I)))⁻¹ * (∫⁻ y in E p, ‖f y‖ₑ) *          (ball (c I) (8 * D ^ s I)).indicator 1 y := by      congr! 3 with y p mp      · ext p; simp_rw [Finset.mem_filter, and_congr_right_iff, and_congr_left_iff]        intro _ he; rw [← he]; rfl      · simp_rw [Finset.mem_filter] at mp        simp_rw [← mp.2.2]; rfl    _ = C2_1_3 a * 2 ^ (4 * a) * ∫⁻ y in J,        (ball (c I) (8 * D ^ s I)).indicator 1 y * ((volume (ball (c I) (8 * D ^ s I)))⁻¹ *        ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with ¬Disjoint ↑J (ball (c I) (8 * D ^ s I)) ∧ 𝓘 p = I,          ∫⁻ y in E p, ‖f y‖ₑ) := by      rw [← lintegral_const_mul' _ _ (by finiteness)]; congr! with y      simp_rw [Finset.mul_sum]; congr! 1 with p mp; ring    _ = C2_1_3 a * 2 ^ (4 * a) * ∫⁻ y in J,        (ball (c I) (8 * D ^ s I)).indicator 1 y * ((volume (ball (c I) (8 * D ^ s I)))⁻¹ *        ∫⁻ y in ⋃ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset.filter          (¬Disjoint ↑J (ball (c I) (8 * D ^ s I)) ∧ 𝓘 · = I), E p, ‖f y‖ₑ) := by      congr! with y      refine (lintegral_biUnion_finset (fun p₁ mp₁ p₂ mp₂ hn ↦ ?_)        (fun p mp ↦ measurableSet_E) _).symm      rw [Finset.coe_filter, mem_setOf_eq] at mp₁ mp₂      exact disjoint_E hn (mp₂.2.2.symm ▸ mp₁.2.2)    _ ≤ C2_1_3 a * 2 ^ (4 * a) * ∫⁻ y in J, (ball (c I) (8 * D ^ s I)).indicator 1 y *        ⨍⁻ y in ball (c I) (8 * D ^ s I), ‖f y‖ₑ ∂volume := by      gcongr with y; rw [setLAverage_eq, ENNReal.div_eq_inv_mul]      refine mul_le_mul_right (lintegral_mono_set (iUnion₂_subset fun p mp ↦ ?_)) _      rw [Finset.mem_filter] at mp      convert! (E_subset_𝓘.trans Grid_subset_ball).trans (ball_subset_ball _)      · exact mp.2.2.symm      · change (4 : ℝ) * D ^ s (𝓘 p) ≤ _        rw [mp.2.2]; gcongr; norm_num    _ ≤ _ := by      refine mul_le_mul_right (lintegral_mono fun y ↦ ?_) _      by_cases my : y ∈ ball (c I) (8 * D ^ s I)      · refine mul_le_mul_right ?_ _; simp only [maximalFunction, ENNReal.rpow_one, inv_one]        have : (3, 0, I) ∈ 𝓑 := by          simp only [𝓑, Set.mem_prod, mem_Iic, Set.mem_univ, and_true]          omega        refine le_of_eq_of_le ?_ (le_biSup _ this)        have : y ∈ ball (c I) (2 ^ 3 * (D : ℝ) ^ s I) := by rwa [show (2 : ℝ) ^ 3 = 8 by norm_num]        simp_rw [c𝓑, r𝓑, Nat.cast_zero, add_zero, indicator_of_mem this, enorm_eq_nnnorm]        norm_num      · rw [indicator_of_notMem my, zero_mul]; exact zero_le