noncomputable def SteinsLemma.Lemma6_σn {ι : Type u_1} [UnitalFreeStateTheory ι] {i : ι} (m : ℕ) (σf : MState (ResourcePretheory.H i)) (σₘ : MState (ResourcePretheory.H (i ^ m))) (n : ℕ) : MState (ResourcePretheory.H (i ^ n))

The \tilde{σ}_n defined in Lemma 6, also in equation (S40) in Lemma 7.

Equations

• SteinsLemma.Lemma6_σn m σf σₘ n = (ResourcePretheory.prodRelabel (UnitalPretheory.statePow σₘ (n / m)) (UnitalPretheory.statePow σf (n % m))).relabel (Equiv.cast ⋯)

theorem SteinsLemma.Lemma6_σn_IsFree {ι : Type u_1} [UnitalFreeStateTheory ι] {i : ι} {σ₁ : MState (ResourcePretheory.H i)} {σₘ : (m : ℕ) → MState (ResourcePretheory.H (i ^ m))} (hσ₁_free : FreeStateTheory.IsFree σ₁) (hσₘ : ∀ (m : ℕ), σₘ m ∈ FreeStateTheory.IsFree) (m n : ℕ) : Lemma6_σn m σ₁ (σₘ m) n ∈ FreeStateTheory.IsFree

theorem SteinsLemma.LemmaS2liminf {ε3 : Prob} {ε4 : NNReal} (hε4 : 0 < ε4) {d : ℕ → Type u_2} [(n : ℕ) → Fintype (d n)] [(n : ℕ) → DecidableEq (d n)] (ρ σ : (n : ℕ) → MState (d n)) {Rinf : NNReal} (hRinf : ↑Rinf ≥ Filter.liminf (fun (n : ℕ) => (OptimalHypothesisRate (ρ n) ε3 {σ n}).negLog / ↑n) Filter.atTop) : Filter.liminf (fun (n : ℕ) => inner ℝ ((Real.exp (↑n * (↑Rinf + ↑ε4)) • ↑(σ n)).projLE ↑(ρ n)) ↑(ρ n)) Filter.atTop ≤ 1 - ↑ε3

theorem SteinsLemma.LemmaS2limsup {ε3 : Prob} {ε4 : NNReal} (hε4 : 0 < ε4) {d : ℕ → Type u_2} [(n : ℕ) → Fintype (d n)] [(n : ℕ) → DecidableEq (d n)] (ρ σ : (n : ℕ) → MState (d n)) {Rsup : NNReal} (hRsup : ↑Rsup ≥ Filter.limsup (fun (n : ℕ) => (OptimalHypothesisRate (ρ n) ε3 {σ n}).negLog / ↑n) Filter.atTop) : Filter.limsup (fun (n : ℕ) => inner ℝ ((Real.exp (↑n * (↑Rsup + ↑ε4)) • ↑(σ n)).projLE ↑(ρ n)) ↑(ρ n)) Filter.atTop ≤ 1 - ↑ε3

theorem SteinsLemma.σ₁_c_littleO {ι : Type u_1} [UnitalFreeStateTheory ι] (i : ι) : (fun (n : ℕ) => SteinsLemma.σ₁_c✝ i n + Real.log 3) =o[Filter.atTop] fun (x : ℕ) => ↑x

theorem SteinsLemma.Lemma7_gap {ι : Type u_1} [UnitalFreeStateTheory ι] {i : ι} (ρ : MState (ResourcePretheory.H i)) {ε : Prob} (hε : 0 < ε ∧ ε < 1) {ε' : Prob} (hε' : 0 < ε' ∧ ε' < ε) (σ : (n : ℕ) → ↑FreeStateTheory.IsFree) : SteinsLemma.R2✝ ρ (SteinsLemma.Lemma7_improver✝ ρ hε hε' σ) - SteinsLemma.R1✝ ρ ε ≤ ↑↑(1 - ε') * (SteinsLemma.R2✝¹ ρ σ - SteinsLemma.R1✝¹ ρ ε)

The Lemma7_improver does its job at shrinking the gap.

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

Theorem 1 in https://arxiv.org/pdf/2408.02722v3

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

Theorem 4, which is also called the Generalized quantum Stein's lemma in Hayashi & Yamasaki. What they state as an equality of limits, which don't exist per se in Mathlib, we state as the existence of a number (which happens to be RegularizedRelativeEntResource) to which both sides converge.