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 declarations

• 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. It is 1 for nonzero constants and 0 for zero.

Main results

• initialOf_eq_leadingCoeff: initᵢ(p) is the leading coefficient when viewing p as a univariate polynomial in X i.
• initialOf_mul_X_pow_add_eraseInitOf: p = initᵢ(p) * Xᵢ^degᵢ(p) + remainder, with strictly smaller degree when degᵢ(p) > 0.
• initial_reducedTo: The initial is always reduced w.r.t. the original polynomial
• initialOf_mul_eq: initᵢ(p * q) = initᵢ(p) * initᵢ(q) (for integral domains)

References

• [Wen-Tsun Wu, Basic principles of mechanical theorem proving in elementary geometries] [WT86]

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 erased.

Equations

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

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)) (p.coeff s)

@[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) : (initialOf i p).coeff s = 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) : (initialOf i p).coeff s = p.coeff (s.update i (degreeOf i p))

theorem MvPolynomial.coeff_initialOf_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (p : MvPolynomial σ R) (s : σ →₀ ℕ) : (initialOf i p).coeff s = if s i = 0 then p.coeff (s.update i (degreeOf i 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 : σ →₀ ℕ} : (initialOf i p).coeff s ≠ 0 → (initialOf i p).coeff s = p.coeff (s.update i (degreeOf i 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.vars_initialOf_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (p : MvPolynomial σ R) : (initialOf i p).vars ⊆ p.vars

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

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

eraseInitOf i p for a polynomial p is the sum of all terms in p whose degree in i is not equal to p.degreeOf i.

Equations

• MvPolynomial.eraseInitOf i p = ∑ s ∈ p.support with s i ≠ MvPolynomial.degreeOf i p, (MvPolynomial.monomial s) (p.coeff s)

theorem MvPolynomial.degreeOf_eraseInitOf_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (p : MvPolynomial σ R) : degreeOf i (eraseInitOf i p) ≤ degreeOf i p - 1

theorem MvPolynomial.initialOf_mul_X_pow_add_eraseInitOf {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (p : MvPolynomial σ R) : p = initialOf i p * X i ^ degreeOf i p + eraseInitOf i p

The fundamental decomposition of a polynomial with respect to a variable i. p = initᵢ(p) * Xᵢ ^ degᵢ(p) + eraseInit, with strictly smaller remainder degree when degᵢ(p) > 0.

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} (h : 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

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.max_vars 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.vars.max 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_max_vars_eq_bot {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p : MvPolynomial σ R} (hp : p ≠ 0) : p.vars.max = ⊥ → p.initial = 1

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

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

@[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.max_vars_initial_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p : MvPolynomial σ R} (hp : p.vars.max ≠ ⊥) : p.initial.vars.max < p.vars.max

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

@[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_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_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