mv_polynomial.total_degree of sum

Stream: Is there code for X?

[Joseph Hua]

I think this is true

lemma mv_polynomial.total_degree_sum
  {A : Type*} {ι : Type*} {σ} [comm_semiring A] (s : finset ι)
  (ps : ι → mv_polynomial σ A) :
  (finset.sum s ps).total_degree  ≤  finset.sup s (mv_polynomial.total_degree ∘ ps) :=
  sorry

but I don't see it in https://leanprover-community.github.io/mathlib_docs/data/mv_polynomial/variables.html

[Joseph Hua]

lemma mv_polynomial.total_degree_monomial
  {A : Type*} [comm_semiring A] [decidable_eq A]
  {σ : Type*} (f : σ →₀ ℕ) (a : A) :
  (mv_polynomial.monomial f a).total_degree
  =
  ite (a = 0) ⊥ (f.sum (λ _ n, n)) :=
dite (a = 0)
(λ h, by rw [mv_polynomial.total_degree, mv_polynomial.support_monomial,
  if_pos h, if_pos h, finset.sup_empty])
(λ h, by rw [mv_polynomial.total_degree, mv_polynomial.support_monomial,
  if_neg h, if_neg h, finset.sup_singleton])

this too whilst I'm at it

[Joseph Hua]

lemma mv_polynomial.total_degree_sum
  {A : Type*} {ι : Type*} {σ} [comm_semiring A] (s : finset ι)
  [decidable_eq ι]
  (ps : ι → mv_polynomial σ A) :
  (finset.sum s ps).total_degree
  ≤
  finset.sup s (mv_polynomial.total_degree ∘ ps) :=
finset.induction_on s (zero_le _)
(λ a s has hind, by rw finset.sum_insert has;
  exact le_trans (mv_polynomial.total_degree_add _ _)
    ( by rw [max_le_iff, finset.sup_insert];
      exact ⟨ le_sup_iff.mpr $ or.inl (le_of_eq rfl) , le_sup_iff.mpr $ or.inr hind ⟩))

Done. Anyone know if this is already in the library? If not I'd PR

[Alex J. Best]

I PR'ed a slightly different lemma called total_degree_monomial at https://github.com/leanprover-community/mathlib/pull/11319/files, based on https://github.com/leanprover-community/flt-regular/blob/master/src/ring_theory/polynomial/homogenization.lean#L200 which I am slowly trying to move into mathlib, so there might be more overlap there

[Alex J. Best]

@Iván Sadofschi Costa has a proof of total_degree_sum in his combinatorial nullstellensatz project https://github.com/isadofschi/combinatorial_nullstellensatz/blob/main/src/degree.lean#L36, so hopefully one of you can get a version into mathlib :grinning:. It looks like we're all wanting lots of stuff for mv_polynomial these days!

[Iván Sadofschi Costa]

@Joseph Hua please feel free to PR mv_polynomial.total_degree_sum. Your proof seems better :tada:

[Joseph Hua]

cool! i will make a PR now :)