10.12. QuantumBlockEncoding/HermiteIntervalMass.lean🔗

19 explicit public declarations, in source order.

Definition10.12.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “power sum closed”. A power sum with iteration bound depending on the degree, not sample count.

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. A power sum with iteration bound depending on the degree, not sample count.

Declaration kind. def.

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

Lean code for Definition10.12.1●1 definition

defdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

def QuantumBlockEncoding.HermiteIntervalMass.powerSumClosed
  (count degree : ℕ) : ℚ

def QuantumBlockEncoding.HermiteIntervalMass.powerSumClosed
  (count degree : ℕ) : ℚ

A power sum with iteration bound depending on the degree, not sample count.

Theorem10.12.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “power sum closed eq”; the hypotheses and conclusion in the code panel fix its exact scope. Mathlib's exact Faulhaber theorem, exposed over the real target field.

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. Mathlib's exact Faulhaber theorem, exposed over the real target field.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

theorem QuantumBlockEncoding.HermiteIntervalMass.powerSumClosed_eq
  (count degree : ℕ) :
  ↑(QuantumBlockEncoding.HermiteIntervalMass.powerSumClosed count
        degree) =
    ∑ j ∈ Finset.range count, ↑j ^ degree

theorem QuantumBlockEncoding.HermiteIntervalMass.powerSumClosed_eq
  (count degree : ℕ) :
  ↑(QuantumBlockEncoding.HermiteIntervalMass.powerSumClosed
        count degree) =
    ∑ j ∈ Finset.range count, ↑j ^ degree

Mathlib's exact Faulhaber theorem, exposed over the real target field.

Definition10.12.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “affine squared”. Square the actual polynomial amplitude after an affine index substitution.

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. Square the actual polynomial amplitude after an affine index substitution.

Declaration kind. def.

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

Lean code for Definition10.12.3●1 definition

defdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

def QuantumBlockEncoding.HermiteIntervalMass.affineSquared
  (p : Polynomial ℝ) (start step : ℝ) : Polynomial ℝ

def QuantumBlockEncoding.HermiteIntervalMass.affineSquared
  (p : Polynomial ℝ) (start step : ℝ) :
  Polynomial ℝ

Square the actual polynomial amplitude after an affine index substitution.

Theorem10.12.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “affine squared 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/HermiteIntervalMass.lean:37. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.12.4●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

theorem QuantumBlockEncoding.HermiteIntervalMass.affineSquared_eval
  (p : Polynomial ℝ) (start step x : ℝ) :
  Polynomial.eval x
      (QuantumBlockEncoding.HermiteIntervalMass.affineSquared p start
        step) =
    Polynomial.eval (start + step * x) p ^ 2

theorem QuantumBlockEncoding.HermiteIntervalMass.affineSquared_eval
  (p : Polynomial ℝ) (start step x : ℝ) :
  Polynomial.eval x
      (QuantumBlockEncoding.HermiteIntervalMass.affineSquared
        p start step) =
    Polynomial.eval (start + step * x) p ^
      2

Definition10.12.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “polynomial mass closed”. A supplied degree bound gives a fixed-size expression for discrete mass.

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. A supplied degree bound gives a fixed-size expression for discrete mass.

Declaration kind. def.

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

Lean code for Definition10.12.5●1 definition

defdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

def QuantumBlockEncoding.HermiteIntervalMass.polynomialMassClosed
  (p : Polynomial ℝ) (start step : ℝ) (count bound : ℕ) : ℝ

def QuantumBlockEncoding.HermiteIntervalMass.polynomialMassClosed
  (p : Polynomial ℝ) (start step : ℝ)
  (count bound : ℕ) : ℝ

A supplied degree bound gives a fixed-size expression for discrete mass.

Theorem10.12.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “polynomial mass closed eq”; the hypotheses and conclusion in the code panel fix its exact scope. Exact arbitrary-count identity; no quadrature or continuum substitution.

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. Exact arbitrary-count identity; no quadrature or continuum substitution.

Declaration kind. theorem.

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

Lean code for Theorem10.12.6●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

theorem QuantumBlockEncoding.HermiteIntervalMass.polynomialMassClosed_eq
  (p : Polynomial ℝ) (start step : ℝ) (count bound : ℕ)
  (h :
    (QuantumBlockEncoding.HermiteIntervalMass.affineSquared p start
          step).natDegree ≤
      bound) :
  QuantumBlockEncoding.HermiteIntervalMass.polynomialMassClosed p start
      step count bound =
    ∑ j ∈ Finset.range count, Polynomial.eval (start + step * ↑j) p ^ 2

theorem QuantumBlockEncoding.HermiteIntervalMass.polynomialMassClosed_eq
  (p : Polynomial ℝ) (start step : ℝ)
  (count bound : ℕ)
  (h :
    (QuantumBlockEncoding.HermiteIntervalMass.affineSquared
          p start step).natDegree ≤
      bound) :
  QuantumBlockEncoding.HermiteIntervalMass.polynomialMassClosed
      p start step count bound =
    ∑ j ∈ Finset.range count,
      Polynomial.eval (start + step * ↑j)
          p ^
        2

Exact arbitrary-count identity; no quadrature or continuum substitution.

Theorem10.12.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “affine squared 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/HermiteIntervalMass.lean:59. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.12.7●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

theorem QuantumBlockEncoding.HermiteIntervalMass.affineSquared_degree
  (p : Polynomial ℝ) (start step : ℝ) :
  (QuantumBlockEncoding.HermiteIntervalMass.affineSquared p start
        step).natDegree ≤
    2 * p.natDegree

theorem QuantumBlockEncoding.HermiteIntervalMass.affineSquared_degree
  (p : Polynomial ℝ) (start step : ℝ) :
  (QuantumBlockEncoding.HermiteIntervalMass.affineSquared
        p start step).natDegree ≤
    2 * p.natDegree

Theorem10.12.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermite affine squared degree”; the hypotheses and conclusion in the code panel fix its exact scope. At most '4*k+3' coefficient terms suffice for every affine progression.

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. At most '4*k+3' coefficient terms suffice for every affine progression.

Declaration kind. theorem.

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

Lean code for Theorem10.12.8●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

theorem QuantumBlockEncoding.HermiteIntervalMass.hermite_affineSquared_degree
  (k : ℕ) (start step : ℝ) :
  (QuantumBlockEncoding.HermiteIntervalMass.affineSquared
        (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)
        start step).natDegree ≤
    4 * k + 2

theorem QuantumBlockEncoding.HermiteIntervalMass.hermite_affineSquared_degree
  (k : ℕ) (start step : ℝ) :
  (QuantumBlockEncoding.HermiteIntervalMass.affineSquared
        (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
          k)
        start step).natDegree ≤
    4 * k + 2

At most `4*k+3` coefficient terms suffice for every affine progression.

Theorem10.12.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermite polynomial mass”; the hypotheses and conclusion in the code panel fix its exact scope. The exact discrete squared mass of the polynomial branch, at arbitrary width.

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 discrete squared mass of the polynomial branch, at arbitrary width.

Declaration kind. theorem.

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

Lean code for Theorem10.12.9●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

theorem QuantumBlockEncoding.HermiteIntervalMass.hermite_polynomial_mass
  (k count : ℕ) (start step : ℝ) :
  QuantumBlockEncoding.HermiteIntervalMass.polynomialMassClosed
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k) start
      step count (4 * k + 2) =
    ∑ j ∈ Finset.range count,
      Polynomial.eval (start + step * ↑j)
          (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k) ^
        2

theorem QuantumBlockEncoding.HermiteIntervalMass.hermite_polynomial_mass
  (k count : ℕ) (start step : ℝ) :
  QuantumBlockEncoding.HermiteIntervalMass.polynomialMassClosed
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k)
      start step count (4 * k + 2) =
    ∑ j ∈ Finset.range count,
      Polynomial.eval (start + step * ↑j)
          (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
            k) ^
        2

The exact discrete squared mass of the polynomial branch, at arbitrary width.

Definition10.12.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “exponential mass closed”. Explicit finite exponential mass, including the zero-step corner case.

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 finite exponential mass, including the zero-step corner case.

Declaration kind. def.

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

Lean code for Definition10.12.10●1 definition

defdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

def QuantumBlockEncoding.HermiteIntervalMass.exponentialMassClosed
  (start step : ℝ) (count : ℕ) : ℝ

def QuantumBlockEncoding.HermiteIntervalMass.exponentialMassClosed
  (start step : ℝ) (count : ℕ) : ℝ

Explicit finite exponential mass, including the zero-step corner case.

Theorem10.12.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exponential mass closed eq”; the hypotheses and conclusion in the code panel fix its exact scope. Exact geometric mass of squared exponential amplitudes.

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. Exact geometric mass of squared exponential amplitudes.

Declaration kind. theorem.

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

Lean code for Theorem10.12.11●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

theorem QuantumBlockEncoding.HermiteIntervalMass.exponentialMassClosed_eq
  (start step : ℝ) (count : ℕ) :
  QuantumBlockEncoding.HermiteIntervalMass.exponentialMassClosed start
      step count =
    ∑ j ∈ Finset.range count, Real.exp (start + step * ↑j) ^ 2

theorem QuantumBlockEncoding.HermiteIntervalMass.exponentialMassClosed_eq
  (start step : ℝ) (count : ℕ) :
  QuantumBlockEncoding.HermiteIntervalMass.exponentialMassClosed
      start step count =
    ∑ j ∈ Finset.range count,
      Real.exp (start + step * ↑j) ^ 2

Exact geometric mass of squared exponential amplitudes.

Theorem10.12.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “right exponential mass”; the hypotheses and conclusion in the code panel fix its exact scope. The positive exponential branch uses the same formula with negated grid.

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 positive exponential branch uses the same formula with negated grid.

Declaration kind. theorem.

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

Lean code for Theorem10.12.12●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

theorem QuantumBlockEncoding.HermiteIntervalMass.right_exponential_mass
  (start step : ℝ) (count : ℕ) :
  QuantumBlockEncoding.HermiteIntervalMass.exponentialMassClosed
      (-start) (-step) count =
    ∑ j ∈ Finset.range count, Real.exp (-(start + step * ↑j)) ^ 2

theorem QuantumBlockEncoding.HermiteIntervalMass.right_exponential_mass
  (start step : ℝ) (count : ℕ) :
  QuantumBlockEncoding.HermiteIntervalMass.exponentialMassClosed
      (-start) (-step) count =
    ∑ j ∈ Finset.range count,
      Real.exp (-(start + step * ↑j)) ^ 2

The positive exponential branch uses the same formula with negated grid.

Theorem10.12.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “smooth initial middle mass”; the hypotheses and conclusion in the code panel fix its exact scope. On the middle branch the formula is the frozen 'smoothInitial' mass.

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. On the middle branch the formula is the frozen 'smoothInitial' mass.

Declaration kind. theorem.

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

Lean code for Theorem10.12.13●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

theorem QuantumBlockEncoding.HermiteIntervalMass.smoothInitial_middle_mass
  (k count : ℕ) (start step : ℝ)
  (h : ∀ j ∈ Finset.range count, start + step * ↑j ∈ Set.Icc (-1) 0) :
  QuantumBlockEncoding.HermiteIntervalMass.polynomialMassClosed
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k) start
      step count (4 * k + 2) =
    ∑ j ∈ Finset.range count,
      QuantumBlockEncoding.HermitePolynomial.smoothInitial k
          (start + step * ↑j) ^
        2

theorem QuantumBlockEncoding.HermiteIntervalMass.smoothInitial_middle_mass
  (k count : ℕ) (start step : ℝ)
  (h :
    ∀ j ∈ Finset.range count,
      start + step * ↑j ∈
        Set.Icc (-1) 0) :
  QuantumBlockEncoding.HermiteIntervalMass.polynomialMassClosed
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k)
      start step count (4 * k + 2) =
    ∑ j ∈ Finset.range count,
      QuantumBlockEncoding.HermitePolynomial.smoothInitial
          k (start + step * ↑j) ^
        2

On the middle branch the formula is the frozen `smoothInitial` mass.

Theorem10.12.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “smooth initial left mass”; the hypotheses and conclusion in the code panel fix its exact scope. The left-tail formula concerns the function amplitude, not its square root.

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 left-tail formula concerns the function amplitude, not its square root.

Declaration kind. theorem.

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

Lean code for Theorem10.12.14●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

theorem QuantumBlockEncoding.HermiteIntervalMass.smoothInitial_left_mass
  (k count : ℕ) (start step : ℝ)
  (h : ∀ j ∈ Finset.range count, start + step * ↑j < -1) :
  QuantumBlockEncoding.HermiteIntervalMass.exponentialMassClosed start
      step count =
    ∑ j ∈ Finset.range count,
      QuantumBlockEncoding.HermitePolynomial.smoothInitial k
          (start + step * ↑j) ^
        2

theorem QuantumBlockEncoding.HermiteIntervalMass.smoothInitial_left_mass
  (k count : ℕ) (start step : ℝ)
  (h :
    ∀ j ∈ Finset.range count,
      start + step * ↑j < -1) :
  QuantumBlockEncoding.HermiteIntervalMass.exponentialMassClosed
      start step count =
    ∑ j ∈ Finset.range count,
      QuantumBlockEncoding.HermitePolynomial.smoothInitial
          k (start + step * ↑j) ^
        2

The left-tail formula concerns the function amplitude, not its square root.

Theorem10.12.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “smooth initial right mass”; the hypotheses and conclusion in the code panel fix its exact scope. The right-tail formula is equally a statement about the exact frozen target.

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 right-tail formula is equally a statement about the exact frozen target.

Declaration kind. theorem.

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

Lean code for Theorem10.12.15●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

theorem QuantumBlockEncoding.HermiteIntervalMass.smoothInitial_right_mass
  (k count : ℕ) (start step : ℝ)
  (h : ∀ j ∈ Finset.range count, 0 < start + step * ↑j) :
  QuantumBlockEncoding.HermiteIntervalMass.exponentialMassClosed
      (-start) (-step) count =
    ∑ j ∈ Finset.range count,
      QuantumBlockEncoding.HermitePolynomial.smoothInitial k
          (start + step * ↑j) ^
        2

theorem QuantumBlockEncoding.HermiteIntervalMass.smoothInitial_right_mass
  (k count : ℕ) (start step : ℝ)
  (h :
    ∀ j ∈ Finset.range count,
      0 < start + step * ↑j) :
  QuantumBlockEncoding.HermiteIntervalMass.exponentialMassClosed
      (-start) (-step) count =
    ∑ j ∈ Finset.range count,
      QuantumBlockEncoding.HermitePolynomial.smoothInitial
          k (start + step * ↑j) ^
        2

The right-tail formula is equally a statement about the exact frozen target.

Theorem10.12.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “smooth initial zero”; the hypotheses and conclusion in the code panel fix its exact scope. The splice passes through amplitude one, independently of smoothing 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 splice passes through amplitude one, independently of smoothing order.

Declaration kind. theorem.

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

Lean code for Theorem10.12.16●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

theorem QuantumBlockEncoding.HermiteIntervalMass.smoothInitial_zero (k : ℕ) :
  QuantumBlockEncoding.HermitePolynomial.smoothInitial k 0 = 1

theorem QuantumBlockEncoding.HermiteIntervalMass.smoothInitial_zero
  (k : ℕ) :
  QuantumBlockEncoding.HermitePolynomial.smoothInitial
      k 0 =
    1

The splice passes through amplitude one, independently of smoothing order.

Definition10.12.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “central index”. The central sample in a nonempty qubit register, in the frozen LE indexing.

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 central sample in a nonempty qubit register, in the frozen LE indexing.

Declaration kind. def.

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

Lean code for Definition10.12.17●1 definition

defdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

def QuantumBlockEncoding.HermiteIntervalMass.centralIndex (n : ℕ) :
  Fin (QuantumBlockEncoding.gridSize (n + 1))

def QuantumBlockEncoding.HermiteIntervalMass.centralIndex
  (n : ℕ) :
  Fin
    (QuantumBlockEncoding.gridSize
      (n + 1))

The central sample in a nonempty qubit register, in the frozen LE indexing.

Theorem10.12.18

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.12.18●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

theorem QuantumBlockEncoding.HermiteIntervalMass.gridPoint_central (n : ℕ)
  (L : ℝ) :
  QuantumBlockEncoding.HermiteStatePreparation.gridPoint (n + 1) L
      (QuantumBlockEncoding.HermiteIntervalMass.centralIndex n) =
    0

theorem QuantumBlockEncoding.HermiteIntervalMass.gridPoint_central
  (n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteStatePreparation.gridPoint
      (n + 1) L
      (QuantumBlockEncoding.HermiteIntervalMass.centralIndex
        n) =
    0

Theorem10.12.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sampled mass ge one”; the hypotheses and conclusion in the code panel fix its exact scope. A width-uniform conditioning anchor: the unnormalized squared norm is at least one.

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 width-uniform conditioning anchor: the unnormalized squared norm is at least one. This uses the actual grid's central sample, not a positivity oracle.

Declaration kind. theorem.

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

Lean code for Theorem10.12.19●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteIntervalMass.lean

complete

theorem QuantumBlockEncoding.HermiteIntervalMass.sampled_mass_ge_one (k n : ℕ)
  (L : ℝ) :
  1 ≤
    ∑ j,
      QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
          (n + 1) L j ^
        2

theorem QuantumBlockEncoding.HermiteIntervalMass.sampled_mass_ge_one
  (k n : ℕ) (L : ℝ) :
  1 ≤
    ∑ j,
      QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
          k (n + 1) L j ^
        2

A width-uniform conditioning anchor: the unnormalized squared norm is at
least one. This uses the actual grid's central sample, not a positivity oracle.