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

37 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2022, Problem 5

A function f : ℝ → ℝ is essentially increasing if f(s) ≤ f(t) holds whenever s ≤ t are real numbers such that f(s) ≠ 0 and f(t) ≠ 0.

Find the smallest integer k such that for any 2022 real numbers x₁, x₂, ..., x₂₀₂₂, there exist k essentially increasing functions f₁, f₂, ..., fₖ such that

f₁(n) + f₂(n) + ⋯ + fₖ(n) = xₙ

for every n = 1, 2, ..., 2022.

Imports (11)

Imported by 1 file

Compfiles.lean

def Usa2022P5.EssentiallyIncreasing A function f : ℝ → ℝ is essentially increasing if f s ≤ f t whenever s ≤ t are real numbers such that f s ≠ 0 and f t ≠ 0 line 44 source
Source documentation
A function f : ℝ → ℝ is essentially increasing if f s ≤ f t whenever s ≤ t are real numbers such that f s ≠ 0 and f t ≠ 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: LE.le, Ne, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
def EssentiallyIncreasing (f : ℝ → ℝ) : Prop :=
…
```
Mentions: f
def Usa2022P5.Good Documented declaration: Good line 50 source
Source documentation
The property of the natural number k occurring in the problem: every 2022-tuple (x₁, …, x₂₀₂₂) of real numbers is the pointwise sum of k essentially increasing functions at the points 1, …, 2022.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Fin, OfNat.ofNat, Real, Exists, And, Usa2022P5.EssentiallyIncreasing, Eq, Finset.sum, Finset.univ, HAdd.hAdd
10 instances, coercions and auxiliary constants left out.
```
def Good (k : ℕ) : Prop :=
…
```
determine Usa2022P5.solution line 55 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
lemma Usa2022P5.essentiallyIncreasing_zero The identically zero function is essentially increasing line 60 source
Source documentation
The identically zero function is essentially increasing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2022P5.EssentiallyIncreasing, OfNat.ofNat, Real
Proof uses: LE.le, Ne, False.elim, rfl
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma essentiallyIncreasing_zero : EssentiallyIncreasing (0 : ℝ → ℝ) := by
…
```
Mentions: Usa2022P5.EssentiallyIncreasing
lemma Usa2022P5.Good.mono If k functions suffice, then so do any m ≥ k functions, by padding with zero functions line 66 source
Source documentation
If k functions suffice, then so do any m ≥ k functions, by padding with zero functions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Usa2022P5.Good
Proof uses: Fin, OfNat.ofNat, Real, And, Usa2022P5.EssentiallyIncreasing, Eq, Finset.sum, Finset.univ, HAdd.hAdd, Exists, Exists.intro, dite, LT.lt, Fin.mk, Not, And.intro, id, Eq.mpr, congrArg, dite_eq_left and 20 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma Good.mono {k m : ℕ} (hkm : k ≤ m) (hk : Good k) : Good m := by
…
```
Mentions: Usa2022P5.Good
lemma Usa2022P5.not_good_ten The lower bound: ten functions do not suffice line 104 source
Source documentation
The lower bound: ten functions do not suffice. Following the official solution, take xₙ = -(n + 1). For each n the support S(n) = {i | fᵢ(n) ≠ 0} is nonempty, and there are only 2¹⁰ - 1 = 1023 < 2022 nonempty subsets of a ten-element set, so two supports coincide, contradicting the essentially increasing condition because x is strictly decreasing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Usa2022P5.Good, OfNat.ofNat, Nat
Proof uses: Fin, Real, And, Usa2022P5.EssentiallyIncreasing, Eq, Finset.sum, Finset.univ, HAdd.hAdd, Neg.neg, Exists, False, Finset, Finset.filter, Ne, rfl, Finset.Nonempty, Decidable.byContradiction, Finset.sum_eq_zero, Membership.mem, Iff.mpr and 109 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
```
lemma not_good_ten : ¬ Good 10 := by
…
```
Mentions: Usa2022P5.Good
def Usa2022P5.lvl The level of n: for n ≥ 1 this is the unique ℓ ≥ 1 with 2^(ℓ-1) ≤ n < 2^ℓ line 191 source
Source documentation
The level of n: for n ≥ 1 this is the unique ℓ ≥ 1 with 2^(ℓ-1) ≤ n < 2^ℓ.

no axioms what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, Nat.log, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
def lvl (n : ℕ) : ℕ := Nat.log 2 n + 1
```
lemma Usa2022P5.lvl_pos line 193 source
no axioms what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Usa2022P5.lvl
Proof uses: Nat.le_add_left, Nat.log
3 instances, coercions and auxiliary constants left out.
lemma Usa2022P5.pow_lvl_sub_one_le line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HPow.hPow, HSub.hSub, Usa2022P5.lvl
Proof uses: Eq, Nat.log, Nat.add_sub_cancel, Eq.mpr, id, congrArg, Nat.pow_log_le_self
17 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P5.lt_pow_lvl line 200 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, Usa2022P5.lvl
Proof uses: Nat.lt_pow_succ_log_self, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P5.lvl_le_of_le line 203 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Usa2022P5.lvl
Proof uses: Decidable.byContradiction, Not, Nat.log, HAdd.hAdd, Eq.mp, LT.lt, HPow.hPow, le_trans, Nat.pow_le_pow_right, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Nat.pow_log_le_self, congrFun', congrArg, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNatPowT.run and 5 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P5.lvl_mono line 214 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Usa2022P5.lvl
Proof uses: Nat.log, OfNat.ofNat, Nat.log_mono_right, id
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P5.lvl_eq_of_mem line 219 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HPow.hPow, OfNat.ofNat, HSub.hSub, LT.lt, Eq, Usa2022P5.lvl
Proof uses: Decidable.byContradiction, Not, False, Eq.mp, congrFun', congrArg, Eq.trans, zero_tsub, pow_zero, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.zero_le, Ne, pow_pos and 7 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
def Usa2022P5.cval The complement of n inside its level line 235 source
Source documentation
The complement of n inside its level.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: HSub.hSub, HPow.hPow, OfNat.ofNat, Usa2022P5.lvl
7 instances, coercions and auxiliary constants left out.
```
def cval (n : ℕ) : ℕ := 2 ^ lvl n - 1 - n
```
Mentions: Usa2022P5.lvl
lemma Usa2022P5.cval_lt line 237 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Usa2022P5.cval, HPow.hPow, HSub.hSub, Usa2022P5.lvl
Proof uses: Usa2022P5.pow_lvl_sub_one_le, Usa2022P5.lt_pow_lvl, Usa2022P5.lvl_pos, Eq, HMul.hMul, Eq.mpr, HAdd.hAdd, id, congrArg, Eq.symm, Nat.sub_add_cancel, pow_succ, mul_comm, Eq.refl
31 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Usa2022P5.xe Extension of the target tuple to all naturals (zero outside [1, 2022]) line 249 source
Source documentation
Extension of the target tuple to all naturals (zero outside [1, 2022]).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real
Proof uses: dite, And, LE.le, Fin.mk, HSub.hSub, Not
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def xe (x : Fin 2022 → ℝ) (m : ℕ) : ℝ :=
…
```
lemma Usa2022P5.xe_apply line 252 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Eq, Usa2022P5.xe, HAdd.hAdd
Proof uses: And, LE.le, And.intro, Nat.le_add_left, Nat.succ_le_of_lt, Fin.isLt, id, Eq.mpr, dite, Fin.mk, HSub.hSub, Not, congrArg, dite_eq_left, Eq.rec, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Usa2022P5.Bnd A constant dominating all values and all consecutive differences of xe line 261 source
Source documentation
A constant dominating all values and all consecutive differences of xe.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real
Proof uses: HAdd.hAdd, Finset.sum, Finset.range, abs, Usa2022P5.xe, HSub.hSub
12 instances, coercions and auxiliary constants left out.
```
noncomputable def Bnd (x : Fin 2022 → ℝ) : ℝ :=
…
```
lemma Usa2022P5.Bnd_pos line 264 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, LT.lt, Usa2022P5.Bnd
Proof uses: LE.le, Finset.sum, Finset.range, HAdd.hAdd, abs, Usa2022P5.xe, HSub.hSub, Finset.sum_nonneg, Membership.mem, Finset, add_nonneg, abs_nonneg, Eq, rfl, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq and 49 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P5.abs_xe_le line 270 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, LE.le, abs, Usa2022P5.xe, HSub.hSub, Usa2022P5.Bnd
Proof uses: HAdd.hAdd, Finset.sum, Finset.range, Finset.single_le_sum, Membership.mem, Finset, add_nonneg, abs_nonneg, Iff.mpr, LT.lt, Finset.mem_range, le_add_of_nonneg_right, Eq, rfl, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq and 48 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P5.abs_gap_le line 281 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, LE.le, abs, HSub.hSub, Usa2022P5.xe, HAdd.hAdd, Usa2022P5.Bnd
Proof uses: Finset.sum, Finset.range, Finset.single_le_sum, Membership.mem, Finset, add_nonneg, abs_nonneg, Iff.mpr, LT.lt, Finset.mem_range, le_add_of_nonneg_left, Eq, rfl, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 47 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Usa2022P5.gval Documented declaration: gval line 297 source
Source documentation
The value of the j-th constructed function at the integer point n: zero outside [1, 2047]; on its own level (j = lvl n - 1) it is the corrector xe x n - cval n * Bnd x, and on higher levels it is the bit contribution 2^j * Bnd x when bit j of cval n is set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real
Proof uses: ite, And, LE.le, HAdd.hAdd, Eq, Bool, Nat.testBit, Usa2022P5.cval, Bool.true, HMul.hMul, HPow.hPow, Usa2022P5.Bnd, HSub.hSub, Usa2022P5.lvl, Usa2022P5.xe
24 instances, coercions and auxiliary constants left out.
```
noncomputable def gval (x : Fin 2022 → ℝ) (j n : ℕ) : ℝ :=
…
```
lemma Usa2022P5.gval_of_mem line 303 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, And, LE.le, Eq, Usa2022P5.gval, HAdd.hAdd, ite, Bool, Nat.testBit, Usa2022P5.cval, Bool.true, HMul.hMul, HPow.hPow, Usa2022P5.Bnd, HSub.hSub, Usa2022P5.lvl, Usa2022P5.xe
Proof uses: ite_eq_left
45 instances, coercions and auxiliary constants left out.
lemma Usa2022P5.gval_of_not_mem line 309 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Not, And, LE.le, Eq, Usa2022P5.gval
Proof uses: ite_eq_right, HAdd.hAdd, ite, Bool, Nat.testBit, Usa2022P5.cval, Bool.true, HMul.hMul, HPow.hPow, Usa2022P5.Bnd, HSub.hSub, Usa2022P5.lvl, Usa2022P5.xe
27 instances, coercions and auxiliary constants left out.
lemma Usa2022P5.testBit_cval_eq_false_of_ge line 313 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HSub.hSub, Usa2022P5.lvl, Eq, Bool, Nat.testBit, Usa2022P5.cval, Bool.false
Proof uses: Nat.testBit_eq_false_of_lt, lt_of_lt_of_le, HPow.hPow, Usa2022P5.cval_lt, Nat.pow_le_pow_right, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P5.if_testBit_false line 318 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, Eq, Bool.false, Real, ite, Bool.true, OfNat.ofNat
Proof uses: ite_eq_right, Bool.false_ne_true, Eq.trans, Eq.symm
6 instances, coercions and auxiliary constants left out.
lemma Usa2022P5.if_testBit_true line 322 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, Eq, Bool.true, Real, ite, OfNat.ofNat
Proof uses: ite_eq_left
6 instances, coercions and auxiliary constants left out.
lemma Usa2022P5.gval_step_corrector Within one level, the corrector values strictly increase from m to m + 1, because Bnd x dominates the consecutive differences of xe line 329 source
Source documentation
Within one level, the corrector values strictly increase from m to m + 1, because Bnd x dominates the consecutive differences of xe.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, LE.le, Eq, HSub.hSub, Usa2022P5.lvl, HAdd.hAdd, HPow.hPow, Usa2022P5.gval
Proof uses: Usa2022P5.lvl_eq_of_mem, le_trans, Usa2022P5.pow_lvl_sub_one_le, Nat.le_add_right, lt_of_le_of_lt, Nat.sub_lt, pow_pos, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Eq.mpr, ite, Nat.testBit, Usa2022P5.cval, Bool.true, HMul.hMul, Usa2022P5.Bnd, Usa2022P5.xe and 75 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
lemma gval_step_corrector (x : Fin 2022 → ℝ) {j m : ℕ}
    (hm : 1 ≤ m) (hjm : j = lvl m - 1) (hm1 : m + 1 ≤ 2 ^ lvl m - 1)
    (hm2 : m + 1 ≤ 2047) :
    gval x j m ≤ gval x j (m + 1) := by
…
```
Mentions: Usa2022P5.lvl, Usa2022P5.gval
lemma Usa2022P5.gval_mono The constructed values are monotone at integer points (on their support); this is the heart of the essentially increasing property line 364 source
Source documentation
The constructed values are monotone at integer points (on their support); this is the heart of the essentially increasing property.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, LE.le, Ne, Usa2022P5.gval
Proof uses: le_trans, Usa2022P5.lvl, Usa2022P5.lvl_mono, Usa2022P5.lvl_pos, HSub.hSub, Decidable.byContradiction, Not, Eq, Bool, Nat.testBit, Usa2022P5.cval, Bool.false, Usa2022P5.testBit_cval_eq_false_of_ge, Eq.mp, LT.lt, HAdd.hAdd, ite, Usa2022P5.xe, HMul.hMul, Usa2022P5.Bnd and 98 more
115 instances, coercions and auxiliary constants left out.

Tactic trace: 116 steps
Open to load the checked before-and-after goal states.
```
lemma gval_mono (x : Fin 2022 → ℝ) {j ns nt : ℕ}
    (hns : 1 ≤ ns) (hle : ns ≤ nt) (htt : nt ≤ 2047)
    (hs : gval x j ns ≠ 0) (ht : gval x j nt ≠ 0) :
    gval x j ns ≤ gval x j nt := by
…
```
Mentions: Usa2022P5.gval
lemma Usa2022P5.sum_range_testBit Binary expansion: a natural number is the sum of its bit values line 465 source
Source documentation
Binary expansion: a natural number is the sum of its bit values.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, Eq, Finset.sum, Finset.range, ite, Bool, Nat.testBit, Bool.true
Proof uses: Nat.recAux, Eq.mpr, id, Eq.mp, Eq.trans, congrArg, pow_zero, of_eq_true, True, congr, EmptyCollection.emptyCollection, Finset, funext, ite_eq_right_of_eq_false, Bool.false, False, congrFun', Nat.zero_testBit, Bool.false_eq_true, Finset.sum_const_zero and 54 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma sum_range_testBit (c : ℕ) {L : ℕ} (h : c < 2 ^ L) :
    ∑ i ∈ Finset.range L, (if c.testBit i = true then 2 ^ i else 0) = c := by
…
```
Mentions: h
lemma Usa2022P5.sum_range_testBit_real Real version of the binary expansion line 498 source
Source documentation
Real version of the binary expansion.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, Eq, Real, Finset.sum, Finset.range, ite, Bool, Nat.testBit, Bool.true
Proof uses: Usa2022P5.sum_range_testBit, cast, Eq.symm, Eq.mp, congrFun', congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Eq.trans, Nat.cast_ite, ite_congr, Nat.cast_pow, Not, Nat.cast_zero, Nat.cast_sum
53 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma sum_range_testBit_real (c : ℕ) {L : ℕ} (h : c < 2 ^ L) :
    ∑ i ∈ Finset.range L, (if c.testBit i = true then (2:ℝ) ^ i else 0) = (c : ℝ) := by
…
```
Mentions: h
def Usa2022P5.ffun The j-th constructed function on the real line; it is nonzero only at the integers 1, …, 2047 line 510 source
Source documentation
The j-th constructed function on the real line; it is nonzero only at the integers 1, …, 2047.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real
Proof uses: ite, Eq, Nat.floor, Usa2022P5.gval
14 instances, coercions and auxiliary constants left out.
```
noncomputable def ffun (x : Fin 2022 → ℝ) (j : Fin 11) (t : ℝ) : ℝ :=
…
```
lemma Usa2022P5.ffun_apply_nat line 513 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Eq, Usa2022P5.ffun, Usa2022P5.gval
Proof uses: id, Eq.mpr, ite, Nat.floor, congrArg, Nat.floor_natCast, ite_eq_left, rfl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P5.ess_incr_ffun line 520 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Usa2022P5.EssentiallyIncreasing, Usa2022P5.ffun
Proof uses: LE.le, Ne, dite, Eq, Nat.floor, Usa2022P5.gval, ite_eq_left, Eq.mp, congrArg, And, Decidable.byContradiction, Not, Usa2022P5.gval_of_not_mem, Eq.mpr, id, Usa2022P5.gval_mono, And.left, Nat.floor_le_floor, And.right, absurd and 2 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma Usa2022P5.sum_ffun The sum identity: at every integer point n ∈ [1, 2047] the eleven constructed functions sum to the target value xe x n line 548 source
Source documentation
The sum identity: at every integer point n ∈ [1, 2047] the eleven constructed functions sum to the target value xe x n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, LE.le, Eq, Finset.sum, Finset.univ, Usa2022P5.ffun, Usa2022P5.xe
Proof uses: Eq.mpr, Usa2022P5.gval, id, congrArg, Finset.sum_congr, rfl, Finset, Membership.mem, Usa2022P5.ffun_apply_nat, HAdd.hAdd, ite, Bool, Nat.testBit, Usa2022P5.cval, Bool.true, HMul.hMul, HPow.hPow, Usa2022P5.Bnd, HSub.hSub, Usa2022P5.lvl and 70 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma sum_ffun (x : Fin 2022 → ℝ) {n : ℕ} (h1 : 1 ≤ n) (h2 : n ≤ 2047) :
    ∑ j : Fin 11, ffun x j (n : ℝ) = xe x n := by
…
```
Mentions: Usa2022P5.ffun, Usa2022P5.xe
lemma Usa2022P5.good_eleven Eleven functions suffice: the explicit construction works for every choice of target values line 590 source
Source documentation
Eleven functions suffice: the explicit construction works for every choice of target values.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2022P5.Good, OfNat.ofNat, Nat
Proof uses: Fin, Real, Exists.intro, And, Usa2022P5.EssentiallyIncreasing, Eq, Finset.sum, Finset.univ, HAdd.hAdd, Usa2022P5.ffun, And.intro, Usa2022P5.ess_incr_ffun, LE.le, Nat.le_add_left, le_trans, Nat.succ_le_of_lt, Fin.isLt, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 11 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma good_eleven : Good 11 := by
…
```
Mentions: Usa2022P5.Good
problem Usa2022P5.usa2022_p5 line 601 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Usa2022P5.Good, Usa2022P5.solution
Proof uses: And.intro, Membership.mem, Set, lowerBounds, Usa2022P5.good_eleven, Decidable.byContradiction, LE.le, Not, OfNat.ofNat, LT.lt, Eq.mp, Usa2022P5.not_good_ten, Usa2022P5.Good.mono
12 instances, coercions and auxiliary constants left out.

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