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

Equations

• cauchyIndex p q a b = ∑ x ∈ rootsInInterval p a b, jump_val p q x

def variation {R : Type u_1} [Field R] [IsRealClosed R] (a b : R) : ℤ

Equations

• variation a b = if a * b ≥ 0 then 0 else if a < b then 1 else -1

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

Equations

• cross p a b = variation (Polynomial.eval a p) (Polynomial.eval b p)

theorem cross_no_root {R : Type u_1} [Field R] [IsRealClosed R] {a b : R} {p : Polynomial R} (hab : a < b) (hxnroot : rootsInInterval p a b = ∅) : cross p a b = 0

theorem cauchyIndex_poly_mod {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (a b : R) : cauchyIndex p q a b = cauchyIndex p (q % p) a b

theorem cauchyIndex_smult_1 {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (a b c : R) : cauchyIndex p (Polynomial.C c * q) a b = sgn c * cauchyIndex p q a b

theorem variation_mult_pos1 {R : Type u_1} [Field R] [IsRealClosed R] (c x y : R) (hc : c > 0) : variation (c * x) y = variation x y

theorem variation_mult_pos2 {R : Type u_1} [Field R] [IsRealClosed R] (c x y : R) (hc : c > 0) : variation x (c * y) = variation x y

theorem variation_mult_pos {R : Type u_1} [Field R] [IsRealClosed R] (c d x y : R) (hc : c > 0) (hd : d > 0) : variation (c * x) (d * y) = variation x y

theorem variation_cases {R : Type u_1} [Field R] [IsRealClosed R] (x y : R) : (x > 0 ∧ y > 0 → variation x y = 0) ∧ (x > 0 ∧ y < 0 → variation x y = -1) ∧ (x < 0 ∧ y > 0 → variation x y = 1) ∧ (x < 0 ∧ y < 0 → variation x y = 0)

theorem variation_mult_neg_1 {R : Type u_1} [Field R] [IsRealClosed R] (c x y : R) (hc : c < 0) : variation (c * x) y = variation x y + if y = 0 then 0 else sgn x

@[simp]

theorem cindex_poly_z_1 {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (a b : R) (hp : p = 0) : cauchyIndex p q a b = 0

@[simp]

theorem cindex_poly_z_2 {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (a b : R) (hq : q = 0) : cauchyIndex p q a b = 0

theorem cindex_poly_const {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (a b x : R) (hp_const : Polynomial.C x = p) : cauchyIndex p q a b = 0

theorem cindex_poly_mult {R : Type u_1} [Field R] [IsRealClosed R] {p q p' : Polynomial R} {a b : R} (hp' : p' ≠ 0) : cauchyIndex (p' * p) (p' * q) a b = cauchyIndex p q a b

theorem cindex_poly_cross {R : Type u_1} [Field R] [IsRealClosed R] {p : Polynomial R} {a b : R} (hab : a < b) (hpa_nroot : Polynomial.eval a p ≠ 0) (hpb_nroot : Polynomial.eval b p ≠ 0) : cauchyIndex p 1 a b = cross p a b

theorem cindex_poly_inverse_add {R : Type u_1} [Field R] [IsRealClosed R] {p q : Polynomial R} (a b : R) (hpq_coprime : IsCoprime p q) : cauchyIndex p q a b + cauchyIndex q p a b = cauchyIndex (q * p) 1 a b

theorem cindex_poly_inverse_add_cross {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (a b : R) (hab : a < b) (hapq : Polynomial.eval a (p * q) ≠ 0) (hbpq : Polynomial.eval b (p * q) ≠ 0) : cauchyIndex p q a b + cauchyIndex q p a b = variation (Polynomial.eval a (p * q)) (Polynomial.eval b (p * q))

theorem cindex_poly_congr {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (a a' b b' : R) (haa' : a < a') (hb'b : b' < b) (ha'b' : a' < b') (hpx : ∀ (x : R), a < x ∧ x ≤ a' ∨ b' ≤ x ∧ x < b → Polynomial.eval x p ≠ 0) : cauchyIndex p q a b = cauchyIndex p q a' b'