@[reducible, inline]

abbrev MEnsemble (d : Type u_1) (α : Type u_2) [Fintype d] [DecidableEq d] [Fintype α] : Type (max u_2 u_1)

A mixed-state ensemble is a random variable valued in MState d. That is, a collection of mixed states var : α → MState d, each with their own probability weight described by distr : Distribution α.

Equations

• MEnsemble d α = Distribution.RandVar α (MState d)

@[reducible, inline]

abbrev PEnsemble (d : Type u_1) (α : Type u_2) [Fintype d] [Fintype α] : Type (max u_2 u_1)

A pure-state ensemble is a random variable valued in Ket d. That is, a collection of pure states var : α → Ket d, each with their own probability weight described by distr : Distribution α.

Equations

• PEnsemble d α = Distribution.RandVar α (Ket d)

@[reducible, inline]

abbrev MEnsemble.states {α : Type u_1} {d : Type u_3} [Fintype d] [DecidableEq d] [Fintype α] : MEnsemble d α → α → MState d

Alias for Distribution.var for mixed-state ensembles.

Equations

• MEnsemble.states = Distribution.RandVar.var

@[reducible, inline]

abbrev PEnsemble.states {α : Type u_1} {d : Type u_3} [Fintype d] [Fintype α] : PEnsemble d α → α → Ket d

Alias for Distribution.var for pure-state ensembles.

Equations

• PEnsemble.states = Distribution.RandVar.var

def Ensemble.toMEnsemble {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] : PEnsemble d α → MEnsemble d α

A pure-state ensemble is a mixed-state ensemble if all kets are interpreted as mixed states.

Equations

• Ensemble.toMEnsemble = Functor.map MState.pure

instance Ensemble.instCoePEnsembleMEnsemble {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] : Coe (PEnsemble d α) (MEnsemble d α)

Equations

• Ensemble.instCoePEnsembleMEnsemble = { coe := Ensemble.toMEnsemble }

@[simp]

theorem Ensemble.toMEnsemble_mk {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] {ps : α → Ket d} {distr : Distribution α} : ↑{ var := ps, distr := distr } = { var := MState.pure ∘ ps, distr := distr }

theorem Ensemble.coe_PEnsemble_iff_pure_states {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] (me : MEnsemble d α) : (∃ (pe : PEnsemble d α), ↑pe = me) ↔ ∃ (ψ : α → Ket d), me.states = MState.pure ∘ ψ

A mixed-state ensemble comes from a pure-state ensemble if and only if all states are pure.

def Ensemble.mix {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] (e : MEnsemble d α) : MState d

The resulting mixed state after mixing the states in an ensemble with their respective probability weights. Note that, generically, a single mixed state has infinitely many ensembles that mixes into it.

Equations

• Ensemble.mix e = Distribution.expect_val e

@[simp]

theorem Ensemble.mix_of {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] (e : MEnsemble d α) : (mix e).m = ∑ i : α, ↑(e.distr i) • (e.states i).m

def Ensemble.congrMEnsemble {α : Type u_1} {β : Type u_2} {d : Type u_3} [Fintype α] [Fintype β] [Fintype d] [DecidableEq d] (σ : α ≃ β) : MEnsemble d α ≃ MEnsemble d β

Two mixed-state ensembles indexed by \alpha and \beta are equivalent if α ≃ β.

Equations

• Ensemble.congrMEnsemble σ = Distribution.congrRandVar σ

def Ensemble.congrPEnsemble {α : Type u_1} {β : Type u_2} {d : Type u_3} [Fintype α] [Fintype β] [Fintype d] (σ : α ≃ β) : PEnsemble d α ≃ PEnsemble d β

Two pure-state ensembles indexed by \alpha and \beta are equivalent if α ≃ β.

Equations

• Ensemble.congrPEnsemble σ = Distribution.congrRandVar σ

@[simp]

theorem Ensemble.mix_congrMEnsemble_eq_mix {α : Type u_1} {β : Type u_2} {d : Type u_3} [Fintype α] [Fintype β] [Fintype d] [DecidableEq d] (σ : α ≃ β) (e : MEnsemble d α) : mix ((congrMEnsemble σ) e) = mix e

Equivalence of mixed-state ensembles leaves the resulting mixed state invariant

@[simp]

theorem Ensemble.mix_congrPEnsemble_eq_mix {α : Type u_1} {β : Type u_2} {d : Type u_3} [Fintype α] [Fintype β] [Fintype d] [DecidableEq d] (σ : α ≃ β) (e : PEnsemble d α) : mix ↑((congrPEnsemble σ) e) = mix ↑e

Equivalence of pure-state ensembles leaves the resulting mixed state invariant

def Ensemble.average {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] {T : Type u_3} {U : Type u_4} [AddCommGroup U] [Module ℝ U] [inst : Mixable U T] (f : MState d → T) (e : MEnsemble d α) : T

The average of a function f : MState d → T, where T is of Mixable U T instance, on a mixed-state ensemble e is the expectation value of f acting on the states of e, with the corresponding probability weights from e.distr.

Equations

• Ensemble.average f e = Distribution.expect_val (f <$> e)

def Ensemble.average_NNReal {α : Type u_1} [Fintype α] {d : Type} [Fintype d] [DecidableEq d] (f : MState d → NNReal) (e : MEnsemble d α) : NNReal

A version of average conveniently specialized for functions f : MState d → ℝ≥0 returning nonnegative reals. Notably, the average is also a nonnegative real number.

Equations

• Ensemble.average_NNReal f e = ⟨Ensemble.average (NNReal.toReal ∘ f) e, ⋯⟩

def Ensemble.pure_average {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] {T : Type u_3} {U : Type u_4} [AddCommGroup U] [Module ℝ U] [inst : Mixable U T] (f : Ket d → T) (e : PEnsemble d α) : T

The average of a function f : Ket d → T, where T is of Mixable U T instance, on a pure-state ensemble e is the expectation value of f acting on the states of e, with the corresponding probability weights from e.distr.

Equations

• Ensemble.pure_average f e = Distribution.expect_val (f <$> e)

def Ensemble.pure_average_NNReal {α : Type u_1} [Fintype α] {d : Type} [Fintype d] (f : Ket d → NNReal) (e : PEnsemble d α) : NNReal

A version of average conveniently specialized for functions f : Ket d → ℝ≥0 returning nonnegative reals. Notably, the average is also a nonnegative real number.

Equations

• Ensemble.pure_average_NNReal f e = ⟨Ensemble.pure_average (NNReal.toReal ∘ f) e, ⋯⟩

theorem Ensemble.average_of_pure_ensemble {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] {T : Type u_3} {U : Type u_4} [AddCommGroup U] [Module ℝ U] [inst : Mixable U T] (f : MState d → T) (e : PEnsemble d α) : average f ↑e = pure_average (f ∘ MState.pure) e

The average of f : MState d → T on a coerced pure-state ensemble ↑e : MEnsemble d α is equal to averaging the restricted function over Kets f ∘ pure : Ket d → T on e.

theorem Ensemble.mix_pEnsemble_pure_iff_pure {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] {ψ : Ket d} {e : PEnsemble d α} : mix ↑e = MState.pure ψ ↔ ∀ (i : α), e.distr i ≠ 0 → e.states i = ψ

A pure-state ensemble mixes into a pure state if and only if the only states in the ensemble with nonzero probability are equal to ψ

theorem Ensemble.mix_pEnsemble_pure_average {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] {ψ : Ket d} {e : PEnsemble d α} {T : Type u_3} {U : Type u_4} [AddCommGroup U] [Module ℝ U] [inst : Mixable U T] (f : Ket d → T) (hmix : mix ↑e = MState.pure ψ) : pure_average f e = f ψ

The average of f : Ket d → T on an ensemble that mixes to a pure state ψ is f ψ

theorem Ensemble.mix_mEnsemble_pure_iff_pure {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] {ψ : Ket d} {e : MEnsemble d α} : mix e = MState.pure ψ ↔ ∀ (i : α), e.distr i ≠ 0 → e.states i = MState.pure ψ

A mixed-state ensemble mixes into a pure state if and only if the only states in the ensemble with nonzero probability are equal to pure ψ

theorem Ensemble.mix_mEnsemble_pure_average {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] {ψ : Ket d} {e : MEnsemble d α} {T : Type u_3} {U : Type u_4} [AddCommGroup U] [Module ℝ U] [inst : Mixable U T] (f : MState d → T) (hmix : mix e = MState.pure ψ) : average f e = f (MState.pure ψ)

The average of f : MState d → T on an ensemble that mixes to a pure state ψ is f (pure ψ)

def Ensemble.trivial_mEnsemble {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] (ρ : MState d) (i : α) : MEnsemble d α

The trivial mixed-state ensemble of ρ consists of copies of rho, with the i-th one having probability 1.

Equations

• Ensemble.trivial_mEnsemble ρ i = { var := fun (x : α) => ρ, distr := Distribution.constant i }

theorem Ensemble.trivial_mEnsemble_mix {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] (ρ : MState d) (i : α) : mix (trivial_mEnsemble ρ i) = ρ

The trivial mixed-state ensemble of ρ mixes to ρ

theorem Ensemble.trivial_mEnsemble_average {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] {T : Type u_3} {U : Type u_4} [AddCommGroup U] [Module ℝ U] [inst : Mixable U T] (f : MState d → T) (ρ : MState d) (i : α) : average f (trivial_mEnsemble ρ i) = f ρ

The average of f : MState d → T on a trivial ensemble of ρ is f ρ

instance Ensemble.MEnsemble.instInhabited {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] [Nonempty d] [Inhabited α] : Inhabited (MEnsemble d α)

Equations

• Ensemble.MEnsemble.instInhabited = { default := Ensemble.trivial_mEnsemble default default }

def Ensemble.trivial_pEnsemble {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] (ψ : Ket d) (i : α) : PEnsemble d α

The trivial pure-state ensemble of ψ consists of copies of ψ, with the i-th one having probability 1.

Equations

• Ensemble.trivial_pEnsemble ψ i = { var := fun (x : α) => ψ, distr := Distribution.constant i }

theorem Ensemble.trivial_pEnsemble_mix {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [DecidableEq d] (ψ : Ket d) (i : α) : mix ↑(trivial_pEnsemble ψ i) = MState.pure ψ

The trivial pure-state ensemble of ψ mixes to ψ

theorem Ensemble.trivial_pEnsemble_average {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] {T : Type u_3} {U : Type u_4} [AddCommGroup U] [Module ℝ U] [inst : Mixable U T] (f : Ket d → T) (ψ : Ket d) (i : α) : pure_average f (trivial_pEnsemble ψ i) = f ψ

The average of f : Ket d → T on a trivial ensemble of ψ is f ψ

instance Ensemble.PEnsemble.instInhabited {α : Type u_1} {d : Type u_3} [Fintype α] [Fintype d] [Nonempty d] [Inhabited α] : Inhabited (PEnsemble d α)

Equations

• Ensemble.PEnsemble.instInhabited = { default := Ensemble.trivial_pEnsemble default default }

def Ensemble.spectral_ensemble {d : Type u_3} [Fintype d] [DecidableEq d] (ρ : MState d) : PEnsemble d d

The spectral pure-state ensemble of ρ. The states are its eigenvectors, and the probabilities, eigenvalues.

Equations

• Ensemble.spectral_ensemble ρ = { var := fun (i : d) => { vec := ⋯.eigenvectorBasis i, normalized' := ⋯ }, distr := ρ.spectrum }

theorem Ensemble.spectral_ensemble_mix {d : Type u_3} [Fintype d] [DecidableEq d] {ρ : MState d} : mix ↑(spectral_ensemble ρ) = ρ

The spectral pure-state ensemble of ρ mixes to ρ