α : Type ?u.233518
β : Type ?u.233521
ι : Type ?u.233524
n : ℕ
A : Summable fun i => if n ≤ i then 2⁻¹ ^ i else 0
B : (∑ i in Finset.range n, if n ≤ i then 2⁻¹ ^ i else 0) = 0
⊢ (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n
α : Type ?u.233518
β : Type ?u.233521
ι : Type ?u.233524
n : ℕ
A : Summable fun i => if n ≤ i then 2⁻¹ ^ i else 0
⊢ (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n
have B : ((Finset.range n).sum fun i : ℕ => ite (n ≤ i) ((2⁻¹ : ℝ) ^ i) 0) = 0 :=
  Finset.sum_eq_zero fun i hi =>
    ite_eq_right_iff.2 fun h => (lt_irrefl _ ((Finset.mem_range.1 hi).trans_le h)).elim
no goals
α : Type ?u.233518
β : Type ?u.233521
ι : Type ?u.233524
n : ℕ
A : Summable fun i => if n ≤ i then 2⁻¹ ^ i else 0
B : (∑ i in Finset.range n, if n ≤ i then 2⁻¹ ^ i else 0) = 0
⊢ (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n
simp only [← _root_.sum_add_tsum_nat_add n A, B, if_true, zero_add, zero_le',
  le_add_iff_nonneg_left, pow_add, _root_.tsum_mul_right, tsum_geometric_inv_two]
α : Type ?u.233518
β : Type ?u.233521
ι : Type ?u.233524
n i : ℕ
⊢ (if n ≤ i then 2⁻¹ ^ i else 0) ≤ (1 / 2) ^ i
α : Type ?u.233518
β : Type ?u.233521
ι : Type ?u.233524
n : ℕ
⊢ ∀ (b : ℕ), (if n ≤ b then 2⁻¹ ^ b else 0) ≤ (1 / 2) ^ b
intro i
case neg
α : Type ?u.233518
β : Type ?u.233521
ι : Type ?u.233524
n i : ℕ
hi : ¬n ≤ i
⊢ 0 ≤ 2 ^ i
α : Type ?u.233518
β : Type ?u.233521
ι : Type ?u.233524
n i : ℕ
⊢ (if n ≤ i then 2⁻¹ ^ i else 0) ≤ (1 / 2) ^ i
by_cases hi : n ≤ i <;> simp [hi]
case neg.H
α : Type ?u.233518
β : Type ?u.233521
ι : Type ?u.233524
n i : ℕ
hi : ¬n ≤ i
⊢ 0 ≤ 2
case neg
α : Type ?u.233518
β : Type ?u.233521
ι : Type ?u.233524
n i : ℕ
hi : ¬n ≤ i
⊢ 0 ≤ 2 ^ i
apply pow_nonneg
no goals
case neg.H
α : Type ?u.233518
β : Type ?u.233521
ι : Type ?u.233524
n i : ℕ
hi : ¬n ≤ i
⊢ 0 ≤ 2
exact zero_le_two