Diamond distance between quantum channels

import Quantum_state
import Quantum_channel
import Choi_correspondence
import Trace_distance

/-- are the channel outputs close for all inputs? -/
def diamond_dist [quantum_channel 𝒩 β„³] : ℝ :=
Sup { Sup { βˆ₯1β‚™βŠ—π’© ρ - 1β‚™βŠ—β„³ ρβˆ₯₁ | quantum_state ρ } | n : β„• }

notation `βˆ₯𝒩 - β„³βˆ₯β‹„` := diamond_dist 𝒩 β„³

ρ is state over main system A and reference system of dim n.

/--
"The normalized diamond distance can be computed efficiently
by means of the following semi-definite program."
-/
theorem diamond_dist_sdp [quantum_channel 𝒩 β„³] : 
1/2 * βˆ₯𝒩 - β„³βˆ₯β‹„ = Inf { pTr_B βˆ₯ZRBβˆ₯∞ | ZRB β‰₯ 0 ∧ ZRB β‰₯ Choi 𝒩 - Choi β„³ } :=
sorry

β€œPrepare a state ρRC of a reference system R and the channel input system C. Feed system C into the unknown channel. Perform a POVM measurement {Ξ›RD i} on the channel output and R.”

import POVM

/--
"The maximum possible error between 𝒩Cβ†’D and β„³Cβ†’D;
Optimizing with respect to all preparations and measurements,
is equal to the normalized diamond distance:"
-/
theorem sup_prob_diff_eq_diamond_dist :
Sup { ∣Tr((Ξ› x) 1βŠ—π’©(ρRC)) - Tr((Ξ› x) 1βŠ—β„³(ρRC))∣ | quantum_state ρRC ∧ POVM Ξ› } = 1/2 * βˆ₯𝒩 - β„³βˆ₯β‹„ :=
sorry

Is diamond_dist suitable as a metric of a metric space?

theorem diamond_dist_self :
βˆ€ [quantum_channel 𝒩], βˆ₯𝒩 - 𝒩βˆ₯β‹„ = 0 := sorry

theorem diamond_dist_comm :
βˆ€ [quantum_channel 𝒩 β„³], βˆ₯𝒩 - β„³βˆ₯β‹„ = βˆ₯β„³ - 𝒩βˆ₯β‹„ := sorry

theorem diamond_dist_triangle_inequality :
βˆ₯𝒩 - β„³βˆ₯β‹„ ≀ βˆ₯𝒩 - Ξ›βˆ₯β‹„ + βˆ₯Ξ› - β„³βˆ₯β‹„ :=
begin
    -- can this be proven?
    -- rw diamond_dist,
end

References