Compfiles/Usa1990P2.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1990, Problem 2

A sequence of functions {fₙ(x)} is defined recursively as follows:

f₀(x) = 8 fₙ₊₁(x) = √(x² + 6fₙ(x)).

For each nonnegative integer n, find all real solutions of the equation

fₙ(x) = 2x.

Imports (2)
Imported by 1 file
  1. def Usa1990P2.f line 32 source

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

    Statement uses: Nat, Real

    2 instances, coercions and auxiliary constants left out.

  2. determine Usa1990P2.solution_set line 36 source

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

    Statement uses: Nat, Set, Real

    Proof uses: Singleton.singleton, OfNat.ofNat

    4 instances, coercions and auxiliary constants left out.

  3. problem Usa1990P2.usa1990_p2 line 38 source

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

    Statement uses: Nat, Real, Iff, Membership.mem, Set, Usa1990P2.solution_set, Eq, Usa1990P2.f, HMul.hMul, OfNat.ofNat

    Proof uses: LT.lt, Nat.recAux, of_eq_true, Eq.trans, True, eq_true, True.intro, Eq.mpr, HAdd.hAdd, Real.sqrt, HPow.hPow, id, congrArg, Usa1990P2.f.eq_def, Real.sqrt_pos_of_pos, Right.add_pos_of_nonneg_of_pos, inferInstance, Zero, PartialOrder, Even.pow_nonneg and 115 more

    106 instances, coercions and auxiliary constants left out.

    Tactic trace: 63 steps

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