Theorem: finset_complex_abs_sum_le (Ray/Misc/Finset.lean)

State before:
N : Finset ℕ
f : ℕ → ℂ
⊢ Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
Tactic:
induction' N using Finset.induction with n N Nn h
State after:
case empty
f : ℕ → ℂ
⊢ Complex.abs (∅.sum fun n => f n) ≤ ∅.sum fun n => Complex.abs (f n)

case insert
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs ((insert n N).sum fun n => f n) ≤ (insert n N).sum fun n => Complex.abs (f n)

State before:
case empty
f : ℕ → ℂ
⊢ Complex.abs (∅.sum fun n => f n) ≤ ∅.sum fun n => Complex.abs (f n)
Tactic:
simp
State after:
no goals

State before:
case insert
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs ((insert n N).sum fun n => f n) ≤ (insert n N).sum fun n => Complex.abs (f n)
Tactic:
rw [Finset.sum_insert Nn]
State after:
case insert
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n + N.sum fun x => f x) ≤ (insert n N).sum fun n => Complex.abs (f n)

State before:
case insert
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n + N.sum fun x => f x) ≤ (insert n N).sum fun n => Complex.abs (f n)
Tactic:
rw [Finset.sum_insert Nn]
State after:
case insert
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n + N.sum fun x => f x) ≤ Complex.abs (f n) + N.sum fun x => Complex.abs (f x)

State before:
case insert
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n + N.sum fun x => f x) ≤ Complex.abs (f n) + N.sum fun x => Complex.abs (f x)
Tactic:
trans abs (f n) + abs (N.sum fun n ↦ f n)
State after:
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n + N.sum fun x => f x) ≤ Complex.abs (f n) + Complex.abs (N.sum fun n => f n)

f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n) + Complex.abs (N.sum fun n => f n) ≤ Complex.abs (f n) + N.sum fun x => Complex.abs (f x)

State before:
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n + N.sum fun x => f x) ≤ Complex.abs (f n) + Complex.abs (N.sum fun n => f n)
Tactic:
exact Complex.abs.add_le _ _
State after:
no goals

State before:
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n) + Complex.abs (N.sum fun n => f n) ≤ Complex.abs (f n) + N.sum fun x => Complex.abs (f x)
Tactic:
apply add_le_add_left
State after:
case bc
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (N.sum fun n => f n) ≤ N.sum fun x => Complex.abs (f x)

State before:
case bc
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (N.sum fun n => f n) ≤ N.sum fun x => Complex.abs (f x)
Tactic:
assumption
State after:
no goals