α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
⊢ ∃ C, ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε)
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
⊢ ∃ C, ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε)
let C := doublingConstant μ
case inl
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)

case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
rcases lt_or_le K 1 with (hK | hK)
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
⊢ ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
⊢ ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
intro n
case zero
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
⊢ ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ Nat.zero * ε)) ≤ ↑(C ^ Nat.zero) * ↑↑μ (closedBall x ε)

case succ
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
⊢ ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * ↑↑μ (closedBall x ε)
induction' n with n ih
case succ
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
case succ
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
replace ih := eventually_nhdsWithin_pos_mul_left (two_pos : 0 < (2 : ℝ)) ih
case succ
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
case succ
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
refine' (ih.and (exists_measure_closedBall_le_mul' μ)).mono fun ε hε x => _
no goals
case succ
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
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]
no goals
case zero
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
⊢ ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (2 ^ Nat.zero * ε)) ≤ ↑(C ^ Nat.zero) * ↑↑μ (closedBall x ε)
simp
no goals
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 * ε)))
rw [pow_succ', mul_assoc]
case bc
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε))
gcongr
no goals
case bc
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
exact hε.2 x
no goals
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
rw [← mul_assoc, pow_succ', ENNReal.coe_mul]
case inl
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
case inl
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
refine' ⟨1, _⟩
case inl
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
case inl
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
simp only [ENNReal.coe_one, one_mul]
no goals
case inl
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
exact
  eventually_mem_nhdsWithin.mono fun ε hε x t ht =>
    measure_mono <| closedBall_subset_closedBall (by nlinarith [mem_Ioi.mp hε])
no goals
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 * ε ≤ ε
nlinarith [mem_Ioi.mp hε]
case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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⌉₊ * ε
case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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 ε)
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)⟩
case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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⌉₊
case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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⌉₊ * ε
refine' mul_le_mul_of_nonneg_right (ht.trans _) (mem_Ioi.mp hε.2).le
case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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⌉₊
case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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⌉₊
conv_lhs => rw [← Real.rpow_logb two_pos (by norm_num) (by linarith : 0 < K)]
case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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⌉₊
case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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⌉₊
rw [← Real.rpow_nat_cast]
no goals
case inr
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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⌉₊
exact Real.rpow_le_rpow_of_exponent_le one_le_two (Nat.le_ceil (Real.logb 2 K))
no goals
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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
norm_num
no goals
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.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
linarith