To do relative entropies, we start with the sandwiched Renyi Relative Entropy which is a nice general form. Then instead of proving many theorems (like DPI, relabelling, additivity, etc.) several times, we just prove it for this one quantity, then it follows for other quantities (like the relative entropy) as a special case.

theorem weighted_jensen_rpow {d : Type u_1} [Fintype d] (b w : d → ℝ) (q : ℝ) (hb : ∀ (j : d), 0 ≤ b j) (hw : ∀ (j : d), 0 ≤ w j) (hsum : ∑ j : d, w j = 1) (hq : 1 ≤ q) : (∑ j : d, w j * b j) ^ q ≤ ∑ j : d, w j * b j ^ q

Weighted Jensen inequality: for weights w_j ≥ 0 with ∑ w_j = 1, values b_j ≥ 0, and q ≥ 1: (∑_j w_j * b_j)^q ≤ ∑_j w_j * b_j^q.

This is the special case of Real.rpow_arith_mean_le_arith_mean_rpow applied to Finset.univ

theorem doubly_stochastic_holder {d : Type u_1} [Fintype d] (a b : d → ℝ) (w : d → d → ℝ) (ha : ∀ (i : d), 0 ≤ a i) (hb : ∀ (j : d), 0 ≤ b j) (hw : ∀ (i j : d), 0 ≤ w i j) (hrow : ∀ (i : d), ∑ j : d, w i j = 1) (hcol : ∀ (j : d), ∑ i : d, w i j = 1) (p q : ℝ) (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) : ∑ i : d, ∑ j : d, a i * b j * w i j ≤ (∑ i : d, a i ^ p) ^ (1 / p) * (∑ j : d, b j ^ q) ^ (1 / q)

Doubly stochastic Hölder inequality: for nonneg a, b, doubly stochastic w, and conjugate p, q > 1: ∑{ij} a_i * b_j * w{ij} ≤ (∑ a_i^p)^{1/p} * (∑ b_j^q)^{1/q}.

theorem HermitianMat.inner_le_trace_rpow_mul {d : Type u_1} [Fintype d] [DecidableEq d] {A B : HermitianMat d ℂ} (hA : 0 ≤ A) (hB : 0 ≤ B) (p q : ℝ) (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) : inner ℝ A B ≤ (A ^ p).trace ^ (1 / p) * (B ^ q).trace ^ (1 / q)

Hermitian trace Hölder inequality: for PSD A, B and conjugate exponents p, q > 1, ⟪A, B⟫ ≤ Tr[A^p]^(1/p) * Tr[B^q]^(1/q).

theorem MState.rpow_le_one' {d : Type u_1} [Fintype d] [DecidableEq d] {σ : MState d} {r : ℝ} (hσ : 0 < r) : ↑σ ^ r ≤ 1

theorem HermitianMat.eigenvalues_le_one_of_le_one {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (hA1 : A ≤ 1) (i : d) : ⋯.eigenvalues i ≤ 1

If A ≥ 0 and A ≤ 1, then each eigenvalue of A is in [0, 1].

theorem HermitianMat.trace_rpow_le_trace_of_le_one {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (hA : 0 ≤ A) (hA1 : A ≤ 1) (p : ℝ) (hp : 1 ≤ p) : (A ^ p).trace ≤ A.trace

For positive A ≤ 1 and p ≥ 1, Tr[A^p] ≤ Tr[A].

theorem HermitianMat.rpow_neg_mul_rpow_eq_supportProj {d : Type u_1} [Fintype d] [DecidableEq d] {A : HermitianMat d ℂ} (hA : 0 ≤ A) {p : ℝ} (hp : p ≠ 0) : ↑(A ^ (-p)) * ↑(A ^ p) = ↑A.supportProj

For PSD A and p ≠ 0, A^{-p} * A^p = HermitianMat.supportProj A.

theorem HermitianMat.supportProj_mul_self {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) : ↑A.supportProj * ↑A = ↑A

theorem HermitianMat.inner_supportProj_self {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) : inner ℝ A A.supportProj = A.trace

theorem HermitianMat.mul_supportProj_of_ker_le {d : Type u_1} [Fintype d] [DecidableEq d] {A B : HermitianMat d ℂ} (h : (↑B.lin).ker ≤ (↑A.lin).ker) : ↑A * ↑B.supportProj = ↑A

theorem HermitianMat.inner_supportProj_of_ker_le {d : Type u_1} [Fintype d] [DecidableEq d] {A B : HermitianMat d ℂ} (h : (↑B.lin).ker ≤ (↑A.lin).ker) : inner ℝ A B.supportProj = A.trace

theorem supportProj_inner_density {d : Type u_1} [Fintype d] [DecidableEq d] {ρ σ : MState d} (h : (↑σ).ker ≤ (↑ρ).ker) : inner ℝ (↑σ).supportProj ↑ρ = 1

theorem inner_log_sub_log_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] {ρ σ : MState d} (h : (↑σ).ker ≤ (↑ρ).ker) : 0 ≤ inner ℝ (↑ρ) ((↑ρ).log - (↑σ).log)

theorem sandwichedRelRentropy_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] {ρ σ : MState d} {α : ℝ} (hα : 0 < α) (h : (↑σ).ker ≤ (↑ρ).ker) : 0 ≤ if α = 1 then inner ℝ (↑ρ) ((↑ρ).log - (↑σ).log) else Real.log ((HermitianMat.conj ↑(↑σ ^ ((1 - α) / (2 * α)))) ↑ρ ^ α).trace / (α - 1)

theorem ker_kron_le_of_le {d₁ : Type u_11} {d₂ : Type u_12} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (A C : Matrix d₁ d₁ ℂ) (B D : Matrix d₂ d₂ ℂ) (hA : (Matrix.toEuclideanLin A).ker ≤ (Matrix.toEuclideanLin C).ker) (hB : (Matrix.toEuclideanLin B).ker ≤ (Matrix.toEuclideanLin D).ker) : (Matrix.toEuclideanLin (A.kronecker B)).ker ≤ (Matrix.toEuclideanLin (C.kronecker D)).ker

If the kernels of the components are contained, then the kernel of the Kronecker product is contained.

theorem ker_le_of_ker_kron_le_left {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂) (h : (↑(σ₁ ⊗ᴹ σ₂)).ker ≤ (↑(ρ₁ ⊗ᴹ ρ₂)).ker) : (↑σ₁).ker ≤ (↑ρ₁).ker

If the kernel of a product state is contained in another, the left component kernel is contained.

theorem ker_le_of_ker_kron_le_right {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂) (h : (↑(σ₁ ⊗ᴹ σ₂)).ker ≤ (↑(ρ₁ ⊗ᴹ ρ₂)).ker) : (↑σ₂).ker ≤ (↑ρ₂).ker

If the kernel of a product state is contained in another, the right component kernel is contained.

theorem ker_prod_le_iff {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂) : (↑(σ₁ ⊗ᴹ σ₂)).ker ≤ (↑(ρ₁ ⊗ᴹ ρ₂)).ker ↔ (↑σ₁).ker ≤ (↑ρ₁).ker ∧ (↑σ₂).ker ≤ (↑ρ₂).ker

The kernel of a product state is contained in another product state's kernel iff the individual kernels are contained.

theorem HermitianMat.inner_kron {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (A : HermitianMat d₁ ℂ) (B : HermitianMat d₂ ℂ) (C : HermitianMat d₁ ℂ) (D : HermitianMat d₂ ℂ) : inner ℝ (A.kronecker B) (C.kronecker D) = inner ℝ A C * inner ℝ B D

theorem continuousOn_rpow_uniform {K : Set ℝ} (hK : IsCompact K) : ContinuousOn (fun (r : ℝ) => (UniformOnFun.ofFun {K}) fun (t : ℝ) => t ^ r) (Set.Ioi 0)

theorem sandwichedRelRentropy_additive_alpha_one_aux {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂) (h1 : (↑σ₁).ker ≤ (↑ρ₁).ker) (h2 : (↑σ₂).ker ≤ (↑ρ₂).ker) : inner ℝ (↑(ρ₁ ⊗ᴹ ρ₂)) ((↑(ρ₁ ⊗ᴹ ρ₂)).log - (↑(σ₁ ⊗ᴹ σ₂)).log) = inner ℝ (↑ρ₁) ((↑ρ₁).log - (↑σ₁).log) + inner ℝ (↑ρ₂) ((↑ρ₂).log - (↑σ₂).log)

def SandwichedRelRentropy {d : Type u_1} [Fintype d] [DecidableEq d] (α : ℝ) (ρ σ : MState d) : ENNReal

The Sandwiched Renyi Relative Entropy, defined with ln (nits). Note that at α = 1 this definition switch to the standard Relative Entropy, for continuity. For α ≤ 0, this gives junk value 0. (There is no conventional value for α < 0; there is a continuous limit at α = 0, but it is complicated and unneeded at the moment.)

Equations

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

def «termD̃__(_‖_)» : Lean.ParserDescr

Equations

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

def qRelativeEnt {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) : ENNReal

The quantum relative entropy 𝐃(ρ‖σ) := Tr[ρ (log ρ - log σ)]. Also called the Umegaki quantum relative entropy, when it's necessary to distinguish from other relative entropies.

Equations

• 𝐃(ρ‖σ) = D̃_1(ρ‖σ)

def «term𝐃(_‖_)» : Lean.ParserDescr

Equations

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

theorem sandwiched_term_product {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂) (α β : ℝ) : ((HermitianMat.conj ↑(↑(σ₁ ⊗ᴹ σ₂) ^ β)) ↑(ρ₁ ⊗ᴹ ρ₂) ^ α).trace = ((HermitianMat.conj ↑(↑σ₁ ^ β)) ↑ρ₁ ^ α).trace * ((HermitianMat.conj ↑(↑σ₂ ^ β)) ↑ρ₂ ^ α).trace

theorem sandwichedRelRentropy_additive_alpha_ne_one {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] {α : ℝ} (hα : α ≠ 1) (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂) : D̃_α(ρ₁ ⊗ᴹ ρ₂‖σ₁ ⊗ᴹ σ₂) = D̃_α(ρ₁‖σ₁) + D̃_α(ρ₂‖σ₂)

@[simp]

theorem sandwichedRelRentropy_additive {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (α : ℝ) (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂) : D̃_α(ρ₁ ⊗ᴹ ρ₂‖σ₁ ⊗ᴹ σ₂) = D̃_α(ρ₁‖σ₁) + D̃_α(ρ₂‖σ₂)

The Sandwiched Renyi Relative entropy is additive when the inputs are product states

@[simp]

theorem qRelativeEnt_additive {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂) : 𝐃(ρ₁ ⊗ᴹ ρ₂‖σ₁ ⊗ᴹ σ₂) = 𝐃(ρ₁‖σ₁) + 𝐃(ρ₂‖σ₂)

The quantum relative entropy is additive when the inputs are product states

@[simp]

theorem sandwichedRelRentropy_relabel {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] {α : ℝ} (ρ σ : MState d) (e : d₂ ≃ d) : D̃_α(ρ.relabel e‖σ.relabel e) = D̃_α(ρ‖σ)

@[simp]

theorem sandwichedRelRentropy_self {d : Type u_1} [Fintype d] [DecidableEq d] {α : ℝ} (hα : 0 < α) (ρ : MState d) : D̃_α(ρ‖ρ) = 0

theorem sandwichedRelEntropy_ne_top {d : Type u_1} [Fintype d] [DecidableEq d] {α : ℝ} {ρ σ : MState d} [(↑σ).NonSingular] : D̃_α(ρ‖σ) ≠ ⊤

theorem continuousOn_exponent : ContinuousOn (fun (α : ℝ) => (1 - α) / (2 * α)) (Set.Ioi 0)

theorem Complex.continuousOn_cpow_const_Ioi (z : ℂ) : ContinuousOn (fun (r : ℝ) => z ^ ↑r) (Set.Ioi 0)

theorem maps_to_Iio_of_Ioi_1 : Set.MapsTo (fun (α : ℝ) => (1 - α) / (2 * α)) (Set.Ioi 1) (Set.Iio 0)

The function α ↦ (1 - α) / (2 * α) maps the interval (1, ∞) to (-∞, 0).

@[simp]

theorem frontier_singleton {X : Type u_11} [TopologicalSpace X] [T1Space X] [PerfectSpace X] (p : X) : frontier {p} = {p}

theorem sandwichedRelRentropy.continuousOn {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) : ContinuousOn (fun (α : ℝ) => D̃_α(ρ‖σ)) (Set.Ioi 0)

theorem qRelativeEnt_ker {d : Type u_1} [Fintype d] [DecidableEq d] {ρ σ : MState d} (h : (↑σ).ker ≤ (↑ρ).ker) : ↑𝐃(ρ‖σ) = ↑(inner ℝ (↑ρ) ((↑ρ).log - (↑σ).log))

Quantum relative entropy as Tr[ρ (log ρ - log σ)] when supports are contained.

theorem qRelativeEnt_eq_neg_Sᵥₙ_add {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) : ↑𝐃(ρ‖σ) = -↑(Sᵥₙ ρ) + if (↑σ).ker ≤ (↑ρ).ker then -↑(inner ℝ (↑ρ) (↑σ).log) else ⊤

@[simp]

theorem qRelativeEnt_relabel {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] (ρ σ : MState d) (e : d₂ ≃ d) : 𝐃(ρ.relabel e‖σ.relabel e) = 𝐃(ρ‖σ)

The quantum relative entropy is unchanged by MState.relabel

@[simp]

theorem sandwichedRelRentropy_of_unique {d : Type u_1} [Fintype d] [DecidableEq d] {α : ℝ} [Unique d] (ρ σ : MState d) : D̃_α(ρ‖σ) = 0

@[simp]

theorem qRelEntropy_of_unique {d : Type u_1} [Fintype d] [DecidableEq d] [Unique d] (ρ σ : MState d) : 𝐃(ρ‖σ) = 0

theorem sandwichedRelRentropy_heq_congr {α : ℝ} {d₁ d₂ : Type u} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] {ρ₁ σ₁ : MState d₁} {ρ₂ σ₂ : MState d₂} (hd : d₁ = d₂) (hρ : ρ₁ ≍ ρ₂) (hσ : σ₁ ≍ σ₂) : D̃_α(ρ₁‖σ₁) = D̃_α(ρ₂‖σ₂)

theorem sandwichedRelRentropy_congr {α : ℝ} {d₁ d₂ : Type u} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] {ρ₁ σ₁ : MState d₁} {ρ₂ σ₂ : MState d₂} (hd : d₁ = d₂) (hρ : ρ₁ = ρ₂.relabel (Equiv.cast hd)) (hσ : σ₁ = σ₂.relabel (Equiv.cast hd)) : D̃_α(ρ₁‖σ₁) = D̃_α(ρ₂‖σ₂)

theorem qRelEntropy_heq_congr {d₁ d₂ : Type u} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] {ρ₁ σ₁ : MState d₁} {ρ₂ σ₂ : MState d₂} (hd : d₁ = d₂) (hρ : ρ₁ ≍ ρ₂) (hσ : σ₁ ≍ σ₂) : 𝐃(ρ₁‖σ₁) = 𝐃(ρ₂‖σ₂)

theorem qRelativeEnt_rank {d : Type u_1} [Fintype d] [DecidableEq d] {ρ σ : MState d} [(↑σ).NonSingular] : ↑𝐃(ρ‖σ) = ↑(inner ℝ (↑ρ) ((↑ρ).log - (↑σ).log))

Quantum relative entropy when σ has full rank

theorem inner_log_bounded_near {d : Type u_1} [Fintype d] [DecidableEq d] {ρ σ : MState d} (hx : (↑σ).ker ≤ (↑ρ).ker) {y : ℝ} (hy : inner ℝ (↑ρ) (↑σ).log < y) : ∀ᶠ (x : MState d) in nhds σ, (↑x).ker ≤ (↑ρ).ker → inner ℝ (↑ρ) (↑x).log < y

theorem qRelativeEnt_lowerSemicontinuous_2 {d : Type u_1} [Fintype d] [DecidableEq d] (ρ x : MState d) (hx : ¬(↑x).ker ≤ (↑ρ).ker) (y : ENNReal) (hy : y < ⊤) : ∀ᶠ (x' : MState d) in nhds x, ↑y < if (↑x').ker ≤ (↑ρ).ker then ↑(inner ℝ (↑ρ) ((↑ρ).log - (↑x').log)) else ⊤

theorem qRelativeEnt.lowerSemicontinuous {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : LowerSemicontinuous fun (σ : MState d) => 𝐃(ρ‖σ)

theorem qRelativeEnt_joint_convexity {d : Type u_1} [Fintype d] [DecidableEq d] (ρ₁ ρ₂ σ₁ σ₂ : MState d) (p : Prob) : 𝐃(p[ρ₁↔ρ₂]‖p[σ₁↔σ₂]) ≤ ↑↑p * 𝐃(ρ₁‖σ₁) + (1 - ↑↑p) * 𝐃(ρ₂‖σ₂)

Joint convexity of Quantum relative entropy. We can't state this with ConvexOn because that requires an AddCommMonoid, which MStates are not. Instead we state it with Mixable.

TODO:

• Add the Mixable instance that infers from the Coe so that the right hand side can be written as p [𝐃(ρ₁‖σ₁) ↔ 𝐃(ρ₂‖σ₂)]
• Define (joint) convexity as its own thing - a ConvexOn for Mixable types.
• Maybe, more broadly, find a way to make ConvexOn work with the subset of Matrix that corresponds to MState.

@[simp]

theorem qRelEntropy_self {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : 𝐃(ρ‖ρ) = 0

theorem qRelativeEnt_ne_top {d : Type u_1} [Fintype d] [DecidableEq d] {ρ σ : MState d} [(↑σ).NonSingular] : 𝐃(ρ‖σ) ≠ ⊤

theorem qMutualInfo_as_qRelativeEnt {dA : Type u_5} {dB : Type u_6} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : MState (dA × dB)) : ↑(qMutualInfo ρ) = ↑𝐃(ρ‖ρ.traceRight ⊗ᴹ ρ.traceLeft)

I(A:B) = 𝐃(ρᴬᴮ‖ρᴬ ⊗ ρᴮ)

theorem qRelEntropy_le_add_of_le_smul {d : Type u_1} [Fintype d] [DecidableEq d] {α : ℝ} (ρ : MState d) {σ₁ σ₂ : MState d} (hσ : ↑σ₂ ≤ α • ↑σ₁) : 𝐃(ρ‖σ₁) ≤ 𝐃(ρ‖σ₂) + ENNReal.ofReal (Real.log α)

theorem qRelativeEnt_op_le {d : Type u_1} [Fintype d] [DecidableEq d] {α : ℝ} {ρ σ : MState d} (h : ↑ρ ≤ α • ↑σ) : 𝐃(ρ‖σ) ≤ ENNReal.ofReal (Real.log α)