Coherence in Athermality

• “Convert quantum state under Time-translation covariant channels.”

• Consider Hamiltonians with non-degenerate Bohr spectrum.

  • Almost all Hamiltonians have such a spectrum.

  • But some do not, e.g. the Hamiltonian of the harmonic oscillator.

    • For such Hamiltonians, some of our results do not apply”

import Twirl
import Athermality

def nonuniformity ρ γ := athermality (twirl ρ) γ

/-- coherence between energy eigenspaces -/
def time_asymmetry ρ :=
quantum_relative_entropy (twirl ρ) ρ

def coherence := time_asymmetry

/-
theorem III2 :
Time-translation asymmetry to determine
if ∃ [time_trans_cov 𝒩], 𝒩 ρ = σ
-/

/-- composite resource -/
lemma athermality_eq_nonuniformity_plus_coherence :
  athermality ρ γ = (nonuniformity ρ γ) + (coherence ρ) :=
sorry

/- If sublinear amount of coherence among energy levels are free,
then resource theory of athermality would become trivial -/

def energy_spread [pure ψ] :=
(max energy_eigenvalues ψ) - (min energy_eigenvalues ψ)

---

“Convert one Athermality state (ρA, γA) to another (σB, γB).”

Let J be free operations of Athermality.”

/-- Conversion distance -/
def d J ( (ρA, γA) → (σB, γB)) : ℝ :=
1/2 * min { trace_dist (ℰ ρA) σB | J_free_operation ℰ }

def uX m := 1/m * (|0⟩⟨0| + (m-1)*|1⟩⟨1|)

/-- Athermality cost -/
def cost J ρ γ ε : ℝ :=
log Inf { m : ℝ | m > 0 ∧ (d J)( (|0⟩⟨0|X, uXₘ) → (ρA, γA)) ≤ ε }

def asymptotic_cost J ρ γ : ℝ :=
limε→0⁺ liminf 1/n * (cost J ρ^⊗n γ^⊗n ε)

/-- Distillable Athermality -/
def distill J ρ γ ε : ℝ :=
log Sup { m : ℝ | m > 0 ∧ (d J)((ρA, γA) → (|0⟩⟨0|X, uXₘ)) ≤ ε }

def asymptotic_distill : ℝ :=
limε→0⁺ limsup 1/n * (distill J ρ^⊗n γ^⊗n ε)

theorem athermality_cost_eq_athermality :
  asymptotic_cost J ρ γ = athermality ρ γ := sorry

theorem distillable_athermality_eq_athermality :
  asymptotic_distill J ρ γ = athermality ρ γ := sorry

/-- Athermality conversions asymptotically reversible under GPO -/
theorem reversible_athermality_conversions :
  asymptotic_distill J ρ γ = asymptotic_cost J ρ γ :=
sorry

def asymptotically_negligible_resource :
sequence of quantum states {ωn}n∈N
[coherence ωn ∈ O(log(n))]
and
Total energy grows sublinearly with n.

def sublinear_athermality_resource (a sequence {Rₙ}n:ℕ) :=
|Rₙ| grows polynomially with n
∧
∃ (0 ≤ α < 1) (c > 0), ∀ n, ∥H^(Rₙ)∥∞ ≤ c n^α

/-
"Assumption: The energy of systems {Rₙ} grows sublinearly with n.

So as n → ∞ the resourcefulness of any sequence of athermality states {(ωRₙ,γRₙ)}n:ℕ
becomes negligible compared to the resourcefulness of n copies of the golden unit (|0⟩⟨0|, u).
-/

Is this idea of a resource that grows sublinearly also used in How much entanglement is needed for quantum metrology?

/-- This negligible amount does not change the distillation rate. -/
lemma distill_rate_stays_same :
... := sorry

/-- But changes the cost rate. -/
lemma cost_rate_changes :
... := sorry

-- And so is sufficient to restore reversibility."

/--
ψ^⊗n can be written as a linear combination
of no more than (n+1)^m energy eigenvectors.
-/
lemma ... : ... := sorry

/- zero energy eigenvector
corresponds to type t = (1,0,...,0)

maximal energy eigenvector
corresponds to type t = (0,0,...,1).

The energy spread of ψ is aₘ - 0
So the energy spread of ψ^⊗n is n aₘ - 0.

The energy spread can be reduced drastically
if one allows for a small deviation from ψ^⊗n.
-/

def Gnε := { t ∈ Type(n,m) | 1/2 * ∥t - p∥₁ ≤ ε }

/-- write ψ^⊗n in two parts -/
def ψ^⊗n (ε > 0) :=
∑ t ∈ Gnε, √(r_t_n) |t⟩_Aⁿ + ∑ t ∈ Gnεᶜ, √(r_t_n) |t⟩_Aⁿ

def ψⁿε := 1/√νε * ∑ t ∈ Gnε, √(r_t_n) |t⟩_Aⁿ

lemma close_at_large_n :
  ∀ ε > 0,
    ∃ k, ∀ n ≥ k,
      trace_dist ψ^⊗n ψⁿε ≤ ε :=
sorry

lemma energy_spread_of_ψⁿε :
  energy_spread ψⁿε ≤ 4nε ∑ x, aₓ :=
sorry

/-- close to ψ^⊗n but with energy spread sublinear in n -/
lemma V1 [pure ψ] [α ∈ (1/2,1)] :
∃ a sequence of pure χₙ in n dim Hilbert space,
χₙ is equal to a linear combination of nore more than (n+1)^m energy eigenstates
∧
energy_spread χₙ ≤ 4n^α ∑ x, aₓ
∧
lim at_top trace_dist ψ^⊗n χₙ = 0 :=
begin
  let εₙ := n^(α-1).

  have : lim at_top εₙ = 0, {sorry},

  have : lim at_top n εₙ² = ∞, {sorry},

  -- Since ψεₙ can be written as a linear combination of 
  -- no more than (n + 1)^m energy eigenvectors

  have : energy_spread χₙ ≤ 4nεₙ ∑ x, aₓ, {
    sorry,
  },
  
  sorry
end

“The golden unit of a resource theory: like ebits in entanglement theory.

Athermality equals nonuniformity in the quasiclassical regime.

So we can use units of nonuniformity to measure the athermality of a given state.

Specifically we can take the golden unit to have the form (|0⟩⟨0|, u)”

Let xⁿ be a sequence with n elements xᵢ ∈ {1,...,m}.

/-- number of elements equal to z in the sequence xⁿ -/
def elements_eq (z ∈ {1,...,m}) (sequence xⁿ) := sorry

notation `N(z|xⁿ)` := elements_eq z xⁿ

/-- fraction of elements equal to z -/
def frac_elements_eq (z ∈ {1,...,m}) (sequence xⁿ) :=
1/n * N(z|xⁿ)

/-- A prob vector in Rᵐ₊ -/
def type (sequence xⁿ) :=
(frac_elements_eq 1 xⁿ, ..., frac_elements_eq m xⁿ)^T

/-- prob that the i.i.d source outputs sequence xⁿ -/
lemma prob_iid_sequence : 
  prob xⁿ = 2^(-n*(H(type xⁿ) + D(type xⁿ||p))) := sorry

def Type(n,m) := the set of all types of xⁿ ∈ {1,...,m}ⁿ

lemma number_of_elements_le :
  |Type(n, m)| ≤ (n + 1)^m :=
sorry

def xⁿ(t) := The set of sequences xⁿ of type t

/-- combinatorial formula
of arranging nt1, ..., ntm objects in a sequence: ..." -/
lemma number_of_sequences_eq : 
  xⁿ(t) = ... :=
sorry

-- bounded by the stirling approximation

References

• Gour2022;