Compfiles/Usa1992P5.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def Usa1992P5.pseq The iterated polynomial sequence of the problem: pseq [z₁, …, zₙ] is the polynomial pₙ, where p₁(z) = z - z₁ and pₖ(z) = pₖ₋₁(z)² - zₖ line 32 source

   Source documentation

   The iterated polynomial sequence of the problem: pseq [z₁, …, zₙ] is the polynomial pₙ, where p₁(z) = z - z₁ and pₖ(z) = pₖ₋₁(z)² - zₖ.

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

   Statement uses: List, Complex, Polynomial

   Proof uses: Usa1992P5.pseq.match_1, Unit, Polynomial.X, List.foldl, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat, RingHom, Polynomial.C

   14 instances, coercions and auxiliary constants left out.

   noncomputable def pseq : List ℂ → ℂ[X]
     | [] => X
     | z :: zs => zs.foldl (fun P w => P ^ 2 - C w) (X - C z)
   
   snip begin
   
   -- Follows the solution at https://prase.cz/kalva/usa/usoln/usol925.html.
   -- Starting from the set S of zeros of q, repeatedly replace S by the smaller
   -- set {(s - m)² : s ∈ S}, where m is the midpoint of two distinct elements
   -- of S; after at most |S| - 1 steps one reaches a set with a single element,
   -- and choosing the next z to be that element makes p vanish on all of S.

   Mentions: P, solution, S

2. lemma Usa1992P5.pseq_concat line 44 source

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

   Statement uses: List, Complex, Ne, List.nil, Eq, Polynomial, Usa1992P5.pseq, HAppend.hAppend, List.cons, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat, RingHom, Polynomial.C

   Proof uses: absurd, rfl, Eq.symm, of_eq_true, List.foldl, Polynomial.X, Eq.trans, True, congrFun', congrArg, List.foldl_append, eq_self, Eq.refl

   32 instances, coercions and auxiliary constants left out.

   Tactic trace: 3 steps

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

3. lemma Usa1992P5.pseq_foldl_comp line 51 source

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

   Statement uses: Polynomial, Complex, List, Eq, Polynomial.comp, List.foldl, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat, RingHom, Polynomial.C

   Proof uses: List.rec, Eq.refl, List.nil, Eq.mpr, List.cons, id, congrFun', congrArg, Eq.rec, of_eq_true, Eq.trans, True, Polynomial.sub_comp, congr, Polynomial.pow_comp, Polynomial.C_comp, eq_self

   29 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

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

4. lemma Usa1992P5.pseq_cons_comp line 61 source

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

   Statement uses: Complex, List, Eq, Polynomial, Usa1992P5.pseq, List.cons, Polynomial.comp, HPow.hPow, Nat, HSub.hSub, Polynomial.X, RingHom, Polynomial.C, OfNat.ofNat

   Proof uses: id, Eq.mpr, List.foldl, congrArg, Usa1992P5.pseq_foldl_comp, Eq.rec, Eq.refl, of_eq_true, Eq.trans, True, Polynomial.sub_comp, congr, Polynomial.X_comp, Polynomial.C_comp, eq_self

   27 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

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

5. lemma Usa1992P5.pseq_cons_eval line 68 source

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

   Statement uses: Complex, List, Ne, List.nil, Eq, Polynomial.eval, Usa1992P5.pseq, List.cons, HPow.hPow, Nat, HSub.hSub, OfNat.ofNat

   Proof uses: absurd, rfl, Eq.symm, Eq.mpr, Polynomial.comp, Polynomial, Polynomial.X, RingHom, Polynomial.C, id, congrArg, Usa1992P5.pseq_cons_comp, Polynomial.eval_comp, of_eq_true, Eq.trans, True, congrFun', Polynomial.eval_pow, Polynomial.eval_sub, congr and 4 more

   31 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

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

6. lemma Usa1992P5.exists_pseq_eval_eq_zero The combinatorial heart of the solution: for any nonempty set S of at most n complex numbers one can choose z₁, …, zₙ so that pₙ vanishes on all of S line 79 source

   Source documentation

   The combinatorial heart of the solution: for any nonempty set S of at most n complex numbers one can choose z₁, …, zₙ so that pₙ vanishes on all of S.

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

   Statement uses: Nat, Finset, Complex, Finset.Nonempty, LE.le, Finset.card, Exists, List, And, Eq, List.length, Membership.mem, Polynomial.eval, Usa1992P5.pseq, OfNat.ofNat

   Proof uses: Nat.recAux, False.elim, LT.lt, Iff.mpr, Finset.card_pos, HAdd.hAdd, Or, lt_or_ge, dite, Exists.intro, List.cons, List.nil, And.intro, rfl, Iff.mp, Finset.card_le_one, of_eq_true, Eq.trans, True, congrFun' and 100 more

   127 instances, coercions and auxiliary constants left out.

   Tactic trace: 58 steps

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

   lemma exists_pseq_eval_eq_zero :
       ∀ n : ℕ, ∀ S : Finset ℂ, S.Nonempty → S.card ≤ n →
         ∃ zs : List ℂ, zs.length = n ∧ ∀ w ∈ S, (pseq zs).eval w = 0 := by
   …

   Mentions: S, Usa1992P5.pseq

7. problem Usa1992P5.usa1992_p5 line 145 source

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

   Statement uses: Polynomial, Complex, Eq, Nat, Polynomial.natDegree, OfNat.ofNat, Multiset.Nodup, Polynomial.roots, Exists, List, And, List.length, Dvd.dvd, Usa1992P5.pseq

   Proof uses: Ne, False, False.elim, Eq.mp, eq_false, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, congrArg, Polynomial.natDegree_zero, Eq.symm, Polynomial.Splits, IsAlgClosed.splits, Multiset.card, Eq.mpr, id, Iff.mp, Polynomial.splits_iff_card_roots and 51 more

   97 instances, coercions and auxiliary constants left out.

   Tactic trace: 31 steps

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