English
Let f: S → R[X] and s be a Finset S with pairwise nonzero summands, then the natDegree of the sum equals the supremum of natDegrees of the summands.
Русский
Пусть f: S → R[X] и s — конечное подмножество, такие что f(i) ≠ 0 и степени (natDegree) попарно различны; тогда natDegree суммы равен sup natDegree(f(i)).
LaTeX
$$$\operatorname{natDegree}\Big(\sum_{i\in s} f(i)\Big) = \sup_{i\in s} \operatorname{natDegree}(f(i))$$$
Lean4
theorem natDegree_sum_eq_of_disjoint (f : S → R[X]) (s : Finset S)
(h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)) :
natDegree (s.sum f) = s.sup fun i => natDegree (f i) :=
by
by_cases H : ∃ x ∈ s, f x ≠ 0
· obtain ⟨x, hx, hx'⟩ := H
have hs : s.Nonempty := ⟨x, hx⟩
refine natDegree_eq_of_degree_eq_some ?_
rw [degree_sum_eq_of_disjoint]
· rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, Nat.cast_withBot, Finset.coe_sup' hs, ←
Finset.sup'_eq_sup hs]
refine le_antisymm ?_ ?_
· rw [Finset.sup'_le_iff]
intro b hb
by_cases hb' : f b = 0
· simpa [hb'] using hs
rw [degree_eq_natDegree hb', Nat.cast_withBot]
exact Finset.le_sup' (fun i : S => (natDegree (f i) : WithBot ℕ)) hb
· rw [Finset.sup'_le_iff]
intro b hb
simp only [Finset.le_sup'_iff, Function.comp_apply]
by_cases hb' : f b = 0
· refine ⟨x, hx, ?_⟩
contrapose! hx'
simpa [← Nat.cast_withBot, hb', degree_eq_bot] using hx'
exact ⟨b, hb, (degree_eq_natDegree hb').ge⟩
· exact h.imp fun x y hxy hxy' => hxy (natDegree_eq_of_degree_eq hxy')
· push_neg at H
rw [Finset.sum_eq_zero H, natDegree_zero, eq_comm, show 0 = ⊥ from rfl, Finset.sup_eq_bot_iff]
intro x hx
simp [H x hx]
