Entanglement measures. (Mixed) convex roof extensions. Definition of product / separable / entangled states are in Braket.lean and/or MState.lean

Important definitions:

• convex_roof: Convex roof extension of g : KetUpToPhase d → ℝ≥0
• mixed_convex_roof: Mixed convex roof extension of f : MState d → ℝ≥0
• EoF: Entanglement of Formation

TODO:

• Other entanglement measures (not necessarily based on convex roof extensions). In roughly increasing order of difficulty to implement: (Logarithmic) Negativity, Entanglement of Purification, Squashed Entanglement, Relative Entropy of Entanglement, Entanglement Cost, Distillable Entanglement. For a compendium on the zoo of entanglement measures, see [1] Christandl, Matthias. “The Structure of Bipartite Quantum States - Insights from Group Theory and Cryptography.” https://doi.org/10.48550/arXiv.quant-ph/0604183.
• Define classes of entanglement measures with good properties, including: monotonicity under LOCC (easier: just LO), monotonicity on average under LOCC, convexity (if the latter two are present, it is called an entanglement monotone by some), vanishing on separable states, normalized on the maximally entangled state, (sub)additivity, regularisible. For other properties, see [1] above and: [2] Szalay, Szilárd. “Multipartite Entanglement Measures.” (mainly Sec. IV) https://doi.org/10.1103/PhysRevA.92.042329. [3] Horodecki, Ryszard, Paweł Horodecki, Michał Horodecki, and Karol Horodecki. “Quantum Entanglement.” https://doi.org/10.1103/RevModPhys.81.865.
• Useful properties of convex roof extensions:
  1. If f is monotonically non-increasing under LOCC, so is its convex roof.
  2. If f ψ is zero if and only if ψ is a product state, then its convex roof is faithful: zero if and only if the mixed state is separable For other properties, see Sec. IV.F of [2] above.

def convex_roof_ENNReal {d : Type} [Fintype d] [DecidableEq d] (g : KetUpToPhase d → NNReal) : MState d → ENNReal

Convex roof extension of a function g : KetUpToPhase d → ℝ≥0, defined as the infimum of all pure-state ensembles of a given ρ of the average of g in that ensemble.

This is valued in the extended nonnegative real numbers ℝ≥0∞ to have good properties of the infimum, which come from the fact that ℝ≥0∞ is a complete lattice. For example, it is necessary for le_iInf and iInf_le_of_le. However, it is also proven in convex_roof_ne_top that the convex roof is never ∞, so the definition convex_roof should be used in most applications.

Equations

• convex_roof_ENNReal g ρ = ⨅ (n : ℕ+), ⨅ (e : PEnsemble d (Fin ↑n)), ⨅ (_ : Ensemble.mix ↑e = ρ), ↑(Ensemble.pure_average_NNReal (g ∘ KetUpToPhase.mk) e)

def mixed_convex_roof_ENNReal {d : Type} [Fintype d] [DecidableEq d] (f : MState d → NNReal) : MState d → ENNReal

Mixed convex roof extension of a function f : MState d → ℝ≥0, defined as the infimum of all mixed-state ensembles of a given ρ of the average of f on that ensemble.

This is valued in the extended nonnegative real numbers ℝ≥0∞ to have good properties of the infimum, which come from the fact that ℝ≥0∞ is a complete lattice (see ENNReal.instCompleteLinearOrder). However, it is also proven in mixed_convex_roof_ne_top that the mixed convex roof is never ∞, so the definition mixed_convex_roof should be used in most applications.

Equations

• mixed_convex_roof_ENNReal f ρ = ⨅ (n : ℕ+), ⨅ (e : MEnsemble d (Fin ↑n)), ⨅ (_ : Ensemble.mix e = ρ), ↑(Ensemble.average_NNReal f e)

theorem convex_roof_ne_top {d : Type} [Fintype d] [Nonempty d] [DecidableEq d] (g : KetUpToPhase d → NNReal) (ρ : MState d) : convex_roof_ENNReal g ρ ≠ ⊤

The convex roof extension convex_roof_ENNReal is never ∞.

theorem mixed_convex_roof_ne_top {d : Type} [Fintype d] [DecidableEq d] (f : MState d → NNReal) (ρ : MState d) : mixed_convex_roof_ENNReal f ρ ≠ ⊤

The convex roof extension mixed_convex_roof_ENNReal is never ∞.

def convex_roof {d : Type} [Fintype d] [Nonempty d] [DecidableEq d] (g : KetUpToPhase d → NNReal) : MState d → NNReal

Convex roof extension of a function g : KetUpToPhase d → ℝ≥0, defined as the infimum of all pure-state ensembles of a given ρ of the average of g in that ensemble.

This is valued in the nonnegative real numbers ℝ≥0 by applying ENNReal.toNNReal to convex_roof_ENNReal. Hence, it should be used in proofs alongside convex_roof_ne_top.

Equations

• convex_roof g x = WithTop.untop (convex_roof_ENNReal g x) ⋯

def mixed_convex_roof {d : Type} [Fintype d] [DecidableEq d] (f : MState d → NNReal) : MState d → NNReal

Mixed convex roof extension of a function f : MState d → ℝ≥0, defined as the infimum of all mixed-state ensembles of a given ρ of the average of f on that ensemble.

This is valued in the nonnegative real numbers ℝ≥0 by applying ENNReal.toNNReal to mixed_convex_roof_ENNReal. Hence, it should be used in proofs alongside mixed_convex_roof_ne_top.

Equations

• mixed_convex_roof f x = WithTop.untop (mixed_convex_roof_ENNReal f x) ⋯

def convex_roof_of_MState_fun {d : Type} [Fintype d] [Nonempty d] [DecidableEq d] (f : MState d → NNReal) : MState d → NNReal

Auxiliary function. Convex roof of a function f : MState d → ℝ≥0 defined over mixed states by restricting f to pure states, via pureQ : KetUpToPhase d → MState d.

Equations

• convex_roof_of_MState_fun f = convex_roof (f ∘ MState.pureQ)

theorem le_mixed_convex_roof {d : Type} [Fintype d] [DecidableEq d] (f : MState d → NNReal) {c : NNReal} (ρ : MState d) : (∀ n > 0, ∀ (e : MEnsemble d (Fin n)), Ensemble.mix e = ρ → c ≤ Ensemble.average_NNReal f e) → c ≤ mixed_convex_roof f ρ

theorem le_convex_roof {d : Type} [Fintype d] [Nonempty d] [DecidableEq d] (g : KetUpToPhase d → NNReal) {c : NNReal} (ρ : MState d) : (∀ n > 0, ∀ (e : PEnsemble d (Fin n)), Ensemble.mix ↑e = ρ → c ≤ Ensemble.pure_average_NNReal (g ∘ KetUpToPhase.mk) e) → c ≤ convex_roof g ρ

theorem convex_roof_le {d : Type} [Fintype d] [Nonempty d] [DecidableEq d] (g : KetUpToPhase d → NNReal) {c : NNReal} (ρ : MState d) : (∃ n > 0, ∃ (e : PEnsemble d (Fin n)), Ensemble.mix ↑e = ρ ∧ Ensemble.pure_average_NNReal (g ∘ KetUpToPhase.mk) e ≤ c) → convex_roof g ρ ≤ c

theorem mixed_convex_roof_le {d : Type} [Fintype d] [DecidableEq d] (f : MState d → NNReal) {c : NNReal} (ρ : MState d) : (∃ n > 0, ∃ (e : MEnsemble d (Fin n)), Ensemble.mix e = ρ ∧ Ensemble.average_NNReal f e ≤ c) → mixed_convex_roof f ρ ≤ c

theorem mixed_convex_roof_le_convex_roof {d : Type} [Fintype d] [Nonempty d] [DecidableEq d] (f : MState d → NNReal) : mixed_convex_roof f ≤ convex_roof_of_MState_fun f

The mixed convex roof extension of f is smaller than or equal to its convex roof extension, since the former minimizes over a larger set of ensembles.

theorem convex_roof_of_pure {d : Type} [Fintype d] [Nonempty d] [DecidableEq d] (g : KetUpToPhase d → NNReal) (ψ : Ket d) : convex_roof g (MState.pure ψ) = g (KetUpToPhase.mk ψ)

The convex roof extension of g : KetUpToPhase d → ℝ≥0 applied to a pure state ψ is g (KetUpToPhase.mk ψ).

theorem mixed_convex_roof_of_pure {d : Type} [Fintype d] [DecidableEq d] (f : MState d → NNReal) (ψ : Ket d) : mixed_convex_roof f (MState.pure ψ) = f (MState.pure ψ)

The mixed convex roof extension of f : MState d → ℝ≥0 applied to a pure state ψ is f (pure ψ).

def EoF {d₁ d₂ : Type} [Fintype d₁] [Fintype d₂] [Nonempty d₁] [Nonempty d₂] [DecidableEq d₁] [DecidableEq d₂] : MState (d₁ × d₂) → NNReal

Entanglement of Formation of bipartite systems. It is the convex roof extension of the von Neumann entropy of one of the subsystems (here chosen to be the left one, but see Entropy.Sᵥₙ_of_partial_eq).

The function Sᵥₙ ∘ traceRight ∘ pure is phase-invariant because pure maps phase-equivalent kets to the same mixed state, so it descends to KetUpToPhase via pureQ.

Equations

• EoF = convex_roof (KetUpToPhase.lift (fun (ψ : Ket (d₁ × d₂)) => ⟨Sᵥₙ (MState.pure ψ).traceRight, ⋯⟩) ⋯)

theorem traceRight_pure_MES (d : Type u_1) [Fintype d] [DecidableEq d] [Nonempty d] : (MState.pure (Ket.MES d)).traceRight = MState.uniform

theorem Sᵥₙ_eq_trace_cfc {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : Sᵥₙ ρ = ((↑ρ).cfc Real.negMulLog).trace

theorem Sᵥₙ_ofClassical {d : Type u_1} [Fintype d] [DecidableEq d] (dist : ProbDistribution d) : Sᵥₙ (MState.ofClassical dist) = Hₛ dist

theorem EoF_of_MES {d : Type} [Fintype d] [Nonempty d] [DecidableEq d] : ↑(EoF (MState.pure (Ket.MES d))) = Real.log ↑Finset.univ.card

The entanglement of formation of the maximally entangled state with on-site dimension 𝕕 is log(𝕕).