TileStructure.Forest.local_tree_control

lemma local_tree_control (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) (hf : BoundedCompactSupport f) :    ⨆ x ∈ ball (c J) (8⁻¹ * D ^ s J), ‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f x‖ₑ ≤    C7_5_7 a * ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x := by  classical  calc    _ ≤ ∑ k ∈ Finset.Icc (s J) (s J + 3),        ∑ p with 𝔰 p = k ∧ ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8⁻¹ * D ^ s J)),          ⨆ x ∈ ball (c J) (8⁻¹ * D ^ s J), ‖adjointCarleson p f x‖ₑ :=      local_tree_control_sumsumsup hu₁ hu₂ hu h2u hJ    _ ≤ ∑ k ∈ Finset.Icc (s J) (s J + 3),        ∑ p ∈ {p | 𝔰 p = k ∧ ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8⁻¹ * D ^ s J))},          2 ^ ((𝕔 + 3) * a ^ 3) * (volume (ball (c J) (16 * D ^ k)))⁻¹ * ∫⁻ x in E p, ‖f x‖ₑ := by      gcongr with k mk p mp      simp_rw [Finset.mem_filter, Finset.mem_univ, true_and] at mp      exact local_tree_control_sup_bound mk mp hf.aestronglyMeasurable.enorm    _ = 2 ^ ((𝕔 + 3) * a ^ 3) * ∑ k ∈ Finset.Icc (s J) (s J + 3),        (volume (ball (c J) (16 * D ^ k)))⁻¹ *          ∑ p with 𝔰 p = k ∧ ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8⁻¹ * D ^ s J)),            ∫⁻ x in E p, ‖f x‖ₑ := by      simp_rw [Finset.mul_sum, mul_assoc]    _ = 2 ^ ((𝕔 + 3) * a ^ 3) * ∑ k ∈ Finset.Icc (s J) (s J + 3),        (volume (ball (c J) (16 * D ^ k)))⁻¹ * ∫⁻ x in ⋃ p ∈ Finset.univ.filter (fun p ↦ 𝔰 p = k ∧          ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8⁻¹ * D ^ s J))), E p, ‖f x‖ₑ := by      congr! with k mk      refine (lintegral_biUnion_finset ?_ (fun _ _ ↦ measurableSet_E) _).symm      intro p mp q mq hn      by_cases hi : 𝓘 p = 𝓘 q      · by_contra h; rw [not_disjoint_iff] at h; obtain ⟨x, mx₁ : x ∈ E p, mx₂ : x ∈ E q⟩ := h        apply absurd (disjoint_Ω hn hi); rw [not_disjoint_iff]; use Q x, mx₁.2.1, mx₂.2.1      · apply disjoint_of_subset E_subset_𝓘 E_subset_𝓘        simp_rw [Finset.coe_filter, Finset.mem_univ, true_and, mem_setOf_eq] at mp mq        have := eq_or_disjoint (mq.1 ▸ mp.1)        exact this.resolve_left hi    _ ≤ 2 ^ ((𝕔 + 3) * a ^ 3) * ∑ k ∈ Finset.Icc (s J) (s J + 3),        (volume (ball (c J) (16 * D ^ k)))⁻¹ * ∫⁻ x in ball (c J) (16 * D ^ k), ‖f x‖ₑ := by      gcongr with k mk; refine iUnion₂_subset fun p mp ↦ ?_      rw [Finset.mem_filter_univ] at mp      refine (E_subset_𝓘.trans Grid_subset_ball).trans (ball_subset_ball' ?_)      obtain ⟨y, my₁, my₂⟩ := not_disjoint_iff.mp mp.2      rw [mem_ball] at my₁ my₂; change 4 * D ^ 𝔰 p + dist (𝔠 p) (c J) ≤ _      calc        _ ≤ 4 * D ^ 𝔰 p + (dist y (𝔠 p) + dist y (c J)) := by gcongr; exact dist_triangle_left ..        _ ≤ 4 * D ^ 𝔰 p + 8 * D ^ 𝔰 p + 8⁻¹ * D ^ s J := by rw [add_assoc]; gcongr        _ ≤ (4 + 8 + 8⁻¹) * D ^ k := by          rw [Finset.mem_Icc] at mk; simp_rw [add_mul, mp.1]; gcongr; exacts [one_le_realD a, mk.1]        _ ≤ _ := by gcongr; norm_num    _ = 2 ^ ((𝕔 + 3) * a ^ 3) *        ∑ k ∈ Finset.Icc (s J) (s J + 3), ⨍⁻ x in ball (c J) (16 * D ^ k), ‖f x‖ₑ ∂volume := by      simp_rw [setLAverage_eq, ENNReal.div_eq_inv_mul]    _ ≤ 2 ^ ((𝕔 + 3) * a ^ 3) *        ∑ k ∈ Finset.Icc (s J) (s J + 3), ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x := by      gcongr with k mk; rw [Finset.mem_Icc] at mk      apply laverage_le_biInf_MB      · gcongr; exacts [by norm_num, one_le_realD a, mk.1]      · use ⟨4, (k - s J).toNat, J⟩        simp only [𝓑, c𝓑, r𝓑, mem_prod, mem_Iic, mem_univ, le_add_iff_nonneg_left, zero_le,          and_true, true_and]        rw [show s J + (k - s J).toNat = k by omega, Int.toNat_le, Nat.cast_add, Nat.cast_mul,          Nat.cast_ofNat]        refine ⟨by omega, by norm_num⟩    _ = 2 ^ ((𝕔 + 3) * a ^ 3) * 2 ^ 2 * ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x := by      rw [Finset.sum_const, Int.card_Icc, show s J + 3 + 1 - s J = 4 by lia, nsmul_eq_mul,        show (Int.toNat 4 : ℝ≥0∞) = 2 ^ 2 by simp; norm_num, mul_assoc]    _ ≤ _ := by      gcongr; rw [C7_5_7, ← pow_add]; norm_cast      refine pow_le_pow_right' one_le_two ?_      rw [show (𝕔 + 4) * a ^ 3 = (𝕔 + 3) * a ^ 3 + a * a * a by ring]      gcongr      nlinarith [four_le_a X]