Theorem: volume_ball_le_same (Carleson/HomogeneousType.lean)

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
⊢ volume.real (ball x r') ≤ As A s * volume.real (ball x r)
Tactic:
have hn (n : ℕ) : volume.real (ball x (2^n * r)) ≤ A^n * volume.real (ball x r) := by
  induction n
  case zero =>
    simp
  case succ m hm =>
    calc volume.real (ball x (2 ^ (Nat.succ m) * r))
        = volume.real (ball x (2 ^ (m+1) * r)) := by rfl
      _ = volume.real (ball x ((2 ^ m*2^1) * r)) := by norm_cast
      _ = volume.real (ball x (2 * 2 ^ m * r)) := by ring_nf
      _ ≤ A * volume.real (ball x (2 ^ m * r)) := by rw[mul_assoc]; norm_cast; apply volume_ball_two_le_same
      _ ≤ A * (↑(A ^ m) * volume.real (ball x r)) := by gcongr
      _ = A^(Nat.succ m) * volume.real (ball x r) := by rw[<- mul_assoc, pow_succ']
State after:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
⊢ volume.real (ball x r') ≤ As A s * volume.real (ball x r)

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
⊢ volume.real (ball x r') ≤ As A s * volume.real (ball x r)
Tactic:
have haux : s * r ≤ 2 ^ ⌈Real.log s / Real.log 2⌉₊ * r := by
  sorry
State after:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
⊢ volume.real (ball x r') ≤ As A s * volume.real (ball x r)

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
⊢ volume.real (ball x r') ≤ As A s * volume.real (ball x r)
Tactic:
have h1 : ball x r' ⊆ ball x (2 ^ ⌈Real.log s / Real.log 2⌉₊ * r) := by
  calc ball x r' ⊆ ball x (s * r) := by apply ball_subset_ball hs
      _ ⊆ ball x (2 ^ ⌈Real.log s / Real.log 2⌉₊ * r) := by apply ball_subset_ball haux
State after:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
h1 : ball x r' ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
⊢ volume.real (ball x r') ≤ As A s * volume.real (ball x r)

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
h1 : ball x r' ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
⊢ volume.real (ball x r') ≤ As A s * volume.real (ball x r)
Tactic:
calc volume.real (ball x r')
        ≤ volume.real (ball x (2 ^ ⌈Real.log s / Real.log 2⌉₊ * r)) := by gcongr; finiteness
      _ ≤ A^(⌈Real.log s / Real.log 2⌉₊) * volume.real (ball x r) := by apply hn
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
n : ℕ
⊢ volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
Tactic:
induction n
State after:
case zero
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
⊢ volume.real (ball x (2 ^ 0 * r)) ≤ A ^ 0 * volume.real (ball x r)

case succ
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
n✝ : ℕ
a✝ : volume.real (ball x (2 ^ n✝ * r)) ≤ A ^ n✝ * volume.real (ball x r)
⊢ volume.real (ball x (2 ^ (n✝ + 1) * r)) ≤ A ^ (n✝ + 1) * volume.real (ball x r)

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
⊢ volume.real (ball x (2 ^ 0 * r)) ≤ A ^ 0 * volume.real (ball x r)
Tactic:
case zero =>
  simp
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 ^ (m + 1) * r)) ≤ A ^ (m + 1) * volume.real (ball x r)
Tactic:
case succ m hm =>
  calc volume.real (ball x (2 ^ (Nat.succ m) * r))
      = volume.real (ball x (2 ^ (m+1) * r)) := by rfl
    _ = volume.real (ball x ((2 ^ m*2^1) * r)) := by norm_cast
    _ = volume.real (ball x (2 * 2 ^ m * r)) := by ring_nf
    _ ≤ A * volume.real (ball x (2 ^ m * r)) := by rw[mul_assoc]; norm_cast; apply volume_ball_two_le_same
    _ ≤ A * (↑(A ^ m) * volume.real (ball x r)) := by gcongr
    _ = A^(Nat.succ m) * volume.real (ball x r) := by rw[<- mul_assoc, pow_succ']
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
⊢ volume.real (ball x (2 ^ 0 * r)) ≤ A ^ 0 * volume.real (ball x r)
Tactic:
simp
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 ^ (m + 1) * r)) ≤ A ^ (m + 1) * volume.real (ball x r)
Tactic:
calc volume.real (ball x (2 ^ (Nat.succ m) * r))
    = volume.real (ball x (2 ^ (m+1) * r)) := by rfl
  _ = volume.real (ball x ((2 ^ m*2^1) * r)) := by norm_cast
  _ = volume.real (ball x (2 * 2 ^ m * r)) := by ring_nf
  _ ≤ A * volume.real (ball x (2 ^ m * r)) := by rw[mul_assoc]; norm_cast; apply volume_ball_two_le_same
  _ ≤ A * (↑(A ^ m) * volume.real (ball x r)) := by gcongr
  _ = A^(Nat.succ m) * volume.real (ball x r) := by rw[<- mul_assoc, pow_succ']
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 ^ m.succ * r)) = volume.real (ball x (2 ^ (m + 1) * r))
Tactic:
rfl
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 ^ (m + 1) * r)) = volume.real (ball x (2 ^ m * 2 ^ 1 * r))
Tactic:
norm_cast
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 ^ m * 2 ^ 1 * r)) = volume.real (ball x (2 * 2 ^ m * r))
Tactic:
ring_nf
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 * 2 ^ m * r)) ≤ A * volume.real (ball x (2 ^ m * r))
Tactic:
rw[mul_assoc]
State after:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 * (2 ^ m * r))) ≤ A * volume.real (ball x (2 ^ m * r))

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 * (2 ^ m * r))) ≤ A * volume.real (ball x (2 ^ m * r))
Tactic:
norm_cast
State after:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 * (↑(2 ^ m) * r))) ≤ A * volume.real (ball x (↑(2 ^ m) * r))

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 * (↑(2 ^ m) * r))) ≤ A * volume.real (ball x (↑(2 ^ m) * r))
Tactic:
apply volume_ball_two_le_same
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ A * volume.real (ball x (2 ^ m * r)) ≤ A * (A ^ m * volume.real (ball x r))
Tactic:
gcongr
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ A * (A ^ m * volume.real (ball x r)) = A ^ m.succ * volume.real (ball x r)
Tactic:
rw[<- mul_assoc, pow_succ']
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
⊢ s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
Tactic:
sorry
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
⊢ ball x r' ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
Tactic:
calc ball x r' ⊆ ball x (s * r) := by apply ball_subset_ball hs
    _ ⊆ ball x (2 ^ ⌈Real.log s / Real.log 2⌉₊ * r) := by apply ball_subset_ball haux
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
⊢ ball x r' ⊆ ball x (s * r)
Tactic:
apply ball_subset_ball hs
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
⊢ ball x (s * r) ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
Tactic:
apply ball_subset_ball haux
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
h1 : ball x r' ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
⊢ volume.real (ball x r') ≤ volume.real (ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r))
Tactic:
gcongr
State after:
case h₂
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
h1 : ball x r' ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
⊢ autoParam (volume (ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)) ≠ ⊤) _auto✝

State before:
case h₂
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
h1 : ball x r' ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
⊢ autoParam (volume (ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)) ≠ ⊤) _auto✝
Tactic:
finiteness
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
h1 : ball x r' ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
⊢ volume.real (ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)) ≤ A ^ ⌈s.log / Real.log 2⌉₊ * volume.real (ball x r)
Tactic:
apply hn
State after:
no goals