Compfiles/Imo1968P5.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1968, Problem 5

Let f be a real-valued function defined for all real numbers x such that, for some positive constant a, the equation

f(x + a) = 1/2 + √(f(x) - (f(x))²)

holds for all x.

(a) Prove that the function f is periodic. (b) For a = 1, give an example of a non-constant function with the required properties.

Imports (2)
Imported by 1 file
  1. abbrev Imo1968P5.P line 33 source

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

    Statement uses: Real

    Proof uses: And, LT.lt, OfNat.ofNat, LE.le, HPow.hPow, Nat, Eq, HAdd.hAdd, HDiv.hDiv, Real.sqrt, HSub.hSub

    21 instances, coercions and auxiliary constants left out.

  2. problem Imo1968P5.imo1968_p5a line 37 source

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

    Statement uses: Real, Imo1968P5.P, Exists, And, LT.lt, OfNat.ofNat, Function.Periodic

    Proof uses: LE.le, HPow.hPow, Nat, Eq, HAdd.hAdd, HDiv.hDiv, Real.sqrt, HSub.hSub, Exists.intro, HMul.hMul, And.intro, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Eq.mpr, id and 104 more

    108 instances, coercions and auxiliary constants left out.

    Tactic trace: 28 steps

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

  3. determine Imo1968P5.solution_func line 67 source

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

    Statement uses: Real

    Proof uses: ite, Even, Int, Int.floor, OfNat.ofNat, HDiv.hDiv

    13 instances, coercions and auxiliary constants left out.

  4. problem Imo1968P5.imo1968_p5b line 70 source

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

    Statement uses: And, Imo1968P5.P, OfNat.ofNat, Real, Imo1968P5.solution_func, Not, Exists, Eq, Function.const

    Proof uses: And.intro, LT.lt, LE.le, HPow.hPow, Nat, HAdd.hAdd, HDiv.hDiv, Real.sqrt, HSub.hSub, Real.zero_lt_one, Even, Int, Int.floor, Or, Classical.em, Iff.mpr, Odd, Int.not_even_iff_odd, Even.add_one, of_eq_true and 62 more

    94 instances, coercions and auxiliary constants left out.

    Tactic trace: 29 steps

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