10.11. QuantumBlockEncoding/HermiteFiniteNorm.lean🔗

11 explicit public declarations, in source order.

Definition10.11.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “raw initial”.

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

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

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

Declaration kind. def.

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

Lean code for Definition10.11.1●1 definition

defdefined in QuantumBlockEncoding/HermiteFiniteNorm.lean

complete

def QuantumBlockEncoding.HermiteFiniteNorm.rawInitial (k n : ℕ) (L : ℝ) :
  Fin (2 * k + 6) → ℝ

def QuantumBlockEncoding.HermiteFiniteNorm.rawInitial
  (k n : ℕ) (L : ℝ) : Fin (2 * k + 6) → ℝ

Definition10.11.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “raw source chain”. A scalar-boundary source representation without a precomputed normalizer.

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 scalar-boundary source representation without a precomputed normalizer.

Declaration kind. def.

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

Lean code for Definition10.11.2●1 definition

defdefined in QuantumBlockEncoding/HermiteFiniteNorm.lean

complete

def QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain (k n : ℕ)
  (L : ℝ) : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1

def QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
    (n + 1) 1 1

A scalar-boundary source representation without a precomputed normalizer.

Theorem10.11.3

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.11.3●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteNorm.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain_contract (k n : ℕ)
  (L : ℝ) (hL : 0 < L)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain k n L) x 0
      0 =
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
      (n + 1) L
      ((QuantumBlockEncoding.TensorTrainWord.sampleEquiv (n + 1)) x)

theorem QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain_contract
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain
        k n L)
      x 0 0 =
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
      k (n + 1) L
      ((QuantumBlockEncoding.TensorTrainWord.sampleEquiv
          (n + 1))
        x)

Theorem10.11.4

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.11.4●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteNorm.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain_maxBond (k n : ℕ)
  (L : ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain k n L) ≤
    2 * k + 6

theorem QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain_maxBond
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain
        k n L) ≤
    2 * k + 6

Definition10.11.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “local sample norm”. Local matrix products followed by one real square root.

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. Local matrix products followed by one real square root.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/HermiteFiniteNorm.lean

complete

def QuantumBlockEncoding.HermiteFiniteNorm.localSampleNorm (k n : ℕ)
  (L : ℝ) : ℝ

def QuantumBlockEncoding.HermiteFiniteNorm.localSampleNorm
  (k n : ℕ) (L : ℝ) : ℝ

Local matrix products followed by one real square root.

Theorem10.11.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.11.6●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteNorm.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteNorm.localSampleNorm_eq_sampleNorm
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.HermiteFiniteNorm.localSampleNorm k n L =
    QuantumBlockEncoding.HermiteStatePreparation.sampleNorm k (n + 1) L

theorem QuantumBlockEncoding.HermiteFiniteNorm.localSampleNorm_eq_sampleNorm
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.HermiteFiniteNorm.localSampleNorm
      k n L =
    QuantumBlockEncoding.HermiteStatePreparation.sampleNorm
      k (n + 1) L

Theorem10.11.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “local sample norm pos”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem10.11.7●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteNorm.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteNorm.localSampleNorm_pos (k n : ℕ)
  (L : ℝ) (hL : 0 < L) :
  0 < QuantumBlockEncoding.HermiteFiniteNorm.localSampleNorm k n L

theorem QuantumBlockEncoding.HermiteFiniteNorm.localSampleNorm_pos
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  0 <
    QuantumBlockEncoding.HermiteFiniteNorm.localSampleNorm
      k n L

Theorem10.11.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “source chain eq local”; the hypotheses and conclusion in the code panel fix its exact scope. The actual normalized source cores can use the local norm supplier.

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

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

Technical source note. The actual normalized source cores can use the local norm supplier.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/HermiteFiniteNorm.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteNorm.sourceChain_eq_local (k n : ℕ)
  (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.HermiteFiniteChain.sourceChain k n L =
    QuantumBlockEncoding.MatrixProductChain.ofKernel
      (QuantumBlockEncoding.HermiteFiniteChain.kernel k n L)
      (fun a =>
        QuantumBlockEncoding.HermiteFiniteNorm.rawInitial k n L a /
          QuantumBlockEncoding.HermiteFiniteNorm.localSampleNorm k n L)
      (QuantumBlockEncoding.HermiteFiniteChain.terminal k) 0 n

theorem QuantumBlockEncoding.HermiteFiniteNorm.sourceChain_eq_local
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.HermiteFiniteChain.sourceChain
      k n L =
    QuantumBlockEncoding.MatrixProductChain.ofKernel
      (QuantumBlockEncoding.HermiteFiniteChain.kernel
        k n L)
      (fun a =>
        QuantumBlockEncoding.HermiteFiniteNorm.rawInitial
            k n L a /
          QuantumBlockEncoding.HermiteFiniteNorm.localSampleNorm
            k n L)
      (QuantumBlockEncoding.HermiteFiniteChain.terminal
        k)
      0 n

The actual normalized source cores can use the local norm supplier.

Theorem10.11.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.11.9●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteNorm.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain_storage (k n : ℕ)
  (L : ℝ) :
  QuantumBlockEncoding.MatrixProductChain.storedScalars
      (QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain k n L) ≤
    2 * (n + 1) * (2 * k + 6) ^ 2

theorem QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain_storage
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.MatrixProductChain.storedScalars
      (QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain
        k n L) ≤
    2 * (n + 1) * (2 * k + 6) ^ 2

Theorem10.11.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.11.10●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteNorm.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteNorm.norm_environment_storage
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.environmentScalars
      (QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain k n L) ≤
    (n + 2) * (2 * k + 6) ^ 2

theorem QuantumBlockEncoding.HermiteFiniteNorm.norm_environment_storage
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.environmentScalars
      (QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain
        k n L) ≤
    (n + 2) * (2 * k + 6) ^ 2

Theorem10.11.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “norm arithmetic budget”; the hypotheses and conclusion in the code panel fix its exact scope. Addition/multiplication budget of the explicit Gram schedule, excluding the final square root and the cost of supplying the raw core entries.

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. Addition/multiplication budget of the explicit Gram schedule, excluding the final square root and the cost of supplying the raw core entries.

Declaration kind. theorem.

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

Lean code for Theorem10.11.11●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteNorm.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteNorm.norm_arithmetic_budget (k n : ℕ)
  (L : ℝ) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.arithmeticBudget
      (QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain k n L) ≤
    9 * (n + 1) * (2 * k + 6) ^ 3

theorem QuantumBlockEncoding.HermiteFiniteNorm.norm_arithmetic_budget
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.arithmeticBudget
      (QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain
        k n L) ≤
    9 * (n + 1) * (2 * k + 6) ^ 3

Addition/multiplication budget of the explicit Gram schedule, excluding
the final square root and the cost of supplying the raw core entries.