QuantumBlockEncoding/TensorTrainWord.lean

This definition gives the library's named construction or computation for “to basis”.

def toBasis : {n : Nat} → Word n → PrimitiveBasis n
  | 0, _ => Fin.elim0
  | _ + 1, x => Fin.cons x.1 (toBasis x.2)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “to basis word of basis”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem toBasis_wordOfBasis {n : Nat} (x : PrimitiveBasis n) :
    toBasis (wordOfBasis x) = x := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “word of basis to basis”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem wordOfBasis_toBasis {n : Nat} (x : Word n) :
    wordOfBasis (toBasis x) = x := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “basis equiv”.

def basisEquiv (n : Nat) : Word n ≃ PrimitiveBasis n where
  toFun := toBasis
  invFun := wordOfBasis
  left_inv := wordOfBasis_toBasis
  right_inv := toBasis_wordOfBasis

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “reverse basis”.

def reverseBasis (n : Nat) : PrimitiveBasis n ≃ PrimitiveBasis n where
  toFun x := fun i => x i.rev
  invFun x := fun i => x i.rev
  left_inv x := by funext i; simp

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sample equiv”.

def sampleEquiv (n : Nat) : Word n ≃ Fin (gridSize n) :=
  (basisEquiv n).trans ((reverseBasis n).trans (primitiveBasisLEEquiv n))

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “to bits”.

def toBits : {n : Nat} → Word n → List Bool
  | 0, _ => []
  | _ + 1, x => decide (x.1 = 1) :: toBits x.2

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “to bits length”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem toBits_length {n : Nat} (x : Word n) : (toBits x).length = n := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “primitive snoc value”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem primitive_snoc_value (n : Nat) (x : PrimitiveBasis n) (bit : Fin 2) :
    (primitiveBasisLEEquiv (n + 1) (Fin.snoc x bit)).val =
      (primitiveBasisLEEquiv n x).val + 2 ^ n * bit.val := by

commit-pinned source · Verso Blueprint panel

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

theorem sampleEquiv_value {n : Nat} (x : Word n) :
    (sampleEquiv n x).val = HermiteBoundaryInjection.wordValue (toBits x) := by

commit-pinned source · Verso Blueprint panel

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

theorem wordSampleIndex_eq (n : Nat) (x : Word (n + 1)) :
    HermiteBoundaryInjection.wordSampleIndex n (toBits x) (toBits_length x) =
      sampleEquiv (n + 1) x := by

commit-pinned source · Verso Blueprint panel

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

theorem sampleEquiv_public {n : Nat} (x : PrimitiveBasis n) :
    sampleEquiv n (wordOfBasis (fun i => x i.rev)) = primitiveBasisLEEquiv n x := by

commit-pinned source · Verso Blueprint panel