This definition gives the library's named construction or computation for “real orthogonal rotation”. A real planar rotation with explicit cosine and sine entries, embedded in 'ℂ'.
noncomputable def realOrthogonalRotation (cosine sine : Real) :
_root_.Matrix (Fin 2) (Fin 2) ℂ := fun row column =>
match row.val, column.val with
| 0, 0 => (cosine : ℂ)
| 0, _ => -(sine : ℂ)
| _, 0 => (sine : ℂ)
| _, _ => (cosine : ℂ)
/-- A real planar rotation is unitary whenever its two entries lie on the unit circle. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “real orthogonal rotation unitary”; the hypotheses and conclusion in the code panel fix its exact scope. A real planar rotation is unitary whenever its two entries lie on the unit circle.
theorem realOrthogonalRotation_unitary
(cosine sine : Real) (normalization : cosine * cosine + sine * sine = 1) :
realOrthogonalRotation cosine sine ∈
_root_.Matrix.unitaryGroup (Fin 2) ℂ := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “real rotation”. A real planar rotation, parameterized by an angle.
noncomputable def realRotation (angle : Real) :
_root_.Matrix (Fin 2) (Fin 2) ℂ :=
realOrthogonalRotation (Real.cos angle) (Real.sin angle)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “real rotation zero zero”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem realRotation_zero_zero (angle : Real) :
realRotation angle 0 0 = (Real.cos angle : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “real rotation zero one”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem realRotation_zero_one (angle : Real) :
realRotation angle 0 1 = -(Real.sin angle : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “real rotation one zero”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem realRotation_one_zero (angle : Real) :
realRotation angle 1 0 = (Real.sin angle : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “real rotation one one”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem realRotation_one_one (angle : Real) :
realRotation angle 1 1 = (Real.cos angle : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “real rotation unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Every real planar rotation is unitary over 'ℂ'.
theorem realRotation_unitary (angle : Real) :
realRotation angle ∈
_root_.Matrix.unitaryGroup (Fin 2) ℂ := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “amplitude rotation”. Rotation whose clean entry is intended to encode 'coefficient'.
noncomputable def amplitudeRotation (coefficient : Real) :
_root_.Matrix (Fin 2) (Fin 2) ℂ :=
realRotation (Real.arccos coefficient)
/-- The amplitude rotation is unitary without any domain hypothesis. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “amplitude rotation unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The amplitude rotation is unitary without any domain hypothesis.
theorem amplitudeRotation_unitary (coefficient : Real) :
amplitudeRotation coefficient ∈
_root_.Matrix.unitaryGroup (Fin 2) ℂ :=
realRotation_unitary _
/-- Under the standard arccos domain, the clean entry is exactly the coefficient. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “amplitude rotation clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. Under the standard arccos domain, the clean entry is exactly the coefficient.
theorem amplitudeRotation_cleanEntry
(coefficient : Real) (lower : -1 ≤ coefficient) (upper : coefficient ≤ 1) :
amplitudeRotation coefficient 0 0 = (coefficient : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “reindex unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Reindexing rows and columns by the same equivalence preserves unitarity.
theorem reindex_unitary
{ι κ : Type*} [Fintype ι] [DecidableEq ι]
[Fintype κ] [DecidableEq κ]
(equiv : ι ≃ κ) (operator : _root_.Matrix ι ι ℂ)
(unitary : operator ∈ _root_.Matrix.unitaryGroup ι ℂ) :
_root_.Matrix.reindexAlgEquiv ℂ ℂ equiv operator ∈
_root_.Matrix.unitaryGroup κ ℂ := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “block diagonal unitary”; the hypotheses and conclusion in the code panel fix its exact scope. A finite family of unitary blocks is unitary when placed block-diagonally.
theorem blockDiagonal_unitary
{ι κ : Type*} [Fintype ι] [DecidableEq ι]
[Fintype κ] [DecidableEq κ]
(blocks : κ → _root_.Matrix ι ι ℂ)
(unitary : ∀ k, blocks k ∈ _root_.Matrix.unitaryGroup ι ℂ) :
_root_.Matrix.blockDiagonal blocks ∈
_root_.Matrix.unitaryGroup (ι × κ) ℂ := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “equiv permutation matrix”. Matrix of a finite basis permutation.
def equivPermutationMatrix
{ι : Type*} [DecidableEq ι] (equiv : ι ≃ ι) :
_root_.Matrix ι ι ℂ := fun row column =>
if row = equiv column then 1 else 0
/-- Every equivalence induces a unitary permutation matrix. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “equiv permutation matrix unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Every equivalence induces a unitary permutation matrix.
theorem equivPermutationMatrix_unitary
{ι : Type*} [Fintype ι] [DecidableEq ι] (equiv : ι ≃ ι) :
equivPermutationMatrix equiv ∈
_root_.Matrix.unitaryGroup ι ℂ := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “equiv permutation matrix mul apply”; the hypotheses and conclusion in the code panel fix its exact scope. Multiplication by a permutation matrix applies the inverse permutation to rows.
theorem equivPermutationMatrix_mul_apply
{ι κ : Type*} [Fintype ι] [DecidableEq ι]
(equiv : ι ≃ ι) (operator : _root_.Matrix ι κ ℂ)
(row : ι) (column : κ) :
(equivPermutationMatrix equiv * operator) row column =
operator (equiv.symm row) column := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “mul equiv permutation matrix apply”; the hypotheses and conclusion in the code panel fix its exact scope. Multiplication on the right by a permutation matrix applies the permutation to columns.
theorem mul_equivPermutationMatrix_apply
{ι κ : Type*} [Fintype κ] [DecidableEq κ]
(operator : _root_.Matrix ι κ ℂ) (equiv : κ ≃ κ)
(row : ι) (column : κ) :
(operator * equivPermutationMatrix equiv) row column =
operator row (equiv column) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “equiv permutation matrix mul”; the hypotheses and conclusion in the code panel fix its exact scope. Chronological composition of finite basis permutations.
theorem equivPermutationMatrix_mul
{ι : Type*} [Fintype ι] [DecidableEq ι]
(first second : ι ≃ ι) :
equivPermutationMatrix second * equivPermutationMatrix first =
equivPermutationMatrix (first.trans second) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “equiv permutation matrix conjugates reindex”; the hypotheses and conclusion in the code panel fix its exact scope. Conjugating a reindexed operator by an involutive basis permutation is the same as composing that permutation into the indexing equivalence.
theorem equivPermutationMatrix_conjugates_reindex
{ι κ : Type*} [Fintype ι] [DecidableEq ι]
[Fintype κ] [DecidableEq κ]
(basis : ι ≃ ι) (logical : ι ≃ κ)
(operator : _root_.Matrix κ κ ℂ)
(involutive : Function.Involutive basis) :
equivPermutationMatrix basis *
_root_.Matrix.reindexAlgEquiv ℂ ℂ logical.symm operator *
equivPermutationMatrix basis =
_root_.Matrix.reindexAlgEquiv ℂ ℂ
(basis.trans logical).symm operator := by
commit-pinned source · Verso Blueprint panel
This abbreviation gives a shorter name to the type or expression used for “lcu index”. Product-register index for coefficient, selector, and system registers.
abbrev LCUIndex (coefficient selector system : Type*) :=
coefficient × (selector × system)
/-- Lift selector PREPARE to coefficient × selector × system. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “selector lift”. Lift selector PREPARE to coefficient × selector × system.
def selectorLift
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(prepare : _root_.Matrix selector selector ℂ) :
_root_.Matrix
(LCUIndex coefficient selector system)
(LCUIndex coefficient selector system) ℂ :=
(1 : _root_.Matrix coefficient coefficient ℂ) ⊗ₖ
(prepare ⊗ₖ (1 : _root_.Matrix system system ℂ))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “selector lift unitary”; the hypotheses and conclusion in the code panel fix its exact scope. A unitary selector PREPARE remains unitary after tensoring with identities.
theorem selectorLift_unitary
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(prepare : _root_.Matrix selector selector ℂ)
(unitary : prepare ∈ _root_.Matrix.unitaryGroup selector ℂ) :
selectorLift (coefficient := coefficient) (system := system) prepare ∈
_root_.Matrix.unitaryGroup
(LCUIndex coefficient selector system) ℂ := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “amplitude lift”. Lift a coefficient-unitary family controlled by selector and system.
def amplitudeLift
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(rotation : selector → system →
_root_.Matrix coefficient coefficient ℂ) :
_root_.Matrix
(LCUIndex coefficient selector system)
(LCUIndex coefficient selector system) ℂ :=
_root_.Matrix.blockDiagonal (fun context => rotation context.1 context.2)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “amplitude lift unitary”; the hypotheses and conclusion in the code panel fix its exact scope. A controlled family of unitary amplitude blocks is unitary.
theorem amplitudeLift_unitary
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(rotation : selector → system →
_root_.Matrix coefficient coefficient ℂ)
(unitary : ∀ selector system,
rotation selector system ∈
_root_.Matrix.unitaryGroup coefficient ℂ) :
amplitudeLift rotation ∈
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “controlled system equiv”. SELECT equivalence preserving coefficient and selector and permuting the system.
def controlledSystemEquiv
{coefficient selector system : Type*}
(permutation : selector → system ≃ system) :
LCUIndex coefficient selector system ≃
LCUIndex coefficient selector system where
toFun index :=
(index.1, (index.2.1, permutation index.2.1 index.2.2))
invFun index :=
(index.1, (index.2.1, (permutation index.2.1).symm index.2.2))
left_inv index := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “select lift”. Logical SELECT matrix for a family of system permutations.
def selectLift
{coefficient selector system : Type*}
[DecidableEq coefficient] [DecidableEq selector] [DecidableEq system]
(permutation : selector → system ≃ system) :
_root_.Matrix
(LCUIndex coefficient selector system)
(LCUIndex coefficient selector system) ℂ :=
equivPermutationMatrix (controlledSystemEquiv permutation)
/-- SELECT is unitary because it is a basis permutation. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “select lift unitary”; the hypotheses and conclusion in the code panel fix its exact scope. SELECT is unitary because it is a basis permutation.
theorem selectLift_unitary
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(permutation : selector → system ≃ system) :
selectLift (coefficient := coefficient) permutation ∈
_root_.Matrix.unitaryGroup
(LCUIndex coefficient selector system) ℂ :=
equivPermutationMatrix_unitary _
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “prepare amplitude select unprepare”. PREPARE → amplitude → SELECT → unprepare logical matrix.
noncomputable def prepareAmplitudeSelectUnprepare
{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) :
_root_.Matrix
(LCUIndex coefficient selector system)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare amplitude select unprepare unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The complete logical LCU composition is unitary from its local certificates.
theorem prepareAmplitudeSelectUnprepare_unitary
{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)
(prepareUnitary :
prepare ∈ _root_.Matrix.unitaryGroup selector ℂ)
commit-pinned source · Verso Blueprint panel