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

Equations

• instLinearOrder_realClosedField = LinearOrder.ofIsSemireal R

theorem or_neg_of_mul_neg {R : Type u_1} [Field R] [IsRealClosed R] (a b : R) : a * b < 0 → a < 0 ∨ b < 0

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

Equations

• rootsInInterval f a b = {x ∈ f.roots.toFinset | x ∈ Set.Ioo a b}

def sgn {R : Type u_1} [Field R] [IsRealClosed R] (k : R) : ℤ

Equations

• sgn k = if k > 0 then 1 else if k = 0 then 0 else -1

theorem sgn_sgn_neg {R : Type u_1} [Field R] [IsRealClosed R] (x : R) : sgn x < 0 ↔ x < 0

theorem sgn_sgn_zero {R : Type u_1} [Field R] [IsRealClosed R] (x : R) : sgn x = 0 ↔ x = 0

theorem sgn_sgn_pos {R : Type u_1} [Field R] [IsRealClosed R] (x : R) : sgn x > 0 ↔ x > 0

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

Equations

• sgn_pos_inf p = sgn p.leadingCoeff

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

Equations

• sgn_neg_inf p = if Even p.natDegree then sgn p.leadingCoeff else -sgn p.leadingCoeff

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

Equations

• seq_sgn_pos_inf [] = []
• seq_sgn_pos_inf (p :: ps) = ↑(sgn_pos_inf p) :: seq_sgn_pos_inf ps

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

Equations

• seq_sgn_neg_inf [] = []
• seq_sgn_neg_inf (p :: ps) = ↑(sgn_neg_inf p) :: seq_sgn_neg_inf ps

def tarskiQuery {R : Type u_1} [Field R] [IsRealClosed R] (f g : Polynomial R) (a b : R) : ℤ

Equations

• tarskiQuery f g a b = ∑ x ∈ rootsInInterval f a b, sgn (Polynomial.eval x g)

theorem rootsInIntervalZero {R : Type u_1} [Field R] [IsRealClosed R] (a b : R) : rootsInInterval 0 a b = ∅

def rootsInSet {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (S : Set R) : Finset R

Equations

• rootsInSet p S = {x ∈ p.roots.toFinset | x ∈ S}

theorem rootsInSet_interval {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (a b : R) : rootsInInterval p a b = rootsInSet p (Set.Ioo a b)

theorem rootsInSet_cup {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (S T : Set R) : rootsInSet p S ∪ rootsInSet p T = rootsInSet p (S ∪ T)

theorem sgn_inf_comp {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) : sgn_neg_inf p = sgn_pos_inf (p.comp (-Polynomial.X))

theorem next_non_root_interval {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (lb : R) (hp : p ≠ 0) : ∃ (ub : R), lb < ub ∧ ∀ z ∈ Set.Ioc lb ub, Polynomial.eval z p ≠ 0

theorem last_non_root_interval {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (ub : R) (hp : p ≠ 0) : ∃ lb < ub, ∀ z ∈ Set.Ico lb ub, Polynomial.eval z p ≠ 0

theorem intermediate_value_property' {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (a b : R) : a ≤ b → Polynomial.eval a p ≤ 0 → 0 ≤ Polynomial.eval b p → ∃ r ≥ a, r ≤ b ∧ Polynomial.eval r p = 0

theorem intermediate_value_property'_ioo {R : Type u_1} [Field R] [IsRealClosed R] {p : Polynomial R} {a b : R} (hab : a ≤ b) (hap : Polynomial.eval a p < 0) (hbp : Polynomial.eval b p > 0) : ∃ r > a, r < b ∧ Polynomial.eval r p = 0

theorem intermediate_value_property_ioo {R : Type u_1} [Field R] [IsRealClosed R] {p : Polynomial R} {a b : R} (hab : a ≤ b) (hap : Polynomial.eval a p > 0) (hbp : Polynomial.eval b p < 0) : ∃ r > a, r < b ∧ Polynomial.eval r p = 0

theorem exists_root_ioo_mul {R : Type u_1} [Field R] [IsRealClosed R] {p : Polynomial R} {a b : R} (hab : a ≤ b) (hap : Polynomial.eval a p * Polynomial.eval b p < 0) : ∃ r > a, r < b ∧ Polynomial.eval r p = 0

theorem not_eq_pos_or_neg_iff_1 {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (lb ub : R) : (∀ z ∈ Set.Ioc lb ub, Polynomial.eval z p ≠ 0) ↔ (∀ z ∈ Set.Ioc lb ub, Polynomial.eval z p < 0) ∨ ∀ z ∈ Set.Ioc lb ub, 0 < Polynomial.eval z p

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

theorem hc {R : Type u_1} [Field R] [IsRealClosed R] {a b t : R} {P : Polynomial R} : a ≤ b → t ∈ Set.Ioo (Polynomial.eval a P) (Polynomial.eval b P) → ∃ s ∈ Set.Ioo a b, Polynomial.eval s P = t

theorem polynomial_has_root_of_le_zero_of_pos {R : Type u_1} [Field R] [IsRealClosed R] {a b : R} (hab : a ≤ b) {P : Polynomial R} (ha : Polynomial.eval a P < 0) (hb : 0 < Polynomial.eval b P) : ∃ s ∈ Set.Ioo a b, Polynomial.eval s P = 0

theorem polynomial_has_root_of_pos_le_zero {R : Type u_1} [Field R] [IsRealClosed R] {a b : R} (hab : a ≤ b) {P : Polynomial R} (ha : 0 < Polynomial.eval a P) (hb : Polynomial.eval b P < 0) : ∃ s ∈ Set.Ioo a b, Polynomial.eval s P = 0

theorem polynomial_has_root_of_mul_neg {R : Type u_1} [Field R] [IsRealClosed R] {a b : R} (hab : a ≤ b) {P : Polynomial R} (habm : Polynomial.eval a P * Polynomial.eval b P < 0) : ∃ s ∈ Set.Ioo a b, Polynomial.eval s P = 0

theorem neg_of_ne_zero_of_exists_neg {R : Type u_1} [Field R] [IsRealClosed R] {a b m : R} {P : Polynomial R} (hP : ∀ x ∈ Set.Ioo a b, Polynomial.eval x P ≠ 0) (hm : m ∈ Set.Ioo a b) (hneg : Polynomial.eval m P < 0) (x : R) : x ∈ Set.Ioo a b → Polynomial.eval x P < 0

theorem pos_of_ne_zero_of_exists_pos {R : Type u_1} [Field R] [IsRealClosed R] {a b m : R} {P : Polynomial R} (hP : ∀ x ∈ Set.Ioo a b, Polynomial.eval x P ≠ 0) (hm : m ∈ Set.Ioo a b) (hpos : Polynomial.eval m P > 0) (x : R) : x ∈ Set.Ioo a b → Polynomial.eval x P > 0

theorem constant_sign_of_ne_zero {R : Type u_1} [Field R] [IsRealClosed R] {a b : R} (hab : a ≤ b) {P : Polynomial R} (hP : ∀ x ∈ Set.Ioo a b, Polynomial.eval x P ≠ 0) : (∀ x ∈ Set.Ioo a b, Polynomial.eval x P > 0) ∨ ∀ x ∈ Set.Ioo a b, Polynomial.eval x P < 0

theorem nonpos_of_ne_zero_of_exists_neg {R : Type u_1} [Field R] [IsRealClosed R] {a b m : R} {P : Polynomial R} (hP : ∀ x ∈ Set.Ioo a b, Polynomial.eval x P ≠ 0) (hm : m ∈ Set.Ioo a b) (hneg : Polynomial.eval m P < 0) (x : R) : x ∈ Set.Icc a b → Polynomial.eval x P ≤ 0

theorem nonneg_of_ne_zero_of_exists_pos {R : Type u_1} [Field R] [IsRealClosed R] {a b m : R} {P : Polynomial R} (hP : ∀ x ∈ Set.Ioo a b, Polynomial.eval x P ≠ 0) (hm : m ∈ Set.Ioo a b) (hpos : Polynomial.eval m P > 0) (x : R) : x ∈ Set.Icc a b → Polynomial.eval x P ≥ 0

theorem constant_sign_of_ne_zero' {R : Type u_1} [Field R] [IsRealClosed R] {a b : R} (hab : a ≤ b) {P : Polynomial R} (hP : ∀ x ∈ Set.Ioo a b, Polynomial.eval x P ≠ 0) : (∀ x ∈ Set.Icc a b, Polynomial.eval x P ≥ 0) ∨ ∀ x ∈ Set.Icc a b, Polynomial.eval x P ≤ 0

theorem rolle_theorem_weak {R : Type u_1} [Field R] [IsRealClosed R] {a b : R} (hab : a < b) {P : Polynomial R} (hP : ∀ x ∈ Set.Ioo a b, Polynomial.eval x P ≠ 0) (hPa : Polynomial.eval a P = 0) (hPb : Polynomial.eval b P = 0) : ∃ c ∈ Set.Ioo a b, Polynomial.eval c (Polynomial.derivative P) = 0

theorem rolle_theorem_weak' {R : Type u_1} [Field R] [IsRealClosed R] {a b : R} (hab : a < b) {P : Polynomial R} (hPa : Polynomial.eval a P = 0) (hPb : Polynomial.eval b P = 0) : ∃ c ∈ Set.Ioo a b, Polynomial.eval c (Polynomial.derivative P) = 0 ∨ Polynomial.eval c P = 0

theorem rolle_theorem_induction {R : Type u_1} [Field R] [IsRealClosed R] (n : ℕ) {a b : R} {P : Polynomial R} (hab : a < b) (hPa : Polynomial.eval a P = 0) (hPb : Polynomial.eval b P = 0) (hcard : {x ∈ P.roots.toFinset | x ∈ Set.Ioo a b}.card < n) : ∃ c ∈ Set.Ioo a b, Polynomial.eval c (Polynomial.derivative P) = 0

theorem rolle_theorem {R : Type u_1} [Field R] [IsRealClosed R] {a b : R} {P : Polynomial R} (hab : a < b) (hPab : Polynomial.eval a P = Polynomial.eval b P) : ∃ c ∈ Set.Ioo a b, Polynomial.eval c (Polynomial.derivative P) = 0

theorem mean_value_theorem {R : Type u_1} [Field R] [IsRealClosed R] {a b : R} {P : Polynomial R} (hab : a < b) : ∃ c ∈ Set.Ioo a b, Polynomial.eval b P - Polynomial.eval a P = Polynomial.eval c (Polynomial.derivative P) * (b - a)

theorem exists_deriv_eq_slope_poly {R : Type u_1} [Field R] [IsRealClosed R] (a b : R) (hab : a < b) (p : Polynomial R) : ∃ c > a, c < b ∧ Polynomial.eval b p - Polynomial.eval a p = (b - a) * Polynomial.eval c (Polynomial.derivative p)

theorem eval_mod {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) (x : R) (h : Polynomial.eval x q = 0) : Polynomial.eval x (p % q) = Polynomial.eval x p

theorem eval_non_zero {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (x : R) (h : Polynomial.eval x p ≠ 0) : p ≠ 0

theorem mul_C_eq_root_multiplicity {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (c r : R) (hc : ¬c = 0) : Polynomial.rootMultiplicity r p = Polynomial.rootMultiplicity r (Polynomial.C c * p)

theorem div_rem_zero {R : Type u_1} [Field R] [IsRealClosed R] {b c r : Polynomial R} (h_rem : r.degree < b.degree) : (c * b + r) / b = c

theorem mul_cancel' {R : Type u_1} [Field R] [IsRealClosed R] {p q r : Polynomial R} (hr : r ≠ 0) : r * p / (r * q) = p / q

theorem mod_eq_sub_div {R : Type u_1} [Field R] [IsRealClosed R] {a b : Polynomial R} : a % b = a - a / b * b

theorem mod_mul {R : Type u_1} [Field R] [IsRealClosed R] (p q r : Polynomial R) (hr : r ≠ 0) : r * p % (r * q) = r * (p % q)

theorem X_sub_C_ne_one {R : Type u_1} [Field R] [IsRealClosed R] (r : R) : Polynomial.X - Polynomial.C r ≠ 1

theorem rootsInInterval_mul {R : Type u_1} [Field R] [IsRealClosed R] {p q : Polynomial R} (a b : R) (hpq : p * q ≠ 0) : rootsInInterval (p * q) a b = rootsInInterval p a b ∪ rootsInInterval q a b

theorem neg_neg_div {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) : -(-p / q) = p / q

theorem mod_minus {R : Type u_1} [Field R] [IsRealClosed R] (p q : Polynomial R) : -p % q = -(p % q)

theorem factorize {R : Type u_1} [Field R] [IsRealClosed R] (a x : R) (ha : a ≠ 0) : x = a * (x / a)

theorem distrib_div {R : Type u_1} [Field R] [IsRealClosed R] (a b d : R) (hd : d ≠ 0) : (a + b) / d = a / d + b / d

theorem sgn_mul_pos {R : Type u_1} [Field R] [IsRealClosed R] (a b : R) (ha : 0 < a) : sgn (a * b) = sgn b

theorem sgn_dont_change {R : Type u_1} [Field R] [IsRealClosed R] (a b : R) (hab : |b| < |a| / 2) : sgn (a + b) = sgn a

theorem bound_sgn_pos_inf {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (hp : p ≠ 0) : ∃ (ub : R), ∀ x ≥ ub, sgn (Polynomial.eval x p) = sgn_pos_inf p

theorem bound_sgn_neg_inf {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (hp : p ≠ 0) : ∃ (lb : R), ∀ x ≤ lb, sgn (Polynomial.eval x p) = sgn_neg_inf p

theorem root_ub {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (hp : p ≠ 0) : ∃ (ub : R), (∀ (x : R), Polynomial.eval x p = 0 → x < ub) ∧ ∀ x ≥ ub, sgn (Polynomial.eval x p) = sgn_pos_inf p

theorem root_lb {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (hp : p ≠ 0) : ∃ (lb : R), (∀ (x : R), Polynomial.eval x p = 0 → x > lb) ∧ ∀ x ≤ lb, sgn (Polynomial.eval x p) = sgn_neg_inf p

theorem root_list_ub {R : Type u_1} [Field R] [IsRealClosed R] (ps : List (Polynomial R)) (a : R) (h0 : 0 ∉ ps) : ∃ (ub : R), (∀ p ∈ ps, ∀ (x : R), Polynomial.eval x p = 0 → x < ub) ∧ a < ub ∧ ∀ x ≥ ub, ∀ p ∈ ps, sgn (Polynomial.eval x p) = sgn_pos_inf p

theorem root_list_lb {R : Type u_1} [Field R] [IsRealClosed R] (ps : List (Polynomial R)) (b : R) (h0 : 0 ∉ ps) : ∃ (lb : R), (∀ p ∈ ps, ∀ (x : R), Polynomial.eval x p = 0 → lb < x) ∧ lb < b ∧ ∀ x ≤ lb, ∀ p ∈ ps, sgn (Polynomial.eval x p) = sgn_neg_inf p