Documentation

HexRealRootsTheory.TarskiSum

source
def HexRealRootsTheory.Tarski.InInterval {R : Type u_1} [LinearOrder R] (a b : Hex.Endpoint R) (x : R) :
Prop

Membership in an open interval with possibly infinite endpoints.

Equations
Instances For
    source
    theorem HexRealRootsTheory.Tarski.inInterval_iff {R : Type u_1} [LinearOrder R] (a b : Hex.Endpoint R) (x : R) :
    InInterval a b x ↔ (match a with | Hex.Endpoint.negInf => True | Hex.Endpoint.finite a => a < x | Hex.Endpoint.posInf => False) ∧ match b with | Hex.Endpoint.posInf => True | Hex.Endpoint.finite b => x < b | Hex.Endpoint.negInf => False

    Membership in an open interval reduces to its two endpoint inequalities.

    source
    noncomputable def HexRealRootsTheory.Tarski.rootsIn {R : Type u_1} [Field R] [LinearOrder R] (p : Polynomial R) (a b : Hex.Endpoint R) :
    Finset R

    The distinct roots in the open interval. This is a semantic finite set, not an executable root enumeration.

    Equations
    Instances For
      source
      @[simp]
      theorem HexRealRootsTheory.Tarski.inInterval_finite {R : Type u_1} [LinearOrder R] (a b x : R) :
      InInterval (Hex.Endpoint.finite a) (Hex.Endpoint.finite b) x ↔ a < x ∧ x < b
      source
      @[simp]
      theorem HexRealRootsTheory.Tarski.inInterval_univ {R : Type u_1} [LinearOrder R] (x : R) :
      InInterval Hex.Endpoint.negInf Hex.Endpoint.posInf x

      Every point lies between the two infinite endpoints.

      source
      @[simp]
      theorem HexRealRootsTheory.Tarski.mem_rootsIn {R : Type u_1} [Field R] [LinearOrder R] (p : Polynomial R) (a b : Hex.Endpoint R) (x : R) :
      x ∈ rootsIn p a b ↔ x ∈ p.roots ∧ InInterval a b x
      source
      theorem HexRealRootsTheory.Tarski.mem_rootsIn_iff {R : Type u_1} [Field R] [LinearOrder R] (p : Polynomial R) (hp : p ≠ 0) (a b : Hex.Endpoint R) (x : R) :
      x ∈ rootsIn p a b ↔ Polynomial.eval x p = 0 ∧ InInterval a b x

      Nonzero heads have exactly their evaluation-zero points as roots.

      source
      theorem HexRealRootsTheory.Tarski.rootsIn_C_mul {R : Type u_1} [Field R] [LinearOrder R] (p : Polynomial R) (c : R) (hc : c ≠ 0) (a b : Hex.Endpoint R) :
      rootsIn (Polynomial.C c * p) a b = rootsIn p a b

      Multiplying the head by a nonzero scalar preserves the interval root set.

      source
      noncomputable def HexRealRootsTheory.Tarski.rootSum {R : Type u_1} [Field R] [LinearOrder R] (p f : Polynomial R) (a b : Hex.Endpoint R) :
      ℤ

      The mathematical Sturm–Tarski sum. Its general executable-query identity requires the separately owned signed-remainder theorem.

      Equations
      Instances For
        source
        theorem HexRealRootsTheory.Tarski.rootSum_eq_sum {R : Type u_1} [Field R] [LinearOrder R] (p f : Polynomial R) (a b : Hex.Endpoint R) :
        rootSum p f a b = ∑ x ∈ rootsIn p a b, ↑(SignType.sign (Polynomial.eval x f))

        Expand a query into its finite sum of signs over distinct roots.

        source
        @[simp]
        theorem HexRealRootsTheory.Tarski.rootSum_zero {R : Type u_1} [Field R] [LinearOrder R] (p : Polynomial R) (a b : Hex.Endpoint R) :
        rootSum p 0 a b = 0
        source
        @[simp]
        theorem HexRealRootsTheory.Tarski.rootSum_one {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (a b : Hex.Endpoint R) :
        rootSum p 1 a b = ↑(rootsIn p a b).card
        source
        theorem HexRealRootsTheory.Tarski.rootSum_singleton {R : Type u_1} [Field R] [LinearOrder R] (p f : Polynomial R) (a b : Hex.Endpoint R) (x : R) (h : rootsIn p a b = {x}) :
        rootSum p f a b = ↑(SignType.sign (Polynomial.eval x f))
        source
        theorem HexRealRootsTheory.Tarski.contribution_zero {R : Type u_1} [Field R] [LinearOrder R] (f : Polynomial R) (x : R) (h : f.IsRoot x) :
        ↑(SignType.sign (Polynomial.eval x f)) = 0

        A common root contributes zero to the signed sum.

        source
        theorem HexRealRootsTheory.Tarski.rootSum_filter {R : Type u_1} [Field R] [LinearOrder R] (p f : Polynomial R) (a b : Hex.Endpoint R) :
        rootSum p f a b = ∑ x ∈ rootsIn p a b with Polynomial.eval x f ≠ 0, ↑(SignType.sign (Polynomial.eval x f))

        Restricting to nonzero query evaluations removes only zero contributions.

        source
        theorem HexRealRootsTheory.Tarski.rootSum_eq_zero {R : Type u_1} [Field R] [LinearOrder R] (p f : Polynomial R) (a b : Hex.Endpoint R) (h : ∀ x ∈ rootsIn p a b, Polynomial.eval x f = 0) :
        rootSum p f a b = 0
        source
        theorem HexRealRootsTheory.Tarski.rootSum_of_dvd {R : Type u_1} [Field R] [LinearOrder R] (p f : Polynomial R) (a b : Hex.Endpoint R) (h : p ∣ f) :
        rootSum p f a b = 0

        Divisibility includes zero initial query remainder without a coprimality assumption.

        source
        theorem HexRealRootsTheory.Tarski.rootsIn_card_le {R : Type u_1} [Field R] [LinearOrder R] (p : Polynomial R) (a b : Hex.Endpoint R) :
        (rootsIn p a b).card ≤ p.natDegree
        source
        theorem HexRealRootsTheory.Tarski.abs_rootSum_le {R : Type u_1} [Field R] [LinearOrder R] (p f : Polynomial R) (a b : Hex.Endpoint R) :
        |rootSum p f a b| ≤ ↑(rootsIn p a b).card
        source
        theorem HexRealRootsTheory.Tarski.abs_rootSum_le_degree {R : Type u_1} [Field R] [LinearOrder R] (p f : Polynomial R) (a b : Hex.Endpoint R) :
        |rootSum p f a b| ≤ ↑p.natDegree
        source
        @[simp]
        theorem HexRealRootsTheory.Tarski.rootsIn_const {R : Type u_1} [Field R] [LinearOrder R] (c : R) (a b : Hex.Endpoint R) :
        rootsIn (Polynomial.C c) a b = ∅
        source
        @[simp]
        theorem HexRealRootsTheory.Tarski.rootSum_const {R : Type u_1} [Field R] [LinearOrder R] (c : R) (f : Polynomial R) (a b : Hex.Endpoint R) :
        rootSum (Polynomial.C c) f a b = 0