QuantumBlockEncoding/HermiteFiniteNorm.lean

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

noncomputable def rawInitial (k n : Nat) (L : ℝ) : Fin (2 * k + 6) → ℝ :=
  fun a => hermiteInitial k n L (bondEquiv k a)

/-- A scalar-boundary source representation without a precomputed normalizer. -/

commit-pinned source · Verso Blueprint panel

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

noncomputable def rawSourceChain (k n : Nat) (L : ℝ) : Chain (n + 1) 1 1 :=
  MatrixProductChain.ofKernel (kernel k n L) (rawInitial k n L) (terminal k) 0 n

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “raw source chain contract”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rawSourceChain_contract (k n : Nat) (L : ℝ) (hL : 0 < L)
    (x : Word (n + 1)) :
    contract (rawSourceChain k n L) x 0 0 =
      HermiteStatePreparation.sampledAmplitude k (n + 1) L (sampleEquiv (n + 1) x) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “raw source chain max bond”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rawSourceChain_maxBond (k n : Nat) (L : ℝ) :
    maxBond (rawSourceChain k n L) ≤ 2 * k + 6 := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def localSampleNorm (k n : Nat) (L : ℝ) : ℝ :=
  TensorTrainNormEnvironment.norm (rawSourceChain k n L)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “local sample norm eq sample norm”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem localSampleNorm_eq_sampleNorm (k n : Nat) (L : ℝ) (hL : 0 < L) :
    localSampleNorm k n L = HermiteStatePreparation.sampleNorm k (n + 1) L :=
  TensorTrainNormEnvironment.norm_eq_of_contract (rawSourceChain k n L)
    (sampleEquiv (n + 1)) (HermiteStatePreparation.sampledAmplitude k (n + 1) L)
    (rawSourceChain_contract k n L hL)

commit-pinned source · Verso Blueprint panel

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

theorem localSampleNorm_pos (k n : Nat) (L : ℝ) (hL : 0 < L) :
    0 < localSampleNorm k n L := by

commit-pinned source · Verso Blueprint panel

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

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

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “raw source chain storage”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rawSourceChain_storage (k n : Nat) (L : ℝ) :
    MatrixProductChain.storedScalars (rawSourceChain k n L) ≤
      2 * (n + 1) * (2 * k + 6) ^ 2 :=
  MatrixProductChain.storedScalars_le _ _ (rawSourceChain_maxBond k n L)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “norm environment storage”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem norm_environment_storage (k n : Nat) (L : ℝ) :
    TensorTrainNormEnvironment.environmentScalars (rawSourceChain k n L) ≤
      (n + 2) * (2 * k + 6) ^ 2 :=
  TensorTrainNormEnvironment.environmentScalars_le _ _ (rawSourceChain_maxBond k n L)

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

commit-pinned source · Verso Blueprint panel

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

theorem norm_arithmetic_budget (k n : Nat) (L : ℝ) :
    TensorTrainNormEnvironment.arithmeticBudget (rawSourceChain k n L) ≤
      9 * (n + 1) * (2 * k + 6) ^ 3 :=
  TensorTrainNormEnvironment.arithmeticBudget_le _ _ (rawSourceChain_maxBond k n L)

commit-pinned source · Verso Blueprint panel