English
msymm μ can be expressed as a finite sum over all s in univ of (multiset.map X s.val).prod, relating to exponent multisets μ.
Русский
Msymm μ может быть выражен как конечная сумма по всем s в univ от (multiset.map X s.val).prod, соответствующая мульти-множества степеней μ.
LaTeX
$$$\\mathrm{msymm}_{\\sigma,R}(\\mu) = \\sum_{s \\in \\mathrm{univ}} (\\mathrm{multiset.map}\\ \\mathrm{MvPolynomial.X}\\ s.1.1).\\mathrm{prod}$$$
Lean4
theorem accumulate_invAccumulate {n m} (hmn : m ≤ n) {s : Fin m → ℕ} (hs : Antitone s) :
accumulate n m (invAccumulate n m s) = s :=
funext <| fun ⟨i, hi⟩ ↦ by
have := Nat.le_sub_one_of_lt hi
revert hi
refine Nat.decreasingInduction' (fun i hi _ ih him ↦ ?_) this fun hm ↦ ?_
· rw [← Nat.pred_eq_sub_one, Nat.lt_pred_iff, Nat.succ_eq_add_one] at hi
rw [accumulate_rec (him.trans_le hmn) hi, ih hi, invAccumulate, dif_pos him, dif_pos hi]
simp only
exact Nat.sub_add_cancel (hs i.le_succ)
· have := (Nat.sub_one_add_one <| Nat.ne_zero_of_lt hm).symm
rw [accumulate_last (hm.trans_le hmn) this, invAccumulate, dif_pos hm, dif_neg this.not_gt, Nat.sub_zero]
intro j hj
rw [invAccumulate, dif_neg hj.not_gt, Nat.zero_sub]
