This record groups the data and proof fields needed for “factorial table”. A proposition-valued field is a requirement until a constructor supplies it.
structure FactorialTable (n : ℕ) where
values : Vector ℝ (n + 1)
next : ℝ
/-- Full-copy table extension, including one index comparison per output. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “extend”. Full-copy table extension, including one index comparison per output.
def extend {n : ℕ} (xs : Vector ℝ (n + 1)) (last : ℝ) : Run (Vector ℝ (n + 2)) :=
collect fun i =>
let result := if h : i.val < n + 1 then StoredGivens.read xs ⟨i.val, h⟩ else pure last
⟨result.value, tick .compare + result.cost⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “extend value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem extend_value {n : ℕ} (xs : Vector ℝ (n + 1)) (last : ℝ) (i : Fin (n + 2)) :
(extend xs last).value[i.val] = if h : i.val < n + 1 then xs[i.val] else last := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “factorials”. The next integer multiplier is itself generated by a charged addition.
noncomputable def factorials : (n : ℕ) → Run (FactorialTable n)
| 0 => do
let values ← collect (fun _ : Fin 1 => pure (1 : ℝ))
pure ⟨values, 1⟩
| n + 1 => do
let previous ← factorials n
let last ← StoredGivens.read previous.values (Fin.last n)
let value ← StoredGivens.mul previous.next last
let next ← StoredGivens.add previous.next 1
let values ← extend previous.values value
pure ⟨values, next⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “factorials next”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem factorials_next (n : ℕ) : (factorials n).value.next = (n + 1 : ℕ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “factorials value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem factorials_value (n : ℕ) (i : Fin (n + 1)) :
(factorials n).value.values[i.val] = (i.val.factorial : ℝ) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “choose from”. 'choose' uses three cached factorial entries and two field operations.
noncomputable def chooseFrom {N : ℕ} (F : Vector ℝ (N + 1)) (n r : ℕ)
(hr : r ≤ n) (hn : n ≤ N) : Run ℝ := do
let top ← StoredGivens.read F ⟨n, by omega⟩
let first ← StoredGivens.read F ⟨r, by omega⟩
let second ← StoredGivens.read F ⟨n - r, by omega⟩
let denominator ← StoredGivens.mul first second
StoredGivens.div top denominator
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “choose from value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem chooseFrom_value {N : ℕ} (F : Vector ℝ (N + 1))
(correct : ∀ i : Fin (N + 1), F[i.val] = (i.val.factorial : ℝ))
(n r : ℕ) (hr : r ≤ n) (hn : n ≤ N) :
(chooseFrom F n r hr hn).value = (n.choose r : ℝ) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “source entry”.
noncomputable def sourceEntry (k : ℕ) (F : Vector ℝ (2 * k + 2)) (i : Fin (k + 1)) : Run ℝ :=
sumEntries fun m : Fin (i.val + 1) => do
let binomial ← chooseFrom F (k + i.val - m.val) k (by omega) (by omega)
let denominator ← StoredGivens.read F ⟨m.val, by omega⟩
StoredGivens.div binomial denominator
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “source entry value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sourceEntry_value (k : ℕ) (F : Vector ℝ (2 * k + 2))
(correct : ∀ i : Fin (2 * k + 2), F[i.val] = (i.val.factorial : ℝ)) (i : Fin (k + 1)) :
(sourceEntry k F i).value = sourceCoefficient k i.val := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “sources”.
noncomputable def sources (k : ℕ) (F : Vector ℝ (2 * k + 2)) : Run (Vector ℝ (k + 1)) :=
collect (sourceEntry k F)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “sources value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sources_value (k : ℕ) (F : Vector ℝ (2 * k + 2))
(correct : ∀ i : Fin (2 * k + 2), F[i.val] = (i.val.factorial : ℝ)) (i : Fin (k + 1)) :
(sources k F).value[i.val] = sourceCoefficient k i.val := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “left term”.
noncomputable def leftTerm (k : ℕ) (F : Vector ℝ (2 * k + 2))
(a : Vector ℝ (k + 1)) (denominator : ℝ) (r : Fin (2 * k + 2))
(i : Fin (k + 1)) : Run ℝ :=
let term : Run ℝ := if h : i.val ≤ r.val ∧ r.val ≤ k then do
let coefficient ← StoredGivens.read a i
let binomial ← chooseFrom F (k - i.val) (r.val - i.val) (by omega) (by omega)
let numerator ← StoredGivens.mul coefficient binomial
StoredGivens.div numerator denominator
else pure 0
⟨term.value, 2 • tick .compare + term.cost⟩
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “left entry”.
noncomputable def leftEntry (k : ℕ) (F : Vector ℝ (2 * k + 2))
(a : Vector ℝ (k + 1)) (r : Fin (2 * k + 2)) : Run ℝ := do
let denominator ← chooseFrom F (2 * k + 1) r.val (by omega) (by omega)
sumEntries (leftTerm k F a denominator r)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “left entry value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem leftEntry_value (k : ℕ) (F : Vector ℝ (2 * k + 2))
(hF : ∀ i : Fin (2 * k + 2), F[i.val] = (i.val.factorial : ℝ))
(a : Vector ℝ (k + 1)) (ha : ∀ i : Fin (k + 1), a[i.val] = sourceCoefficient k i.val)
(r : Fin (2 * k + 2)) : (leftEntry k F a r).value = leftCoefficient k r.val := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “lefts”.
noncomputable def lefts (k : ℕ) (F : Vector ℝ (2 * k + 2)) (a : Vector ℝ (k + 1)) :
Run (Vector ℝ (2 * k + 2)) := collect (leftEntry k F a)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “lefts value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem lefts_value (k : ℕ) (F : Vector ℝ (2 * k + 2))
(hF : ∀ i : Fin (2 * k + 2), F[i.val] = (i.val.factorial : ℝ))
(a : Vector ℝ (k + 1)) (ha : ∀ i : Fin (k + 1), a[i.val] = sourceCoefficient k i.val)
(r : Fin (2 * k + 2)) : (lefts k F a).value[r.val] = leftCoefficient k r.val := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “from constant”. All shared intermediate arrays are materialized before they are consumed.
noncomputable def fromConstant (k : ℕ) (e : ℝ) : Run (Vector ℝ (2 * k + 2)) := do
let F ← factorials (2 * k + 1)
let a ← sources k F.values
let left ← lefts k F.values a
collect fun r => do
let x ← StoredGivens.read left r
let y ← StoredGivens.read left ⟨2 * k + 1 - r.val, by omega⟩
let scaled ← StoredGivens.mul e x
StoredGivens.add scaled y
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “from constant value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem fromConstant_value (k : ℕ) (e : ℝ) (r : Fin (2 * k + 2)) :
(fromConstant k e).value[r.val] = e * leftCoefficient k r.val +
leftCoefficient k (2 * k + 1 - r.val) := by
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “source run”. A proposition-valued field is a requirement until a constructor supplies it. Extra source primitive accounting, deliberately separate from 'Op'.
structure SourceRun (α : Type) where
run : Run α
exponentialCalls : ℕ
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “exponential”.
noncomputable def exponential (x : ℝ) : SourceRun ℝ := ⟨⟨Real.exp x, 0⟩, 1⟩
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “compile”.
noncomputable def compile (k : ℕ) : SourceRun (Vector ℝ (2 * k + 2)) :=
let e := exponential (-1)
let result := fromConstant k e.run.value
⟨⟨result.value, e.run.cost + result.cost⟩, e.exponentialCalls⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_value (k : ℕ) (r : Fin (2 * k + 2)) :
(compile k).run.value[r.val] = sourceBernsteinCoefficient k r.val :=
fromConstant_value k (Real.exp (-1)) r
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile nonneg”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_nonneg (k : ℕ) (r : Fin (2 * k + 2)) :
0 ≤ (compile k).run.value[r.val] := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “left coefficient pos”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem leftCoefficient_pos (k r : ℕ) (hr : r ≤ k) : 0 < leftCoefficient k r := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile pos”; the hypotheses and conclusion in the code panel fix its exact scope. Every returned source coefficient is strictly positive, including k=0.
theorem compile_pos (k : ℕ) (r : Fin (2 * k + 2)) :
0 < (compile k).run.value[r.val] := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile exponential calls”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_exponentialCalls (k : ℕ) : (compile k).exponentialCalls = 1 := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “extend cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem extend_cost_le {n : ℕ} (xs : Vector ℝ (n + 1)) (last : ℝ) (op : Op) :
(extend xs last).cost op ≤ 6 * (n + 2) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “factorials cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem factorials_cost_le (n : ℕ) (op : Op) :
(factorials n).cost op ≤ 10 * (n + 1) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “choose from cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem chooseFrom_cost {N : ℕ} (F : Vector ℝ (N + 1)) (n r : ℕ)
(hr : r ≤ n) (hn : n ≤ N) (op : Op) :
(chooseFrom F n r hr hn).cost op = 3 * tick .read op + 2 * tick .field op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “source entry cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sourceEntry_cost_le (k : ℕ) (F : Vector ℝ (2 * k + 2))
(i : Fin (k + 1)) (op : Op) : (sourceEntry k F i).cost op ≤ 8 * (k + 1) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “sources cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sources_cost_le (k : ℕ) (F : Vector ℝ (2 * k + 2)) (op : Op) :
(sources k F).cost op ≤ 12 * (k + 1) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “left term cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem leftTerm_cost_le (k : ℕ) (F : Vector ℝ (2 * k + 2))
(a : Vector ℝ (k + 1)) (denominator : ℝ) (r : Fin (2 * k + 2))
(i : Fin (k + 1)) (op : Op) : (leftTerm k F a denominator r i).cost op ≤ 10 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “left entry cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem leftEntry_cost_le (k : ℕ) (F : Vector ℝ (2 * k + 2))
(a : Vector ℝ (k + 1)) (r : Fin (2 * k + 2)) (op : Op) :
(leftEntry k F a r).cost op ≤ 16 * (k + 1) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “lefts cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem lefts_cost_le (k : ℕ) (F : Vector ℝ (2 * k + 2))
(a : Vector ℝ (k + 1)) (op : Op) : (lefts k F a).cost op ≤ 40 * (k + 1) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “from constant cost le”; the hypotheses and conclusion in the code panel fix its exact scope. Quadratic bound for every ordinary operation category of the same run.
theorem fromConstant_cost_le (k : ℕ) (e : ℝ) (op : Op) :
(fromConstant k e).cost op ≤ 108 * (k + 1) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_cost_le (k : ℕ) (op : Op) :
(compile k).run.cost op ≤ 108 * (k + 1) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. The separate exponential count is exactly one and is not in this sum.
theorem compile_total_cost_le (k : ℕ) :
StoredRectangularGivens.total (compile k).run.cost ≤ 864 * (k + 1) ^ 2 := by
commit-pinned source · Verso Blueprint panel