Initial of a Polynomial

This file defines the initial of a multivariate polynomial.

For a polynomial p with main variable xᵢ, the initial is the coefficient (a polynomial) of the highest power of xᵢ appearing in p.

Main Definitions

• MvPolynomial.initialOf i p: The initial of p with respect to a specific variable i. This is the coefficient of X i ^ degᵢ(p).
• MvPolynomial.initial: The initial of p with respect to its main variable. For constants, this is defined as 1.

Main Theorems

• initialOf_eq_leadingCoeff: initᵢ(p) is the leading coefficient when viewing p as a univariate polynomial in X i.
• initialOf_decomposition: p = initᵢ(p) * Xᵢ^degᵢ(p) + remainder where degᵢ(remainder) < degᵢ(p)
• initial_reducedTo: The initial is always reduced w.r.t. the original polynomial
• initialOf_mul: initᵢ(p * q) = initᵢ(p) * initᵢ(q) (for integral domains)

noncomputable def MvPolynomial.initialOf {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (p : MvPolynomial σ R) : MvPolynomial σ R

The "initial" of a polynomial p with respect to a variable i. It is the coefficient of the highest power of X i appearing in p. More formally, it is the sum of terms in p whose degree in i equals p.degreeOf i, but with the variable i removed (set to 1).

Equations

• MvPolynomial.initialOf i p = ∑ s ∈ p.support with s i = MvPolynomial.degreeOf i p, (MvPolynomial.monomial (Finsupp.erase i s)) (MvPolynomial.coeff s p)

theorem MvPolynomial.initialOf_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {i : σ} : initialOf i p = ∑ s ∈ p.support with s i = degreeOf i p, (monomial (Finsupp.erase i s)) (coeff s p)

@[simp]

theorem MvPolynomial.initialOf_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) : initialOf i 0 = 0

@[simp]

theorem MvPolynomial.initialOf_monomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (s : σ →₀ ℕ) (r : R) : initialOf i ((monomial s) r) = (monomial (Finsupp.erase i s)) r

@[simp]

theorem MvPolynomial.initialOf_C {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (r : R) : initialOf i (C r) = C r

@[simp]

theorem MvPolynomial.initialOf_one {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) : initialOf i 1 = 1

@[simp]

theorem MvPolynomial.initialOf_mul_X_self {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (p : MvPolynomial σ R) : initialOf i (p * X i) = initialOf i p

theorem MvPolynomial.initialOf_mul_X_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) {i j : σ} (h : i ≠ j) : initialOf i (p * X j) = initialOf i p * X j

@[simp]

theorem MvPolynomial.initialOf_mul_X_self_pow {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (p : MvPolynomial σ R) (k : ℕ) : initialOf i (p * X i ^ k) = initialOf i p

theorem MvPolynomial.initialOf_mul_X_pow_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) {i j : σ} (k : ℕ) (h : i ≠ j) : initialOf i (p * X j ^ k) = initialOf i p * X j ^ k

@[simp]

theorem MvPolynomial.initialOf_X_self {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) : initialOf i (X i) = 1

@[simp]

theorem MvPolynomial.initialOf_X_self_pow {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (k : ℕ) : initialOf i (X i ^ k) = 1

theorem MvPolynomial.initialOf_X_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i j : σ} (h : i ≠ j) : initialOf i (X j) = X j

theorem MvPolynomial.initialOf_X_pow_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i j : σ} (k : ℕ) (h : i ≠ j) : initialOf i (X j ^ k) = X j ^ k

theorem MvPolynomial.coeff_initialOf_eq_of_apply_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (p : MvPolynomial σ R) {s : σ →₀ ℕ} (h : s i ≠ 0) : coeff s (initialOf i p) = 0

theorem MvPolynomial.coeff_initialOf_eq_of_apply_eq_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (p : MvPolynomial σ R) {s : σ →₀ ℕ} (h : s i = 0) : coeff s (initialOf i p) = coeff (s.update i (degreeOf i p)) p

theorem MvPolynomial.coeff_initialOf_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (p : MvPolynomial σ R) (s : σ →₀ ℕ) : coeff s (initialOf i p) = if s i = 0 then coeff (s.update i (degreeOf i p)) p else 0

theorem MvPolynomial.coeff_initialOf_eq_of_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i : σ} {p : MvPolynomial σ R} {s : σ →₀ ℕ} : coeff s (initialOf i p) ≠ 0 → coeff s (initialOf i p) = coeff (s.update i (degreeOf i p)) p

@[simp]

theorem MvPolynomial.degreeOf_initialOf_self {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (p : MvPolynomial σ R) : degreeOf i (initialOf i p) = 0

theorem MvPolynomial.initialOf_eq_leadingCoeff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq σ] {p : MvPolynomial σ R} {i : σ} : initialOf i p = (rename Subtype.val) ((optionEquivLeft R { b : σ // b ≠ i }) ((rename ⇑(Equiv.optionSubtypeNe i).symm) p)).leadingCoeff

The initial of p with respect to i is the leading coefficient when viewing p as a univariate polynomial in X i.

theorem MvPolynomial.initialOf_eq_of_degreeOf_eq_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {i : σ} : degreeOf i p = 0 → initialOf i p = p

theorem MvPolynomial.degreeOf_initialOf_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i j : σ) (p : MvPolynomial σ R) : degreeOf j (initialOf i p) ≤ degreeOf j p

theorem MvPolynomial.initialOf_add_eq_of_degreeOf_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i : σ} {p q : MvPolynomial σ R} (h : degreeOf i q < degreeOf i p) : initialOf i (p + q) = initialOf i p

theorem MvPolynomial.degreeOf_eq_of_initialOf_decomposition {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i : σ} {p q r : MvPolynomial σ R} {d : ℕ} (q_ne : q ≠ 0) (hq : degreeOf i q = 0) (hr : degreeOf i r < d) (decomp : p = q * X i ^ d + r) : degreeOf i p = d

@[simp]

theorem MvPolynomial.initialOf_initialOf_self {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (p : MvPolynomial σ R) : initialOf i (initialOf i p) = initialOf i p

theorem MvPolynomial.initialOf_eq_iff_degreeOf_eq_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i : σ} {p : MvPolynomial σ R} : degreeOf i p = 0 ↔ initialOf i p = p

theorem MvPolynomial.initialOf_decomposition {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (p : MvPolynomial σ R) : ∃ (q : MvPolynomial σ R), degreeOf i q ≤ degreeOf i p - 1 ∧ p = initialOf i p * X i ^ degreeOf i p + q

The fundamental decomposition of a polynomial with respect to a variable i. p = initᵢ(p) * Xᵢ ^ degᵢ(p) + tail, where degᵢ(tail) < degᵢ(p).

theorem MvPolynomial.initialOf_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) {p : MvPolynomial σ R} : p ≠ 0 → initialOf i p ≠ 0

theorem MvPolynomial.initialOf_ne_zero_of_degreeOf_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i : σ} {p : MvPolynomial σ R} : degreeOf i p ≠ 0 → initialOf i p ≠ 0

theorem MvPolynomial.degreeOf_add_lt_of_initialOf_cancel {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i : σ} {p q : MvPolynomial σ R} (hd : degreeOf i p = degreeOf i q) (hi : initialOf i p + initialOf i q = 0) : degreeOf i (p + q) ≤ degreeOf i p - 1

theorem MvPolynomial.initialOf_cancel_of_degreeOf_add_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i : σ} {p q : MvPolynomial σ R} (h : degreeOf i (p + q) < degreeOf i p) : initialOf i p + initialOf i q = 0

theorem MvPolynomial.initialOf_eq_of_initialOf_decomposition {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i : σ} {p q r : MvPolynomial σ R} {d : ℕ} (q_ne : q ≠ 0) (hq : degreeOf i q = 0) (hr : degreeOf i r < d) (decomp : p = q * X i ^ d + r) : initialOf i p = q

theorem MvPolynomial.initialOf_add_of_degreeOf_eq_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) {p q : MvPolynomial σ R} (hi : initialOf i p + initialOf i q ≠ 0) (h : degreeOf i q = degreeOf i p) : initialOf i (p + q) = initialOf i p + initialOf i q

theorem MvPolynomial.initialOf_mul_decomposition {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (p q : MvPolynomial σ R) : ∃ (r : MvPolynomial σ R), degreeOf i r ≤ degreeOf i p + degreeOf i q - 1 ∧ p * q = initialOf i p * initialOf i q * X i ^ (degreeOf i p + degreeOf i q) + r

noncomputable def MvPolynomial.initial {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (p : MvPolynomial σ R) : MvPolynomial σ R

The "Initial" of a polynomial p is p.initialOf p.mainVariable if p is not a constant, and 1 if p is a non-zero constant.

Equations

• p.initial = if p = 0 then 0 else match p.mainVariable with | none => 1 | some c => MvPolynomial.initialOf c p

@[simp]

theorem MvPolynomial.initial_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] : initial 0 = 0

theorem MvPolynomial.initial_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] [Nontrivial R] {p : MvPolynomial σ R} : p ≠ 0 → p.initial ≠ 0

theorem MvPolynomial.initial_of_mainVariable_eq_bot {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p : MvPolynomial σ R} (hp : p ≠ 0) : p.mainVariable = ⊥ → p.initial = 1

theorem MvPolynomial.initial_of_mainVariable_isSome' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p : MvPolynomial σ R} {c : σ} : p.mainVariable = ↑c → p.initial = initialOf c p

theorem MvPolynomial.initial_of_mainVariable_isSome {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p : MvPolynomial σ R} {c : σ} : p.mainVariable = ↑c → p.initial = ∑ s ∈ p.support with s c = degreeOf c p, (monomial (Finsupp.erase c s)) (coeff s p)

@[simp]

theorem MvPolynomial.initial_C {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {r : R} (hr : r ≠ 0) : (C r).initial = 1

theorem MvPolynomial.initial_monomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {s : σ →₀ ℕ} (r : R) {c : σ} : s.support.max = ↑c → ((monomial s) r).initial = (monomial (Finsupp.erase c s)) r

@[simp]

theorem MvPolynomial.initial_X_pow {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (i : σ) {k : ℕ} (hk : k ≠ 0) : (X i ^ k).initial = 1

@[simp]

theorem MvPolynomial.initial_X {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (i : σ) : (X i).initial = 1

theorem MvPolynomial.mainVariable_initial_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p : MvPolynomial σ R} (hp : p.mainVariable ≠ ⊥) : p.initial.mainVariable < p.mainVariable

theorem MvPolynomial.degreeOf_initial_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (p : MvPolynomial σ R) (i : σ) : degreeOf i p.initial ≤ degreeOf i p

noncomputable def MvPolynomial.initialProd {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (PS : Finset (MvPolynomial σ R)) : MvPolynomial σ R

The product of initials of a set of polynomials.

Equations

• MvPolynomial.initialProd PS = ∏ p ∈ PS, p.initial

theorem MvPolynomial.initialProd_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (PS : Finset (MvPolynomial σ R)) : initialProd PS = ∏ p ∈ PS, p.initial

theorem MvPolynomial.initial_reducedTo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} : q.reducedTo p → q.initial.reducedTo p

theorem MvPolynomial.initial_reducedTo_self {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p : MvPolynomial σ R} (hp : p.mainVariable ≠ ⊥) : p.initial.reducedTo p

theorem MvPolynomial.initial_reducedToSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {α : Type u_3} [Membership (MvPolynomial σ R) α] {p : MvPolynomial σ R} {a : α} : p.reducedToSet a → p.initial.reducedToSet a

@[simp]

theorem MvPolynomial.initialOf_C_mul {R : Type u_1} {σ : Type u_2} [CommSemiring R] [NoZeroDivisors R] (i : σ) (p : MvPolynomial σ R) {r : R} : initialOf i (C r * p) = C r * initialOf i p

@[simp]

theorem MvPolynomial.initialOf_mul_C {R : Type u_1} {σ : Type u_2} [CommSemiring R] [NoZeroDivisors R] (i : σ) (p : MvPolynomial σ R) {r : R} : initialOf i (p * C r) = initialOf i p * C r

@[simp]

theorem MvPolynomial.initialOf_smul {R : Type u_1} {σ : Type u_2} [CommSemiring R] [NoZeroDivisors R] (i : σ) (p : MvPolynomial σ R) {r : R} : initialOf i (r • p) = r • initialOf i p

@[simp]

theorem MvPolynomial.initialOf_mul_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [NoZeroDivisors R] (i : σ) (p q : MvPolynomial σ R) : initialOf i (p * q) = initialOf i p * initialOf i q

@[simp]

theorem MvPolynomial.initialOf_pow_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [NoZeroDivisors R] (i : σ) (p : MvPolynomial σ R) (n : ℕ) : initialOf i (p ^ n) = initialOf i p ^ n

@[simp]

theorem MvPolynomial.initialOf_neg {R : Type u_3} {σ : Type u_4} [CommRing R] {p : MvPolynomial σ R} (i : σ) : initialOf i (-p) = -initialOf i p

theorem MvPolynomial.degreeOf_sub_lt_of_initialOf_eq {R : Type u_3} {σ : Type u_4} [CommRing R] {p q : MvPolynomial σ R} {i : σ} (hi : initialOf i p = initialOf i q) (hd : degreeOf i p = degreeOf i q) : degreeOf i (p - q) ≤ degreeOf i p - 1

theorem MvPolynomial.initialOf_eq_of_degreeOf_sub_lt {R : Type u_3} {σ : Type u_4} [CommRing R] {i : σ} {p q : MvPolynomial σ R} (h : degreeOf i (p - q) < degreeOf i p) : initialOf i p = initialOf i q