theorem sturm_tarski_interval {R : Type u_1} [Field R] [IsRealClosed R] (a b : R) (p q : Polynomial R) (hab : a < b) (hpa : Polynomial.eval a p ≠ 0) (hpb : Polynomial.eval b p ≠ 0) : tarskiQuery p q a b = seqVarSturm_ab p (Polynomial.derivative p * q) a b

def rootsAbove {R : Type u_1} [Field R] [IsRealClosed R] (f : Polynomial R) (a : R) : Finset R

Equations

• rootsAbove f a = {x ∈ f.roots.toFinset | x > a}

def tarskiQuery_above {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (a : R) : ℤ

Equations

• tarskiQuery_above p q a = ∑ x ∈ rootsAbove p a, sgn (Polynomial.eval x q)

def rootsBelow {R : Type u_1} [Field R] [IsRealClosed R] (f : Polynomial R) (b : R) : Finset R

Equations

• rootsBelow f b = {x ∈ f.roots.toFinset | x < b}

def tarskiQuery_below {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (b : R) : ℤ

Equations

• tarskiQuery_below p q b = ∑ x ∈ rootsBelow p b, sgn (Polynomial.eval x q)

def tarskiQuery_R {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) : ℤ

Equations

• tarskiQuery_R p q = ∑ x ∈ p.roots.toFinset, sgn (Polynomial.eval x q)

theorem seq_sgn_pos_inf_seqEvalSgn {R : Type u_1} [Field R] [IsRealClosed R] (ub : R) (ps : List (Polynomial R)) (key : ∀ x ≥ ub, ∀ pp ∈ ps, sgn (Polynomial.eval x pp) = sgn_pos_inf pp) : seq_sgn_pos_inf ps = seqEvalSgn ub ps

theorem sturm_tarski_above {R : Type u_1} [Field R] [IsRealClosed R] (a : R) (p q : Polynomial R) (hpa : Polynomial.eval a p ≠ 0) : tarskiQuery_above p q a = seqVarAboveSturm p (Polynomial.derivative p * q) a

theorem seq_sgn_neg_inf_seqEvalSgn {R : Type u_1} [Field R] [IsRealClosed R] (lb : R) (ps : List (Polynomial R)) (key : ∀ x ≤ lb, ∀ pp ∈ ps, sgn (Polynomial.eval x pp) = sgn_neg_inf pp) : seq_sgn_neg_inf ps = seqEvalSgn lb ps

theorem sturm_tarski_below {R : Type u_1} [Field R] [IsRealClosed R] (b : R) (p q : Polynomial R) (hpa : Polynomial.eval b p ≠ 0) : tarskiQuery_below p q b = seqVarBelowSturm p (Polynomial.derivative p * q) b

theorem sturm_tarski_R {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) : tarskiQuery_R p q = seqVarRSturm p (Polynomial.derivative p * q)

theorem sturm_interval {R : Type u_1} [Field R] [IsRealClosed R] (a b : R) (p : Polynomial R) (hab : a < b) (hpa : Polynomial.eval a p ≠ 0) (hpb : Polynomial.eval b p ≠ 0) : ↑(rootsInInterval p a b).card = seqVarSturm_ab p (Polynomial.derivative p) a b

theorem sturm_above {R : Type u_1} [Field R] [IsRealClosed R] (a : R) (p : Polynomial R) (hpa : Polynomial.eval a p ≠ 0) : ↑(rootsAbove p a).card = seqVarAboveSturm p (Polynomial.derivative p) a

theorem sturm_below {R : Type u_1} [Field R] [IsRealClosed R] (b : R) (p : Polynomial R) (hpa : Polynomial.eval b p ≠ 0) : ↑(rootsBelow p b).card = seqVarBelowSturm p (Polynomial.derivative p) b

theorem sturm_R {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) : ↑p.roots.toFinset.card = seqVarRSturm p (Polynomial.derivative p)