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

Equations

• jump_val p q x = if p ≠ 0 ∧ q ≠ 0 ∧ Odd (Polynomial.rootMultiplicity x p - Polynomial.rootMultiplicity x q) then if sign_r_pos x (p * q) then 1 else -1 else 0

theorem jump_poly_mult {R : Type u_1} [Field R] [IsRealClosed R] {p q p' : Polynomial R} {x : R} (hp' : p' ≠ 0) : jump_val (p' * p) (p' * q) x = jump_val p q x

theorem jump_poly_mod {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (x : R) : jump_val p q x = jump_val p (q % p) x

theorem jump_poly_smult_1 {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (c x : R) : jump_val p (Polynomial.C c * q) x = sgn c * jump_val p q x

@[simp]

theorem jump_poly_not_root {R : Type u_1} [Field R] [IsRealClosed R] {p q : Polynomial R} {x : R} (hp : Polynomial.eval x p ≠ 0) : jump_val p q x = 0

@[simp]

theorem jump_poly_z1 {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (x : R) : jump_val p 0 x = 0

@[simp]

theorem jump_poly_z2 {R : Type u_1} [Field R] [IsRealClosed R] (q : Polynomial R) (x : R) : jump_val 0 q x = 0

theorem jump_poly_coprime {R : Type u_1} [Field R] [IsRealClosed R] {p q : Polynomial R} {x : R} (hp : Polynomial.eval x p = 0) (hpq_coprime : IsCoprime p q) : jump_val p q x = jump_val (q * p) 1 x

theorem jump_poly_1_mult {R : Type u_1} [Field R] [IsRealClosed R] {p q : Polynomial R} {x : R} (hnroot : Polynomial.eval x p ≠ 0 ∨ Polynomial.eval x q ≠ 0) : jump_val (p * q) 1 x = sgn (Polynomial.eval x q) * jump_val p 1 x + sgn (Polynomial.eval x p) * jump_val q 1 x

theorem jump_poly_sign {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (x : R) : p ≠ 0 → Polynomial.eval x p = 0 → jump_val p (Polynomial.derivative p * q) x = sgn (Polynomial.eval x q)