Finite dimensional quantum mixed states, ρ.

The same comments apply as in Braket:

These could be done with a Hilbert space of Fintype, which would look like

(H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [FiniteDimensional ℂ H]

or by choosing a particular Basis and asserting it is Fintype. But frankly it seems easier to mostly focus on the basis-dependent notion of Matrix, which has the added benefit of an obvious "classical" interpretation (as the basis elements, or diagonal elements of a mixed state). In that sense, this quantum theory comes with the a particular classical theory always preferred.

Important definitions:

• instMixable: the Mixable instance allowing convex combinations of MStates
• ofClassical: Mixed states representing classical distributions
• purity: The purity Tr[ρ^2] of a state
• spectrum: The spectrum of the matrix
• uniform: The maximally mixed state
• mix: The total state corresponding to an ensemble
• average: Averages a function over an ensemble, with appropriate weights

structure MState (d : Type u_1) [Fintype d] [DecidableEq d] : Type u_1

A mixed quantum state is a PSD matrix with trace 1.

We don't extend (M : HermitianMat d ℂ) because that gives an annoying thing where M is actually a Subtype, which means ρ.M.foo notation doesn't work.

• M : HermitianMat d ℂ
• nonneg : 0 ≤ ↑self
• tr : (↑self).trace = 1

theorem MState.ext_iff {d : Type u_1} {inst✝ : Fintype d} {inst✝¹ : DecidableEq d} {x y : MState d} : x = y ↔ ↑x = ↑y

theorem MState.ext {d : Type u_1} {inst✝ : Fintype d} {inst✝¹ : DecidableEq d} {x y : MState d} (M : ↑x = ↑y) : x = y

instance MState.instCoe {d : Type u_1} [Fintype d] [DecidableEq d] : Coe (MState d) (HermitianMat d ℂ)

Equations

• MState.instCoe = { coe := MState.M }

def MState.m {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : Matrix d d ℂ

The underlying Matrix in an MState. Prefer MState.M for the HermitianMat.

Equations

• ρ.m = ↑↑ρ

@[simp]

theorem MState.mat_M {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : ↑↑ρ = ρ.m

theorem MState.pos {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : 0 < ↑ρ

def MState.evalMStateM : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for MState.M: it is always positive (0 < ρ.M). Note: we must not call whnfR on e because MState.M is a structure projection (reducible), so whnfR would reduce it and destroy the pattern.

Equations

• One or more equations did not get rendered due to their size.

theorem MState.psd {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : ρ.m.PosSemidef

theorem MState.Hermitian {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : ρ.m.IsHermitian

Every mixed state is Hermitian.

@[simp]

theorem MState.tr' {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : ρ.m.trace = 1

theorem MState.ext_m {d : Type u_1} [Fintype d] [DecidableEq d] {ρ₁ ρ₂ : MState d} (h : ρ₁.m = ρ₂.m) : ρ₁ = ρ₂

theorem MState.m_inj {d : Type u_1} [Fintype d] [DecidableEq d] : Function.Injective m

The map from mixed states to their matrices is injective

theorem MState.M_Injective {d : Type u_1} [Fintype d] [DecidableEq d] : Function.Injective M

theorem MState.convex (d : Type u_1) [Fintype d] [DecidableEq d] : Convex ℝ (Set.range M)

The matrices corresponding to MStates are Convex ℝ

instance MState.instMixable {d : Type u_1} [Fintype d] [DecidableEq d] : Mixable (HermitianMat d ℂ) (MState d)

Equations

• MState.instMixable = { to_U := MState.M, to_U_inj := ⋯, convex := ⋯, mkT := fun {u : HermitianMat d ℂ} (h : ∃ (t : MState d), ↑t = u) => ⟨{ M := u, nonneg := ⋯, tr := ⋯ }, ⋯⟩ }

instance MState.nonempty {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : Nonempty d

theorem MState.eigenvalue_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (i : d) : 0 ≤ ⋯.eigenvalues i

theorem MState.eigenvalue_le_one {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (i : d) : ⋯.eigenvalues i ≤ 1

theorem MState.le_one {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : ↑ρ ≤ 1

def MState.instInnerProb {d : Type u_1} [Fintype d] [DecidableEq d] : Inner Prob (MState d)

The inner product of two MState's, as a real number between 0 and 1.

Equations

• MState.instInnerProb = { inner := fun (ρ σ : MState d) => ⟨inner ℝ ↑ρ ↑σ, ⋯⟩ }

theorem MState.inner_def {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) : inner Prob ρ σ = ⟨inner ℝ ↑ρ ↑σ, ⋯⟩

theorem MState.val_inner {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) : ↑(inner Prob ρ σ) = inner ℝ ↑ρ ↑σ

def MState.exp_val_ℂ {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (T : Matrix d d ℂ) : ℂ

Equations

• ρ.exp_val_ℂ T = (T * ρ.m).trace

def MState.exp_val {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (T : HermitianMat d ℂ) : ℝ

The expectation value of an operator on a quantum state.

Equations

• ρ.exp_val T = inner ℝ (↑ρ) T

theorem MState.exp_val_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) {T : HermitianMat d ℂ} (h : 0 ≤ T) : 0 ≤ ρ.exp_val T

@[simp]

theorem MState.exp_val_zero {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : ρ.exp_val 0 = 0

@[simp]

theorem MState.exp_val_one {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : ρ.exp_val 1 = 1

theorem MState.exp_val_le_one {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) {T : HermitianMat d ℂ} (h : T ≤ 1) : ρ.exp_val T ≤ 1

theorem MState.exp_val_prob {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) {T : HermitianMat d ℂ} (h : 0 ≤ T ∧ T ≤ 1) : 0 ≤ ρ.exp_val T ∧ ρ.exp_val T ≤ 1

theorem MState.exp_val_sub {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (A B : HermitianMat d ℂ) : ρ.exp_val (A - B) = ρ.exp_val A - ρ.exp_val B

theorem MState.exp_val_eq_zero_iff {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) {A : HermitianMat d ℂ} (hA₁ : 0 ≤ A) : ρ.exp_val A = 0 ↔ (↑ρ).support ≤ A.ker

If a PSD observable A has expectation value of 0 on a state ρ, it must entirely contain the support of ρ in its kernel.

theorem MState.exp_val_eq_one_iff {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) {A : HermitianMat d ℂ} (hA₂ : A ≤ 1) : ρ.exp_val A = 1 ↔ (↑ρ).support ≤ (1 - A).ker

If an observable A has expectation value of 1 on a state ρ, it must entirely contain the support of ρ in its 1-eigenspace.

theorem MState.exp_val_add {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (A B : HermitianMat d ℂ) : ρ.exp_val (A + B) = ρ.exp_val A + ρ.exp_val B

@[simp]

theorem MState.exp_val_smul {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (r : ℝ) (A : HermitianMat d ℂ) : ρ.exp_val (r • A) = r * ρ.exp_val A

theorem MState.exp_val_le_exp_val {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) {A B : HermitianMat d ℂ} (h : A ≤ B) : ρ.exp_val A ≤ ρ.exp_val B

def MState.pure {d : Type u_1} [Fintype d] [DecidableEq d] (ψ : Ket d) : MState d

A mixed state can be constructed as a pure state arising from a ket.

Equations

• MState.pure ψ = { M := ⟨Matrix.vecMulVec ⇑ψ ⇑↑ψ, ⋯⟩, nonneg := ⋯, tr := ⋯ }

@[simp]

theorem MState.pure_apply {d : Type u_1} [Fintype d] [DecidableEq d] (ψ : Ket d) {i j : d} : (pure ψ).m i j = ψ i * (starRingEnd ℂ) (ψ j)

theorem MState.pure_mul_self {d : Type u_1} [Fintype d] [DecidableEq d] (ψ : Ket d) : (pure ψ).m * (pure ψ).m = ↑↑(pure ψ)

def MState.purity {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : Prob

The purity of a state is Tr[ρ^2]. This is a Prob, because it is always between zero and one.

Equations

• ρ.purity = inner Prob ρ ρ

def MState.spectrum {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : ProbDistribution d

The eigenvalue spectrum of a mixed quantum state, as a Distribution.

Equations

• ρ.spectrum = ProbDistribution.mk' (fun (x : d) => ⋯.eigenvalues x) ⋯ ⋯

theorem MState.spectrum_pure_eq_constant {d : Type u_1} [Fintype d] [DecidableEq d] (ψ : Ket d) : ∃ (i : d), (pure ψ).spectrum = ProbDistribution.constant i

The spectrum of a pure state is (1,0,0,...), i.e. a constant distribution.

theorem MState.pure_of_constant_spectrum {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (h : ∃ (i : d), ρ.spectrum = ProbDistribution.constant i) : ∃ (ψ : Ket d), ρ = pure ψ

If the spectrum of a mixed state is (1,0,0...) i.e. a constant distribution, it is a pure state.

theorem MState.pure_iff_constant_spectrum {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : (∃ (ψ : Ket d), ρ = pure ψ) ↔ ∃ (i : d), ρ.spectrum = ProbDistribution.constant i

A state ρ is pure iff its spectrum is (1,0,0,...) i.e. a constant distribution.

theorem MState.pure_iff_purity_one {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : (∃ (ψ : Ket d), ρ = pure ψ) ↔ ρ.purity = 1

theorem MState.spectralDecomposition {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : ∃ (ψs : d → Ket d), ↑ρ = ∑ i : d, ↑(ρ.spectrum i) • ↑(pure (ψs i))

def MState.prod {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ₁ : MState d₁) (ρ₂ : MState d₂) : MState (d₁ × d₂)

Equations

• ρ₁ ⊗ᴹ ρ₂ = { M := (↑ρ₁).kronecker ↑ρ₂, nonneg := ⋯, tr := ⋯ }

def MState.«term_⊗ᴹ_» : Lean.TrailingParserDescr

Equations

• MState.«term_⊗ᴹ_» = Lean.ParserDescr.trailingNode `MState.«term_⊗ᴹ_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ᴹ ") (Lean.ParserDescr.cat `term 101))

theorem MState.prod_inner_prod {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ξ1 ψ1 : MState d₁) (ξ2 ψ2 : MState d₂) : inner Prob (ξ1 ⊗ᴹ ξ2) (ψ1 ⊗ᴹ ψ2) = inner Prob ξ1 ψ1 * inner Prob ξ2 ψ2

theorem MState.pure_prod_pure {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ψ₁ : Ket d₁) (ψ₂ : Ket d₂) : pure (ψ₁ ⊗ᵠ ψ₂) = pure ψ₁ ⊗ᴹ pure ψ₂

The product of pure states is a pure product state , Ket.prod.

def MState.ofClassical {d : Type u_1} [Fintype d] [DecidableEq d] (dist : ProbDistribution d) : MState d

A representation of a classical distribution as a quantum state, diagonal in the given basis.

Equations

• MState.ofClassical dist = { M := HermitianMat.diagonal ℂ fun (x : d) => ↑(dist x), nonneg := ⋯, tr := ⋯ }

@[simp]

theorem MState.coe_ofClassical {d : Type u_1} [Fintype d] [DecidableEq d] (dist : ProbDistribution d) : ↑(ofClassical dist) = HermitianMat.diagonal ℂ fun (x : d) => ↑(dist x)

theorem MState.ofClassical_pow {d : Type u_1} [Fintype d] [DecidableEq d] (dist : ProbDistribution d) (p : ℝ) : ↑(ofClassical dist) ^ p = HermitianMat.diagonal ℂ fun (i : d) => ↑(dist i) ^ p

def MState.uniform {d : Type u_1} [Fintype d] [DecidableEq d] [Nonempty d] : MState d

The maximally mixed state.

Equations

• MState.uniform = MState.ofClassical ProbDistribution.uniform

instance MState.instUnique {d : Type u_1} [Fintype d] [DecidableEq d] [Unique d] : Unique (MState d)

There is exactly one state on a dimension-1 system.

Equations

• MState.instUnique = { default := MState.uniform, uniq := ⋯ }

instance MState.instInhabited {d : Type u_1} [Fintype d] [DecidableEq d] [Nonempty d] : Inhabited (MState d)

There exists a mixed state for every nonempty d. Here, the maximally mixed one is chosen.

Equations

• MState.instInhabited = { default := MState.uniform }

@[simp]

theorem MState.M_default {d : Type u_1} [Fintype d] [DecidableEq d] [Unique d] : ↑default = 1

def MState.traceLeft {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : MState d₂

Partial tracing out the left half of a system.

Equations

• ρ.traceLeft = { M := (↑ρ).traceLeft, nonneg := ⋯, tr := ⋯ }

@[simp]

theorem MState.traceLeft_M {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : ↑ρ.traceLeft = (↑ρ).traceLeft

def MState.traceRight {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : MState d₁

Partial tracing out the right half of a system.

Equations

• ρ.traceRight = { M := (↑ρ).traceRight, nonneg := ⋯, tr := ⋯ }

@[simp]

theorem MState.traceRight_M {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : ↑ρ.traceRight = (↑ρ).traceRight

@[simp]

theorem MState.traceLeft_prod_eq {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ₁ : MState d₁) (ρ₂ : MState d₂) : (ρ₁ ⊗ᴹ ρ₂).traceLeft = ρ₂

Taking the direct product on the left and tracing it back out gives the same state.

@[simp]

theorem MState.traceRight_prod_eq {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ₁ : MState d₁) (ρ₂ : MState d₂) : (ρ₁ ⊗ᴹ ρ₂).traceRight = ρ₁

Taking the direct product on the right and tracing it back out gives the same state.

theorem MState.spectrum_prod {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ₁ : MState d₁) (ρ₂ : MState d₂) : ∃ (σ : d₁ × d₂ ≃ d₁ × d₂), ∀ (i : d₁) (j : d₂), (ρ₁ ⊗ᴹ ρ₂).spectrum (σ (i, j)) = ρ₁.spectrum i * ρ₂.spectrum j

Spectrum of direct product. There is a permutation σ so that the spectrum of the direct product of ρ₁ and ρ₂, as permuted under σ, is the pairwise products of the spectra of ρ₁ and ρ₂.

theorem MState.sInf_spectrum_prod {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] (ρ : MState d) (σ : MState d₂) : sInf (_root_.spectrum ℝ (ρ ⊗ᴹ σ).m) = sInf (_root_.spectrum ℝ ρ.m) * sInf (_root_.spectrum ℝ σ.m)

def MState.IsSeparable {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : Prop

A mixed state is separable iff it can be written as a convex combination of product mixed states.

Equations

• ρ.IsSeparable = ∃ (ρLRs : Finset (MState d₁ × MState d₂)) (ps : ProbDistribution ↥ρLRs), ↑ρ = ∑ ρLR : ↥ρLRs, ↑(ps ρLR) • (↑(↑ρLR).1).kronecker ↑(↑ρLR).2

theorem MState.IsSeparable_prod {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ₁ : MState d₁) (ρ₂ : MState d₂) : (ρ₁ ⊗ᴹ ρ₂).IsSeparable

A product state MState.prod is separable.

theorem MState.eq_of_sum_eq_pure {d : Type u_5} [Fintype d] [DecidableEq d] {ι : Type u_6} {s : Finset ι} {p : ι → ℝ} {ρs : ι → MState d} {ρ : MState d} (h_pure : ρ.purity = 1) (h_sum : ↑ρ = ∑ i ∈ s, p i • ↑(ρs i)) (hp_nonneg : ∀ i ∈ s, 0 ≤ p i) (hp_sum : ∑ i ∈ s, p i = 1) (i : ι) (hi : i ∈ s) (hpi : 0 < p i) : ρs i = ρ

theorem MState.purity_prod {d₁ : Type u_5} {d₂ : Type u_6} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ₁ : MState d₁) (ρ₂ : MState d₂) : (ρ₁ ⊗ᴹ ρ₂).purity = ρ₁.purity * ρ₂.purity

theorem MState.pure_eq_pure_iff {d : Type u_5} [Fintype d] [DecidableEq d] (ψ φ : Ket d) : pure ψ = pure φ ↔ ∃ (z : ℂ), ‖z‖ = 1 ∧ ψ.vec = z • φ.vec

theorem MState.PhaseEquiv_iff_pure_eq {d : Type u_5} [Fintype d] [DecidableEq d] (ψ φ : Ket d) : Ket.PhaseEquiv ψ φ ↔ pure ψ = pure φ

Two kets are phase-equivalent if and only if their pure states are equal.

def MState.pureQ {d : Type u_5} [Fintype d] [DecidableEq d] : KetUpToPhase d → MState d

MState.pure descends to the quotient KetUpToPhase.

Equations

• MState.pureQ = Quotient.lift MState.pure ⋯

@[simp]

theorem MState.pureQ_mk {d : Type u_5} [Fintype d] [DecidableEq d] (ψ : Ket d) : pureQ ⟦ψ⟧ = pure ψ

theorem MState.pureQ_injective {d : Type u_5} [Fintype d] [DecidableEq d] : Function.Injective pureQ

theorem MState.pure_separable_imp_IsProd {d₁ : Type u_5} {d₂ : Type u_6} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ψ : Ket (d₁ × d₂)) (h : (pure ψ).IsSeparable) : ψ.IsProd

theorem MState.pure_separable_iff_IsProd {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ψ : Ket (d₁ × d₂)) : (pure ψ).IsSeparable ↔ ψ.IsProd

A pure state is separable iff the ket is a product state.

theorem MState.pure_iff_rank_eq_one {d : Type u_5} [Fintype d] [DecidableEq d] (ρ : MState d) : (∃ (ψ : Ket d), ρ = pure ψ) ↔ ρ.m.rank = 1

A mixed state is pure if and only if its rank is 1.

theorem MState.Ket.IsProd_iff_rank_eq_one {d₁ : Type u_5} {d₂ : Type u_6} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ψ : Ket (d₁ × d₂)) : ψ.IsProd ↔ (Matrix.of fun (i : d₁) (j : d₂) => ψ (i, j)).rank = 1

A ket on a product space is a product state if and only if its coefficient matrix has rank 1.

theorem MState.pure_separable_iff_traceLeft_pure {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ψ : Ket (d₁ × d₂)) : (pure ψ).IsSeparable ↔ ∃ (ψ₁ : Ket d₂), pure ψ₁ = (pure ψ).traceLeft

A pure state is separable iff the partial trace on the left is pure.

def MState.purify {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : Ket (d × d)

The purification of a mixed state. Always uses the full dimension of the Hilbert space (d) to purify, so e.g. an existing pure state with d=4 still becomes d=16 in the purification. The defining property is MState.traceRight_of_purify; see also MState.purify' for the bundled version.

Equations

• ρ.purify = { vec := fun (x : d × d) => match x with | (i, j) => have ρ2 := ↑⋯.eigenvectorUnitary i j; ρ2 * ↑√(⋯.eigenvalues j), normalized' := ⋯ }

@[simp]

theorem MState.purify_spec {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : (pure ρ.purify).traceRight = ρ

The defining property of purification, that tracing out the purifying system gives the original mixed state.

def MState.purifyX {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : { ψ : Ket (d × d) // (pure ψ).traceRight = ρ }

MState.purify bundled with its defining property MState.traceRight_of_purify.

Equations

• ρ.purifyX = ⟨ρ.purify, ⋯⟩

def MState.relabel {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState d₁) (e : d₂ ≃ d₁) : MState d₂

Equations

• ρ.relabel e = { M := (↑ρ).reindex e.symm, nonneg := ⋯, tr := ⋯ }

@[simp]

theorem MState.relabel_M {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState d₁) (e : d₂ ≃ d₁) : ↑(ρ.relabel e) = (↑ρ).reindex e.symm

@[simp]

theorem MState.relabel_m {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState d₁) (e : d₂ ≃ d₁) : (ρ.relabel e).m = ρ.m.submatrix ⇑e ⇑e

@[simp]

theorem MState.relabel_refl {d : Type u_5} [Fintype d] [DecidableEq d] (ρ : MState d) : ρ.relabel (Equiv.refl d) = ρ

theorem MState.relabel_pure_exists {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ψ : Ket d₁) (e : d₂ ≃ d₁) : ∃ (ψ' : Ket d₂), (pure ψ).relabel e = pure ψ'

Relabeling a pure state by a bijection yields another pure state.

@[simp]

theorem MState.relabel_relabel {d : Type u_5} {d₂ : Type u_6} {d₃ : Type u_7} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] [Fintype d₃] [DecidableEq d₃] (ρ : MState d) (e : d₂ ≃ d) (e₂ : d₃ ≃ d₂) : (ρ.relabel e).relabel e₂ = ρ.relabel (e₂.trans e)

theorem MState.eq_relabel_iff {d₁ d₂ : Type u} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] (ρ : MState d₁) (σ : MState d₂) (h : d₁ ≃ d₂) : ρ = σ.relabel h ↔ ρ.relabel h.symm = σ

theorem MState.relabel_comp {d₁ : Type u_5} {d₂ : Type u_6} {d₃ : Type u_7} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] [Fintype d₃] [DecidableEq d₃] (ρ : MState d₁) (e : d₂ ≃ d₁) (f : d₃ ≃ d₂) : (ρ.relabel e).relabel f = ρ.relabel (f.trans e)

theorem MState.relabel_cast {d₁ d₂ : Type u} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] (ρ : MState d₁) (e : d₂ = d₁) : ρ.relabel (Equiv.cast e) = cast ⋯ ρ

@[simp]

theorem MState.spectrum_relabel {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] {ρ : MState d} (e : d₂ ≃ d) : _root_.spectrum ℝ (ρ.relabel e).m = _root_.spectrum ℝ ρ.m

@[simp]

theorem MState.purity_relabel {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState d₁) (e : d₂ ≃ d₁) : (ρ.relabel e).purity = ρ.purity

The purity of a state is invariant under relabeling of the basis.

def MState.SWAP {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : MState (d₂ × d₁)

The heterogeneous SWAP gate that exchanges the left and right halves of a quantum system. This can apply even when the two "halves" are of different types, as opposed to (say) the SWAP gate on quantum circuits that leaves the qubit dimensions unchanged. Notably, it is not unitary.

Equations

• ρ.SWAP = ρ.relabel (Equiv.prodComm d₁ d₂).symm

theorem MState.multiset_spectrum_relabel_eq {d₁ : Type u_5} {d₂ : Type u_6} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] (ρ : MState d₁) (e : d₂ ≃ d₁) : Multiset.map (⇑(ρ.relabel e).spectrum) Finset.univ.val = Multiset.map (⇑ρ.spectrum) Finset.univ.val

The multiset of values in the spectrum of a relabeled state is the same as the multiset of values in the spectrum of the original state.

def MState.spectrum_SWAP {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : ∃ (e : d₁ × d₂ ≃ d₂ × d₁), ρ.SWAP.spectrum.relabel e = ρ.spectrum

Equations

• ⋯ = ⋯

@[simp]

theorem MState.SWAP_SWAP {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : ρ.SWAP.SWAP = ρ

@[simp]

theorem MState.traceLeft_SWAP {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : ρ.SWAP.traceLeft = ρ.traceRight

@[simp]

theorem MState.traceRight_SWAP {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : ρ.SWAP.traceRight = ρ.traceLeft

def MState.assoc {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState ((d₁ × d₂) × d₃)) : MState (d₁ × d₂ × d₃)

The associator that re-clusters the parts of a quantum system.

Equations

• ρ.assoc = ρ.relabel (Equiv.prodAssoc d₁ d₂ d₃).symm

def MState.assoc' {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState (d₁ × d₂ × d₃)) : MState ((d₁ × d₂) × d₃)

The associator that re-clusters the parts of a quantum system.

Equations

• ρ.assoc' = ρ.SWAP.assoc.SWAP.assoc.SWAP

@[simp]

theorem MState.assoc_assoc' {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState (d₁ × d₂ × d₃)) : ρ.assoc'.assoc = ρ

@[simp]

theorem MState.assoc'_assoc {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState ((d₁ × d₂) × d₃)) : ρ.assoc.assoc' = ρ

@[simp]

theorem MState.traceLeft_right_assoc {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState ((d₁ × d₂) × d₃)) : ρ.assoc.traceLeft.traceRight = ρ.traceRight.traceLeft

@[simp]

theorem MState.traceRight_left_assoc' {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState (d₁ × d₂ × d₃)) : ρ.assoc'.traceRight.traceLeft = ρ.traceLeft.traceRight

@[simp]

theorem MState.traceRight_assoc {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState ((d₁ × d₂) × d₃)) : ρ.assoc.traceRight = ρ.traceRight.traceRight

@[simp]

theorem MState.traceLeft_assoc' {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState (d₁ × d₂ × d₃)) : ρ.assoc'.traceLeft = ρ.traceLeft.traceLeft

@[simp]

theorem MState.traceLeft_left_assoc {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState ((d₁ × d₂) × d₃)) : ρ.assoc.traceLeft.traceLeft = ρ.traceLeft

@[simp]

theorem MState.traceRight_right_assoc' {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState (d₁ × d₂ × d₃)) : ρ.assoc'.traceRight.traceRight = ρ.traceRight

@[simp]

theorem MState.traceNorm_eq_1 {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : ρ.m.traceNorm = 1

theorem MState.relabel_kron {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState d₁) (σ : MState d₂) (e : d₃ ≃ d₁) : ρ.relabel e ⊗ᴹ σ = (ρ ⊗ᴹ σ).relabel (e.prodCongr (Equiv.refl d₂))

theorem MState.kron_relabel {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState d₁) (σ : MState d₂) (e : d₃ ≃ d₂) : ρ ⊗ᴹ σ.relabel e = (ρ ⊗ᴹ σ).relabel ((Equiv.refl d₁).prodCongr e)

theorem MState.prod_assoc {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState d₁) (σ : MState d₂) (τ : MState d₃) : ρ ⊗ᴹ (σ ⊗ᴹ τ) = (ρ ⊗ᴹ σ ⊗ᴹ τ).relabel (Equiv.prodAssoc d₁ d₂ d₃).symm

instance MState.instTopologicalSpace {d : Type u_1} [Fintype d] [DecidableEq d] : TopologicalSpace (MState d)

Mixed states inherit the subspace topology from matrices

Equations

• MState.instTopologicalSpace = TopologicalSpace.induced MState.M inferInstance

theorem MState.toMat_IsEmbedding {d : Type u_1} [Fintype d] [DecidableEq d] : Topology.IsEmbedding M

The projection from mixed states to their Hermitian matrices is an embedding

instance MState.instT3Space {d : Type u_1} [Fintype d] [DecidableEq d] : T3Space (MState d)

instance MState.instCompactSpace {d : Type u_1} [Fintype d] [DecidableEq d] : CompactSpace (MState d)

noncomputable instance MState.instMetricSpace {d : Type u_1} [Fintype d] [DecidableEq d] : MetricSpace (MState d)

Equations

• MState.instMetricSpace = MetricSpace.induced MState.M ⋯ inferInstance

theorem MState.dist_eq {d : Type u_1} [Fintype d] [DecidableEq d] (x y : MState d) : dist x y = dist ↑x ↑y

instance MState.instBoundedSpace {d : Type u_1} [Fintype d] [DecidableEq d] : BoundedSpace (MState d)

theorem MState.Continuous_HermitianMat {d : Type u_1} [Fintype d] [DecidableEq d] : Continuous M

theorem MState.Continuous_Matrix {d : Type u_1} [Fintype d] [DecidableEq d] : Continuous m

theorem MState.image_M_isBounded {d : Type u_1} [Fintype d] [DecidableEq d] (S : Set (MState d)) : Bornology.IsBounded (M '' S)

def MState.piProd {ι : Type u} [DecidableEq ι] [fι : Fintype ι] {dI : ι → Type v} [(i : ι) → Fintype (dI i)] [(i : ι) → DecidableEq (dI i)] (ρi : (i : ι) → MState (dI i)) : MState ((i : ι) → dI i)

Equations

• MState.piProd ρi = { M := ⟨Matrix.piProd fun (i : ι) => (ρi i).m, ⋯⟩, nonneg := ⋯, tr := ⋯ }

def MState.npow {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (n : ℕ) : MState (Fin n → d)

The n-copy "power" of a mixed state, with the standard basis indexed by pi types.

Equations

• ρ ⊗ᴹ^ n = MState.piProd fun (x : Fin n) => ρ

def MState.«term_⊗ᴹ^_» : Lean.TrailingParserDescr

The n-copy "power" of a mixed state, with the standard basis indexed by pi types.

Equations

• MState.«term_⊗ᴹ^_» = Lean.ParserDescr.trailingNode `MState.«term_⊗ᴹ^_» 110 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ᴹ^ ") (Lean.ParserDescr.cat `term 111))

theorem MState.PosDef.kron {d₁ : Type u_5} {d₂ : Type u_6} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] {σ₁ : MState d₁} {σ₂ : MState d₂} (hσ₁ : σ₁.m.PosDef) (hσ₂ : σ₂.m.PosDef) : (σ₁ ⊗ᴹ σ₂).m.PosDef

theorem MState.PosDef.relabel {d₁ : Type u_5} {d₂ : Type u_6} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] {ρ : MState d₁} (hρ : ρ.m.PosDef) (e : d₂ ≃ d₁) : (ρ.relabel e).m.PosDef

theorem MState.PosDef_mix {d : Type u_5} [Fintype d] [DecidableEq d] {σ₁ σ₂ : MState d} (hσ₁ : σ₁.m.PosDef) (hσ₂ : σ₂.m.PosDef) (p : Prob) : p[σ₁↔σ₂].m.PosDef

If both states positive definite, so is their mixture.

theorem MState.PosDef_mix_of_ne_zero {d : Type u_5} [Fintype d] [DecidableEq d] {σ₁ σ₂ : MState d} (hσ₁ : σ₁.m.PosDef) (p : Prob) (hp : p ≠ 0) : p[σ₁↔σ₂].m.PosDef

If one state is positive definite and the mixture is nondegenerate, their mixture is also positive definite.

theorem MState.PosDef_mix_of_ne_one {d : Type u_5} [Fintype d] [DecidableEq d] {σ₁ σ₂ : MState d} (hσ₂ : σ₂.m.PosDef) (p : Prob) (hp : p ≠ 1) : p[σ₁↔σ₂].m.PosDef

If the second state is positive definite and the mixture is nondegenerate, their mixture is also positive definite.

theorem MState.uniform_posDef {d : Type u_5} [Nonempty d] [Fintype d] [DecidableEq d] : uniform.m.PosDef

theorem MState.posDef_of_unique {d : Type u_5} [Fintype d] [DecidableEq d] (ρ : MState d) [Unique d] : ρ.m.PosDef