Polynomial

Results named in Tau Ceti's TauCeti.Algebra.Polynomial modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremSturm–Tarski on [a, b]#

The contributions of both closed endpoints are added explicitly to the open-interval formula. For a = b this is the contribution of a point.

TauCeti.Sturm.sum_sign_Icc.{u_1} {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
  [IsRealClosed R] {p f : Polynomial R} {cs : List (Polynomial R)}
  (h : TauCeti.Sturm.IsSignedRemainderSeq (p :: cs))
  (hseed : TauCeti.Sturm.IsTarskiSeed p f (cs.head?.getD 0)) {a b : R} (hab : a ≤ b) :
  ((↑(TauCeti.Sturm.signVariationsRight (p :: cs) a) -
          ↑(TauCeti.Sturm.signVariationsLeft (p :: cs) b) +
        if Polynomial.eval a p = 0 then ↑(SignType.sign (Polynomial.eval a f)) else 0) +
      if Polynomial.eval b p = 0 then ↑(SignType.sign (Polynomial.eval b f)) else 0) =
    ∑ r ∈ p.roots.toFinset with a ≤ r ∧ r ≤ b, ↑(SignType.sign (Polynomial.eval r f))

Lean

Formalized in Tau Ceti as TauCeti.Sturm.sum_sign_Icc.

Other forms

Sturm–Tarski. Formalized in Tau Ceti as TauCeti.Sturm.sum_sign.

TauCeti.Sturm.sum_sign.{u_1} {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
  [IsRealClosed R] {p f : Polynomial R} {cs : List (Polynomial R)}
  (h : TauCeti.Sturm.IsSignedRemainderSeq (p :: cs))
  (hseed : TauCeti.Sturm.IsTarskiSeed p f (cs.head?.getD 0)) {a b : R} (hab : a < b)
  (ha : Polynomial.eval a p ≠ 0) (hb : Polynomial.eval b p ≠ 0) :
  ↑(TauCeti.Sturm.signVariationsAt (p :: cs) a) - ↑(TauCeti.Sturm.signVariationsAt (p :: cs) b) =
    ∑ r ∈ p.roots.toFinset with a < r ∧ r < b, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski on (a, b]. Formalized in Tau Ceti as TauCeti.Sturm.sum_sign_Ioc.

TauCeti.Sturm.sum_sign_Ioc.{u_1} {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
  [IsRealClosed R] {p f : Polynomial R} {cs : List (Polynomial R)}
  (h : TauCeti.Sturm.IsSignedRemainderSeq (p :: cs))
  (hseed : TauCeti.Sturm.IsTarskiSeed p f (cs.head?.getD 0)) {a b : R} (hab : a ≤ b) :
  (↑(TauCeti.Sturm.signVariationsRight (p :: cs) a) -
        ↑(TauCeti.Sturm.signVariationsLeft (p :: cs) b) +
      if Polynomial.eval b p = 0 then ↑(SignType.sign (Polynomial.eval b f)) else 0) =
    ∑ r ∈ p.roots.toFinset with a < r ∧ r ≤ b, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski on [a, b). Formalized in Tau Ceti as TauCeti.Sturm.sum_sign_Ico.

TauCeti.Sturm.sum_sign_Ico.{u_1} {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
  [IsRealClosed R] {p f : Polynomial R} {cs : List (Polynomial R)}
  (h : TauCeti.Sturm.IsSignedRemainderSeq (p :: cs))
  (hseed : TauCeti.Sturm.IsTarskiSeed p f (cs.head?.getD 0)) {a b : R} (hab : a ≤ b) :
  (↑(TauCeti.Sturm.signVariationsRight (p :: cs) a) -
        ↑(TauCeti.Sturm.signVariationsLeft (p :: cs) b) +
      if Polynomial.eval a p = 0 then ↑(SignType.sign (Polynomial.eval a f)) else 0) =
    ∑ r ∈ p.roots.toFinset with a ≤ r ∧ r < b, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski on the whole line. Formalized in Tau Ceti as Polynomial.tarskiQuery_eq_signVariationsAtBot_sub_signVariationsAtTop.

Polynomial.tarskiQuery_eq_signVariationsAtBot_sub_signVariationsAtTop.{u_1} {R : Type u_1} [Field R]
  [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p q : Polynomial R) :
  p.tarskiQuery q =
    ↑(TauCeti.Sturm.signVariationsAtBot (p.sturmSeq (Polynomial.derivative p * q))) -
      ↑(TauCeti.Sturm.signVariationsAtTop (p.sturmSeq (Polynomial.derivative p * q)))

Sturm–Tarski with one-sided endpoints. Formalized in Tau Ceti as TauCeti.Sturm.sum_sign_Ioo.

TauCeti.Sturm.sum_sign_Ioo.{u_1} {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
  [IsRealClosed R] {p f : Polynomial R} {cs : List (Polynomial R)}
  (h : TauCeti.Sturm.IsSignedRemainderSeq (p :: cs))
  (hseed : TauCeti.Sturm.IsTarskiSeed p f (cs.head?.getD 0)) {a b : R} (hab : a < b) :
  ↑(TauCeti.Sturm.signVariationsRight (p :: cs) a) -
      ↑(TauCeti.Sturm.signVariationsLeft (p :: cs) b) =
    ∑ r ∈ p.roots.toFinset with a < r ∧ r < b, ↑(SignType.sign (Polynomial.eval r f))

Sources

• Tau Ceti documentation: TauCeti.Sturm.sum_sign_Icc
• Source of TauCeti.Sturm.sum_sign_Icc in TauCeti/Algebra/Polynomial/Sturm/OneSided.lean

LeanTauCeti.Sturm.sum_sign_Icc · TauCeti.Sturm.sum_sign · TauCeti.Sturm.sum_sign_Ioc · TauCeti.Sturm.sum_sign_Ico · Polynomial.tarskiQuery_eq_signVariationsAtBot_sub_signVariationsAtTop · TauCeti.Sturm.sum_sign_Ioo

TheoremTaylor's estimate#

If d ∣ x - t, d ∣ e and e ∣ x' - x, then the derivative at t linearises the polynomial f from x to x' up to an error divisible by d * e.

Polynomial.mul_dvd_eval_sub_eval_sub_mul.{u_1} {R : Type u_1} [CommRing R] (f : Polynomial R)
  {d e t x x' : R} (hx : d ∣ x - t) (hde : d ∣ e) (hxx' : e ∣ x' - x) :
  d * e ∣
    Polynomial.eval x' f - Polynomial.eval x f -
      Polynomial.eval t (Polynomial.derivative f) * (x' - x)

Lean

Formalized in Tau Ceti as Polynomial.mul_dvd_eval_sub_eval_sub_mul.

Sources

• Tau Ceti documentation: Polynomial.mul_dvd_eval_sub_eval_sub_mul
• Source of Polynomial.mul_dvd_eval_sub_eval_sub_mul in TauCeti/Algebra/Polynomial/Identities.lean

LeanPolynomial.mul_dvd_eval_sub_eval_sub_mul

Used by 1

Used byHensel's lemma with a derivative dividing π ^ k

TheoremThom's lemma#

For any signs σ k prescribed for the derivatives of every order of p, including order zero, the set of points where p realizes them is empty, a single point, or an open interval with endpoints a ∈ WithBot R and b ∈ WithTop R.

Polynomial.preimage_derivativeSign_subsingleton_or_eq_Ioo.{u_1} {R : Type u_1} [Field R]
  [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) (σ : ℕ → SignType) :
  (p.derivativeSign ⁻¹' {σ}).Subsingleton ∨ ∃ a b, p.derivativeSign ⁻¹' {σ} = {x | a < ↑x ∧ ↑x < b}

Lean

Formalized in Tau Ceti as Polynomial.preimage_derivativeSign_subsingleton_or_eq_Ioo.

Other forms

Thom's lemma for finite Thom encodings. Formalized in Tau Ceti as Polynomial.preimage_thomEncoding_subsingleton_or_eq_Ioo.

Polynomial.preimage_thomEncoding_subsingleton_or_eq_Ioo.{u_1} {R : Type u_1} [Field R]
  [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R)
  (τ : Fin p.natDegree → SignType) :
  (p.thomEncoding ⁻¹' {τ}).Subsingleton ∨ ∃ a b, p.thomEncoding ⁻¹' {τ} = {x | a < ↑x ∧ ↑x < b}

Sources

• Tau Ceti documentation: Polynomial.preimage_derivativeSign_subsingleton_or_eq_Ioo
• Source of Polynomial.preimage_derivativeSign_subsingleton_or_eq_Ioo in TauCeti/Algebra/Polynomial/Thom/Interval.lean

LeanPolynomial.preimage_derivativeSign_subsingleton_or_eq_Ioo · Polynomial.preimage_thomEncoding_subsingleton_or_eq_Ioo

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.