10.65. QuantumBlockEncoding/StoredHermiteRawSource.lean🔗

15 explicit public declarations, in source order.

Definition10.65.1

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “stage run”. A proposition-valued field is a requirement until a constructor supplies it.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

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. structure.

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

Lean code for Definition10.65.1●1 definition

structure(extends 1, 3 fields)defined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete
structure QuantumBlockEncoding.StoredHermiteRawSource.StageRun (α : Type) : Type
structure QuantumBlockEncoding.StoredHermiteRawSource.StageRun (α : Type) : Type
Extends
- QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun α
Fields
run : QuantumBlockEncoding.StoredGivens.Run α
Inherited from

QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun
exponentialCalls : ℕ
Inherited from

QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun
integerAdditions : ℕ

Definition10.65.2

uses 0used by 0✓L∃∀N

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

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/StoredHermiteRawSource.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.65.2●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete

def QuantumBlockEncoding.StoredHermiteRawSource.stage {k n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n)
  (t : Fin (n + 1)) :
  QuantumBlockEncoding.StoredHermiteRawSource.StageRun
    (QuantumBlockEncoding.StoredTensorTrain.StoredCore (2 * k + 6)
      (2 * k + 6))

def QuantumBlockEncoding.StoredHermiteRawSource.stage
  {k n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n)
  (t : Fin (n + 1)) :
  QuantumBlockEncoding.StoredHermiteRawSource.StageRun
    (QuantumBlockEncoding.StoredTensorTrain.StoredCore
      (2 * k + 6) (2 * k + 6))

Theorem10.65.3

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.65.3●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawSource.stage_source (k n : ℕ)
  (L : ℝ) (hL : 0 < L) (t : Fin (n + 1)) (a : Fin (2 * k + 6))
  (out : Fin 2 × Fin (2 * k + 6)) :
  QuantumBlockEncoding.StoredTensorTrain.denoteCore
      (QuantumBlockEncoding.StoredHermiteRawSource.stage
            (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
                  L).run.value
            t).run.value
      a out =
    QuantumBlockEncoding.HermiteExplicitBond.kernel k n L (↑t) out.1 a
      out.2

theorem QuantumBlockEncoding.StoredHermiteRawSource.stage_source
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (t : Fin (n + 1)) (a : Fin (2 * k + 6))
  (out : Fin 2 × Fin (2 * k + 6)) :
  QuantumBlockEncoding.StoredTensorTrain.denoteCore
      (QuantumBlockEncoding.StoredHermiteRawSource.stage
            (QuantumBlockEncoding.StoredHermiteSourceCache.compile
                  k n L).run.value
            t).run.value
      a out =
    QuantumBlockEncoding.HermiteExplicitBond.kernel
      k n L (↑t) out.1 a out.2

Definition10.65.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “collect stages”. Materialize the stage records once, then project cores and their ledgers.

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. Materialize the stage records once, then project cores and their ledgers. The full records are not recomputed when integer/exp counters are summed.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete

def QuantumBlockEncoding.StoredHermiteRawSource.collectStages {α : Type}
  {m : ℕ}
  (f : Fin m → QuantumBlockEncoding.StoredHermiteRawSource.StageRun α) :
  QuantumBlockEncoding.StoredHermiteRawSource.StageRun (Vector α m)

def QuantumBlockEncoding.StoredHermiteRawSource.collectStages
  {α : Type} {m : ℕ}
  (f :
    Fin m →
      QuantumBlockEncoding.StoredHermiteRawSource.StageRun
        α) :
  QuantumBlockEncoding.StoredHermiteRawSource.StageRun
    (Vector α m)

Materialize the stage records once, then project cores and their ledgers.
The full records are not recomputed when integer/exp counters are summed.

Theorem10.65.5

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.65.5●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawSource.collectStages_value
  {α : Type} {m : ℕ}
  (f : Fin m → QuantumBlockEncoding.StoredHermiteRawSource.StageRun α)
  (i : Fin m) :
  (QuantumBlockEncoding.StoredHermiteRawSource.collectStages
            f).run.value[↑i] =
    (f i).run.value

theorem QuantumBlockEncoding.StoredHermiteRawSource.collectStages_value
  {α : Type} {m : ℕ}
  (f :
    Fin m →
      QuantumBlockEncoding.StoredHermiteRawSource.StageRun
        α)
  (i : Fin m) :
  (QuantumBlockEncoding.StoredHermiteRawSource.collectStages
            f).run.value[↑i] =
    (f i).run.value

Definition10.65.6

uses 0used by 0✓L∃∀N

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

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/StoredHermiteRawSource.lean:57. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.65.6●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete

def QuantumBlockEncoding.StoredHermiteRawSource.tables {k n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n) :
  QuantumBlockEncoding.StoredHermiteRawSource.StageRun
    (Vector
      (QuantumBlockEncoding.StoredTensorTrain.StoredCore (2 * k + 6)
        (2 * k + 6))
      (n + 1))

def QuantumBlockEncoding.StoredHermiteRawSource.tables
  {k n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n) :
  QuantumBlockEncoding.StoredHermiteRawSource.StageRun
    (Vector
      (QuantumBlockEncoding.StoredTensorTrain.StoredCore
        (2 * k + 6) (2 * k + 6))
      (n + 1))

Theorem10.65.7

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.65.7●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawSource.tables_window (k n : ℕ)
  (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.StoredMatrixProductChain.Window
    (QuantumBlockEncoding.StoredHermiteRawSource.tables
          (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
                L).run.value).run.value
    (QuantumBlockEncoding.HermiteExplicitBond.kernel k n L) 0

theorem QuantumBlockEncoding.StoredHermiteRawSource.tables_window
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.StoredMatrixProductChain.Window
    (QuantumBlockEncoding.StoredHermiteRawSource.tables
          (QuantumBlockEncoding.StoredHermiteSourceCache.compile
                k n
                L).run.value).run.value
    (QuantumBlockEncoding.HermiteExplicitBond.kernel
      k n L)
    0

Definition10.65.8

uses 0used by 0✓L∃∀N

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

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/StoredHermiteRawSource.lean:69. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.65.8●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete

def QuantumBlockEncoding.StoredHermiteRawSource.boundaryInputs {k n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n) :
  QuantumBlockEncoding.StoredGivens.Run (ℕ × ℕ)

def QuantumBlockEncoding.StoredHermiteRawSource.boundaryInputs
  {k n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n) :
  QuantumBlockEncoding.StoredGivens.Run
    (ℕ × ℕ)

Definition10.65.9

uses 0used by 0✓L∃∀N

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

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/StoredHermiteRawSource.lean:76. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.65.9●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete

def QuantumBlockEncoding.StoredHermiteRawSource.boundaries {k n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ (2 * k + 6) × Vector ℝ (2 * k + 6))

def QuantumBlockEncoding.StoredHermiteRawSource.boundaries
  {k n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ (2 * k + 6) ×
      Vector ℝ (2 * k + 6))

Theorem10.65.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.65.10●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawSource.boundaries_initial (k n : ℕ)
  (L : ℝ) (hL : 0 < L) (i : Fin (2 * k + 6)) :
  (QuantumBlockEncoding.StoredHermiteRawSource.boundaries
            (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
                  L).run.value).value.1[↑i] =
    QuantumBlockEncoding.HermiteExplicitBond.initial k n L i

theorem QuantumBlockEncoding.StoredHermiteRawSource.boundaries_initial
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (i : Fin (2 * k + 6)) :
  (QuantumBlockEncoding.StoredHermiteRawSource.boundaries
            (QuantumBlockEncoding.StoredHermiteSourceCache.compile
                  k n
                  L).run.value).value.1[↑i] =
    QuantumBlockEncoding.HermiteExplicitBond.initial
      k n L i

Theorem10.65.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.65.11●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawSource.boundaries_terminal
  (k n : ℕ) (L : ℝ) (i : Fin (2 * k + 6)) :
  (QuantumBlockEncoding.StoredHermiteRawSource.boundaries
            (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
                  L).run.value).value.2[↑i] =
    QuantumBlockEncoding.HermiteExplicitBond.terminal k i

theorem QuantumBlockEncoding.StoredHermiteRawSource.boundaries_terminal
  (k n : ℕ) (L : ℝ)
  (i : Fin (2 * k + 6)) :
  (QuantumBlockEncoding.StoredHermiteRawSource.boundaries
            (QuantumBlockEncoding.StoredHermiteSourceCache.compile
                  k n
                  L).run.value).value.2[↑i] =
    QuantumBlockEncoding.HermiteExplicitBond.terminal
      k i

Definition10.65.12

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “raw run”. A proposition-valued field is a requirement until a constructor supplies it.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

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. structure.

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

Lean code for Definition10.65.12●1 definition

structure(extends 2, 6 fields)defined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete
structure QuantumBlockEncoding.StoredHermiteRawSource.RawRun (α : Type) : Type
structure QuantumBlockEncoding.StoredHermiteRawSource.RawRun (α : Type) : Type
Extends
- QuantumBlockEncoding.StoredHermiteSourceCache.CacheRun α
Fields
run : QuantumBlockEncoding.StoredGivens.Run α
Inherited from

QuantumBlockEncoding.StoredHermiteSourceCache.CacheRun

QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun
exponentialCalls : ℕ
Inherited from

QuantumBlockEncoding.StoredHermiteSourceCache.CacheRun

QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun
quotientCalls : ℕ
Inherited from

QuantumBlockEncoding.StoredHermiteSourceCache.CacheRun
remainderCalls : ℕ
Inherited from

QuantumBlockEncoding.StoredHermiteSourceCache.CacheRun
integerDoublings : ℕ
Inherited from

QuantumBlockEncoding.StoredHermiteSourceCache.CacheRun
integerAdditions : ℕ

Definition10.65.13

uses 0used by 0✓L∃∀N

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

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/StoredHermiteRawSource.lean:105. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.65.13●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete

def QuantumBlockEncoding.StoredHermiteRawSource.raw (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredHermiteRawSource.RawRun
    (QuantumBlockEncoding.StoredTensorTrain.StoredChain (n + 1) 1 1)

def QuantumBlockEncoding.StoredHermiteRawSource.raw
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredHermiteRawSource.RawRun
    (QuantumBlockEncoding.StoredTensorTrain.StoredChain
      (n + 1) 1 1)

Theorem10.65.14

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.65.14●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawSource.raw_value (k n : ℕ) (L : ℝ)
  (hL : 0 < L) :
  QuantumBlockEncoding.StoredTensorTrain.denoteChain
      (QuantumBlockEncoding.StoredHermiteRawSource.raw k n
            L).run.value =
    QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain k n L

theorem QuantumBlockEncoding.StoredHermiteRawSource.raw_value
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.StoredTensorTrain.denoteChain
      (QuantumBlockEncoding.StoredHermiteRawSource.raw
            k n L).run.value =
    QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain
      k n L

Theorem10.65.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.65.15●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawSource.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawSource.raw_contract (k n : ℕ)
  (L : ℝ) (hL : 0 < L)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain
        (QuantumBlockEncoding.StoredHermiteRawSource.raw k n
              L).run.value)
      x 0 0 =
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
      (n + 1) L
      ((QuantumBlockEncoding.TensorTrainWord.sampleEquiv (n + 1)) x)

theorem QuantumBlockEncoding.StoredHermiteRawSource.raw_contract
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain
        (QuantumBlockEncoding.StoredHermiteRawSource.raw
              k n L).run.value)
      x 0 0 =
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
      k (n + 1) L
      ((QuantumBlockEncoding.TensorTrainWord.sampleEquiv
          (n + 1))
        x)

10.65. QuantumBlockEncoding/StoredHermiteRawSource.lean🔗

Extends

Fields

Extends

Fields