Compfiles/Usa2002P3.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem Usa2002P3.injOn_range_of_step If ξ is strictly increasing at consecutive arguments below n, then it is injective on Finset.range n line 34 source

   Source documentation

   If ξ is strictly increasing at consecutive arguments below n, then it is injective on Finset.range n.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Real, LT.lt, HAdd.hAdd, OfNat.ofNat, Set.InjOn, Finset, Finset.range

   Proof uses: Nat.recAux, Eq.mp, congrFun', congrArg, zero_add, LT.lt.trans, Membership.mem, Set, Eq, Or, lt_trichotomy, HSub.hSub, Set.Iio, propext, Set.mem_Iio, Finset.coe_range, absurd, ne_of_lt, Eq.symm, ne_of_gt

   32 instances, coercions and auxiliary constants left out.

   Tactic trace: 30 steps

   Open to load the checked before-and-after goal states.

   theorem injOn_range_of_step {n : ℕ} {ξ : ℕ → ℝ}
       (h : ∀ i, i + 1 < n → ξ i < ξ (i + 1)) :
       Set.InjOn ξ (Finset.range n) := by
   …

   Mentions: h

2. theorem Usa2002P3.card_roots_eq_n A nonzero real polynomial of degree n that has n distinct real roots has exactly n roots (counted with multiplicity), and in particular it splits line 62 source

   Source documentation

   A nonzero real polynomial of degree n that has n distinct real roots has exactly n roots (counted with multiplicity), and in particular it splits.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Polynomial, Real, Nat, Ne, OfNat.ofNat, Eq, Polynomial.natDegree, Set.InjOn, Finset, Finset.range, Membership.mem, Polynomial.eval, And, Multiset.card, Polynomial.roots, Polynomial.Splits

   Proof uses: LE.le, Multiset, Finset.val, Finset.image, Eq.mpr, HasSubset.Subset, id, congrArg, propext, Multiset.le_iff_subset, Finset.nodup, Exists, Iff.mp, Finset.mem_image, Iff.mpr, Polynomial.IsRoot, Polynomial.mem_roots, Finset.card, Finset.card_image_of_injOn, Finset.card_range and 8 more

   31 instances, coercions and auxiliary constants left out.

   Tactic trace: 14 steps

   Open to load the checked before-and-after goal states.

   theorem card_roots_eq_n {p : ℝ[X]} {n : ℕ} (hp0 : p ≠ 0) (hn : p.natDegree = n)
       {ξ : ℕ → ℝ} (hinj : Set.InjOn ξ (Finset.range n))
       (hroot : ∀ i ∈ Finset.range n, p.eval (ξ i) = 0) :
       p.roots.card = n ∧ p.Splits := by
   …

3. theorem Usa2002P3.card_roots_eq_n_of_intervals Documented declaration: card_roots_eq_n_of_intervals line 83 source

   Source documentation

   A nonzero real polynomial of degree n that has a root in each of n open intervals (L i, R i) arranged in increasing order (R i ≤ L (i+1)) has exactly n real roots and splits.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Polynomial, Real, Nat, Ne, OfNat.ofNat, Eq, Polynomial.natDegree, LT.lt, HAdd.hAdd, LE.le, Exists, And, Membership.mem, Set, Set.Ioo, Polynomial.eval, Multiset.card, Polynomial.roots, Polynomial.Splits

   Proof uses: Exists.intro, dite, Classical.choose, Not, Eq.mpr, id, congr, congrArg, Decidable, dite_eq_left, congrFun', Classical.choose_spec, And.right, And.left, lt_trans, lt_of_lt_of_le, Usa2002P3.card_roots_eq_n, Usa2002P3.injOn_range_of_step, Finset, Finset.range and 2 more

   33 instances, coercions and auxiliary constants left out.

   Tactic trace: 11 steps

   Open to load the checked before-and-after goal states.

   theorem card_roots_eq_n_of_intervals {p : ℝ[X]} {n : ℕ} (hp0 : p ≠ 0) (hn : p.natDegree = n)
       {L R : ℕ → ℝ} (hstep : ∀ i, i + 1 < n → R i ≤ L (i + 1))
       (hex : ∀ i, i < n → ∃ x ∈ Set.Ioo (L i) (R i), p.eval x = 0) :
       p.roots.card = n ∧ p.Splits := by
   …

4. theorem Usa2002P3.exists_root_of_eval_mul_neg Intermediate value theorem for polynomials: if p changes sign between a and b, then p has a root in the open interval (a, b) line 102 source

   Source documentation

   Intermediate value theorem for polynomials: if p changes sign between a and b, then p has a root in the open interval (a, b).

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Polynomial, Real, LT.lt, HMul.hMul, Polynomial.eval, OfNat.ofNat, Exists, And, Membership.mem, Set, Set.Ioo, Eq

   Proof uses: Or, Iff.mp, mul_neg_iff, HAdd.hAdd, Set.image, intermediate_value_Ioo', LT.lt.le, Polynomial.continuousOn, Set.Icc, And.intro, Exists.intro, intermediate_value_Ioo

   72 instances, coercions and auxiliary constants left out.

   Tactic trace: 7 steps

   Open to load the checked before-and-after goal states.

   theorem exists_root_of_eval_mul_neg {p : ℝ[X]} {a b : ℝ} (hab : a < b)
       (h : p.eval a * p.eval b < 0) : ∃ c ∈ Set.Ioo a b, p.eval c = 0 := by
   …

   Mentions: h

5. theorem Usa2002P3.card_roots_and_splits Let p be a nonzero real polynomial of degree n whose values at the integers 1, ..., n alternate in sign, so that p has a root in each of the n - 1 intervals (i, i+1) line 114 source

   Source documentation

   Let p be a nonzero real polynomial of degree n whose values at the integers 1, ..., n alternate in sign, so that p has a root in each of the n - 1 intervals (i, i+1). If moreover p changes sign on one of the two "tails" (-∞, 1) or (n, ∞), then p has exactly n real roots and splits.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Polynomial, Real, Nat, Ne, OfNat.ofNat, Eq, Polynomial.natDegree, LE.le, HAdd.hAdd, LT.lt, HMul.hMul, Polynomial.eval, Or, Exists, And, Multiset.card, Polynomial.roots, Polynomial.Splits

   Proof uses: Usa2002P3.card_roots_eq_n_of_intervals, ite, Eq.mpr, id, congrArg, ite_eq_right, le_refl, dite, Membership.mem, Set, Set.Ioo, ite_eq_left, rfl, Usa2002P3.exists_root_of_eval_mul_neg, Exists.intro, And.intro, of_eq_true, Eq.trans, True, congrFun' and 8 more

   73 instances, coercions and auxiliary constants left out.

   Tactic trace: 47 steps

   Open to load the checked before-and-after goal states.

   theorem card_roots_and_splits {p : ℝ[X]} {n : ℕ} (hp0 : p ≠ 0) (hn : p.natDegree = n)
       (hmul : ∀ i : ℕ, 1 ≤ i → i + 1 ≤ n →
         p.eval (i : ℝ) * p.eval ((i + 1 : ℕ) : ℝ) < 0)
       (htail : (∃ a₁ : ℝ, a₁ < 1 ∧ p.eval a₁ * p.eval 1 < 0) ∨
                (∃ a₂ : ℝ, (n : ℝ) < a₂ ∧ p.eval (n : ℝ) * p.eval a₂ < 0)) :
       p.roots.card = n ∧ p.Splits := by
   …

6. theorem Usa2002P3.exists_eval_pos A monic real polynomial of positive degree takes arbitrarily large positive values line 158 source

   Source documentation

   A monic real polynomial of positive degree takes arbitrarily large positive values.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Polynomial, Real, Polynomial.Monic, LE.le, Nat, OfNat.ofNat, Polynomial.natDegree, Exists, And, LT.lt, Polynomial.eval

   Proof uses: WithBot, Polynomial.degree, Iff.mp, Polynomial.natDegree_pos_iff_degree_pos, Polynomial.leadingCoeff, Eq, Eq.mpr, id, congrArg, zero_le_one, Filter.Tendsto, Filter.atTop, Polynomial.tendsto_atTop_of_leadingCoeff_nonneg, Filter.Eventually.exists, Filter.Eventually.and, Filter.Tendsto.eventually_ge_atTop, Filter.eventually_gt_atTop, Exists.intro, And.intro, lt_of_not_ge and 47 more

   82 instances, coercions and auxiliary constants left out.

   Tactic trace: 10 steps

   Open to load the checked before-and-after goal states.

   theorem exists_eval_pos {p : ℝ[X]} (hm : p.Monic) (hd : 1 ≤ p.natDegree) (B : ℝ) :
       ∃ c : ℝ, B < c ∧ 0 < p.eval c := by
   …

7. theorem Usa2002P3.exists_eval_neg_one_pow_pos A monic real polynomial p of degree n, multiplied by (-1)^n, takes arbitrarily large positive values at large negative arguments line 172 source

   Source documentation

   A monic real polynomial p of degree n, multiplied by (-1)^n, takes arbitrarily large positive values at large negative arguments.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Polynomial, Real, Polynomial.Monic, LE.le, Nat, OfNat.ofNat, Polynomial.natDegree, Exists, And, LT.lt, HMul.hMul, HPow.hPow, Neg.neg, Polynomial.eval

   Proof uses: Ne, Eq, Polynomial.leadingCoeff, Asymptotics.IsEquivalent, Filter.atBot, Polynomial.isEquivalent_atBot_lead, Eq.mp, congrArg, funext, one_mul, Asymptotics.IsEquivalent.mul, Asymptotics.IsEquivalent.refl, Filter.Tendsto, Filter.atTop, Filter.Tendsto.comp, Filter.tendsto_pow_atTop, Filter.tendsto_neg_atBot_atTop, Filter.Tendsto.congr', Filter.univ_mem', Set.ofPred and 71 more

   115 instances, coercions and auxiliary constants left out.

   Tactic trace: 19 steps

   Open to load the checked before-and-after goal states.

   theorem exists_eval_neg_one_pow_pos {p : ℝ[X]} (hm : p.Monic) (hd : 1 ≤ p.natDegree) (B : ℝ) :
       ∃ a : ℝ, a < B ∧ 0 < (-1 : ℝ) ^ p.natDegree * p.eval a := by
   …

8. problem Usa2002P3.usa2002_p3 line 197 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Polynomial, Real, Polynomial.Monic, Eq, Polynomial.natDegree, Exists, And, Multiset.card, Polynomial.roots, Polynomial.Splits, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat

   Proof uses: Ne, Or, eq_or_ne, Iff.mp, Polynomial.Monic.natDegree_eq_zero, two_ne_zero, Exists.intro, And.intro, Polynomial.monic_one, of_eq_true, Eq.trans, True, congrFun', congrArg, Polynomial.natDegree_one, eq_self, Multiset, Polynomial.roots_one, Polynomial.Splits.one, Eq.mpr and 131 more

   175 instances, coercions and auxiliary constants left out.

   Tactic trace: 174 steps

   Open to load the checked before-and-after goal states.