Compfiles/Usa2000P1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2000, Problem 1

A function f : ℝ → ℝ is called "very convex" if it satisfies

∀ x y : ℝ, (f(x) + f(y))/2 ≥ f((x + y)/2) + |x - y|.

Show that there exist no very convex functions.

Imports (3)
Imported by 1 file
  1. problem Usa2000P1.usa2000_p1 line 30 source

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

    Statement uses: Not, Exists, Real, LE.le, HAdd.hAdd, HDiv.hDiv, OfNat.ofNat, Nat, abs, HSub.hSub

    Proof uses: Eq.mpr, id, Eq, congrArg, propext, not_exists, Or, False, Classical.em, Neg.neg, HPow.hPow, LT.lt, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false, zero_add and 143 more

    175 instances, coercions and auxiliary constants left out.

    Tactic trace: 153 steps

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