Thermal operation

Athermality;

Coherence in Athermality;

import Time_translation_covariant
import Quantum_channel
import Thermal_state

variables [quantum_state ρ]

/-- unitary on system and thermal environment -/
def thermal_op [quantum_channel 𝒩]  :=
∃ n, ∃ U, 𝒩 ρ = Tr_B [U ρ ⊗ (thermal_state n) U†]

variables [thermal_op T]

/-- Thermal operations preserve the thermal state -/
theorem preserves_thermal_state_of_thermal_op :
T thermal_state = thermal_state := sorry

theorem thermal_ops_time_trans_cov :
time_trans_cov T := sorry

import Markovian

/--
A thermal_op T = E(t,0) is said to be time-independent Markovian (or embeddable) 
if ∃ Lindblad generator L, ∀s, thermal_op E(s,0) = exp (Ls).
-/
def time_indep_Markovian [thermal_op T] :=
∃ Lindblad_generator L,
∀s, thermal_op e^(L s)

notation ETOn := The set of embeddable thermal operations on n-dimensional systems.

/-- ∃ continuous family of Lindblad generators {L(s) | 0 ≤ s ≤ t} 
s.t. ∀ s > r ∈ [0, t] the time-ordered exponential E(s,r) = T exp (∫ s r L(τ) dτ)
defines a thermal operation and T = E(t,0) -/
def Markovian [thermal_op T] :=
sorry

notation MTOn := The set of Markovian thermal operations on n-dimensional systems.

The previous two definitions capture the difference between maps that can be generated by time-independent Lindblad generators, and the more general CP-divisible maps.

References

• Spaventa2021;