noncomputable def SteinsLemma.OptimalHypothesisRate {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) (ε : ℝ) (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

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

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

Equations

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

noncomputable def Prob.negLog : Prob → ENNReal

Map a probability [0,1] to [0,+∞] with -log p. Special case that 0 maps to +∞ (not 0, as Real.log does). This makes it Antitone.

TODO: Pull out into another file? Maybe?

Equations

• p.negLog = if p = 0 then ⊤ else some ⟨-Real.log ↑p, ⋯⟩

theorem Prob.negLog_Antitone : Antitone negLog

def SteinsLemma.«term—log» : Lean.ParserDescr

Equations

• SteinsLemma.«term—log» = Lean.ParserDescr.node `SteinsLemma.«term—log» 1024 (Lean.ParserDescr.symbol "—log ")

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

theorem SteinsLemma.limit_rel_entropy_exists {ι : Type u_1} [FreeStateTheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) : ∃ (d : NNReal), Filter.Tendsto (fun (n : ℕ+) => (↑↑n)⁻¹ * ⨅ σ ∈ FreeStateTheory.IsFree, 𝐃(ResourcePretheory.statePow ρ n‖σ)) Filter.atTop (nhds ↑d)

Lemma 5

theorem SteinsLemma.limit_hypotesting_eq_limit_rel_entropy {ι : Type u_1} [FreeStateTheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) (ε : ℝ) (hε : 0 < ε ∧ ε < 1) : ∃ (d : NNReal), Filter.Tendsto (fun (n : ℕ+) => (OptimalHypothesisRate (ResourcePretheory.statePow ρ n) ε FreeStateTheory.IsFree).negLog / ↑↑n) Filter.atTop (nhds ↑d) ∧ Filter.Tendsto (fun (n : ℕ+) => (↑↑n)⁻¹ * ⨅ σ ∈ FreeStateTheory.IsFree, 𝐃(ResourcePretheory.statePow ρ n‖σ)) Filter.atTop (nhds ↑d)

Theorem 4, which is also called the Generalized Quantum Stein's Lemma in Hayashi & Yamasaki

theorem SteinsLemma.GeneralizedQSteinsLemma {ι : Type u_1} [FreeStateTheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) (ε : ℝ) (hε : 0 < ε ∧ ε < 1) : Filter.Tendsto (fun (n : ℕ+) => (OptimalHypothesisRate (ResourcePretheory.statePow ρ n) ε FreeStateTheory.IsFree).negLog / ↑↑n) Filter.atTop (nhds ↑(RegularizedRelativeEntResource ρ))