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

State before:
A B : Finset ℕ
f : ℕ → ℂ
⊢ dist (A.sum f) (B.sum f) ≤ (A ∆ B).sum fun n => Complex.abs (f n)
Tactic:
rw [finset_sum_partition A B f, finset_sum_partition B A f, Finset.inter_comm B A]
State after:
A B : Finset ℕ
f : ℕ → ℂ
⊢ dist ((A \ B).sum f + (A ∩ B).sum f) ((B \ A).sum f + (A ∩ B).sum f) ≤ (A ∆ B).sum fun n => Complex.abs (f n)

State before:
A B : Finset ℕ
f : ℕ → ℂ
⊢ dist ((A \ B).sum f + (A ∩ B).sum f) ((B \ A).sum f + (A ∩ B).sum f) ≤ (A ∆ B).sum fun n => Complex.abs (f n)
Tactic:
rw [dist_add_right ((A \ B).sum f) ((B \ A).sum f) ((A ∩ B).sum f)]
State after:
A B : Finset ℕ
f : ℕ → ℂ
⊢ dist ((A \ B).sum f) ((B \ A).sum f) ≤ (A ∆ B).sum fun n => Complex.abs (f n)

State before:
A B : Finset ℕ
f : ℕ → ℂ
⊢ dist ((A \ B).sum f) ((B \ A).sum f) ≤ (A ∆ B).sum fun n => Complex.abs (f n)
Tactic:
rw [Complex.dist_eq]
State after:
A B : Finset ℕ
f : ℕ → ℂ
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤ (A ∆ B).sum fun n => Complex.abs (f n)

State before:
A B : Finset ℕ
f : ℕ → ℂ
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤ (A ∆ B).sum fun n => Complex.abs (f n)
Tactic:
trans (A \ B).sum (fun n ↦ abs (f n)) + (B \ A).sum (fun n ↦ abs (f n))
State after:
A B : Finset ℕ
f : ℕ → ℂ
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤
    ((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)

A B : Finset ℕ
f : ℕ → ℂ
⊢ (((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)) ≤
    (A ∆ B).sum fun n => Complex.abs (f n)

State before:
A B : Finset ℕ
f : ℕ → ℂ
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤
    ((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)
Tactic:
have ha := finset_complex_abs_sum_le (A \ B) f
State after:
A B : Finset ℕ
f : ℕ → ℂ
ha : Complex.abs ((A \ B).sum fun n => f n) ≤ (A \ B).sum fun n => Complex.abs (f n)
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤
    ((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)

State before:
A B : Finset ℕ
f : ℕ → ℂ
ha : Complex.abs ((A \ B).sum fun n => f n) ≤ (A \ B).sum fun n => Complex.abs (f n)
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤
    ((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)
Tactic:
have hb := finset_complex_abs_sum_le (B \ A) f
State after:
A B : Finset ℕ
f : ℕ → ℂ
ha : Complex.abs ((A \ B).sum fun n => f n) ≤ (A \ B).sum fun n => Complex.abs (f n)
hb : Complex.abs ((B \ A).sum fun n => f n) ≤ (B \ A).sum fun n => Complex.abs (f n)
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤
    ((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)

State before:
A B : Finset ℕ
f : ℕ → ℂ
ha : Complex.abs ((A \ B).sum fun n => f n) ≤ (A \ B).sum fun n => Complex.abs (f n)
hb : Complex.abs ((B \ A).sum fun n => f n) ≤ (B \ A).sum fun n => Complex.abs (f n)
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤
    ((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)
Tactic:
calc abs ((A \ B).sum f - (B \ A).sum f)
  _ ≤ abs ((A \ B).sum f) + abs ((B \ A).sum f) := by bound
  _ ≤ (A \ B).sum (fun n ↦ abs (f n)) + (B \ A).sum (fun n ↦ abs (f n)) := by bound
State after:
no goals

State before:
A B : Finset ℕ
f : ℕ → ℂ
ha : Complex.abs ((A \ B).sum fun n => f n) ≤ (A \ B).sum fun n => Complex.abs (f n)
hb : Complex.abs ((B \ A).sum fun n => f n) ≤ (B \ A).sum fun n => Complex.abs (f n)
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤ Complex.abs ((A \ B).sum f) + Complex.abs ((B \ A).sum f)
Tactic:
bound
State after:
no goals

State before:
A B : Finset ℕ
f : ℕ → ℂ
ha : Complex.abs ((A \ B).sum fun n => f n) ≤ (A \ B).sum fun n => Complex.abs (f n)
hb : Complex.abs ((B \ A).sum fun n => f n) ≤ (B \ A).sum fun n => Complex.abs (f n)
⊢ Complex.abs ((A \ B).sum f) + Complex.abs ((B \ A).sum f) ≤
    ((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)
Tactic:
bound
State after:
no goals

State before:
A B : Finset ℕ
f : ℕ → ℂ
⊢ (((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)) ≤
    (A ∆ B).sum fun n => Complex.abs (f n)
Tactic:
apply le_of_eq
State after:
case a
A B : Finset ℕ
f : ℕ → ℂ
⊢ (((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)) =
    (A ∆ B).sum fun n => Complex.abs (f n)

State before:
case a
A B : Finset ℕ
f : ℕ → ℂ
⊢ (((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)) =
    (A ∆ B).sum fun n => Complex.abs (f n)
Tactic:
rw [←Finset.sum_union (sdiff_sdiff_disjoint A B), symmDiff_union]
State after:
no goals