TileStructure.Forest.global_tree_control1_edist_part1

lemma global_tree_control1_edist_part1    (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_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 := by  classical calc    _ ≤ ∑ p ∈ ℭ, edist (exp (.I * 𝒬 u x) * adjointCarleson p f x)        (exp (.I * 𝒬 u x') * adjointCarleson p f x') := by      simp_rw [adjointCarlesonSum, Finset.mul_sum]      have heq : Finset.univ.filter (· ∈ ℭ) = ℭ.toFinset := by        ext x        simp only [Finset.mem_filter, Finset.mem_univ, true_and, Set.mem_toFinset]      rw [heq]      exact ENNReal.edist_sum_le_sum_edist    _ = ∑ p ∈ ℭ with ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)),        edist (exp (.I * 𝒬 u x) * adjointCarleson p f x)          (exp (.I * 𝒬 u x') * adjointCarleson p f x') := by      refine (Finset.sum_filter_of_ne fun p mp hp ↦ ?_).symm; contrapose! hp      replace hp : Disjoint (ball (𝔠 p) (5 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)) :=        hp.mono_left (ball_subset_ball (by gcongr; norm_num))      rw [adjoint_tile_support1, indicator_of_notMem (disjoint_right.mp hp hx), mul_zero,        indicator_of_notMem (disjoint_right.mp hp hx'), mul_zero, edist_self]    _ ≤ ∑ p ∈ ℭ with ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)),        C7_5_5 a / volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) *          (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹ * ∫⁻ x in E p, ‖f x‖ₑ := by      gcongr with p mp; rw [Finset.mem_filter, mem_toFinset] at mp      exact holder_correlation_tile hu (hℭ mp.1) hf    _ = C7_5_5 a * edist x x' ^ (a : ℝ)⁻¹ *        ∑ p ∈ ℭ with ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)),          D ^ (-𝔰 p / (a : ℝ)) / volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) * ∫⁻ x in E p, ‖f x‖ₑ := by      rw [Finset.mul_sum]; congr! 1 with p mp      rw [← mul_assoc, ← mul_div_assoc, mul_assoc _ _ ((D : ℝ≥0∞) ^ _), mul_comm _ (_ * _),        mul_div_assoc, mul_comm (_ ^ _ * _)]; congr      rw [div_eq_mul_inv, ENNReal.mul_rpow_of_nonneg _ _ (by positivity),        ← ENNReal.zpow_neg, ← ENNReal.rpow_intCast, ← ENNReal.rpow_mul,        ← div_eq_mul_inv, Int.cast_neg]    _ = C7_5_5 a * edist x x' ^ (a : ℝ)⁻¹ * ∑ k ∈ Finset.Icc (s J) S,        ∑ p ∈ ℭ with ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)) ∧ 𝔰 p = k,          D ^ (-𝔰 p / (a : ℝ)) / volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) * ∫⁻ x in E p, ‖f x‖ₑ := by      congr 1; simp_rw [← Finset.filter_filter]      refine (Finset.sum_fiberwise_of_maps_to (fun p mp ↦ ?_) _).symm      rw [Finset.mem_Icc]; rw [Finset.mem_filter, mem_toFinset] at mp      exact ⟨hs p mp.1 mp.2, scale_mem_Icc.2⟩    _ = C7_5_5 a * edist x x' ^ (a : ℝ)⁻¹ * ∑ k ∈ Finset.Icc (s J) S, D ^ (-k / (a : ℝ)) *        ∑ p ∈ ℭ with ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)) ∧ 𝔰 p = k,          (∫⁻ x in E p, ‖f x‖ₑ) / volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) := by      congr! 2 with k mk; rw [Finset.mul_sum]; congr! 1 with p mp      rw [mul_comm, ← mul_div_assoc, ← mul_div_assoc, mul_comm]; congr      rw [Finset.mem_filter] at mp; exact mp.2.2    _ ≤ C7_5_5 a * edist x x' ^ (a : ℝ)⁻¹ * ∑ k ∈ Finset.Icc (s J) S, D ^ (-k / (a : ℝ)) *        ∑ p ∈ ℭ with ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)) ∧ 𝔰 p = k,          (∫⁻ x in E p, ‖f x‖ₑ) / (volume (ball (c J) (32 * D ^ k)) / 2 ^ (4 * a)) := by      gcongr with k mk p mp; rw [Finset.mem_filter, mem_toFinset] at mp      rw [← mp.2.2]; exact volume_cpDsp_bound mp.2.1 (hs p mp.1 mp.2.1)    _ = C7_5_5 a * 2 ^ (4 * a) * edist x x' ^ (a : ℝ)⁻¹ * ∑ k ∈ Finset.Icc (s J) S,        D ^ (-k / (a : ℝ)) * (volume (ball (c J) (32 * D ^ k)))⁻¹ *        ∑ p ∈ ℭ with ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)) ∧ 𝔰 p = k,          ∫⁻ x in E p, ‖f x‖ₑ := by      rw [← mul_rotate _ _ (2 ^ (4 * a)), mul_comm (_ ^ _), mul_assoc (_ * _),        Finset.mul_sum (a := 2 ^ (4 * a))]; congr! 2 with k mk      rw [← mul_assoc _ (_ * _), mul_rotate', ← ENNReal.div_eq_inv_mul, mul_assoc,        Finset.mul_sum (a := _ / _)]; congr! 2 with p mp      rw [← ENNReal.inv_div (b := 2 ^ (4 * a)) (by left; simp) (by left; simp),        ENNReal.div_eq_inv_mul]    _ ≤ C7_5_5 a * 2 ^ (4 * a) * edist x x' ^ (a : ℝ)⁻¹ * ∑ k ∈ Finset.Icc (s J) S,        D ^ (-k / (a : ℝ)) * (volume (ball (c J) (32 * D ^ k)))⁻¹ *        ∫⁻ x in ball (c J) (32 * D ^ k), ‖f x‖ₑ := by      gcongr with k mk; exact gtc_integral_bound hs    _ = _ := by congr! 2 with k mk; rw [mul_assoc, setLAverage_eq, ENNReal.div_eq_inv_mul]