ASPBE Lean Blueprint

10.5. QuantumBlockEncoding/HermiteBernstein.lean🔗

53 explicit public declarations, in source order.

Definition10.5.1
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “basis”. Evaluation of the exact degree-'d' Bernstein basis polynomial.

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. Evaluation of the exact degree-'d' Bernstein basis polynomial.

Declaration kind. def.

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

Lean code for Definition10.5.1●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.basis (d r : ℕ) (t : ℝ) : ℝ
    def QuantumBlockEncoding.HermiteBernstein.basis
  (d r : ℕ) (t : ℝ) : ℝ
    Evaluation of the exact degree-`d` Bernstein basis polynomial.
Theorem10.5.2
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.2●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.basis_eq (d r : ℕ) (t : ℝ) :
  QuantumBlockEncoding.HermiteBernstein.basis d r t =
    ↑(d.choose r) * t ^ r * (1 - t) ^ (d - r)
    theorem QuantumBlockEncoding.HermiteBernstein.basis_eq
  (d r : ℕ) (t : ℝ) :
  QuantumBlockEncoding.HermiteBernstein.basis
      d r t =
    ↑(d.choose r) * t ^ r *
      (1 - t) ^ (d - r)
Theorem10.5.3
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.3●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.basis_nonneg (d r : ℕ) (t : ℝ)
  (ht : t ∈ Set.Icc 0 1) :
  0 ≤ QuantumBlockEncoding.HermiteBernstein.basis d r t
    theorem QuantumBlockEncoding.HermiteBernstein.basis_nonneg
  (d r : ℕ) (t : ℝ)
  (ht : t ∈ Set.Icc 0 1) :
  0 ≤
    QuantumBlockEncoding.HermiteBernstein.basis
      d r t
Theorem10.5.4
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.4●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.basis_flip (d r : ℕ) (hr : r ≤ d)
  (t : ℝ) :
  QuantumBlockEncoding.HermiteBernstein.basis d r (1 - t) =
    QuantumBlockEncoding.HermiteBernstein.basis d (d - r) t
    theorem QuantumBlockEncoding.HermiteBernstein.basis_flip
  (d r : ℕ) (hr : r ≤ d) (t : ℝ) :
  QuantumBlockEncoding.HermiteBernstein.basis
      d r (1 - t) =
    QuantumBlockEncoding.HermiteBernstein.basis
      d (d - r) t
Definition10.5.5
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “source coefficient”. The coefficient of 't^i' in the source's positive truncated series.

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 coefficient of 't^i' in the source's positive truncated series.

Declaration kind. def.

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

Lean code for Definition10.5.5●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.sourceCoefficient (k i : ℕ) : ℝ
    def QuantumBlockEncoding.HermiteBernstein.sourceCoefficient
  (k i : ℕ) : ℝ
    The coefficient of `t^i` in the source's positive truncated series.
Theorem10.5.6
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.6●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.sourceCoefficient_eq (k i : ℕ) :
  QuantumBlockEncoding.HermiteBernstein.sourceCoefficient k i =
    ∑ m ∈ Finset.range (i + 1), ↑((k + i - m).choose k) / ↑m.factorial
    theorem QuantumBlockEncoding.HermiteBernstein.sourceCoefficient_eq
  (k i : ℕ) :
  QuantumBlockEncoding.HermiteBernstein.sourceCoefficient
      k i =
    ∑ m ∈ Finset.range (i + 1),
      ↑((k + i - m).choose k) /
        ↑m.factorial
Theorem10.5.7
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “source coefficient 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/HermiteBernstein.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.5.7●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.sourceCoefficient_nonneg
  (k i : ℕ) :
  0 ≤ QuantumBlockEncoding.HermiteBernstein.sourceCoefficient k i
    theorem QuantumBlockEncoding.HermiteBernstein.sourceCoefficient_nonneg
  (k i : ℕ) :
  0 ≤
    QuantumBlockEncoding.HermiteBernstein.sourceCoefficient
      k i
Definition10.5.8
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “elevation weight”. Degree-elevation weight from source monomial 'i' to basis index 'i+j'.

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. Degree-elevation weight from source monomial 'i' to basis index 'i+j'.

Declaration kind. def.

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

Lean code for Definition10.5.8●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.elevationWeight (k i j : ℕ) : ℝ
    def QuantumBlockEncoding.HermiteBernstein.elevationWeight
  (k i j : ℕ) : ℝ
    Degree-elevation weight from source monomial `i` to basis index `i+j`.
Theorem10.5.9
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.9●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.elevationWeight_nonneg
  (k i j : ℕ) :
  0 ≤ QuantumBlockEncoding.HermiteBernstein.elevationWeight k i j
    theorem QuantumBlockEncoding.HermiteBernstein.elevationWeight_nonneg
  (k i j : ℕ) :
  0 ≤
    QuantumBlockEncoding.HermiteBernstein.elevationWeight
      k i j
Theorem10.5.10
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.10●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.elevation_term (k i j : ℕ)
  (hi : i ≤ k) (hj : j ≤ k - i) (t : ℝ) :
  QuantumBlockEncoding.HermiteBernstein.elevationWeight k i j *
      QuantumBlockEncoding.HermiteBernstein.basis (2 * k + 1) (i + j)
        t =
    t ^ i * (1 - t) ^ (k + 1) * ↑((k - i).choose j) * t ^ j *
      (1 - t) ^ (k - i - j)
    theorem QuantumBlockEncoding.HermiteBernstein.elevation_term
  (k i j : ℕ) (hi : i ≤ k)
  (hj : j ≤ k - i) (t : ℝ) :
  QuantumBlockEncoding.HermiteBernstein.elevationWeight
        k i j *
      QuantumBlockEncoding.HermiteBernstein.basis
        (2 * k + 1) (i + j) t =
    t ^ i * (1 - t) ^ (k + 1) *
          ↑((k - i).choose j) *
        t ^ j *
      (1 - t) ^ (k - i - j)
Theorem10.5.11
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “elevation sum”; the hypotheses and conclusion in the code panel fix its exact scope. Exact degree elevation of one endpoint-factor monomial.

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 degree elevation of one endpoint-factor monomial.

Declaration kind. theorem.

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

Lean code for Theorem10.5.11●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.elevation_sum (k i : ℕ)
  (hi : i ≤ k) (t : ℝ) :
  ∑ j ∈ Finset.range (k - i + 1),
      QuantumBlockEncoding.HermiteBernstein.elevationWeight k i j *
        QuantumBlockEncoding.HermiteBernstein.basis (2 * k + 1) (i + j)
          t =
    t ^ i * (1 - t) ^ (k + 1)
    theorem QuantumBlockEncoding.HermiteBernstein.elevation_sum
  (k i : ℕ) (hi : i ≤ k) (t : ℝ) :
  ∑ j ∈ Finset.range (k - i + 1),
      QuantumBlockEncoding.HermiteBernstein.elevationWeight
          k i j *
        QuantumBlockEncoding.HermiteBernstein.basis
          (2 * k + 1) (i + j) t =
    t ^ i * (1 - t) ^ (k + 1)
    Exact degree elevation of one endpoint-factor monomial.
Definition10.5.12
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “left coefficient”. Collected Bernstein coefficients for the source's left endpoint factor.

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. Collected Bernstein coefficients for the source's left endpoint factor. The double-sum presentation makes degree elevation explicit; 'leftCoefficient_eq' identifies it with the single-sum formula used by the candidate implementation.

Declaration kind. def.

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

Lean code for Definition10.5.12●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.leftCoefficient (k r : ℕ) : ℝ
    def QuantumBlockEncoding.HermiteBernstein.leftCoefficient
  (k r : ℕ) : ℝ
    Collected Bernstein coefficients for the source's left endpoint factor.
The double-sum presentation makes degree elevation explicit; `leftCoefficient_eq`
identifies it with the single-sum formula used by the candidate implementation.
Theorem10.5.13
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.13●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.leftCoefficient_eq (k r : ℕ) :
  QuantumBlockEncoding.HermiteBernstein.leftCoefficient k r =
    ∑ i ∈ Finset.range (k + 1),
      if i ≤ r ∧ r ≤ k then
        QuantumBlockEncoding.HermiteBernstein.sourceCoefficient k i *
            ↑((k - i).choose (r - i)) /
          ↑((2 * k + 1).choose r)
      else 0
    theorem QuantumBlockEncoding.HermiteBernstein.leftCoefficient_eq
  (k r : ℕ) :
  QuantumBlockEncoding.HermiteBernstein.leftCoefficient
      k r =
    ∑ i ∈ Finset.range (k + 1),
      if i ≤ r ∧ r ≤ k then
        QuantumBlockEncoding.HermiteBernstein.sourceCoefficient
              k i *
            ↑((k - i).choose (r - i)) /
          ↑((2 * k + 1).choose r)
      else 0
Theorem10.5.14
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.14●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.leftCoefficient_nonneg (k r : ℕ) :
  0 ≤ QuantumBlockEncoding.HermiteBernstein.leftCoefficient k r
    theorem QuantumBlockEncoding.HermiteBernstein.leftCoefficient_nonneg
  (k r : ℕ) :
  0 ≤
    QuantumBlockEncoding.HermiteBernstein.leftCoefficient
      k r
Theorem10.5.15
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “left coefficient eval”; the hypotheses and conclusion in the code panel fix its exact scope. The collected coefficients evaluate to the literal source endpoint factor.

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 collected coefficients evaluate to the literal source endpoint factor.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermiteBernstein.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.5.15●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.leftCoefficient_eval (k : ℕ)
  (t : ℝ) :
  ∑ r ∈ Finset.range (2 * k + 2),
      QuantumBlockEncoding.HermiteBernstein.leftCoefficient k r *
        QuantumBlockEncoding.HermiteBernstein.basis (2 * k + 1) r t =
    Polynomial.eval t
      (QuantumBlockEncoding.HermitePolynomial.endpointFactor k)
    theorem QuantumBlockEncoding.HermiteBernstein.leftCoefficient_eval
  (k : ℕ) (t : ℝ) :
  ∑ r ∈ Finset.range (2 * k + 2),
      QuantumBlockEncoding.HermiteBernstein.leftCoefficient
          k r *
        QuantumBlockEncoding.HermiteBernstein.basis
          (2 * k + 1) r t =
    Polynomial.eval t
      (QuantumBlockEncoding.HermitePolynomial.endpointFactor
        k)
    The collected coefficients evaluate to the literal source endpoint factor.
Definition10.5.16
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “source bernstein coefficient”. The actual positive Bernstein coefficient vector of the source polynomial.

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 actual positive Bernstein coefficient vector of the source polynomial.

Declaration kind. def.

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

Lean code for Definition10.5.16●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient
  (k r : ℕ) : ℝ
    def QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient
  (k r : ℕ) : ℝ
    The actual positive Bernstein coefficient vector of the source polynomial.
Theorem10.5.17
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.17●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient_nonneg
  (k r : ℕ) :
  0 ≤
    QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient k r
    theorem QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient_nonneg
  (k r : ℕ) :
  0 ≤
    QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient
      k r
Theorem10.5.18
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “reflected sum”; the hypotheses and conclusion in the code panel fix its exact scope. Reflection of a coefficient vector corresponds exactly to 't ↦ 1-t'.

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. Reflection of a coefficient vector corresponds exactly to 't ↦ 1-t'.

Declaration kind. theorem.

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

Lean code for Theorem10.5.18●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.reflected_sum (d : ℕ) (c : ℕ → ℝ)
  (t : ℝ) :
  ∑ r ∈ Finset.range (d + 1),
      c (d - r) * QuantumBlockEncoding.HermiteBernstein.basis d r t =
    ∑ r ∈ Finset.range (d + 1),
      c r * QuantumBlockEncoding.HermiteBernstein.basis d r (1 - t)
    theorem QuantumBlockEncoding.HermiteBernstein.reflected_sum
  (d : ℕ) (c : ℕ → ℝ) (t : ℝ) :
  ∑ r ∈ Finset.range (d + 1),
      c (d - r) *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r t =
    ∑ r ∈ Finset.range (d + 1),
      c r *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r (1 - t)
    Reflection of a coefficient vector corresponds exactly to `t ↦ 1-t`.
Theorem10.5.19
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “source interpolant bernstein”; the hypotheses and conclusion in the code panel fix its exact scope. Exact source-to-Bernstein bridge, valid for every real coordinate, not merely on '[0,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. Exact source-to-Bernstein bridge, valid for every real coordinate, not merely on '[0,1]'. The interval is needed only for the nonnegativity of the basis.

Declaration kind. theorem.

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

Lean code for Theorem10.5.19●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.sourceInterpolant_bernstein
  (k : ℕ) (t : ℝ) :
  ∑ r ∈ Finset.range (2 * k + 2),
      QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient k
          r *
        QuantumBlockEncoding.HermiteBernstein.basis (2 * k + 1) r t =
    Polynomial.eval (t - 1)
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)
    theorem QuantumBlockEncoding.HermiteBernstein.sourceInterpolant_bernstein
  (k : ℕ) (t : ℝ) :
  ∑ r ∈ Finset.range (2 * k + 2),
      QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient
          k r *
        QuantumBlockEncoding.HermiteBernstein.basis
          (2 * k + 1) r t =
    Polynomial.eval (t - 1)
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k)
    Exact source-to-Bernstein bridge, valid for every real coordinate, not merely
on `[0,1]`. The interval is needed only for the nonnegativity of the basis.
Definition10.5.20
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “coefficient shift”. Shift a coefficient row by one entry.

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. Shift a coefficient row by one entry.

Declaration kind. def.

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

Lean code for Definition10.5.20●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.coefficientShift :
  Module.End ℝ (ℕ → ℝ)
    def QuantumBlockEncoding.HermiteBernstein.coefficientShift :
  Module.End ℝ (ℕ → ℝ)
    Shift a coefficient row by one entry.
Theorem10.5.21
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “coefficient shift pow”; 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/HermiteBernstein.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.5.21●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.coefficientShift_pow (n i : ℕ)
  (c : ℕ → ℝ) :
  (QuantumBlockEncoding.HermiteBernstein.coefficientShift ^ n) c i =
    c (i + n)
    theorem QuantumBlockEncoding.HermiteBernstein.coefficientShift_pow
  (n i : ℕ) (c : ℕ → ℝ) :
  (QuantumBlockEncoding.HermiteBernstein.coefficientShift ^
        n)
      c i =
    c (i + n)
Definition10.5.22
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “casteljau step”. One exact de Casteljau update on an infinite coefficient row.

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 exact de Casteljau update on an infinite coefficient row. Only the first 'd+1' entries can influence a degree-'d' evaluation.

Declaration kind. def.

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

Lean code for Definition10.5.22●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.casteljauStep (t : ℝ) :
  Module.End ℝ (ℕ → ℝ)
    def QuantumBlockEncoding.HermiteBernstein.casteljauStep
  (t : ℝ) : Module.End ℝ (ℕ → ℝ)
    One exact de Casteljau update on an infinite coefficient row. Only the first
`d+1` entries can influence a degree-`d` evaluation.
Theorem10.5.23
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “casteljau step apply”; 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/HermiteBernstein.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.5.23●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.casteljauStep_apply (t : ℝ)
  (c : ℕ → ℝ) (i : ℕ) :
  (QuantumBlockEncoding.HermiteBernstein.casteljauStep t) c i =
    (1 - t) * c i + t * c (i + 1)
    theorem QuantumBlockEncoding.HermiteBernstein.casteljauStep_apply
  (t : ℝ) (c : ℕ → ℝ) (i : ℕ) :
  (QuantumBlockEncoding.HermiteBernstein.casteljauStep
        t)
      c i =
    (1 - t) * c i + t * c (i + 1)
Definition10.5.24
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “casteljau”. Repeated rows of the exact de Casteljau triangle.

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. Repeated rows of the exact de Casteljau triangle.

Declaration kind. def.

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

Lean code for Definition10.5.24●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.casteljau (d : ℕ) (c : ℕ → ℝ)
  (t : ℝ) (i : ℕ) : ℝ
    def QuantumBlockEncoding.HermiteBernstein.casteljau
  (d : ℕ) (c : ℕ → ℝ) (t : ℝ) (i : ℕ) : ℝ
    Repeated rows of the exact de Casteljau triangle.
Theorem10.5.25
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.25●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.casteljau_eq_sum (d : ℕ)
  (c : ℕ → ℝ) (t : ℝ) (i : ℕ) :
  QuantumBlockEncoding.HermiteBernstein.casteljau d c t i =
    ∑ j ∈ Finset.range (d + 1),
      c (i + j) * QuantumBlockEncoding.HermiteBernstein.basis d j t
    theorem QuantumBlockEncoding.HermiteBernstein.casteljau_eq_sum
  (d : ℕ) (c : ℕ → ℝ) (t : ℝ) (i : ℕ) :
  QuantumBlockEncoding.HermiteBernstein.casteljau
      d c t i =
    ∑ j ∈ Finset.range (d + 1),
      c (i + j) *
        QuantumBlockEncoding.HermiteBernstein.basis
          d j t
Definition10.5.26
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “left restriction”. Left edge of the de Casteljau triangle: coefficients on '[0,u]'.

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. Left edge of the de Casteljau triangle: coefficients on '[0,u]'.

Declaration kind. def.

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

Lean code for Definition10.5.26●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.leftRestriction (u : ℝ)
  (c : ℕ → ℝ) (i : ℕ) : ℝ
    def QuantumBlockEncoding.HermiteBernstein.leftRestriction
  (u : ℝ) (c : ℕ → ℝ) (i : ℕ) : ℝ
    Left edge of the de Casteljau triangle: coefficients on `[0,u]`.
Theorem10.5.27
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.27●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.casteljauStep_mul_parameter
  (u t : ℝ) :
  QuantumBlockEncoding.HermiteBernstein.casteljauStep (u * t) =
    (1 - t) • 1 +
      t • QuantumBlockEncoding.HermiteBernstein.casteljauStep u
    theorem QuantumBlockEncoding.HermiteBernstein.casteljauStep_mul_parameter
  (u t : ℝ) :
  QuantumBlockEncoding.HermiteBernstein.casteljauStep
      (u * t) =
    (1 - t) • 1 +
      t •
        QuantumBlockEncoding.HermiteBernstein.casteljauStep
          u
Theorem10.5.28
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.28●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.leftRestriction_step (u t : ℝ)
  (c : ℕ → ℝ) :
  QuantumBlockEncoding.HermiteBernstein.leftRestriction u
      ((QuantumBlockEncoding.HermiteBernstein.casteljauStep (u * t))
        c) =
    (QuantumBlockEncoding.HermiteBernstein.casteljauStep t)
      (QuantumBlockEncoding.HermiteBernstein.leftRestriction u c)
    theorem QuantumBlockEncoding.HermiteBernstein.leftRestriction_step
  (u t : ℝ) (c : ℕ → ℝ) :
  QuantumBlockEncoding.HermiteBernstein.leftRestriction
      u
      ((QuantumBlockEncoding.HermiteBernstein.casteljauStep
          (u * t))
        c) =
    (QuantumBlockEncoding.HermiteBernstein.casteljauStep
        t)
      (QuantumBlockEncoding.HermiteBernstein.leftRestriction
        u c)
Theorem10.5.29
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “casteljau left restriction”; the hypotheses and conclusion in the code panel fix its exact scope. The left subdivision evaluates the original polynomial at 'u*t'.

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 subdivision evaluates the original polynomial at 'u*t'.

Declaration kind. theorem.

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

Lean code for Theorem10.5.29●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.casteljau_leftRestriction (d : ℕ)
  (c : ℕ → ℝ) (u t : ℝ) :
  QuantumBlockEncoding.HermiteBernstein.casteljau d
      (QuantumBlockEncoding.HermiteBernstein.leftRestriction u c) t 0 =
    QuantumBlockEncoding.HermiteBernstein.casteljau d c (u * t) 0
    theorem QuantumBlockEncoding.HermiteBernstein.casteljau_leftRestriction
  (d : ℕ) (c : ℕ → ℝ) (u t : ℝ) :
  QuantumBlockEncoding.HermiteBernstein.casteljau
      d
      (QuantumBlockEncoding.HermiteBernstein.leftRestriction
        u c)
      t 0 =
    QuantumBlockEncoding.HermiteBernstein.casteljau
      d c (u * t) 0
    The left subdivision evaluates the original polynomial at `u*t`.
Theorem10.5.30
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “left restriction eval”; the hypotheses and conclusion in the code panel fix its exact scope. Exact coefficient-level semantics of left de Casteljau subdivision.

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 coefficient-level semantics of left de Casteljau subdivision.

Declaration kind. theorem.

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

Lean code for Theorem10.5.30●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.leftRestriction_eval (d : ℕ)
  (c : ℕ → ℝ) (u t : ℝ) :
  ∑ r ∈ Finset.range (d + 1),
      QuantumBlockEncoding.HermiteBernstein.leftRestriction u c r *
        QuantumBlockEncoding.HermiteBernstein.basis d r t =
    ∑ r ∈ Finset.range (d + 1),
      c r * QuantumBlockEncoding.HermiteBernstein.basis d r (u * t)
    theorem QuantumBlockEncoding.HermiteBernstein.leftRestriction_eval
  (d : ℕ) (c : ℕ → ℝ) (u t : ℝ) :
  ∑ r ∈ Finset.range (d + 1),
      QuantumBlockEncoding.HermiteBernstein.leftRestriction
          u c r *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r t =
    ∑ r ∈ Finset.range (d + 1),
      c r *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r (u * t)
    Exact coefficient-level semantics of left de Casteljau subdivision.
Definition10.5.31
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “right restriction”. Right edge of the de Casteljau triangle, equivalently reflected left subdivision.

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. Right edge of the de Casteljau triangle, equivalently reflected left subdivision. The degree is required because the right edge reverses order.

Declaration kind. def.

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

Lean code for Definition10.5.31●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.rightRestriction (d : ℕ) (u : ℝ)
  (c : ℕ → ℝ) (i : ℕ) : ℝ
    def QuantumBlockEncoding.HermiteBernstein.rightRestriction
  (d : ℕ) (u : ℝ) (c : ℕ → ℝ) (i : ℕ) : ℝ
    Right edge of the de Casteljau triangle, equivalently reflected left
subdivision. The degree is required because the right edge reverses order.
Theorem10.5.32
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “right restriction eq casteljau”; 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/HermiteBernstein.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.5.32●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.rightRestriction_eq_casteljau
  (d i : ℕ) (hi : i ≤ d) (u : ℝ) (c : ℕ → ℝ) :
  QuantumBlockEncoding.HermiteBernstein.rightRestriction d u c i =
    QuantumBlockEncoding.HermiteBernstein.casteljau (d - i) c u i
    theorem QuantumBlockEncoding.HermiteBernstein.rightRestriction_eq_casteljau
  (d i : ℕ) (hi : i ≤ d) (u : ℝ)
  (c : ℕ → ℝ) :
  QuantumBlockEncoding.HermiteBernstein.rightRestriction
      d u c i =
    QuantumBlockEncoding.HermiteBernstein.casteljau
      (d - i) c u i
Theorem10.5.33
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.33●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.rightRestriction_eval (d : ℕ)
  (c : ℕ → ℝ) (u t : ℝ) :
  ∑ r ∈ Finset.range (d + 1),
      QuantumBlockEncoding.HermiteBernstein.rightRestriction d u c r *
        QuantumBlockEncoding.HermiteBernstein.basis d r t =
    ∑ r ∈ Finset.range (d + 1),
      c r *
        QuantumBlockEncoding.HermiteBernstein.basis d r
          (u + (1 - u) * t)
    theorem QuantumBlockEncoding.HermiteBernstein.rightRestriction_eval
  (d : ℕ) (c : ℕ → ℝ) (u t : ℝ) :
  ∑ r ∈ Finset.range (d + 1),
      QuantumBlockEncoding.HermiteBernstein.rightRestriction
          d u c r *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r t =
    ∑ r ∈ Finset.range (d + 1),
      c r *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r (u + (1 - u) * t)
Definition10.5.34
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “restrict coefficients”. The candidate's two successive subdivisions restricting to '[u,v]'.

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 candidate's two successive subdivisions restricting to '[u,v]'.

Declaration kind. def.

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

Lean code for Definition10.5.34●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.restrictCoefficients (d : ℕ)
  (u v : ℝ) (c : ℕ → ℝ) : ℕ → ℝ
    def QuantumBlockEncoding.HermiteBernstein.restrictCoefficients
  (d : ℕ) (u v : ℝ) (c : ℕ → ℝ) : ℕ → ℝ
    The candidate's two successive subdivisions restricting to `[u,v]`.
Theorem10.5.35
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “restrict coefficients eval”; the hypotheses and conclusion in the code panel fix its exact scope. Exact affine restriction; no floating-point quantities occur.

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 affine restriction; no floating-point quantities occur.

Declaration kind. theorem.

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

Lean code for Theorem10.5.35●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.restrictCoefficients_eval (d : ℕ)
  (c : ℕ → ℝ) (u v t : ℝ) (hu : u ≠ 1) :
  ∑ r ∈ Finset.range (d + 1),
      QuantumBlockEncoding.HermiteBernstein.restrictCoefficients d u v c
          r *
        QuantumBlockEncoding.HermiteBernstein.basis d r t =
    ∑ r ∈ Finset.range (d + 1),
      c r *
        QuantumBlockEncoding.HermiteBernstein.basis d r
          (u + (v - u) * t)
    theorem QuantumBlockEncoding.HermiteBernstein.restrictCoefficients_eval
  (d : ℕ) (c : ℕ → ℝ) (u v t : ℝ)
  (hu : u ≠ 1) :
  ∑ r ∈ Finset.range (d + 1),
      QuantumBlockEncoding.HermiteBernstein.restrictCoefficients
          d u v c r *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r t =
    ∑ r ∈ Finset.range (d + 1),
      c r *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r (u + (v - u) * t)
    Exact affine restriction; no floating-point quantities occur.
Theorem10.5.36
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.36●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.basis_sum (d : ℕ) (t : ℝ) :
  ∑ r ∈ Finset.range (d + 1),
      QuantumBlockEncoding.HermiteBernstein.basis d r t =
    1
    theorem QuantumBlockEncoding.HermiteBernstein.basis_sum
  (d : ℕ) (t : ℝ) :
  ∑ r ∈ Finset.range (d + 1),
      QuantumBlockEncoding.HermiteBernstein.basis
        d r t =
    1
Theorem10.5.37
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “bernstein sum bounds”; the hypotheses and conclusion in the code panel fix its exact scope. Bernstein evaluation lies in any common interval containing its coefficients.

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. Bernstein evaluation lies in any common interval containing its coefficients.

Declaration kind. theorem.

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

Lean code for Theorem10.5.37●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.bernstein_sum_bounds (d : ℕ)
  (c : ℕ → ℝ) (t lo hi : ℝ) (ht : t ∈ Set.Icc 0 1)
  (hc : ∀ r ≤ d, c r ∈ Set.Icc lo hi) :
  ∑ r ∈ Finset.range (d + 1),
      c r * QuantumBlockEncoding.HermiteBernstein.basis d r t ∈
    Set.Icc lo hi
    theorem QuantumBlockEncoding.HermiteBernstein.bernstein_sum_bounds
  (d : ℕ) (c : ℕ → ℝ) (t lo hi : ℝ)
  (ht : t ∈ Set.Icc 0 1)
  (hc : ∀ r ≤ d, c r ∈ Set.Icc lo hi) :
  ∑ r ∈ Finset.range (d + 1),
      c r *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r t ∈
    Set.Icc lo hi
    Bernstein evaluation lies in any common interval containing its coefficients.
Theorem10.5.38
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.38●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.leftRestriction_bounds (d : ℕ)
  (c : ℕ → ℝ) (u lo hi : ℝ) (hu : u ∈ Set.Icc 0 1)
  (hc : ∀ r ≤ d, c r ∈ Set.Icc lo hi) (i : ℕ) (hi' : i ≤ d) :
  QuantumBlockEncoding.HermiteBernstein.leftRestriction u c i ∈
    Set.Icc lo hi
    theorem QuantumBlockEncoding.HermiteBernstein.leftRestriction_bounds
  (d : ℕ) (c : ℕ → ℝ) (u lo hi : ℝ)
  (hu : u ∈ Set.Icc 0 1)
  (hc : ∀ r ≤ d, c r ∈ Set.Icc lo hi)
  (i : ℕ) (hi' : i ≤ d) :
  QuantumBlockEncoding.HermiteBernstein.leftRestriction
      u c i ∈
    Set.Icc lo hi
Theorem10.5.39
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.39●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.rightRestriction_bounds (d : ℕ)
  (c : ℕ → ℝ) (u lo hi : ℝ) (hu : u ∈ Set.Icc 0 1)
  (hc : ∀ r ≤ d, c r ∈ Set.Icc lo hi) (i : ℕ) :
  QuantumBlockEncoding.HermiteBernstein.rightRestriction d u c i ∈
    Set.Icc lo hi
    theorem QuantumBlockEncoding.HermiteBernstein.rightRestriction_bounds
  (d : ℕ) (c : ℕ → ℝ) (u lo hi : ℝ)
  (hu : u ∈ Set.Icc 0 1)
  (hc : ∀ r ≤ d, c r ∈ Set.Icc lo hi)
  (i : ℕ) :
  QuantumBlockEncoding.HermiteBernstein.rightRestriction
      d u c i ∈
    Set.Icc lo hi
Theorem10.5.40
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “restrict coefficients bounds”; the hypotheses and conclusion in the code panel fix its exact scope. Every restricted coefficient remains in the original coefficient bounds.

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 restricted coefficient remains in the original coefficient bounds.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermiteBernstein.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.5.40●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.restrictCoefficients_bounds
  (d : ℕ) (c : ℕ → ℝ) (u v lo hi : ℝ) (hu : 0 ≤ u) (huv : u < v)
  (hv : v ≤ 1) (hc : ∀ r ≤ d, c r ∈ Set.Icc lo hi) (i : ℕ)
  (hi' : i ≤ d) :
  QuantumBlockEncoding.HermiteBernstein.restrictCoefficients d u v c i ∈
    Set.Icc lo hi
    theorem QuantumBlockEncoding.HermiteBernstein.restrictCoefficients_bounds
  (d : ℕ) (c : ℕ → ℝ) (u v lo hi : ℝ)
  (hu : 0 ≤ u) (huv : u < v) (hv : v ≤ 1)
  (hc : ∀ r ≤ d, c r ∈ Set.Icc lo hi)
  (i : ℕ) (hi' : i ≤ d) :
  QuantumBlockEncoding.HermiteBernstein.restrictCoefficients
      d u v c i ∈
    Set.Icc lo hi
    Every restricted coefficient remains in the original coefficient bounds.
Theorem10.5.41
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.41●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.basis_half (d r : ℕ)
  (hr : r ≤ d) :
  QuantumBlockEncoding.HermiteBernstein.basis d r (1 / 2) =
    ↑(d.choose r) / 2 ^ d
    theorem QuantumBlockEncoding.HermiteBernstein.basis_half
  (d r : ℕ) (hr : r ≤ d) :
  QuantumBlockEncoding.HermiteBernstein.basis
      d r (1 / 2) =
    ↑(d.choose r) / 2 ^ d
Theorem10.5.42
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “left restriction half”; the hypotheses and conclusion in the code panel fix its exact scope. The lower half-interval subdivision row is the candidate's binomial row.

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 lower half-interval subdivision row is the candidate's binomial row.

Declaration kind. theorem.

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

Lean code for Theorem10.5.42●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.leftRestriction_half (c : ℕ → ℝ)
  (i : ℕ) :
  QuantumBlockEncoding.HermiteBernstein.leftRestriction (1 / 2) c i =
    ∑ j ∈ Finset.range (i + 1), c j * ↑(i.choose j) / 2 ^ i
    theorem QuantumBlockEncoding.HermiteBernstein.leftRestriction_half
  (c : ℕ → ℝ) (i : ℕ) :
  QuantumBlockEncoding.HermiteBernstein.leftRestriction
      (1 / 2) c i =
    ∑ j ∈ Finset.range (i + 1),
      c j * ↑(i.choose j) / 2 ^ i
    The lower half-interval subdivision row is the candidate's binomial row.
Theorem10.5.43
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “right restriction half”; the hypotheses and conclusion in the code panel fix its exact scope. The upper half-interval subdivision row, with 'j' the offset from row 'i'.

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 upper half-interval subdivision row, with 'j' the offset from row 'i'.

Declaration kind. theorem.

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

Lean code for Theorem10.5.43●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.rightRestriction_half (d i : ℕ)
  (hi : i ≤ d) (c : ℕ → ℝ) :
  QuantumBlockEncoding.HermiteBernstein.rightRestriction d (1 / 2) c i =
    ∑ j ∈ Finset.range (d - i + 1),
      c (i + j) * ↑((d - i).choose j) / 2 ^ (d - i)
    theorem QuantumBlockEncoding.HermiteBernstein.rightRestriction_half
  (d i : ℕ) (hi : i ≤ d) (c : ℕ → ℝ) :
  QuantumBlockEncoding.HermiteBernstein.rightRestriction
      d (1 / 2) c i =
    ∑ j ∈ Finset.range (d - i + 1),
      c (i + j) * ↑((d - i).choose j) /
        2 ^ (d - i)
    The upper half-interval subdivision row, with `j` the offset from row `i`.
Theorem10.5.44
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “source interpolant restricted”; the hypotheses and conclusion in the code panel fix its exact scope. The complete exact source/restriction bridge needed by Bernstein injection.

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 complete exact source/restriction bridge needed by Bernstein injection.

Declaration kind. theorem.

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

Lean code for Theorem10.5.44●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.sourceInterpolant_restricted
  (k : ℕ) (u v t : ℝ) (hu : u ≠ 1) :
  ∑ r ∈ Finset.range (2 * k + 2),
      QuantumBlockEncoding.HermiteBernstein.restrictCoefficients
          (2 * k + 1) u v
          (QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient
            k)
          r *
        QuantumBlockEncoding.HermiteBernstein.basis (2 * k + 1) r t =
    Polynomial.eval (u + (v - u) * t - 1)
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)
    theorem QuantumBlockEncoding.HermiteBernstein.sourceInterpolant_restricted
  (k : ℕ) (u v t : ℝ) (hu : u ≠ 1) :
  ∑ r ∈ Finset.range (2 * k + 2),
      QuantumBlockEncoding.HermiteBernstein.restrictCoefficients
          (2 * k + 1) u v
          (QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient
            k)
          r *
        QuantumBlockEncoding.HermiteBernstein.basis
          (2 * k + 1) r t =
    Polynomial.eval (u + (v - u) * t - 1)
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k)
    The complete exact source/restriction bridge needed by Bernstein injection.
Definition10.5.45
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “half subdivision”. Exact coefficient update for one binary digit; 'false' is the lower child.

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. Exact coefficient update for one binary digit; 'false' is the lower child.

Declaration kind. def.

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

Lean code for Definition10.5.45●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.halfSubdivision (d : ℕ)
  (bit : Bool) (c : ℕ → ℝ) : ℕ → ℝ
    def QuantumBlockEncoding.HermiteBernstein.halfSubdivision
  (d : ℕ) (bit : Bool) (c : ℕ → ℝ) : ℕ → ℝ
    Exact coefficient update for one binary digit; `false` is the lower child.
Definition10.5.46
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “child coordinate”. The local coordinate of one binary child.

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 local coordinate of one binary child.

Declaration kind. def.

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

Lean code for Definition10.5.46●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.childCoordinate (bit : Bool)
  (t : ℝ) : ℝ
    def QuantumBlockEncoding.HermiteBernstein.childCoordinate
  (bit : Bool) (t : ℝ) : ℝ
    The local coordinate of one binary child.
Theorem10.5.47
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “half subdivision 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/HermiteBernstein.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.5.47●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.halfSubdivision_eval (d : ℕ)
  (c : ℕ → ℝ) (bit : Bool) (t : ℝ) :
  ∑ r ∈ Finset.range (d + 1),
      QuantumBlockEncoding.HermiteBernstein.halfSubdivision d bit c r *
        QuantumBlockEncoding.HermiteBernstein.basis d r t =
    ∑ r ∈ Finset.range (d + 1),
      c r *
        QuantumBlockEncoding.HermiteBernstein.basis d r
          (QuantumBlockEncoding.HermiteBernstein.childCoordinate bit t)
    theorem QuantumBlockEncoding.HermiteBernstein.halfSubdivision_eval
  (d : ℕ) (c : ℕ → ℝ) (bit : Bool)
  (t : ℝ) :
  ∑ r ∈ Finset.range (d + 1),
      QuantumBlockEncoding.HermiteBernstein.halfSubdivision
          d bit c r *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r t =
    ∑ r ∈ Finset.range (d + 1),
      c r *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r
          (QuantumBlockEncoding.HermiteBernstein.childCoordinate
            bit t)
Definition10.5.48
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “subdivision path”. Successive binary subdivisions in MSB-first order.

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. Successive binary subdivisions in MSB-first order.

Declaration kind. def.

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

Lean code for Definition10.5.48●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.subdivisionPath (d : ℕ)
  (c : ℕ → ℝ) : List Bool → ℕ → ℝ
    def QuantumBlockEncoding.HermiteBernstein.subdivisionPath
  (d : ℕ) (c : ℕ → ℝ) : List Bool → ℕ → ℝ
    Successive binary subdivisions in MSB-first order.
Definition10.5.49
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “path coordinate”. Composition of the same MSB-first binary-child coordinate maps.

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. Composition of the same MSB-first binary-child coordinate maps.

Declaration kind. def.

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

Lean code for Definition10.5.49●1 definition
  • defdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    def QuantumBlockEncoding.HermiteBernstein.pathCoordinate : List Bool → ℝ → ℝ
    def QuantumBlockEncoding.HermiteBernstein.pathCoordinate :
  List Bool → ℝ → ℝ
    Composition of the same MSB-first binary-child coordinate maps.
Theorem10.5.50
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “subdivision path eval”; the hypotheses and conclusion in the code panel fix its exact scope. The shared Bernstein state is exact after any finite bit prefix.

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 shared Bernstein state is exact after any finite bit prefix.

Declaration kind. theorem.

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

Lean code for Theorem10.5.50●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.subdivisionPath_eval (d : ℕ)
  (c : ℕ → ℝ) (bits : List Bool) (t : ℝ) :
  ∑ r ∈ Finset.range (d + 1),
      QuantumBlockEncoding.HermiteBernstein.subdivisionPath d c bits r *
        QuantumBlockEncoding.HermiteBernstein.basis d r t =
    ∑ r ∈ Finset.range (d + 1),
      c r *
        QuantumBlockEncoding.HermiteBernstein.basis d r
          (QuantumBlockEncoding.HermiteBernstein.pathCoordinate bits t)
    theorem QuantumBlockEncoding.HermiteBernstein.subdivisionPath_eval
  (d : ℕ) (c : ℕ → ℝ) (bits : List Bool)
  (t : ℝ) :
  ∑ r ∈ Finset.range (d + 1),
      QuantumBlockEncoding.HermiteBernstein.subdivisionPath
          d c bits r *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r t =
    ∑ r ∈ Finset.range (d + 1),
      c r *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r
          (QuantumBlockEncoding.HermiteBernstein.pathCoordinate
            bits t)
    The shared Bernstein state is exact after any finite bit prefix.
Theorem10.5.51
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.5.51●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.bernstein_eval_zero (d : ℕ)
  (c : ℕ → ℝ) :
  ∑ r ∈ Finset.range (d + 1),
      c r * QuantumBlockEncoding.HermiteBernstein.basis d r 0 =
    c 0
    theorem QuantumBlockEncoding.HermiteBernstein.bernstein_eval_zero
  (d : ℕ) (c : ℕ → ℝ) :
  ∑ r ∈ Finset.range (d + 1),
      c r *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r 0 =
    c 0
Theorem10.5.52
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “subdivision path readout”; the hypotheses and conclusion in the code panel fix its exact scope. The zeroth coefficient after the last digit is the value at the represented left endpoint.

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 zeroth coefficient after the last digit is the value at the represented left endpoint. This is the exact shared-state readout invariant.

Declaration kind. theorem.

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

Lean code for Theorem10.5.52●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.subdivisionPath_readout (d : ℕ)
  (c : ℕ → ℝ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBernstein.subdivisionPath d c bits 0 =
    ∑ r ∈ Finset.range (d + 1),
      c r *
        QuantumBlockEncoding.HermiteBernstein.basis d r
          (QuantumBlockEncoding.HermiteBernstein.pathCoordinate bits 0)
    theorem QuantumBlockEncoding.HermiteBernstein.subdivisionPath_readout
  (d : ℕ) (c : ℕ → ℝ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBernstein.subdivisionPath
      d c bits 0 =
    ∑ r ∈ Finset.range (d + 1),
      c r *
        QuantumBlockEncoding.HermiteBernstein.basis
          d r
          (QuantumBlockEncoding.HermiteBernstein.pathCoordinate
            bits 0)
    The zeroth coefficient after the last digit is the value at the represented
left endpoint. This is the exact shared-state readout invariant.
Theorem10.5.53
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “source interpolant subdivision readout”; the hypotheses and conclusion in the code panel fix its exact scope. Source-correct readout from a restricted Bernstein injection followed by any finite MSB-first suffix.

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-correct readout from a restricted Bernstein injection followed by any finite MSB-first suffix. The separate threshold-injection automaton is not asserted by this theorem.

Declaration kind. theorem.

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

Lean code for Theorem10.5.53●1 theorem
  • theoremdefined in QuantumBlockEncoding/HermiteBernstein.lean
    complete
    theorem QuantumBlockEncoding.HermiteBernstein.sourceInterpolant_subdivision_readout
  (k : ℕ) (u v : ℝ) (hu : u ≠ 1) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBernstein.subdivisionPath (2 * k + 1)
      (QuantumBlockEncoding.HermiteBernstein.restrictCoefficients
        (2 * k + 1) u v
        (QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient
          k))
      bits 0 =
    Polynomial.eval
      (u +
          (v - u) *
            QuantumBlockEncoding.HermiteBernstein.pathCoordinate bits
              0 -
        1)
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)
    theorem QuantumBlockEncoding.HermiteBernstein.sourceInterpolant_subdivision_readout
  (k : ℕ) (u v : ℝ) (hu : u ≠ 1)
  (bits : List Bool) :
  QuantumBlockEncoding.HermiteBernstein.subdivisionPath
      (2 * k + 1)
      (QuantumBlockEncoding.HermiteBernstein.restrictCoefficients
        (2 * k + 1) u v
        (QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient
          k))
      bits 0 =
    Polynomial.eval
      (u +
          (v - u) *
            QuantumBlockEncoding.HermiteBernstein.pathCoordinate
              bits 0 -
        1)
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k)
    Source-correct readout from a restricted Bernstein injection followed by any
finite MSB-first suffix. The separate threshold-injection automaton is not
asserted by this theorem.