Channel coherent information

import Quantum_channel
import State_coherent_information

/-- "The coherent information of a quantum channel -/
def coh_info_of_channel [quantum_channel 𝒩A'] : ℝ :=
max {coh_info_of_state I⨂𝒩A' ψAA' | pure ψAA'}

References: