`Compfiles/Usa2018P2.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

29 declarations, 0 contain sorry, 0 declared as axioms

United States of America Mathematical Olympiad 2018, Problem 2

Find all functions $f : (0, \infty) \to (0, \infty)$ such that $$f\left(x + \frac{1}{y}\right) + f\left(y + \frac{1}{z}\right) + f\left(z + \frac{1}{x}\right) = 1$$ for all $x, y, z > 0$ with $xyz = 1$.

Imports (8)

Imported by 1 file

Compfiles.lean

theorem Usa2018P2.jensen_bounded_eq_zero If h satisfies Jensen's functional equation on [0, 1], vanishes at the endpoints and is bounded there, then h is identically zero on [0, 1] line 37 source
Source documentation
If h satisfies Jensen's functional equation on [0, 1], vanishes at the endpoints and is bounded there, then h is identically zero on [0, 1].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, Eq, HDiv.hDiv, HAdd.hAdd, Nat, abs
Proof uses: HPow.hPow, Nat.recAux, dite, Eq.mpr, id, congrFun', congrArg, Eq.trans, congr, Nat.cast_one, pow_zero, div_self, of_eq_true, Not, False, True, not_false_eq_true, Eq.symm, le_antisymm, Nat.rawCast and 173 more
198 instances, coercions and auxiliary constants left out.

Tactic trace: 158 steps
Open to load the checked before-and-after goal states.
```
theorem jensen_bounded_eq_zero {h : ℝ → ℝ}
    (hJ : ∀ s t : ℝ, 0 ≤ s → s ≤ 1 → 0 ≤ t → t ≤ 1 → h ((s + t) / 2) = (h s + h t) / 2)
    (h0 : h 0 = 0) (h1 : h 1 = 0)
    (hb : ∀ t : ℝ, 0 ≤ t → t ≤ 1 → |h t| ≤ 1) :
    ∀ t : ℝ, 0 ≤ t → t ≤ 1 → h t = 0 := by
…
```
Mentions: h
def Usa2018P2.g The normalized function $g(s) = f(1/s - 1)$, mapping $(0, 1)$ to $(0, 1)$ line 195 source
Source documentation
The normalized function $g(s) = f(1/s - 1)$, mapping $(0, 1)$ to $(0, 1)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HSub.hSub, HDiv.hDiv, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
noncomputable def g (f : ℝ → ℝ) : ℝ → ℝ := fun s ↦ f (1 / s - 1)
```
Mentions: f
def Usa2018P2.hfn The discrepancy between g and its linear interpolant on [1/8, 3/8], rescaled to parameters in [0, 1] line 199 source
Source documentation
The discrepancy between g and its linear interpolant on [1/8, 3/8], rescaled to parameters in [0, 1].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HSub.hSub, Usa2018P2.g, HDiv.hDiv, HAdd.hAdd, HMul.hMul, OfNat.ofNat
16 instances, coercions and auxiliary constants left out.
```
noncomputable def hfn (f : ℝ → ℝ) : ℝ → ℝ := fun t ↦
…
```
Mentions: f
theorem Usa2018P2.f_lt_one Every value f t with t > 0 is less than 1 (plug (x, y, z) = (t / 2, 2 / t, 1) into the equation) line 210 source
Source documentation
Every value f t with t > 0 is less than 1 (plug (x, y, z) = (t / 2, 2 / t, 1) into the equation).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv
Proof uses: Ne, ne_of_gt, Nat, of_eq_true, Eq.trans, inferInstance, CommGroupWithZero, True, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, List.nil, Prod, Int, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, congr_arg₂, rfl, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Mathlib.Tactic.FieldSimp.NF.mul_eq_eval, Neg.neg and 114 more
128 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
theorem f_lt_one {t : ℝ} (ht : 0 < t) : f t < 1 := by
…
```
Mentions: f
theorem Usa2018P2.arg_pos For s ∈ (0, 1) the argument 1 / s - 1 of f in g is positive line 220 source
Source documentation
For s ∈ (0, 1) the argument 1 / s - 1 of f in g is positive.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, HSub.hSub, HDiv.hDiv
Proof uses: Eq.mpr, id, Eq, congrArg, propext, one_lt_div, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, HPow.hPow, Nat, Inv.inv and 56 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem arg_pos {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) : 0 < 1 / s - 1 := by
…
```
theorem Usa2018P2.g_pos line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Usa2018P2.g
Proof uses: HSub.hSub, HDiv.hDiv, Usa2018P2.arg_pos
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P2.g_lt_one line 229 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv, Usa2018P2.g
Proof uses: Usa2018P2.f_lt_one, HSub.hSub, Usa2018P2.arg_pos
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P2.g_eq The functional equation rewritten in terms of g via the substitution (x, y, z) = (b / c, c / a, a / b) line 235 source
Source documentation
The functional equation rewritten in terms of g via the substitution (x, y, z) = (b / c, c / a, a / b).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv, Usa2018P2.g
Proof uses: Ne, ne_of_gt, add_pos', of_eq_true, Eq.trans, inferInstance, CommGroupWithZero, True, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, List.nil, Prod, Int, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, congr_arg₂, rfl, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Mathlib.Tactic.FieldSimp.NF.mul_eq_eval, Neg.neg and 103 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
theorem g_eq {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    g f (a / (a + b + c)) + g f (b / (a + b + c)) + g f (c / (a + b + c)) = 1 := by
…
```
Mentions: Usa2018P2.g, f
theorem Usa2018P2.g_eq_one For a + b + c = 1 this reads g a + g b + g c = 1 line 263 source
Source documentation
For a + b + c = 1 this reads g a + g b + g c = 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv, Usa2018P2.g
Proof uses: Usa2018P2.g_eq, Eq.mp, congrArg, div_one
33 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem g_eq_one {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
    (hsum : a + b + c = 1) : g f a + g f b + g f c = 1 := by
…
```
Mentions: Usa2018P2.g, f
theorem Usa2018P2.g_jensen Jensen's functional equation for g on pairs summing to less than 1 line 270 source
Source documentation
Jensen's functional equation for g on pairs summing to less than 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv, Usa2018P2.g, Nat
Proof uses: HSub.hSub, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, 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.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, Eq.symm and 79 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem g_jensen {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a + b < 1) :
    g f a + g f b = 2 * g f ((a + b) / 2) := by
…
```
Mentions: Usa2018P2.g, f
theorem Usa2018P2.hfn_zero line 277 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Usa2018P2.hfn, OfNat.ofNat
Proof uses: HDiv.hDiv, HAdd.hAdd, HMul.hMul, Nat, Mathlib.Meta.NormNum.isNNRat_eq_true, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Eq.refl, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.cast_zero, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Nat.mul, id, Eq.mpr and 41 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P2.hfn_one line 283 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Usa2018P2.hfn, OfNat.ofNat
Proof uses: HDiv.hDiv, HAdd.hAdd, HMul.hMul, Nat, Mathlib.Meta.NormNum.isNNRat_eq_true, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Eq.refl, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Nat.mul, id, Eq.mpr, HSub.hSub and 41 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P2.hfn_jensen line 290 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv, LE.le, Usa2018P2.hfn, Nat
Proof uses: lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, 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, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Meta.NormNum.IsInt.to_raw_eq and 94 more
126 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P2.hfn_bdd line 306 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv, LE.le, abs, Usa2018P2.hfn
Proof uses: Nat, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, 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, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.Common.neg_add and 93 more
126 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P2.hfn_eq_zero line 330 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv, LE.le, Usa2018P2.hfn
Proof uses: Usa2018P2.jensen_bounded_eq_zero, Usa2018P2.hfn_jensen, Usa2018P2.hfn_zero, Usa2018P2.hfn_one, Usa2018P2.hfn_bdd
26 instances, coercions and auxiliary constants left out.
theorem Usa2018P2.g_linear_mid_exp g agrees with a linear function on [1/8, 3/8] line 336 source
Source documentation
g agrees with a linear function on [1/8, 3/8].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv, LE.le, Nat, Usa2018P2.g, HSub.hSub
Proof uses: le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, HPow.hPow, Int.rawCast, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.Common.add_mul and 92 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem g_linear_mid_exp {x : ℝ} (hx0 : 1 / 8 ≤ x) (hx1 : x ≤ 3 / 8) :
    g f x = 4 * (g f (3 / 8) - g f (1 / 8)) * x + (3 * g f (1 / 8) - g f (3 / 8)) / 2 := by
…
```
Mentions: Usa2018P2.g, f
theorem Usa2018P2.kl_sum With 3 g (1/3) = 1 and 1/3 ∈ [1/8, 3/8], the coefficients satisfy k + 3 l = 1 line 349 source
Source documentation
With 3 g (1/3) = 1 and 1/3 ∈ [1/8, 3/8], the coefficients satisfy k + 3 l = 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv, LE.le, Nat, Usa2018P2.g
Proof uses: Usa2018P2.g_eq_one, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Eq.refl, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.mul, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.instAddMonoidWithOne', Mathlib.Meta.NormNum.IsNNRat.to_isNat, Mathlib.Meta.NormNum.isNNRat_add, Mathlib.Meta.NormNum.isRat_le_true and 78 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem kl_sum {k l : ℝ}
    (hmid : ∀ x : ℝ, 1 / 8 ≤ x → x ≤ 3 / 8 → g f x = k * x + l) : k + 3 * l = 1 := by
…
```
Mentions: Usa2018P2.g, f
theorem Usa2018P2.g_linear_ext_low Linearity extends from [1/8, 3/8] down to (0, 1/8) using Jensen line 358 source
Source documentation
Linearity extends from [1/8, 3/8] down to (0, 1/8) using Jensen.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv, LE.le, Nat, Usa2018P2.g
Proof uses: HSub.hSub, Usa2018P2.g_jensen, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 90 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem g_linear_ext_low {k l : ℝ}
    (hmid : ∀ x : ℝ, 1 / 8 ≤ x → x ≤ 3 / 8 → g f x = k * x + l)
    {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1 / 8) : g f x = k * x + l := by
…
```
Mentions: Usa2018P2.g, f
theorem Usa2018P2.g_linear_low g is linear on all of (0, 3/8] line 371 source
Source documentation
g is linear on all of (0, 3/8].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv, LE.le, Nat, Usa2018P2.g
Proof uses: Or, le_or_gt, Usa2018P2.g_linear_ext_low
42 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem g_linear_low {k l : ℝ}
    (hmid : ∀ x : ℝ, 1 / 8 ≤ x → x ≤ 3 / 8 → g f x = k * x + l)
    {x : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 3 / 8) : g f x = k * x + l := by
…
```
Mentions: Usa2018P2.g, f
theorem Usa2018P2.g_linear_ext_high Linearity extends from (0, 3/8] up to (0, 1) using the equation with (x, (1 - x) / 2, (1 - x) / 2) line 381 source
Source documentation
Linearity extends from (0, 3/8] up to (0, 1) using the equation with (x, (1 - x) / 2, (1 - x) / 2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv, Nat, LE.le, Usa2018P2.g
Proof uses: HSub.hSub, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id and 101 more
115 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem g_linear_ext_high {k l : ℝ} (hsum : k + 3 * l = 1)
    (hmid : ∀ x : ℝ, 1 / 8 ≤ x → x ≤ 3 / 8 → g f x = k * x + l)
    {x : ℝ} (hx0 : 3 / 8 ≤ x) (hx1 : x < 1) : g f x = k * x + l := by
…
```
Mentions: Usa2018P2.g, f
theorem Usa2018P2.g_linear g is linear on all of (0, 1) line 391 source
Source documentation
g is linear on all of (0, 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv, Nat, LE.le, Usa2018P2.g
Proof uses: Or, le_or_gt, Usa2018P2.g_linear_low, Usa2018P2.g_linear_ext_high, le_of_lt
43 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem g_linear {k l : ℝ} (hsum : k + 3 * l = 1)
    (hmid : ∀ x : ℝ, 1 / 8 ≤ x → x ≤ 3 / 8 → g f x = k * x + l)
    {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : g f x = k * x + l := by
…
```
Mentions: Usa2018P2.g, f
theorem Usa2018P2.l_nonneg Since g is positive, the constant term of the linear function is nonnegative line 401 source
Source documentation
Since g is positive, the constant term of the linear function is nonnegative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, Usa2018P2.g, HAdd.hAdd, HMul.hMul, LE.le
Proof uses: Decidable.byContradiction, Not, Or, False, le_or_gt, HDiv.hDiv, Nat, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Eq.refl, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.mul, Bool and 94 more
127 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
theorem l_nonneg {k l : ℝ}
    (hg : ∀ x : ℝ, 0 < x → x < 1 → g f x = k * x + l) : 0 ≤ l := by
…
```
Mentions: Usa2018P2.g, f
theorem Usa2018P2.kl_nonneg Since g is positive, the value of the linear function at 1 is nonnegative line 433 source
Source documentation
Since g is positive, the value of the linear function at 1 is nonnegative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, Usa2018P2.g, HAdd.hAdd, HMul.hMul, LE.le
Proof uses: Decidable.byContradiction, Not, Or, False, le_or_gt, HDiv.hDiv, Nat, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Eq.refl, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.mul, Bool and 135 more
132 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
theorem kl_nonneg {k l : ℝ}
    (hg : ∀ x : ℝ, 0 < x → x < 1 → g f x = k * x + l) : 0 ≤ k + l := by
…
```
Mentions: Usa2018P2.g, f
theorem Usa2018P2.k_mem The slope of the linear function lies in [-1/2, 1] line 470 source
Source documentation
The slope of the linear function lies in [-1/2, 1].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HMul.hMul, Nat, Usa2018P2.g, Membership.mem, Set, Set.Icc, HDiv.hDiv, Neg.neg
Proof uses: LE.le, Usa2018P2.l_nonneg, Usa2018P2.kl_nonneg, Eq.mpr, And, id, congrArg, propext, Set.mem_Icc, And.intro, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast and 78 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem k_mem {k l : ℝ} (hsum : k + 3 * l = 1)
    (hg : ∀ x : ℝ, 0 < x → x < 1 → g f x = k * x + l) : k ∈ Set.Icc (-1 / 2) 1 := by
…
```
Mentions: Usa2018P2.g, f
theorem Usa2018P2.f_formula Transfer the linear formula for g back to f line 478 source
Source documentation
Transfer the linear formula for g back to f.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Nat, LT.lt, Usa2018P2.g, HDiv.hDiv, HSub.hSub
Proof uses: lt_of_not_ge, LE.le, 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, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Meta.NormNum.IsInt.to_raw_eq and 77 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem f_formula {k l : ℝ} (hsum : k + 3 * l = 1)
    (hg : ∀ x : ℝ, 0 < x → x < 1 → g f x = k * x + l)
    {t : ℝ} (ht : 0 < t) : f t = k / (t + 1) + (1 - k) / 3 := by
…
```
Mentions: Usa2018P2.g, f
theorem Usa2018P2.forward Forward direction: every solution belongs to the one-parameter family line 496 source
Source documentation
Forward direction: every solution belongs to the one-parameter family.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv, Exists, And, Membership.mem, Set, Set.Icc, Neg.neg, Nat, HSub.hSub
Proof uses: LE.le, Usa2018P2.g, Usa2018P2.g_linear_mid_exp, Usa2018P2.kl_sum, Usa2018P2.g_linear, Exists.intro, And.intro, Usa2018P2.k_mem, Usa2018P2.f_formula
45 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem forward :
    ∃ k : ℝ, k ∈ Set.Icc (-1 / 2) 1 ∧ ∀ t : ℝ, 0 < t → f t = k / (t + 1) + (1 - k) / 3 := by
…
```
Mentions: f
theorem Usa2018P2.backward Backward direction: every function of the one-parameter family solves the problem line 509 source
Source documentation
Backward direction: every function of the one-parameter family solves the problem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Membership.mem, Set, Set.Icc, HDiv.hDiv, Neg.neg, OfNat.ofNat, Nat, LT.lt, Eq, HAdd.hAdd, HSub.hSub, And, HMul.hMul
Proof uses: LE.le, Eq.mp, congrArg, propext, Set.mem_Icc, And.intro, Eq.mpr, id, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, 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, Mathlib.Tactic.Ring.cast_pos and 154 more
177 instances, coercions and auxiliary constants left out.

Tactic trace: 72 steps
Open to load the checked before-and-after goal states.
```
theorem backward {f : ℝ → ℝ} {k : ℝ} (hk : k ∈ Set.Icc (-1 / 2) 1)
    (hf : ∀ t : ℝ, 0 < t → f t = k / (t + 1) + (1 - k) / 3) :
    (∀ x : ℝ, 0 < x → 0 < f x) ∧
    (∀ x y z : ℝ, 0 < x → 0 < y → 0 < z → x * y * z = 1 →
      f (x + 1 / y) + f (y + 1 / z) + f (z + 1 / x) = 1) := by
…
```
Mentions: f
determine Usa2018P2.solution_set line 573 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Real
Proof uses: Set.ofPred, Exists, And, Membership.mem, Set.Icc, HDiv.hDiv, Neg.neg, OfNat.ofNat, LT.lt, Eq, HAdd.hAdd, HSub.hSub
19 instances, coercions and auxiliary constants left out.
problem Usa2018P2.usa2018_p2 line 576 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Iff, Membership.mem, Set, Usa2018P2.solution_set, And, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, HDiv.hDiv
Proof uses: Iff.intro, Set.Icc, Neg.neg, HSub.hSub, Usa2018P2.backward, Usa2018P2.forward
36 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.