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.extracted_limsup_inequality (z : ENNReal) (hz : z ≠ ⊤) (y x : ℕ → ENNReal) (h_lem5 : ∀ (n : ℕ), x n ≤ y n + z) : Filter.limsup (fun (n : ℕ) => x n / ↑n) Filter.atTop ≤ Filter.limsup (fun (n : ℕ) => y n / ↑n) Filter.atTop

theorem Filter.tendsto_sub_atTop_iff_nat {α : Type u_2} {f : ℕ → α} {l : Filter α} (k : ℕ) : Tendsto (fun (n : ℕ) => f (n - k)) atTop l ↔ Tendsto f atTop l

Like Filter.tendsto_add_atTop_iff_nat, but with nat subtraction.

theorem ENNReal.tendsto_sub_const_nhds_zero_iff {α : Type u_2} {l : Filter α} {f : α → ENNReal} {a : ENNReal} : Filter.Tendsto (fun (x : α) => f x - a) l (nhds 0) ↔ Filter.limsup f l ≤ a

Sort of dual to ENNReal.tendsto_const_sub_nhds_zero_iff. Takes a substantially different form though, since we don't actually have equality of the limits, or even the fact that the other one converges, which is why we need to use limsup.

theorem SteinsLemma.optimalHypothesisRate_unique {d : Type u_2} [Fintype d] [DecidableEq d] (ε : Prob) (ρ σ : MState d) [Unique d] : OptimalHypothesisRate ρ ε {σ} = 1 - ε

theorem SteinsLemma.LemmaS2liminf {ε3 : Prob} {ε4 : NNReal} (hε4 : 0 < ε4) {d : ℕ → Type u_5} [(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 : ℕ) => ((Real.exp (↑n * (↑Rinf + ↑ε4)) • ↑(σ n)).proj_le ↑(ρ n)).inner ↑(ρ n)) Filter.atTop ≤ 1 - ↑ε3

theorem SteinsLemma.LemmaS2limsup {ε3 : Prob} {ε4 : NNReal} (hε4 : 0 < ε4) {d : ℕ → Type u_5} [(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 : ℕ) => ((Real.exp (↑n * (↑Rsup + ↑ε4)) • ↑(σ n)).proj_le ↑(ρ n)).inner ↑(ρ n)) Filter.atTop ≤ 1 - ↑ε3

instance SteinsLemma.instPosSMulReflectLERealHermitianMatOfDecidableEq {d : Type u_5} {𝕜 : Type u_6} [Fintype d] [DecidableEq d] [RCLike 𝕜] : PosSMulReflectLE ℝ (HermitianMat d 𝕜)

theorem Matrix.PosDef.zero_lt {n : Type u_5} [Nonempty n] [Fintype n] {A : Matrix n n ℂ} (hA : A.PosDef) : 0 < A

theorem HermitianMat.cfc_le_cfc_of_PosDef {d : Type u_5} [Fintype d] [DecidableEq d] {f g : ℝ → ℝ} (hfg : ∀ (i : ℝ), 0 < i → f i ≤ g i) (A : HermitianMat d ℂ) (hA : (↑A).PosDef) : A.cfc f ≤ A.cfc g

theorem HermitianMat.cfc_commute {d : Type u_5} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (f g : ℝ → ℝ) : Commute ↑(A.cfc f) ↑(A.cfc g)

theorem Commute.exists_HermitianMat_cfc {d : Type u_5} [Fintype d] [DecidableEq d] (A B : HermitianMat d ℂ) (hAB : Commute ↑A ↑B) : ∃ (C : HermitianMat d ℂ), (∃ (f : ℝ → ℝ), A = C.cfc f) ∧ ∃ (g : ℝ → ℝ), B = C.cfc g

theorem HermitianMat.proj_lt_mul_nonneg {d : Type u_5} [Fintype d] [DecidableEq d] (A B : HermitianMat d ℂ) : 0 ≤ ↑(A.proj_lt B) * ↑(B - A)

theorem HermitianMat.proj_lt_mul_lt {d : Type u_5} [Fintype d] [DecidableEq d] (A B : HermitianMat d ℂ) : ↑(A.proj_lt B) * ↑A ≤ ↑(A.proj_lt B) * ↑B

theorem HermitianMat.one_sub_proj_le {d : Type u_5} [Fintype d] [DecidableEq d] (A B : HermitianMat d ℂ) : 1 - B.proj_le A = A.proj_lt B

@[reducible, inline]

noncomputable abbrev SteinsLemma.HermitianMat.mul_commute {d : Type u_5} [Fintype d] {A B : HermitianMat d ℂ} (hAB : Commute ↑A ↑B) : HermitianMat d ℂ

Equations

• SteinsLemma.HermitianMat.mul_commute hAB = ⟨↑A * ↑B, ⋯⟩

theorem Matrix.card_spectrum_eq_image {d : Type u_5} [Fintype d] [DecidableEq d] (A : Matrix d d ℂ) (hA : A.IsHermitian) [Fintype ↑(spectrum ℝ A)] : Fintype.card ↑(spectrum ℝ A) = (Finset.image hA.eigenvalues Finset.univ).card

theorem SteinsLemma.exists_liminf_zero_of_forall_liminf_le (y : NNReal) (f : NNReal → ℕ → ENNReal) (hf : ∀ x > 0, Filter.liminf (f x) Filter.atTop ≤ ↑y) : ∃ (g : ℕ → NNReal), (∀ (x : ℕ), g x > 0) ∧ Filter.Tendsto g Filter.atTop (nhds 0) ∧ Filter.liminf (fun (n : ℕ) => f (g n) n) Filter.atTop ≤ ↑y

theorem SteinsLemma.exists_liminf_zero_of_forall_liminf_le_with_UB (y : NNReal) (f : NNReal → ℕ → ENNReal) {z : NNReal} (hz : 0 < z) (hf : ∀ x > 0, Filter.liminf (f x) Filter.atTop ≤ ↑y) : ∃ (g : ℕ → NNReal), (∀ (x : ℕ), g x > 0) ∧ (∀ (x : ℕ), g x < z) ∧ Filter.Tendsto g Filter.atTop (nhds 0) ∧ Filter.liminf (fun (n : ℕ) => f (g n) n) Filter.atTop ≤ ↑y

theorem SteinsLemma.exists_limsup_zero_of_forall_limsup_le (y : NNReal) (f : NNReal → ℕ → ENNReal) (hf : ∀ x > 0, Filter.limsup (f x) Filter.atTop ≤ ↑y) : ∃ (g : ℕ → NNReal), (∀ (x : ℕ), g x > 0) ∧ Filter.Tendsto g Filter.atTop (nhds 0) ∧ Filter.limsup (fun (n : ℕ) => f (g n) n) Filter.atTop ≤ ↑y

theorem SteinsLemma.exists_liminf_zero_of_forall_liminf_limsup_le_with_UB (y₁ y₂ : NNReal) (f₁ f₂ : NNReal → ℕ → ENNReal) {z : NNReal} (hz : 0 < z) (hf₁ : ∀ x > 0, Filter.liminf (f₁ x) Filter.atTop ≤ ↑y₁) (hf₂ : ∀ x > 0, Filter.limsup (f₂ x) Filter.atTop ≤ ↑y₂) : ∃ (g : ℕ → NNReal), (∀ (x : ℕ), g x > 0) ∧ (∀ (x : ℕ), g x < z) ∧ Filter.Tendsto g Filter.atTop (nhds 0) ∧ Filter.liminf (fun (n : ℕ) => f₁ (g n) n) Filter.atTop ≤ ↑y₁ ∧ Filter.limsup (fun (n : ℕ) => f₂ (g n) n) Filter.atTop ≤ ↑y₂

theorem SteinsLemma.sub_iInf_eignevalues {d : Type u_5} [Fintype d] [DecidableEq d] {A : Matrix d d ℂ} (hA : A.IsHermitian) : (A - iInf hA.eigenvalues • 1).PosSemidef

theorem SteinsLemma.iInf_eigenvalues_le_dotProduct_mulVec {d : Type u_5} [Fintype d] [DecidableEq d] {A : Matrix d d ℂ} (hA : A.IsHermitian) (v : d → ℂ) : ↑(iInf hA.eigenvalues) * star v ⬝ᵥ v ≤ star v ⬝ᵥ A.mulVec v

theorem SteinsLemma.iInf_eigenvalues_le_of_posSemidef {d : Type u_5} [Fintype d] [DecidableEq d] {A B : Matrix d d ℂ} (hAB : (B - A).PosSemidef) (hA : A.IsHermitian) (hB : B.IsHermitian) : iInf hA.eigenvalues ≤ iInf hB.eigenvalues

theorem SteinsLemma.iInf_eigenvalues_le {d : Type u_5} [Fintype d] [DecidableEq d] {A B : Matrix d d ℂ} (hAB : A ≤ B) (hA : A.IsHermitian) (hB : B.IsHermitian) : iInf hA.eigenvalues ≤ iInf hB.eigenvalues

@[simp]

theorem MState.spectrum_relabel {d : Type u_5} {d₂ : Type u_6} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] {ρ : MState d} (e : d₂ ≃ d) : _root_.spectrum ℝ (ρ.relabel e).m = _root_.spectrum ℝ ρ.m

theorem SteinsLemma.HermitianMat.spectrum_prod {d : Type u_5} {d₂ : Type u_6} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] {A : HermitianMat d ℂ} {B : HermitianMat d₂ ℂ} : spectrum ℝ ↑(A.kronecker B) = spectrum ℝ ↑A * spectrum ℝ ↑B

theorem SteinsLemma.csInf_mul_nonneg {s t : Set ℝ} (hs₀ : s.Nonempty) (hs₁ : ∀ x ∈ s, 0 ≤ x) (ht₀ : t.Nonempty) (ht₁ : ∀ x ∈ t, 0 ≤ x) : sInf (s * t) = sInf s * sInf t

theorem SteinsLemma.sInf_spectrum_prod {d : Type u_5} {d₂ : Type u_6} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] {ρ : MState d} {σ : MState d₂} : sInf (spectrum ℝ (ρ ⊗ σ).m) = sInf (spectrum ℝ ρ.m) * sInf (spectrum ℝ σ.m)

theorem SteinsLemma.sInf_spectrum_rprod {ι : Type u_1} [UnitalFreeStateTheory ι] {i j : ι} {ρ : MState (ResourcePretheory.H i)} {σ : MState (ResourcePretheory.H j)} : sInf (spectrum ℝ (ResourcePretheory.prodRelabel ρ σ).m) = sInf (spectrum ℝ ρ.m) * sInf (spectrum ℝ σ.m)

theorem SteinsLemma.sInf_spectrum_spacePow {ι : Type u_1} [UnitalFreeStateTheory ι] {i : ι} (σ : MState (ResourcePretheory.H i)) (n : ℕ) : sInf (spectrum ℝ (UnitalPretheory.statePow σ n).m) = sInf (spectrum ℝ σ.m) ^ n

theorem SteinsLemma.iInf_eigenvalues_smul_one_le {d : Type u_5} [Fintype d] [DecidableEq d] {A : Matrix d d ℂ} (hA : A.IsHermitian) : iInf hA.eigenvalues • 1 ≤ A

theorem ENNReal.bdd_le_mul_tendsto_zero {α : Type u_2} {l : Filter α} {f g : α → ENNReal} {b : ENNReal} (hb : b ≠ ⊤) (hf : Filter.Tendsto f l (nhds 0)) (hg : ∀ᶠ (x : α) in l, g x ≤ b) : Filter.Tendsto (fun (x : α) => f x * g x) l (nhds 0)

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.