-- Mathlib/Analysis/SpecificLimits/Normed.lean
lemma hasSum_choose_mul_geometric_of_norm_lt_one'
    (k : ℕ) {r : R} (hr : ‖r‖ < 1) :
    HasSum (fun n ↦ (n + k).choose k * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
I1 : Summable fun n => ‖↑((n + k).choose k) * r ^ n‖
n i : ℕ
hi : i < n + 1
⊢ ↑((i + k).choose k) * r ^ i * r ^ (n - i) = ↑((i + k).choose k) * r ^ n

Tactic:
rw [mul_assoc, ← pow_add, show i + (n - i) = n by omega]

Result:
no goals

Proof state:
case h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
n : ℕ
hn : k < n
⊢ ↑((n + k).choose k) ≤ 2 ^ k * ↑n ^ k

Tactic:
norm_cast

Result:
case h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
n : ℕ
hn : k < n
⊢ (n + k).choose k ≤ 2 ^ k * n ^ k

Proof state:
case h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
n : ℕ
hn : k < n
⊢ ‖↑((n + k).choose k)‖ ≤ 2 ^ k * ‖↑(n ^ k)‖

Tactic:
simp only [Real.norm_eq_abs, abs_cast, cast_pow, norm_pow]

Result:
case h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
n : ℕ
hn : k < n
⊢ ↑((n + k).choose k) ≤ 2 ^ k * ↑n ^ k

Proof state:
case succ
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
⊢ HasSum (fun n => ↑((n + (k + 1)).choose (k + 1)) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1 + 1))

Tactic:
have I1 : Summable (fun (n : ℕ) ↦ ‖(n + k).choose k * r ^ n‖) := by
  apply summable_norm_mul_geometric_of_norm_lt_one (k := k) hr
  apply isBigO_iff.2 ⟨2 ^ k, ?_⟩
  filter_upwards [Ioi_mem_atTop k] with n (hn : k < n)
  simp only [Real.norm_eq_abs, abs_cast, cast_pow, norm_pow]
  norm_cast
  calc (n + k).choose k
    _ ≤ (2 * n).choose k := choose_le_choose k (by omega)
    _ ≤ (2 * n) ^ k := Nat.choose_le_pow _ _
    _ = 2 ^ k * n ^ k := Nat.mul_pow 2 n k

Result:
case succ
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
I1 : Summable fun n => ‖↑((n + k).choose k) * r ^ n‖
⊢ HasSum (fun n => ↑((n + (k + 1)).choose (k + 1)) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1 + 1))

Proof state:
case h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
n : ℕ
hn : k < n
⊢ (n + k).choose k ≤ 2 ^ k * n ^ k

Tactic:
calc (n + k).choose k
  _ ≤ (2 * n).choose k := choose_le_choose k (by omega)
  _ ≤ (2 * n) ^ k := Nat.choose_le_pow _ _
  _ = 2 ^ k * n ^ k := Nat.mul_pow 2 n k

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
I1 : Summable fun n => ‖↑((n + k).choose k) * r ^ n‖
n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ i * r ^ (n - i) =
    ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ n

Tactic:
apply Finset.sum_congr rfl (fun i hi ↦ ?_)

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
I1 : Summable fun n => ‖↑((n + k).choose k) * r ^ n‖
n i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ↑((i + k).choose k) * r ^ i * r ^ (n - i) = ↑((i + k).choose k) * r ^ n

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
⊢ (fun n => ↑((n + k).choose k)) =O[atTop] fun n => ↑(n ^ k)

Tactic:
apply isBigO_iff.2 ⟨2 ^ k, ?_⟩

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
⊢ ∀ᶠ (x : ℕ) in atTop, ‖↑((x + k).choose k)‖ ≤ 2 ^ k * ‖↑(x ^ k)‖

Proof state:
case h.e'_5.h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
I1 : Summable fun n => ‖↑((n + k).choose k) * r ^ n‖
n : ℕ
this :
  ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ i * r ^ (n - i) =
    ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ n
⊢ ↑((n + (k + 1)).choose (k + 1)) * r ^ n =
    ∑ k_1 ∈ Finset.range (n + 1), ↑((k_1 + k).choose k) * r ^ k_1 * r ^ (n - k_1)

Tactic:
simp [this, ← sum_mul, ← Nat.cast_sum, sum_range_add_choose n k, add_assoc]

Result:
no goals

Proof state:
case h.e'_6
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
I1 : Summable fun n => ‖↑((n + k).choose k) * r ^ n‖
⊢ Ring.inverse (1 - r) ^ (k + 1 + 1) = (∑' (n : ℕ), ↑((n + k).choose k) * r ^ n) * ∑' (n : ℕ), r ^ n

Tactic:
rw [ih.tsum_eq, (hasSum_geom_series_inverse r hr).tsum_eq, pow_succ]

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
I1 : Summable fun n => ‖↑((n + k).choose k) * r ^ n‖
n i : ℕ
hi : i < n + 1
⊢ i + (n - i) = n

Tactic:
omega

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
n : ℕ
hn : k < n
⊢ n + k ≤ 2 * n

Tactic:
omega

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
I1 : Summable fun n => ‖↑((n + k).choose k) * r ^ n‖
n i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ↑((i + k).choose k) * r ^ i * r ^ (n - i) = ↑((i + k).choose k) * r ^ n

Tactic:
simp only [Finset.mem_range] at hi

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
I1 : Summable fun n => ‖↑((n + k).choose k) * r ^ n‖
n i : ℕ
hi : i < n + 1
⊢ ↑((i + k).choose k) * r ^ i * r ^ (n - i) = ↑((i + k).choose k) * r ^ n

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
⊢ Summable fun n => ‖↑((n + k).choose k) * r ^ n‖

Tactic:
apply summable_norm_mul_geometric_of_norm_lt_one (k := k) hr

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
⊢ (fun n => ↑((n + k).choose k)) =O[atTop] fun n => ↑(n ^ k)

Proof state:
case zero
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
⊢ HasSum (fun n => ↑((n + 0).choose 0) * r ^ n) (Ring.inverse (1 - r) ^ (0 + 1))

Tactic:
simpa using hasSum_geom_series_inverse r hr

Result:
no goals