Compfiles/Imo1976P2.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1976, Problem 2

Let $P_{1}(x) = x^{2} - 2$ and $P_{j}(x) = P_{1}(P_{j - 1}(x))$ for $j= 2,\ldots$. Show that for any positive integer $n,$ the roots of the equation $P_{n}(x) = x$ are real and distinct.

Imports (2)
Imported by 1 file
  1. def Imo1976P2.P line 30 source

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

    Statement uses: Nat, Polynomial, Real

    Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, Imo1976P2.P.match_1, Unit, OfNat.ofNat, HSub.hSub, HPow.hPow, Polynomial.X, Nat.succ, Polynomial.comp, HAdd.hAdd

    21 instances, coercions and auxiliary constants left out.

  2. theorem Imo1976P2.all_real_roots line 39 source

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

    Statement uses: Polynomial, Real, Finset, Membership.mem, Polynomial.IsRoot, Eq, Nat, Finset.card, Polynomial.natDegree, Multiset, Complex, Polynomial.aroots, Finset.val, Finset.image

    Proof uses: Ne, OfNat.ofNat, Not, Or, Classical.em, Eq.mpr, id, congrArg, propext, eq_comm, Multiset.eq_of_le_of_card_le, LE.le, HasSubset.Subset, Multiset.le_iff_subset, of_eq_true, Multiset.Nodup, Multiset.dedup, Multiset.map, Exists, And and 33 more

    116 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

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

  3. theorem Imo1976P2.root_of_sign_flip line 62 source

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

    Statement uses: ConditionallyCompleteLinearOrder, TopologicalSpace, OrderTopology, DenselyOrdered, Ring, LinearOrder, OrderClosedTopology, AddLeftMono, MulPosMono, PosMulMono, LE.le, ContinuousOn, Set.Icc, LT.lt, HMul.hMul, OfNat.ofNat, Exists, And, Membership.mem, Set and 2 more

    Proof uses: dite, Set.image, intermediate_value_Ioo, Eq.mpr, id, Mathlib.Tactic.Contrapose.contrapose₁, Not, implies_congr, Eq.trans, Mathlib.Tactic.Push.not_and_eq, Eq.refl, le_mul_of_le_mul_of_nonneg_left, mul_nonneg, le_of_lt, Eq.mp, Neg.neg, congrArg, Eq.symm, neg_mul_neg, le_mul_of_le_mul_of_nonneg_right and 5 more

    68 instances, coercions and auxiliary constants left out.

    Tactic trace: 42 steps

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

  4. theorem Imo1976P2.P_natDegree line 100 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Polynomial.natDegree, Real, Imo1976P2.P, HPow.hPow

    Proof uses: Imo1976P2.P.induct_unfolding, Polynomial, False.elim, Eq.mp, False, of_eq_true, HSub.hSub, Polynomial.X, Eq.trans, True, congr, congrArg, RingHom, Polynomial.C, Polynomial.natDegree_sub_C, HMul.hMul, Polynomial.natDegree_pow, Polynomial.natDegree_X, mul_one, pow_one and 38 more

    99 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  5. structure Imo1976P2.NicePlotOfP line 112 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  6. theorem Imo1976P2.NicePlotOfP.findRoot line 122 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Imo1976P2.NicePlotOfP, HAdd.hAdd, Imo1976P2.NicePlotOfP.k, Exists, Real, And, Membership.mem, Set, Set.Ioo, Imo1976P2.NicePlotOfP.x, Fin.mk, Polynomial.IsRoot, Imo1976P2.P

    Proof uses: Polynomial.eval, Continuous, Polynomial.continuous_eval₂, RingHom.id, LE.le, id, StrictMono.monotone, Fin, Imo1976P2.NicePlotOfP.strictMono, of_eq_true, Eq.trans, True, HMul.hMul, Eq.mpr, HPow.hPow, Neg.neg, Eq, congrArg, Imo1976P2.NicePlotOfP.y_eq, pow_succ and 17 more

    167 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  7. theorem Imo1976P2.NicePlotOfP.findRoot.spec_gt line 140 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Imo1976P2.NicePlotOfP, HAdd.hAdd, Imo1976P2.NicePlotOfP.k, Fin, Eq, Real, Imo1976P2.NicePlotOfP.x, Exists.choose, And, Membership.mem, Set, Set.Ioo, Fin.mk, Polynomial.IsRoot, Imo1976P2.P, Imo1976P2.NicePlotOfP.findRoot

    Proof uses: Exists.choose_spec, Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, congrArg, of_eq_true, Eq.symm, True, Fin.mk.congr_simp, eq_self, And.left, Iff.mpr, Set.mem_Ioo

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  8. theorem Imo1976P2.NicePlotOfP.findRoot.spec_lt line 148 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Imo1976P2.NicePlotOfP, HAdd.hAdd, Imo1976P2.NicePlotOfP.k, Fin, Eq, Real, Exists.choose, And, Membership.mem, Set, Set.Ioo, Imo1976P2.NicePlotOfP.x, Fin.mk, Polynomial.IsRoot, Imo1976P2.P, Imo1976P2.NicePlotOfP.findRoot

    Proof uses: Exists.choose_spec, Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, congrArg, of_eq_true, Eq.symm, True, Fin.mk.congr_simp, eq_self, And.right, Iff.mpr, Set.mem_Ioo, And.left

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  9. theorem Imo1976P2.NicePlotOfP.findRoot.spec_root line 154 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Imo1976P2.NicePlotOfP, HAdd.hAdd, Imo1976P2.NicePlotOfP.k, Polynomial.IsRoot, Real, Imo1976P2.P, Exists.choose, And, Membership.mem, Set, Set.Ioo, Imo1976P2.NicePlotOfP.x, Fin.mk, Imo1976P2.NicePlotOfP.findRoot

    Proof uses: Exists.choose_spec, And.right

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  10. theorem Imo1976P2.Fin.val_orderSucc_of_notTop line 160 source

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

    Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Ne, Top.top, Eq, Order.succ

    Proof uses: Eq.mpr, Fin.castSucc, Fin.mk, Fin.val_lt_last, id, congrArg, of_eq_true, eq_self, Fin.succ, Fin.orderSucc_castSucc, Eq.trans, True

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  11. def Imo1976P2.makePlot line 166 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Imo1976P2.NicePlotOfP

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 95 steps

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

  12. theorem Imo1976P2.P_intersect_X line 267 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Imo1976P2.NicePlotOfP, Membership.mem, Finset, Finset.range, HSub.hSub, Polynomial.natDegree, Real, Imo1976P2.P, Exists, And, Set, Set.Ioo, Imo1976P2.NicePlotOfP.x, Fin.mk, Imo1976P2.NicePlotOfP.k, HAdd.hAdd, Eq and 3 more

    Proof uses: Continuous, Polynomial.continuous_eval₂, RingHom.id, LE.le, id, StrictMono.monotone, Fin, Imo1976P2.NicePlotOfP.strictMono, Insert.insert, Singleton.singleton, Neg.neg, Eq.mpr, HMul.hMul, HPow.hPow, congrArg, Imo1976P2.NicePlotOfP.y_eq, dite, Even, Iff.mpr, neg_one_pow_eq_one_iff_even and 90 more

    185 instances, coercions and auxiliary constants left out.

    Tactic trace: 63 steps

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

  13. theorem Imo1976P2.P_intersect_X.spec_gt line 328 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Imo1976P2.NicePlotOfP, Membership.mem, Finset, Finset.range, HSub.hSub, Polynomial.natDegree, Real, Imo1976P2.P, Fin, Imo1976P2.NicePlotOfP.k, Eq, Imo1976P2.NicePlotOfP.x, Exists.choose, And, Set, Set.Ioo, Fin.mk and 5 more

    Proof uses: Exists.choose_spec

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  14. theorem Imo1976P2.P_intersect_X.spec_lt line 333 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Imo1976P2.NicePlotOfP, Membership.mem, Finset, Finset.range, HSub.hSub, Polynomial.natDegree, Real, Imo1976P2.P, Fin, Imo1976P2.NicePlotOfP.k, Eq, HAdd.hAdd, Exists.choose, And, Set, Set.Ioo, Imo1976P2.NicePlotOfP.x and 5 more

    Proof uses: Exists.choose_spec

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  15. theorem Imo1976P2.P_intersect_X.spec_root line 338 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Imo1976P2.NicePlotOfP, Membership.mem, Finset, Finset.range, HSub.hSub, Polynomial.natDegree, Real, Imo1976P2.P, Polynomial.IsRoot, Polynomial, Polynomial.X, Exists.choose, And, Set, Set.Ioo, Imo1976P2.NicePlotOfP.x, Fin.mk and 5 more

    Proof uses: Exists.choose_spec, And.right

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  16. problem Imo1976P2.imo1976_p2 line 346 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, And, Complex, Membership.mem, Multiset, Polynomial.aroots, Real, HSub.hSub, Polynomial, Imo1976P2.P, Polynomial.X, Eq, Complex.im, Multiset.Nodup

    Proof uses: Exists, Finset, Finset.card, Polynomial.natDegree, Polynomial.IsRoot, Imo1976P2.NicePlotOfP, Imo1976P2.makePlot, Exists.intro, Union.union, Singleton.singleton, Finset.image, Subtype, Finset.range, Exists.choose, Set, Set.Ioo, Imo1976P2.NicePlotOfP.x, Fin.mk, Imo1976P2.NicePlotOfP.k, Subtype.prop and 91 more

    183 instances, coercions and auxiliary constants left out.

    Tactic trace: 57 steps

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