Defines OptimalHypothesisRate, the optimal rate of distinguishing an MState ρ from a set of other mixed states S, with at most Type I error ε.

That is to say: take a projective measurement (a POVM) with elements {T, 1-T}, where measuring T will mean we conclude our unknown state was ρ, and measuring 1-T will mean we think the state was something in S. We only accept T's such that Tr[(1-T)ρ] ≤ ε, that is, we have at most an ε probability of incorrectly concluding it was ρ. The Type II error associated to this T is then max_{σ ∈ S} Tr[T σ], that is, the (worst possible, over possible states) chance of incorrectly concluding our state was in S. Optimize over T to get the lowest possible Type II error rate, and the resulting error rate is OptimalHypothesisRate ρ ε S.

We make this accessible through the notation β_ ε(ρ‖S).

See The tangled state of quantum hypothesis testing by Mario Berta et al. for a broader overview.

noncomputable def OptimalHypothesisRate {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (ε : Prob) (S : Set (MState d)) : Prob

The optimal hypothesis testing rate, for a tolerance ε: given a state ρ and a set of states S, the optimum distinguishing rate that allows a probability ε of errors.

Equations

• OptimalHypothesisRate ρ ε S = ⨅ (T : { m : HermitianMat d ℂ // ρ.exp_val (1 - m) ≤ ↑ε ∧ 0 ≤ m ∧ m ≤ 1 }), ⨆ σ ∈ S, ⟨σ.exp_val ↑T, ⋯⟩

def OptimalHypothesisRate.«termβ__(_‖_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

instance OptimalHypothesisRate.iInf_Inhabited {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (ε : Prob) : Inhabited { m : HermitianMat d ℂ // ρ.exp_val (1 - m) ≤ ↑ε ∧ 0 ≤ m ∧ m ≤ 1 }

The space of strategies T in OptimalHypothesisRate is inhabited, we always have some valid strategy.

Equations

• OptimalHypothesisRate.iInf_Inhabited ρ ε = { default := ⟨1, ⋯⟩ }

instance OptimalHypothesisRate.instInhabitedElemHermitianMatComplexSetOfAndLeRealExp_valHSubOfNatVal {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (ε : Prob) : Inhabited ↑{m : HermitianMat d ℂ | ρ.exp_val (1 - m) ≤ ↑ε ∧ 0 ≤ m ∧ m ≤ 1}

Equations

• OptimalHypothesisRate.instInhabitedElemHermitianMatComplexSetOfAndLeRealExp_valHSubOfNatVal ρ ε = OptimalHypothesisRate.iInf_Inhabited ρ ε

theorem OptimalHypothesisRate.iInf_IsCompact {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (ε : Prob) : IsCompact {m : HermitianMat d ℂ | ρ.exp_val (1 - m) ≤ ↑ε ∧ 0 ≤ m ∧ m ≤ 1}

The space of strategies T in OptimalHypothesisRate is compact.

theorem OptimalHypothesisRate.iInf_IsConvex {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (ε : Prob) : Convex ℝ {m : HermitianMat d ℂ | ρ.exp_val (1 - m) ≤ ↑ε ∧ 0 ≤ m ∧ m ≤ 1}

The space of strategies T in OptimalHypothesisRate is convex.

@[simp]

theorem OptimalHypothesisRate.of_empty {d : Type u_1} [Fintype d] [DecidableEq d] {ρ : MState d} (ε : Prob) : OptimalHypothesisRate ρ ε ∅ = 0

When S is empty, the optimal hypothesis testing rate is zero.

theorem OptimalHypothesisRate.le_sup_exp_val {d : Type u_1} [Fintype d] [DecidableEq d] {ρ : MState d} (ε : Prob) {S : Set (MState d)} (m : HermitianMat d ℂ) (hExp : ρ.exp_val (1 - m) ≤ ↑ε) (hm : 0 ≤ m ∧ m ≤ 1) : OptimalHypothesisRate ρ ε S ≤ ⨆ σ ∈ S, ⟨σ.exp_val m, ⋯⟩

theorem OptimalHypothesisRate.le_of_subset {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (ε : Prob) {S1 S2 : Set (MState d)} (h : S1 ⊆ S2) : OptimalHypothesisRate ρ ε S1 ≤ OptimalHypothesisRate ρ ε S2

theorem OptimalHypothesisRate.of_singleton {d : Type u_1} [Fintype d] [DecidableEq d] {ρ σ : MState d} {ε : Prob} : OptimalHypothesisRate ρ ε {σ} = ⨅ (T : { m : HermitianMat d ℂ // ρ.exp_val (1 - m) ≤ ↑ε ∧ 0 ≤ m ∧ m ≤ 1 }), ⟨σ.exp_val ↑T, ⋯⟩

theorem OptimalHypothesisRate.negLog_le_singleton {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (ε : Prob) (S : Set (MState d)) (σ : MState d) (h : σ ∈ S) : (OptimalHypothesisRate ρ ε S).negLog ≤ (OptimalHypothesisRate ρ ε {σ}).negLog

theorem OptimalHypothesisRate.singleton_le_exp_val {d : Type u_1} [Fintype d] [DecidableEq d] {ρ σ : MState d} {ε : Prob} (m : HermitianMat d ℂ) (hExp : ρ.exp_val (1 - m) ≤ ↑ε) (hm : 0 ≤ m ∧ m ≤ 1) : OptimalHypothesisRate ρ ε {σ} ≤ ⟨σ.exp_val m, ⋯⟩

theorem OptimalHypothesisRate.exists_min' {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (ε : Prob) (S : Set (MState d)) : ∃ (T : { m : HermitianMat d ℂ // ρ.exp_val (1 - m) ≤ ↑ε ∧ 0 ≤ m ∧ m ≤ 1 }), ⨆ σ ∈ S, ⟨σ.exp_val ↑T, ⋯⟩ = OptimalHypothesisRate ρ ε S ∧ 1 - ↑ε ≤ ρ.exp_val ↑T

There exists an optimal T for the hypothesis testing, that is, it's a minimum and not just an infimum. This states we have 1 - ε ≤ ρ.exp_val T, but we can always "worsen" T to make that bound tight, which is exists_min.

theorem OptimalHypothesisRate.exists_min {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (ε : Prob) (S : Set (MState d)) : ∃ (T : { m : HermitianMat d ℂ // ρ.exp_val (1 - m) ≤ ↑ε ∧ 0 ≤ m ∧ m ≤ 1 }), ⨆ σ ∈ S, ⟨σ.exp_val ↑T, ⋯⟩ = OptimalHypothesisRate ρ ε S ∧ ρ.exp_val ↑T = 1 - ↑ε

There exists an optimal T for the hypothesis testing, that is, it's a minimum and not just an infimum. This tightens the T from exists_min' to a ⟪ρ,T⟫ = 1 - ε bound.

theorem OptimalHypothesisRate.pos_of_lt_one {d : Type u_1} [Fintype d] [DecidableEq d] {ρ : MState d} (S : Set (MState d)) (hρ : ∃ σ ∈ S, (↑σ).ker ≤ (↑ρ).ker) {ε : Prob} (hε : ε < 1) : 0 < OptimalHypothesisRate ρ ε S

When the allowed Type I error ε is less than 1 (so, we have some limit on our errors), and the kernel of the state ρ contains the kernel of some element in S, then the optimal hypothesis rate is positive - there is some lower bound on the type II errors we'll see. In other words, under these conditions, we cannot completely avoid type II errors.

theorem OptimalHypothesisRate.Lemma3 {d : Type u_1} [Fintype d] [DecidableEq d] {ρ : MState d} (ε : Prob) {S : Set (MState d)} (hS₁ : IsCompact S) (hS₂ : Convex ℝ (MState.M '' S)) : ⨆ σ ∈ S, OptimalHypothesisRate ρ ε {σ} = OptimalHypothesisRate ρ ε S

theorem OptimalHypothesisRate.ker_diagonal_prob_eq_bot {q : Prob} (hq₁ : 0 < q) (hq₂ : q < 1) : (HermitianMat.diagonal fun (x : Fin 2) => ↑((Distribution.coin q) x)).ker = ⊥

theorem OptimalHypothesisRate.optimalHypothesisRate_antitone {d : Type u_1} [Fintype d] [DecidableEq d] {d₂ : Type u_2} [Fintype d₂] [DecidableEq d₂] (ρ σ : MState d) (ℰ : CPTPMap d d₂ ℂ) (ε : Prob) : OptimalHypothesisRate ρ ε {σ} ≤ OptimalHypothesisRate (ℰ ρ) ε {ℰ σ}

Lemma S1

theorem OptimalHypothesisRate.Ref81Lem5 {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) (ε : Prob) (hε : ε < 1) (α : ℝ) (hα : 1 < α) : (OptimalHypothesisRate ρ ε {σ}).negLog ≤ D̃_α(ρ‖σ) + (1 - ε).negLog * ↑⟨α, ⋯⟩ / ↑⟨α - 1, ⋯⟩

This is from Strong converse exponents for a quantum channel discrimination problem and quantum-feedback-assisted communication, Lemma 5.

It seems like this is actually true for all 0 < α (with appropriate modifications at α = 1), but we only need it for the case of 1 < α.

theorem OptimalHypothesisRate.rate_pos_of_smul_pos {ε : Prob} {d : Type u_2} [Fintype d] [DecidableEq d] {ρ σ₁ σ₂ : MState d} (hσ₂ : 0 < OptimalHypothesisRate ρ ε {σ₂}) {c : ℝ} (hc : 0 < c) (hσ : c • ↑σ₂ ≤ ↑σ₁) : 0 < OptimalHypothesisRate ρ ε {σ₁}

theorem OptimalHypothesisRate.rate_Continuous_singleton {ε : Prob} {d : Type u_2} [Fintype d] [DecidableEq d] (ρ : MState d) : Continuous fun (σ : MState d) => OptimalHypothesisRate ρ ε {σ}