TileStructure.Forest.global_tree_control1_edist_part2

lemma global_tree_control1_edist_part2    (hu : u ∈ t) {ℭ : Set (𝔓 X)} (hℭ : ℭ ⊆ t u) (hf : BoundedCompactSupport f)    (hs : ∀ p ∈ ℭ, ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)) → s J ≤ 𝔰 p)    (hx : x ∈ ball (c J) (16 * D ^ s J)) (hx' : x' ∈ ball (c J) (16 * D ^ s J)) :    edist (exp (.I * 𝒬 u x) * adjointCarlesonSum ℭ f x)      (exp (.I * 𝒬 u x') * adjointCarlesonSum ℭ f x') ≤    C7_5_9d a * (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ * ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x := by  calc    _ ≤ C7_5_5 a * 2 ^ (4 * a) * edist x x' ^ (a : ℝ)⁻¹ * ∑ k ∈ Finset.Icc (s J) S,        D ^ (-k / (a : ℝ)) * ⨍⁻ x in ball (c J) (32 * D ^ k), ‖f x‖ₑ ∂volume :=      global_tree_control1_edist_part1 hu hℭ hf hs hx hx'    _ ≤ C7_5_5 a * 2 ^ (4 * a) * edist x x' ^ (a : ℝ)⁻¹ * ∑ k ∈ Finset.Icc (s J) S,        D ^ (-k / (a : ℝ)) * ⨅ 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 ⟨5, (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]        have : -S ≤ s J := scale_mem_Icc.1        exact ⟨by omega, by norm_num⟩    _ = C7_5_5 a * 2 ^ (4 * a) * (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ *        (∑ k ∈ Finset.Icc (s J) S, (D : ℝ≥0∞) ^ ((s J - k) / (a : ℝ))) *        ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x := by      have fla := four_le_a X      have dpos : 0 < (D : ℝ≥0∞) ^ s J := ENNReal.zpow_pos (by simp) (by simp) _      have dlt : (D : ℝ≥0∞) ^ s J < ⊤ := ENNReal.zpow_lt_top (by simp) (by simp) _      have bpos : ((D : ℝ≥0∞) ^ s J) ^ (a : ℝ)⁻¹ ≠ 0 := (ENNReal.rpow_pos dpos dlt.ne).ne'      have bnt : ((D : ℝ≥0∞) ^ s J) ^ (a : ℝ)⁻¹ ≠ ⊤ :=        ENNReal.rpow_ne_top_of_nonneg (by positivity) dlt.ne      rw [← ENNReal.inv_mul_cancel_right (a := (_ ^ (a : ℝ)⁻¹)) bpos bnt, mul_comm _ _⁻¹,        ← ENNReal.div_eq_inv_mul, ← ENNReal.div_rpow_of_nonneg _ _ (by positivity), ← mul_assoc,        mul_assoc _ _ (∑ k ∈ _, _), Finset.mul_sum]      conv_lhs => enter [2, 2, k]; rw [← mul_assoc]      rw [← Finset.sum_mul, ← mul_assoc]; congr! with k mk      rw [← ENNReal.rpow_intCast, ← ENNReal.rpow_mul, ← div_eq_mul_inv,        ← ENNReal.rpow_add _ _ (by simp) (by simp), neg_div, ← sub_eq_add_neg, sub_div]    _ ≤ C7_5_5 a * 2 ^ (4 * a + 1) * (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ *        ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x := by      rw [pow_succ, ← mul_assoc, mul_assoc _ 2, mul_comm 2, ← mul_assoc]; gcongr      exact gtc_sum_Icc_le_two    _ = _ := by congr; rw [C7_5_9d, C7_5_5]; norm_cast