`Compfiles/Usa1977P5.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

4 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1977, Problem 5

The positive reals v, w, x, y, z satisfy 0 < h ≤ v, w, x, y, z ≤ k. Show that

(v + w + x + y + z)(1/v + 1/w + 1/x + 1/y + 1/z) ≤ 25 + 6(√(h/k) - √(k/h))².

When do we have equality?

Imports (8)

Imported by 1 file

Compfiles.lean

lemma Usa1977P5.le_max_endpoint Documented declaration: le_max_endpoint line 41 source
Source documentation
If r ≥ 0 and 0 < a ≤ x ≤ b, then (r + x) * (s + 1 / x) is bounded above by the maximum of its values at the endpoints x = a and x = b (as a function of x it is a sum of rs + 1, the linear function s * x and the convex function r / x, hence it attains its maximum on [a, b] at an endpoint).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, LT.lt, HMul.hMul, HAdd.hAdd, HDiv.hDiv, Max.max
Proof uses: LT.lt.trans_le, Ne, LT.lt.ne', Eq, Or, LE.le.eq_or_lt, le_trans, le_antisymm, le_max_left, HSub.hSub, Iff.mpr, sub_pos, HPow.hPow, Nat, Eq.mpr, inferInstance, CommGroupWithZero, GroupWithZero, id, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq and 146 more
156 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma le_max_endpoint {r s a b x : ℝ} (hr : 0 ≤ r) (ha : 0 < a) (hb : 0 < b)
    (hax : a ≤ x) (hxb : x ≤ b) :
    (r + x) * (s + 1 / x) ≤ max ((r + a) * (s + 1 / a)) ((r + b) * (s + 1 / b)) := by
…
```
def Usa1977P5.cornerMax Documented declaration: cornerMax line 90 source
Source documentation
cornerMax h k r s n is the maximum, over all ways of choosing each of n further variables to be either h or k, of (r + sum of the choices) * (s + sum of the reciprocals of the choices). It is defined recursively; the leaves of the recursion are exactly the 2 ^ n "corner" values.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat
2 instances, coercions and auxiliary constants left out.
```
noncomputable def cornerMax (h k r s : ℝ) : ℕ → ℝ
  | 0 => r * s
  | n + 1 => max (cornerMax h k (r + h) (s + 1 / h) n) (cornerMax h k (r + k) (s + 1 / k) n)

/-- The product `(r + Σ f i) * (s + Σ 1 / f i)`, where each `f i ∈ [h, k]`, is bounded
above by the corresponding corner maximum. Proved by induction on `n`, applying
`le_max_endpoint` to one variable at a time. -/
```
Mentions: h, f, Usa1977P5.le_max_endpoint
lemma Usa1977P5.le_cornerMax The product (r + Σ f i) * (s + Σ 1 / f i), where each f i ∈ [h, k], is bounded above by the corresponding corner maximum line 97 source
Source documentation
The product (r + Σ f i) * (s + Σ 1 / f i), where each f i ∈ [h, k], is bounded above by the corresponding corner maximum. Proved by induction on n, applying le_max_endpoint to one variable at a time.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Nat, Fin, And, LE.le, HMul.hMul, HAdd.hAdd, Finset.sum, Finset.univ, HDiv.hDiv, Usa1977P5.cornerMax
Proof uses: Nat.recAux, Eq, Fin.sum_univ_zero, Eq.mpr, id, congrArg, add_zero, le_of_eq, rfl, Fin.succ, Finset.sum_nonneg, Membership.mem, Finset, LE.le.trans, LT.lt.le, And.left, Fin.sum_univ_succ, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast and 37 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma le_cornerMax (h k : ℝ) (hh : 0 < h) (hk : 0 < k) {n : ℕ} :
    ∀ (f : Fin n → ℝ) (_ : ∀ i, h ≤ f i ∧ f i ≤ k) (r s : ℝ) (_ : 0 ≤ r),
      (r + ∑ i, f i) * (s + ∑ i, 1 / f i) ≤ cornerMax h k r s n := by
…
```
Mentions: h, f, Usa1977P5.cornerMax
problem Usa1977P5.usa1977_p5 line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, And, LE.le, HMul.hMul, HAdd.hAdd, HDiv.hDiv, Nat, HPow.hPow, HSub.hSub, Real.sqrt
Proof uses: LT.lt.trans_le, LE.le.trans, And.left, And.right, Ne, LT.lt.ne', Eq, Eq.mpr, id, congrArg, Eq.symm, Real.sqrt_mul, div_nonneg, LT.lt.le, div_mul_div_cancel₀, div_self, Real.sqrt_one, Eq.refl, Trans.trans, Mathlib.Tactic.Ring.of_eq and 170 more
154 instances, coercions and auxiliary constants left out.

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