Theorem: late_geometric_bound (Ray/Misc/Bounds.lean)

State before:
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
⊢ (N.sum fun n => a ^ n) ≤ a ^ m * (1 - a)⁻¹
Tactic:
rcases late_series_sum' h (fun n ↦ a^n) with ⟨M,L⟩
State after:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
L : (N.sum fun n => a ^ n) = M.sum fun n => a ^ (n + m)
⊢ (N.sum fun n => a ^ n) ≤ a ^ m * (1 - a)⁻¹

State before:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
L : (N.sum fun n => a ^ n) = M.sum fun n => a ^ (n + m)
⊢ (N.sum fun n => a ^ n) ≤ a ^ m * (1 - a)⁻¹
Tactic:
rw [L]
State after:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
L : (N.sum fun n => a ^ n) = M.sum fun n => a ^ (n + m)
⊢ (M.sum fun n => a ^ (n + m)) ≤ a ^ m * (1 - a)⁻¹

State before:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
L : (N.sum fun n => a ^ n) = M.sum fun n => a ^ (n + m)
⊢ (M.sum fun n => a ^ (n + m)) ≤ a ^ m * (1 - a)⁻¹
Tactic:
clear L
State after:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
⊢ (M.sum fun n => a ^ (n + m)) ≤ a ^ m * (1 - a)⁻¹

State before:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
⊢ (M.sum fun n => a ^ (n + m)) ≤ a ^ m * (1 - a)⁻¹
Tactic:
have pa : (fun n ↦ a^(n + m)) = (fun n ↦ a^n * a^m) := by apply funext; intro n; rw [pow_add]
State after:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
pa : (fun n => a ^ (n + m)) = fun n => a ^ n * a ^ m
⊢ (M.sum fun n => a ^ (n + m)) ≤ a ^ m * (1 - a)⁻¹

State before:
case intro
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
pa : (fun n => a ^ (n + m)) = fun n => a ^ n * a ^ m
⊢ (M.sum fun n => a ^ (n + m)) ≤ a ^ m * (1 - a)⁻¹
Tactic:
calc
  M.sum (fun n ↦ a^(n + m)) = M.sum (fun n ↦ a^n * a^m) := by rw [ pa ]
  _ = M.sum (fun n ↦ a^n) * a^m := (Finset.sum_mul _ _ _).symm
  _ ≤ (1 - a)⁻¹ * a^m := by bound [partial_geometric_bound M a0 a1]
  _ = a^m * (1 - a)⁻¹ := by ring
State after:
no goals

State before:
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
⊢ (fun n => a ^ (n + m)) = fun n => a ^ n * a ^ m
Tactic:
apply funext
State after:
case h
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
⊢ ∀ (x : ℕ), a ^ (x + m) = a ^ x * a ^ m

State before:
case h
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
⊢ ∀ (x : ℕ), a ^ (x + m) = a ^ x * a ^ m
Tactic:
intro n
State after:
case h
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
n : ℕ
⊢ a ^ (n + m) = a ^ n * a ^ m

State before:
case h
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
n : ℕ
⊢ a ^ (n + m) = a ^ n * a ^ m
Tactic:
rw [pow_add]
State after:
no goals

State before:
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
pa : (fun n => a ^ (n + m)) = fun n => a ^ n * a ^ m
⊢ (M.sum fun n => a ^ (n + m)) = M.sum fun n => a ^ n * a ^ m
Tactic:
rw [ pa ]
State after:
no goals

State before:
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
pa : (fun n => a ^ (n + m)) = fun n => a ^ n * a ^ m
⊢ (M.sum fun n => a ^ n) * a ^ m ≤ (1 - a)⁻¹ * a ^ m
Tactic:
bound [partial_geometric_bound M a0 a1]
State after:
no goals

State before:
m : ℕ
a : ℝ
N : Finset ℕ
h : Late N m
a0 : 0 ≤ a
a1 : a < 1
M : Finset ℕ
pa : (fun n => a ^ (n + m)) = fun n => a ^ n * a ^ m
⊢ (1 - a)⁻¹ * a ^ m = a ^ m * (1 - a)⁻¹
Tactic:
ring
State after:
no goals