6.38. QuantumBlockEncoding/StoredTensorTrainNorm.lean🔗

29 explicit public declarations, in source order.

Definition6.38.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “first entry”. The first pass computes one entry of 'A_bit * E'.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. The first pass computes one entry of 'A_bit * E'.

Declaration kind. def.

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

Lean code for Definition6.38.1●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

def QuantumBlockEncoding.StoredTensorTrainNorm.firstEntry {l m : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (E : QuantumBlockEncoding.StoredGivens.StoredMatrix m m) (bit : Fin 2)
  (a : Fin l) (j : Fin m) : QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredTensorTrainNorm.firstEntry
  {l m : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (E :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m m)
  (bit : Fin 2) (a : Fin l) (j : Fin m) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

The first pass computes one entry of `A_bit * E`.

Definition6.38.2

uses 0used by 0✓L∃∀N

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

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

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

Lean code for Definition6.38.2●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

def QuantumBlockEncoding.StoredTensorTrainNorm.firstPass {l m : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (E : QuantumBlockEncoding.StoredGivens.StoredMatrix m m)
  (bit : Fin 2) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix l m)

def QuantumBlockEncoding.StoredTensorTrainNorm.firstPass
  {l m : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (E :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m m)
  (bit : Fin 2) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      l m)

Theorem6.38.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “first pass 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.

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

Lean code for Theorem6.38.3●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.firstPass_value {l m : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (E : QuantumBlockEncoding.StoredGivens.StoredMatrix m m)
  (bit : Fin 2) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredTensorTrainNorm.firstPass A E
          bit).value =
    QuantumBlockEncoding.TensorTrainCanonical.slice
        (QuantumBlockEncoding.StoredTensorTrain.denoteCore A) bit *
      QuantumBlockEncoding.StoredGivens.denote E

theorem QuantumBlockEncoding.StoredTensorTrainNorm.firstPass_value
  {l m : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (E :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m m)
  (bit : Fin 2) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredTensorTrainNorm.firstPass
          A E bit).value =
    QuantumBlockEncoding.TensorTrainCanonical.slice
        (QuantumBlockEncoding.StoredTensorTrain.denoteCore
          A)
        bit *
      QuantumBlockEncoding.StoredGivens.denote
        E

Definition6.38.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “second entry”. The second pass reads the stored first pass and the original core.

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

Technical source note. The second pass reads the stored first pass and the original core. The transpose is an index exchange, not an uncharged matrix constructor.

Declaration kind. def.

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

Lean code for Definition6.38.4●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

def QuantumBlockEncoding.StoredTensorTrainNorm.secondEntry {l m : ℕ}
  (F : QuantumBlockEncoding.StoredGivens.StoredMatrix l m)
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (bit : Fin 2) (a c : Fin l) : QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredTensorTrainNorm.secondEntry
  {l m : ℕ}
  (F :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      l m)
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (bit : Fin 2) (a c : Fin l) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

The second pass reads the stored first pass and the original core.
The transpose is an index exchange, not an uncharged matrix constructor.

Definition6.38.5

uses 0used by 0✓L∃∀N

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

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

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

Lean code for Definition6.38.5●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

def QuantumBlockEncoding.StoredTensorTrainNorm.secondPass {l m : ℕ}
  (F : QuantumBlockEncoding.StoredGivens.StoredMatrix l m)
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (bit : Fin 2) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix l l)

def QuantumBlockEncoding.StoredTensorTrainNorm.secondPass
  {l m : ℕ}
  (F :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      l m)
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (bit : Fin 2) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      l l)

Theorem6.38.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “second pass 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.

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

Lean code for Theorem6.38.6●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.secondPass_value {l m : ℕ}
  (F : QuantumBlockEncoding.StoredGivens.StoredMatrix l m)
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (bit : Fin 2) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredTensorTrainNorm.secondPass F A
          bit).value =
    QuantumBlockEncoding.StoredGivens.denote F *
      (QuantumBlockEncoding.TensorTrainCanonical.slice
          (QuantumBlockEncoding.StoredTensorTrain.denoteCore A)
          bit).transpose

theorem QuantumBlockEncoding.StoredTensorTrainNorm.secondPass_value
  {l m : ℕ}
  (F :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      l m)
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (bit : Fin 2) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredTensorTrainNorm.secondPass
          F A bit).value =
    QuantumBlockEncoding.StoredGivens.denote
        F *
      (QuantumBlockEncoding.TensorTrainCanonical.slice
          (QuantumBlockEncoding.StoredTensorTrain.denoteCore
            A)
          bit).transpose

Definition6.38.7

uses 0used by 0✓L∃∀N

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

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

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

Lean code for Definition6.38.7●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

def QuantumBlockEncoding.StoredTensorTrainNorm.addMatrices {l : ℕ}
  (A B : QuantumBlockEncoding.StoredGivens.StoredMatrix l l) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix l l)

def QuantumBlockEncoding.StoredTensorTrainNorm.addMatrices
  {l : ℕ}
  (A B :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      l l) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      l l)

Theorem6.38.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “add matrices 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.

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

Lean code for Theorem6.38.8●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.addMatrices_value {l : ℕ}
  (A B : QuantumBlockEncoding.StoredGivens.StoredMatrix l l) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredTensorTrainNorm.addMatrices A
          B).value =
    QuantumBlockEncoding.StoredGivens.denote A +
      QuantumBlockEncoding.StoredGivens.denote B

theorem QuantumBlockEncoding.StoredTensorTrainNorm.addMatrices_value
  {l : ℕ}
  (A B :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      l l) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredTensorTrainNorm.addMatrices
          A B).value =
    QuantumBlockEncoding.StoredGivens.denote
        A +
      QuantumBlockEncoding.StoredGivens.denote
        B

Definition6.38.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “update”. All four contraction outputs and the sum are materialized.

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

Technical source note. All four contraction outputs and the sum are materialized. The two uses of 'E' are stored reads of the same cached environment.

Declaration kind. def.

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

Lean code for Definition6.38.9●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

def QuantumBlockEncoding.StoredTensorTrainNorm.update {l m : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (E : QuantumBlockEncoding.StoredGivens.StoredMatrix m m) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix l l)

def QuantumBlockEncoding.StoredTensorTrainNorm.update
  {l m : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (E :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m m) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      l l)

All four contraction outputs and the sum are materialized.
The two uses of `E` are stored reads of the same cached environment.

Theorem6.38.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “update 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.

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

Lean code for Theorem6.38.10●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.update_value {l m : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (E : QuantumBlockEncoding.StoredGivens.StoredMatrix m m) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredTensorTrainNorm.update A E).value =
    ∑ bit,
      QuantumBlockEncoding.TensorTrainCanonical.slice
            (QuantumBlockEncoding.StoredTensorTrain.denoteCore A) bit *
          QuantumBlockEncoding.StoredGivens.denote E *
        (QuantumBlockEncoding.TensorTrainCanonical.slice
            (QuantumBlockEncoding.StoredTensorTrain.denoteCore A)
            bit).transpose

theorem QuantumBlockEncoding.StoredTensorTrainNorm.update_value
  {l m : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (E :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m m) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredTensorTrainNorm.update
          A E).value =
    ∑ bit,
      QuantumBlockEncoding.TensorTrainCanonical.slice
            (QuantumBlockEncoding.StoredTensorTrain.denoteCore
              A)
            bit *
          QuantumBlockEncoding.StoredGivens.denote
            E *
        (QuantumBlockEncoding.TensorTrainCanonical.slice
            (QuantumBlockEncoding.StoredTensorTrain.denoteCore
              A)
            bit).transpose

Definition6.38.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cache node”. A fixed six-word traversal/cache-record allowance per chain node, as in the stored canonicalizer.

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

Technical source note. A fixed six-word traversal/cache-record allowance per chain node, as in the stored canonicalizer. Matrix copying is charged separately by each pass.

Declaration kind. def.

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

Lean code for Definition6.38.11●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

def QuantumBlockEncoding.StoredTensorTrainNorm.cacheNode {α : Type}
  (run : QuantumBlockEncoding.StoredGivens.Run α) :
  QuantumBlockEncoding.StoredGivens.Run α

def QuantumBlockEncoding.StoredTensorTrainNorm.cacheNode
  {α : Type}
  (run :
    QuantumBlockEncoding.StoredGivens.Run
      α) :
  QuantumBlockEncoding.StoredGivens.Run α

A fixed six-word traversal/cache-record allowance per chain node, as in
the stored canonicalizer. Matrix copying is charged separately by each pass.

Definition6.38.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “gram”. Streaming cached Gram environments.

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

Technical source note. Streaming cached Gram environments. The recursive result is bound once and remains a stored matrix throughout the two physical-bit updates.

Declaration kind. def.

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

Lean code for Definition6.38.12●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

def QuantumBlockEncoding.StoredTensorTrainNorm.gram {n l r : ℕ} :
  QuantumBlockEncoding.StoredTensorTrain.StoredChain n l r →
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredGivens.StoredMatrix l l)

def QuantumBlockEncoding.StoredTensorTrainNorm.gram
  {n l r : ℕ} :
  QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n l r →
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredGivens.StoredMatrix
        l l)

Streaming cached Gram environments. The recursive result is bound once
and remains a stored matrix throughout the two physical-bit updates.

Theorem6.38.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “gram 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.

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

Lean code for Theorem6.38.13●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.gram_value {n l r : ℕ}
  (C : QuantumBlockEncoding.StoredTensorTrain.StoredChain n l r) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredTensorTrainNorm.gram C).value =
    QuantumBlockEncoding.TensorTrainNormEnvironment.gram
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain C)

theorem QuantumBlockEncoding.StoredTensorTrainNorm.gram_value
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n l r) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredTensorTrainNorm.gram
          C).value =
    QuantumBlockEncoding.TensorTrainNormEnvironment.gram
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain
        C)

Definition6.38.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “norm”. Scalar-boundary norm with the final table lookup and square root charged.

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

Technical source note. Scalar-boundary norm with the final table lookup and square root charged.

Declaration kind. def.

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

Lean code for Definition6.38.14●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

def QuantumBlockEncoding.StoredTensorTrainNorm.norm {n : ℕ}
  (C : QuantumBlockEncoding.StoredTensorTrain.StoredChain n 1 1) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredTensorTrainNorm.norm
  {n : ℕ}
  (C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n 1 1) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Scalar-boundary norm with the final table lookup and square root charged.

Theorem6.38.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “norm 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.

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

Lean code for Theorem6.38.15●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.norm_value {n : ℕ}
  (C : QuantumBlockEncoding.StoredTensorTrain.StoredChain n 1 1) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.norm C).value =
    QuantumBlockEncoding.TensorTrainNormEnvironment.norm
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain C)

theorem QuantumBlockEncoding.StoredTensorTrainNorm.norm_value
  {n : ℕ}
  (C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n 1 1) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.norm
        C).value =
    QuantumBlockEncoding.TensorTrainNormEnvironment.norm
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain
        C)

Theorem6.38.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “norm 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.

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

Lean code for Theorem6.38.16●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.norm_eq_sum {n : ℕ}
  (C : QuantumBlockEncoding.StoredTensorTrain.StoredChain n 1 1) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.norm C).value =
    √(∑ x,
        QuantumBlockEncoding.TensorTrainCanonical.contract
            (QuantumBlockEncoding.StoredTensorTrain.denoteChain C) x 0
            0 ^
          2)

theorem QuantumBlockEncoding.StoredTensorTrainNorm.norm_eq_sum
  {n : ℕ}
  (C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n 1 1) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.norm
        C).value =
    √(∑ x,
        QuantumBlockEncoding.TensorTrainCanonical.contract
            (QuantumBlockEncoding.StoredTensorTrain.denoteChain
              C)
            x 0 0 ^
          2)

Definition6.38.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “product budget”. Scalar-boundary norm with the final table lookup and square root charged.

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

Technical source note. Scalar-boundary norm with the final table lookup and square root charged. -/ noncomputable def norm {n : ℕ} (C : StoredChain n 1 1) : Run ℝ := do let E ← gram C let mass ← StoredThinLQ.entry E 0 0 StoredGivens.sqrt mass theorem norm_value {n : ℕ} (C : StoredChain n 1 1) : (norm C).value = TensorTrainNormEnvironment.norm (denoteChain C) := by change Real.sqrt (denote (gram C).value 0 0) = _ rw [gram_value] rfl theorem norm_eq_sum {n : ℕ} (C : StoredChain n 1 1) : (norm C).value = Real.sqrt (∑ x : Word n, contract (denoteChain C) x 0 0 ^ 2) := (norm_value C).trans (TensorTrainNormEnvironment.norm_eq (denoteChain C)) /-! number number Operation counts for the same producer

Declaration kind. def.

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

Lean code for Definition6.38.17●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

def QuantumBlockEncoding.StoredTensorTrainNorm.productBudget (l m r : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredTensorTrainNorm.productBudget
  (l m r : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Definition6.38.18

uses 0used by 0✓L∃∀N

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

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

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

Lean code for Definition6.38.18●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

def QuantumBlockEncoding.StoredTensorTrainNorm.additionBudget (l : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredTensorTrainNorm.additionBudget
  (l : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Definition6.38.19

uses 0used by 0✓L∃∀N

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

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

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

Lean code for Definition6.38.19●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

def QuantumBlockEncoding.StoredTensorTrainNorm.updateBudget (l m : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredTensorTrainNorm.updateBudget
  (l m : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.38.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “first entry cost le”; 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.

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

Lean code for Theorem6.38.20●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.firstEntry_cost_le {l m : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (E : QuantumBlockEncoding.StoredGivens.StoredMatrix m m) (bit : Fin 2)
  (a : Fin l) (j : Fin m) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.firstEntry A E bit a
          j).cost
      op ≤
    m *
      (4 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.field op)

theorem QuantumBlockEncoding.StoredTensorTrainNorm.firstEntry_cost_le
  {l m : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (E :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m m)
  (bit : Fin 2) (a : Fin l) (j : Fin m)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.firstEntry
          A E bit a j).cost
      op ≤
    m *
      (4 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read
            op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.field
            op)

Theorem6.38.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “second entry cost le”; 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.

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

Lean code for Theorem6.38.21●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.secondEntry_cost_le {l m : ℕ}
  (F : QuantumBlockEncoding.StoredGivens.StoredMatrix l m)
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (bit : Fin 2) (a c : Fin l)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.secondEntry F A bit a
          c).cost
      op ≤
    m *
      (4 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.field op)

theorem QuantumBlockEncoding.StoredTensorTrainNorm.secondEntry_cost_le
  {l m : ℕ}
  (F :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      l m)
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (bit : Fin 2) (a c : Fin l)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.secondEntry
          F A bit a c).cost
      op ≤
    m *
      (4 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read
            op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.field
            op)

Theorem6.38.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “first pass cost le”; 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.

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

Lean code for Theorem6.38.22●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.firstPass_cost_le {l m : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (E : QuantumBlockEncoding.StoredGivens.StoredMatrix m m) (bit : Fin 2)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.firstPass A E bit).cost
      op ≤
    QuantumBlockEncoding.StoredTensorTrainNorm.productBudget l m m op

theorem QuantumBlockEncoding.StoredTensorTrainNorm.firstPass_cost_le
  {l m : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (E :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m m)
  (bit : Fin 2)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.firstPass
          A E bit).cost
      op ≤
    QuantumBlockEncoding.StoredTensorTrainNorm.productBudget
      l m m op

Theorem6.38.23

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “second pass cost le”; 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.

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

Lean code for Theorem6.38.23●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.secondPass_cost_le {l m : ℕ}
  (F : QuantumBlockEncoding.StoredGivens.StoredMatrix l m)
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (bit : Fin 2) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.secondPass F A bit).cost
      op ≤
    QuantumBlockEncoding.StoredTensorTrainNorm.productBudget l m l op

theorem QuantumBlockEncoding.StoredTensorTrainNorm.secondPass_cost_le
  {l m : ℕ}
  (F :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      l m)
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (bit : Fin 2)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.secondPass
          F A bit).cost
      op ≤
    QuantumBlockEncoding.StoredTensorTrainNorm.productBudget
      l m l op

Theorem6.38.24

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “add matrices cost le”; 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.

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

Lean code for Theorem6.38.24●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.addMatrices_cost_le {l : ℕ}
  (A B : QuantumBlockEncoding.StoredGivens.StoredMatrix l l)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.addMatrices A B).cost op ≤
    QuantumBlockEncoding.StoredTensorTrainNorm.additionBudget l op

theorem QuantumBlockEncoding.StoredTensorTrainNorm.addMatrices_cost_le
  {l : ℕ}
  (A B :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      l l)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.addMatrices
          A B).cost
      op ≤
    QuantumBlockEncoding.StoredTensorTrainNorm.additionBudget
      l op

Theorem6.38.25

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “update cost le”; 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.

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

Lean code for Theorem6.38.25●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.update_cost_le {l m : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (E : QuantumBlockEncoding.StoredGivens.StoredMatrix m m)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.update A E).cost op ≤
    QuantumBlockEncoding.StoredTensorTrainNorm.updateBudget l m op

theorem QuantumBlockEncoding.StoredTensorTrainNorm.update_cost_le
  {l m : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (E :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m m)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.update
          A E).cost
      op ≤
    QuantumBlockEncoding.StoredTensorTrainNorm.updateBudget
      l m op

Theorem6.38.26

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “update total cost le”; 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.

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

Lean code for Theorem6.38.26●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.update_total_cost_le
  {l m : ℕ} (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (E : QuantumBlockEncoding.StoredGivens.StoredMatrix m m) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredTensorTrainNorm.update A E).cost ≤
    12 * l * m * m + 12 * l * l * m + 8 * l * m + 17 * l * l + 20 * l

theorem QuantumBlockEncoding.StoredTensorTrainNorm.update_total_cost_le
  {l m : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (E :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m m) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredTensorTrainNorm.update
          A E).cost ≤
    12 * l * m * m + 12 * l * l * m +
          8 * l * m +
        17 * l * l +
      20 * l

Theorem6.38.27

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “gram total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. Total of all eight counters, including every materialization pass and the fixed node records.

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

Technical source note. Total of all eight counters, including every materialization pass and the fixed node records. The bond bound concerns the already stored input chain.

Declaration kind. theorem.

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

Lean code for Theorem6.38.27●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.gram_total_cost_le
  {n l r : ℕ}
  (C : QuantumBlockEncoding.StoredTensorTrain.StoredChain n l r) (D : ℕ)
  (bound :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        (QuantumBlockEncoding.StoredTensorTrain.denoteChain C) ≤
      D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredTensorTrainNorm.gram C).cost ≤
    n * (24 * D ^ 3 + 25 * D ^ 2 + 20 * D + 6) + 5 * D ^ 2 + 4 * D + 6

theorem QuantumBlockEncoding.StoredTensorTrainNorm.gram_total_cost_le
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n l r)
  (D : ℕ)
  (bound :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        (QuantumBlockEncoding.StoredTensorTrain.denoteChain
          C) ≤
      D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredTensorTrainNorm.gram
          C).cost ≤
    n *
            (24 * D ^ 3 + 25 * D ^ 2 +
                20 * D +
              6) +
          5 * D ^ 2 +
        4 * D +
      6

Total of all eight counters, including every materialization pass and the
fixed node records. The bond bound concerns the already stored input chain.

Theorem6.38.28

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “norm cost”; 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.

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

Lean code for Theorem6.38.28●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.norm_cost {n : ℕ}
  (C : QuantumBlockEncoding.StoredTensorTrain.StoredChain n 1 1)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.norm C).cost op =
    (QuantumBlockEncoding.StoredTensorTrainNorm.gram C).cost op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read op +
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.sqrt op

theorem QuantumBlockEncoding.StoredTensorTrainNorm.norm_cost
  {n : ℕ}
  (C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n 1 1)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrainNorm.norm
          C).cost
      op =
    (QuantumBlockEncoding.StoredTensorTrainNorm.gram
              C).cost
          op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read
            op +
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.sqrt
        op

Theorem6.38.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “norm total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. The scalar supplier adds precisely two stored reads and one square root.

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

Technical source note. The scalar supplier adds precisely two stored reads and one square root.

Declaration kind. theorem.

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

Lean code for Theorem6.38.29●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrainNorm.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrainNorm.norm_total_cost_le {n : ℕ}
  (C : QuantumBlockEncoding.StoredTensorTrain.StoredChain n 1 1) (D : ℕ)
  (bound :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        (QuantumBlockEncoding.StoredTensorTrain.denoteChain C) ≤
      D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredTensorTrainNorm.norm C).cost ≤
    n * (24 * D ^ 3 + 25 * D ^ 2 + 20 * D + 6) + 5 * D ^ 2 + 4 * D + 9

theorem QuantumBlockEncoding.StoredTensorTrainNorm.norm_total_cost_le
  {n : ℕ}
  (C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n 1 1)
  (D : ℕ)
  (bound :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        (QuantumBlockEncoding.StoredTensorTrain.denoteChain
          C) ≤
      D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredTensorTrainNorm.norm
          C).cost ≤
    n *
            (24 * D ^ 3 + 25 * D ^ 2 +
                20 * D +
              6) +
          5 * D ^ 2 +
        4 * D +
      9

The scalar supplier adds precisely two stored reads and one square root.