MeasureTheory.eq_zero_of_isDoubling_lt_one

lemma eq_zero_of_isDoubling_lt_one [ProperSpace X] [IsFiniteMeasureOnCompacts μ] (hA : A < 1) :    μ = 0 := by  rcases isEmpty_or_nonempty X with hX | ⟨⟨x⟩⟩  · simp [eq_zero_of_isEmpty μ]  have M (r : ℝ) (hr : 0 ≤ r) : μ (ball x r) = 0 := by    have I : μ (ball x r) ≤ A * μ (ball x r) := calc      _ = μ (ball x (2 * (r / 2))) := by        have : 2 * (r / 2) = r := by ring        simp [this]      _ ≤ A * μ (ball x (r / 2)) := by        apply measure_ball_two_le_same (μ := μ)      _ ≤ A * μ (ball x r) := by gcongr; linarith    by_contra H    have : μ (ball x r) < 1 * μ (ball x r) := by      apply I.trans_lt (ENNReal.mul_lt_mul_left H measure_ball_lt_top.ne (mod_cast hA))    simp at this  rw [← measure_univ_eq_zero, ← iUnion_ball_nat x]  exact measure_iUnion_null_iff.mpr fun i ↦ M i (by positivity)