volume_xDsp_bound_4

lemma volume_xDsp_bound_4 {x : X} (hx : x ∈ 𝓘 p) :    volume (ball (𝔠 p) (8 * D ^ 𝔰 p)) / 2 ^ (4 * a) ≤ volume (ball x (D ^ 𝔰 p)) := by  apply ENNReal.div_le_of_le_mul'  have h : dist x (𝔠 p) + 8 * D ^ 𝔰 p ≤ 16 * D ^ 𝔰 p := by    calc      _ ≤ 4 * (D : ℝ) ^ 𝔰 p + 8 * ↑D ^ 𝔰 p := by        gcongr; exact (mem_ball.mp (Grid_subset_ball hx)).le      _ ≤ _ := by rw [← add_mul]; gcongr; norm_num  convert measure_ball_le_of_dist_le' (μ := volume) (by norm_num) h  unfold As defaultA; norm_cast  rw [← pow_mul', show (16 : ℕ) = 2 ^ 4 by norm_num, Nat.clog_pow]; norm_num