TileStructure.Forest.enorm_ψ_le_edist

lemma enorm_ψ_le_edist {y : X} (my : y ∈ E p) (hx' : x' ∉ ball (𝔠 p) (5 * D ^ 𝔰 p)) :    ‖ψ (D ^ (-𝔰 p) * dist y x)‖ₑ ≤ 4 * (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹ := by  by_cases h : 1 / 2 ≤ D ^ (-𝔰 p) * dist y x  · rw [ψ_formula₄ h, enorm_zero]; exact zero_le  replace h : 0 ≤ 2 - 4 * (D ^ (-𝔰 p) * dist y x) := by linarith  calc    _ ≤ ‖max 0 ((2 - 4 * (D ^ (-𝔰 p) * dist y x)) ^ (a : ℝ)⁻¹)‖ₑ :=      Real.enorm_le_enorm (zero_le_ψ ..) (ψ_le_max (X := X))    _ = ‖2 - 4 * (D ^ (-𝔰 p) * dist y x)‖ₑ ^ (a : ℝ)⁻¹ := by      rw [max_eq_right (Real.rpow_nonneg h _), Real.enorm_rpow_of_nonneg h (by positivity)]    _ ≤ ‖dist x x' / D ^ (𝔰 p) * 4‖ₑ ^ (a : ℝ)⁻¹ := by      gcongr; exact Real.enorm_le_enorm h (le_of_mem_E my hx')    _ = (edist x x' / D ^ (𝔰 p) * 4) ^ (a : ℝ)⁻¹ := by      rw [enorm_mul]; nth_rw 2 [enorm_eq_nnnorm]; rw [Real.nnnorm_ofNat, ENNReal.coe_ofNat]; congr      rw [enorm_eq_nnnorm, nnnorm_div, nnnorm_zpow]; norm_cast      rw [ENNReal.coe_div (by simp only [defaultD, Nat.cast_pow, Nat.cast_ofNat, defaultA, ne_eq]; positivity),        ENNReal.coe_zpow (by simp)]; norm_cast; congr      rw [edist_dist, ← Real.enorm_of_nonneg dist_nonneg, enorm_eq_nnnorm]    _ ≤ _ := by      rw [ENNReal.mul_rpow_of_nonneg _ _ (by positivity), mul_comm]; gcongr      nth_rw 2 [← ENNReal.rpow_one 4]      exact ENNReal.rpow_le_rpow_of_exponent_le (by norm_num) (Nat.cast_inv_le_one a)