TileStructure.Forest.boundary_overlap

lemma boundary_overlap (I : Grid X) : (kissing I).card ≤ 2 ^ (9 * a) := by  have key : (kissing I).card * volume (ball (c I) (33 * D ^ s I)) ≤      2 ^ (9 * a) * volume (ball (c I) (33 * D ^ s I)) := by    calc      _ = ∑ _ ∈ kissing I, volume (ball (c I) (33 * D ^ s I)) := by        rw [Finset.sum_const, nsmul_eq_mul]      _ ≤ ∑ J ∈ kissing I, 2 ^ (9 * a) * volume (ball (c J) (D ^ s J / 4)) :=        Finset.sum_le_sum fun _ ↦ volume_le_of_kissing      _ = 2 ^ (9 * a) * volume (⋃ J ∈ kissing I, ball (c J) (D ^ s J / 4)) := by        rw [← Finset.mul_sum]; congr        exact (measure_biUnion_finset pairwiseDisjoint_of_kissing fun _ _ ↦ measurableSet_ball).symm      _ ≤ _ := by gcongr; exact iUnion₂_subset fun _ ↦ subset_of_kissing  have vn0 : volume (ball (c I) (33 * D ^ s I)) ≠ 0 := by    refine (measure_ball_pos volume _ ?_).ne'; simp only [defaultD]; positivity  rw [ENNReal.mul_le_mul_iff_left vn0 measure_ball_ne_top] at key; norm_cast at key