Indexed Sum Equals Multiset Sum

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.NewtonIdentities

Statement

Theorem Indexed Sum Equals Multiset Sum
[blueprint]

$\sum_{i \in \mathrm{Fin}(\lvert l\rvert)} g(l[i]) = \sum_{x \in l} g(x).$

theorem fin_sum_eq_multiset_sum (l : List ℝ) (g : ℝ → ℝ) :
    ∑ i : Fin l.length, g (l.get i) = ((↑l : Multiset ℝ).map g).sum := by
Proof ▼ 


  -- Key: convert the Finset sum to List sum via List.ofFn
  conv_lhs => rw [← List.sum_ofFn]
  -- Convert l.get to bracket notation
  change (List.ofFn fun i => g l[i.val]).sum = (Multiset.map g ↑l).sum
  -- Now use List.ofFn_getElem_eq_map which says ofFn (fun i => g (l[i])) = l.map g
  rw [List.ofFn_getElem_eq_map]
  -- List.sum = Multiset.sum for coerced lists
  rfl

Dependencies (uses)

None

Dependents (used by)

Neighborhood

Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms