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

18 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2010, Problem 3

The 2010 positive real numbers $a_1, a_2, \ldots, a_{2010}$ satisfy the inequality $a_i a_j \le i + j$ for all $1 \le i < j \le 2010$. Determine, with proof, the largest possible value of the product $a_1 a_2 \cdots a_{2010}$.

Imports (2)

Imported by 1 file

Compfiles.lean

lemma Usa2010P3.prod_range_pair Split a product over Finset.range (2 * n) into a product of consecutive pairs line 44 source
Source documentation
Split a product over Finset.range (2 * n) into a product of consecutive pairs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Eq, Finset.prod, Finset.range, HMul.hMul, OfNat.ofNat, HAdd.hAdd
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, EmptyCollection.emptyCollection, Finset, MulZeroClass.mul_zero, eq_self, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 19 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma prod_range_pair (f : ℕ → ℝ) (n : ℕ) :
    ∏ i ∈ Finset.range (2 * n), f i = ∏ k ∈ Finset.range n, f (2 * k) * f (2 * k + 1) := by
…
```
Mentions: f
lemma Usa2010P3.mul_sqrt_eq_sqrt_mul For 0 ≤ C and 0 ≤ Z: C * √Z = √(C² * Z) line 54 source
Source documentation
For 0 ≤ C and 0 ≤ Z: C * √Z = √(C² * Z).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, Eq, HMul.hMul, Real.sqrt, HPow.hPow, Nat
Proof uses: Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, Real.sqrt_sq, Real.sqrt_mul, sq_nonneg
37 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma mul_sqrt_eq_sqrt_mul {C Z : ℝ} (hC : 0 ≤ C) (_hZ : 0 ≤ Z) :
    C * Real.sqrt Z = Real.sqrt (C ^ 2 * Z) := by
…
```
lemma Usa2010P3.key₁ Key inequality for the "even index, odd index" case: the difference factors as (q - p) * (4 * (p + 1) * (q + 1) - (2 * p + 1) ^ 2), which is nonnegative for 0 ≤ p ≤ q line 62 source
Source documentation
Key inequality for the "even index, odd index" case: the difference factors as (q - p) * (4 * (p + 1) * (q + 1) - (2 * p + 1) ^ 2), which is nonnegative for 0 ≤ p ≤ q.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, HMul.hMul, HPow.hPow, Nat, HAdd.hAdd
Proof uses: Eq, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 65 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma key₁ {p q : ℝ} (hp : 0 ≤ p) (hpq : p ≤ q) :
    (4 * p + 3) ^ 2 * (q + 1) ≤ (2 * p + 2 * q + 3) ^ 2 * (p + 1) := by
…
```
lemma Usa2010P3.key₂ Documented declaration: key₂ line 75 source
Source documentation
Key inequality for the "odd index, even index" case: the difference factors as (p - q) * (4 * (p + 1) * (q + 1) - (2 * q + 1) ^ 2), a product of two nonpositive factors for 0 ≤ p and p + 1 ≤ q.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat
Proof uses: Eq, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 67 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma key₂ {p q : ℝ} (hp : 0 ≤ p) (hpq : p + 1 ≤ q) :
    (4 * q + 3) ^ 2 * (p + 1) ≤ (2 * p + 2 * q + 3) ^ 2 * (q + 1) := by
…
```
lemma Usa2010P3.key₃ Key inequality for the "even index, even index" case line 88 source
Source documentation
Key inequality for the "even index, even index" case. Writing q = p + 1 + t with 0 ≤ t, the difference expands to a polynomial in p and t all of whose coefficients are positive.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat
Proof uses: And, Eq, Exists, Exists.intro, HSub.hSub, And.intro, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf and 70 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma key₃ {p q : ℝ} (hp : 0 ≤ p) (hpq : p + 1 ≤ q) :
    (4 * p + 3) ^ 2 * (4 * q + 3) ^ 2
      ≤ 64 * (p + q + 1) ^ 2 * (p + 1) * (q + 1) := by
…
```
lemma Usa2010P3.key₄ Key inequality for the "odd index, odd index" case (AM–GM) line 102 source
Source documentation
Key inequality for the "odd index, odd index" case (AM–GM).

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

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma key₄ {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    (2 * Real.sqrt x) * (2 * Real.sqrt y) ≤ 2 * x + 2 * y := by
…
```
def Usa2010P3.constr The extremal sequence (zero-based): at index 2k the value is (4k+3) / (2 * √(k+1)), and at index 2k+1 it is 2 * √(k+1) line 109 source
Source documentation
The extremal sequence (zero-based): at index 2k the value is (4k+3) / (2 * √(k+1)), and at index 2k+1 it is 2 * √(k+1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: ite, Even, HDiv.hDiv, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Real.sqrt
19 instances, coercions and auxiliary constants left out.
```
noncomputable def constr (i : ℕ) : ℝ :=
…
```
lemma Usa2010P3.constr_even line 113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Usa2010P3.constr, HMul.hMul, OfNat.ofNat, HDiv.hDiv, HAdd.hAdd, Real.sqrt
Proof uses: Even, Exists.intro, two_mul, of_eq_true, Eq.trans, True, congrFun', congrArg, ite, ite_congr, Eq.refl, congr, Not, Decidable, ite_eq_left, eq_self
40 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P3.constr_odd line 119 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Usa2010P3.constr, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Real.sqrt
Proof uses: Not, Even, Iff.mpr, Odd, Nat.not_even_iff_odd, Exists.intro, rfl, HDiv.hDiv, of_eq_true, Eq.trans, True, congrFun', congrArg, ite, ite_congr, Eq.refl, congr, Decidable, ite_eq_right, eq_self
47 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P3.constr_pos line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Real, OfNat.ofNat, Usa2010P3.constr
Proof uses: dite, Even, Eq.mpr, HDiv.hDiv, HAdd.hAdd, HMul.hMul, Real.sqrt, id, Eq, congrArg, Decidable, ite_eq_left, div_pos, Right.add_pos_of_nonneg_of_pos, mul_nonneg, le_of_lt, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo and 11 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P3.constr_pair The product of two consecutive terms is exactly 4k + 3 line 133 source
Source documentation
The product of two consecutive terms is exactly 4k + 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, HMul.hMul, Usa2010P3.constr, OfNat.ofNat, HAdd.hAdd
Proof uses: Eq.mpr, HDiv.hDiv, Real.sqrt, id, congrArg, Usa2010P3.constr_even, Usa2010P3.constr_odd, div_mul_cancel₀, ne_of_gt, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Real.sqrt_pos_of_pos, Right.add_pos_of_nonneg_of_pos, inferInstance, Zero and 3 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma constr_pair (k : ℕ) : constr (2 * k) * constr (2 * k + 1) = 4 * (k : ℝ) + 3 := by
…
```
Mentions: Usa2010P3.constr
lemma Usa2010P3.ineq_ee Validity of the construction: case both indices even line 138 source
Source documentation
Validity of the construction: case both indices even.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, HAdd.hAdd, HMul.hMul, HDiv.hDiv, Nat, Real.sqrt
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, 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 79 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma ineq_ee {p q : ℝ} (hp : 0 ≤ p) (hpq : p + 1 ≤ q) :
    (4 * p + 3) / (2 * Real.sqrt (p + 1)) * ((4 * q + 3) / (2 * Real.sqrt (q + 1)))
      ≤ (2 * p + 1) + (2 * q + 1) := by
…
```
lemma Usa2010P3.ineq_eo Validity of the construction: case even index, odd index line 153 source
Source documentation
Validity of the construction: case even index, odd index.

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

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma ineq_eo {p q : ℝ} (hp : 0 ≤ p) (hpq : p ≤ q) :
    (4 * p + 3) / (2 * Real.sqrt (p + 1)) * (2 * Real.sqrt (q + 1))
      ≤ (2 * p + 1) + (2 * q + 2) := by
…
```
lemma Usa2010P3.ineq_oe Validity of the construction: case odd index, even index line 171 source
Source documentation
Validity of the construction: case odd index, even index.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, HAdd.hAdd, HMul.hMul, Nat, Real.sqrt, HDiv.hDiv
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, 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 81 more
115 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma ineq_oe {p q : ℝ} (hp : 0 ≤ p) (hpq : p + 1 ≤ q) :
    (2 * Real.sqrt (p + 1)) * ((4 * q + 3) / (2 * Real.sqrt (q + 1)))
      ≤ (2 * p + 2) + (2 * q + 1) := by
…
```
lemma Usa2010P3.ineq_oo Validity of the construction: case both indices odd line 189 source
Source documentation
Validity of the construction: case both indices odd.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, HMul.hMul, Nat, Real.sqrt, HAdd.hAdd
Proof uses: Usa2010P3.key₄, le_of_lt, Right.add_pos_of_nonneg_of_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring and 48 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma ineq_oo {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :
    (2 * Real.sqrt (p + 1)) * (2 * Real.sqrt (q + 1)) ≤ (2 * p + 2) + (2 * q + 2) := by
…
```
lemma Usa2010P3.constr_ineq The construction satisfies aᵢaⱼ ≤ (i+1) + (j+1) for all i < j line 195 source
Source documentation
The construction satisfies aᵢaⱼ ≤ (i+1) + (j+1) for all i < j.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, LE.le, Real, HMul.hMul, Usa2010P3.constr, HAdd.hAdd, OfNat.ofNat
Proof uses: Or, Eq, Exists, Exists.intro, HDiv.hDiv, Eq.mpr, Real.sqrt, id, congrArg, Usa2010P3.constr_even, congr, congrFun', Nat.cast_mul, Usa2010P3.ineq_ee, Nat.cast_nonneg, cast, Eq.symm, Eq.trans, Nat.cast_one, le_of_not_gt and 90 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma constr_ineq {i j : ℕ} (hij : i < j) :
    constr i * constr j ≤ (i : ℝ) + 1 + ((j : ℝ) + 1) := by
…
```
Mentions: Usa2010P3.constr
determine Usa2010P3.answer line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: Finset.prod, Nat, Finset.range, OfNat.ofNat, HAdd.hAdd, HMul.hMul
11 instances, coercions and auxiliary constants left out.
problem Usa2010P3.usa2010_p3 line 227 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsGreatest, Real, Set.ofPred, Exists, Nat, And, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, HAdd.hAdd, Eq, Finset.prod, Finset.range, Usa2010P3.answer
Proof uses: And.intro, Membership.mem, Set, upperBounds, Exists.intro, Usa2010P3.constr, Usa2010P3.constr_pos, Usa2010P3.constr_ineq, Eq.mpr, id, congrArg, Usa2010P3.prod_range_pair, Finset.prod_congr, rfl, Finset, Eq.symm, Usa2010P3.constr_pair, Finset.prod_le_prod₀, Iff.mp, Finset.mem_range and 63 more
94 instances, coercions and auxiliary constants left out.

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