10.19. QuantumBlockEncoding/HermiteTransferCores.lean🔗

10 explicit public declarations, in source order.

Definition10.19.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “row features”. Monomial row features through degree 'd'.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Monomial row features through degree 'd'.

Declaration kind. def.

Source: QuantumBlockEncoding/HermiteTransferCores.lean:20. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.19.1●1 definition

defdefined in QuantumBlockEncoding/HermiteTransferCores.lean

complete

def QuantumBlockEncoding.HermiteTransferCores.rowFeatures (d : ℕ) (x : ℝ) :
  Fin (d + 1) → ℝ

def QuantumBlockEncoding.HermiteTransferCores.rowFeatures
  (d : ℕ) (x : ℝ) : Fin (d + 1) → ℝ

Monomial row features through degree `d`.

Definition10.19.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “translation core”. Explicit binomial translation core.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Explicit binomial translation core. Entries below the diagonal vanish because the corresponding binomial coefficient is zero.

Declaration kind. def.

Source: QuantumBlockEncoding/HermiteTransferCores.lean:24. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.19.2●1 definition

defdefined in QuantumBlockEncoding/HermiteTransferCores.lean

complete

def QuantumBlockEncoding.HermiteTransferCores.translationCore (d : ℕ)
  (w : ℝ) : Matrix (Fin (d + 1)) (Fin (d + 1)) ℝ

def QuantumBlockEncoding.HermiteTransferCores.translationCore
  (d : ℕ) (w : ℝ) :
  Matrix (Fin (d + 1)) (Fin (d + 1)) ℝ

Explicit binomial translation core.  Entries below the diagonal vanish
because the corresponding binomial coefficient is zero.

Theorem10.19.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “translation core below diagonal”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermiteTransferCores.lean:27. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.19.3●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteTransferCores.lean

complete

theorem QuantumBlockEncoding.HermiteTransferCores.translationCore_below_diagonal
  (d : ℕ) (w : ℝ) (i j : Fin (d + 1)) (h : ↑j < ↑i) :
  QuantumBlockEncoding.HermiteTransferCores.translationCore d w i j = 0

theorem QuantumBlockEncoding.HermiteTransferCores.translationCore_below_diagonal
  (d : ℕ) (w : ℝ) (i j : Fin (d + 1))
  (h : ↑j < ↑i) :
  QuantumBlockEncoding.HermiteTransferCores.translationCore
      d w i j =
    0

Theorem10.19.4

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The binomial theorem gives the exact single-core update.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermiteTransferCores.lean:32. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.19.4●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteTransferCores.lean

complete

theorem QuantumBlockEncoding.HermiteTransferCores.rowFeatures_translationCore
  (d : ℕ) (x w : ℝ) :
  Matrix.vecMul
      (QuantumBlockEncoding.HermiteTransferCores.rowFeatures d x)
      (QuantumBlockEncoding.HermiteTransferCores.translationCore d w) =
    QuantumBlockEncoding.HermiteTransferCores.rowFeatures d (x + w)

theorem QuantumBlockEncoding.HermiteTransferCores.rowFeatures_translationCore
  (d : ℕ) (x w : ℝ) :
  Matrix.vecMul
      (QuantumBlockEncoding.HermiteTransferCores.rowFeatures
        d x)
      (QuantumBlockEncoding.HermiteTransferCores.translationCore
        d w) =
    QuantumBlockEncoding.HermiteTransferCores.rowFeatures
      d (x + w)

The binomial theorem gives the exact single-core update.

Definition10.19.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “transfer”. Sequentially contract the explicit cores, without enumerating bit strings.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Sequentially contract the explicit cores, without enumerating bit strings.

Declaration kind. def.

Source: QuantumBlockEncoding/HermiteTransferCores.lean:51. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.19.5●1 definition

defdefined in QuantumBlockEncoding/HermiteTransferCores.lean

complete

def QuantumBlockEncoding.HermiteTransferCores.transfer (d : ℕ) :
  List ℝ → (Fin (d + 1) → ℝ) → Fin (d + 1) → ℝ

def QuantumBlockEncoding.HermiteTransferCores.transfer
  (d : ℕ) :
  List ℝ →
    (Fin (d + 1) → ℝ) → Fin (d + 1) → ℝ

Sequentially contract the explicit cores, without enumerating bit strings.

Theorem10.19.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “transfer row features”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermiteTransferCores.lean:55. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.19.6●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteTransferCores.lean

complete

theorem QuantumBlockEncoding.HermiteTransferCores.transfer_rowFeatures (d : ℕ)
  (weights : List ℝ) (origin : ℝ) :
  QuantumBlockEncoding.HermiteTransferCores.transfer d weights
      (QuantumBlockEncoding.HermiteTransferCores.rowFeatures d origin) =
    QuantumBlockEncoding.HermiteTransferCores.rowFeatures d
      (origin + weights.sum)

theorem QuantumBlockEncoding.HermiteTransferCores.transfer_rowFeatures
  (d : ℕ) (weights : List ℝ)
  (origin : ℝ) :
  QuantumBlockEncoding.HermiteTransferCores.transfer
      d weights
      (QuantumBlockEncoding.HermiteTransferCores.rowFeatures
        d origin) =
    QuantumBlockEncoding.HermiteTransferCores.rowFeatures
      d (origin + weights.sum)

Definition10.19.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “polynomial amplitude”. Contract the last bond against the polynomial's coefficient vector.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Contract the last bond against the polynomial's coefficient vector.

Declaration kind. def.

Source: QuantumBlockEncoding/HermiteTransferCores.lean:65. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.19.7●1 definition

defdefined in QuantumBlockEncoding/HermiteTransferCores.lean

complete

def QuantumBlockEncoding.HermiteTransferCores.polynomialAmplitude (d : ℕ)
  (p : Polynomial ℝ) (origin : ℝ) (weights : List ℝ) : ℝ

def QuantumBlockEncoding.HermiteTransferCores.polynomialAmplitude
  (d : ℕ) (p : Polynomial ℝ) (origin : ℝ)
  (weights : List ℝ) : ℝ

Contract the last bond against the polynomial's coefficient vector.

Theorem10.19.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “polynomial amplitude eq eval”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermiteTransferCores.lean:68. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.19.8●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteTransferCores.lean

complete

theorem QuantumBlockEncoding.HermiteTransferCores.polynomialAmplitude_eq_eval
  (d : ℕ) (p : Polynomial ℝ) (hp : p.natDegree ≤ d) (origin : ℝ)
  (weights : List ℝ) :
  QuantumBlockEncoding.HermiteTransferCores.polynomialAmplitude d p
      origin weights =
    Polynomial.eval (origin + weights.sum) p

theorem QuantumBlockEncoding.HermiteTransferCores.polynomialAmplitude_eq_eval
  (d : ℕ) (p : Polynomial ℝ)
  (hp : p.natDegree ≤ d) (origin : ℝ)
  (weights : List ℝ) :
  QuantumBlockEncoding.HermiteTransferCores.polynomialAmplitude
      d p origin weights =
    Polynomial.eval (origin + weights.sum)
      p

Theorem10.19.9

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The actual source Hermite polynomial, with no assumed interpolation data.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermiteTransferCores.lean:80. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.19.9●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteTransferCores.lean

complete

theorem QuantumBlockEncoding.HermiteTransferCores.sourceInterpolant_transfer
  (k : ℕ) (origin : ℝ) (weights : List ℝ) :
  QuantumBlockEncoding.HermiteTransferCores.polynomialAmplitude
      (2 * k + 1)
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)
      origin weights =
    Polynomial.eval (origin + weights.sum)
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)

theorem QuantumBlockEncoding.HermiteTransferCores.sourceInterpolant_transfer
  (k : ℕ) (origin : ℝ)
  (weights : List ℝ) :
  QuantumBlockEncoding.HermiteTransferCores.polynomialAmplitude
      (2 * k + 1)
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k)
      origin weights =
    Polynomial.eval (origin + weights.sum)
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k)

The actual source Hermite polynomial, with no assumed interpolation data.

Theorem10.19.10

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The exact core dimensions are linear in the interpolation order.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermiteTransferCores.lean:86. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.19.10●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteTransferCores.lean

complete

theorem QuantumBlockEncoding.HermiteTransferCores.source_transfer_dimension
  (k : ℕ) : Fintype.card (Fin (2 * k + 1 + 1)) = 2 * k + 2

theorem QuantumBlockEncoding.HermiteTransferCores.source_transfer_dimension
  (k : ℕ) :
  Fintype.card (Fin (2 * k + 1 + 1)) =
    2 * k + 2

The exact core dimensions are linear in the interpolation order.