MeasureTheory.measure_ball_le_same

lemma measure_ball_le_same (x : X) {r s r' : ℝ} (hsp : 0 < s) (hs : r' ≤ s * r) :    μ (ball x r') ≤ As A s * μ (ball x r) := by  /- If the large ball is empty, all balls are -/  by_cases! hr : r < 0  · have hr' : r' < 0 := by      calc r' ≤ s * r := hs      _ < 0 := mul_neg_of_pos_of_neg hsp hr    simp [ball_eq_empty.mpr hr.le, ball_eq_empty.mpr hr'.le]  /- Show inclusion in larger ball -/  have haux : s * r ≤ 2 ^ ⌈Real.logb 2 s⌉₊ * r := by    gcongr    apply Real.le_pow_natCeil_logb (by norm_num) hsp  have h1 : ball x r' ⊆ ball x (2 ^ ⌈Real.logb 2 s⌉₊ * r) := ball_subset_ball <| hs.trans haux  /- Apply result for power of two to slightly larger ball -/  calc μ (ball x r')      ≤ μ (ball x (2 ^ ⌈Real.logb 2 s⌉₊ * r)) := by gcongr    _ ≤ As A s * μ (ball x r) := measure_ball_two_le_same_iterate x r _