TileStructure.Forest.volume_le_of_kissing

lemma volume_le_of_kissing (h : J ∈ kissing I) :    volume (ball (c I) (33 * D ^ s I)) ≤ 2 ^ (9 * a) * volume (ball (c J) (D ^ s J / 4)) := by  simp_rw [kissing, Finset.mem_filter_univ] at h  obtain ⟨x, xI, xJ⟩ := not_disjoint_iff.mp h.2  have : ball (c I) (33 * D ^ s I) ⊆ ball (c J) (128 * D ^ s J) := by    apply ball_subset_ball'    calc      _ ≤ 33 * D ^ s I + dist (c I) x + dist x (c J) := by        rw [add_assoc]; exact add_le_add_right (dist_triangle ..) _      _ ≤ 33 * D ^ s I + 16 * D ^ s I + 16 * D ^ s J := by        gcongr        · exact (mem_ball'.mp xI).le        · exact (mem_ball.mp xJ).le      _ ≤ _ := by        rw [h.1, ← distrib_three_right]        gcongr; norm_num  have double := @measure_ball_two_le_same_iterate X _ _ _ volume _ (c J) (D ^ s J / 4) 9  have A9 : (defaultA a : ℝ≥0) ^ 9 = (2 : ℝ≥0∞) ^ (9 * a) := by    simp only [defaultA]; norm_cast; ring  rw [show (2 : ℝ) ^ 9 * (D ^ s J / 4) = 128 * D ^ s J by ring, A9] at double  exact (measure_mono this).trans double