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

State before:
a : ℝ
c : ℝ≥0
N : Finset ℕ
a0 : 0 ≤ a
a1 : a < 1
⊢ (N.sum fun n => ↑c * a ^ n) ≤ ↑c * (1 - a)⁻¹
Tactic:
rw [←Finset.mul_sum]
State after:
a : ℝ
c : ℝ≥0
N : Finset ℕ
a0 : 0 ≤ a
a1 : a < 1
⊢ (↑c * N.sum fun i => a ^ i) ≤ ↑c * (1 - a)⁻¹

State before:
a : ℝ
c : ℝ≥0
N : Finset ℕ
a0 : 0 ≤ a
a1 : a < 1
⊢ (↑c * N.sum fun i => a ^ i) ≤ ↑c * (1 - a)⁻¹
Tactic:
bound [partial_geometric_bound N a0 a1]
State after:
no goals