@[irreducible]

def sturmSeq {R : Type u_1} [Field R] [IsRealClosed R] (f g : Polynomial R) : List (Polynomial R)

Equations

• sturmSeq f g = if f = 0 then [] else f :: sturmSeq g (-f % g)

theorem no_zero_in_sturmSeq {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) : 0 ∉ sturmSeq p q

@[irreducible]

def seqVar {R : Type u_1} [Field R] [IsRealClosed R] : List R → ℕ

Equations

• seqVar [] = 0
• seqVar [head] = 0
• seqVar (a :: b :: as) = if (b == 0) = true then seqVar (a :: as) else if a * b < 0 then 1 + seqVar (b :: as) else seqVar (b :: as)

def seqEval {R : Type u_1} [Field R] (k : R) : List (Polynomial R) → List R

Equations

• seqEval k [] = []
• seqEval k (a :: as) = Polynomial.eval k a :: seqEval k as

def seqEvalSgn {R : Type u_1} [Field R] [IsRealClosed R] (k : R) : List (Polynomial R) → List R

Equations

• seqEvalSgn k [] = []
• seqEvalSgn k (a :: as) = ↑(sgn (Polynomial.eval k a)) :: seqEvalSgn k as

def seqVar_ab {R : Type u_1} [Field R] [IsRealClosed R] (P : List (Polynomial R)) (a b : R) : ℤ

Equations

• seqVar_ab P a b = ↑(seqVar (seqEval a P)) - ↑(seqVar (seqEval b P))

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

Equations

• seqVarSturm_ab p q a b = seqVar_ab (sturmSeq p q) a b

def seqVarAbove_a {R : Type u_1} [Field R] [IsRealClosed R] (P : List (Polynomial R)) (a : R) : ℤ

Equations

• seqVarAbove_a P a = ↑(seqVar (seqEval a P)) - ↑(seqVar (seq_sgn_pos_inf P))

def seqVarBelow_b {R : Type u_1} [Field R] [IsRealClosed R] (P : List (Polynomial R)) (b : R) : ℤ

Equations

• seqVarBelow_b P b = ↑(seqVar (seq_sgn_neg_inf P)) - ↑(seqVar (seqEval b P))

def seqVarR {R : Type u_1} [Field R] [IsRealClosed R] (P : List (Polynomial R)) : ℤ

Equations

• seqVarR P = ↑(seqVar (seq_sgn_neg_inf P)) - ↑(seqVar (seq_sgn_pos_inf P))

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

Equations

• seqVarAboveSturm p q a = seqVarAbove_a (sturmSeq p q) a

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

Equations

• seqVarBelowSturm p q b = seqVarBelow_b (sturmSeq p q) b

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

Equations

• seqVarRSturm p q = seqVarR (sturmSeq p q)

@[irreducible]

theorem seqVarSgn {R : Type u_1} [Field R] [IsRealClosed R] (ps : List (Polynomial R)) (k : R) : seqVar (seqEval k ps) = seqVar (seqEvalSgn k ps)

theorem smod_nil_eq {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) : sturmSeq p q = [] ↔ p = 0

@[simp]

theorem smods_s_0_1 {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) : sturmSeq 0 p = []

@[simp]

theorem smods_s_0_2 {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) : sturmSeq p 0 = if p = 0 then [] else [p]

@[simp]

theorem seqVarSturm_ab_z_1 {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (a b : R) : seqVarSturm_ab 0 p a b = 0

@[simp]

theorem seqVarSturm_ab_z_2 {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (a b : R) : seqVarSturm_ab p 0 a b = 0

theorem cauchyIndex_poly_taq {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (a b : R) : tarskiQuery p q a b = cauchyIndex p (Polynomial.derivative p * q) a b

theorem changes_itv_smods_rec {R : Type u_1} [Field R] [IsRealClosed R] {a b : R} {p q : Polynomial R} (hpqa : Polynomial.eval a (p * q) ≠ 0) (hpqb : Polynomial.eval b (p * q) ≠ 0) : seqVarSturm_ab p q a b = cross (p * q) a b + seqVarSturm_ab q (-p % q) a b

theorem cauchyIndex_sturmSeq_aux {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (a b : R) (hab : a < b) : ∃ (a' : R) (b' : R), a < a' ∧ a' < b' ∧ b' < b ∧ ∀ p' ∈ sturmSeq p q, ∀ (x : R), a < x ∧ x ≤ a' ∨ b' ≤ x ∧ x < b → Polynomial.eval x p' ≠ 0

theorem cauchyIndex_poly_rec {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (a b : R) (hab : a < b) (ha : Polynomial.eval a (p * q) ≠ 0) (hb : Polynomial.eval b (p * q) ≠ 0) : cauchyIndex p q a b = cross (p * q) a b + cauchyIndex q (-p % q) a b

@[irreducible]

theorem changes_smods_congr {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (a a' : R) (haa' : a ≠ a') (hpa : Polynomial.eval a p ≠ 0) (no_root : ∀ p' ∈ sturmSeq p q, ∀ (x : R), a < x ∧ x ≤ a' ∨ a' ≤ x ∧ x < a → Polynomial.eval x p' ≠ 0) : seqVar (seqEval a (sturmSeq p q)) = seqVar (seqEval a' (sturmSeq p q))

theorem changes_itv_smods_congr {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (a a' b b' : R) (hpa : Polynomial.eval a p ≠ 0) (hpb : Polynomial.eval b p ≠ 0) (haa' : a < a') (hb'b : b' < b) (no_root : ∀ p' ∈ sturmSeq p q, ∀ (x : R), a < x ∧ x ≤ a' ∨ b' ≤ x ∧ x < b → Polynomial.eval x p' ≠ 0) : seqVarSturm_ab p q a b = seqVarSturm_ab p q a' b'

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