English
Under the additional assumption r ≠ 0, the identity of the previous item remains: ofLex (supDegree toLex (esymmAlgMonomial (Fin m) t r)) = accumulate n m t for t ∈ Fin n →₀ ℕ and n ≤ m.
Русский
Дополнительно, при r ≠ 0 формула сохраняется: ofLex (supDegree toLex (esymmAlgMonomial (Fin m) t r)) = accumulate n m t.
LaTeX
$$$\text{ofLex}(\operatorname{supDegree} \text{toLex} <| \operatorname{esymmAlgMonomial} (\operatorname{Fin} m) t r) = \operatorname{accumulate} n m t$$
Lean4
theorem antitone_supDegree [LinearOrder σ] {p : MvPolynomial σ R} (hp : p.IsSymmetric) :
Antitone ↑(ofLex <| p.supDegree toLex) :=
by
obtain rfl | h0 := eq_or_ne p 0
· rw [supDegree_zero, Finsupp.bot_eq_zero]
exact Pi.zero_mono
rw [Antitone]
by_contra! h
obtain ⟨i, j, hle, hlt⟩ := h
apply (le_sup (s := p.support) (f := toLex) _).not_gt
pick_goal 3
· rw [← hp (Equiv.swap i j), mem_support_iff, coeff_rename_mapDomain _ (Equiv.injective _)]
rw [Ne, ← leadingCoeff_eq_zero toLex.injective, leadingCoeff_toLex] at h0
assumption
refine ⟨i, fun k hk ↦ ?_, ?_⟩
all_goals dsimp only [Pi.toLex_apply, ofLex_toLex]
· conv_rhs => rw [← Equiv.swap_apply_of_ne_of_ne hk.ne (hk.trans_le hle).ne]
rw [Finsupp.mapDomain_apply (Equiv.injective _), supDegree]; rfl
· apply hlt.trans_eq
simp_rw [Finsupp.mapDomain_equiv_apply, Equiv.symm_swap, Equiv.swap_apply_left]
