Compfiles/Imo1977P4.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1977, Problem 4

Define f(x) = 1 - a cos x - b sin x - A cos 2x - B sin 2x, where a, b, A, B are real constants. Suppose that f(x) ≥ 0 for all real x. Prove that a^2 + b^2 ≤ 2 and A^2 + B^2 ≤ 1.

Imports (2)
Imported by 1 file
  1. problem Imo1977P4.imo1977_p4 line 28 source

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

    Statement uses: Real, Eq, HSub.hSub, OfNat.ofNat, HMul.hMul, Real.cos, Real.sin, Nat, GE.ge, And, LE.le, HAdd.hAdd, HPow.hPow

    Proof uses: Decidable.byContradiction, Not, LT.lt, lt_trans, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, Eq.mp, Real.sqrt, rfl, Iff.mpr, Real.sqrt_pos, Real.sq_sqrt, le_of_lt, HDiv.hDiv, Trans.trans, Eq.mpr and 210 more

    177 instances, coercions and auxiliary constants left out.

    Tactic trace: 204 steps (first 200 of 204)

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