[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
⊢ ∃ C, ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε)
[PROOFSTEP]
let C := doublingConstant μ
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
⊢ ∃ C, ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε)
[PROOFSTEP]
have hμ : ∀ n : ℕ, ∀ᶠ ε in 𝓝[>] 0, ∀ x, μ (closedBall x ((2 : ℝ) ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε) :=
  by
  intro n
  induction' n with n ih
  · simp
  replace ih := eventually_nhdsWithin_pos_mul_left (two_pos : 0 < (2 : ℝ)) ih
  refine' (ih.and (exists_measure_closedBall_le_mul' μ)).mono fun ε hε x => _
  calc
    μ (closedBall x ((2 : ℝ) ^ (n + 1) * ε)) = μ (closedBall x ((2 : ℝ) ^ n * (2 * ε))) := by rw [pow_succ', mul_assoc]
    _ ≤ ↑(C ^ n) * μ (closedBall x (2 * ε)) := (hε.1 x)
    _ ≤ ↑(C ^ n) * (C * μ (closedBall x ε)) := by gcongr; exact hε.2 x
    _ = ↑(C ^ (n + 1)) * μ (closedBall x ε) := by rw [← mul_assoc, pow_succ', ENNReal.coe_mul]
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
⊢ ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
⊢ ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
⊢ ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ Nat.zero * ε)) ≤ ↑(C ^ Nat.zero) * ↑↑μ (closedBall x ε)
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ih : ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
⊢ ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
    ∀ (x : α), ↑↑μ (closedBall x (2 ^ Nat.succ n * ε)) ≤ ↑(C ^ Nat.succ n) * ↑↑μ (closedBall x ε)
[PROOFSTEP]
replace ih := eventually_nhdsWithin_pos_mul_left (two_pos : 0 < (2 : ℝ)) ih
[GOAL]
case succ
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ih : ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑(C ^ n) * ↑↑μ (closedBall x (2 * ε))
⊢ ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
    ∀ (x : α), ↑↑μ (closedBall x (2 ^ Nat.succ n * ε)) ≤ ↑(C ^ Nat.succ n) * ↑↑μ (closedBall x ε)
[PROOFSTEP]
refine' (ih.and (exists_measure_closedBall_le_mul' μ)).mono fun ε hε x => _
[GOAL]
case succ
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ih : ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑(C ^ n) * ↑↑μ (closedBall x (2 * ε))
ε : ℝ
hε :
  (∀ (x : α), ↑↑μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑(C ^ n) * ↑↑μ (closedBall x (2 * ε))) ∧
    ∀ (x : α), ↑↑μ (closedBall x (2 * ε)) ≤ ↑(doublingConstant μ) * ↑↑μ (closedBall x ε)
x : α
⊢ ↑↑μ (closedBall x (2 ^ Nat.succ n * ε)) ≤ ↑(C ^ Nat.succ n) * ↑↑μ (closedBall x ε)
[PROOFSTEP]
calc
  μ (closedBall x ((2 : ℝ) ^ (n + 1) * ε)) = μ (closedBall x ((2 : ℝ) ^ n * (2 * ε))) := by rw [pow_succ', mul_assoc]
  _ ≤ ↑(C ^ n) * μ (closedBall x (2 * ε)) := (hε.1 x)
  _ ≤ ↑(C ^ n) * (C * μ (closedBall x ε)) := by gcongr; exact hε.2 x
  _ = ↑(C ^ (n + 1)) * μ (closedBall x ε) := by rw [← mul_assoc, pow_succ', ENNReal.coe_mul]
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ih : ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑(C ^ n) * ↑↑μ (closedBall x (2 * ε))
ε : ℝ
hε :
  (∀ (x : α), ↑↑μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑(C ^ n) * ↑↑μ (closedBall x (2 * ε))) ∧
    ∀ (x : α), ↑↑μ (closedBall x (2 * ε)) ≤ ↑(doublingConstant μ) * ↑↑μ (closedBall x ε)
x : α
⊢ ↑↑μ (closedBall x (2 ^ (n + 1) * ε)) = ↑↑μ (closedBall x (2 ^ n * (2 * ε)))
[PROOFSTEP]
rw [pow_succ', mul_assoc]
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ih : ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑(C ^ n) * ↑↑μ (closedBall x (2 * ε))
ε : ℝ
hε :
  (∀ (x : α), ↑↑μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑(C ^ n) * ↑↑μ (closedBall x (2 * ε))) ∧
    ∀ (x : α), ↑↑μ (closedBall x (2 * ε)) ≤ ↑(doublingConstant μ) * ↑↑μ (closedBall x ε)
x : α
⊢ ↑(C ^ n) * ↑↑μ (closedBall x (2 * ε)) ≤ ↑(C ^ n) * (↑C * ↑↑μ (closedBall x ε))
[PROOFSTEP]
gcongr
[GOAL]
case bc
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ih : ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑(C ^ n) * ↑↑μ (closedBall x (2 * ε))
ε : ℝ
hε :
  (∀ (x : α), ↑↑μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑(C ^ n) * ↑↑μ (closedBall x (2 * ε))) ∧
    ∀ (x : α), ↑↑μ (closedBall x (2 * ε)) ≤ ↑(doublingConstant μ) * ↑↑μ (closedBall x ε)
x : α
⊢ ↑↑μ (closedBall x (2 * ε)) ≤ ↑C * ↑↑μ (closedBall x ε)
[PROOFSTEP]
exact hε.2 x
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ih : ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑(C ^ n) * ↑↑μ (closedBall x (2 * ε))
ε : ℝ
hε :
  (∀ (x : α), ↑↑μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑(C ^ n) * ↑↑μ (closedBall x (2 * ε))) ∧
    ∀ (x : α), ↑↑μ (closedBall x (2 * ε)) ≤ ↑(doublingConstant μ) * ↑↑μ (closedBall x ε)
x : α
⊢ ↑(C ^ n) * (↑C * ↑↑μ (closedBall x ε)) = ↑(C ^ (n + 1)) * ↑↑μ (closedBall x ε)
[PROOFSTEP]
rw [← mul_assoc, pow_succ', ENNReal.coe_mul]
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
⊢ ∃ C, ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε)
[PROOFSTEP]
rcases lt_or_le K 1 with (hK | hK)
[GOAL]
case inl
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
hK : K < 1
⊢ ∃ C, ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε)
[PROOFSTEP]
refine' ⟨1, _⟩
[GOAL]
case inl
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
hK : K < 1
⊢ ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑1 * ↑↑μ (closedBall x ε)
[PROOFSTEP]
simp only [ENNReal.coe_one, one_mul]
[GOAL]
case inl
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
hK : K < 1
⊢ ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑↑μ (closedBall x ε)
[PROOFSTEP]
exact
  eventually_mem_nhdsWithin.mono fun ε hε x t ht =>
    measure_mono <| closedBall_subset_closedBall (by nlinarith [mem_Ioi.mp hε])
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
hK : K < 1
ε : ℝ
hε : ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ t * ε ≤ ε
[PROOFSTEP]
nlinarith [mem_Ioi.mp hε]
[GOAL]
case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
hK : 1 ≤ K
⊢ ∃ C, ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε)
[PROOFSTEP]
refine'
  ⟨C ^ ⌈Real.logb 2 K⌉₊,
    ((hμ ⌈Real.logb 2 K⌉₊).and eventually_mem_nhdsWithin).mono fun ε hε x t ht =>
      le_trans (measure_mono <| closedBall_subset_closedBall _) (hε.1 x)⟩
[GOAL]
case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε :
  (∀ (x : α), ↑↑μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * ↑↑μ (closedBall x ε)) ∧
    ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ t * ε ≤ 2 ^ ⌈Real.logb 2 K⌉₊ * ε
[PROOFSTEP]
refine' mul_le_mul_of_nonneg_right (ht.trans _) (mem_Ioi.mp hε.2).le
[GOAL]
case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε :
  (∀ (x : α), ↑↑μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * ↑↑μ (closedBall x ε)) ∧
    ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ K ≤ 2 ^ ⌈Real.logb 2 K⌉₊
[PROOFSTEP]
conv_lhs => rw [← Real.rpow_logb two_pos (by norm_num) (by linarith : 0 < K)]
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε :
  (∀ (x : α), ↑↑μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * ↑↑μ (closedBall x ε)) ∧
    ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
| K
[PROOFSTEP]
rw [← Real.rpow_logb two_pos (by norm_num) (by linarith : 0 < K)]
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε :
  (∀ (x : α), ↑↑μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * ↑↑μ (closedBall x ε)) ∧
    ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
| K
[PROOFSTEP]
rw [← Real.rpow_logb two_pos (by norm_num) (by linarith : 0 < K)]
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε :
  (∀ (x : α), ↑↑μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * ↑↑μ (closedBall x ε)) ∧
    ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
| K
[PROOFSTEP]
rw [← Real.rpow_logb two_pos (by norm_num) (by linarith : 0 < K)]
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε :
  (∀ (x : α), ↑↑μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * ↑↑μ (closedBall x ε)) ∧
    ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ 2 ≠ 1
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε :
  (∀ (x : α), ↑↑μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * ↑↑μ (closedBall x ε)) ∧
    ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ 0 < K
[PROOFSTEP]
linarith
[GOAL]
case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε :
  (∀ (x : α), ↑↑μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * ↑↑μ (closedBall x ε)) ∧
    ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ 2 ^ Real.logb 2 K ≤ 2 ^ ⌈Real.logb 2 K⌉₊
[PROOFSTEP]
rw [← Real.rpow_nat_cast]
[GOAL]
case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
hμ : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
hK : 1 ≤ K
ε : ℝ
hε :
  (∀ (x : α), ↑↑μ (closedBall x (2 ^ ⌈Real.logb 2 K⌉₊ * ε)) ≤ ↑(C ^ ⌈Real.logb 2 K⌉₊) * ↑↑μ (closedBall x ε)) ∧
    ε ∈ Ioi 0
x : α
t : ℝ
ht : t ≤ K
⊢ 2 ^ Real.logb 2 K ≤ 2 ^ ↑⌈Real.logb 2 K⌉₊
[PROOFSTEP]
exact Real.rpow_le_rpow_of_exponent_le one_le_two (Nat.le_ceil (Real.logb 2 K))
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
⊢ ∃ R,
    0 < R ∧
      ∀ (x : α) (t r : ℝ),
        t ∈ Ioc 0 K → r ≤ R → ↑↑μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * ↑↑μ (closedBall x r)
[PROOFSTEP]
have h := Classical.choose_spec (exists_eventually_forall_measure_closedBall_le_mul μ K)
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
    ∀ (x : α) (t : ℝ),
      t ≤ K →
        ↑↑μ (closedBall x (t * ε)) ≤
          ↑(Classical.choose
                (_ :
                  ∃ C,
                    ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                      ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
            ↑↑μ (closedBall x ε)
⊢ ∃ R,
    0 < R ∧
      ∀ (x : α) (t r : ℝ),
        t ∈ Ioc 0 K → r ≤ R → ↑↑μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * ↑↑μ (closedBall x r)
[PROOFSTEP]
rcases mem_nhdsWithin_Ioi_iff_exists_Ioc_subset.1 h with ⟨R, Rpos, hR⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
    ∀ (x : α) (t : ℝ),
      t ≤ K →
        ↑↑μ (closedBall x (t * ε)) ≤
          ↑(Classical.choose
                (_ :
                  ∃ C,
                    ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                      ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
            ↑↑μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆
    {x |
      (fun ε =>
          ∀ (x : α) (t : ℝ),
            t ≤ K →
              ↑↑μ (closedBall x (t * ε)) ≤
                ↑(Classical.choose
                      (_ :
                        ∃ C,
                          ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                            ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
                  ↑↑μ (closedBall x ε))
        x}
⊢ ∃ R,
    0 < R ∧
      ∀ (x : α) (t r : ℝ),
        t ∈ Ioc 0 K → r ≤ R → ↑↑μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * ↑↑μ (closedBall x r)
[PROOFSTEP]
refine' ⟨R, Rpos, fun x t r ht hr => _⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
    ∀ (x : α) (t : ℝ),
      t ≤ K →
        ↑↑μ (closedBall x (t * ε)) ≤
          ↑(Classical.choose
                (_ :
                  ∃ C,
                    ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                      ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
            ↑↑μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆
    {x |
      (fun ε =>
          ∀ (x : α) (t : ℝ),
            t ≤ K →
              ↑↑μ (closedBall x (t * ε)) ≤
                ↑(Classical.choose
                      (_ :
                        ∃ C,
                          ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                            ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
                  ↑↑μ (closedBall x ε))
        x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
⊢ ↑↑μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * ↑↑μ (closedBall x r)
[PROOFSTEP]
rcases lt_trichotomy r 0 with (rneg | rfl | rpos)
[GOAL]
case intro.intro.inl
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
    ∀ (x : α) (t : ℝ),
      t ≤ K →
        ↑↑μ (closedBall x (t * ε)) ≤
          ↑(Classical.choose
                (_ :
                  ∃ C,
                    ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                      ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
            ↑↑μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆
    {x |
      (fun ε =>
          ∀ (x : α) (t : ℝ),
            t ≤ K →
              ↑↑μ (closedBall x (t * ε)) ≤
                ↑(Classical.choose
                      (_ :
                        ∃ C,
                          ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                            ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
                  ↑↑μ (closedBall x ε))
        x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rneg : r < 0
⊢ ↑↑μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * ↑↑μ (closedBall x r)
[PROOFSTEP]
have : t * r < 0 := mul_neg_of_pos_of_neg ht.1 rneg
[GOAL]
case intro.intro.inl
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
    ∀ (x : α) (t : ℝ),
      t ≤ K →
        ↑↑μ (closedBall x (t * ε)) ≤
          ↑(Classical.choose
                (_ :
                  ∃ C,
                    ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                      ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
            ↑↑μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆
    {x |
      (fun ε =>
          ∀ (x : α) (t : ℝ),
            t ≤ K →
              ↑↑μ (closedBall x (t * ε)) ≤
                ↑(Classical.choose
                      (_ :
                        ∃ C,
                          ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                            ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
                  ↑↑μ (closedBall x ε))
        x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rneg : r < 0
this : t * r < 0
⊢ ↑↑μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * ↑↑μ (closedBall x r)
[PROOFSTEP]
simp only [closedBall_eq_empty.2 this, measure_empty, zero_le']
[GOAL]
case intro.intro.inr.inl
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
    ∀ (x : α) (t : ℝ),
      t ≤ K →
        ↑↑μ (closedBall x (t * ε)) ≤
          ↑(Classical.choose
                (_ :
                  ∃ C,
                    ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                      ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
            ↑↑μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆
    {x |
      (fun ε =>
          ∀ (x : α) (t : ℝ),
            t ≤ K →
              ↑↑μ (closedBall x (t * ε)) ≤
                ↑(Classical.choose
                      (_ :
                        ∃ C,
                          ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                            ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
                  ↑↑μ (closedBall x ε))
        x}
x : α
t : ℝ
ht : t ∈ Ioc 0 K
hr : 0 ≤ R
⊢ ↑↑μ (closedBall x (t * 0)) ≤ ↑(scalingConstantOf μ K) * ↑↑μ (closedBall x 0)
[PROOFSTEP]
simp only [mul_zero, closedBall_zero]
[GOAL]
case intro.intro.inr.inl
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
    ∀ (x : α) (t : ℝ),
      t ≤ K →
        ↑↑μ (closedBall x (t * ε)) ≤
          ↑(Classical.choose
                (_ :
                  ∃ C,
                    ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                      ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
            ↑↑μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆
    {x |
      (fun ε =>
          ∀ (x : α) (t : ℝ),
            t ≤ K →
              ↑↑μ (closedBall x (t * ε)) ≤
                ↑(Classical.choose
                      (_ :
                        ∃ C,
                          ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                            ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
                  ↑↑μ (closedBall x ε))
        x}
x : α
t : ℝ
ht : t ∈ Ioc 0 K
hr : 0 ≤ R
⊢ ↑↑μ {x} ≤ ↑(scalingConstantOf μ K) * ↑↑μ {x}
[PROOFSTEP]
refine' le_mul_of_one_le_of_le _ le_rfl
[GOAL]
case intro.intro.inr.inl
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
    ∀ (x : α) (t : ℝ),
      t ≤ K →
        ↑↑μ (closedBall x (t * ε)) ≤
          ↑(Classical.choose
                (_ :
                  ∃ C,
                    ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                      ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
            ↑↑μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆
    {x |
      (fun ε =>
          ∀ (x : α) (t : ℝ),
            t ≤ K →
              ↑↑μ (closedBall x (t * ε)) ≤
                ↑(Classical.choose
                      (_ :
                        ∃ C,
                          ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                            ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
                  ↑↑μ (closedBall x ε))
        x}
x : α
t : ℝ
ht : t ∈ Ioc 0 K
hr : 0 ≤ R
⊢ 1 ≤ ↑(scalingConstantOf μ K)
[PROOFSTEP]
apply ENNReal.one_le_coe_iff.2 (le_max_right _ _)
[GOAL]
case intro.intro.inr.inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
    ∀ (x : α) (t : ℝ),
      t ≤ K →
        ↑↑μ (closedBall x (t * ε)) ≤
          ↑(Classical.choose
                (_ :
                  ∃ C,
                    ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                      ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
            ↑↑μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆
    {x |
      (fun ε =>
          ∀ (x : α) (t : ℝ),
            t ≤ K →
              ↑↑μ (closedBall x (t * ε)) ≤
                ↑(Classical.choose
                      (_ :
                        ∃ C,
                          ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                            ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
                  ↑↑μ (closedBall x ε))
        x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rpos : 0 < r
⊢ ↑↑μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * ↑↑μ (closedBall x r)
[PROOFSTEP]
apply (hR ⟨rpos, hr⟩ x t ht.2).trans _
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h :
  ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
    ∀ (x : α) (t : ℝ),
      t ≤ K →
        ↑↑μ (closedBall x (t * ε)) ≤
          ↑(Classical.choose
                (_ :
                  ∃ C,
                    ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                      ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
            ↑↑μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆
    {x |
      (fun ε =>
          ∀ (x : α) (t : ℝ),
            t ≤ K →
              ↑↑μ (closedBall x (t * ε)) ≤
                ↑(Classical.choose
                      (_ :
                        ∃ C,
                          ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                            ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
                  ↑↑μ (closedBall x ε))
        x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rpos : 0 < r
⊢ ↑(Classical.choose
          (_ :
            ∃ C,
              ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
      ↑↑μ (closedBall x r) ≤
    ↑(scalingConstantOf μ K) * ↑↑μ (closedBall x r)
[PROOFSTEP]
exact mul_le_mul_right' (ENNReal.coe_le_coe.2 (le_max_left _ _)) _
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
⊢ ∀ᶠ (r : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (K * r)) ≤ ↑(scalingConstantOf μ K) * ↑↑μ (closedBall x r)
[PROOFSTEP]
filter_upwards [Classical.choose_spec (exists_eventually_forall_measure_closedBall_le_mul μ K)] with r hr x
[GOAL]
case h
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K r : ℝ
hr :
  ∀ (x : α) (t : ℝ),
    t ≤ K →
      ↑↑μ (closedBall x (t * r)) ≤
        ↑(Classical.choose
              (_ :
                ∃ C,
                  ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                    ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
          ↑↑μ (closedBall x r)
x : α
⊢ ↑↑μ (closedBall x (K * r)) ≤ ↑(scalingConstantOf μ K) * ↑↑μ (closedBall x r)
[PROOFSTEP]
exact (hr x K le_rfl).trans (mul_le_mul_right' (ENNReal.coe_le_coe.2 (le_max_left _ _)) _)
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
⊢ ∀ᶠ (r : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x r) ≤ ↑(scalingConstantOf μ K⁻¹) * ↑↑μ (closedBall x (K * r))
[PROOFSTEP]
convert eventually_nhdsWithin_pos_mul_left hK (eventually_measure_le_scaling_constant_mul μ K⁻¹)
[GOAL]
case h.e'_2.h.h.h.e'_3.h.e'_3.h.e'_4
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
x✝ : ℝ
a✝ : α
⊢ x✝ = K⁻¹ * (K * x✝)
[PROOFSTEP]
simp [inv_mul_cancel_left₀ hK.ne']
