TileStructure.Forest.QQQQ_bound

lemma QQQQ_bound {y : X} (my : y ∈ E p) (hu : u ∈ t) (hp : p ∈ t u)    (hx : x ∈ ball (𝔠 p) (5 * D ^ 𝔰 p)) (hx' : x' ∈ ball (𝔠 p) (5 * D ^ 𝔰 p)) :    ‖-Q y x + Q y x' + 𝒬 u x - 𝒬 u x'‖ₑ ≤ Q7_5_5 a * (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹ := by  calc    _ ≤ ‖Q7_5_5 a * (dist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹‖ₑ := by      rw [← enorm_norm]      exact Real.enorm_le_enorm (norm_nonneg _) (QQQQ_bound_real my hu hp hx hx')    _ = _ := by      rw [enorm_mul, Real.enorm_rpow_of_nonneg (by positivity) (by norm_cast; positivity),        NNReal.enorm_eq, div_eq_mul_inv, enorm_mul, enorm_inv (by unfold defaultD; positivity),        ← div_eq_mul_inv]; congr      · rw [Real.enorm_eq_ofReal dist_nonneg, dist_edist, ENNReal.ofReal_toReal]        exact edist_ne_top x x'      · rw [Real.enorm_eq_ofReal (by positivity), ← Real.rpow_intCast,          ← ENNReal.ofReal_rpow_of_pos (by simp), ENNReal.rpow_intCast]; norm_cast