10.13. QuantumBlockEncoding/HermitePolynomial.lean🔗

47 explicit public declarations, in source order.

Definition10.13.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “jet polynomial”. The truncated Taylor polynomial with the prescribed ordinary derivatives.

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. The truncated Taylor polynomial with the prescribed ordinary derivatives.

Declaration kind. def.

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

Lean code for Definition10.13.1●1 definition

defdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

def QuantumBlockEncoding.HermitePolynomial.jetPolynomial (a : ℝ) (k : ℕ)
  (v : ℕ → ℝ) : Polynomial ℝ

def QuantumBlockEncoding.HermitePolynomial.jetPolynomial
  (a : ℝ) (k : ℕ) (v : ℕ → ℝ) :
  Polynomial ℝ

The truncated Taylor polynomial with the prescribed ordinary derivatives.

Theorem10.13.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval iterate derivative”; the hypotheses and conclusion in the code panel fix its exact scope. Convert Taylor coefficients to ordinary iterated derivatives.

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. Convert Taylor coefficients to ordinary iterated derivatives.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermitePolynomial.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.13.2●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.eval_iterate_derivative
  (p : Polynomial ℝ) (a : ℝ) (j : ℕ) :
  Polynomial.eval a ((⇑Polynomial.derivative)^[j] p) =
    ↑j.factorial * ((Polynomial.taylor a) p).coeff j

theorem QuantumBlockEncoding.HermitePolynomial.eval_iterate_derivative
  (p : Polynomial ℝ) (a : ℝ) (j : ℕ) :
  Polynomial.eval a
      ((⇑Polynomial.derivative)^[j] p) =
    ↑j.factorial *
      ((Polynomial.taylor a) p).coeff j

Convert Taylor coefficients to ordinary iterated derivatives.

Theorem10.13.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “jet polynomial jet”; the hypotheses and conclusion in the code panel fix its exact scope. Every requested jet is realized by its local Taylor polynomial.

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. Every requested jet is realized by its local Taylor polynomial.

Declaration kind. theorem.

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

Lean code for Theorem10.13.3●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.jetPolynomial_jet (a : ℝ)
  (k j : ℕ) (v : ℕ → ℝ) (hj : j ≤ k) :
  Polynomial.eval a
      ((⇑Polynomial.derivative)^[j]
        (QuantumBlockEncoding.HermitePolynomial.jetPolynomial a k v)) =
    v j

theorem QuantumBlockEncoding.HermitePolynomial.jetPolynomial_jet
  (a : ℝ) (k j : ℕ) (v : ℕ → ℝ)
  (hj : j ≤ k) :
  Polynomial.eval a
      ((⇑Polynomial.derivative)^[j]
        (QuantumBlockEncoding.HermitePolynomial.jetPolynomial
          a k v)) =
    v j

Every requested jet is realized by its local Taylor polynomial.

Theorem10.13.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “jet eq of pow dvd sub”; the hypotheses and conclusion in the code panel fix its exact scope. A high-multiplicity zero preserves all derivatives below the multiplicity.

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. A high-multiplicity zero preserves all derivatives below the multiplicity.

Declaration kind. theorem.

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

Lean code for Theorem10.13.4●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.jet_eq_of_pow_dvd_sub
  (p q : Polynomial ℝ) (a : ℝ) (k j : ℕ) (hj : j ≤ k)
  (h : (Polynomial.X - Polynomial.C a) ^ (k + 1) ∣ p - q) :
  Polynomial.eval a ((⇑Polynomial.derivative)^[j] p) =
    Polynomial.eval a ((⇑Polynomial.derivative)^[j] q)

theorem QuantumBlockEncoding.HermitePolynomial.jet_eq_of_pow_dvd_sub
  (p q : Polynomial ℝ) (a : ℝ) (k j : ℕ)
  (hj : j ≤ k)
  (h :
    (Polynomial.X - Polynomial.C a) ^
        (k + 1) ∣
      p - q) :
  Polynomial.eval a
      ((⇑Polynomial.derivative)^[j] p) =
    Polynomial.eval a
      ((⇑Polynomial.derivative)^[j] q)

A high-multiplicity zero preserves all derivatives below the multiplicity.

Definition10.13.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “bezout normalizer”. The inverse constant that normalizes the extended-gcd identity.

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. The inverse constant that normalizes the extended-gcd identity.

Declaration kind. def.

Source: QuantumBlockEncoding/HermitePolynomial.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.13.5●1 definition

defdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

def QuantumBlockEncoding.HermitePolynomial.bezoutNormalizer
  (A B : Polynomial ℝ) : Polynomial ℝ

def QuantumBlockEncoding.HermitePolynomial.bezoutNormalizer
  (A B : Polynomial ℝ) : Polynomial ℝ

The inverse constant that normalizes the extended-gcd identity.

Theorem10.13.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “bezout normalizer gcd”; 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/HermitePolynomial.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.13.6●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.bezoutNormalizer_gcd
  (A B : Polynomial ℝ) (h : IsCoprime A B) :
  QuantumBlockEncoding.HermitePolynomial.bezoutNormalizer A B *
      EuclideanDomain.gcd A B =
    1

theorem QuantumBlockEncoding.HermitePolynomial.bezoutNormalizer_gcd
  (A B : Polynomial ℝ)
  (h : IsCoprime A B) :
  QuantumBlockEncoding.HermitePolynomial.bezoutNormalizer
        A B *
      EuclideanDomain.gcd A B =
    1

Definition10.13.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “two point interpolant”. An explicit Chinese-remainder interpolant, using extended Euclid.

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. An explicit Chinese-remainder interpolant, using extended Euclid.

Declaration kind. def.

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

Lean code for Definition10.13.7●1 definition

defdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

def QuantumBlockEncoding.HermitePolynomial.twoPointInterpolant
  (A B u v : Polynomial ℝ) : Polynomial ℝ

def QuantumBlockEncoding.HermitePolynomial.twoPointInterpolant
  (A B u v : Polynomial ℝ) : Polynomial ℝ

An explicit Chinese-remainder interpolant, using extended Euclid.

Theorem10.13.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “two point interpolant left”; 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/HermitePolynomial.lean:83. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.8●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.twoPointInterpolant_left
  (A B u v : Polynomial ℝ) (h : IsCoprime A B) :
  A ∣
    QuantumBlockEncoding.HermitePolynomial.twoPointInterpolant A B u v -
      u

theorem QuantumBlockEncoding.HermitePolynomial.twoPointInterpolant_left
  (A B u v : Polynomial ℝ)
  (h : IsCoprime A B) :
  A ∣
    QuantumBlockEncoding.HermitePolynomial.twoPointInterpolant
        A B u v -
      u

Theorem10.13.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “two point interpolant right”; 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/HermitePolynomial.lean:101. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.9●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.twoPointInterpolant_right
  (A B u v : Polynomial ℝ) (h : IsCoprime A B) :
  B ∣
    QuantumBlockEncoding.HermitePolynomial.twoPointInterpolant A B u v -
      v

theorem QuantumBlockEncoding.HermitePolynomial.twoPointInterpolant_right
  (A B u v : Polynomial ℝ)
  (h : IsCoprime A B) :
  B ∣
    QuantumBlockEncoding.HermitePolynomial.twoPointInterpolant
        A B u v -
      v

Definition10.13.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “left modulus”. The multiplicity polynomial for the endpoint '-1'.

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. The multiplicity polynomial for the endpoint '-1'.

Declaration kind. def.

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

Lean code for Definition10.13.10●1 definition

defdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

def QuantumBlockEncoding.HermitePolynomial.leftModulus (k : ℕ) :
  Polynomial ℝ

def QuantumBlockEncoding.HermitePolynomial.leftModulus
  (k : ℕ) : Polynomial ℝ

The multiplicity polynomial for the endpoint `-1`.

Definition10.13.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “right modulus”. The multiplicity polynomial for the endpoint '0'.

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. The multiplicity polynomial for the endpoint '0'.

Declaration kind. def.

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

Lean code for Definition10.13.11●1 definition

defdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

def QuantumBlockEncoding.HermitePolynomial.rightModulus (k : ℕ) :
  Polynomial ℝ

def QuantumBlockEncoding.HermitePolynomial.rightModulus
  (k : ℕ) : Polynomial ℝ

The multiplicity polynomial for the endpoint `0`.

Theorem10.13.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “endpoint moduli coprime”; 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/HermitePolynomial.lean:125. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.12●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.endpointModuli_coprime (k : ℕ) :
  IsCoprime (QuantumBlockEncoding.HermitePolynomial.leftModulus k)
    (QuantumBlockEncoding.HermitePolynomial.rightModulus k)

theorem QuantumBlockEncoding.HermitePolynomial.endpointModuli_coprime
  (k : ℕ) :
  IsCoprime
    (QuantumBlockEncoding.HermitePolynomial.leftModulus
      k)
    (QuantumBlockEncoding.HermitePolynomial.rightModulus
      k)

Definition10.13.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “interpolant”. The degree-bounded polynomial joining the jets of 'exp p' and 'exp (-p)'.

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. The degree-bounded polynomial joining the jets of 'exp p' and 'exp (-p)'.

Declaration kind. def.

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

Lean code for Definition10.13.13●1 definition

defdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

def QuantumBlockEncoding.HermitePolynomial.interpolant (k : ℕ) :
  Polynomial ℝ

def QuantumBlockEncoding.HermitePolynomial.interpolant
  (k : ℕ) : Polynomial ℝ

The degree-bounded polynomial joining the jets of `exp p` and `exp (-p)`.

Theorem10.13.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “interpolant left jet”; the hypotheses and conclusion in the code panel fix its exact scope. All derivatives through order 'k' at '-1' equal 'exp (-1)'.

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. All derivatives through order 'k' at '-1' equal 'exp (-1)'.

Declaration kind. theorem.

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

Lean code for Theorem10.13.14●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.interpolant_left_jet (k j : ℕ)
  (hj : j ≤ k) :
  Polynomial.eval (-1)
      ((⇑Polynomial.derivative)^[j]
        (QuantumBlockEncoding.HermitePolynomial.interpolant k)) =
    Real.exp (-1)

theorem QuantumBlockEncoding.HermitePolynomial.interpolant_left_jet
  (k j : ℕ) (hj : j ≤ k) :
  Polynomial.eval (-1)
      ((⇑Polynomial.derivative)^[j]
        (QuantumBlockEncoding.HermitePolynomial.interpolant
          k)) =
    Real.exp (-1)

All derivatives through order `k` at `-1` equal `exp (-1)`.

Theorem10.13.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “interpolant right jet”; the hypotheses and conclusion in the code panel fix its exact scope. All derivatives through order 'k' at '0' equal '(-1)^j'.

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. All derivatives through order 'k' at '0' equal '(-1)^j'.

Declaration kind. theorem.

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

Lean code for Theorem10.13.15●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.interpolant_right_jet (k j : ℕ)
  (hj : j ≤ k) :
  Polynomial.eval 0
      ((⇑Polynomial.derivative)^[j]
        (QuantumBlockEncoding.HermitePolynomial.interpolant k)) =
    (-1) ^ j

theorem QuantumBlockEncoding.HermitePolynomial.interpolant_right_jet
  (k j : ℕ) (hj : j ≤ k) :
  Polynomial.eval 0
      ((⇑Polynomial.derivative)^[j]
        (QuantumBlockEncoding.HermitePolynomial.interpolant
          k)) =
    (-1) ^ j

All derivatives through order `k` at `0` equal `(-1)^j`.

Theorem10.13.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “interpolant degree”; the hypotheses and conclusion in the code panel fix its exact scope. The construction has the minimal Hermite degree bound.

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 construction has the minimal Hermite degree bound.

Declaration kind. theorem.

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

Lean code for Theorem10.13.16●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.interpolant_degree (k : ℕ) :
  (QuantumBlockEncoding.HermitePolynomial.interpolant k).natDegree ≤
    2 * k + 1

theorem QuantumBlockEncoding.HermitePolynomial.interpolant_degree
  (k : ℕ) :
  (QuantumBlockEncoding.HermitePolynomial.interpolant
        k).natDegree ≤
    2 * k + 1

The construction has the minimal Hermite degree bound.

Definition10.13.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “coefficient series”. The generating series whose first 'k+1' coefficients are the source's 'a_{k,r}'.

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. The generating series whose first 'k+1' coefficients are the source's 'a_{k,r}'.

Declaration kind. def.

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

Lean code for Definition10.13.17●1 definition

defdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

def QuantumBlockEncoding.HermitePolynomial.coefficientSeries (k : ℕ) :
  PowerSeries ℝ

def QuantumBlockEncoding.HermitePolynomial.coefficientSeries
  (k : ℕ) : PowerSeries ℝ

The generating series whose first `k+1` coefficients are the source's `a_{k,r}`.

Definition10.13.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “coefficient polynomial”. The exact polynomial 'A_k', implemented as a finite Taylor truncation.

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. The exact polynomial 'A_k', implemented as a finite Taylor truncation.

Declaration kind. def.

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

Lean code for Definition10.13.18●1 definition

defdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

def QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial (k : ℕ) :
  Polynomial ℝ

def QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial
  (k : ℕ) : Polynomial ℝ

The exact polynomial `A_k`, implemented as a finite Taylor truncation.

Definition10.13.19

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “endpoint factor”. One endpoint cardinal factor in the symmetric closed-form Hermite formula.

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. One endpoint cardinal factor in the symmetric closed-form Hermite formula.

Declaration kind. def.

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

Lean code for Definition10.13.19●1 definition

defdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

def QuantumBlockEncoding.HermitePolynomial.endpointFactor (k : ℕ) :
  Polynomial ℝ

def QuantumBlockEncoding.HermitePolynomial.endpointFactor
  (k : ℕ) : Polynomial ℝ

One endpoint cardinal factor in the symmetric closed-form Hermite formula.

Definition10.13.20

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “source interpolant”. The source closed form, in the coordinate 't = p + 1'.

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. The source closed form, in the coordinate 't = p + 1'.

Declaration kind. def.

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

Lean code for Definition10.13.20●1 definition

defdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

def QuantumBlockEncoding.HermitePolynomial.sourceInterpolant (k : ℕ) :
  Polynomial ℝ

def QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
  (k : ℕ) : Polynomial ℝ

The source closed form, in the coordinate `t = p + 1`.

Theorem10.13.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “coefficient series coeff”; 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/HermitePolynomial.lean:184. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.21●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.coefficientSeries_coeff
  (k r : ℕ) :
  (PowerSeries.coeff r)
      (QuantumBlockEncoding.HermitePolynomial.coefficientSeries k) =
    ∑ m ∈ Finset.range (r + 1), ↑((k + r - m).choose k) / ↑m.factorial

theorem QuantumBlockEncoding.HermitePolynomial.coefficientSeries_coeff
  (k r : ℕ) :
  (PowerSeries.coeff r)
      (QuantumBlockEncoding.HermitePolynomial.coefficientSeries
        k) =
    ∑ m ∈ Finset.range (r + 1),
      ↑((k + r - m).choose k) /
        ↑m.factorial

Theorem10.13.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “coefficient series coeff nonneg”; 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/HermitePolynomial.lean:197. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.22●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.coefficientSeries_coeff_nonneg
  (k r : ℕ) :
  0 ≤
    (PowerSeries.coeff r)
      (QuantumBlockEncoding.HermitePolynomial.coefficientSeries k)

theorem QuantumBlockEncoding.HermitePolynomial.coefficientSeries_coeff_nonneg
  (k r : ℕ) :
  0 ≤
    (PowerSeries.coeff r)
      (QuantumBlockEncoding.HermitePolynomial.coefficientSeries
        k)

Theorem10.13.23

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “coefficient series coeff zero”; 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/HermitePolynomial.lean:202. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.23●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.coefficientSeries_coeff_zero
  (k : ℕ) :
  (PowerSeries.coeff 0)
      (QuantumBlockEncoding.HermitePolynomial.coefficientSeries k) =
    1

theorem QuantumBlockEncoding.HermitePolynomial.coefficientSeries_coeff_zero
  (k : ℕ) :
  (PowerSeries.coeff 0)
      (QuantumBlockEncoding.HermitePolynomial.coefficientSeries
        k) =
    1

Theorem10.13.24

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “endpoint factor series trunc”; 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/HermitePolynomial.lean:206. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.24●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.endpointFactor_series_trunc
  (k : ℕ) :
  (PowerSeries.trunc (k + 1))
      ↑(QuantumBlockEncoding.HermitePolynomial.endpointFactor k) =
    (PowerSeries.trunc (k + 1)) (PowerSeries.exp ℝ)

theorem QuantumBlockEncoding.HermitePolynomial.endpointFactor_series_trunc
  (k : ℕ) :
  (PowerSeries.trunc (k + 1))
      ↑(QuantumBlockEncoding.HermitePolynomial.endpointFactor
          k) =
    (PowerSeries.trunc (k + 1))
      (PowerSeries.exp ℝ)

Theorem10.13.25

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “endpoint factor coeff”; 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/HermitePolynomial.lean:217. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.25●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.endpointFactor_coeff (k j : ℕ)
  (hj : j ≤ k) :
  (QuantumBlockEncoding.HermitePolynomial.endpointFactor k).coeff j =
    1 / ↑j.factorial

theorem QuantumBlockEncoding.HermitePolynomial.endpointFactor_coeff
  (k j : ℕ) (hj : j ≤ k) :
  (QuantumBlockEncoding.HermitePolynomial.endpointFactor
          k).coeff
      j =
    1 / ↑j.factorial

Theorem10.13.26

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “endpoint factor zero jet”; 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/HermitePolynomial.lean:222. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.26●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.endpointFactor_zero_jet (k j : ℕ)
  (hj : j ≤ k) :
  Polynomial.eval 0
      ((⇑Polynomial.derivative)^[j]
        (QuantumBlockEncoding.HermitePolynomial.endpointFactor k)) =
    1

theorem QuantumBlockEncoding.HermitePolynomial.endpointFactor_zero_jet
  (k j : ℕ) (hj : j ≤ k) :
  Polynomial.eval 0
      ((⇑Polynomial.derivative)^[j]
        (QuantumBlockEncoding.HermitePolynomial.endpointFactor
          k)) =
    1

Theorem10.13.27

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “endpoint factor one jet”; 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/HermitePolynomial.lean:227. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.27●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.endpointFactor_one_jet (k j : ℕ)
  (hj : j ≤ k) :
  Polynomial.eval 1
      ((⇑Polynomial.derivative)^[j]
        (QuantumBlockEncoding.HermitePolynomial.endpointFactor k)) =
    0

theorem QuantumBlockEncoding.HermitePolynomial.endpointFactor_one_jet
  (k j : ℕ) (hj : j ≤ k) :
  Polynomial.eval 1
      ((⇑Polynomial.derivative)^[j]
        (QuantumBlockEncoding.HermitePolynomial.endpointFactor
          k)) =
    0

Theorem10.13.28

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “source interpolant left jet”; 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/HermitePolynomial.lean:237. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.28●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_left_jet
  (k j : ℕ) (hj : j ≤ k) :
  Polynomial.eval (-1)
      ((⇑Polynomial.derivative)^[j]
        (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)) =
    Real.exp (-1)

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_left_jet
  (k j : ℕ) (hj : j ≤ k) :
  Polynomial.eval (-1)
      ((⇑Polynomial.derivative)^[j]
        (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
          k)) =
    Real.exp (-1)

Theorem10.13.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “source interpolant right jet”; 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/HermitePolynomial.lean:246. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.29●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_right_jet
  (k j : ℕ) (hj : j ≤ k) :
  Polynomial.eval 0
      ((⇑Polynomial.derivative)^[j]
        (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)) =
    (-1) ^ j

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_right_jet
  (k j : ℕ) (hj : j ≤ k) :
  Polynomial.eval 0
      ((⇑Polynomial.derivative)^[j]
        (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
          k)) =
    (-1) ^ j

Theorem10.13.30

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “coefficient polynomial pos”; 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/HermitePolynomial.lean:254. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.30●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial_pos (k : ℕ)
  (t : ℝ) (ht : 0 ≤ t) :
  0 <
    Polynomial.eval t
      (QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial k)

theorem QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial_pos
  (k : ℕ) (t : ℝ) (ht : 0 ≤ t) :
  0 <
    Polynomial.eval t
      (QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial
        k)

Theorem10.13.31

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “source interpolant pos”; 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/HermitePolynomial.lean:267. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.31●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_pos (k : ℕ)
  (p : ℝ) (hp : p ∈ Set.Icc (-1) 0) :
  0 <
    Polynomial.eval p
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_pos
  (k : ℕ) (p : ℝ)
  (hp : p ∈ Set.Icc (-1) 0) :
  0 <
    Polynomial.eval p
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k)

Theorem10.13.32

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “coefficient polynomial eval”; the hypotheses and conclusion in the code panel fix its exact scope. The coefficient polynomial is exactly the finite sum in the closed form.

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 coefficient polynomial is exactly the finite sum in the closed form.

Declaration kind. theorem.

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

Lean code for Theorem10.13.32●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial_eval
  (k : ℕ) (t : ℝ) :
  Polynomial.eval t
      (QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial k) =
    ∑ r ∈ Finset.range (k + 1),
      (∑ m ∈ Finset.range (r + 1),
          ↑((k + r - m).choose k) / ↑m.factorial) *
        t ^ r

theorem QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial_eval
  (k : ℕ) (t : ℝ) :
  Polynomial.eval t
      (QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial
        k) =
    ∑ r ∈ Finset.range (k + 1),
      (∑ m ∈ Finset.range (r + 1),
          ↑((k + r - m).choose k) /
            ↑m.factorial) *
        t ^ r

The coefficient polynomial is exactly the finite sum in the closed form.

Theorem10.13.33

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “source interpolant eval”; the hypotheses and conclusion in the code panel fix its exact scope. Source formula with the coordinate convention 't = p + 1' made explicit.

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. Source formula with the coordinate convention 't = p + 1' made explicit.

Declaration kind. theorem.

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

Lean code for Theorem10.13.33●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_eval (k : ℕ)
  (p : ℝ) :
  Polynomial.eval p
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k) =
    Real.exp (-1) * (1 - (p + 1)) ^ (k + 1) *
        Polynomial.eval (p + 1)
          (QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial
            k) +
      (p + 1) ^ (k + 1) *
        Polynomial.eval (1 - (p + 1))
          (QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial
            k)

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_eval
  (k : ℕ) (p : ℝ) :
  Polynomial.eval p
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k) =
    Real.exp (-1) *
          (1 - (p + 1)) ^ (k + 1) *
        Polynomial.eval (p + 1)
          (QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial
            k) +
      (p + 1) ^ (k + 1) *
        Polynomial.eval (1 - (p + 1))
          (QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial
            k)

Source formula with the coordinate convention `t = p + 1` made explicit.

Theorem10.13.34

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “coefficient polynomial degree”; 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/HermitePolynomial.lean:310. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.34●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial_degree
  (k : ℕ) :
  (QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial
        k).natDegree ≤
    k

theorem QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial_degree
  (k : ℕ) :
  (QuantumBlockEncoding.HermitePolynomial.coefficientPolynomial
        k).natDegree ≤
    k

Theorem10.13.35

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “endpoint factor degree”; 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/HermitePolynomial.lean:313. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.35●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.endpointFactor_degree (k : ℕ) :
  (QuantumBlockEncoding.HermitePolynomial.endpointFactor k).natDegree ≤
    2 * k + 1

theorem QuantumBlockEncoding.HermitePolynomial.endpointFactor_degree
  (k : ℕ) :
  (QuantumBlockEncoding.HermitePolynomial.endpointFactor
        k).natDegree ≤
    2 * k + 1

Theorem10.13.36

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “source interpolant degree”; the hypotheses and conclusion in the code panel fix its exact scope. The source closed form has degree at most '2k+1'.

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 closed form has degree at most '2k+1'.

Declaration kind. theorem.

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

Lean code for Theorem10.13.36●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_degree
  (k : ℕ) :
  (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k).natDegree ≤
    2 * k + 1

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_degree
  (k : ℕ) :
  (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k).natDegree ≤
    2 * k + 1

The source closed form has degree at most `2k+1`.

Theorem10.13.37

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “iterated deriv polynomial”; the hypotheses and conclusion in the code panel fix its exact scope. Algebraic and analytic repeated differentiation agree for real polynomials.

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. Algebraic and analytic repeated differentiation agree for real polynomials.

Declaration kind. theorem.

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

Lean code for Theorem10.13.37●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.iteratedDeriv_polynomial
  (p : Polynomial ℝ) (j : ℕ) (x : ℝ) :
  iteratedDeriv j (fun y => Polynomial.eval y p) x =
    Polynomial.eval x ((⇑Polynomial.derivative)^[j] p)

theorem QuantumBlockEncoding.HermitePolynomial.iteratedDeriv_polynomial
  (p : Polynomial ℝ) (j : ℕ) (x : ℝ) :
  iteratedDeriv j
      (fun y => Polynomial.eval y p) x =
    Polynomial.eval x
      ((⇑Polynomial.derivative)^[j] p)

Algebraic and analytic repeated differentiation agree for real polynomials.

Theorem10.13.38

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “source interpolant left iterated deriv”; 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/HermitePolynomial.lean:346. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.38●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_left_iteratedDeriv
  (k j : ℕ) (hj : j ≤ k) :
  iteratedDeriv j
      (fun p =>
        Polynomial.eval p
          (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k))
      (-1) =
    Real.exp (-1)

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_left_iteratedDeriv
  (k j : ℕ) (hj : j ≤ k) :
  iteratedDeriv j
      (fun p =>
        Polynomial.eval p
          (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
            k))
      (-1) =
    Real.exp (-1)

Theorem10.13.39

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “source interpolant right iterated deriv”; 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/HermitePolynomial.lean:351. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.39●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_right_iteratedDeriv
  (k j : ℕ) (hj : j ≤ k) :
  iteratedDeriv j
      (fun p =>
        Polynomial.eval p
          (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k))
      0 =
    (-1) ^ j

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_right_iteratedDeriv
  (k j : ℕ) (hj : j ≤ k) :
  iteratedDeriv j
      (fun p =>
        Polynomial.eval p
          (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
            k))
      0 =
    (-1) ^ j

Definition10.13.40

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “smooth initial”. The literal piecewise initial datum: left exponential, Hermite bridge, right exponential.

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. The literal piecewise initial datum: left exponential, Hermite bridge, right exponential.

Declaration kind. def.

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

Lean code for Definition10.13.40●1 definition

defdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

def QuantumBlockEncoding.HermitePolynomial.smoothInitial (k : ℕ) (p : ℝ) : ℝ

def QuantumBlockEncoding.HermitePolynomial.smoothInitial
  (k : ℕ) (p : ℝ) : ℝ

The literal piecewise initial datum: left exponential, Hermite bridge, right exponential.

Theorem10.13.41

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “smooth initial left”; 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/HermitePolynomial.lean:361. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.41●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.smoothInitial_left (k : ℕ)
  (p : ℝ) (hp : p < -1) :
  QuantumBlockEncoding.HermitePolynomial.smoothInitial k p = Real.exp p

theorem QuantumBlockEncoding.HermitePolynomial.smoothInitial_left
  (k : ℕ) (p : ℝ) (hp : p < -1) :
  QuantumBlockEncoding.HermitePolynomial.smoothInitial
      k p =
    Real.exp p

Theorem10.13.42

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “smooth initial middle”; 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/HermitePolynomial.lean:364. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.42●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.smoothInitial_middle (k : ℕ)
  (p : ℝ) (hp : p ∈ Set.Icc (-1) 0) :
  QuantumBlockEncoding.HermitePolynomial.smoothInitial k p =
    Polynomial.eval p
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)

theorem QuantumBlockEncoding.HermitePolynomial.smoothInitial_middle
  (k : ℕ) (p : ℝ)
  (hp : p ∈ Set.Icc (-1) 0) :
  QuantumBlockEncoding.HermitePolynomial.smoothInitial
      k p =
    Polynomial.eval p
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k)

Theorem10.13.43

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “smooth initial right”; 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/HermitePolynomial.lean:368. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.13.43●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.smoothInitial_right (k : ℕ)
  (p : ℝ) (hp : 0 < p) :
  QuantumBlockEncoding.HermitePolynomial.smoothInitial k p =
    Real.exp (-p)

theorem QuantumBlockEncoding.HermitePolynomial.smoothInitial_right
  (k : ℕ) (p : ℝ) (hp : 0 < p) :
  QuantumBlockEncoding.HermitePolynomial.smoothInitial
      k p =
    Real.exp (-p)

Theorem10.13.44

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “smooth initial pos”; the hypotheses and conclusion in the code panel fix its exact scope. Strict positivity holds globally and makes every finite sampled norm nonzero.

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. Strict positivity holds globally and makes every finite sampled norm nonzero.

Declaration kind. theorem.

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

Lean code for Theorem10.13.44●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.smoothInitial_pos (k : ℕ)
  (p : ℝ) : 0 < QuantumBlockEncoding.HermitePolynomial.smoothInitial k p

theorem QuantumBlockEncoding.HermitePolynomial.smoothInitial_pos
  (k : ℕ) (p : ℝ) :
  0 <
    QuantumBlockEncoding.HermitePolynomial.smoothInitial
      k p

Strict positivity holds globally and makes every finite sampled norm nonzero.

Theorem10.13.45

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pow dvd sub of jet eq”; the hypotheses and conclusion in the code panel fix its exact scope. Agreement of a finite jet is equivalent to divisibility by the endpoint multiplicity.

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. Agreement of a finite jet is equivalent to divisibility by the endpoint multiplicity.

Declaration kind. theorem.

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

Lean code for Theorem10.13.45●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.pow_dvd_sub_of_jet_eq
  (p q : Polynomial ℝ) (a : ℝ) (k : ℕ)
  (h :
    ∀ j ≤ k,
      Polynomial.eval a ((⇑Polynomial.derivative)^[j] p) =
        Polynomial.eval a ((⇑Polynomial.derivative)^[j] q)) :
  (Polynomial.X - Polynomial.C a) ^ (k + 1) ∣ p - q

theorem QuantumBlockEncoding.HermitePolynomial.pow_dvd_sub_of_jet_eq
  (p q : Polynomial ℝ) (a : ℝ) (k : ℕ)
  (h :
    ∀ j ≤ k,
      Polynomial.eval a
          ((⇑Polynomial.derivative)^[j]
            p) =
        Polynomial.eval a
          ((⇑Polynomial.derivative)^[j]
            q)) :
  (Polynomial.X - Polynomial.C a) ^
      (k + 1) ∣
    p - q

Agreement of a finite jet is equivalent to divisibility by the endpoint multiplicity.

Theorem10.13.46

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “source interpolant unique”; the hypotheses and conclusion in the code panel fix its exact scope. There is only one degree-bounded polynomial with the source endpoint jets.

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. There is only one degree-bounded polynomial with the source endpoint jets.

Declaration kind. theorem.

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

Lean code for Theorem10.13.46●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_unique (k : ℕ)
  (p : Polynomial ℝ) (hp : p.natDegree ≤ 2 * k + 1)
  (hl :
    ∀ j ≤ k,
      Polynomial.eval (-1) ((⇑Polynomial.derivative)^[j] p) =
        Real.exp (-1))
  (hr :
    ∀ j ≤ k,
      Polynomial.eval 0 ((⇑Polynomial.derivative)^[j] p) = (-1) ^ j) :
  p = QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k

theorem QuantumBlockEncoding.HermitePolynomial.sourceInterpolant_unique
  (k : ℕ) (p : Polynomial ℝ)
  (hp : p.natDegree ≤ 2 * k + 1)
  (hl :
    ∀ j ≤ k,
      Polynomial.eval (-1)
          ((⇑Polynomial.derivative)^[j]
            p) =
        Real.exp (-1))
  (hr :
    ∀ j ≤ k,
      Polynomial.eval 0
          ((⇑Polynomial.derivative)^[j]
            p) =
        (-1) ^ j) :
  p =
    QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
      k

There is only one degree-bounded polynomial with the source endpoint jets.

Theorem10.13.47

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “interpolant eq source interpolant”; the hypotheses and conclusion in the code panel fix its exact scope. The Euclidean-algorithm construction and the positive source formula agree exactly.

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 Euclidean-algorithm construction and the positive source formula agree exactly.

Declaration kind. theorem.

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

Lean code for Theorem10.13.47●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomial.lean

complete

theorem QuantumBlockEncoding.HermitePolynomial.interpolant_eq_sourceInterpolant
  (k : ℕ) :
  QuantumBlockEncoding.HermitePolynomial.interpolant k =
    QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k

theorem QuantumBlockEncoding.HermitePolynomial.interpolant_eq_sourceInterpolant
  (k : ℕ) :
  QuantumBlockEncoding.HermitePolynomial.interpolant
      k =
    QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
      k

The Euclidean-algorithm construction and the positive source formula agree exactly.