PolynomialDegree.lean

import Mathlib
open scoped Pointwise
open Polynomial

#check Finset.sup_le
example [inst : SemilatticeSup α] [inst_1 : OrderBot α] [DecidableEq β] {s : Finset β} {f : β → α} {a : α} :
  (∀ b ∈ s, f b ≤ a) → s.sup f ≤ a
:= by
  induction s using Finset.induction_on with
  | empty => simp
  | @insert i s' F IH =>
    intro H; simp at H
    rcases H with ⟨H1, H2⟩
    rw [Finset.sup_insert]
    apply sup_le; assumption
    apply IH H2


#check Finset.le_sup
example [SemilatticeSup α] [OrderBot α] {s : Finset β} [DecidableEq β] {f : β → α}
  {b : β} (hb : b ∈ s) : f b ≤ s.sup f
:= by
  induction s using Finset.induction_on with
  | empty => contradiction
  | @insert i s' F IH =>
    simp at *
    rcases hb with hb | hb
    · subst i
      apply le_sup_left
    · apply le_trans; swap; apply le_sup_right
      apply IH hb


#check Finset.sup_mono
example [SemilatticeSup α] [OrderBot α] {s₁ s₂ : Finset β} {f : β → α}
  (h : s₁ ⊆ s₂) : s₁.sup f ≤ s₂.sup f
:= by
  apply Finset.sup_le
  intro b Hb
  apply Finset.le_sup
  apply h Hb

#check Finsupp.support_add
example [AddZeroClass M] [DecidableEq α] {g₁ g₂ : α →₀ M} :
  (g₁ + g₂).support ⊆ g₁.support ∪ g₂.support
:= by
  intro x Hx; simp at *
  by_contra F; simp at F
  rcases F with ⟨F1, F2⟩
  apply Hx; rw [F1, F2]
  simp

#check Finset.sup_union
example [SemilatticeSup α] [OrderBot α] {s₁ s₂ : Finset β} {f : β → α}
  [DecidableEq β] : (s₁ ∪ s₂).sup f = s₁.sup f ⊔ s₂.sup f
:= by
  apply le_antisymm
  · apply Finset.sup_le
    intro x Hx; simp at Hx
    rcases Hx with Hx | Hx
    · apply le_trans; swap; apply le_sup_left
      apply Finset.le_sup Hx
    · apply le_trans; swap; apply le_sup_right
      apply Finset.le_sup Hx
  · apply sup_le<;> apply Finset.sup_mono<;> simp



#check MvPolynomial.totalDegree_add
example {R σ : Type} [CommSemiring R] (a b : MvPolynomial σ R) :
  (a + b).totalDegree ≤ max a.totalDegree b.totalDegree
:= by classical
  unfold MvPolynomial.totalDegree
  apply LE.le.trans_eq
  · apply Finset.sup_mono
    apply Finsupp.support_add
  · rw [Finset.sup_union]; rfl



----------------------------------

#check Finsupp.support_mul
example [inst : MulZeroClass β] [inst_1 : DecidableEq α] {g₁ g₂ : α →₀ β} :
  (g₁ * g₂).support ⊆ g₁.support ∩ g₂.support
:= by
  intro x Hx; simp at *
  by_contra F; rw [not_and_or] at F; simp at F
  apply Hx
  rcases F with F | F<;> rw [F]<;> simp


#check Finset.sup_add_le
example [DecidableEq α] [Add α] {β : Type u_5} [SemilatticeSup β]
  [inst_3 : OrderBot β] {S T : Finset α} {f : α → β} {a : β} :
  (S + T).sup f ≤ a ↔ ∀ x ∈ S, ∀ y ∈ T, f (x + y) ≤ a
:= by
  constructor<;> intro H
  · intro s Hs t Ht
    apply le_trans; swap; apply H
    apply Finset.le_sup
    apply Finset.add_mem_add Hs Ht
  · apply Finset.sup_le
    intro x Hx
    rw [Finset.mem_add] at Hx
    rcases Hx with ⟨s, Hs, t, Ht, H⟩
    subst x
    apply H s Hs t Ht

#check Finset.sum_add_distrib
example  {α : Type u_3} {β : Type u_4} {S : Finset α} {f g : α → β} [DecidableEq α][AddCommMonoid β] :
  ∑ x ∈ S, (f x + g x) = ∑ x ∈ S, f x + ∑ x ∈ S, g x
:= by
  induction S using Finset.induction_on with
  | empty => simp
  | @insert s S' FS IH =>
    rw [Finset.sum_insert FS, Finset.sum_insert FS, Finset.sum_insert FS]
    rw [IH, add_assoc, <- add_assoc (g s), add_comm (g s), <- add_assoc (f s)]
    rw [<- add_assoc (f s), add_assoc]

#check Finsupp.sum_of_support_subset
example [DecidableEq α] [Zero M] [AddCommMonoid N] (f : α →₀ M) {s : Finset α} (hs : f.support ⊆ s) (g : α → M → N) (h : ∀ i ∈ s, g i 0 = 0) :
  f.sum g = ∑ x ∈ s, g x (f x)
:= by
  simp [Finsupp.sum]
  have : s = f.support ∪ (s  \ f.support) := by aesop

  rw [this, Finset.sum_union]
  suffices : ∑ x ∈ s \ f.support, g x (f x) = 0; rw [this]; simp
  apply Finset.sum_eq_zero
  intro x Hx; simp at Hx
  rw [Hx.2, h x Hx.1]
  intro S HS HS' x Hx; simp
  have := (HS' Hx); simp at this
  rcases this with ⟨H1, H2⟩
  have := HS Hx; simp at this
  contradiction


#check Finsupp.sum_add_index'
example [AddZeroClass M] [AddCommMonoid N] [DecidableEq α]
  {f g : α →₀ M} {h : α → M → N} (h_zero : ∀ (a : α), h a 0 = 0)
  (h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) :
  (f + g).sum h = f.sum h + g.sum h
:= by
  rw [Finsupp.sum_of_support_subset (f + g) Finsupp.support_add h (by aesop)]
  rw [Finsupp.sum_of_support_subset f (Finset.subset_union_left (s₂ := g.support)) h (by aesop)]
  rw [Finsupp.sum_of_support_subset g (Finset.subset_union_right (s₁ := f.support)) h (by aesop)]
  rw [<- Finset.sum_add_distrib]
  apply Finset.sum_congr; rfl
  intro x Hx; simp
  rw [h_add x (f x) (g x)]



#check MvPolynomial.totalDegree_mul
example {R σ : Type} [CommSemiring R] (a b : MvPolynomial σ R) :
  (a * b).totalDegree ≤ a.totalDegree + b.totalDegree
:= by classical
  unfold MvPolynomial.totalDegree
  trans
  · apply Finset.sup_mono
    apply AddMonoidAlgebra.support_mul
  · apply Finset.sup_add_le.mpr
    intro x Hx y Hy; simp at *
    apply Nat.le_trans (m := (x.sum fun x e => e) + (y.sum fun x e => e))
    · rw [Finsupp.sum_add_index']<;> aesop
    · apply Nat.add_le_add
      · conv => arg 1; change (fun s => s.sum fun x e => e ) x
        apply Finset.le_sup (s := a.support) (f := (fun s => s.sum fun x e => e )) (b := x)
        aesop
      · conv => arg 1; change (fun s => s.sum fun x e => e ) y
        apply Finset.le_sup (s := b.support) (f := (fun s => s.sum fun x e => e )) (b := y)
        aesop