LeanPool.Monlib4.QuantumGraph.QamAExample

Imported Lean Pool material for LeanPool.Monlib4.QuantumGraph.QamAExample.

Examples of single-edged quantum graph

This file contains examples of single-edged quantum graphs over M₂(ℂ). The main result is that all single-edged quantum graphs over M₂(ℂ) are isomorphic each other.

def traceModuleDual {𝕜 : Type u_1} {n : Type u_2} [Fintype n] [RCLike 𝕜] : Module.Dual 𝕜 (Matrix n n 𝕜)

The trace functional on square matrices.

Equations

• traceModuleDual = Matrix.traceLinearMap n 𝕜 𝕜

instance trace_isFaithfulPosMap {n : Type u_1} [Fintype n] {𝕜 : Type u_2} [RCLike 𝕜] : traceModuleDual.IsFaithfulPosMap

The trace functional is faithful and positive.

theorem traceModuleDual_matrix {n : Type u_1} [Fintype n] [DecidableEq n] : traceModuleDual.matrix = 1

theorem Matrix.smul_stdBasisMatrix {R : Type u_1} {α : Type u_2} {n : Type u_3} {m : Type u_4} [DecidableEq n] [DecidableEq m] [Zero R] [SMulZeroClass α R] (a : α) (i : n) (j : m) (x : R) : a • stdBasisMatrix i j x = stdBasisMatrix i j (a • x)

theorem Matrix.stdBasisMatrix.transpose {R : Type u_1} {n : Type u_2} {m : Type u_3} [DecidableEq n] [DecidableEq m] [Semiring R] (i : n) (j : m) : (stdBasisMatrix i j 1).transpose = stdBasisMatrix j i 1

theorem StarAlgEquiv.eq_comp_iff {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} [_inst_1 : CommSemiring R] [_inst_2 : Semiring E₂] [_inst_3 : Semiring E₃] [_inst_4 : AddCommMonoid E₁] [_inst_5 : Algebra R E₂] [_inst_6 : Algebra R E₃] [_inst_7 : Module R E₁] [_inst_8 : Star E₂] [_inst_9 : Star E₃] (f : E₂ ≃⋆ₐ[R] E₃) (x : E₁ →ₗ[R] E₂) (y : E₁ →ₗ[R] E₃) : f.toAlgEquiv.toLinearMap ∘ₗ x = y ↔ x = f.symm.toAlgEquiv.toLinearMap ∘ₗ y

theorem ite_comp {R : Type u_1} {U : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring R] [AddCommMonoid U] [AddCommMonoid V] [AddCommMonoid W] [Module R U] [Module R V] [Module R W] {P : Prop} [Decidable P] {x y : W →ₗ[R] U} {f : V →ₗ[R] W} : (if P then x else y) ∘ₗ f = if P then x ∘ₗ f else y ∘ₗ f

theorem comp_ite {R : Type u_1} {U : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring R] [AddCommMonoid U] [AddCommMonoid V] [AddCommMonoid W] [Module R U] [Module R V] [Module R W] {P : Prop} [Decidable P] {x y : W →ₗ[R] U} {f : U →ₗ[R] V} : (f ∘ₗ if P then x else y) = if P then f ∘ₗ x else f ∘ₗ y

theorem StarAlgEquiv.comp_symm_self {R : Type u_1} {U : Type u_2} {V : Type u_3} [CommSemiring R] [Semiring U] [Semiring V] [Algebra R U] [Algebra R V] [Star U] [Star V] {f : U ≃⋆ₐ[R] V} : f.toAlgEquiv.toLinearMap ∘ₗ f.symm.toAlgEquiv.toLinearMap = 1

theorem StarAlgEquiv.symm_comp_self {R : Type u_1} {U : Type u_2} {V : Type u_3} [CommSemiring R] [Semiring U] [Semiring V] [Algebra R U] [Algebra R V] [Star U] [Star V] {f : U ≃⋆ₐ[R] V} : f.symm.toAlgEquiv.toLinearMap ∘ₗ f.toAlgEquiv.toLinearMap = 1

theorem Qam.iso_preserves_ir_reflexive {n : Type u_1} [Fintype n] [DecidableEq n] [Nontrivial n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {x y : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (hxhy : Iso x y) (ir_reflexive : Prop) [Decidable ir_reflexive] : ((reflIdempotent hφ x) 1 = if ir_reflexive then 1 else 0) ↔ (reflIdempotent hφ y) 1 = if ir_reflexive then 1 else 0

def Function.IsAlmostInjective {A : Type u_1} {B : Type u_2} (f : A → B) [SMul ℂˣ A] : Prop

a function f : A → B is almost injective if for all $x, y \in A$, if $f(x)=f(y)$ then there exists some $0\neq\alpha \in \mathbb{C}$ such that $x = \alpha y$ (in other words, $x$ and $y$ are co-linear)

Equations

• Function.IsAlmostInjective f = ∀ (x y : A), f x = f y ↔ ∃ (α : ℂˣ), x = α • y

theorem Matrix.IsAlmostHermitian.spectrum {n : Type u_1} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsAlmostHermitian) : _root_.spectrum ℂ (toLin' x) = {x_1 : ℂ | ∃ (i : n), hx.eigenvalues i = x_1}

theorem spectra_fin_two {x : Matrix (Fin 2) (Fin 2) ℂ} (hx : x.IsAlmostHermitian) : hx.spectra = {hx.eigenvalues 0, hx.eigenvalues 1}

theorem spectra_fin_two' {x : Matrix (Fin 2) (Fin 2) ℂ} (hx : x.IsAlmostHermitian) : hx.spectra = ↑[hx.eigenvalues 0, hx.eigenvalues 1]

theorem spectra_fin_two'' {α : Type u_1} (a : Fin 2 → α) : Multiset.map a Finset.univ.val = {a 0, a 1}

theorem List.coe_inj {α : Type u_1} (l₁ l₂ : List α) : ↑l₁ = ↑l₂ ↔ l₁.Perm l₂

theorem spectra_fin_two_ext_aux {A : Type u_1} (α β γ : A) : {α, α} = {β, γ} ↔ α = β ∧ α = γ

theorem spectra_fin_two_ext {α : Type u_1} (α₁ α₂ β₁ β₂ : α) : {α₁, α₂} = {β₁, β₂} ↔ α₁ = β₁ ∧ α₂ = β₂ ∨ α₁ = β₂ ∧ α₂ = β₁

@[reducible]

instance Multiset.hasSmul {α : Type u_1} [SMul ℂ α] : SMul ℂ (Multiset α)

Equations

• Multiset.hasSmul = { smul := fun (a : ℂ) (s : Multiset α) => Multiset.map ((fun (x1 : ℂ) (x2 : α) => x1 • x2) a) s }

theorem Multiset.smul_fin_two {α : Type u_1} [SMul ℂ α] (a b : α) (c : ℂ) : c • {a, b} = {c • a, c • b}

theorem IsAlmostHermitian.smul_eq {n : Type u_1} {x : Matrix n n ℂ} (hx : x.IsAlmostHermitian) (c : ℂ) : ⋯.scalar • ⋯.matrix = c • x

theorem spectra_fin_two_ext_of_traceless {α₁ α₂ β₁ β₂ : ℂ} (hα₂ : α₂ ≠ 0) (hβ₂ : β₂ ≠ 0) (h₁ : α₁ = -α₂) (h₂ : β₁ = -β₂) : ∃ (c : ℂˣ), {α₁, α₂} = ↑c • {β₁, β₂}

theorem Matrix.IsAlmostHermitian.trace {n : Type u_1} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsAlmostHermitian) : x.trace = ∑ i : n, hx.eigenvalues i

@[reducible]

noncomputable def Matrix.IsAlmostHermitian.eigenvectorUnitary {n : Type u_1} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsAlmostHermitian) : ↥(unitaryGroup n ℂ)

The unitary eigenvector matrix chosen for an almost-Hermitian matrix.

Equations

• hx.eigenvectorUnitary = ⋯.eigenvectorUnitary

@[reducible]

noncomputable def Matrix.IsAlmostHermitian.eigenvectorMatrix {n : Type u_1} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsAlmostHermitian) : Matrix n n ℂ

The eigenvector matrix chosen for an almost-Hermitian matrix.

Equations

• hx.eigenvectorMatrix = ⋯.eigenvectorMatrix

theorem Matrix.IsAlmostHermitian.eigenvectorMatrix_eq {n : Type u_1} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsAlmostHermitian) : hx.eigenvectorMatrix = ⋯.eigenvectorMatrix

theorem Matrix.IsAlmostHermitian.eigenvectorUnitary_eq {n : Type u_1} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsAlmostHermitian) : ↑hx.eigenvectorUnitary = hx.eigenvectorMatrix

theorem Matrix.IsAlmostHermitian.spectral_theorem' {n : Type u_1} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsAlmostHermitian) : x = hx.scalar • (innerAut hx.eigenvectorUnitary) (diagonal (RCLike.ofReal ∘ ⋯.eigenvalues))

theorem Matrix.IsAlmostHermitian.eigenvalues_eq {n : Type u_1} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsAlmostHermitian) : hx.eigenvalues = hx.scalar • RCLike.ofReal ∘ ⋯.eigenvalues

theorem Matrix.IsAlmostHermitian.spectral_theorem {n : Type u_1} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsAlmostHermitian) : x = (innerAut hx.eigenvectorUnitary) (diagonal hx.eigenvalues)

theorem Matrix.IsAlmostHermitian.eigenvalues_eq_zero_iff {n : Type u_1} [Fintype n] [DecidableEq n] {x : Matrix n n ℂ} (hx : x.IsAlmostHermitian) : hx.eigenvalues = 0 ↔ x = 0

theorem Matrix.diagonal_eq_zero_iff {n : Type u_1} [DecidableEq n] {x : n → ℂ} : diagonal x = 0 ↔ x = 0

theorem Matrix.unitaryGroup.star_mul_cancel_right {n : Type u_1} [Fintype n] [DecidableEq n] {U₁ U₂ : ↥(unitaryGroup n ℂ)} : U₁ * star U₂ * U₂ = U₁

theorem qamA.finTwoIso (x y : { x : Matrix (Fin 2) (Fin 2) ℂ // x ≠ 0 }) (hx1 : IsSelfAdjoint (qamA ⋯ x)) (hx2 : (Qam.reflIdempotent ⋯ (qamA ⋯ x)) 1 = 0) (hy1 : IsSelfAdjoint (qamA ⋯ y)) (hy2 : (Qam.reflIdempotent ⋯ (qamA ⋯ y)) 1 = 0) : Qam.Iso (qamA ⋯ x) (qamA ⋯ y)

theorem Qam.finTwoIsoOfSingleEdge {A B : Matrix (Fin 2) (Fin 2) ℂ →ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ} (hx0 : RealQam ⋯ A) (hy0 : RealQam ⋯ B) (hx : hx0.edges = 1) (hy : hy0.edges = 1) (hx1 : IsSelfAdjoint A) (hx2 : (reflIdempotent ⋯ A) 1 = 0) (hy1 : IsSelfAdjoint B) (hy2 : (reflIdempotent ⋯ B) 1 = 0) : Iso A B