instance instLinearOrder_realClosedField_1 {R : Type u_1} [Field R] [IsRealClosed R] : LinearOrder R

Equations

• instLinearOrder_realClosedField_1 = LinearOrder.ofIsSemireal R

instance instTopologicalSpace_realClosedField {R : Type u_1} [Field R] [IsRealClosed R] : TopologicalSpace R

Equations

• instTopologicalSpace_realClosedField = Preorder.topology R

instance instOrderTopology_realClosedField {R : Type u_1} [Field R] [IsRealClosed R] : OrderTopology R

def rightNear {R : Type u_1} [Field R] [IsRealClosed R] (x : R) : Filter R

Equations

• rightNear x = nhdsWithin x (Set.Ioi x)

def eventually_at_right {R : Type u_1} [Field R] [IsRealClosed R] (x : R) (P : R → Prop) : Prop

Equations

• eventually_at_right x P = Filter.Eventually P (rightNear x)

theorem eventually_at_right_equiv {R : Type u_1} [Field R] [IsRealClosed R] {x : R} {P : R → Prop} : eventually_at_right x P ↔ ∃ b > x, ∀ (y : R), x < y ∧ y < b → P y

theorem eventually_at_right_def {R : Type u_1} [Field R] [IsRealClosed R] (x : R) (P : R → Prop) : eventually_at_right x P = Filter.Eventually P (rightNear x)

def sign_r_pos {R : Type u_1} [Field R] [IsRealClosed R] (x : R) (p : Polynomial R) : Prop

Equations

• sign_r_pos x p = eventually_at_right x fun (x : R) => Polynomial.eval x p > 0

theorem eventually_at_right_equiv' {R : Type u_1} [Field R] [IsRealClosed R] {x : R} {p : Polynomial R} : sign_r_pos x p ↔ ∃ b > x, ∀ (y : R), x < y ∧ y < b → 0 < Polynomial.eval y p

theorem eventually_subst {R : Type u_1} [Field R] [IsRealClosed R] (P Q : R → Prop) (F : Filter R) (h : ∀ᶠ (a : R) in F, P a = Q a) : Filter.Eventually P F = Filter.Eventually Q F

theorem sign_r_pos_rec {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (x : R) (hp : p ≠ 0) : sign_r_pos x p = if Polynomial.eval x p = 0 then sign_r_pos x (Polynomial.derivative p) else Polynomial.eval x p > 0

theorem sign_r_pos_minus {R : Type u_1} [Field R] [IsRealClosed R] (x : R) (p : Polynomial R) : p ≠ 0 → (sign_r_pos x p ↔ ¬sign_r_pos x (-p))

theorem sign_r_pos_mult {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (x : R) (hp : p ≠ 0) (hq : q ≠ 0) : sign_r_pos x (p * q) = (sign_r_pos x p ↔ sign_r_pos x q)

theorem sign_r_pos_deriv {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (x : R) (hp : p ≠ 0) (hev : Polynomial.eval x p = 0) : sign_r_pos x (Polynomial.derivative p * p)

theorem sign_r_pos_add {R : Type u_1} [Field R] [IsRealClosed R] {x : R} (p q : Polynomial R) (hp_eval : Polynomial.eval x p = 0) (hq_eval : Polynomial.eval x q ≠ 0) : sign_r_pos x (p + q) = sign_r_pos x q

theorem sign_r_pos_mod {R : Type u_1} [Field R] [IsRealClosed R] {x : R} (p q : Polynomial R) (hp_eval : Polynomial.eval x p = 0) (hq_eval : Polynomial.eval x q ≠ 0) : sign_r_pos x (q % p) = sign_r_pos x q

theorem sign_r_pos_smult {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (x c : R) : c ≠ 0 → p ≠ 0 → sign_r_pos x (Polynomial.C c * p) = if c > 0 then sign_r_pos x p else ¬sign_r_pos x p

theorem sign_r_pos_power {R : Type u_1} [Field R] [IsRealClosed R] (a : R) (n : ℕ) : sign_r_pos a ((Polynomial.X - Polynomial.C a) ^ n)