Compfiles/Bulgaria1998P3.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bulgarian Mathematical Olympiad 1998, Problem 3

Let ℝ⁺ be the set of positive real numbers. Prove that there does not exist a function f: ℝ⁺ → ℝ⁺ such that

(f(x))² ≥ f(x + y) * (f(x) + y)

for every x,y ∈ ℝ⁺.

Imports (4)
Imported by 1 file
  1. lemma Bulgaria1998P3.geom_sum_bound line 35 source

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

    Statement uses: Nat, LT.lt, Real, Finset.sum, Finset.range, HDiv.hDiv, OfNat.ofNat, HPow.hPow

    Proof uses: Trans.trans, LE.le, Eq, AddCommMonoid, Finset, Eq.rec, Eq.refl, of_eq_true, Eq.trans, Inv.inv, True, congr, congrArg, funext, HMul.hMul, div_eq_mul_inv, one_mul, congrFun', inv_pow, eq_self and 6 more

    66 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  2. problem Bulgaria1998P3.bulgaria1998_p3 line 43 source

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

    Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, HAdd.hAdd, HPow.hPow, Nat, False

    Proof uses: add_pos, lt_add_of_pos_right, HDiv.hDiv, Iff.mpr, div_lt_one, Trans.trans, Eq, Eq.symm, mul_one, Eq.mpr, id, congrArg, div_self, Ne.symm, ne_of_lt, Eq.refl, mul_div_assoc', div_le_div_iff_of_pos_right, of_eq_true, Eq.trans and 169 more

    181 instances, coercions and auxiliary constants left out.

    Tactic trace: 77 steps

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