Compfiles/Imo1972P5.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1972, Problem 5

f and g are real-valued functions defined on the real line. For all x and y, f(x + y) + f(x - y) = 2f(x)g(y). f is not identically zero and |f(x)| ≤ 1 for all x. Prove that |g(x)| ≤ 1 for all x.

Imports (3)
Imported by 1 file
  1. problem Imo1972P5.imo1972_p5 line 31 source

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

    Statement uses: Real, Eq, HAdd.hAdd, HSub.hSub, HMul.hMul, OfNat.ofNat, Nat, BddAbove, Set.range, Norm.norm, Exists, Ne, LE.le

    Proof uses: Decidable.byContradiction, Not, False, iSup, le_ciSup, LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.neg_congr and 77 more

    136 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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