class ResourcePretheory (ι : Type u_1) extends Semigroup ι : 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).

The Semigroup ι structure means we have a way to take products of our labels of Hilbert spaces in a way that is associative (with actual equality). The prodEquiv lets us reinterpret between a product-labelled Hilbert spaces, and an actual pair of Hilbert spaces.

• mul : ι → ι → ι
• mul_assoc (a b c : ι) : a * b * c = a * (b * c)
• 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)

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

  The product structure induces an isomorphism of Hilbert spaces

• hAssoc (i j k : ι) : (prodEquiv (i * j) k).trans (((prodEquiv i j).prodCongr (Equiv.refl (H k))).trans ((Equiv.prodAssoc (H i) (H j) (H k)).trans (((Equiv.refl (H i)).prodCongr (prodEquiv j k).symm).trans (prodEquiv i (j * k)).symm))) = Equiv.cast ⋯

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

The prod operation of ResourcePretheory gives the natural product operation on MStates that puts us in a new Hilbert space of the category. 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.

theorem ResourcePretheory.prodRelabel_assoc {ι : Type u_1} [ResourcePretheory ι] {i j k : ι} (ρ₁ : MState (H i)) (ρ₂ : MState (H j)) (ρ₃ : MState (H k)) : prodRelabel (prodRelabel ρ₁ ρ₂) ρ₃ ≍ prodRelabel ρ₁ (prodRelabel ρ₂ ρ₃)

theorem ResourcePretheory.prodRelabel_relabel_cast_prod {ι : Type u_1} [ResourcePretheory ι] {i j k l : ι} (ρ₁ : MState (H i)) (ρ₂ : MState (H j)) (h : H (k * l) = H (i * j)) (hik : k = i) (hlj : l = j) : (prodRelabel ρ₁ ρ₂).relabel (Equiv.cast h) = prodRelabel (ρ₁.relabel (Equiv.cast ⋯)) (ρ₂.relabel (Equiv.cast ⋯))

A MState.relabel can be distributed across a prodRelabel, if you have proofs that the factors correspond correctly.

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 (i * k)) (H (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.ofEquiv (ResourcePretheory.prodEquiv j l).symm∘ₘ((M₁⊗ₖM₂)∘ₘCPTPMap.ofEquiv (ResourcePretheory.prodEquiv i k))

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

Equations

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

theorem ResourcePretheory.PosDef.prod {ι : Type u_1} [ResourcePretheory ι] {i j : ι} {ρ : MState (H i)} {σ : MState (H j)} (hρ : ρ.m.PosDef) (hσ : σ.m.PosDef) : (prodRelabel ρ σ).m.PosDef

@[simp]

theorem ResourcePretheory.qRelEntropy_prodRelabel {ι : Type u_1} [ResourcePretheory ι] {i j : ι} (ρ₁ ρ₂ : MState (H i)) (σ₁ σ₂ : MState (H j)) : 𝐃(prodRelabel ρ₁ σ₁‖prodRelabel ρ₂ σ₂) = 𝐃(ρ₁‖ρ₂) + 𝐃(σ₁‖σ₂)

@[simp]

theorem ResourcePretheory.sandwichedRelRentropy_prodRelabel {ι : Type u_1} [ResourcePretheory ι] {i j : ι} {α : ℝ} (ρ₁ ρ₂ : MState (H i)) (σ₁ σ₂ : MState (H j)) : D̃_α(prodRelabel ρ₁ σ₁‖prodRelabel ρ₂ σ₂) = D̃_α(ρ₁‖ρ₂) + D̃_α(σ₁‖σ₂)

class UnitalPretheory (ι : Type u_1) extends ResourcePretheory ι, MulOneClass ι, Unique (ResourcePretheory.H 1) : Type (max u_1 (u_2 + 1))

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

• mul : ι → ι → ι
• mul_assoc (a b c : ι) : a * b * c = a * (b * c)
• H : ι → Type u_2
• FinH (i : ι) : Fintype (H i)
• DecEqH (i : ι) : DecidableEq (H i)
• NonemptyH (i : ι) : Nonempty (H i)
• prodEquiv (i j : ι) : H (i * j) ≃ H i × H j
• hAssoc (i j k : ι) : (prodEquiv (i * j) k).trans (((prodEquiv i j).prodCongr (Equiv.refl (H k))).trans ((Equiv.prodAssoc (H i) (H j) (H k)).trans (((Equiv.refl (H i)).prodCongr (prodEquiv j k).symm).trans (prodEquiv i (j * k)).symm))) = Equiv.cast ⋯
• one : ι
• one_mul (a : ι) : 1 * a = a
• mul_one (a : ι) : a * 1 = a
• default : ResourcePretheory.H 1
• uniq (a : ResourcePretheory.H 1) : a = default
• prod_default {i : ι} (ρ : MState (ResourcePretheory.H i)) : ResourcePretheory.prodRelabel ρ default ≍ ρ
• default_prod {i : ι} (ρ : MState (ResourcePretheory.H i)) : ResourcePretheory.prodRelabel default ρ ≍ ρ

instance UnitalPretheory.instMonoid {ι : Type u_1} [UnitalPretheory ι] : Monoid ι

Equations

• UnitalPretheory.instMonoid = { toSemigroup := inst✝.toSemigroup, toOne := inst✝.toMulOneClass.toOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }

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

Powers of spaces.

We define it for Nat in a UnitalPretheory. In principal this could be done for any ResourcePretheory and be defined for PNat so that we don't have zeroth powers. In anticipation that we might some day want that, and that we might do everything with a non-equality associator, we keep this as its own definition and keep our own names for rewriting theorems where possible.

Equations

• UnitalPretheory.spacePow i n = i ^ n

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

Equations

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

@[simp]

theorem UnitalPretheory.spacePow_zero {ι : Type u_1} [UnitalPretheory ι] (i : ι) : i ^ 0 = 1

@[simp]

theorem UnitalPretheory.spacePow_one {ι : Type u_1} [UnitalPretheory ι] (i : ι) : i ^ 1 = i

theorem UnitalPretheory.spacePow_succ {ι : Type u_1} [UnitalPretheory ι] (i : ι) (n : ℕ) : i ^ (n + 1) = i ^ n * i

theorem UnitalPretheory.spacePow_add {ι : Type u_1} [UnitalPretheory ι] {i : ι} (m n : ℕ) : i ^ (m + n) = i ^ m * i ^ n

theorem UnitalPretheory.spacePow_mul {ι : Type u_1} [UnitalPretheory ι] {i : ι} (m n : ℕ) : i ^ (m * n) = (i ^ m) ^ n

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

Powers of states, using the resource theory's notion of product.

Equations

• UnitalPretheory.statePow ρ n = Nat.rec default (fun (x : ℕ) (σ : MState (ResourcePretheory.H (i ^ x))) => ResourcePretheory.prodRelabel σ ρ) n

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

Equations

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

@[simp]

theorem UnitalPretheory.statePow_zero {ι : Type u_1} [UnitalPretheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) : statePow ρ 0 = default

@[simp]

theorem UnitalPretheory.statePow_one {ι : Type u_1} [UnitalPretheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) : statePow ρ 1 ≍ ρ

theorem UnitalPretheory.statePow_succ {ι : Type u_1} [UnitalPretheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) (n : ℕ) : statePow ρ (n + 1) = ResourcePretheory.prodRelabel (statePow ρ n) ρ

theorem UnitalPretheory.statePow_add {ι : Type u_1} [UnitalPretheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) (m n : ℕ) : statePow ρ (m + n) ≍ ResourcePretheory.prodRelabel (statePow ρ m) (statePow ρ n)

theorem UnitalPretheory.statePow_add_relabel {ι : Type u_1} [UnitalPretheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) (m n : ℕ) : statePow ρ (m + n) = (ResourcePretheory.prodRelabel (statePow ρ m) (statePow ρ n)).relabel (Equiv.cast ⋯)

theorem UnitalPretheory.statePow_mul {ι : Type u_1} [UnitalPretheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) (m n : ℕ) : statePow ρ (m * n) ≍ statePow (statePow ρ m) n

theorem UnitalPretheory.statePow_mul_relabel {ι : Type u_1} [UnitalPretheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) (m n : ℕ) : statePow ρ (m * n) = (statePow (statePow ρ m) n).relabel (Equiv.cast ⋯)

theorem UnitalPretheory.PosDef.npow {ι : Type u_1} [UnitalPretheory ι] {i : ι} {ρ : MState (ResourcePretheory.H i)} (hρ : ρ.m.PosDef) (n : ℕ) : (statePow ρ n).m.PosDef

theorem UnitalPretheory.statePow_rw {ι : Type u_1} [UnitalPretheory ι] {i : ι} {n m : ℕ} (h : n = m) (ρ : MState (ResourcePretheory.H i)) : statePow ρ n = (statePow ρ m).relabel (Equiv.cast ⋯)

@[simp]

theorem UnitalPretheory.qRelEntropy_statePow {ι : Type u_1} [UnitalPretheory ι] {i : ι} (ρ σ : MState (ResourcePretheory.H i)) (n : ℕ) : 𝐃(statePow ρ n‖statePow σ n) = ↑n * 𝐃(ρ‖σ)

@[simp]

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

@[simp]

theorem HermitianMat.one_rpow {d : Type u_2} [Fintype d] [DecidableEq d] (r : ℝ) : 1 ^ r = 1

@[simp]

theorem HermitianMat.trace_one {d : Type u_2} [Fintype d] [DecidableEq d] : trace 1 = ↑(Fintype.card d)

@[simp]

theorem sandwichedRelRentropy_of_unique {d : Type u_2} [Fintype d] [DecidableEq d] [Unique d] (ρ σ : MState d) (α : ℝ) : D̃_α(ρ‖σ) = 0

@[simp]

theorem UnitalPretheory.sandwichedRelRentropy_statePow {ι : Type u_1} [UnitalPretheory ι] {i : ι} {α : ℝ} (ρ σ : MState (ResourcePretheory.H i)) (n : ℕ) : D̃_α(statePow ρ n‖statePow σ n) = ↑n * D̃_α(ρ‖σ)

theorem UnitalPretheory.sandwichedRelRentropy_heq_congr {α : ℝ} {d₁ d₂ : Type u} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] {ρ₁ σ₁ : MState d₁} {ρ₂ σ₂ : MState d₂} (hd : d₁ = d₂) (hρ : ρ₁ ≍ ρ₂) (hσ : σ₁ ≍ σ₂) : D̃_α(ρ₁‖σ₁) = D̃_α(ρ₂‖σ₂)

theorem UnitalPretheory.sandwichedRelRentropy_congr {α : ℝ} {d₁ d₂ : Type u} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] {ρ₁ σ₁ : MState d₁} {ρ₂ σ₂ : MState d₂} (hd : d₁ = d₂) (hρ : ρ₁ = ρ₂.relabel (Equiv.cast hd)) (hσ : σ₁ = σ₂.relabel (Equiv.cast hd)) : D̃_α(ρ₁‖σ₁) = D̃_α(ρ₂‖σ₂)

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).

• mul : ι → ι → ι
• mul_assoc (a b c : ι) : a * b * c = a * (b * c)
• H : ι → Type u_2
• FinH (i : ι) : Fintype (H i)
• DecEqH (i : ι) : DecidableEq (H i)
• NonemptyH (i : ι) : Nonempty (H i)
• prodEquiv (i j : ι) : H (i * j) ≃ H i × H j
• hAssoc (i j k : ι) : (prodEquiv (i * j) k).trans (((prodEquiv i j).prodCongr (Equiv.refl (H k))).trans ((Equiv.prodAssoc (H i) (H j) (H k)).trans (((Equiv.refl (H i)).prodCongr (prodEquiv j k).symm).trans (prodEquiv i (j * k)).symm))) = Equiv.cast ⋯
• 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)), ρ.m.PosDef ∧ IsFree ρ

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

noncomputable instance FreeStateTheory.Inhabited_IsFree {ι : Type u_1} [FreeStateTheory ι] {i : ι} : Inhabited ↑IsFree

Equations

• FreeStateTheory.Inhabited_IsFree = { default := ⟨⋯.choose, ⋯⟩ }

theorem FreeStateTheory.IsFree.of_unique {ι : Type u_1} [FreeStateTheory ι] {i : ι} [Unique (ResourcePretheory.H i)] (ρ : MState (ResourcePretheory.H i)) : ρ ∈ IsFree

theorem FreeStateTheory.IsCompact_IsFree {ι : Type u_1} [FreeStateTheory ι] {i : ι} : IsCompact IsFree

The set of free states is compact because it's a closed subset of a compact space.

theorem FreeStateTheory.IsFree.mix {ι : Type u_2} [FreeStateTheory ι] {i : ι} {σ₁ σ₂ : MState (ResourcePretheory.H i)} (hσ₁ : IsFree σ₁) (hσ₂ : IsFree σ₂) (p : Prob) : IsFree (p[σ₁↔σ₂])

class UnitalFreeStateTheory (ι : Type u_1) extends FreeStateTheory ι, UnitalPretheory ι : Type (max u_1 (u_2 + 1))

• mul : ι → ι → ι
• mul_assoc (a b c : ι) : a * b * c = a * (b * c)
• H : ι → Type u_2
• FinH (i : ι) : Fintype (H i)
• DecEqH (i : ι) : DecidableEq (H i)
• NonemptyH (i : ι) : Nonempty (H i)
• prodEquiv (i j : ι) : H (i * j) ≃ H i × H j
• hAssoc (i j k : ι) : (prodEquiv (i * j) k).trans (((prodEquiv i j).prodCongr (Equiv.refl (H k))).trans ((Equiv.prodAssoc (H i) (H j) (H k)).trans (((Equiv.refl (H i)).prodCongr (prodEquiv j k).symm).trans (prodEquiv i (j * k)).symm))) = Equiv.cast ⋯
• IsFree {i : ι} : Set (MState (ResourcePretheory.H i))
• free_closed {i : ι} : IsClosed IsFree
• free_convex {i : ι} : Convex ℝ (MState.M '' IsFree)
• free_prod {i j : ι} {ρ₁ : MState (ResourcePretheory.H i)} {ρ₂ : MState (ResourcePretheory.H j)} (h₁ : IsFree ρ₁) (h₂ : IsFree ρ₂) : IsFree (ResourcePretheory.prodRelabel ρ₁ ρ₂)
• free_fullRank (i : ι) : ∃ (ρ : MState (ResourcePretheory.H i)), ρ.m.PosDef ∧ IsFree ρ
• one : ι
• one_mul (a : ι) : 1 * a = a
• mul_one (a : ι) : a * 1 = a
• default : ResourcePretheory.H 1
• uniq (a : ResourcePretheory.H 1) : a = default
• prod_default {i : ι} (ρ : MState (ResourcePretheory.H i)) : ResourcePretheory.prodRelabel ρ default ≍ ρ
• default_prod {i : ι} (ρ : MState (ResourcePretheory.H i)) : ResourcePretheory.prodRelabel default ρ ≍ ρ

theorem FreeStateTheory.IsFree.npow {ι : Type u_1} [UnitalFreeStateTheory ι] {i : ι} {ρ : MState (ResourcePretheory.H i)} (hρ : IsFree ρ) (n : ℕ) : IsFree (UnitalPretheory.statePow ρ n)

@[simp]

theorem UnitalFreeStateTheory.relabel_cast_isFree {ι : Type u_1} [UnitalFreeStateTheory ι] {i j : ι} (ρ : MState (ResourcePretheory.H i)) (h : j = i) {h' : ResourcePretheory.H j = ResourcePretheory.H i} : ρ.relabel (Equiv.cast h') ∈ FreeStateTheory.IsFree ↔ ρ ∈ FreeStateTheory.IsFree

theorem UnitalFreeStateTheory.relativeEntResource_ne_top {ι : Type u_1} [UnitalFreeStateTheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) : ⨅ σ ∈ FreeStateTheory.IsFree, 𝐃(ρ‖σ) ≠ ⊤

In a FreeStateTheory, we have free states of full rank, therefore the minimum relative entropy of any state ρ to a free state is finite.

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

Equations

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

def UnitalFreeStateTheory.«term𝑅ᵣ» : Lean.ParserDescr

Equations

• UnitalFreeStateTheory.«term𝑅ᵣ» = Lean.ParserDescr.node `UnitalFreeStateTheory.«term𝑅ᵣ» 1024 (Lean.ParserDescr.symbol "𝑅ᵣ")

theorem UnitalFreeStateTheory.exists_isFree_relativeEntResource {ι : Type u_1} [UnitalFreeStateTheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) : ∃ σ ∈ FreeStateTheory.IsFree, 𝐃(ρ‖σ) = ↑(RelativeEntResource ρ)

theorem UnitalFreeStateTheory.RelativeEntResource.Subadditive {ι : Type u_1} [UnitalFreeStateTheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) : _root_.Subadditive fun (n : ℕ) => ↑(RelativeEntResource (UnitalPretheory.statePow ρ n))

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

Equations

• UnitalFreeStateTheory.RegularizedRelativeEntResource ρ = ⟨⋯.lim, ⋯⟩

def UnitalFreeStateTheory.«term𝑅ᵣ∞» : Lean.ParserDescr

Equations

• UnitalFreeStateTheory.«term𝑅ᵣ∞» = Lean.ParserDescr.node `UnitalFreeStateTheory.«term𝑅ᵣ∞» 1024 (Lean.ParserDescr.symbol "𝑅ᵣ∞")

theorem UnitalFreeStateTheory.RelativeEntResource.tendsto {ι : Type u_1} [UnitalFreeStateTheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) : Filter.Tendsto (fun (n : ℕ) => RelativeEntResource (UnitalPretheory.statePow ρ n) / ↑n) Filter.atTop (nhds (RegularizedRelativeEntResource ρ))

Lemma 5

theorem UnitalFreeStateTheory.RelativeEntResource.tendsto_ennreal {ι : Type u_1} [UnitalFreeStateTheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) : Filter.Tendsto (fun (n : ℕ) => (⨅ σ ∈ FreeStateTheory.IsFree, 𝐃(UnitalPretheory.statePow ρ n‖σ)) / ↑n) Filter.atTop (nhds ↑(RegularizedRelativeEntResource ρ))

Alternate version of Lemma 5 which states the convergence with the ENNReal expression for RelativeEntResource, as opposed its untop-ped NNReal value.

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

Equations

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

def UnitalFreeStateTheory.IsAsymptoticallyNongenerating {ι : Type u_1} [UnitalFreeStateTheory ι] (dI dO : ι) (f : (n : ℕ) → CPTPMap (ResourcePretheory.H (UnitalPretheory.spacePow dI n)) (ResourcePretheory.H (UnitalPretheory.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.