6.43. QuantumBlockEncoding/TensorTrainNormEnvironment.lean🔗

15 explicit public declarations, in source order.

Definition6.43.1

uses 0used by 0✓L∃∀N

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

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. Right Gram environment. Each update uses only two local matrix products per physical bit, with the previous environment as its right factor.

Declaration kind. def.

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

Lean code for Definition6.43.1●1 definition

defdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

def QuantumBlockEncoding.TensorTrainNormEnvironment.gram {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain n l r →
    Matrix (Fin l) (Fin l) ℝ

def QuantumBlockEncoding.TensorTrainNormEnvironment.gram
  {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r →
    Matrix (Fin l) (Fin l) ℝ

Right Gram environment. Each update uses only two local matrix products
per physical bit, with the previous environment as its right factor.

Theorem6.43.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “gram eq sum”; the hypotheses and conclusion in the code panel fix its exact scope. Exact semantics of the small-matrix recursion, including every terminal bond label.

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

Technical source note. Exact semantics of the small-matrix recursion, including every terminal bond label. The full word sum appears only in the specification.

Declaration kind. theorem.

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

Lean code for Theorem6.43.2●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.gram_eq_sum {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.gram C =
    ∑ x,
      QuantumBlockEncoding.TensorTrainCanonical.contract C x *
        (QuantumBlockEncoding.TensorTrainCanonical.contract C
            x).transpose

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.gram_eq_sum
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.gram
      C =
    ∑ x,
      QuantumBlockEncoding.TensorTrainCanonical.contract
          C x *
        (QuantumBlockEncoding.TensorTrainCanonical.contract
            C x).transpose

Exact semantics of the small-matrix recursion, including every terminal
bond label. The full word sum appears only in the specification.

Theorem6.43.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “gram scalar”; the hypotheses and conclusion in the code panel fix its exact scope. A scalar-boundary train's environment entry is its complete squared norm.

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

Technical source note. A scalar-boundary train's environment entry is its complete squared norm.

Declaration kind. theorem.

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

Lean code for Theorem6.43.3●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.gram_scalar {n : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n 1 1) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.gram C 0 0 =
    ∑ x, QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0 ^ 2

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.gram_scalar
  {n : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n 1 1) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.gram
      C 0 0 =
    ∑ x,
      QuantumBlockEncoding.TensorTrainCanonical.contract
          C x 0 0 ^
        2

A scalar-boundary train's environment entry is its complete squared norm.

Theorem6.43.4

uses 0used by 0✓L∃∀N

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

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

Lean code for Theorem6.43.4●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.gram_scalar_nonneg
  {n : ℕ} (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n 1 1) :
  0 ≤ QuantumBlockEncoding.TensorTrainNormEnvironment.gram C 0 0

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.gram_scalar_nonneg
  {n : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n 1 1) :
  0 ≤
    QuantumBlockEncoding.TensorTrainNormEnvironment.gram
      C 0 0

Definition6.43.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “norm”. Local-core norm supplier; only one square root is performed after the Gram recursion.

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. Local-core norm supplier; only one square root is performed after the Gram recursion. This is meaningful for zero trains as well as normalized trains.

Declaration kind. def.

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

Lean code for Definition6.43.5●1 definition

defdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

def QuantumBlockEncoding.TensorTrainNormEnvironment.norm {n : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n 1 1) : ℝ

def QuantumBlockEncoding.TensorTrainNormEnvironment.norm
  {n : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n 1 1) :
  ℝ

Local-core norm supplier; only one square root is performed after the Gram
recursion. This is meaningful for zero trains as well as normalized trains.

Theorem6.43.6

uses 0used by 0✓L∃∀N

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

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

Lean code for Theorem6.43.6●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.norm_eq {n : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n 1 1) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.norm C =
    √(∑ x,
        QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0 ^ 2)

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.norm_eq
  {n : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n 1 1) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.norm
      C =
    √(∑ x,
        QuantumBlockEncoding.TensorTrainCanonical.contract
            C x 0 0 ^
          2)

Theorem6.43.7

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.43.7●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.norm_sq {n : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n 1 1) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.norm C ^ 2 =
    ∑ x, QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0 ^ 2

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.norm_sq
  {n : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n 1 1) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.norm
        C ^
      2 =
    ∑ x,
      QuantumBlockEncoding.TensorTrainCanonical.contract
          C x 0 0 ^
        2

Theorem6.43.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.43.8●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.norm_pos_of_nonzero
  {n : ℕ} (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n 1 1)
  (h :
    ∃ x,
      QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0 ≠ 0) :
  0 < QuantumBlockEncoding.TensorTrainNormEnvironment.norm C

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.norm_pos_of_nonzero
  {n : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n 1 1)
  (h :
    ∃ x,
      QuantumBlockEncoding.TensorTrainCanonical.contract
          C x 0 0 ≠
        0) :
  0 <
    QuantumBlockEncoding.TensorTrainNormEnvironment.norm
      C

Theorem6.43.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “norm eq of contract”; the hypotheses and conclusion in the code panel fix its exact scope. A reusable target adapter.

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

Technical source note. A reusable target adapter. This identifies a proven core action with the target norm; it does not assume the norm supplier is already correct.

Declaration kind. theorem.

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

Lean code for Theorem6.43.9●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.norm_eq_of_contract.{u_1}
  {n : ℕ} {I : Type u_1} [Fintype I]
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n 1 1)
  (e : QuantumBlockEncoding.TensorTrainCanonical.Word n ≃ I)
  (target : I → ℝ)
  (h :
    ∀ (x : QuantumBlockEncoding.TensorTrainCanonical.Word n),
      QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0 =
        target (e x)) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.norm C =
    √(∑ i, target i ^ 2)

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.norm_eq_of_contract.{u_1}
  {n : ℕ} {I : Type u_1} [Fintype I]
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n 1 1)
  (e :
    QuantumBlockEncoding.TensorTrainCanonical.Word
        n ≃
      I)
  (target : I → ℝ)
  (h :
    ∀
      (x :
        QuantumBlockEncoding.TensorTrainCanonical.Word
          n),
      QuantumBlockEncoding.TensorTrainCanonical.contract
          C x 0 0 =
        target (e x)) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.norm
      C =
    √(∑ i, target i ^ 2)

A reusable target adapter. This identifies a proven core action with the
target norm; it does not assume the norm supplier is already correct.

Definition6.43.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “environment scalars”. Storage if every intermediate environment is retained.

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. Storage if every intermediate environment is retained. Streaming can use less; no exponential word address occurs in this definition.

Declaration kind. def.

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

Lean code for Definition6.43.10●1 definition

defdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

def QuantumBlockEncoding.TensorTrainNormEnvironment.environmentScalars
  {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain n l r → ℕ

def QuantumBlockEncoding.TensorTrainNormEnvironment.environmentScalars
  {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r →
    ℕ

Storage if every intermediate environment is retained. Streaming can use
less; no exponential word address occurs in this definition.

Theorem6.43.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.43.11●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.environmentScalars_le
  {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) (D : ℕ)
  (hD : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ D) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.environmentScalars C ≤
    (n + 1) * D ^ 2

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.environmentScalars_le
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (D : ℕ)
  (hD :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      D) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.environmentScalars
      C ≤
    (n + 1) * D ^ 2

Definition6.43.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “update arithmetic budget”. A conservative count for direct dense real arithmetic at one update: two bits, products (l by m)*(m by m) and (l by m)*(m by l), charging one multiplication and at most one addition per inner-product term, then l^2 additions to combine the two bits.

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 conservative count for direct dense real arithmetic at one update: two bits, products (l by m)*(m by m) and (l by m)*(m by l), charging one multiplication and at most one addition per inner-product term, then l^2 additions to combine the two bits. Copies/transposes are index views.

Declaration kind. def.

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

Lean code for Definition6.43.12●1 definition

defdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

def QuantumBlockEncoding.TensorTrainNormEnvironment.updateArithmeticBudget
  (l m : ℕ) : ℕ

def QuantumBlockEncoding.TensorTrainNormEnvironment.updateArithmeticBudget
  (l m : ℕ) : ℕ

A conservative count for direct dense real arithmetic at one update:
two bits, products (l by m)*(m by m) and (l by m)*(m by l), charging
one multiplication and at most one addition per inner-product term, then
l^2 additions to combine the two bits. Copies/transposes are index views.

Definition6.43.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “arithmetic budget”. Syntactic real-operation budget of the stated local evaluation schedule.

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. Syntactic real-operation budget of the stated local evaluation schedule. This is not a cost semantics for an external runtime or finite-bit arithmetic.

Declaration kind. def.

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

Lean code for Definition6.43.13●1 definition

defdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

def QuantumBlockEncoding.TensorTrainNormEnvironment.arithmeticBudget
  {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain n l r → ℕ

def QuantumBlockEncoding.TensorTrainNormEnvironment.arithmeticBudget
  {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r →
    ℕ

Syntactic real-operation budget of the stated local evaluation schedule.
This is not a cost semantics for an external runtime or finite-bit arithmetic.

Theorem6.43.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “update arithmetic budget 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/TensorTrainNormEnvironment.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.43.14●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.updateArithmeticBudget_le
  (l m D : ℕ) (hl : l ≤ D) (hm : m ≤ D) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.updateArithmeticBudget
      l m ≤
    9 * D ^ 3

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.updateArithmeticBudget_le
  (l m D : ℕ) (hl : l ≤ D) (hm : m ≤ D) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.updateArithmeticBudget
      l m ≤
    9 * D ^ 3

Theorem6.43.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.43.15●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainNormEnvironment.lean

complete

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.arithmeticBudget_le
  {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) (D : ℕ)
  (hD : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ D) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.arithmeticBudget C ≤
    9 * n * D ^ 3

theorem QuantumBlockEncoding.TensorTrainNormEnvironment.arithmeticBudget_le
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (D : ℕ)
  (hD :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      D) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.arithmeticBudget
      C ≤
    9 * n * D ^ 3