Real

Here we use the transpose rather than the complex conjugate transpose.

def pureState {R : Type u_1} [Mul R] [Add R] [Zero R] {k : ℕ} (e : Matrix (Fin k) (Fin 1) R) : Matrix (Fin k) (Fin k) R

Equations

• pureState e = e.mulᵣ e.transpose

theorem pureState_selfAdjoint {k : ℕ} (e : Matrix (Fin k) (Fin 1) ℝ) : (pureState e).IsHermitian

def pureState_projection' {k : ℕ} (e : EuclideanSpace ℝ (Fin k)) (he : ‖e‖ = 1) : IsStarProjection (pureState fun (i : Fin k) (x : Fin 1) => e.ofLp i)

Equations

• ⋯ = ⋯

theorem pureState_projection {k : ℕ} (i : Fin k) : IsStarProjection (pureState (e i))

theorem pureState_projection'' : IsStarProjection (pureState (e 0) + pureState (e 1))

Projection onto span ⟨e₁, e₂⟩ is indeed a star-projection. So we could form a PMF with two outcomes (e₁,e₂) vs. e₃.

theorem pureState_psd {k : ℕ} (e : Matrix (Fin k) (Fin 1) ℝ) : (e.mulᵣ e.transpose).PosSemidef

@[implicit_reducible]

noncomputable instance instNormedRingMatrixFinOfNatNatComplex_kraus_1 : NormedRing (Matrix (Fin 2) (Fin 2) ℂ)

Equations

• instNormedRingMatrixFinOfNatNatComplex_kraus_1 = Matrix.frobeniusNormedRing

@[implicit_reducible]

noncomputable instance instNormedAlgebraRealMatrixFinOfNatNatComplex_kraus_1 : NormedAlgebra ℝ (Matrix (Fin 2) (Fin 2) ℂ)

Equations

• instNormedAlgebraRealMatrixFinOfNatNatComplex_kraus_1 = Matrix.frobeniusNormedAlgebra

theorem nonneg_trace' {n : ℕ} {ρ : Matrix (Fin n) (Fin n) ℝ} (hρ' : ρ.PosSemidef) (e : Matrix (Fin n) (Fin 1) ℝ) (he : ‖WithLp.toLp 2 fun (i : Fin n) => e i 0‖ = 1) : 0 ≤ (pureState e * ρ).trace

A general reason why nonneg_trace below holds. Can be generalized to let (e * eᵀ) be any projection, see above ^^.

theorem nonneg_trace_of_posSemidef {n : ℕ} {ρ : Matrix (Fin n) (Fin n) ℝ} (hρ' : ρ.PosSemidef) (i : Fin n) : 0 ≤ (pureState (e i) * ρ).trace

theorem POVM_PMF.aux₀ {k : ℕ} {ρ : Matrix (Fin k) (Fin k) ℝ} (hρ : ρ.trace = 1) (hρ' : ρ.PosSemidef) : ∑ a : Fin k, ⟨(pureState (e a) * ρ).trace, ⋯⟩ = ENNReal.toNNReal 1

theorem standard_basis_probability_one {k : ℕ} {ρ : Matrix (Fin k) (Fin k) ℝ} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : ∑ a : Fin k, ↑⟨(pureState (e a) * ρ).trace, ⋯⟩ = 1

def PVM_PMF₂₃ {ρ : Matrix (Fin 3) (Fin 3) ℝ} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PMF (Fin 2)

A probability measure that gives the probability of being in the xy-plane, or the z-axis, for a given PSD trace-one matrix ρ. See myPVM₂₃ below.

Equations

• PVM_PMF₂₃ hUT hPS = PMF.ofFintype (fun (i : Fin 2) => ↑(if i = 0 then ⟨((pureState (e 0) + pureState (e 1)) * ρ).trace, ⋯⟩ else ⟨(pureState (e 2) * ρ).trace, ⋯⟩)) ⋯

theorem one_eq_sum_pureState_R {k : ℕ} : 1 = ∑ i : Fin k, pureState (e i)

theorem trace_one_sub {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) ℝ} (hPS : ρ.PosSemidef) : 0 ≤ ((1 - pureState (e acc)) * ρ).trace

theorem PMF_of_state.sum_one {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) ℝ} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : ∑ i : Fin 2, ↑(if i = 0 then ⟨((1 - pureState (e acc)) * ρ).trace, ⋯⟩ else ⟨(pureState (e acc) * ρ).trace, ⋯⟩) = 1

def PMF_of_state {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) ℝ} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PMF (Fin 2)

Defining a Bernoulli probability measure by declaring that e_{acc} is the accepted subspace.

Equations

• PMF_of_state acc hUT hPS = PMF.ofFintype (fun (i : Fin 2) => ↑(if i = 0 then ⟨((1 - pureState (e acc)) * ρ).trace, ⋯⟩ else ⟨(pureState (e acc) * ρ).trace, ⋯⟩)) ⋯

noncomputable def myPVM {k : ℕ} {ρ : Matrix (Fin k) (Fin k) ℝ} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PVM

Equations

• myPVM hUT hPS = { k := k, ρ := ρ, hρ := hPS, t := k, op := fun (i : Fin k) => pureState (e i), pf := ⋯, p := POVM_PMF hUT ⋯, pf' := ⋯ }

def myPVM₂₃ {ρ : Matrix (Fin 3) (Fin 3) ℝ} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PVM

Equations

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

def PVM_of_state {k : ℕ} (acc : Fin k) {ρ : Matrix (Fin k) (Fin k) ℝ} (hUT : ρ.trace = 1) (hPS : ρ.PosSemidef) : PVM

Equations

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

def languageAcceptedBy {α : Type u_1} {q r : ℕ} (acceptStateIndex : Fin q.succ) (𝓚 : α → Fin r → Matrix (Fin q.succ) (Fin q.succ) ℝ) : Set ((n : ℕ) × (Fin n → α))

1/24/26

Equations

• languageAcceptedBy acceptStateIndex 𝓚 = {word : (n : ℕ) × (Fin n → α) | krausApplyWord word.snd 𝓚 (pureState (e 0)) = pureState (e acceptStateIndex)}

theorem basisState_trace_one {k : ℕ} {i : Fin k.succ} : (pureState (e i)).trace = 1

def PVM_of_word_of_channel {α : Type u_1} {r k : ℕ} (acc : Fin k.succ) {𝓚 : α → Fin r → Matrix (Fin k.succ) (Fin k.succ) ℝ} (h𝓚 : ∀ (a : α), QuantumChannel (𝓚 a)) (word : (n : ℕ) × (Fin n → α)) : PVM

The projection-valued measure corresponding to word belong to the measure-once language of KOA 𝓚.

Equations

• PVM_of_word_of_channel acc h𝓚 word = PVM_of_state acc ⋯ ⋯

def getPVM₃ {α : Type u_1} {r : ℕ} {𝓚 : α → Fin r → Matrix (Fin (Nat.succ 2)) (Fin (Nat.succ 2)) ℝ} (h𝓚 : ∀ (a : α), QuantumChannel (𝓚 a)) (word : (n : ℕ) × (Fin n → α)) : PVM

Equations

• getPVM₃ h𝓚 word = PVM_of_word_of_channel 2 h𝓚 word

def MOlanguageAcceptedBy {α : Type u_1} {r k : ℕ} (acc : Fin k.succ) {𝓚 : α → Fin r → Matrix (Fin k.succ) (Fin k.succ) ℝ} (h𝓚 : ∀ (a : α), QuantumChannel (𝓚 a)) : Set ((n : ℕ) × (Fin n → α))

1/25/26 We accept word if starting in e₀ we end up in e₁ with probability at least 1/2.

Equations

• MOlanguageAcceptedBy acc h𝓚 = {word : (n : ℕ) × (Fin n → α) | (PVM_of_word_of_channel acc h𝓚 word).p 1 > 1 / 2}

theorem MO_language_nonempty {α : Type u_1} {r k : ℕ} {𝓚 : α → Fin r → Matrix (Fin k.succ) (Fin k.succ) ℝ} (h𝓚 : ∀ (a : α), QuantumChannel (𝓚 a)) : MOlanguageAcceptedBy 0 h𝓚 ≠ ∅

If the start and accept states are the same then the empty string is accepted in the measure-once setting.

def MOlanguageAcceptedBy₃ {α : Type u_1} {r : ℕ} (𝓚 : α → Fin r → Matrix (Fin 3) (Fin 3) ℝ) (h𝓚 : ∀ (a : α), QuantumChannel (𝓚 a)) : Set ((n : ℕ) × (Fin n → α))

A word is measure-once accepted if after processing it, the probability of being in state 1 : Fin 2, is greater than 1/2.

Measure-Once language accepted by 𝓚 is {word | Probability that we are in state e₃, and not in the span of e₁,e₂, > 1/2}. q = 2 because we haven't generalized myPVM₂₃ yet

Equations

• MOlanguageAcceptedBy₃ 𝓚 h𝓚 = MOlanguageAcceptedBy 2 h𝓚