This definition gives the library's named construction or computation for “row features”. Monomial row features through degree 'd'.
def rowFeatures (d : ℕ) (x : ℝ) : Fin (d + 1) → ℝ := fun i => x ^ i.val
/-- Explicit binomial translation core. Entries below the diagonal vanish
because the corresponding binomial coefficient is zero. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “translation core”. Explicit binomial translation core.
def translationCore (d : ℕ) (w : ℝ) : Matrix (Fin (d + 1)) (Fin (d + 1)) ℝ :=
Matrix.of fun i j => (j.val.choose i.val : ℝ) * w ^ (j.val - i.val)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “translation core below diagonal”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem translationCore_below_diagonal (d : ℕ) (w : ℝ) (i j : Fin (d + 1))
(h : j.val < i.val) : translationCore d w i j = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “row features translation core”; the hypotheses and conclusion in the code panel fix its exact scope. The binomial theorem gives the exact single-core update.
theorem rowFeatures_translationCore (d : ℕ) (x w : ℝ) :
rowFeatures d x ᵥ* translationCore d w = rowFeatures d (x + w) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “transfer”. Sequentially contract the explicit cores, without enumerating bit strings.
def transfer (d : ℕ) : List ℝ → (Fin (d + 1) → ℝ) → (Fin (d + 1) → ℝ)
| [], v => v
| w :: ws, v => transfer d ws (v ᵥ* translationCore d w)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “transfer row features”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem transfer_rowFeatures (d : ℕ) (weights : List ℝ) (origin : ℝ) :
transfer d weights (rowFeatures d origin) = rowFeatures d (origin + weights.sum) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “polynomial amplitude”. Contract the last bond against the polynomial's coefficient vector.
def polynomialAmplitude (d : ℕ) (p : Polynomial ℝ) (origin : ℝ) (weights : List ℝ) : ℝ :=
transfer d weights (rowFeatures d origin) ⬝ᵥ fun i => p.coeff i.val
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “polynomial amplitude eq eval”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem polynomialAmplitude_eq_eval (d : ℕ) (p : Polynomial ℝ)
(hp : p.natDegree ≤ d) (origin : ℝ) (weights : List ℝ) :
polynomialAmplitude d p origin weights = p.eval (origin + weights.sum) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “source interpolant transfer”; the hypotheses and conclusion in the code panel fix its exact scope. The actual source Hermite polynomial, with no assumed interpolation data.
theorem sourceInterpolant_transfer (k : ℕ) (origin : ℝ) (weights : List ℝ) :
polynomialAmplitude (2 * k + 1) (HermitePolynomial.sourceInterpolant k) origin weights =
(HermitePolynomial.sourceInterpolant k).eval (origin + weights.sum) :=
polynomialAmplitude_eq_eval _ _ (HermitePolynomial.sourceInterpolant_degree k) _ _
/-- The exact core dimensions are linear in the interpolation order. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “source transfer dimension”; the hypotheses and conclusion in the code panel fix its exact scope. The exact core dimensions are linear in the interpolation order.
theorem source_transfer_dimension (k : ℕ) : Fintype.card (Fin ((2 * k + 1) + 1)) =
2 * k + 2 := by simp
commit-pinned source · Verso Blueprint panel