TileStructure.Forest.volume_cpDsp_bound

lemma volume_cpDsp_bound {J : Grid X}    (hd : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J))) (hs : s J ≤ 𝔰 p) :    volume (ball (c J) (32 * D ^ 𝔰 p)) / 2 ^ (4 * a) ≤ volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) := by  apply ENNReal.div_le_of_le_mul'  have h : dist (𝔠 p) (c J) + 32 * D ^ 𝔰 p ≤ 16 * (4 * D ^ 𝔰 p) := by    calc      _ ≤ 8 * (D : ℝ) ^ 𝔰 p + 16 * D ^ s J + 32 * D ^ 𝔰 p := by        gcongr; exact (dist_lt_of_not_disjoint_ball hd).le      _ ≤ 8 * (D : ℝ) ^ 𝔰 p + 16 * D ^ 𝔰 p + 32 * D ^ 𝔰 p := by        gcongr; exact one_le_realD a      _ ≤ _ := by rw [← add_mul, ← add_mul, ← mul_assoc]; 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 _ _ one_lt_two]