class ResourcePretheory (ι : Type u_1) : Type (max u_1 (u_2 + 1))

A ResourcePretheory is a family of Hilbert spaces closed under tensor products, with an instance of Fintype and DecidableEq for each. It forms a pre-structure then on which to discuss resource theories. For instance, to talk about "two-party scenarios", we could write ResourcePretheory (ℕ × ℕ), with H (a,b) := (Fin a) × (Fin b).

• H : ι → Type u_2

  The indexing of each Hilbert space

• FinH (i : ι) : Fintype (H i)

  Each space is finite

• DecEqH (i : ι) : DecidableEq (H i)

  Each object has decidable equality

• NonemptyH (i : ι) : Nonempty (H i)

  Each space is nonempty (dimension at least 1)

• prod : ι → ι → ι

  The Hilbert spaces must have a product structure.

• prodEquiv (i j : ι) : H (prod i j) ≃ H i × H j

  The product structure induces an isomorphism of Hilbert spaces

instance ResourcePretheory.instQRT_FintypeH {ι : Type u_1} [ResourcePretheory ι] (i : ι) : Fintype (H i)

Equations

• ResourcePretheory.instQRT_FintypeH i = ResourcePretheory.FinH i

instance ResourcePretheory.instQRT_DecEqH {ι : Type u_1} [ResourcePretheory ι] (i : ι) : DecidableEq (H i)

Equations

• ResourcePretheory.instQRT_DecEqH i = ResourcePretheory.DecEqH i

instance ResourcePretheory.instQRT_NonemptyH {ι : Type u_1} [ResourcePretheory ι] (i : ι) : Nonempty (H i)

def ResourcePretheory.prodRelabel {ι : Type u_1} [ResourcePretheory ι] {i j : ι} (ρ₁ : MState (H i)) (ρ₂ : MState (H j)) : MState (H (prod i j))

The prod operation of ResourcePretheory gives the natural product operation on MStates. Accessible by the notation ρ₁ ⊗ᵣ ρ₂.

Equations

• ResourcePretheory.prodRelabel ρ₁ ρ₂ = (ρ₁⊗ρ₂).relabel (ResourcePretheory.prodEquiv i j)

def ResourcePretheory.«term_⊗ᵣ_» : Lean.TrailingParserDescr

Equations

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

noncomputable def ResourcePretheory.prodCPTPMap {ι : Type u_1} [ResourcePretheory ι] {i j k l : ι} (M₁ : CPTPMap (H i) (H j)) (M₂ : CPTPMap (H k) (H l)) : CPTPMap (H (prod i k)) (H (prod j l))

The prod operation of ResourcePretheory gives the natural product operation on CPTPMaps. Accessible by the notation M₁ ⊗ᵣ M₂.

Equations

• ResourcePretheory.prodCPTPMap M₁ M₂ = (CPTPMap.of_equiv (ResourcePretheory.prodEquiv j l).symm).compose ((M₁⊗M₂).compose (CPTPMap.of_equiv (ResourcePretheory.prodEquiv i k)))

def ResourcePretheory.«term_⊗ᵣ__1» : Lean.TrailingParserDescr

Equations

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

noncomputable def ResourcePretheory.spacePow {ι : Type u_1} [ResourcePretheory ι] (i : ι) (n : ℕ+) : ι

Powers of spaces. Defined for PNat so that we don't have zeroth powers.

Equations

• ResourcePretheory.spacePow i n = Nat.rec i (fun (x : ℕ) (j : ι) => ResourcePretheory.prod i j) n.natPred

def ResourcePretheory.«term_⊗^[_]» : Lean.TrailingParserDescr

Equations

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

noncomputable def ResourcePretheory.statePow {ι : Type u_1} [ResourcePretheory ι] {i : ι} (ρ : MState (H i)) (n : ℕ+) : MState (H (spacePow i n))

Powers of states. Defined for PNat, so that we don't have zeroth powers

Equations

• ResourcePretheory.statePow ρ n = Nat.rec ρ (fun (x : ℕ) (σ : MState (ResourcePretheory.H (ResourcePretheory.spacePow i x.succPNat))) => ResourcePretheory.prodRelabel ρ σ) n.natPred

def ResourcePretheory.«term_⊗^[_]_1» : Lean.TrailingParserDescr

Equations

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

class ResourcePretheory.Unital (ι : Type u_2) [ResourcePretheory ι] : Type (max u_2 u_3)

A ResourcePretheory is Unital if it has a Hilbert space of size 1, i.e. ℂ.

• unit : ι
• unit_unique : Unique (H unit)

instance ResourcePretheory.instUnitalUnique {ι : Type u_1} [ResourcePretheory ι] [u : Unital ι] : Unique (H Unital.unit)

Equations

• ResourcePretheory.instUnitalUnique = ResourcePretheory.Unital.unit_unique

class FreeStateTheory (ι : Type u_1) extends ResourcePretheory ι : Type (max u_1 (u_2 + 1))

A FreeStateTheory is a collection of mixed states (MStates) in a ResourcePretheory that obeys some necessary axioms:

• For each Hilbert space H i, the free states are a closed, convex set
• For each Hilbert space H i, there is a free state of full rank
• If ρᵢ ∈ H i and ρⱼ ∈ H j are free, then ρᵢ ⊗ ρⱼ is free in H (prod i j).

• H : ι → Type u_2
• FinH (i : ι) : Fintype (H i)
• DecEqH (i : ι) : DecidableEq (H i)
• NonemptyH (i : ι) : Nonempty (H i)
• prod : ι → ι → ι
• prodEquiv (i j : ι) : H (prod i j) ≃ H i × H j
• IsFree {i : ι} : Set (MState (ResourcePretheory.H i))

  The set of states we're calling "free"

• free_closed {i : ι} : IsClosed IsFree

  The set F(H) of free states is closed

• free_convex {i : ι} : Convex ℝ (MState.m '' IsFree)

  The set F(H) of free states is convex (more precisely, their matrices are)

• free_prod {i j : ι} {ρ₁ : MState (ResourcePretheory.H i)} {ρ₂ : MState (ResourcePretheory.H j)} (h₁ : IsFree ρ₁) (h₂ : IsFree ρ₂) : IsFree (ResourcePretheory.prodRelabel ρ₁ ρ₂)

  The set of free states is closed under tensor product

• free_fullRank (i : ι) : ∃ (ρ : MState (ResourcePretheory.H i)), 0 < ↑ρ ∧ IsFree ρ

  The set F(H) of free states contains a full-rank state ρfull, equivalently ρfull is positive definite.

noncomputable def RelativeEntResource {ι : Type u_1} [FreeStateTheory ι] {i : ι} : MState (ResourcePretheory.H i) → NNReal

Equations

• RelativeEntResource ρ = WithTop.untop (⨅ σ ∈ FreeStateTheory.IsFree, 𝐃(ρ‖σ)) ⋯

noncomputable def RegularizedRelativeEntResource {ι : Type u_1} [FreeStateTheory ι] {i : ι} : MState (ResourcePretheory.H i) → NNReal

Equations

• RegularizedRelativeEntResource = sorry

noncomputable def GlobalRobustness {ι : Type u_1} [FreeStateTheory ι] {i : ι} : MState (ResourcePretheory.H i) → NNReal

Equations

• GlobalRobustness ρ = sInf {s : NNReal | ∃ (σ : MState (ResourcePretheory.H i)), FreeStateTheory.IsFree (⟨1 / (1 + ↑s), ⋯⟩[ρ↔σ])}

def IsAsymptoticallyNongenerating {ι : Type u_1} [FreeStateTheory ι] (dI dO : ι) (f : (n : ℕ+) → CPTPMap (ResourcePretheory.H (ResourcePretheory.spacePow dI n)) (ResourcePretheory.H (ResourcePretheory.spacePow dO n))) : Prop

A sequence of operations f_n is asymptotically nongenerating if lim_{n→∞} RG(f_n(ρ_n)) = 0, where RG is GlobalRobustness and ρ_n is any sequence of free states. Equivalently, we can take the max ( over operations and states) on the left-hand side inside the limit.

Equations

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