Time-translation covariant

import Twirl

/-- commutes with free evolution -/
def time_trans_cov [quantum_channel 𝒩] :
∀ (t : ℝ) [quantum_state ρ],
𝒩(e^(-i HA t) * ρ * e^(i HA t)) = e^(-i HB t) * 𝒩(ρ) * e^(i HB t)

lemma twirl_commutes_with_time_trans_cov :
  time_trans_cov ℰ ↔ twirl ∘ ℰ = ℰ ∘ twirl :=
sorry

References

• Gour2022;