Lean checks the proposition indexed as “amplitude lift apply”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem amplitudeLift_apply
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(rotation : selector → system →
_root_.Matrix coefficient coefficient ℂ)
(row column : LCUIndex coefficient selector system) :
amplitudeLift rotation row column =
if row.2 = column.2 then
rotation row.2.1 row.2.2 row.1 column.1
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “select lift apply”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem selectLift_apply
{coefficient selector system : Type*}
[DecidableEq coefficient] [DecidableEq selector] [DecidableEq system]
(permutation : selector → system ≃ system)
(row column : LCUIndex coefficient selector system) :
selectLift (coefficient := coefficient) permutation row column =
if row =
(column.1, (column.2.1,
permutation column.2.1 column.2.2)) then 1 else 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “selector lift clean column apply”; the hypotheses and conclusion in the code panel fix its exact scope. A selector lift has one coefficient/system delta on a clean input column.
@[simp] theorem selectorLift_cleanColumn_apply
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(prepare : _root_.Matrix selector selector ℂ)
(cleanCoefficient : coefficient) (cleanSelector : selector)
(systemColumn : system)
(row : LCUIndex coefficient selector system) :
selectorLift (coefficient := coefficient) (system := system) prepare
row (cleanCoefficient, (cleanSelector, systemColumn)) =
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “star selector lift clean row apply”; the hypotheses and conclusion in the code panel fix its exact scope. The clean PREPARE bra has the conjugate selector entry and two deltas.
@[simp] theorem star_selectorLift_cleanRow_apply
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(prepare : _root_.Matrix selector selector ℂ)
(cleanCoefficient : coefficient) (cleanSelector : selector)
(systemRow : system)
(column : LCUIndex coefficient selector system) :
star (selectorLift (coefficient := coefficient) (system := system) prepare)
(cleanCoefficient, (cleanSelector, systemRow)) column =
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “amplitude lift mul selector lift clean”; the hypotheses and conclusion in the code panel fix its exact scope. Amplitude followed by selector preparation, evaluated on a clean input.
theorem amplitudeLift_mul_selectorLift_clean
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(prepare : _root_.Matrix selector selector ℂ)
(rotation : selector → system →
_root_.Matrix coefficient coefficient ℂ)
(cleanCoefficient : coefficient) (cleanSelector : selector)
(systemColumn : system)
(row : LCUIndex coefficient selector system) :
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “select lift mul amplitude lift mul selector lift clean”; the hypotheses and conclusion in the code panel fix its exact scope. SELECT applied after amplitude and PREPARE, on one clean input column.
theorem selectLift_mul_amplitudeLift_mul_selectorLift_clean
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(prepare : _root_.Matrix selector selector ℂ)
(rotation : selector → system →
_root_.Matrix coefficient coefficient ℂ)
(permutation : selector → system ≃ system)
(cleanCoefficient : coefficient) (cleanSelector : selector)
(systemColumn : system)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “star selector lift mul clean”; the hypotheses and conclusion in the code panel fix its exact scope. Project an arbitrary right factor through the clean PREPARE bra.
theorem star_selectorLift_mul_clean
{coefficient selector system κ : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
[Fintype κ]
(prepare : _root_.Matrix selector selector ℂ)
(operator : _root_.Matrix
(LCUIndex coefficient selector system) κ ℂ)
(cleanCoefficient : coefficient) (cleanSelector : selector)
(systemRow : system) (column : κ) :
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare amplitude select unprepare clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. Exact projected clean entry of PREPARE/amplitude/SELECT/unprepare.
theorem prepareAmplitudeSelectUnprepare_cleanEntry
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(prepare : _root_.Matrix selector selector ℂ)
(rotation : selector → system →
_root_.Matrix coefficient coefficient ℂ)
(permutation : selector → system ≃ system)
(cleanCoefficient : coefficient) (cleanSelector : selector)
(systemRow systemColumn : system) :
commit-pinned source · Verso Blueprint panel