counting_balls

lemma counting_balls {k : ℤ} (hk_lower : -S ≤ k) {Y : Set X}    (hY : Y ⊆ ball o (4 * D ^ S - D ^ k))    (hYdisjoint : Y.PairwiseDisjoint (ball · (D ^ k))) :    (Set.encard Y).toENNReal ≤ C4_1_1 X := by  suffices (Set.encard Y).toENNReal * volume (ball o (4 * D ^ S)) ≤      (As (2 ^ a) (2 ^ J' X)) * volume (ball o (4 * D ^ S)) by    have volume_pos : 0 < volume (ball o (4 * D ^ S)) := by      apply measure_ball_pos volume o      simp only [defaultD, Nat.ofNat_pos, mul_pos_iff_of_pos_left]      positivity    rw [← ENNReal.mul_le_mul_iff_right volume_pos.ne.symm (by finiteness), mul_comm,      mul_comm (volume _)]    exact this  have val_ne_zero : (As (2 ^ a) (2 ^ J' X) : ℝ≥0∞) ≠ 0 := by    exact_mod_cast (As_pos' (volume : Measure X) (2 ^ J' X)).ne.symm  calc    (Y.encard).toENNReal * volume (ball o (4 * D ^ S))      = ∑' (y : Y), volume (ball o (4 * D ^ S)) := by rw [ENNReal.tsum_const_eq']    _ ≤ ∑' (y : Y), volume (ball (y : X) (8 * D ^ (2 * S) * D ^ k)) :=      ENNReal.summable.tsum_le_tsum (fun ⟨y, hy⟩ ↦ volume.mono (ball_bound k hk_lower hY y hy))        ENNReal.summable    _ ≤ ∑' (y : Y), (As (2 ^ a) (2 ^ J' X)) * volume (ball (y : X) (D ^ k)) := by      apply ENNReal.summable.tsum_le_tsum _ ENNReal.summable      intro y      rw_mod_cast [← twopow_J]      apply measure_ball_le_same _ (by positivity) (le_refl _)    _ ≤ (As (2 ^ a) (2 ^ J' X)) * ∑' (y : Y), volume (ball (y : X) (D ^ k)):= by      rw [ENNReal.tsum_mul_left]    _ = (As (2 ^ a) (2 ^ J' X)) * volume (⋃ y ∈ Y, ball y (D ^ k)) := by      rw [ENNReal.mul_right_inj val_ne_zero ENNReal.coe_ne_top]      · rw [measure_biUnion _ hYdisjoint (fun y _ => measurableSet_ball)]        apply hYdisjoint.countable_of_isOpen (fun y _ => isOpen_ball)        intro y _        use y        rw [mem_ball, dist_self]        positivity [realD_pos a]    _ ≤ (As (2 ^ a) (2 ^ J' X)) * volume (ball o (4 * D ^ S)) := by        gcongr        rw [iUnion₂_subset_iff]        intro y hy z hz        specialize hY hy        simp only [mem_ball] at hY hz ⊢        calc          dist z o          _ ≤ dist z y + dist y o := dist_triangle z y o          _ < D ^ k + (4 * D ^ S - D ^ k) := add_lt_add hz hY          _ = 4 * D ^ S := by rw [add_sub_cancel]