From a2b052af9bfd471bd9524626510a14cf4ee275ee Mon Sep 17 00:00:00 2001 From: Dennj Osele Date: Wed, 13 May 2026 16:35:19 +0100 Subject: [PATCH 1/2] feat(AxiomatizedEntropy): expand RelEntropy API and add Hellinger overlap --- QuantumInfo/ClassicalInfo/Hellinger.lean | 115 ++ .../Finite/AxiomatizedEntropy/Defs.lean | 1111 +++++++++++++++-- .../Finite/AxiomatizedEntropy/Renyi.lean | 81 +- 3 files changed, 1206 insertions(+), 101 deletions(-) create mode 100644 QuantumInfo/ClassicalInfo/Hellinger.lean diff --git a/QuantumInfo/ClassicalInfo/Hellinger.lean b/QuantumInfo/ClassicalInfo/Hellinger.lean new file mode 100644 index 000000000..1b4ea17c3 --- /dev/null +++ b/QuantumInfo/ClassicalInfo/Hellinger.lean @@ -0,0 +1,115 @@ +/- +Copyright (c) 2026 Dennj Osele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Dennj Osele +-/ +module + +public import QuantumInfo.ClassicalInfo.Distribution +public import Mathlib.Data.Real.Sqrt + +/-! # Hellinger overlap for finite probability distributions + +This file contains finite-distribution API for the Hellinger overlap, also known as the +Bhattacharyya coefficient. The statements are deliberately classical/probabilistic and avoid +quantum-specific matrix or state types. +-/ + +@[expose] public section + +noncomputable section +universe u + +open scoped BigOperators + +/-- The Hellinger overlap, or Bhattacharyya coefficient, of two finite probability distributions. -/ +def hellingerOverlap {κ : Type u} [Fintype κ] (P Q : ProbDistribution κ) : ℝ := + ∑ x, Real.sqrt ((P x : ℝ) * (Q x : ℝ)) + +/-- The Hellinger overlap is multiplicative over independent product distributions. -/ +theorem hellingerOverlap_prod {κ η : Type u} [Fintype κ] [Fintype η] + (P₁ Q₁ : ProbDistribution κ) (P₂ Q₂ : ProbDistribution η) : + hellingerOverlap (ProbDistribution.prod P₁ P₂) (ProbDistribution.prod Q₁ Q₂) = + hellingerOverlap P₁ Q₁ * hellingerOverlap P₂ Q₂ := by + rw [hellingerOverlap, hellingerOverlap, hellingerOverlap, Fintype.sum_prod_type] + calc + (∑ x : κ, ∑ y : η, + Real.sqrt ((((P₁ x) * (P₂ y) : Prob) : ℝ) * + (((Q₁ x) * (Q₂ y) : Prob) : ℝ))) = + ∑ x : κ, ∑ y : η, + Real.sqrt ((P₁ x : ℝ) * (Q₁ x : ℝ)) * + Real.sqrt ((P₂ y : ℝ) * (Q₂ y : ℝ)) := by + exact Finset.sum_congr rfl fun x _ => Finset.sum_congr rfl fun y _ => by + simp [mul_assoc, mul_left_comm, mul_comm] + _ = (∑ x : κ, Real.sqrt ((P₁ x : ℝ) * (Q₁ x : ℝ))) * + ∑ y : η, Real.sqrt ((P₂ y : ℝ) * (Q₂ y : ℝ)) := by + rw [Finset.sum_mul] + simp_rw [Finset.mul_sum] + +/-- Closed form for the Hellinger overlap of two Bernoulli distributions. -/ +theorem hellingerOverlap_coin (p q : Prob) : + hellingerOverlap (ProbDistribution.coin p) (ProbDistribution.coin q) = + Real.sqrt ((p : ℝ) * (q : ℝ)) + + Real.sqrt ((1 - (p : ℝ)) * (1 - (q : ℝ))) := by + simp [hellingerOverlap, Fin.sum_univ_two] + +/-- Distinct Bernoulli parameters have Hellinger overlap strictly less than one. -/ +theorem hellingerOverlap_coin_lt_one (p q : Prob) (hpq : (p : ℝ) < q) : + hellingerOverlap (ProbDistribution.coin p) (ProbDistribution.coin q) < 1 := by + rw [hellingerOverlap_coin] + have hp0 : 0 ≤ (p : ℝ) := p.2.1 + have hp1 : (p : ℝ) ≤ 1 := p.2.2 + have hq0 : 0 ≤ (q : ℝ) := q.2.1 + have hq1 : (q : ℝ) ≤ 1 := q.2.2 + have hsqrt_lt : + Real.sqrt (((p : ℝ) * q) * ((1 - p) * (1 - q))) < + ((p : ℝ) + q - 2 * p * q) / 2 := by + rw [Real.sqrt_lt' (by + nlinarith [mul_nonneg hp0 (sub_nonneg.mpr hq1), + mul_pos (lt_of_le_of_lt hp0 hpq) (sub_pos.mpr (hpq.trans_le hq1))])] + nlinarith [sq_pos_of_pos (sub_pos.mpr hpq)] + exact (sq_lt_sq₀ (by positivity) (by positivity)).mp <| by + rw [add_sq, Real.sq_sqrt (mul_nonneg hp0 hq0), + Real.sq_sqrt (mul_nonneg (sub_nonneg.mpr hp1) (sub_nonneg.mpr hq1))] + nlinarith [(Real.sqrt_mul (mul_nonneg hp0 hq0) ((1 - p) * (1 - q))).symm] + +/-- The type obtained by taking `n` iterated dyadic self-products of `d`. -/ +def DyadicPow (d : Type u) : ℕ → Type u + | 0 => d + | n + 1 => DyadicPow d n × DyadicPow d n + +instance dyadicPowFintype {d : Type u} [Fintype d] (n : ℕ) : Fintype (DyadicPow d n) := by + induction n with + | zero => simpa [DyadicPow] using (inferInstance : Fintype d) + | succ n ih => simpa [DyadicPow] using (inferInstance : Fintype (DyadicPow d n × DyadicPow d n)) + +instance dyadicPowDecidableEq {d : Type u} [DecidableEq d] (n : ℕ) : + DecidableEq (DyadicPow d n) := by + induction n with + | zero => simpa [DyadicPow] using (inferInstance : DecidableEq d) + | succ n ih => + simpa [DyadicPow] using (inferInstance : DecidableEq (DyadicPow d n × DyadicPow d n)) + +/-- Iterated dyadic product power of a finite probability distribution. -/ +def dyadicProbPow {d : Type u} [Fintype d] (dist : ProbDistribution d) : + ∀ n, ProbDistribution (DyadicPow d n) + | 0 => dist + | n + 1 => ProbDistribution.prod (dyadicProbPow dist n) (dyadicProbPow dist n) + +/-- Hellinger overlap of dyadic product powers. -/ +theorem hellingerOverlap_dyadicProbPow {d : Type u} [Fintype d] + (P Q : ProbDistribution d) : + ∀ n, hellingerOverlap (dyadicProbPow P n) (dyadicProbPow Q n) = + (hellingerOverlap P Q) ^ (2 ^ n : ℕ) := by + intro n + induction n with + | zero => + change hellingerOverlap P Q = (hellingerOverlap P Q) ^ (1 : ℕ) + rw [pow_one] + | succ n ih => + change hellingerOverlap + (ProbDistribution.prod (dyadicProbPow P n) (dyadicProbPow P n)) + (ProbDistribution.prod (dyadicProbPow Q n) (dyadicProbPow Q n)) = + (hellingerOverlap P Q) ^ (2 ^ (n + 1) : ℕ) + rw [hellingerOverlap_prod, ih, show 2 ^ (n + 1) = 2 ^ n + 2 ^ n by omega, pow_add] + diff --git a/QuantumInfo/Finite/AxiomatizedEntropy/Defs.lean b/QuantumInfo/Finite/AxiomatizedEntropy/Defs.lean index bc005b822..6756feedf 100644 --- a/QuantumInfo/Finite/AxiomatizedEntropy/Defs.lean +++ b/QuantumInfo/Finite/AxiomatizedEntropy/Defs.lean @@ -1,13 +1,18 @@ /- Copyright (c) 2025 Alex Meiburg. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Alex Meiburg +Authors: Alex Meiburg, Dennj Osele -/ module public import QuantumInfo.ClassicalInfo.Entropy +public import QuantumInfo.ClassicalInfo.Hellinger public import QuantumInfo.Finite.MState public import QuantumInfo.Finite.CPTPMap +public import QuantumInfo.Finite.POVM +public import QuantumInfo.Finite.Entropy.Relative + +@[expose] public section /-! # Generalized quantum entropy and relative entropy @@ -41,13 +46,14 @@ by Marco Tomamichel -/ -@[expose] public section - noncomputable section universe u +open ComplexOrder open scoped NNReal open scoped ENNReal +open scoped Kronecker +open scoped HermitianMat variable (f : ∀ {d : Type u} [Fintype d] [DecidableEq d], MState d → HermitianMat d ℂ → ℝ≥0∞) @@ -55,24 +61,26 @@ variable (f : ∀ {d : Type u} [Fintype d] [DecidableEq d], MState d → Hermiti [Tomamichel](https://www.marcotom.info/files/entropy-masterclass2022.pdf). This simpler class allows for _trivial_ relative entropies, such as `-log tr(ρ⁰σ)`. -Use mixing `RelEntropy.Nontrivial` to only allow nontrivial relative entropies. -/ +Use the mixin `RelEntropy.Nontrivial` to only allow nontrivial relative entropies. -/ class RelEntropy : Prop where /-- The data processing inequality -/ DPI {d₁ d₂ : Type u} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] (ρ σ : MState d₁) (Λ : CPTPMap d₁ d₂) : f (Λ ρ) (Λ σ) ≤ f ρ σ /-- Entropy is additive under tensor products -/ of_kron {d₁ d₂ : Type u} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] : - ∀ (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂), f (ρ₁ ⊗ ρ₂) (σ₁ ⊗ σ₂) = f ρ₁ σ₁ + f ρ₂ σ₂ + ∀ (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂), f (ρ₁ ⊗ᴹ ρ₂) (σ₁ ⊗ᴹ σ₂) = f ρ₁ σ₁ + f ρ₂ σ₂ /-- Normalization of entropy to be `ln N` for a pure state vs. uniform on `N` many states. -/ normalized {d : Type u} [fin : Fintype d] [DecidableEq d] [Nonempty d] (i : d) : f (.ofClassical (.constant i)) MState.uniform.M = some ⟨Real.log fin.card, Real.log_nonneg (mod_cast Fintype.card_pos)⟩ -/-- The axioms to be a well-behaved quantum relative entropy, as given by -[Tomamichel](https://www.marcotom.info/files/entropy-masterclass2022.pdf). -/ +/-- Mixin on top of `RelEntropy` that rules out trivial relative entropies (those that vanish +on every pair of full-support states). See [Tomamichel](https://www.marcotom.info/files/entropy-masterclass2022.pdf). -/ class RelEntropy.Nontrivial [RelEntropy f] where - /-- Nontriviality condition for a relative entropy. -/ - nontrivial (d) [Fintype d] [DecidableEq d] : ∃ (ρ σ : MState d), + /-- Nontriviality condition for a relative entropy: some pair of full-support states has + positive relative entropy. This is the negation of Tomamichel's definition of a trivial + relative entropy, which vanishes on all full-support state pairs. -/ + nontrivial : ∃ (d : Type u) (_ : Fintype d) (_ : DecidableEq d) (ρ σ : MState d), ρ.M.support = ⊤ ∧ σ.M.support = ⊤ ∧ 0 < f ρ σ namespace RelEntropy @@ -101,23 +109,22 @@ At that point we need the fact that it's not `⊤`, and then it must be zero. -/ -/-- Relabelling a state with `CPTPMap.of_equiv` leaves relative entropies unchanged. -/ +/-- Relabelling a state with `CPTPMap.ofEquiv` leaves relative entropies unchanged. -/ @[simp] -theorem of_equiv_eq (e : d ≃ d₂) (ρ σ : MState d) : - f (CPTPMap.of_equiv e ρ) (CPTPMap.of_equiv e σ) = f ρ σ := by +theorem ofEquiv_eq (e : d ≃ d₂) (ρ σ : MState d) : + f (CPTPMap.ofEquiv e ρ) (CPTPMap.ofEquiv e σ) = f ρ σ := by apply le_antisymm · apply DPI - · convert DPI (f := f) ((CPTPMap.of_equiv e) ρ) ((CPTPMap.of_equiv e) σ) (CPTPMap.of_equiv e.symm) - · symm - exact congrFun (CPTPMap.equiv_inverse e.symm) ρ - · symm - exact congrFun (CPTPMap.equiv_inverse e.symm) σ + · convert DPI (f := f) ((CPTPMap.ofEquiv e) ρ) ((CPTPMap.ofEquiv e) σ) (CPTPMap.ofEquiv e.symm) + all_goals + symm + exact congrFun (CPTPMap.equiv_inverse e.symm) _ /-- Relabelling a state with `MState.relabel` leaves relative entropies unchanged. -/ @[simp] theorem relabel_eq (e : d₂ ≃ d) (ρ σ : MState d) : f (ρ.relabel e) (σ.relabel e) = f ρ σ := by - apply of_equiv_eq + exact ofEquiv_eq (f := f) e.symm ρ σ --Tomamichel's "4. Positivity" theorem is implicit true in our description because we --only allow ENNReals. The only part to prove is that "D(ρ‖σ) = 0 if ρ = σ". @@ -125,65 +132,78 @@ theorem relabel_eq (e : d₂ ≃ d) (ρ σ : MState d) : /-- The relative entropy is zero between any two states on a 1-D Hilbert space. -/ private lemma wrt_self_eq_zero' [Unique d] (ρ σ : MState d) : f ρ σ = 0 := by convert normalized (f := f) (d := d) default - · apply Subsingleton.allEq - · apply Subsingleton.allEq - · simp + · exact Subsingleton.allEq _ _ + · exact Subsingleton.allEq _ _ + · simp [Fintype.card_unique, Real.log_one] + rfl /-- The relative entropy `D(ρ‖ρ) = 0`. -/ @[simp] theorem wrt_self_eq_zero (ρ : MState d) : f ρ ρ.M = 0 := by rw [← nonpos_iff_eq_zero, ← wrt_self_eq_zero' f (d := PUnit) default default] - convert DPI (f := f) _ _ (CPTPMap.const_state ρ) - · rw [CPTPMap.const_state_apply] - · rw [CPTPMap.const_state_apply] + convert DPI (f := f) _ _ (CPTPMap.replacement ρ) + all_goals rw [CPTPMap.replacement_apply] end possibly_trivial -section nontrivial -variable [Nontrivial f] - -/-- A nontrivial relative entropy is **faithful**, it can distinguish when two states are equal. -/ -theorem faithful (ρ σ : MState d) : f ρ σ = 0 ↔ ρ = σ := by - sorry - -end nontrivial - section bounds open Prob in -/-- Quantum relative min-entropy. -/ +/-- A support-test lower bound for relative entropies. + +This is not the standard quantum relative min-entropy on state inputs: for density-matrix +second arguments it collapses to zero, as `min_state_eq_zero` shows. The name is kept because +it is the min-side bound paired with `max` in this axiomatized API. -/ def min (ρ : MState d) (σ : HermitianMat d ℂ) : ENNReal := - —log ⟨_, ρ.exp_val_prob ⟨proj_le_nonneg 0 σ, proj_le_le_one _ _⟩⟩ + —log ⟨ρ.exp_val (HermitianMat.projLE 0 σ), + ρ.exp_val_prob ⟨HermitianMat.projLE_nonneg 0 σ, HermitianMat.projLE_le_one 0 σ⟩⟩ @[aesop (rule_sets := [finiteness]) simp] theorem min_eq_top_iff (ρ : MState d) (σ : HermitianMat d ℂ) : - (min ρ σ) = ⊤ ↔ ρ.M.support ≤ σ.ker := by - open scoped HermitianMat in - have h₂ : {0 ≤ₚ σ}.ker = σ.ker := by - sorry --missing simp lemma - simp [min, Prob.negLog_eq_top_iff, MState.exp_val_eq_zero_iff, Subtype.ext_iff, proj_le_nonneg, h₂] + (min ρ σ) = ⊤ ↔ ρ.M.support ≤ (HermitianMat.projLE 0 σ).ker := by + rw [min, Prob.negLog_eq_top_iff] + constructor + · intro h + have h0 : ρ.exp_val (HermitianMat.projLE 0 σ) = 0 := by + simpa using congrArg (fun p : Prob => (p : ℝ)) h + exact (ρ.exp_val_eq_zero_iff (HermitianMat.projLE_nonneg 0 σ)).mp h0 + · intro h + exact Subtype.ext ((ρ.exp_val_eq_zero_iff (HermitianMat.projLE_nonneg 0 σ)).mpr h) -open scoped HermitianMat in protected theorem toReal_min (ρ : MState d) (σ : HermitianMat d ℂ) : - (min ρ σ).toReal = -Real.log (ρ.exp_val {0 ≤ₚ σ}) := - Prob.negLog_pos_Real + (min ρ σ).toReal = -Real.log (ρ.exp_val (HermitianMat.projLE 0 σ)) := by + simp [min, + Prob.negLog_pos_Real (p := ⟨ρ.exp_val (HermitianMat.projLE 0 σ), + ρ.exp_val_prob ⟨HermitianMat.projLE_nonneg 0 σ, HermitianMat.projLE_le_one 0 σ⟩⟩)] + + +/-- On state inputs, the current support-based `min` quantity is always zero. -/ +@[simp] +theorem min_state_eq_zero (ρ σ : MState d) : min ρ σ.M = 0 := by + have hproj : HermitianMat.projLE 0 σ.M = 1 := by + rw [HermitianMat.projLE_zero_cfc] + calc σ.M.cfc (fun x ↦ if 0 ≤ x then 1 else 0) = σ.M.cfc (fun _ ↦ (1 : ℝ)) := + HermitianMat.cfc_congr_of_nonneg σ.nonneg fun _ hx => by simpa using hx + _ = 1 := by simp [HermitianMat.cfc_const (A := σ.M) (r := (1 : ℝ))] + simp [min, show (⟨ρ.exp_val (HermitianMat.projLE 0 σ.M), + ρ.exp_val_prob ⟨HermitianMat.projLE_nonneg 0 σ.M, HermitianMat.projLE_le_one 0 σ.M⟩⟩ : Prob) = 1 + from Subtype.ext (by change ρ.exp_val _ = 1; rw [hproj, MState.exp_val_one])] -/-- Min-relative entropy is a valid entropy function, albeit trivial (and not faithful). -/ -instance : RelEntropy min where - DPI := sorry - of_kron := sorry - normalized := sorry +/-- The current support-based `min` quantity does not satisfy the normalization axiom of `RelEntropy`. -/ +theorem not_RelEntropy_min : ¬ RelEntropy min := by + intro hmin + have := congrArg ENNReal.toReal (hmin.normalized (d := ULift (Fin 2)) (i := ⟨0⟩)) + simp at this; linarith [Real.log_pos one_lt_two] -theorem not_Nontrivial_min : ¬Nontrivial min := by +theorem not_Nontrivial_min [RelEntropy min] : ¬Nontrivial min := by rintro ⟨h⟩ - obtain ⟨ρ, σ, h₁, h₂, h₃⟩ := h (ULift (Fin 2)) - replace h₂ : proj_le 0 σ = (1 : HermitianMat (ULift (Fin 2)) ℂ) := by - sorry--TODO - simp [min, Subtype.ext_iff, MState.exp_val_eq_one_iff, proj_le_le_one, h₁, h₂] at h₃ + obtain ⟨d, _, _, ρ, σ, -, -, hpos⟩ := h + simp at hpos +omit [RelEntropy f] in /-- The relative min-entropy is a lower bound on all relative entropies. -/ -theorem min_le (ρ σ : MState d) : min ρ σ ≤ f ρ σ := by - sorry --Tomamichel, https://www.marcotom.info/files/entropy-masterclass2022.pdf, (1.28) +theorem min_le (ρ σ : MState d) : min ρ σ.M ≤ f ρ σ.M := by + simp open Classical in /-- Quantum relative max-entropy. -/ @@ -194,54 +214,979 @@ def max (ρ : MState d) (σ : HermitianMat d ℂ) : ENNReal := ⊤ @[aesop (rule_sets := [finiteness]) simp] -protected theorem max_not_top (ρ : MState d) (σ : HermitianMat d ℂ) : +protected theorem max_not_top (ρ : MState d) (σ : HermitianMat d ℂ) (hσ : 0 ≤ σ) : (max ρ σ) ≠ ⊤ ↔ σ.ker ≤ ρ.M.ker := by open ComplexOrder in constructor · intro h - contrapose! h - simp only [max, ENNReal.some_eq_coe, ite_eq_right_iff, ENNReal.coe_ne_top, imp_false, - not_exists] - intro x - contrapose! h - intro v hv - rw [HermitianMat.ker, LinearMap.mem_ker] at hv ⊢ - replace hv : σ.toMat.mulVec v = 0 := sorry --why is this not defeq?? - replace h := h.right v - rw [Matrix.sub_mulVec] at h - simp [hv, Matrix.smul_mulVec_assoc] at h - have := ρ.pos.right v - -- have := le_antisymm (ρ.pos.right v) (by ) - sorry - · intro - rw [max, if_pos] - · nofun - sorry --log ("min nonzero eigenvalue of σ" / "max eigenvalue of ρ") should work + have hx : ∃ x : ℝ, ρ.M ≤ Real.exp x • σ := by + by_contra hx + exact h (by simp [max, hx]) + obtain ⟨x, hx⟩ := hx + exact HermitianMat.ker_le_of_le_smul (Real.exp_pos x).ne' ρ.nonneg hx + · intro hker + let P := σ.supportProj + have hright : ρ.M.mat * P.mat = ρ.M.mat := by + dsimp [P]; simpa using HermitianMat.mul_supportProj_of_ker_le (A := ρ.M) (B := σ) hker + have hleft : P.mat * ρ.M.mat = ρ.M.mat := by + simpa only [Matrix.conjTranspose_mul, HermitianMat.conjTranspose_mat] using + congrArg Matrix.conjTranspose hright + have hP_idem : P.mat * P.mat = P.mat := by + rw [← pow_two, ← HermitianMat.mat_pow] + congr 1 + dsimp [P] + rw [HermitianMat.supportProj_eq_cfc, ← HermitianMat.cfc_pow, + ← HermitianMat.cfc_comp_apply] + exact HermitianMat.cfc_congr_of_nonneg hσ fun x _ => by + by_cases hx : x = 0 <;> simp [hx] + have hρ_le_P : ρ.M ≤ P := calc + ρ.M = ρ.M.conj P.mat := by + symm; apply HermitianMat.ext + simp only [HermitianMat.conj_apply_mat, HermitianMat.conjTranspose_mat, + hright, hleft] + _ ≤ (1 : HermitianMat d ℂ).conj P.mat := HermitianMat.conj_mono ρ.le_one + _ = P := by apply HermitianMat.ext; simp [HermitianMat.conj_apply_mat, hP_idem] + let α : ℝ := ∑ i, if σ.H.eigenvalues i = 0 then 0 else (σ.H.eigenvalues i)⁻¹ + have hterm j : 0 ≤ if σ.H.eigenvalues j = 0 then 0 else (σ.H.eigenvalues j)⁻¹ := by + split_ifs + · rfl + · exact inv_nonneg.mpr (HermitianMat.eigenvalues_nonneg hσ j) + have hα_nonneg : 0 ≤ α := Finset.sum_nonneg fun i _ => hterm i + have hP_le : P ≤ α • σ := by + dsimp [P, α] + rw [← sub_nonneg, show (∑ i, if σ.H.eigenvalues i = 0 then 0 else (σ.H.eigenvalues i)⁻¹) • σ = + σ.cfc (fun x => (∑ i, if σ.H.eigenvalues i = 0 then 0 else (σ.H.eigenvalues i)⁻¹) * x) from by + simp, + HermitianMat.supportProj_eq_cfc, ← HermitianMat.cfc_sub_apply, HermitianMat.cfc_nonneg_iff] + intro i + by_cases hi : σ.H.eigenvalues i = 0 + · simp [hi] + · have hsingle : (σ.H.eigenvalues i)⁻¹ ≤ α := by + dsimp [α]; simpa [hi] using + Finset.single_le_sum (fun j _ => hterm j) (Finset.mem_univ i) + have := mul_le_mul_of_nonneg_right hsingle (HermitianMat.eigenvalues_nonneg hσ i) + simp [hi]; linarith [inv_mul_cancel₀ hi] + rw [max, if_pos ⟨Real.log (α + 1), by + calc ρ.M ≤ P := hρ_le_P + _ ≤ α • σ := hP_le + _ ≤ (α + 1) • σ := smul_le_smul_of_nonneg_right (by linarith) hσ + _ = Real.exp (Real.log (α + 1)) • σ := by + rw [Real.exp_log (by positivity : (0 : ℝ) < α + 1)]⟩] + simp protected theorem toReal_max (ρ : MState d) (σ : HermitianMat d ℂ) : - (max ρ σ).toReal = sInf { x : ℝ | ρ.M ≤ Real.exp x • σ } := by + (max ρ σ).toReal = sInf ((↑) '' { x : ℝ≥0 | ρ.M ≤ Real.exp x • σ }) := by rw [max] split_ifs with h - · have : { x : ℝ | ρ.M ≤ Real.exp x • σ }.Nonempty := by - convert h + · have hs : ({ x : ℝ≥0 | ρ.M ≤ Real.exp x • σ } : Set ℝ≥0).Nonempty := by + rcases h with ⟨x, hx⟩ + have hσ_nonneg : 0 ≤ σ := + (smul_le_smul_iff_of_pos_left (Real.exp_pos x)).mp (by simpa using le_trans ρ.nonneg hx) + refine ⟨⟨Max.max x 0, le_max_right _ _⟩, ?_⟩ + exact hx.trans <| + smul_le_smul_of_nonneg_right + (Real.exp_le_exp.mpr (show x ≤ Max.max x 0 from le_max_left _ _)) hσ_nonneg + simp [ENNReal.some_eq_coe, NNReal.coe_sInf] + · push Not at h + have hs : ({ x : ℝ≥0 | ρ.M ≤ Real.exp x • σ } : Set ℝ≥0) = ∅ := by + ext x + simp [h (x : ℝ)] + simp [hs] + +@[simp] +theorem max_self_eq_zero (ρ : MState d) : max ρ ρ.M = 0 := by + rw [max, if_pos ⟨0, by simp⟩] + simp [show sInf { x : ℝ≥0 | ρ.M ≤ Real.exp x • ρ.M } = 0 from + le_antisymm (csInf_le ⟨0, fun x _ => x.2⟩ (by simp)) + (le_csInf ⟨0, by simp⟩ fun x _ => x.2)] + +/-- A full-support state dominates every other state up to an integer scalar. -/ +private theorem exists_le_nat_smul_of_fullSupport (ρ σ : MState d) + (hσ : σ.M.support = ⊤) : + ∃ N : ℕ, 0 < N ∧ ρ.M ≤ ((N + 1 : ℝ) • σ.M) := by + letI : σ.M.NonSingular := HermitianMat.nonSingular_iff_support_top.mpr hσ + have hexp : ∃ x : ℝ, ρ.M ≤ Real.exp x • σ.M := by + by_contra h + exact (RelEntropy.max_not_top ρ σ.M σ.nonneg).mpr + (by simp [HermitianMat.nonSingular_ker_bot]) (by simp [max, h]) + obtain ⟨x, hx⟩ := hexp + refine ⟨Nat.ceil (Real.exp x), Nat.ceil_pos.mpr (Real.exp_pos x), ?_⟩ + exact hx.trans <| smul_le_smul_of_nonneg_right ((Nat.le_ceil _).trans (by norm_num)) σ.nonneg + +/-- The output of Tomamichel's preparation channel on the first binary point. -/ +private def binaryPrepOne (γ ω : MState d) (s t : ℝ) (hden : 0 < 1 - s - t) + (h : t • γ.M ≤ (1 - s) • ω.M) : MState d where + M := (1 - s - t)⁻¹ • ((1 - s) • ω.M - t • γ.M) + nonneg := smul_nonneg (inv_nonneg.mpr hden.le) (sub_nonneg.mpr h) + tr := by + simpa [HermitianMat.trace_smul, HermitianMat.trace_sub, γ.tr, ω.tr] using + inv_mul_cancel₀ hden.ne' + +/-- The output of Tomamichel's preparation channel on the second binary point. -/ +private def binaryPrepZero (γ ω : MState d) (s t : ℝ) (hden : 0 < 1 - s - t) + (h : s • ω.M ≤ (1 - t) • γ.M) : MState d where + M := (1 - s - t)⁻¹ • ((1 - t) • γ.M - s • ω.M) + nonneg := smul_nonneg (inv_nonneg.mpr hden.le) (sub_nonneg.mpr h) + tr := by + simp [HermitianMat.trace_smul, HermitianMat.trace_sub, γ.tr, ω.tr] + field_simp [hden.ne'] + ring_nf + +/-- A binary coin lifted to the working universe. -/ +private def uliftCoin (p : Prob) : ProbDistribution (ULift.{u} (Fin 2)) := + (ProbDistribution.congr Equiv.ulift.symm) (.coin p) + +private def cqPrepareChoiH {κ : Type u} [Fintype κ] [DecidableEq κ] (τ : κ → MState d) : + HermitianMat (d × κ) ℂ := + ∑ i, HermitianMat.kronecker (τ i).M (MState.ofClassical (.constant i)).M + +private def cqPrepareChoi {κ : Type u} [Fintype κ] [DecidableEq κ] (τ : κ → MState d) : + Matrix (d × κ) (d × κ) ℂ := + (cqPrepareChoiH (d := d) τ).mat + +private def cqPrepareMap {κ : Type u} [Fintype κ] [DecidableEq κ] (τ : κ → MState d) : + MatrixMap κ d ℂ where + toFun X := fun b₁ b₂ => ∑ i, X i i * (τ i).m b₁ b₂ + map_add' X Y := by + ext b₁ b₂ + simp [Matrix.add_apply, Finset.sum_add_distrib, add_mul] + map_smul' c X := by + ext b₁ b₂ + simp [Matrix.smul_apply, Finset.mul_sum, mul_assoc] + +private theorem cqPrepareMap_choi {κ : Type u} [Fintype κ] [DecidableEq κ] (τ : κ → MState d) : + (cqPrepareMap (d := d) τ).choi_matrix = cqPrepareChoi (d := d) τ := by + ext ⟨b₁, a₁⟩ ⟨b₂, a₂⟩ + simp only [MatrixMap.choi_matrix, cqPrepareMap, Matrix.single, + cqPrepareChoi, cqPrepareChoiH, HermitianMat.mat_finset_sum, Matrix.sum_apply] + refine Finset.sum_congr rfl fun x _ => ?_ + show (if a₁ = x ∧ a₂ = x then 1 else 0) * (τ x).m b₁ b₂ = + (τ x).m b₁ b₂ * (HermitianMat.diagonal ℂ (fun x₁ => ((ProbDistribution.constant x) x₁ : ℝ))).mat a₁ a₂ + rw [HermitianMat.diagonal_mat] + aesop (add simp [Matrix.diagonal, ProbDistribution.constant_eq, Ne.symm]) + +private theorem cqPrepareChoi_psd {κ : Type u} [Fintype κ] [DecidableEq κ] (τ : κ → MState d) : + (cqPrepareChoi (d := d) τ).PosSemidef := by + change ((cqPrepareChoiH (d := d) τ).mat).PosSemidef + have hnonneg : (0 : HermitianMat (d × κ) ℂ) ≤ cqPrepareChoiH (d := d) τ := by + unfold cqPrepareChoiH + exact Finset.sum_nonneg fun i _ => + HermitianMat.kronecker_nonneg (τ i).nonneg (MState.ofClassical (.constant i)).nonneg + exact HermitianMat.zero_le_iff.mp hnonneg + +private theorem cqPrepareChoi_traceLeft {κ : Type u} [Fintype κ] [DecidableEq κ] + (τ : κ → MState d) : + (cqPrepareChoi (d := d) τ).traceLeft = 1 := by + rw [← cqPrepareMap_choi (d := d) τ, ← MatrixMap.IsTracePreserving_iff_trace_choi] + intro X + change ∑ x, ∑ i, X i i * (τ i).m x x = X.trace + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun i _ => ?_ + rw [← Finset.mul_sum, show ∑ x, (τ i).m x x = 1 by + simpa [Matrix.trace] using (MState.tr' (ρ := τ i))] + simp [Matrix.diag_apply] + +private def cqPrepareCPTP {κ : Type u} [Fintype κ] [DecidableEq κ] (τ : κ → MState d) : + CPTPMap κ d := + CPTPMap.CPTP_of_choi_PSD_Tr + (M := cqPrepareChoi (d := d) τ) + (cqPrepareChoi_psd (d := d) τ) + (cqPrepareChoi_traceLeft (d := d) τ) + +private theorem cqPrepare_apply_ofClassical {κ : Type u} [Fintype κ] [DecidableEq κ] + (τ : κ → MState d) (dist : ProbDistribution κ) : + MatrixMap.of_choi_matrix (cqPrepareChoi (d := d) τ) (MState.ofClassical dist).m + = ∑ i, (dist i : ℝ) • (τ i).m := by + rw [← cqPrepareMap_choi (d := d) τ, MatrixMap.choi_map_inv] + ext b₁ b₂ + change ∑ i, (Matrix.diagonal fun x => ((dist x : Prob) : ℂ)) i i * (τ i).m b₁ b₂ = + (∑ i, (dist i : ℝ) • (τ i).m) b₁ b₂ + rw [Matrix.sum_apply] + simp [Matrix.smul_apply] + +private theorem cqPrepare_apply_uliftCoin (τ : ULift (Fin 2) → MState d) (p : Prob) : + MatrixMap.of_choi_matrix (cqPrepareChoi (d := d) τ) (MState.ofClassical (uliftCoin p)).m = + (p : ℝ) • (τ (ULift.up (0 : Fin 2))).m + + ((1 - p : Prob) : ℝ) • (τ (ULift.up (1 : Fin 2))).m := by + rw [cqPrepare_apply_ofClassical (d := d) τ (uliftCoin p)] + ext i j + simp only [Matrix.sum_apply, Matrix.smul_apply, Complex.real_smul] + have hsum : + (∑ x : ULift (Fin 2), ↑↑((uliftCoin p) x) * (τ x).m i j) = + ∑ y : Fin 2, ↑↑((ProbDistribution.coin p) y) * (τ (ULift.up y)).m i j := by + simpa [uliftCoin, ProbDistribution.congr_apply] using + (Equiv.sum_comp (Equiv.ulift : ULift (Fin 2) ≃ Fin 2) + (fun y : Fin 2 => ↑↑((ProbDistribution.coin p) y) * (τ (ULift.up y)).m i j)) + rw [hsum] + simp [Fin.sum_univ_two] + + +private def binaryClassicalPostprocess (a b : Prob) : + CPTPMap (ULift (Fin 2)) (ULift (Fin 2)) := + let τ : ULift (Fin 2) → MState (ULift (Fin 2)) := fun i => + if i = ULift.up (0 : Fin 2) then MState.ofClassical (uliftCoin a) + else MState.ofClassical (uliftCoin b) + CPTPMap.CPTP_of_choi_PSD_Tr + (M := cqPrepareChoi (d := ULift (Fin 2)) τ) + (cqPrepareChoi_psd (d := ULift (Fin 2)) τ) + (cqPrepareChoi_traceLeft (d := ULift (Fin 2)) τ) + +private theorem binaryClassicalPostprocess_apply (a b p : Prob) : + binaryClassicalPostprocess a b (MState.ofClassical (uliftCoin p)) = + MState.ofClassical (uliftCoin (Prob.mix p a b)) := by + apply MState.ext_m + change MatrixMap.of_choi_matrix + (cqPrepareChoi (d := ULift (Fin 2)) + (fun i : ULift (Fin 2) => + if i = ULift.up (0 : Fin 2) then MState.ofClassical (uliftCoin a) + else MState.ofClassical (uliftCoin b))) + (MState.ofClassical (uliftCoin p)).m = + (MState.ofClassical (uliftCoin (Prob.mix p a b))).m + rw [cqPrepare_apply_uliftCoin] + ext i j + rcases i with ⟨i⟩ + rcases j with ⟨j⟩ + fin_cases i <;> fin_cases j + all_goals + simp [MState.m, MState.ofClassical, Matrix.add_apply, Prob.coe_one_minus, uliftCoin, + ProbDistribution.congr_apply] + rw [← HermitianMat.mat_apply, HermitianMat.diagonal_mat] + simp [Matrix.diagonal, Prob.mix, Mixable.mix, Mixable.mix_ab, Prob.coe_one_minus] + all_goals ring_nf + +private theorem uliftCoin_support_top (p : Prob) (hp0 : 0 < (p : ℝ)) (hp1 : (p : ℝ) < 1) : + (MState.ofClassical (uliftCoin p)).M.support = ⊤ := by + rw [← HermitianMat.nonSingular_iff_support_top] + apply HermitianMat.nonSingular_of_posDef + rw [MState.coe_ofClassical] + apply Matrix.PosDef.diagonal + intro i + rcases i with ⟨i⟩ + fin_cases i + · simpa [Complex.real_lt_real, uliftCoin, ProbDistribution.congr_apply] using hp0 + · simp [uliftCoin, ProbDistribution.congr_apply, Prob.coe_one_minus] + exact_mod_cast hp1 + +private def classicalIndicatorEffect {κ : Type u} [DecidableEq κ] (A : Set κ) : + HermitianMat κ ℂ := by classical exact HermitianMat.diagonal ℂ fun x => if x ∈ A then 1 else 0 + +private theorem ofClassical_exp_val_indicator + {κ : Type u} [Fintype κ] [DecidableEq κ] (dist : ProbDistribution κ) (A : Set κ) + [DecidablePred (fun x => x ∈ A)] : + (MState.ofClassical dist).exp_val (classicalIndicatorEffect A) = + ∑ x, if x ∈ A then (dist x : ℝ) else 0 := by + rw [classicalIndicatorEffect, MState.exp_val, MState.coe_ofClassical, + HermitianMat.inner_eq_re_trace] + simp [Matrix.trace, HermitianMat.diagonal] + exact Finset.sum_congr rfl fun _ _ => by split_ifs <;> simp + +private theorem exists_effect_exp_val_ne_of_ne (ρ σ : MState d) (hne : ρ ≠ σ) : + ∃ T : HermitianMat d ℂ, (0 ≤ T ∧ T ≤ 1) ∧ ρ.exp_val T ≠ σ.exp_val T := by + let A : HermitianMat d ℂ := ρ.M - σ.M + have hA_not_nonneg : ¬ 0 ≤ A := by + intro hA_nonneg + exact hne (MState.ext (eq_of_sub_eq_zero (HermitianMat.ext <| + (Matrix.PosSemidef.trace_eq_zero_iff (HermitianMat.zero_le_iff.mp hA_nonneg)).1 <| + (HermitianMat.trace_eq_zero_iff (A := A)).1 + (by simp [A, HermitianMat.trace_sub, ρ.tr, σ.tr])))) + let B : HermitianMat d ℂ := A⁻ + have hB_nonneg : 0 ≤ B := by + simpa [B] using HermitianMat.negPart_nonneg A + have hinner_neg : inner ℝ A B < 0 := by + simpa [B] using (HermitianMat.inner_negPart_neg_iff (A := A)).2 hA_not_nonneg + have hB_trace_pos : 0 < B.trace := by + refine lt_of_le_of_ne (HermitianMat.trace_nonneg hB_nonneg) ?_ + intro htrace + have hB_zero : B = 0 := HermitianMat.ext <| + (Matrix.PosSemidef.trace_eq_zero_iff (HermitianMat.zero_le_iff.mp hB_nonneg)).1 <| + (HermitianMat.trace_eq_zero_iff (A := B)).1 htrace.symm + rw [hB_zero] at hinner_neg + simp at hinner_neg + let T : HermitianMat d ℂ := B.trace⁻¹ • B + have hT_nonneg : 0 ≤ T := by + simpa [T] using smul_nonneg (inv_nonneg.mpr hB_trace_pos.le) hB_nonneg + have hT_le_one : T ≤ 1 := by + dsimp [T] + simpa [smul_smul, inv_mul_cancel₀ hB_trace_pos.ne'] using + smul_le_smul_of_nonneg_left (HermitianMat.le_trace_smul_one hB_nonneg) + (inv_nonneg.mpr hB_trace_pos.le) + refine ⟨T, ⟨hT_nonneg, hT_le_one⟩, fun hsame => ?_⟩ + have hzero : inner ℝ A T = 0 := by + simpa [A, MState.exp_val, inner_sub_left] using sub_eq_zero.mpr hsame + have hneg : inner ℝ A T < 0 := by + simpa [T, inner_smul_right] using + mul_neg_of_pos_of_neg (inv_pos.mpr hB_trace_pos) hinner_neg + linarith + +private def tauOfLE (N : ℕ) (hN : 0 < N) (ρ σ : MState d) + (h : ρ.M ≤ ((N + 1 : ℝ) • σ.M)) : MState d where + M := ((N : ℝ)⁻¹) • (((N + 1 : ℝ) • σ.M) - ρ.M) + nonneg := smul_nonneg (by positivity) (sub_nonneg.mpr h) + tr := by + have hN' : (N : ℝ) ≠ 0 := by positivity + simp [HermitianMat.trace_sub, σ.tr, ρ.tr, hN'] + +private theorem cqPrepareCPTP_uniform_tauOfLE + (M : ℕ) (hM_pos : 0 < M) (ρ σ : MState d) + (h : ρ.M ≤ ((M + 1 : ℝ) • σ.M)) : + cqPrepareCPTP (d := d) (fun i : ULift (Fin (M + 1)) => + if i = ⟨0⟩ then ρ else tauOfLE (d := d) M hM_pos ρ σ h) + (MState.uniform : MState (ULift (Fin (M + 1)))) = σ := by + let x0 : ULift (Fin (M + 1)) := ⟨0⟩ + let τr := tauOfLE (d := d) M hM_pos ρ σ h + let τ : ULift (Fin (M + 1)) → MState d := fun i => if i = x0 then ρ else τr + change cqPrepareCPTP (d := d) τ (MState.uniform : MState (ULift (Fin (M + 1)))) = σ + apply MState.ext_m + change MatrixMap.of_choi_matrix + (cqPrepareChoi (d := d) τ) + (MState.ofClassical ProbDistribution.uniform).m = σ.m + rw [cqPrepare_apply_ofClassical (d := d) τ ProbDistribution.uniform] + ext i j + simp only [ProbDistribution.uniform_def, Matrix.sum_apply, Matrix.smul_apply, + Complex.real_smul, Finset.card_univ, Fintype.card_ulift, Fintype.card_fin, one_div, + Nat.cast_add, Nat.cast_one, Complex.ofReal_inv, Complex.ofReal_add, + Complex.ofReal_natCast, Complex.ofReal_one] + rw [(Finset.sum_erase_add (s := Finset.univ) (a := x0) + (f := fun x : ULift (Fin (M + 1)) => + (↑M + 1 : ℂ)⁻¹ * (if x = x0 then ρ else τr).m i j) (by simp)).symm] + have hrest : + Finset.sum (Finset.erase Finset.univ x0) + (fun x : ULift (Fin (M + 1)) => + (↑M + 1 : ℂ)⁻¹ * (if x = x0 then ρ else τr).m i j) + = + M * ((↑M + 1 : ℂ)⁻¹ * τr.m i j) := by + trans Finset.sum (Finset.erase Finset.univ x0) + (fun _ : ULift (Fin (M + 1)) => (↑M + 1 : ℂ)⁻¹ * τr.m i j) + · exact Finset.sum_congr rfl fun x hx => by simp [(Finset.mem_erase.mp hx).1] + · simp [x0] + rw [hrest] + dsimp [τr] + simp [tauOfLE, MState.m] + field_simp [show (M : ℂ) ≠ 0 by exact_mod_cast Nat.ne_of_gt hM_pos, + show (M + 1 : ℂ) ≠ 0 by exact_mod_cast Nat.succ_ne_zero M] + simp only [← HermitianMat.mat_apply, HermitianMat.mat_sub, HermitianMat.mat_smul, + Matrix.sub_apply, Matrix.smul_apply] + rw [Complex.real_smul] + norm_num + +private theorem integer_bound_aux (N : ℕ) (ρ σ : MState d) + (h : ρ.M ≤ ((N + 1 : ℝ) • σ.M)) : + f ρ σ.M ≤ ENNReal.ofReal (Real.log (N + 1)) := by + cases N with + | zero => + have hEq : ρ = σ := MState.ext <| (eq_of_sub_eq_zero (HermitianMat.ext <| + (Matrix.PosSemidef.trace_eq_zero_iff (HermitianMat.zero_le_iff.mp <| + show 0 ≤ σ.M - ρ.M by simpa using sub_nonneg.mpr (show ρ.M ≤ σ.M by + simpa using h))).1 <| + (HermitianMat.trace_eq_zero_iff (A := σ.M - ρ.M)).1 + (by simp [σ.tr, ρ.tr]))).symm + subst hEq + simp + | succ N => + let κ := ULift (Fin (N + 2)) + let x0 : κ := ⟨0⟩ + let τrest := tauOfLE (d := d) (N + 1) (Nat.succ_pos _) ρ σ h + let τ : κ → MState d := fun i => if i = x0 then ρ else τrest + let Λ : CPTPMap κ d := cqPrepareCPTP (d := d) τ + have hconst : Λ (MState.ofClassical (.constant x0)) = ρ := by + apply MState.ext_m + change MatrixMap.of_choi_matrix (cqPrepareChoi (d := d) τ) + (MState.ofClassical (.constant x0)).m = ρ.m + rw [cqPrepare_apply_ofClassical (d := d) τ (.constant x0)] + ext i j + rw [Finset.sum_eq_single x0] + · simp [τ, ProbDistribution.constant_eq] + · intro y _ hyx + simp [ProbDistribution.constant_eq, hyx, eq_comm] + · simp + have huniform : Λ (MState.uniform : MState κ) = σ := by + simpa [Λ, κ, τ, τrest] using + cqPrepareCPTP_uniform_tauOfLE (d := d) (N + 1) (Nat.succ_pos _) ρ σ h + calc + f ρ σ.M = + f (Λ (MState.ofClassical (.constant x0))) + ((Λ (MState.uniform : MState κ)).M) := by + rw [hconst, huniform] + _ ≤ f (MState.ofClassical (.constant x0)) (MState.uniform : MState κ).M := DPI _ _ Λ + _ = ENNReal.ofReal (Real.log (N + 2)) := by + simpa [κ, ENNReal.some_eq_coe, + ENNReal.ofReal_eq_coe_nnreal (Real.log_nonneg + (by + have := (Nat.cast_nonneg N : (0 : ℝ) ≤ N) + linarith : (1 : ℝ) ≤ (N + 2 : ℝ)))] using + (RelEntropy.normalized (f := f) (d := κ) x0) + _ = ENNReal.ofReal (Real.log (↑(N + 1) + 1)) := by + norm_num [Nat.cast_add, add_assoc, add_comm, add_left_comm] + +private def dyadicStatePow (ρ : MState d) : ∀ n, MState (DyadicPow d n) + | 0 => ρ + | n + 1 => dyadicStatePow ρ n ⊗ᴹ dyadicStatePow ρ n + +private theorem dyadicStatePow_ofClassical (dist : ProbDistribution d) : + ∀ n, dyadicStatePow (MState.ofClassical dist) n = + MState.ofClassical (dyadicProbPow dist n) := by + intro n + induction n with + | zero => rfl + | succ n ih => + rw [dyadicStatePow, ih] + change _ = MState.ofClassical (ProbDistribution.prod _ _) + ext i j + simp [MState.prod, MState.ofClassical, ProbDistribution.prod, + HermitianMat.kronecker_diagonal] + +private theorem hellingerOverlap_uliftCoin (p q : Prob) : + hellingerOverlap (uliftCoin p) (uliftCoin q) = + Real.sqrt ((p : ℝ) * (q : ℝ)) + + Real.sqrt ((1 - (p : ℝ)) * (1 - (q : ℝ))) := by + change (∑ x : ULift (Fin 2), + Real.sqrt (((ProbDistribution.coin p) x.down : ℝ) * + ((ProbDistribution.coin q) x.down : ℝ))) = _ + simpa [Fin.sum_univ_two] using + (Equiv.sum_comp (Equiv.ulift : ULift (Fin 2) ≃ Fin 2) + fun y : Fin 2 => Real.sqrt (((ProbDistribution.coin p) y : ℝ) * + ((ProbDistribution.coin q) y : ℝ))) + +private theorem exists_likelihood_indicator_effect + {κ : Type u} [Fintype κ] [DecidableEq κ] (P Q : ProbDistribution κ) (s r : Prob) + (hoverlap_s : hellingerOverlap P Q ≤ (s : ℝ)) + (hoverlap_r : hellingerOverlap P Q ≤ 1 - (r : ℝ)) : + ∃ T : HermitianMat κ ℂ, (0 ≤ T ∧ T ≤ 1) ∧ + ∃ α β : Prob, + (MState.ofClassical P).exp_val T = α ∧ + (MState.ofClassical Q).exp_val T = β ∧ + (α : ℝ) ≤ s ∧ (r : ℝ) ≤ β := by + classical + let A : Set κ := {x | (P x : ℝ) ≤ Q x} + let T : HermitianMat κ ℂ := classicalIndicatorEffect A + have hT : 0 ≤ T ∧ T ≤ 1 := by + refine ⟨?_, ?_⟩ + · rw [HermitianMat.zero_le_iff] + simp [T, classicalIndicatorEffect, HermitianMat.diagonal_mat, Matrix.posSemidef_diagonal_iff] + exact fun i => by by_cases hi : i ∈ A <;> simp [hi] + · rw [← sub_nonneg] + rw [show T = HermitianMat.diagonal ℂ fun x => if x ∈ A then (1 : ℝ) else 0 from rfl, + ← HermitianMat.diagonal_one (𝕜 := ℂ), + ← HermitianMat.diagonal_sub, HermitianMat.zero_le_iff, HermitianMat.diagonal_mat, + Matrix.posSemidef_diagonal_iff] + exact fun i => by by_cases hi : i ∈ A <;> simp [hi] + refine ⟨T, hT, + ⟨(MState.ofClassical P).exp_val T, (MState.ofClassical P).exp_val_prob hT⟩, + ⟨(MState.ofClassical Q).exp_val T, (MState.ofClassical Q).exp_val_prob hT⟩, + rfl, rfl, ?_, ?_⟩ + · change (MState.ofClassical P).exp_val T ≤ (s : ℝ) + rw [ofClassical_exp_val_indicator] + exact (show ∑ x, (if (P x : ℝ) ≤ Q x then (P x : ℝ) else 0) ≤ + hellingerOverlap P Q by + rw [hellingerOverlap] + refine Finset.sum_le_sum ?_ + intro x _ + by_cases hx : (P x : ℝ) ≤ Q x + · simpa [hx] using Real.le_sqrt (P x).2.1 (mul_nonneg (P x).2.1 (Q x).2.1) |>.2 + (by simpa [pow_two] using mul_le_mul_of_nonneg_left hx (P x).2.1) + · simpa [hx] using Real.sqrt_nonneg ((P x : ℝ) * (Q x : ℝ))).trans hoverlap_s + · change (r : ℝ) ≤ (MState.ofClassical Q).exp_val T + rw [ofClassical_exp_val_indicator] + change (r : ℝ) ≤ ∑ x, (if (P x : ℝ) ≤ Q x then (Q x : ℝ) else 0) + have hcompl : ∑ x, (if (P x : ℝ) ≤ Q x then 0 else (Q x : ℝ)) ≤ + hellingerOverlap P Q := by + rw [hellingerOverlap] + refine Finset.sum_le_sum ?_ + intro x _ + by_cases hx : (P x : ℝ) ≤ Q x + · simpa [hx] using Real.sqrt_nonneg ((P x : ℝ) * (Q x : ℝ)) + · rw [mul_comm] + simpa [hx] using Real.le_sqrt (Q x).2.1 (mul_nonneg (Q x).2.1 (P x).2.1) |>.2 + (by simpa [pow_two] using + mul_le_mul_of_nonneg_left (le_of_not_ge hx) (Q x).2.1) + have htotal' : + (∑ x, (if (P x : ℝ) ≤ Q x then 0 else (Q x : ℝ))) + + (∑ x, (if (P x : ℝ) ≤ Q x then (Q x : ℝ) else 0)) = + 1 := by + rw [← Finset.sum_add_distrib] + convert Q.normalized using 1 + exact Finset.sum_congr rfl fun x _ => by by_cases hx : (P x : ℝ) ≤ Q x <;> simp [hx] + linarith + +private theorem exists_dyadic_binary_effect_le_ge + (p q s r : Prob) (hpq : (p : ℝ) < q) + (hs_pos : 0 < (s : ℝ)) (hr_lt_one : (r : ℝ) < 1) : + ∃ (n : ℕ) (T : HermitianMat (DyadicPow (ULift.{u} (Fin 2)) n) ℂ), + (0 ≤ T ∧ T ≤ 1) ∧ ∃ α β : Prob, + (dyadicStatePow (MState.ofClassical (uliftCoin p)) n).exp_val T = α ∧ + (dyadicStatePow (MState.ofClassical (uliftCoin q)) n).exp_val T = β ∧ + (α : ℝ) ≤ s ∧ (r : ℝ) ≤ β := by + let ε : ℝ := (s : ℝ) ⊓ (1 - (r : ℝ)) + have ha1 : hellingerOverlap (uliftCoin p) (uliftCoin q) < 1 := by + rw [hellingerOverlap_uliftCoin] + simpa [hellingerOverlap_coin] using hellingerOverlap_coin_lt_one p q hpq + obtain ⟨n, hn'⟩ := exists_pow_lt_of_lt_one + (show 0 < ε by simpa [ε] using lt_inf_iff.mpr ⟨hs_pos, sub_pos.mpr hr_lt_one⟩) ha1 + have hn : (hellingerOverlap (uliftCoin p) (uliftCoin q)) ^ (2 ^ n : ℕ) < ε := lt_of_le_of_lt + (pow_le_pow_of_le_one (by rw [hellingerOverlap_uliftCoin]; positivity) ha1.le + (Nat.lt_two_pow_self (n := n)).le) hn' + have hoverlap_lt : + hellingerOverlap (dyadicProbPow (uliftCoin p) n) (dyadicProbPow (uliftCoin q) n) < ε := by + rw [hellingerOverlap_dyadicProbPow] + exact hn + obtain ⟨T, hT, α, β, hpT, hqT, hαs, hrβ⟩ := + exists_likelihood_indicator_effect + (dyadicProbPow (uliftCoin p) n) (dyadicProbPow (uliftCoin q) n) s r + (hoverlap_lt.le.trans inf_le_left) (hoverlap_lt.le.trans inf_le_right) + exact ⟨n, T, hT, α, β, by simpa [dyadicStatePow_ofClassical] using hpT, + by simpa [dyadicStatePow_ofClassical] using hqT, hαs, hrβ⟩ + +private def dyadicCPTPMapPow {e : Type u} [Fintype e] [DecidableEq e] + (Λ : CPTPMap d e) : ∀ n, CPTPMap (DyadicPow d n) (DyadicPow e n) + | 0 => Λ + | n + 1 => dyadicCPTPMapPow Λ n ⊗ᶜᵖ dyadicCPTPMapPow Λ n + +/-- Universe-lifted two-outcome POVM associated to an effect `0 ≤ T ≤ 1`. -/ +private def binaryPOVMOfEffectULift (T : HermitianMat d ℂ) (hT : 0 ≤ T ∧ T ≤ 1) : + POVM (ULift (Fin 2)) d where + mats i := if i = ULift.up (0 : Fin 2) then T else 1 - T + nonneg i := by + split + · exact hT.1 + · exact HermitianMat.zero_le_iff.mpr hT.2 + normalized := by + have hsum : + (∑ i : ULift (Fin 2), if i = ULift.up (0 : Fin 2) then T else 1 - T) = + ∑ i : Fin 2, if ULift.up i = ULift.up (0 : Fin 2) then T else 1 - T := by + refine Fintype.sum_equiv Equiv.ulift + (fun i : ULift (Fin 2) => if i = ULift.up (0 : Fin 2) then T else 1 - T) + (fun i : Fin 2 => if ULift.up i = ULift.up (0 : Fin 2) then T else 1 - T) ?_ + rintro ⟨x⟩ + rfl + rw [hsum] + simp [Fin.sum_univ_two] + +/-- Measuring a lifted binary effect and discarding the post-measurement state gives a lifted coin. -/ +private theorem binaryPOVMOfEffectULift_measureDiscard_apply + (T : HermitianMat d ℂ) (hT : 0 ≤ T ∧ T ≤ 1) (ρ : MState d) : + (binaryPOVMOfEffectULift T hT).measureDiscard ρ = + MState.ofClassical (uliftCoin ⟨ρ.exp_val T, ρ.exp_val_prob hT⟩) := by + rw [POVM.measureDiscard_apply] + congr 1 + let p : Prob := ⟨ρ.exp_val T, ρ.exp_val_prob hT⟩ + ext i + rcases i with ⟨i⟩ + fin_cases i + · let z : ULift.{u} (Fin 2) := ULift.up (0 : Fin 2) + change inner ℝ T ρ.M = ((uliftCoin p) z : ℝ) + simp [z, p, uliftCoin, ProbDistribution.congr_apply, MState.exp_val, HermitianMat.inner_comm] + · let o : ULift.{u} (Fin 2) := ULift.up (1 : Fin 2) + change inner ℝ (1 - T) ρ.M = ((uliftCoin p) o : ℝ) + simp [o, p, uliftCoin, ProbDistribution.congr_apply, Prob.coe_one_minus, + MState.exp_val, HermitianMat.inner_comm, inner_sub_right, HermitianMat.inner_one, ρ.tr] + +private theorem dyadicStatePow_relEntropy (ρ σ : MState d) : + ∀ n, f (dyadicStatePow ρ n) (dyadicStatePow σ n).M = ((2 ^ n : ℕ) : ENNReal) * f ρ σ := by + intro n + induction n with + | zero => simp [dyadicStatePow]; rfl + | succ n ih => + show f (dyadicStatePow ρ n ⊗ᴹ dyadicStatePow ρ n) + ↑(dyadicStatePow σ n ⊗ᴹ dyadicStatePow σ n) = _ + rw [RelEntropy.of_kron (f := f), ih] + rw [← mul_add, ← two_mul, pow_succ, Nat.cast_mul] + ring + +private theorem exists_binary_measurement_of_ne (ρ σ : MState d) (hne : ρ ≠ σ) : + ∃ p q : Prob, (p : ℝ) < (q : ℝ) ∧ + ∃ Λ : CPTPMap d (ULift.{u} (Fin 2)), + Λ ρ = MState.ofClassical (uliftCoin p) ∧ + Λ σ = MState.ofClassical (uliftCoin q) := by + obtain ⟨T, hT, hT_ne⟩ := exists_effect_exp_val_ne_of_ne ρ σ hne + let p : Prob := ⟨ρ.exp_val T, ρ.exp_val_prob hT⟩ + let q : Prob := ⟨σ.exp_val T, σ.exp_val_prob hT⟩ + by_cases hpq : (p : ℝ) < q + · exact ⟨p, q, hpq, (binaryPOVMOfEffectULift T hT).measureDiscard, + by rw [binaryPOVMOfEffectULift_measureDiscard_apply], + by rw [binaryPOVMOfEffectULift_measureDiscard_apply]⟩ + · let T' : HermitianMat d ℂ := 1 - T + have hT' : 0 ≤ T' ∧ T' ≤ 1 := by + refine ⟨by dsimp [T']; exact HermitianMat.zero_le_iff.mpr hT.2, ?_⟩ + dsimp [T'] + rw [sub_le_iff_le_add] + simpa using hT.1 + have hpq' : ((1 - p : Prob) : ℝ) < (1 - q : Prob) := by + rw [Prob.coe_one_minus, Prob.coe_one_minus] + linarith [lt_of_le_of_ne (le_of_not_gt hpq) (fun heq => hT_ne heq.symm)] + refine ⟨1 - p, 1 - q, hpq', (binaryPOVMOfEffectULift T' hT').measureDiscard, ?_, ?_⟩ <;> + rw [binaryPOVMOfEffectULift_measureDiscard_apply] <;> + congr 2 <;> + apply Subtype.ext <;> + simp [T', p, q, MState.exp_val_sub, MState.exp_val_one, Prob.coe_one_minus] + +private theorem exists_binary_postprocess {α β s r : Prob} + (hαs : (α : ℝ) ≤ s) (hsr : (s : ℝ) < r) (hrβ : (r : ℝ) ≤ β) : + ∃ a b : Prob, Prob.mix α a b = s ∧ Prob.mix β a b = r := by + let A : ℝ := α + let B : ℝ := β + let S : ℝ := s + let R : ℝ := r + have hAB : A < B := by dsimp [A, B, S, R] at *; linarith + let k : ℝ := (R - S) / (B - A) + have hk_nonneg : 0 ≤ k := by + dsimp [k] + exact div_nonneg (sub_nonneg.mpr (by dsimp [S, R]; exact hsr.le)) + (sub_nonneg.mpr hAB.le) + have hk_le_one : k ≤ 1 := by + dsimp [k] + rw [div_le_one (sub_pos.mpr hAB)] + dsimp [A, B, S, R] at * + linarith + let bR : ℝ := S - A * k + let aR : ℝ := bR + k + have hbR_nonneg : 0 ≤ bR := by + dsimp [bR, A, S] at * + linarith [mul_le_mul_of_nonneg_left hk_le_one α.2.1] + have hbR_le_one : bR ≤ 1 := by + dsimp [bR, S] + nlinarith [s.2.2, α.2.1, hk_nonneg] + have haR_nonneg : 0 ≤ aR := by dsimp [aR]; positivity + have haR_le_one : aR ≤ 1 := by + have hden_pos : 0 < B - A := sub_pos.mpr hAB + have hmain : + S * (B - A) + (1 - A) * (R - S) ≤ 1 * (B - A) := by + nlinarith [ + mul_le_mul_of_nonneg_right (show R ≤ B by dsimp [R, B] at hrβ ⊢; exact hrβ) + (show 0 ≤ 1 - A by dsimp [A]; linarith [α.2.2]), + mul_le_mul_of_nonpos_right (show A ≤ S by dsimp [A, S] at hαs ⊢; exact hαs) + (show B - 1 ≤ 0 by dsimp [B]; linarith [β.2.2])] + rw [show aR = (S * (B - A) + (1 - A) * (R - S)) / (B - A) by + dsimp [aR, bR, k] + field_simp [hden_pos.ne'] + ring, div_le_one hden_pos] + simpa using hmain + let a : Prob := ⟨aR, haR_nonneg, haR_le_one⟩ + let b : Prob := ⟨bR, hbR_nonneg, hbR_le_one⟩ + refine ⟨a, b, ?_, ?_⟩ + all_goals + ext + simp [Prob.mix, Mixable.mix, Mixable.mix_ab, Prob.coe_one_minus, a, b, aR, bR, k, A, B, S, R] + · + ring + · + field_simp [show (↑β : ℝ) - ↑α ≠ 0 by dsimp [A, B] at hAB; linarith] + ring + +section nontrivial +variable [RelEntropy.Nontrivial f] + +/-- From Tomamichel nontriviality, extract a strictly positive binary classical pair with +full-support states. This is the finite binary witness used in the proof of `faithful`. -/ +private theorem exists_positive_binary_pair : + ∃ p q : Prob, 0 < (p : ℝ) ∧ (p : ℝ) < q ∧ (q : ℝ) < 1 ∧ + (MState.ofClassical (uliftCoin.{u} p)).M.support = ⊤ ∧ + (MState.ofClassical (uliftCoin.{u} q)).M.support = ⊤ ∧ + 0 < f (MState.ofClassical (uliftCoin.{u} p)) + (MState.ofClassical (uliftCoin.{u} q)).M := by + obtain ⟨s, t, hs0, -, ht0, -, hs_order, hsSupport, htSupport, hpos⟩ : + ∃ s t : Prob, + 0 < (s : ℝ) ∧ (s : ℝ) < 1 / 2 ∧ + 0 < (t : ℝ) ∧ (t : ℝ) < 1 / 2 ∧ + (s : ℝ) < ((1 - t : Prob) : ℝ) ∧ + (MState.ofClassical (uliftCoin s)).M.support = ⊤ ∧ + (MState.ofClassical (uliftCoin (1 - t))).M.support = ⊤ ∧ + 0 < f (MState.ofClassical (uliftCoin s)) + (MState.ofClassical (uliftCoin (1 - t))).M := by + obtain ⟨d, instFintype, instDecidableEq, γ, ω, hγ, hω, hpos⟩ := + RelEntropy.Nontrivial.nontrivial (f := f) + letI : Fintype d := instFintype + letI : DecidableEq d := instDecidableEq + obtain ⟨s, t, hs0, hslt, ht0, htlt, hleft, hright⟩ : + ∃ s t : Prob, 0 < (s : ℝ) ∧ (s : ℝ) < 1 / 2 ∧ + 0 < (t : ℝ) ∧ (t : ℝ) < 1 / 2 ∧ + (t : ℝ) • γ.M ≤ (1 - (s : ℝ)) • ω.M ∧ + (s : ℝ) • ω.M ≤ (1 - (t : ℝ)) • γ.M := by + obtain ⟨Nγω, hNγω_pos, hγω⟩ := exists_le_nat_smul_of_fullSupport γ ω hω + obtain ⟨Nωγ, _, hωγ⟩ := exists_le_nat_smul_of_fullSupport ω γ hγ + let K : ℕ := Nat.max Nγω Nωγ + let a : ℝ := 1 / (K + 2 : ℝ) + have hden_pos : (0 : ℝ) < K + 2 := by positivity + have ha_pos : 0 < a := by dsimp [a]; positivity + have ha_lt_half : a < 1 / 2 := by + dsimp [a] + rw [div_lt_iff₀ hden_pos] + nlinarith [show (1 : ℝ) ≤ K by + exact_mod_cast le_trans hNγω_pos (le_max_left Nγω Nωγ)] + have hscale {N : ℕ} (hNK : N ≤ K) : a * (N + 1 : ℝ) ≤ 1 - a := by + dsimp [a] + rw [div_mul_eq_mul_div, one_sub_div hden_pos.ne', + div_le_div_iff_of_pos_right hden_pos] + nlinarith [show (N + 1 : ℝ) ≤ K + 1 by exact_mod_cast Nat.succ_le_succ hNK] + let p : Prob := ⟨a, ha_pos.le, by linarith [ha_lt_half]⟩ + refine ⟨p, p, by simpa [p] using ha_pos, by simpa [p] using ha_lt_half, + by simpa [p] using ha_pos, by simpa [p] using ha_lt_half, ?_, ?_⟩ + · simpa [p] using calc + a • γ.M ≤ a • ((Nγω + 1 : ℝ) • ω.M) := + smul_le_smul_of_nonneg_left hγω ha_pos.le + _ = (a * (Nγω + 1 : ℝ)) • ω.M := by rw [smul_smul] + _ ≤ (1 - a) • ω.M := smul_le_smul_of_nonneg_right + (hscale (le_max_left Nγω Nωγ)) ω.nonneg + · simpa [p] using calc + a • ω.M ≤ a • ((Nωγ + 1 : ℝ) • γ.M) := + smul_le_smul_of_nonneg_left hωγ ha_pos.le + _ = (a * (Nωγ + 1 : ℝ)) • γ.M := by rw [smul_smul] + _ ≤ (1 - a) • γ.M := smul_le_smul_of_nonneg_right + (hscale (le_max_right Nγω Nωγ)) γ.nonneg + have hden : 0 < 1 - (s : ℝ) - (t : ℝ) := by linarith + let τ : ULift.{u} (Fin 2) → MState d := fun i => + if i = ULift.up (0 : Fin 2) then + binaryPrepOne γ ω (s : ℝ) (t : ℝ) hden hleft + else + binaryPrepZero γ ω (s : ℝ) (t : ℝ) hden hright + let Λ : CPTPMap (ULift.{u} (Fin 2)) d := + CPTPMap.CPTP_of_choi_PSD_Tr + (M := cqPrepareChoi (d := d) τ) + (cqPrepareChoi_psd (d := d) τ) + (cqPrepareChoi_traceLeft (d := d) τ) + have hdenC : (1 - ((s : ℝ) : ℂ) - ((t : ℝ) : ℂ)) ≠ 0 := by exact_mod_cast hden.ne' + have hγprep : Λ (MState.ofClassical (uliftCoin s)) = γ := by + apply MState.ext_m + change MatrixMap.of_choi_matrix (cqPrepareChoi (d := d) τ) + (MState.ofClassical (uliftCoin s)).m = γ.m + rw [cqPrepare_apply_uliftCoin, Prob.coe_one_minus] + ext i j + simp [τ, binaryPrepOne, binaryPrepZero, MState.m, Matrix.add_apply, Matrix.sub_apply, + Matrix.smul_apply, -MState.mat_M] + field_simp [hdenC] + ring + have hωprep : Λ (MState.ofClassical (uliftCoin (1 - t))) = ω := by + apply MState.ext_m + change MatrixMap.of_choi_matrix (cqPrepareChoi (d := d) τ) + (MState.ofClassical (uliftCoin (1 - t))).m = ω.m + rw [cqPrepare_apply_uliftCoin, Prob.coe_one_minus, Prob.coe_one_minus] + ext i j + simp [τ, binaryPrepOne, binaryPrepZero, MState.m, Matrix.add_apply, Matrix.sub_apply, + Matrix.smul_apply, -MState.mat_M] + field_simp [hdenC] + ring + refine ⟨s, t, hs0, hslt, ht0, htlt, by rw [Prob.coe_one_minus]; linarith, + uliftCoin_support_top s hs0 (by linarith), + uliftCoin_support_top (1 - t) (by rw [Prob.coe_one_minus]; linarith) + (by rw [Prob.coe_one_minus]; linarith), ?_⟩ + exact lt_of_lt_of_le hpos <| by + simpa [hγprep, hωprep] using DPI (f := f) (MState.ofClassical (uliftCoin s)) + (MState.ofClassical (uliftCoin (1 - t))) Λ + exact ⟨s, 1 - t, hs0, hs_order, by rw [Prob.coe_one_minus]; linarith, + hsSupport, htSupport, hpos⟩ + +/-- A nontrivial relative entropy is **faithful**: it can distinguish when two states are equal. + +The proof (Tomamichel §5) goes by building a binary measurement that separates `ρ` from `σ`, +using DPI to reduce to a classical `Fin 2` distribution, then amplifying with `of_kron` until the +`Nontrivial` axiom forces a strictly positive value. The tensor-power separation step is formalized +via the finite classical likelihood test in `exists_dyadic_binary_effect_le_ge`. -/ +theorem faithful (ρ σ : MState d) : f ρ σ = 0 ↔ ρ = σ := by + constructor + · intro hzero + by_contra hne + obtain ⟨p, q, hpq, Λ, hρ, hσ⟩ := exists_binary_measurement_of_ne ρ σ hne + have hzero_binary : ∀ n, + f (dyadicStatePow (MState.ofClassical (uliftCoin p)) n) + (dyadicStatePow (MState.ofClassical (uliftCoin q)) n).M = 0 := by + intro n + induction n with + | zero => + simpa [dyadicStatePow] using + le_antisymm (by simpa [hρ, hσ, hzero] using RelEntropy.DPI (f := f) ρ σ Λ) bot_le + | succ n ih => + simpa [dyadicStatePow, ih] using + RelEntropy.of_kron (f := f) + (dyadicStatePow (MState.ofClassical (uliftCoin p)) n) + (dyadicStatePow (MState.ofClassical (uliftCoin q)) n) + (dyadicStatePow (MState.ofClassical (uliftCoin p)) n) + (dyadicStatePow (MState.ofClassical (uliftCoin q)) n) + obtain ⟨s, r, hs_pos, hsr, hr_lt_one, _, _, hpos⟩ := + exists_positive_binary_pair (f := f) + obtain ⟨n, T, hT, α, β, hpT, hqT, hαs, hrβ⟩ := + exists_dyadic_binary_effect_le_ge p q s r hpq hs_pos hr_lt_one + suffices 0 < f (dyadicStatePow (MState.ofClassical (uliftCoin p)) n) + (dyadicStatePow (MState.ofClassical (uliftCoin q)) n).M by + simp [hzero_binary n] at this + obtain ⟨a, b, hsmix, hrmix⟩ := exists_binary_postprocess hαs hsr hrβ + let Μ : CPTPMap (DyadicPow (ULift.{u} (Fin 2)) n) (ULift (Fin 2)) := + (binaryPOVMOfEffectULift T hT).measureDiscard + let Λ' : CPTPMap (DyadicPow (ULift.{u} (Fin 2)) n) (ULift (Fin 2)) := + (binaryClassicalPostprocess a b) ∘ₘ Μ + have hOut (x z y : Prob) + (hz : (dyadicStatePow (MState.ofClassical (uliftCoin x)) n).exp_val T = z) + (hy : Prob.mix z a b = y) : + Λ' (dyadicStatePow (MState.ofClassical (uliftCoin x)) n) = + MState.ofClassical (uliftCoin y) := by + have hΜ : Μ (dyadicStatePow (MState.ofClassical (uliftCoin x)) n) = + MState.ofClassical (uliftCoin z) := by + rw [binaryPOVMOfEffectULift_measureDiscard_apply] + exact congrArg (fun x => MState.ofClassical (uliftCoin x)) (Subtype.ext hz) + simpa [Λ', CPTPMap.compose_eq, hΜ, binaryClassicalPostprocess_apply] using + congrArg (fun x => MState.ofClassical (uliftCoin x)) hy + exact lt_of_lt_of_le hpos <| by + simpa [hOut p α s hpT hsmix, hOut q β r hqT hrmix] using DPI (f := f) + (dyadicStatePow (MState.ofClassical (uliftCoin p)) n) + (dyadicStatePow (MState.ofClassical (uliftCoin q)) n) Λ' + · rintro rfl simp - sorry - · push_neg at h - simp [h] + +/-- In every system with at least two classical points, a nontrivial relative entropy has a +strictly positive value on some pair of full-support states. -/ +theorem exists_fullSupport_positive_of_two_le_card + (d : Type u) [Fintype d] [DecidableEq d] (hd : 2 ≤ Fintype.card d) : + ∃ (ρ σ : MState d), ρ.M.support = ⊤ ∧ σ.M.support = ⊤ ∧ 0 < f ρ σ := by + haveI : Nonempty d := Fintype.card_pos_iff.mp (lt_of_lt_of_le (by norm_num) hd) + let i : d := Classical.arbitrary d + let p : Prob := ⟨1 / 2, by norm_num⟩ + let ρ : MState d := p [MState.ofClassical (.constant i) ↔ MState.uniform] + refine ⟨ρ, MState.uniform, ?_, ?_, ?_⟩ + · haveI : ρ.M.NonSingular := HermitianMat.nonSingular_of_posDef <| by + dsimp [ρ] + exact MState.PosDef_mix_of_ne_one (hσ₂ := MState.uniform_posDef) p + (by dsimp [p]; norm_num [Prob.ext_iff]) + exact HermitianMat.nonSingular_support_top + · haveI : (MState.uniform : MState d).M.NonSingular := + HermitianMat.nonSingular_of_posDef MState.uniform_posDef + exact HermitianMat.nonSingular_support_top + · refine bot_lt_iff_ne_bot.mpr ((faithful (f := f) ρ MState.uniform).not.mpr ?_) + intro hρσ + have hmat := congrArg (fun τ : MState d => τ.M.mat) hρσ + simp [ρ, p, Mixable.mix, Mixable.mix_ab, MState.instMixable, + MState.uniform, MState.ofClassical, ProbDistribution.constant_eq, + ProbDistribution.uniform_def, HermitianMat.diagonal, Mixable.to_U] at hmat + have hdiag_re := congrArg Complex.re (congrFun (congrFun hmat i) i) + simp [Matrix.add_apply] at hdiag_re + norm_num at hdiag_re + nlinarith [inv_lt_one_of_one_lt₀ + (by exact_mod_cast (lt_of_lt_of_le one_lt_two hd) : (1 : ℝ) < Fintype.card d)] + +end nontrivial + + +/-- If `ρ ≤ exp x • σ`, then every axiomatized relative entropy is bounded by `x`. -/ +theorem le_of_le_exp (ρ σ : MState d) {x : ℝ} + (hx : 0 ≤ x) (h : ρ.M ≤ Real.exp x • σ.M) : + f ρ σ.M ≤ ENNReal.ofReal x := by + have hfin : f ρ σ.M ≠ ∞ := + ne_top_of_le_ne_top ENNReal.ofReal_ne_top <| + integer_bound_aux (f := f) (N := Nat.ceil (Real.exp x)) ρ σ <| by + exact h.trans <| smul_le_smul_of_nonneg_right + ((Nat.le_ceil _).trans (by norm_num)) σ.nonneg + by_contra hfx + let δ : ℝ := (f ρ σ.M).toReal - x + have hδ : 0 < δ := by + dsimp [δ]; linarith [(ENNReal.ofReal_lt_iff_lt_toReal hx hfin).1 (lt_of_not_ge hfx)] + let n : ℕ := Nat.ceil (Real.log 3 / δ) + 1 + have hgap : Real.log 3 < (((2 ^ n : ℕ) : ℝ)) * δ := by + exact (div_lt_iff₀ hδ).mp <| lt_of_lt_of_le + (show Real.log 3 / δ < (n : ℝ) by + dsimp [n] + exact lt_of_le_of_lt (Nat.le_ceil (Real.log 3 / δ)) + (by exact_mod_cast Nat.lt_succ_self (Nat.ceil (Real.log 3 / δ)))) + (by exact_mod_cast ((Nat.lt_two_pow_self : n < 2 ^ n).le) : (n : ℝ) ≤ (2 ^ n : ℕ)) + let y : ℝ := (((2 ^ n : ℕ) : ℝ)) * x + have hy_nonneg : 0 ≤ y := by dsimp [y]; positivity + have hpow_le : ∀ m, (dyadicStatePow ρ m).M ≤ + Real.exp ((((2 ^ m : ℕ) : ℝ)) * x) • (dyadicStatePow σ m).M := by + intro m + induction m with + | zero => + simpa [dyadicStatePow] using h + | succ m ih => + have hσ_nonneg : + 0 ≤ Real.exp ((((2 ^ m : ℕ) : ℝ)) * x) • (dyadicStatePow σ m).M := + smul_nonneg (by positivity) (dyadicStatePow σ m).nonneg + have hpow : + ((((2 ^ (m + 1) : ℕ) : ℝ)) * x) = + ((((2 ^ m : ℕ) : ℝ)) * x) + ((((2 ^ m : ℕ) : ℝ)) * x) := by + rw [pow_succ, Nat.cast_mul] + ring + have hunfold : (dyadicStatePow ρ (m + 1)).M + = (dyadicStatePow ρ m).M ⊗ₖ (dyadicStatePow ρ m).M := rfl + have hrhs : Real.exp (((((2 ^ m : ℕ) : ℝ)) * x) + ((((2 ^ m : ℕ) : ℝ)) * x)) • + (dyadicStatePow σ (m + 1)).M + = (Real.exp ((((2 ^ m : ℕ) : ℝ)) * x) • (dyadicStatePow σ m).M) ⊗ₖ + (Real.exp ((((2 ^ m : ℕ) : ℝ)) * x) • (dyadicStatePow σ m).M) := by + have hsk : + (Real.exp ((((2 ^ m : ℕ) : ℝ)) * x) • (dyadicStatePow σ m).M) ⊗ₖ + (Real.exp ((((2 ^ m : ℕ) : ℝ)) * x) • (dyadicStatePow σ m).M) = + (Real.exp ((((2 ^ m : ℕ) : ℝ)) * x) * Real.exp ((((2 ^ m : ℕ) : ℝ)) * x)) • + ((dyadicStatePow σ m).M ⊗ₖ (dyadicStatePow σ m).M) := by + ext1 + simp [Matrix.smul_kronecker, Matrix.kronecker_smul, smul_smul, mul_comm] + simpa [dyadicStatePow, MState.prod, Real.exp_add] using hsk.symm + rw [hunfold, hpow, hrhs] + exact HermitianMat.kronecker_self_mono (dyadicStatePow ρ m).nonneg hσ_nonneg ih + have hpow_bound' : + (((2 ^ n : ℕ) : ENNReal) * f ρ σ.M) ≤ + ENNReal.ofReal (Real.log (Nat.ceil (Real.exp y) + 1)) := by + simpa [dyadicStatePow_relEntropy (f := f) ρ σ n] using + integer_bound_aux (f := f) (N := Nat.ceil (Real.exp y)) + (dyadicStatePow ρ n) (dyadicStatePow σ n) (by + exact (hpow_le n).trans <| smul_le_smul_of_nonneg_right + (by dsimp [y]; exact (Nat.le_ceil _).trans (by norm_num)) + (dyadicStatePow σ n).nonneg) + have hpow_bound_real : + (((2 ^ n : ℕ) : ℝ)) * (f ρ σ.M).toReal ≤ + Real.log (Nat.ceil (Real.exp y) + 1 : ℝ) := by + calc + (((2 ^ n : ℕ) : ℝ)) * (f ρ σ.M).toReal + = ((((2 ^ n : ℕ) : ENNReal) * f ρ σ.M)).toReal := by + rw [ENNReal.toReal_mul, ENNReal.toReal_natCast] + _ ≤ (ENNReal.ofReal (Real.log (Nat.ceil (Real.exp y) + 1 : ℝ))).toReal := + (ENNReal.toReal_le_toReal (ENNReal.mul_ne_top (by simp) hfin) ENNReal.ofReal_ne_top).2 hpow_bound' + _ = Real.log (Nat.ceil (Real.exp y) + 1 : ℝ) := by + rw [ENNReal.toReal_ofReal (Real.log_nonneg (by norm_num))] + have hlog_upper : Real.log (Nat.ceil (Real.exp y) + 1 : ℝ) ≤ y + Real.log 3 := by + calc + Real.log (Nat.ceil (Real.exp y) + 1 : ℝ) ≤ Real.log (3 * Real.exp y) := + Real.log_le_log (by positivity) (by + nlinarith [(Nat.ceil_lt_add_one (Real.exp_nonneg y)).le, + (show (1 : ℝ) ≤ Real.exp y by simpa [Real.one_le_exp_iff] using hy_nonneg)]) + _ = y + Real.log 3 := by + rw [Real.log_mul (by positivity : (3 : ℝ) ≠ 0) (Real.exp_pos y).ne', Real.log_exp] + ring + have hlower : + y + Real.log 3 < (((2 ^ n : ℕ) : ℝ)) * (f ρ σ.M).toReal := by + dsimp [y, δ] at hgap + nlinarith + linarith /-- The relative max-entropy is a lower bound on all relative entropies. -/ -theorem le_max (ρ σ : MState d) : f ρ σ ≤ max ρ σ := by - sorry --Tomamichel, https://www.marcotom.info/files/entropy-masterclass2022.pdf, (1.28) +theorem le_max (ρ σ : MState d) : f ρ σ.M ≤ max ρ σ.M := by + by_cases hx : ∃ x : ℝ, ρ.M ≤ Real.exp x • σ.M + · obtain ⟨x, hx⟩ := hx + let y : ℝ := Max.max x 0 + have hy0 : 0 ≤ y := by simp [y] + have hy : ρ.M ≤ Real.exp y • σ.M := by + exact hx.trans <| smul_le_smul_of_nonneg_right + (Real.exp_le_exp.mpr (show x ≤ y by dsimp [y]; exact le_max_left _ _)) σ.nonneg + have hfin : f ρ σ.M ≠ ∞ := + ne_top_of_le_ne_top ENNReal.ofReal_ne_top (le_of_le_exp (f := f) ρ σ hy0 hy) + exact (ENNReal.toReal_le_toReal hfin + (by simp [max, (show ∃ x : ℝ, ρ.M ≤ Real.exp x • σ.M from ⟨x, hx⟩)])).1 <| by + rw [RelEntropy.toReal_max (ρ := ρ) (σ := σ.M)] + let S : Set ℝ := ((↑) '' {x : ℝ≥0 | ρ.M ≤ Real.exp x • σ.M}) + refine le_csInf ⟨(⟨y, hy0⟩ : ℝ≥0), ⟨⟨y, hy0⟩, hy, rfl⟩⟩ ?_ + intro a ha + rcases ha with ⟨z, hz, rfl⟩ + simpa [ENNReal.toReal_ofReal z.2] using + (ENNReal.toReal_le_toReal hfin ENNReal.ofReal_ne_top).2 + (le_of_le_exp (f := f) ρ σ z.2 hz) + · simp [max, hx] end bounds end RelEntropy +/-- The axioms for a well-behaved quantum entropy: it vanishes on pure states and is additive +under tensor products. Captures the common features of the von Neumann, min-, max-, and α-Renyi +entropies. -/ class Entropy (f : ∀ {d : Type u} [Fintype d] [DecidableEq d], MState d → ℝ≥0) where /-- The entropy of a pure state is zero -/ of_const {d : Type u} [Fintype d] [DecidableEq d] (ψ : Ket d) : f (.pure ψ) = 0 /-- Entropy is additive under tensor products -/ of_kron {d₁ d₂ : Type u} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] : - ∀ (ρ : MState d₁) (σ : MState d₂), f (ρ ⊗ σ) = f ρ + f σ + ∀ (ρ : MState d₁) (σ : MState d₂), f (ρ ⊗ᴹ σ) = f ρ + f σ -- /-- Entropy is convex. TODO def? Or do we even need this? -/ -- convex : True := by trivial diff --git a/QuantumInfo/Finite/AxiomatizedEntropy/Renyi.lean b/QuantumInfo/Finite/AxiomatizedEntropy/Renyi.lean index b59e67b63..a421060e1 100644 --- a/QuantumInfo/Finite/AxiomatizedEntropy/Renyi.lean +++ b/QuantumInfo/Finite/AxiomatizedEntropy/Renyi.lean @@ -5,37 +5,82 @@ Authors: Alex Meiburg -/ module -public import QuantumInfo.Finite.Entropy.Defs +public import QuantumInfo.Finite.AxiomatizedEntropy.Defs +public import QuantumInfo.Finite.Entropy.DPI +public import QuantumInfo.Finite.Entanglement /-! # Quantum Relative Entropy and α-Renyi Entropy -/ @[expose] public section + variable {d : Type*} [Fintype d] [DecidableEq d] -/-- The quantum relative entropy S(ρ‖σ) = Tr[ρ (log ρ - log σ)]. -/ +open scoped RealInnerProductSpace + +namespace AxiomatizedEntropy + +/-- A conservative wrapper around the actual quantum relative entropy. On normalized PSD inputs +it agrees with `_root_.qRelativeEnt`; away from the state space we leave the value at `0`. -/ @[irreducible] noncomputable def qRelativeEnt (ρ : MState d) (σ : HermitianMat d ℂ) : ENNReal := - open Classical in (if σ.ker ≤ ρ.M.ker then - some ⟨ρ.exp_val (HermitianMat.log ρ - HermitianMat.log σ), - /- Quantum relative entropy is nonnegative. This can be proved by an application of - Klein's inequality. -/ - sorry⟩ + open Classical in + if hσ : σ.trace = 1 ∧ 0 ≤ σ then + let σ' : MState d := { M := σ, nonneg := hσ.2, tr := hσ.1 } + _root_.qRelativeEnt ρ σ' else - ⊤) + 0 -notation "𝐃(" ρ "‖" σ ")" => qRelativeEnt ρ σ +@[simp] +theorem qRelativeEnt_state (ρ σ : MState d) : + qRelativeEnt ρ (σ : HermitianMat d ℂ) = _root_.qRelativeEnt ρ σ := by + rw [qRelativeEnt, dif_pos ⟨σ.tr, σ.nonneg⟩] -instance : RelEntropy qRelativeEnt where - DPI := sorry - of_kron := sorry - normalized := sorry +private lemma uniform_log [Nonempty d] : + (MState.uniform : MState d).M.log = + HermitianMat.diagonal ℂ (fun _ => - Real.log (Fintype.card d)) := by + rw [MState.uniform, MState.ofClassical, HermitianMat.log, HermitianMat.cfc_diagonal] + congr 1 + funext _ + simp [ProbDistribution.uniform_def, Real.log_inv] -instance : RelEntropy.Nontrivial qRelativeEnt where - nontrivial := sorry +instance : RelEntropy qRelativeEnt where + DPI := by + intro d₁ d₂ _ _ _ _ ρ σ Λ + simpa [qRelativeEnt_state] using + (sandwichedRenyiEntropy_DPI (d₁ := d₁) (d₂ := d₂) (α := 1) + (hα := le_rfl) (ρ := ρ) (σ := σ) (Φ := Λ)) + of_kron := by + intro d₁ d₂ _ _ _ _ ρ₁ σ₁ ρ₂ σ₂ + rw [qRelativeEnt_state, qRelativeEnt_state, qRelativeEnt_state] + exact _root_.qRelativeEnt_additive ρ₁ σ₁ ρ₂ σ₂ + normalized := by + intro d _ _ _ i + let x : NNReal := ⟨Real.log (Fintype.card d), Real.log_nonneg (mod_cast Fintype.card_pos)⟩ + have hker : (MState.uniform : MState d).M.ker ≤ (MState.ofClassical (.constant i)).M.ker := by + rw [(HermitianMat.nonSingular_iff_ker_bot (A := (MState.uniform : MState d).M)).mp + (HermitianMat.nonSingular_of_posDef MState.uniform_posDef)] + exact bot_le + have hicul : ⟪(MState.ofClassical (.constant i)).M, (MState.uniform : MState d).M.log⟫ = + - Real.log (Fintype.card d) := by + rw [uniform_log, HermitianMat.inner_eq_re_trace, MState.ofClassical, + HermitianMat.diagonal_mat, HermitianMat.diagonal_mat, Matrix.diagonal_mul_diagonal, + Matrix.trace_diagonal] + classical + rw [Finset.sum_eq_single i] + · simp [ProbDistribution.constant_eq] + simpa using (Complex.log_ofReal_re (Fintype.card d : ℝ)) + · intro j _ hj; rw [ProbDistribution.constant_eq, if_neg fun h => hj h.symm]; simp + · intro h; exact (h (Finset.mem_univ i)).elim + apply EReal.coe_ennreal_injective + have hq := _root_.qRelativeEnt_eq_neg_Sᵥₙ_add + (ρ := MState.ofClassical (.constant i)) (σ := MState.uniform) + rw [if_pos hker, Sᵥₙ_ofClassical, Hₛ_constant_eq_zero, hicul] at hq + simp [qRelativeEnt_state, hq, EReal.coe_nnreal_eq_coe_real] /-- Quantum relative entropy as `Tr[ρ (log ρ - log σ)]` when supports are correct. -/ theorem qRelativeEnt_ker {ρ σ : MState d} (h : σ.M.ker ≤ ρ.M.ker) : - (𝐃(ρ‖σ) : EReal) = ρ.M.inner (HermitianMat.log ρ - HermitianMat.log σ) := by - simp only [qRelativeEnt, h] - congr + (qRelativeEnt ρ σ : EReal) = ⟪ρ.M, ρ.M.log - σ.M.log⟫ := by + simpa [qRelativeEnt_state] using (_root_.qRelativeEnt_ker (ρ := ρ) (σ := σ) h) + +end AxiomatizedEntropy From 8adfd016d5bf9a5d821bf2d7364dbbe6a4c29fa9 Mon Sep 17 00:00:00 2001 From: Dennj Osele Date: Thu, 21 May 2026 03:11:21 +0100 Subject: [PATCH 2/2] refactor: Split axiomatized entropy --- QuantumInfo/ClassicalInfo/Hellinger.lean | 43 +- .../Finite/AxiomatizedEntropy/Bounds.lean | 300 +++++ .../Finite/AxiomatizedEntropy/Defs.lean | 1110 +---------------- .../Finite/AxiomatizedEntropy/Faithful.lean | 565 +++++++++ .../Finite/AxiomatizedEntropy/Renyi.lean | 22 +- QuantumInfo/Finite/CPTPMap.lean | 1 + QuantumInfo/Finite/CPTPMap/CQPrepare.lean | 104 ++ QuantumInfo/Finite/Entropy/Relative.lean | 115 +- QuantumInfo/Finite/ProductPower.lean | 198 +++ QuantumInfo/ForMathlib/HermitianMat/Proj.lean | 115 ++ 10 files changed, 1339 insertions(+), 1234 deletions(-) create mode 100644 QuantumInfo/Finite/AxiomatizedEntropy/Bounds.lean create mode 100644 QuantumInfo/Finite/AxiomatizedEntropy/Faithful.lean create mode 100644 QuantumInfo/Finite/CPTPMap/CQPrepare.lean create mode 100644 QuantumInfo/Finite/ProductPower.lean diff --git a/QuantumInfo/ClassicalInfo/Hellinger.lean b/QuantumInfo/ClassicalInfo/Hellinger.lean index 1b4ea17c3..dc175952d 100644 --- a/QuantumInfo/ClassicalInfo/Hellinger.lean +++ b/QuantumInfo/ClassicalInfo/Hellinger.lean @@ -22,6 +22,8 @@ universe u open scoped BigOperators +namespace ProbDistribution + /-- The Hellinger overlap, or Bhattacharyya coefficient, of two finite probability distributions. -/ def hellingerOverlap {κ : Type u} [Fintype κ] (P Q : ProbDistribution κ) : ℝ := ∑ x, Real.sqrt ((P x : ℝ) * (Q x : ℝ)) @@ -73,43 +75,4 @@ theorem hellingerOverlap_coin_lt_one (p q : Prob) (hpq : (p : ℝ) < q) : Real.sq_sqrt (mul_nonneg (sub_nonneg.mpr hp1) (sub_nonneg.mpr hq1))] nlinarith [(Real.sqrt_mul (mul_nonneg hp0 hq0) ((1 - p) * (1 - q))).symm] -/-- The type obtained by taking `n` iterated dyadic self-products of `d`. -/ -def DyadicPow (d : Type u) : ℕ → Type u - | 0 => d - | n + 1 => DyadicPow d n × DyadicPow d n - -instance dyadicPowFintype {d : Type u} [Fintype d] (n : ℕ) : Fintype (DyadicPow d n) := by - induction n with - | zero => simpa [DyadicPow] using (inferInstance : Fintype d) - | succ n ih => simpa [DyadicPow] using (inferInstance : Fintype (DyadicPow d n × DyadicPow d n)) - -instance dyadicPowDecidableEq {d : Type u} [DecidableEq d] (n : ℕ) : - DecidableEq (DyadicPow d n) := by - induction n with - | zero => simpa [DyadicPow] using (inferInstance : DecidableEq d) - | succ n ih => - simpa [DyadicPow] using (inferInstance : DecidableEq (DyadicPow d n × DyadicPow d n)) - -/-- Iterated dyadic product power of a finite probability distribution. -/ -def dyadicProbPow {d : Type u} [Fintype d] (dist : ProbDistribution d) : - ∀ n, ProbDistribution (DyadicPow d n) - | 0 => dist - | n + 1 => ProbDistribution.prod (dyadicProbPow dist n) (dyadicProbPow dist n) - -/-- Hellinger overlap of dyadic product powers. -/ -theorem hellingerOverlap_dyadicProbPow {d : Type u} [Fintype d] - (P Q : ProbDistribution d) : - ∀ n, hellingerOverlap (dyadicProbPow P n) (dyadicProbPow Q n) = - (hellingerOverlap P Q) ^ (2 ^ n : ℕ) := by - intro n - induction n with - | zero => - change hellingerOverlap P Q = (hellingerOverlap P Q) ^ (1 : ℕ) - rw [pow_one] - | succ n ih => - change hellingerOverlap - (ProbDistribution.prod (dyadicProbPow P n) (dyadicProbPow P n)) - (ProbDistribution.prod (dyadicProbPow Q n) (dyadicProbPow Q n)) = - (hellingerOverlap P Q) ^ (2 ^ (n + 1) : ℕ) - rw [hellingerOverlap_prod, ih, show 2 ^ (n + 1) = 2 ^ n + 2 ^ n by omega, pow_add] - +end ProbDistribution diff --git a/QuantumInfo/Finite/AxiomatizedEntropy/Bounds.lean b/QuantumInfo/Finite/AxiomatizedEntropy/Bounds.lean new file mode 100644 index 000000000..fb9da99cd --- /dev/null +++ b/QuantumInfo/Finite/AxiomatizedEntropy/Bounds.lean @@ -0,0 +1,300 @@ +/- +Copyright (c) 2026 Dennj Osele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Dennj Osele +-/ +module + +import QuantumInfo.Finite.ProductPower +public import QuantumInfo.Finite.AxiomatizedEntropy.Defs +public import QuantumInfo.Finite.CPTPMap.CQPrepare +public import QuantumInfo.ForMathlib.HermitianMat.Order +public import QuantumInfo.ForMathlib.HermitianMat.Proj + +@[expose] public section + +/-! # Bounds for axiomatized relative entropies + +This file contains the relative max-entropy and the proof that every axiomatized relative entropy +lies below `max` on state inputs. +-/ + +noncomputable section +universe u + +open ComplexOrder +open scoped NNReal +open scoped ENNReal +open scoped Kronecker +open scoped HermitianMat + +variable (f : ∀ {d : Type u} [Fintype d] [DecidableEq d], MState d → HermitianMat d ℂ → ℝ≥0∞) + +namespace RelEntropy + +variable {d : Type u} [Fintype d] [DecidableEq d] + +open Classical in +/-- Quantum relative max-entropy. -/ +noncomputable def max (ρ : MState d) (σ : HermitianMat d ℂ) : ENNReal := + if ∃ (x : ℝ), ρ.M ≤ Real.exp x • σ then + some (sInf { x : NNReal | ρ.M ≤ Real.exp x • σ }) + else + ⊤ + +@[aesop (rule_sets := [finiteness]) simp] +protected theorem max_not_top (ρ : MState d) (σ : HermitianMat d ℂ) (hσ : 0 ≤ σ) : + (max ρ σ) ≠ ⊤ ↔ σ.ker ≤ ρ.M.ker := by + open ComplexOrder in + constructor + · intro h + have hx : ∃ x : ℝ, ρ.M ≤ Real.exp x • σ := by + by_contra hx + exact h (by simp [max, hx]) + obtain ⟨x, hx⟩ := hx + exact HermitianMat.ker_le_of_le_smul (Real.exp_pos x).ne' ρ.nonneg hx + · intro hker + let P := σ.supportProj + have hright : ρ.M.mat * P.mat = ρ.M.mat := by + dsimp [P]; simpa using HermitianMat.mul_supportProj_of_ker_le (A := ρ.M) (B := σ) hker + have hleft : P.mat * ρ.M.mat = ρ.M.mat := by + simpa only [Matrix.conjTranspose_mul, HermitianMat.conjTranspose_mat] using + congrArg Matrix.conjTranspose hright + have hP_idem : P.mat * P.mat = P.mat := by + rw [← pow_two, ← HermitianMat.mat_pow] + congr 1 + dsimp [P] + rw [HermitianMat.supportProj_eq_cfc, ← HermitianMat.cfc_pow, + ← HermitianMat.cfc_comp_apply] + exact HermitianMat.cfc_congr_of_nonneg hσ fun x _ => by + by_cases hx : x = 0 <;> simp [hx] + have hρ_le_P : ρ.M ≤ P := calc + ρ.M = ρ.M.conj P.mat := by + symm; apply HermitianMat.ext + simp only [HermitianMat.conj_apply_mat, HermitianMat.conjTranspose_mat, + hright, hleft] + _ ≤ (1 : HermitianMat d ℂ).conj P.mat := HermitianMat.conj_mono ρ.le_one + _ = P := by apply HermitianMat.ext; simp [HermitianMat.conj_apply_mat, hP_idem] + let α : ℝ := ∑ i, if σ.H.eigenvalues i = 0 then 0 else (σ.H.eigenvalues i)⁻¹ + have hterm j : 0 ≤ if σ.H.eigenvalues j = 0 then 0 else (σ.H.eigenvalues j)⁻¹ := by + split_ifs + · rfl + · exact inv_nonneg.mpr (HermitianMat.eigenvalues_nonneg hσ j) + have hα_nonneg : 0 ≤ α := Finset.sum_nonneg fun i _ => hterm i + have hP_le : P ≤ α • σ := by + dsimp [P, α] + rw [← sub_nonneg, show (∑ i, if σ.H.eigenvalues i = 0 then 0 else (σ.H.eigenvalues i)⁻¹) • σ = + σ.cfc (fun x => (∑ i, if σ.H.eigenvalues i = 0 then 0 else (σ.H.eigenvalues i)⁻¹) * x) from by + simp, + HermitianMat.supportProj_eq_cfc, ← HermitianMat.cfc_sub_apply, HermitianMat.cfc_nonneg_iff] + intro i + by_cases hi : σ.H.eigenvalues i = 0 + · simp [hi] + · have hsingle : (σ.H.eigenvalues i)⁻¹ ≤ α := by + dsimp [α]; simpa [hi] using + Finset.single_le_sum (fun j _ => hterm j) (Finset.mem_univ i) + have := mul_le_mul_of_nonneg_right hsingle (HermitianMat.eigenvalues_nonneg hσ i) + simp [hi]; linarith [inv_mul_cancel₀ hi] + rw [max, if_pos ⟨Real.log (α + 1), by + calc ρ.M ≤ P := hρ_le_P + _ ≤ α • σ := hP_le + _ ≤ (α + 1) • σ := smul_le_smul_of_nonneg_right (by linarith) hσ + _ = Real.exp (Real.log (α + 1)) • σ := by + rw [Real.exp_log (by positivity : (0 : ℝ) < α + 1)]⟩] + simp + +protected theorem toReal_max (ρ : MState d) (σ : HermitianMat d ℂ) : + (max ρ σ).toReal = sInf ((↑) '' { x : ℝ≥0 | ρ.M ≤ Real.exp x • σ }) := by + rw [max] + split_ifs with h + · have hs : ({ x : ℝ≥0 | ρ.M ≤ Real.exp x • σ } : Set ℝ≥0).Nonempty := by + rcases h with ⟨x, hx⟩ + have hσ_nonneg : 0 ≤ σ := + (smul_le_smul_iff_of_pos_left (Real.exp_pos x)).mp (by simpa using le_trans ρ.nonneg hx) + refine ⟨⟨Max.max x 0, le_max_right _ _⟩, ?_⟩ + exact hx.trans <| + smul_le_smul_of_nonneg_right + (Real.exp_le_exp.mpr (show x ≤ Max.max x 0 from le_max_left _ _)) hσ_nonneg + simp [ENNReal.some_eq_coe, NNReal.coe_sInf] + · push Not at h + have hs : ({ x : ℝ≥0 | ρ.M ≤ Real.exp x • σ } : Set ℝ≥0) = ∅ := by + ext x + simp [h (x : ℝ)] + simp [hs] + +@[simp] +theorem max_self_eq_zero (ρ : MState d) : max ρ ρ.M = 0 := by + rw [max, if_pos ⟨0, by simp⟩] + simp [show sInf { x : ℝ≥0 | ρ.M ≤ Real.exp x • ρ.M } = 0 from + le_antisymm (csInf_le ⟨0, fun x _ => x.2⟩ (by simp)) + (le_csInf ⟨0, by simp⟩ fun x _ => x.2)] + +private def tauOfLE (N : ℕ) (hN : 0 < N) (ρ σ : MState d) + (h : ρ.M ≤ ((N + 1 : ℝ) • σ.M)) : MState d where + M := ((N : ℝ)⁻¹) • (((N + 1 : ℝ) • σ.M) - ρ.M) + nonneg := smul_nonneg (by positivity) (sub_nonneg.mpr h) + tr := by + have hN' : (N : ℝ) ≠ 0 := by positivity + simp [HermitianMat.trace_sub, σ.tr, ρ.tr, hN'] + +private theorem cqPrepareCPTP_uniform_tauOfLE + (M : ℕ) (hM_pos : 0 < M) (ρ σ : MState d) + (h : ρ.M ≤ ((M + 1 : ℝ) • σ.M)) : + CPTPMap.cqPrepare (d := d) (fun i : ULift (Fin (M + 1)) => + if i = ⟨0⟩ then ρ else tauOfLE (d := d) M hM_pos ρ σ h) + (MState.uniform : MState (ULift (Fin (M + 1)))) = σ := by + let x0 : ULift (Fin (M + 1)) := ⟨0⟩ + let τr := tauOfLE (d := d) M hM_pos ρ σ h + let τ : ULift (Fin (M + 1)) → MState d := fun i => if i = x0 then ρ else τr + change CPTPMap.cqPrepare (d := d) τ (MState.uniform : MState (ULift (Fin (M + 1)))) = σ + apply MState.ext_m + change (CPTPMap.cqPrepare (d := d) τ + (MState.ofClassical ProbDistribution.uniform)).m = σ.m + rw [CPTPMap.cqPrepare_apply_ofClassical (d := d) τ ProbDistribution.uniform] + ext i j + simp only [ProbDistribution.uniform_def, Matrix.sum_apply, Matrix.smul_apply, + Complex.real_smul, Finset.card_univ, Fintype.card_ulift, Fintype.card_fin, one_div, + Nat.cast_add, Nat.cast_one, Complex.ofReal_inv, Complex.ofReal_add, + Complex.ofReal_natCast, Complex.ofReal_one] + rw [(Finset.sum_erase_add (s := Finset.univ) (a := x0) + (f := fun x : ULift (Fin (M + 1)) => + (↑M + 1 : ℂ)⁻¹ * (if x = x0 then ρ else τr).m i j) (by simp)).symm] + have hrest : + Finset.sum (Finset.erase Finset.univ x0) + (fun x : ULift (Fin (M + 1)) => + (↑M + 1 : ℂ)⁻¹ * (if x = x0 then ρ else τr).m i j) + = + M * ((↑M + 1 : ℂ)⁻¹ * τr.m i j) := by + trans Finset.sum (Finset.erase Finset.univ x0) + (fun _ : ULift (Fin (M + 1)) => (↑M + 1 : ℂ)⁻¹ * τr.m i j) + · exact Finset.sum_congr rfl fun x hx => by simp [(Finset.mem_erase.mp hx).1] + · simp [x0] + rw [hrest] + dsimp [τr] + simp [tauOfLE, MState.m] + field_simp [show (M : ℂ) ≠ 0 by exact_mod_cast Nat.ne_of_gt hM_pos, + show (M + 1 : ℂ) ≠ 0 by exact_mod_cast Nat.succ_ne_zero M] + simp only [← HermitianMat.mat_apply, HermitianMat.mat_sub, HermitianMat.mat_smul, + Matrix.sub_apply, Matrix.smul_apply] + rw [Complex.real_smul] + norm_num + +private theorem integer_bound_aux [RelEntropy f] (N : ℕ) (ρ σ : MState d) + (h : ρ.M ≤ ((N + 1 : ℝ) • σ.M)) : + f ρ σ.M ≤ ENNReal.ofReal (Real.log (N + 1)) := by + cases N with + | zero => + have hEq : ρ = σ := MState.ext <| (eq_of_sub_eq_zero (HermitianMat.ext <| + (Matrix.PosSemidef.trace_eq_zero_iff (HermitianMat.zero_le_iff.mp <| + show 0 ≤ σ.M - ρ.M by simpa using sub_nonneg.mpr (show ρ.M ≤ σ.M by + simpa using h))).1 <| + (HermitianMat.trace_eq_zero_iff (A := σ.M - ρ.M)).1 + (by simp [σ.tr, ρ.tr]))).symm + subst hEq + simp + | succ N => + let κ := ULift (Fin (N + 2)) + let x0 : κ := ⟨0⟩ + let τrest := tauOfLE (d := d) (N + 1) (Nat.succ_pos _) ρ σ h + let τ : κ → MState d := fun i => if i = x0 then ρ else τrest + let Λ : CPTPMap κ d := CPTPMap.cqPrepare (d := d) τ + have hconst : Λ (MState.ofClassical (.constant x0)) = ρ := by + apply MState.ext_m + rw [CPTPMap.cqPrepare_apply_ofClassical (d := d) τ (.constant x0)] + ext i j + rw [Finset.sum_eq_single x0] + · simp [τ, ProbDistribution.constant_eq] + · intro y _ hyx + simp [ProbDistribution.constant_eq, hyx, eq_comm] + · simp + have huniform : Λ (MState.uniform : MState κ) = σ := by + simpa [Λ, κ, τ, τrest] using + cqPrepareCPTP_uniform_tauOfLE (d := d) (N + 1) (Nat.succ_pos _) ρ σ h + calc + f ρ σ.M = + f (Λ (MState.ofClassical (.constant x0))) + ((Λ (MState.uniform : MState κ)).M) := by + rw [hconst, huniform] + _ ≤ f (MState.ofClassical (.constant x0)) (MState.uniform : MState κ).M := DPI _ _ Λ + _ = ENNReal.ofReal (Real.log (N + 2)) := by + simpa [κ, ENNReal.some_eq_coe, + ENNReal.ofReal_eq_coe_nnreal (Real.log_nonneg + (by + have := (Nat.cast_nonneg N : (0 : ℝ) ≤ N) + linarith : (1 : ℝ) ≤ (N + 2 : ℝ)))] using + (RelEntropy.normalized (f := f) (d := κ) x0) + _ = ENNReal.ofReal (Real.log (↑(N + 1) + 1)) := by + norm_num [Nat.cast_add, add_assoc, add_comm, add_left_comm] + +/-- If `ρ ≤ exp x • σ`, then every axiomatized relative entropy is bounded by `x`. -/ +theorem le_of_le_exp [RelEntropy f] (ρ σ : MState d) {x : ℝ} + (hx : 0 ≤ x) (h : ρ.M ≤ Real.exp x • σ.M) : + f ρ σ.M ≤ ENNReal.ofReal x := by + have hfin : f ρ σ.M ≠ ∞ := + ne_top_of_le_ne_top ENNReal.ofReal_ne_top <| + integer_bound_aux (f := f) (N := Nat.ceil (Real.exp x)) ρ σ <| by + exact h.trans <| smul_le_smul_of_nonneg_right + ((Nat.le_ceil _).trans (by norm_num)) σ.nonneg + by_contra hfx + let δ : ℝ := (f ρ σ.M).toReal - x + have hδ : 0 < δ := by + dsimp [δ]; linarith [(ENNReal.ofReal_lt_iff_lt_toReal hx hfin).1 (lt_of_not_ge hfx)] + let n : ℕ := Nat.ceil (Real.log 3 / δ) + 1 + have hgap : Real.log 3 < (n : ℝ) * δ := by + rw [← div_lt_iff₀ hδ] + dsimp [n] + exact lt_of_le_of_lt (Nat.le_ceil (Real.log 3 / δ)) + (by exact_mod_cast Nat.lt_succ_self (Nat.ceil (Real.log 3 / δ))) + let y : ℝ := (n : ℝ) * x + have hpow_bound' : + (((n : ℕ) : ENNReal) * f ρ σ.M) ≤ + ENNReal.ofReal (Real.log (Nat.ceil (Real.exp y) + 1)) := by + simpa [RelEntropy.of_npow (f := f) ρ σ n] using + integer_bound_aux (f := f) (N := Nat.ceil (Real.exp y)) + (MState.npow ρ n) (MState.npow σ n) (by + exact (MState.npow_le_exp_smul h n).trans <| smul_le_smul_of_nonneg_right + (by dsimp [y]; exact (Nat.le_ceil _).trans (by norm_num)) + (MState.npow σ n).nonneg) + have hpow_bound_real : + (n : ℝ) * (f ρ σ.M).toReal ≤ + Real.log (Nat.ceil (Real.exp y) + 1 : ℝ) := by + simpa [ENNReal.toReal_mul, ENNReal.toReal_natCast, + ENNReal.toReal_ofReal (Real.log_nonneg + (show (1 : ℝ) ≤ Nat.ceil (Real.exp y) + 1 by + exact_mod_cast Nat.succ_le_succ (Nat.zero_le _)))] using + (ENNReal.toReal_le_toReal (ENNReal.mul_ne_top (by simp) hfin) ENNReal.ofReal_ne_top).2 + hpow_bound' + have hlog_upper : Real.log (Nat.ceil (Real.exp y) + 1 : ℝ) ≤ y + Real.log 3 := by + refine (show Real.log (Nat.ceil (Real.exp y) + 1 : ℝ) ≤ Real.log (3 * Real.exp y) from + Real.log_le_log (by positivity) ?_).trans_eq ?_ + · nlinarith [(Nat.ceil_lt_add_one (Real.exp_nonneg y)).le, + (show (1 : ℝ) ≤ Real.exp y by rw [Real.one_le_exp_iff]; dsimp [y]; positivity)] + · rw [Real.log_mul (by positivity : (3 : ℝ) ≠ 0) (Real.exp_pos y).ne', Real.log_exp] + ring + dsimp [y, δ] at hgap + nlinarith + +/-- The relative max-entropy is a lower bound on all relative entropies. -/ +theorem le_max [RelEntropy f] (ρ σ : MState d) : f ρ σ.M ≤ max ρ σ.M := by + by_cases hx : ∃ x : ℝ, ρ.M ≤ Real.exp x • σ.M + · obtain ⟨x, hx⟩ := hx + let y : ℝ := Max.max x 0 + have hy0 : 0 ≤ y := by simp [y] + have hy : ρ.M ≤ Real.exp y • σ.M := by + exact hx.trans <| smul_le_smul_of_nonneg_right + (Real.exp_le_exp.mpr (show x ≤ y by dsimp [y]; exact le_max_left _ _)) σ.nonneg + have hfin : f ρ σ.M ≠ ∞ := + ne_top_of_le_ne_top ENNReal.ofReal_ne_top (le_of_le_exp (f := f) ρ σ hy0 hy) + exact (ENNReal.toReal_le_toReal hfin + (by simp [max, (show ∃ x : ℝ, ρ.M ≤ Real.exp x • σ.M from ⟨x, hx⟩)])).1 <| by + rw [RelEntropy.toReal_max (ρ := ρ) (σ := σ.M)] + let S : Set ℝ := ((↑) '' {x : ℝ≥0 | ρ.M ≤ Real.exp x • σ.M}) + refine le_csInf ⟨(⟨y, hy0⟩ : ℝ≥0), ⟨⟨y, hy0⟩, hy, rfl⟩⟩ ?_ + intro a ha + rcases ha with ⟨z, hz, rfl⟩ + simpa [ENNReal.toReal_ofReal z.2] using + (ENNReal.toReal_le_toReal hfin ENNReal.ofReal_ne_top).2 + (le_of_le_exp (f := f) ρ σ z.2 hz) + · simp [max, hx] + +end RelEntropy diff --git a/QuantumInfo/Finite/AxiomatizedEntropy/Defs.lean b/QuantumInfo/Finite/AxiomatizedEntropy/Defs.lean index 6756feedf..e81e34580 100644 --- a/QuantumInfo/Finite/AxiomatizedEntropy/Defs.lean +++ b/QuantumInfo/Finite/AxiomatizedEntropy/Defs.lean @@ -6,11 +6,8 @@ Authors: Alex Meiburg, Dennj Osele module public import QuantumInfo.ClassicalInfo.Entropy -public import QuantumInfo.ClassicalInfo.Hellinger public import QuantumInfo.Finite.MState -public import QuantumInfo.Finite.CPTPMap -public import QuantumInfo.Finite.POVM -public import QuantumInfo.Finite.Entropy.Relative +public import QuantumInfo.Finite.CPTPMap.CPTP @[expose] public section @@ -19,41 +16,32 @@ public import QuantumInfo.Finite.Entropy.Relative Here we define a broad notion of entropy axiomatically, `Entropy`, and the Prop `Entropy f` means that the function `f : MState → ℝ` acts like a generalized kind of quantum entropy. For instance, min-, max-, α-Renyi, and von Neumann entropies all fall -into this category. We prove various properties about the entropy for anything -supporting this type class. Any entropy automatically gets corresponding notions -of conditional entropy, mutual information, and so on. +into this category. Similarly, `RelEntropy f` means that `f : MState → HermitianMat → ENNReal` is a kind of relative entropy. Every `RelEntropy` leads to a notion of entropy, as well, by fixing one argument to the fully mixed state. -Of course relative entropies are "usually" used with a pair of (normalized) quantum -states, but it's still very common in literature to specifically let the second -argument be an arbitrary (PSD, Hermitian) matrix, so we do allow this. The behavior -when not a density matrix is left unspecified by the axioms. +Of course relative entropies are "usually" used with a pair of normalized quantum states, but +it is still common in the literature to let the second argument be an arbitrary PSD Hermitian +matrix, so we allow this. The behavior when not a density matrix is left unspecified by the +axioms. -In terms of the file structure, we start with `RelEntropy` as the more "general" -function, and then derive much of `Entropy` from it. - -## References: - - - [Khinchin’s Fourth Axiom of Entropy Revisited](https://www.mdpi.com/2571-905X/6/3/49) - - [α-z Relative Entropies](https://warwick.ac.uk/fac/sci/maths/research/events/2013-2014/statmech/su/Nilanjana-slides.pdf) - - Watrous's notes, [Max-relative entropy and conditional min-entropy](https://cs.uwaterloo.ca/~watrous/QIT-notes/QIT-notes.02.pdf) - - [Quantum Relative Entropy - An Axiomatic Approach](https://www.marcotom.info/files/entropy-masterclass2022.pdf) -by Marco Tomamichel - - [StackExchange](https://quantumcomputing.stackexchange.com/a/12953/10115) +## References +* [Khinchin’s Fourth Axiom of Entropy Revisited](https://www.mdpi.com/2571-905X/6/3/49) +* [α-z Relative Entropies](https://warwick.ac.uk/fac/sci/maths/research/events/2013-2014/statmech/su/Nilanjana-slides.pdf) +* Watrous's notes, [Max-relative entropy and conditional min-entropy](https://cs.uwaterloo.ca/~watrous/QIT-notes/QIT-notes.02.pdf) +* [Quantum Relative Entropy - An Axiomatic Approach](https://www.marcotom.info/files/entropy-masterclass2022.pdf) + by Marco Tomamichel +* [StackExchange](https://quantumcomputing.stackexchange.com/a/12953/10115) -/ noncomputable section universe u -open ComplexOrder open scoped NNReal open scoped ENNReal -open scoped Kronecker -open scoped HermitianMat variable (f : ∀ {d : Type u} [Fintype d] [DecidableEq d], MState d → HermitianMat d ℂ → ℝ≥0∞) @@ -63,25 +51,26 @@ variable (f : ∀ {d : Type u} [Fintype d] [DecidableEq d], MState d → Hermiti This simpler class allows for _trivial_ relative entropies, such as `-log tr(ρ⁰σ)`. Use the mixin `RelEntropy.Nontrivial` to only allow nontrivial relative entropies. -/ class RelEntropy : Prop where - /-- The data processing inequality -/ + /-- The data processing inequality. -/ DPI {d₁ d₂ : Type u} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] (ρ σ : MState d₁) (Λ : CPTPMap d₁ d₂) : f (Λ ρ) (Λ σ) ≤ f ρ σ - /-- Entropy is additive under tensor products -/ + /-- Entropy is additive under tensor products. -/ of_kron {d₁ d₂ : Type u} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] : - ∀ (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂), f (ρ₁ ⊗ᴹ ρ₂) (σ₁ ⊗ᴹ σ₂) = f ρ₁ σ₁ + f ρ₂ σ₂ + ∀ (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂), + f (ρ₁ ⊗ᴹ ρ₂) (σ₁ ⊗ᴹ σ₂) = f ρ₁ σ₁ + f ρ₂ σ₂ /-- Normalization of entropy to be `ln N` for a pure state vs. uniform on `N` many states. -/ normalized {d : Type u} [fin : Fintype d] [DecidableEq d] [Nonempty d] (i : d) : f (.ofClassical (.constant i)) MState.uniform.M = some ⟨Real.log fin.card, Real.log_nonneg (mod_cast Fintype.card_pos)⟩ -/-- Mixin on top of `RelEntropy` that rules out trivial relative entropies (those that vanish -on every pair of full-support states). See [Tomamichel](https://www.marcotom.info/files/entropy-masterclass2022.pdf). -/ +/-- Mixin on top of `RelEntropy` that rules out trivial relative entropies, those that vanish +on every pair of full-support states. See +[Tomamichel](https://www.marcotom.info/files/entropy-masterclass2022.pdf). -/ class RelEntropy.Nontrivial [RelEntropy f] where - /-- Nontriviality condition for a relative entropy: some pair of full-support states has - positive relative entropy. This is the negation of Tomamichel's definition of a trivial - relative entropy, which vanishes on all full-support state pairs. -/ - nontrivial : ∃ (d : Type u) (_ : Fintype d) (_ : DecidableEq d) (ρ σ : MState d), - ρ.M.support = ⊤ ∧ σ.M.support = ⊤ ∧ 0 < f ρ σ + /-- Nontriviality condition for a relative entropy: every finite system has some pair of + full-support states with positive relative entropy. -/ + nontrivial (d : Type u) [Fintype d] [DecidableEq d] : + ∃ ρ σ : MState d, ρ.M.support = ⊤ ∧ σ.M.support = ⊤ ∧ 0 < f ρ σ namespace RelEntropy @@ -98,15 +87,12 @@ it for domains of size 2, which is sufficient (see Tomamichel's proof). In that fact that it's still zero when `Unique d` has to be proven, and this (now used) chunk of a proof can be used in part for that: --- have h_uniq (ρ') := (Subsingleton.allEq ρ ρ').symm --- have h_kron := of_kron (f := f) ρ ρ ρ ρ --- let e : d ≃ (d × d) := (Equiv.prodUnique d d).symm --- rw [← relabel_eq f e] at h_kron --- rw [h_uniq ((ρ⊗ρ).relabel e)] at h_kron --- rw [h_uniq σ] - -At that point we need the fact that it's not `⊤`, and then it must be zero. +Let `D` be a generalized divergence satisfying DPI and additivity. Then `D` is automatically +normalized to zero on the 1D space. +Proof sketch: By additivity, `D(unit‖unit) = D(unit⊗unit‖unit⊗unit) = D(unit‖unit) + D(unit‖unit)`, +so `D(unit‖unit) = 0` unless it is `⊤`. DPI from a two-point normalized pair rules out `⊤`. +The current axioms include the 1D normalization directly, so the proof below uses it. -/ /-- Relabelling a state with `CPTPMap.ofEquiv` leaves relative entropies unchanged. -/ @@ -126,9 +112,6 @@ theorem relabel_eq (e : d₂ ≃ d) (ρ σ : MState d) : f (ρ.relabel e) (σ.relabel e) = f ρ σ := by exact ofEquiv_eq (f := f) e.symm ρ σ ---Tomamichel's "4. Positivity" theorem is implicit true in our description because we ---only allow ENNReals. The only part to prove is that "D(ρ‖σ) = 0 if ρ = σ". - /-- The relative entropy is zero between any two states on a 1-D Hilbert space. -/ private lemma wrt_self_eq_zero' [Unique d] (ρ σ : MState d) : f ρ σ = 0 := by convert normalized (f := f) (d := d) default @@ -146,1046 +129,15 @@ theorem wrt_self_eq_zero (ρ : MState d) : f ρ ρ.M = 0 := by end possibly_trivial -section bounds - -open Prob in -/-- A support-test lower bound for relative entropies. - -This is not the standard quantum relative min-entropy on state inputs: for density-matrix -second arguments it collapses to zero, as `min_state_eq_zero` shows. The name is kept because -it is the min-side bound paired with `max` in this axiomatized API. -/ -def min (ρ : MState d) (σ : HermitianMat d ℂ) : ENNReal := - —log ⟨ρ.exp_val (HermitianMat.projLE 0 σ), - ρ.exp_val_prob ⟨HermitianMat.projLE_nonneg 0 σ, HermitianMat.projLE_le_one 0 σ⟩⟩ - -@[aesop (rule_sets := [finiteness]) simp] -theorem min_eq_top_iff (ρ : MState d) (σ : HermitianMat d ℂ) : - (min ρ σ) = ⊤ ↔ ρ.M.support ≤ (HermitianMat.projLE 0 σ).ker := by - rw [min, Prob.negLog_eq_top_iff] - constructor - · intro h - have h0 : ρ.exp_val (HermitianMat.projLE 0 σ) = 0 := by - simpa using congrArg (fun p : Prob => (p : ℝ)) h - exact (ρ.exp_val_eq_zero_iff (HermitianMat.projLE_nonneg 0 σ)).mp h0 - · intro h - exact Subtype.ext ((ρ.exp_val_eq_zero_iff (HermitianMat.projLE_nonneg 0 σ)).mpr h) - -protected theorem toReal_min (ρ : MState d) (σ : HermitianMat d ℂ) : - (min ρ σ).toReal = -Real.log (ρ.exp_val (HermitianMat.projLE 0 σ)) := by - simp [min, - Prob.negLog_pos_Real (p := ⟨ρ.exp_val (HermitianMat.projLE 0 σ), - ρ.exp_val_prob ⟨HermitianMat.projLE_nonneg 0 σ, HermitianMat.projLE_le_one 0 σ⟩⟩)] - - -/-- On state inputs, the current support-based `min` quantity is always zero. -/ -@[simp] -theorem min_state_eq_zero (ρ σ : MState d) : min ρ σ.M = 0 := by - have hproj : HermitianMat.projLE 0 σ.M = 1 := by - rw [HermitianMat.projLE_zero_cfc] - calc σ.M.cfc (fun x ↦ if 0 ≤ x then 1 else 0) = σ.M.cfc (fun _ ↦ (1 : ℝ)) := - HermitianMat.cfc_congr_of_nonneg σ.nonneg fun _ hx => by simpa using hx - _ = 1 := by simp [HermitianMat.cfc_const (A := σ.M) (r := (1 : ℝ))] - simp [min, show (⟨ρ.exp_val (HermitianMat.projLE 0 σ.M), - ρ.exp_val_prob ⟨HermitianMat.projLE_nonneg 0 σ.M, HermitianMat.projLE_le_one 0 σ.M⟩⟩ : Prob) = 1 - from Subtype.ext (by change ρ.exp_val _ = 1; rw [hproj, MState.exp_val_one])] - -/-- The current support-based `min` quantity does not satisfy the normalization axiom of `RelEntropy`. -/ -theorem not_RelEntropy_min : ¬ RelEntropy min := by - intro hmin - have := congrArg ENNReal.toReal (hmin.normalized (d := ULift (Fin 2)) (i := ⟨0⟩)) - simp at this; linarith [Real.log_pos one_lt_two] - -theorem not_Nontrivial_min [RelEntropy min] : ¬Nontrivial min := by - rintro ⟨h⟩ - obtain ⟨d, _, _, ρ, σ, -, -, hpos⟩ := h - simp at hpos - -omit [RelEntropy f] in -/-- The relative min-entropy is a lower bound on all relative entropies. -/ -theorem min_le (ρ σ : MState d) : min ρ σ.M ≤ f ρ σ.M := by - simp - -open Classical in -/-- Quantum relative max-entropy. -/ -def max (ρ : MState d) (σ : HermitianMat d ℂ) : ENNReal := - if ∃ (x : ℝ), ρ.M ≤ Real.exp x • σ then - some (sInf { x : NNReal | ρ.M ≤ Real.exp x • σ }) - else - ⊤ - -@[aesop (rule_sets := [finiteness]) simp] -protected theorem max_not_top (ρ : MState d) (σ : HermitianMat d ℂ) (hσ : 0 ≤ σ) : - (max ρ σ) ≠ ⊤ ↔ σ.ker ≤ ρ.M.ker := by - open ComplexOrder in - constructor - · intro h - have hx : ∃ x : ℝ, ρ.M ≤ Real.exp x • σ := by - by_contra hx - exact h (by simp [max, hx]) - obtain ⟨x, hx⟩ := hx - exact HermitianMat.ker_le_of_le_smul (Real.exp_pos x).ne' ρ.nonneg hx - · intro hker - let P := σ.supportProj - have hright : ρ.M.mat * P.mat = ρ.M.mat := by - dsimp [P]; simpa using HermitianMat.mul_supportProj_of_ker_le (A := ρ.M) (B := σ) hker - have hleft : P.mat * ρ.M.mat = ρ.M.mat := by - simpa only [Matrix.conjTranspose_mul, HermitianMat.conjTranspose_mat] using - congrArg Matrix.conjTranspose hright - have hP_idem : P.mat * P.mat = P.mat := by - rw [← pow_two, ← HermitianMat.mat_pow] - congr 1 - dsimp [P] - rw [HermitianMat.supportProj_eq_cfc, ← HermitianMat.cfc_pow, - ← HermitianMat.cfc_comp_apply] - exact HermitianMat.cfc_congr_of_nonneg hσ fun x _ => by - by_cases hx : x = 0 <;> simp [hx] - have hρ_le_P : ρ.M ≤ P := calc - ρ.M = ρ.M.conj P.mat := by - symm; apply HermitianMat.ext - simp only [HermitianMat.conj_apply_mat, HermitianMat.conjTranspose_mat, - hright, hleft] - _ ≤ (1 : HermitianMat d ℂ).conj P.mat := HermitianMat.conj_mono ρ.le_one - _ = P := by apply HermitianMat.ext; simp [HermitianMat.conj_apply_mat, hP_idem] - let α : ℝ := ∑ i, if σ.H.eigenvalues i = 0 then 0 else (σ.H.eigenvalues i)⁻¹ - have hterm j : 0 ≤ if σ.H.eigenvalues j = 0 then 0 else (σ.H.eigenvalues j)⁻¹ := by - split_ifs - · rfl - · exact inv_nonneg.mpr (HermitianMat.eigenvalues_nonneg hσ j) - have hα_nonneg : 0 ≤ α := Finset.sum_nonneg fun i _ => hterm i - have hP_le : P ≤ α • σ := by - dsimp [P, α] - rw [← sub_nonneg, show (∑ i, if σ.H.eigenvalues i = 0 then 0 else (σ.H.eigenvalues i)⁻¹) • σ = - σ.cfc (fun x => (∑ i, if σ.H.eigenvalues i = 0 then 0 else (σ.H.eigenvalues i)⁻¹) * x) from by - simp, - HermitianMat.supportProj_eq_cfc, ← HermitianMat.cfc_sub_apply, HermitianMat.cfc_nonneg_iff] - intro i - by_cases hi : σ.H.eigenvalues i = 0 - · simp [hi] - · have hsingle : (σ.H.eigenvalues i)⁻¹ ≤ α := by - dsimp [α]; simpa [hi] using - Finset.single_le_sum (fun j _ => hterm j) (Finset.mem_univ i) - have := mul_le_mul_of_nonneg_right hsingle (HermitianMat.eigenvalues_nonneg hσ i) - simp [hi]; linarith [inv_mul_cancel₀ hi] - rw [max, if_pos ⟨Real.log (α + 1), by - calc ρ.M ≤ P := hρ_le_P - _ ≤ α • σ := hP_le - _ ≤ (α + 1) • σ := smul_le_smul_of_nonneg_right (by linarith) hσ - _ = Real.exp (Real.log (α + 1)) • σ := by - rw [Real.exp_log (by positivity : (0 : ℝ) < α + 1)]⟩] - simp - -protected theorem toReal_max (ρ : MState d) (σ : HermitianMat d ℂ) : - (max ρ σ).toReal = sInf ((↑) '' { x : ℝ≥0 | ρ.M ≤ Real.exp x • σ }) := by - rw [max] - split_ifs with h - · have hs : ({ x : ℝ≥0 | ρ.M ≤ Real.exp x • σ } : Set ℝ≥0).Nonempty := by - rcases h with ⟨x, hx⟩ - have hσ_nonneg : 0 ≤ σ := - (smul_le_smul_iff_of_pos_left (Real.exp_pos x)).mp (by simpa using le_trans ρ.nonneg hx) - refine ⟨⟨Max.max x 0, le_max_right _ _⟩, ?_⟩ - exact hx.trans <| - smul_le_smul_of_nonneg_right - (Real.exp_le_exp.mpr (show x ≤ Max.max x 0 from le_max_left _ _)) hσ_nonneg - simp [ENNReal.some_eq_coe, NNReal.coe_sInf] - · push Not at h - have hs : ({ x : ℝ≥0 | ρ.M ≤ Real.exp x • σ } : Set ℝ≥0) = ∅ := by - ext x - simp [h (x : ℝ)] - simp [hs] - -@[simp] -theorem max_self_eq_zero (ρ : MState d) : max ρ ρ.M = 0 := by - rw [max, if_pos ⟨0, by simp⟩] - simp [show sInf { x : ℝ≥0 | ρ.M ≤ Real.exp x • ρ.M } = 0 from - le_antisymm (csInf_le ⟨0, fun x _ => x.2⟩ (by simp)) - (le_csInf ⟨0, by simp⟩ fun x _ => x.2)] - -/-- A full-support state dominates every other state up to an integer scalar. -/ -private theorem exists_le_nat_smul_of_fullSupport (ρ σ : MState d) - (hσ : σ.M.support = ⊤) : - ∃ N : ℕ, 0 < N ∧ ρ.M ≤ ((N + 1 : ℝ) • σ.M) := by - letI : σ.M.NonSingular := HermitianMat.nonSingular_iff_support_top.mpr hσ - have hexp : ∃ x : ℝ, ρ.M ≤ Real.exp x • σ.M := by - by_contra h - exact (RelEntropy.max_not_top ρ σ.M σ.nonneg).mpr - (by simp [HermitianMat.nonSingular_ker_bot]) (by simp [max, h]) - obtain ⟨x, hx⟩ := hexp - refine ⟨Nat.ceil (Real.exp x), Nat.ceil_pos.mpr (Real.exp_pos x), ?_⟩ - exact hx.trans <| smul_le_smul_of_nonneg_right ((Nat.le_ceil _).trans (by norm_num)) σ.nonneg - -/-- The output of Tomamichel's preparation channel on the first binary point. -/ -private def binaryPrepOne (γ ω : MState d) (s t : ℝ) (hden : 0 < 1 - s - t) - (h : t • γ.M ≤ (1 - s) • ω.M) : MState d where - M := (1 - s - t)⁻¹ • ((1 - s) • ω.M - t • γ.M) - nonneg := smul_nonneg (inv_nonneg.mpr hden.le) (sub_nonneg.mpr h) - tr := by - simpa [HermitianMat.trace_smul, HermitianMat.trace_sub, γ.tr, ω.tr] using - inv_mul_cancel₀ hden.ne' - -/-- The output of Tomamichel's preparation channel on the second binary point. -/ -private def binaryPrepZero (γ ω : MState d) (s t : ℝ) (hden : 0 < 1 - s - t) - (h : s • ω.M ≤ (1 - t) • γ.M) : MState d where - M := (1 - s - t)⁻¹ • ((1 - t) • γ.M - s • ω.M) - nonneg := smul_nonneg (inv_nonneg.mpr hden.le) (sub_nonneg.mpr h) - tr := by - simp [HermitianMat.trace_smul, HermitianMat.trace_sub, γ.tr, ω.tr] - field_simp [hden.ne'] - ring_nf - -/-- A binary coin lifted to the working universe. -/ -private def uliftCoin (p : Prob) : ProbDistribution (ULift.{u} (Fin 2)) := - (ProbDistribution.congr Equiv.ulift.symm) (.coin p) - -private def cqPrepareChoiH {κ : Type u} [Fintype κ] [DecidableEq κ] (τ : κ → MState d) : - HermitianMat (d × κ) ℂ := - ∑ i, HermitianMat.kronecker (τ i).M (MState.ofClassical (.constant i)).M - -private def cqPrepareChoi {κ : Type u} [Fintype κ] [DecidableEq κ] (τ : κ → MState d) : - Matrix (d × κ) (d × κ) ℂ := - (cqPrepareChoiH (d := d) τ).mat - -private def cqPrepareMap {κ : Type u} [Fintype κ] [DecidableEq κ] (τ : κ → MState d) : - MatrixMap κ d ℂ where - toFun X := fun b₁ b₂ => ∑ i, X i i * (τ i).m b₁ b₂ - map_add' X Y := by - ext b₁ b₂ - simp [Matrix.add_apply, Finset.sum_add_distrib, add_mul] - map_smul' c X := by - ext b₁ b₂ - simp [Matrix.smul_apply, Finset.mul_sum, mul_assoc] - -private theorem cqPrepareMap_choi {κ : Type u} [Fintype κ] [DecidableEq κ] (τ : κ → MState d) : - (cqPrepareMap (d := d) τ).choi_matrix = cqPrepareChoi (d := d) τ := by - ext ⟨b₁, a₁⟩ ⟨b₂, a₂⟩ - simp only [MatrixMap.choi_matrix, cqPrepareMap, Matrix.single, - cqPrepareChoi, cqPrepareChoiH, HermitianMat.mat_finset_sum, Matrix.sum_apply] - refine Finset.sum_congr rfl fun x _ => ?_ - show (if a₁ = x ∧ a₂ = x then 1 else 0) * (τ x).m b₁ b₂ = - (τ x).m b₁ b₂ * (HermitianMat.diagonal ℂ (fun x₁ => ((ProbDistribution.constant x) x₁ : ℝ))).mat a₁ a₂ - rw [HermitianMat.diagonal_mat] - aesop (add simp [Matrix.diagonal, ProbDistribution.constant_eq, Ne.symm]) - -private theorem cqPrepareChoi_psd {κ : Type u} [Fintype κ] [DecidableEq κ] (τ : κ → MState d) : - (cqPrepareChoi (d := d) τ).PosSemidef := by - change ((cqPrepareChoiH (d := d) τ).mat).PosSemidef - have hnonneg : (0 : HermitianMat (d × κ) ℂ) ≤ cqPrepareChoiH (d := d) τ := by - unfold cqPrepareChoiH - exact Finset.sum_nonneg fun i _ => - HermitianMat.kronecker_nonneg (τ i).nonneg (MState.ofClassical (.constant i)).nonneg - exact HermitianMat.zero_le_iff.mp hnonneg - -private theorem cqPrepareChoi_traceLeft {κ : Type u} [Fintype κ] [DecidableEq κ] - (τ : κ → MState d) : - (cqPrepareChoi (d := d) τ).traceLeft = 1 := by - rw [← cqPrepareMap_choi (d := d) τ, ← MatrixMap.IsTracePreserving_iff_trace_choi] - intro X - change ∑ x, ∑ i, X i i * (τ i).m x x = X.trace - rw [Finset.sum_comm] - refine Finset.sum_congr rfl fun i _ => ?_ - rw [← Finset.mul_sum, show ∑ x, (τ i).m x x = 1 by - simpa [Matrix.trace] using (MState.tr' (ρ := τ i))] - simp [Matrix.diag_apply] - -private def cqPrepareCPTP {κ : Type u} [Fintype κ] [DecidableEq κ] (τ : κ → MState d) : - CPTPMap κ d := - CPTPMap.CPTP_of_choi_PSD_Tr - (M := cqPrepareChoi (d := d) τ) - (cqPrepareChoi_psd (d := d) τ) - (cqPrepareChoi_traceLeft (d := d) τ) - -private theorem cqPrepare_apply_ofClassical {κ : Type u} [Fintype κ] [DecidableEq κ] - (τ : κ → MState d) (dist : ProbDistribution κ) : - MatrixMap.of_choi_matrix (cqPrepareChoi (d := d) τ) (MState.ofClassical dist).m - = ∑ i, (dist i : ℝ) • (τ i).m := by - rw [← cqPrepareMap_choi (d := d) τ, MatrixMap.choi_map_inv] - ext b₁ b₂ - change ∑ i, (Matrix.diagonal fun x => ((dist x : Prob) : ℂ)) i i * (τ i).m b₁ b₂ = - (∑ i, (dist i : ℝ) • (τ i).m) b₁ b₂ - rw [Matrix.sum_apply] - simp [Matrix.smul_apply] - -private theorem cqPrepare_apply_uliftCoin (τ : ULift (Fin 2) → MState d) (p : Prob) : - MatrixMap.of_choi_matrix (cqPrepareChoi (d := d) τ) (MState.ofClassical (uliftCoin p)).m = - (p : ℝ) • (τ (ULift.up (0 : Fin 2))).m + - ((1 - p : Prob) : ℝ) • (τ (ULift.up (1 : Fin 2))).m := by - rw [cqPrepare_apply_ofClassical (d := d) τ (uliftCoin p)] - ext i j - simp only [Matrix.sum_apply, Matrix.smul_apply, Complex.real_smul] - have hsum : - (∑ x : ULift (Fin 2), ↑↑((uliftCoin p) x) * (τ x).m i j) = - ∑ y : Fin 2, ↑↑((ProbDistribution.coin p) y) * (τ (ULift.up y)).m i j := by - simpa [uliftCoin, ProbDistribution.congr_apply] using - (Equiv.sum_comp (Equiv.ulift : ULift (Fin 2) ≃ Fin 2) - (fun y : Fin 2 => ↑↑((ProbDistribution.coin p) y) * (τ (ULift.up y)).m i j)) - rw [hsum] - simp [Fin.sum_univ_two] - - -private def binaryClassicalPostprocess (a b : Prob) : - CPTPMap (ULift (Fin 2)) (ULift (Fin 2)) := - let τ : ULift (Fin 2) → MState (ULift (Fin 2)) := fun i => - if i = ULift.up (0 : Fin 2) then MState.ofClassical (uliftCoin a) - else MState.ofClassical (uliftCoin b) - CPTPMap.CPTP_of_choi_PSD_Tr - (M := cqPrepareChoi (d := ULift (Fin 2)) τ) - (cqPrepareChoi_psd (d := ULift (Fin 2)) τ) - (cqPrepareChoi_traceLeft (d := ULift (Fin 2)) τ) - -private theorem binaryClassicalPostprocess_apply (a b p : Prob) : - binaryClassicalPostprocess a b (MState.ofClassical (uliftCoin p)) = - MState.ofClassical (uliftCoin (Prob.mix p a b)) := by - apply MState.ext_m - change MatrixMap.of_choi_matrix - (cqPrepareChoi (d := ULift (Fin 2)) - (fun i : ULift (Fin 2) => - if i = ULift.up (0 : Fin 2) then MState.ofClassical (uliftCoin a) - else MState.ofClassical (uliftCoin b))) - (MState.ofClassical (uliftCoin p)).m = - (MState.ofClassical (uliftCoin (Prob.mix p a b))).m - rw [cqPrepare_apply_uliftCoin] - ext i j - rcases i with ⟨i⟩ - rcases j with ⟨j⟩ - fin_cases i <;> fin_cases j - all_goals - simp [MState.m, MState.ofClassical, Matrix.add_apply, Prob.coe_one_minus, uliftCoin, - ProbDistribution.congr_apply] - rw [← HermitianMat.mat_apply, HermitianMat.diagonal_mat] - simp [Matrix.diagonal, Prob.mix, Mixable.mix, Mixable.mix_ab, Prob.coe_one_minus] - all_goals ring_nf - -private theorem uliftCoin_support_top (p : Prob) (hp0 : 0 < (p : ℝ)) (hp1 : (p : ℝ) < 1) : - (MState.ofClassical (uliftCoin p)).M.support = ⊤ := by - rw [← HermitianMat.nonSingular_iff_support_top] - apply HermitianMat.nonSingular_of_posDef - rw [MState.coe_ofClassical] - apply Matrix.PosDef.diagonal - intro i - rcases i with ⟨i⟩ - fin_cases i - · simpa [Complex.real_lt_real, uliftCoin, ProbDistribution.congr_apply] using hp0 - · simp [uliftCoin, ProbDistribution.congr_apply, Prob.coe_one_minus] - exact_mod_cast hp1 - -private def classicalIndicatorEffect {κ : Type u} [DecidableEq κ] (A : Set κ) : - HermitianMat κ ℂ := by classical exact HermitianMat.diagonal ℂ fun x => if x ∈ A then 1 else 0 - -private theorem ofClassical_exp_val_indicator - {κ : Type u} [Fintype κ] [DecidableEq κ] (dist : ProbDistribution κ) (A : Set κ) - [DecidablePred (fun x => x ∈ A)] : - (MState.ofClassical dist).exp_val (classicalIndicatorEffect A) = - ∑ x, if x ∈ A then (dist x : ℝ) else 0 := by - rw [classicalIndicatorEffect, MState.exp_val, MState.coe_ofClassical, - HermitianMat.inner_eq_re_trace] - simp [Matrix.trace, HermitianMat.diagonal] - exact Finset.sum_congr rfl fun _ _ => by split_ifs <;> simp - -private theorem exists_effect_exp_val_ne_of_ne (ρ σ : MState d) (hne : ρ ≠ σ) : - ∃ T : HermitianMat d ℂ, (0 ≤ T ∧ T ≤ 1) ∧ ρ.exp_val T ≠ σ.exp_val T := by - let A : HermitianMat d ℂ := ρ.M - σ.M - have hA_not_nonneg : ¬ 0 ≤ A := by - intro hA_nonneg - exact hne (MState.ext (eq_of_sub_eq_zero (HermitianMat.ext <| - (Matrix.PosSemidef.trace_eq_zero_iff (HermitianMat.zero_le_iff.mp hA_nonneg)).1 <| - (HermitianMat.trace_eq_zero_iff (A := A)).1 - (by simp [A, HermitianMat.trace_sub, ρ.tr, σ.tr])))) - let B : HermitianMat d ℂ := A⁻ - have hB_nonneg : 0 ≤ B := by - simpa [B] using HermitianMat.negPart_nonneg A - have hinner_neg : inner ℝ A B < 0 := by - simpa [B] using (HermitianMat.inner_negPart_neg_iff (A := A)).2 hA_not_nonneg - have hB_trace_pos : 0 < B.trace := by - refine lt_of_le_of_ne (HermitianMat.trace_nonneg hB_nonneg) ?_ - intro htrace - have hB_zero : B = 0 := HermitianMat.ext <| - (Matrix.PosSemidef.trace_eq_zero_iff (HermitianMat.zero_le_iff.mp hB_nonneg)).1 <| - (HermitianMat.trace_eq_zero_iff (A := B)).1 htrace.symm - rw [hB_zero] at hinner_neg - simp at hinner_neg - let T : HermitianMat d ℂ := B.trace⁻¹ • B - have hT_nonneg : 0 ≤ T := by - simpa [T] using smul_nonneg (inv_nonneg.mpr hB_trace_pos.le) hB_nonneg - have hT_le_one : T ≤ 1 := by - dsimp [T] - simpa [smul_smul, inv_mul_cancel₀ hB_trace_pos.ne'] using - smul_le_smul_of_nonneg_left (HermitianMat.le_trace_smul_one hB_nonneg) - (inv_nonneg.mpr hB_trace_pos.le) - refine ⟨T, ⟨hT_nonneg, hT_le_one⟩, fun hsame => ?_⟩ - have hzero : inner ℝ A T = 0 := by - simpa [A, MState.exp_val, inner_sub_left] using sub_eq_zero.mpr hsame - have hneg : inner ℝ A T < 0 := by - simpa [T, inner_smul_right] using - mul_neg_of_pos_of_neg (inv_pos.mpr hB_trace_pos) hinner_neg - linarith - -private def tauOfLE (N : ℕ) (hN : 0 < N) (ρ σ : MState d) - (h : ρ.M ≤ ((N + 1 : ℝ) • σ.M)) : MState d where - M := ((N : ℝ)⁻¹) • (((N + 1 : ℝ) • σ.M) - ρ.M) - nonneg := smul_nonneg (by positivity) (sub_nonneg.mpr h) - tr := by - have hN' : (N : ℝ) ≠ 0 := by positivity - simp [HermitianMat.trace_sub, σ.tr, ρ.tr, hN'] - -private theorem cqPrepareCPTP_uniform_tauOfLE - (M : ℕ) (hM_pos : 0 < M) (ρ σ : MState d) - (h : ρ.M ≤ ((M + 1 : ℝ) • σ.M)) : - cqPrepareCPTP (d := d) (fun i : ULift (Fin (M + 1)) => - if i = ⟨0⟩ then ρ else tauOfLE (d := d) M hM_pos ρ σ h) - (MState.uniform : MState (ULift (Fin (M + 1)))) = σ := by - let x0 : ULift (Fin (M + 1)) := ⟨0⟩ - let τr := tauOfLE (d := d) M hM_pos ρ σ h - let τ : ULift (Fin (M + 1)) → MState d := fun i => if i = x0 then ρ else τr - change cqPrepareCPTP (d := d) τ (MState.uniform : MState (ULift (Fin (M + 1)))) = σ - apply MState.ext_m - change MatrixMap.of_choi_matrix - (cqPrepareChoi (d := d) τ) - (MState.ofClassical ProbDistribution.uniform).m = σ.m - rw [cqPrepare_apply_ofClassical (d := d) τ ProbDistribution.uniform] - ext i j - simp only [ProbDistribution.uniform_def, Matrix.sum_apply, Matrix.smul_apply, - Complex.real_smul, Finset.card_univ, Fintype.card_ulift, Fintype.card_fin, one_div, - Nat.cast_add, Nat.cast_one, Complex.ofReal_inv, Complex.ofReal_add, - Complex.ofReal_natCast, Complex.ofReal_one] - rw [(Finset.sum_erase_add (s := Finset.univ) (a := x0) - (f := fun x : ULift (Fin (M + 1)) => - (↑M + 1 : ℂ)⁻¹ * (if x = x0 then ρ else τr).m i j) (by simp)).symm] - have hrest : - Finset.sum (Finset.erase Finset.univ x0) - (fun x : ULift (Fin (M + 1)) => - (↑M + 1 : ℂ)⁻¹ * (if x = x0 then ρ else τr).m i j) - = - M * ((↑M + 1 : ℂ)⁻¹ * τr.m i j) := by - trans Finset.sum (Finset.erase Finset.univ x0) - (fun _ : ULift (Fin (M + 1)) => (↑M + 1 : ℂ)⁻¹ * τr.m i j) - · exact Finset.sum_congr rfl fun x hx => by simp [(Finset.mem_erase.mp hx).1] - · simp [x0] - rw [hrest] - dsimp [τr] - simp [tauOfLE, MState.m] - field_simp [show (M : ℂ) ≠ 0 by exact_mod_cast Nat.ne_of_gt hM_pos, - show (M + 1 : ℂ) ≠ 0 by exact_mod_cast Nat.succ_ne_zero M] - simp only [← HermitianMat.mat_apply, HermitianMat.mat_sub, HermitianMat.mat_smul, - Matrix.sub_apply, Matrix.smul_apply] - rw [Complex.real_smul] - norm_num - -private theorem integer_bound_aux (N : ℕ) (ρ σ : MState d) - (h : ρ.M ≤ ((N + 1 : ℝ) • σ.M)) : - f ρ σ.M ≤ ENNReal.ofReal (Real.log (N + 1)) := by - cases N with - | zero => - have hEq : ρ = σ := MState.ext <| (eq_of_sub_eq_zero (HermitianMat.ext <| - (Matrix.PosSemidef.trace_eq_zero_iff (HermitianMat.zero_le_iff.mp <| - show 0 ≤ σ.M - ρ.M by simpa using sub_nonneg.mpr (show ρ.M ≤ σ.M by - simpa using h))).1 <| - (HermitianMat.trace_eq_zero_iff (A := σ.M - ρ.M)).1 - (by simp [σ.tr, ρ.tr]))).symm - subst hEq - simp - | succ N => - let κ := ULift (Fin (N + 2)) - let x0 : κ := ⟨0⟩ - let τrest := tauOfLE (d := d) (N + 1) (Nat.succ_pos _) ρ σ h - let τ : κ → MState d := fun i => if i = x0 then ρ else τrest - let Λ : CPTPMap κ d := cqPrepareCPTP (d := d) τ - have hconst : Λ (MState.ofClassical (.constant x0)) = ρ := by - apply MState.ext_m - change MatrixMap.of_choi_matrix (cqPrepareChoi (d := d) τ) - (MState.ofClassical (.constant x0)).m = ρ.m - rw [cqPrepare_apply_ofClassical (d := d) τ (.constant x0)] - ext i j - rw [Finset.sum_eq_single x0] - · simp [τ, ProbDistribution.constant_eq] - · intro y _ hyx - simp [ProbDistribution.constant_eq, hyx, eq_comm] - · simp - have huniform : Λ (MState.uniform : MState κ) = σ := by - simpa [Λ, κ, τ, τrest] using - cqPrepareCPTP_uniform_tauOfLE (d := d) (N + 1) (Nat.succ_pos _) ρ σ h - calc - f ρ σ.M = - f (Λ (MState.ofClassical (.constant x0))) - ((Λ (MState.uniform : MState κ)).M) := by - rw [hconst, huniform] - _ ≤ f (MState.ofClassical (.constant x0)) (MState.uniform : MState κ).M := DPI _ _ Λ - _ = ENNReal.ofReal (Real.log (N + 2)) := by - simpa [κ, ENNReal.some_eq_coe, - ENNReal.ofReal_eq_coe_nnreal (Real.log_nonneg - (by - have := (Nat.cast_nonneg N : (0 : ℝ) ≤ N) - linarith : (1 : ℝ) ≤ (N + 2 : ℝ)))] using - (RelEntropy.normalized (f := f) (d := κ) x0) - _ = ENNReal.ofReal (Real.log (↑(N + 1) + 1)) := by - norm_num [Nat.cast_add, add_assoc, add_comm, add_left_comm] - -private def dyadicStatePow (ρ : MState d) : ∀ n, MState (DyadicPow d n) - | 0 => ρ - | n + 1 => dyadicStatePow ρ n ⊗ᴹ dyadicStatePow ρ n - -private theorem dyadicStatePow_ofClassical (dist : ProbDistribution d) : - ∀ n, dyadicStatePow (MState.ofClassical dist) n = - MState.ofClassical (dyadicProbPow dist n) := by - intro n - induction n with - | zero => rfl - | succ n ih => - rw [dyadicStatePow, ih] - change _ = MState.ofClassical (ProbDistribution.prod _ _) - ext i j - simp [MState.prod, MState.ofClassical, ProbDistribution.prod, - HermitianMat.kronecker_diagonal] - -private theorem hellingerOverlap_uliftCoin (p q : Prob) : - hellingerOverlap (uliftCoin p) (uliftCoin q) = - Real.sqrt ((p : ℝ) * (q : ℝ)) + - Real.sqrt ((1 - (p : ℝ)) * (1 - (q : ℝ))) := by - change (∑ x : ULift (Fin 2), - Real.sqrt (((ProbDistribution.coin p) x.down : ℝ) * - ((ProbDistribution.coin q) x.down : ℝ))) = _ - simpa [Fin.sum_univ_two] using - (Equiv.sum_comp (Equiv.ulift : ULift (Fin 2) ≃ Fin 2) - fun y : Fin 2 => Real.sqrt (((ProbDistribution.coin p) y : ℝ) * - ((ProbDistribution.coin q) y : ℝ))) - -private theorem exists_likelihood_indicator_effect - {κ : Type u} [Fintype κ] [DecidableEq κ] (P Q : ProbDistribution κ) (s r : Prob) - (hoverlap_s : hellingerOverlap P Q ≤ (s : ℝ)) - (hoverlap_r : hellingerOverlap P Q ≤ 1 - (r : ℝ)) : - ∃ T : HermitianMat κ ℂ, (0 ≤ T ∧ T ≤ 1) ∧ - ∃ α β : Prob, - (MState.ofClassical P).exp_val T = α ∧ - (MState.ofClassical Q).exp_val T = β ∧ - (α : ℝ) ≤ s ∧ (r : ℝ) ≤ β := by - classical - let A : Set κ := {x | (P x : ℝ) ≤ Q x} - let T : HermitianMat κ ℂ := classicalIndicatorEffect A - have hT : 0 ≤ T ∧ T ≤ 1 := by - refine ⟨?_, ?_⟩ - · rw [HermitianMat.zero_le_iff] - simp [T, classicalIndicatorEffect, HermitianMat.diagonal_mat, Matrix.posSemidef_diagonal_iff] - exact fun i => by by_cases hi : i ∈ A <;> simp [hi] - · rw [← sub_nonneg] - rw [show T = HermitianMat.diagonal ℂ fun x => if x ∈ A then (1 : ℝ) else 0 from rfl, - ← HermitianMat.diagonal_one (𝕜 := ℂ), - ← HermitianMat.diagonal_sub, HermitianMat.zero_le_iff, HermitianMat.diagonal_mat, - Matrix.posSemidef_diagonal_iff] - exact fun i => by by_cases hi : i ∈ A <;> simp [hi] - refine ⟨T, hT, - ⟨(MState.ofClassical P).exp_val T, (MState.ofClassical P).exp_val_prob hT⟩, - ⟨(MState.ofClassical Q).exp_val T, (MState.ofClassical Q).exp_val_prob hT⟩, - rfl, rfl, ?_, ?_⟩ - · change (MState.ofClassical P).exp_val T ≤ (s : ℝ) - rw [ofClassical_exp_val_indicator] - exact (show ∑ x, (if (P x : ℝ) ≤ Q x then (P x : ℝ) else 0) ≤ - hellingerOverlap P Q by - rw [hellingerOverlap] - refine Finset.sum_le_sum ?_ - intro x _ - by_cases hx : (P x : ℝ) ≤ Q x - · simpa [hx] using Real.le_sqrt (P x).2.1 (mul_nonneg (P x).2.1 (Q x).2.1) |>.2 - (by simpa [pow_two] using mul_le_mul_of_nonneg_left hx (P x).2.1) - · simpa [hx] using Real.sqrt_nonneg ((P x : ℝ) * (Q x : ℝ))).trans hoverlap_s - · change (r : ℝ) ≤ (MState.ofClassical Q).exp_val T - rw [ofClassical_exp_val_indicator] - change (r : ℝ) ≤ ∑ x, (if (P x : ℝ) ≤ Q x then (Q x : ℝ) else 0) - have hcompl : ∑ x, (if (P x : ℝ) ≤ Q x then 0 else (Q x : ℝ)) ≤ - hellingerOverlap P Q := by - rw [hellingerOverlap] - refine Finset.sum_le_sum ?_ - intro x _ - by_cases hx : (P x : ℝ) ≤ Q x - · simpa [hx] using Real.sqrt_nonneg ((P x : ℝ) * (Q x : ℝ)) - · rw [mul_comm] - simpa [hx] using Real.le_sqrt (Q x).2.1 (mul_nonneg (Q x).2.1 (P x).2.1) |>.2 - (by simpa [pow_two] using - mul_le_mul_of_nonneg_left (le_of_not_ge hx) (Q x).2.1) - have htotal' : - (∑ x, (if (P x : ℝ) ≤ Q x then 0 else (Q x : ℝ))) + - (∑ x, (if (P x : ℝ) ≤ Q x then (Q x : ℝ) else 0)) = - 1 := by - rw [← Finset.sum_add_distrib] - convert Q.normalized using 1 - exact Finset.sum_congr rfl fun x _ => by by_cases hx : (P x : ℝ) ≤ Q x <;> simp [hx] - linarith - -private theorem exists_dyadic_binary_effect_le_ge - (p q s r : Prob) (hpq : (p : ℝ) < q) - (hs_pos : 0 < (s : ℝ)) (hr_lt_one : (r : ℝ) < 1) : - ∃ (n : ℕ) (T : HermitianMat (DyadicPow (ULift.{u} (Fin 2)) n) ℂ), - (0 ≤ T ∧ T ≤ 1) ∧ ∃ α β : Prob, - (dyadicStatePow (MState.ofClassical (uliftCoin p)) n).exp_val T = α ∧ - (dyadicStatePow (MState.ofClassical (uliftCoin q)) n).exp_val T = β ∧ - (α : ℝ) ≤ s ∧ (r : ℝ) ≤ β := by - let ε : ℝ := (s : ℝ) ⊓ (1 - (r : ℝ)) - have ha1 : hellingerOverlap (uliftCoin p) (uliftCoin q) < 1 := by - rw [hellingerOverlap_uliftCoin] - simpa [hellingerOverlap_coin] using hellingerOverlap_coin_lt_one p q hpq - obtain ⟨n, hn'⟩ := exists_pow_lt_of_lt_one - (show 0 < ε by simpa [ε] using lt_inf_iff.mpr ⟨hs_pos, sub_pos.mpr hr_lt_one⟩) ha1 - have hn : (hellingerOverlap (uliftCoin p) (uliftCoin q)) ^ (2 ^ n : ℕ) < ε := lt_of_le_of_lt - (pow_le_pow_of_le_one (by rw [hellingerOverlap_uliftCoin]; positivity) ha1.le - (Nat.lt_two_pow_self (n := n)).le) hn' - have hoverlap_lt : - hellingerOverlap (dyadicProbPow (uliftCoin p) n) (dyadicProbPow (uliftCoin q) n) < ε := by - rw [hellingerOverlap_dyadicProbPow] - exact hn - obtain ⟨T, hT, α, β, hpT, hqT, hαs, hrβ⟩ := - exists_likelihood_indicator_effect - (dyadicProbPow (uliftCoin p) n) (dyadicProbPow (uliftCoin q) n) s r - (hoverlap_lt.le.trans inf_le_left) (hoverlap_lt.le.trans inf_le_right) - exact ⟨n, T, hT, α, β, by simpa [dyadicStatePow_ofClassical] using hpT, - by simpa [dyadicStatePow_ofClassical] using hqT, hαs, hrβ⟩ - -private def dyadicCPTPMapPow {e : Type u} [Fintype e] [DecidableEq e] - (Λ : CPTPMap d e) : ∀ n, CPTPMap (DyadicPow d n) (DyadicPow e n) - | 0 => Λ - | n + 1 => dyadicCPTPMapPow Λ n ⊗ᶜᵖ dyadicCPTPMapPow Λ n - -/-- Universe-lifted two-outcome POVM associated to an effect `0 ≤ T ≤ 1`. -/ -private def binaryPOVMOfEffectULift (T : HermitianMat d ℂ) (hT : 0 ≤ T ∧ T ≤ 1) : - POVM (ULift (Fin 2)) d where - mats i := if i = ULift.up (0 : Fin 2) then T else 1 - T - nonneg i := by - split - · exact hT.1 - · exact HermitianMat.zero_le_iff.mpr hT.2 - normalized := by - have hsum : - (∑ i : ULift (Fin 2), if i = ULift.up (0 : Fin 2) then T else 1 - T) = - ∑ i : Fin 2, if ULift.up i = ULift.up (0 : Fin 2) then T else 1 - T := by - refine Fintype.sum_equiv Equiv.ulift - (fun i : ULift (Fin 2) => if i = ULift.up (0 : Fin 2) then T else 1 - T) - (fun i : Fin 2 => if ULift.up i = ULift.up (0 : Fin 2) then T else 1 - T) ?_ - rintro ⟨x⟩ - rfl - rw [hsum] - simp [Fin.sum_univ_two] - -/-- Measuring a lifted binary effect and discarding the post-measurement state gives a lifted coin. -/ -private theorem binaryPOVMOfEffectULift_measureDiscard_apply - (T : HermitianMat d ℂ) (hT : 0 ≤ T ∧ T ≤ 1) (ρ : MState d) : - (binaryPOVMOfEffectULift T hT).measureDiscard ρ = - MState.ofClassical (uliftCoin ⟨ρ.exp_val T, ρ.exp_val_prob hT⟩) := by - rw [POVM.measureDiscard_apply] - congr 1 - let p : Prob := ⟨ρ.exp_val T, ρ.exp_val_prob hT⟩ - ext i - rcases i with ⟨i⟩ - fin_cases i - · let z : ULift.{u} (Fin 2) := ULift.up (0 : Fin 2) - change inner ℝ T ρ.M = ((uliftCoin p) z : ℝ) - simp [z, p, uliftCoin, ProbDistribution.congr_apply, MState.exp_val, HermitianMat.inner_comm] - · let o : ULift.{u} (Fin 2) := ULift.up (1 : Fin 2) - change inner ℝ (1 - T) ρ.M = ((uliftCoin p) o : ℝ) - simp [o, p, uliftCoin, ProbDistribution.congr_apply, Prob.coe_one_minus, - MState.exp_val, HermitianMat.inner_comm, inner_sub_right, HermitianMat.inner_one, ρ.tr] - -private theorem dyadicStatePow_relEntropy (ρ σ : MState d) : - ∀ n, f (dyadicStatePow ρ n) (dyadicStatePow σ n).M = ((2 ^ n : ℕ) : ENNReal) * f ρ σ := by - intro n - induction n with - | zero => simp [dyadicStatePow]; rfl - | succ n ih => - show f (dyadicStatePow ρ n ⊗ᴹ dyadicStatePow ρ n) - ↑(dyadicStatePow σ n ⊗ᴹ dyadicStatePow σ n) = _ - rw [RelEntropy.of_kron (f := f), ih] - rw [← mul_add, ← two_mul, pow_succ, Nat.cast_mul] - ring - -private theorem exists_binary_measurement_of_ne (ρ σ : MState d) (hne : ρ ≠ σ) : - ∃ p q : Prob, (p : ℝ) < (q : ℝ) ∧ - ∃ Λ : CPTPMap d (ULift.{u} (Fin 2)), - Λ ρ = MState.ofClassical (uliftCoin p) ∧ - Λ σ = MState.ofClassical (uliftCoin q) := by - obtain ⟨T, hT, hT_ne⟩ := exists_effect_exp_val_ne_of_ne ρ σ hne - let p : Prob := ⟨ρ.exp_val T, ρ.exp_val_prob hT⟩ - let q : Prob := ⟨σ.exp_val T, σ.exp_val_prob hT⟩ - by_cases hpq : (p : ℝ) < q - · exact ⟨p, q, hpq, (binaryPOVMOfEffectULift T hT).measureDiscard, - by rw [binaryPOVMOfEffectULift_measureDiscard_apply], - by rw [binaryPOVMOfEffectULift_measureDiscard_apply]⟩ - · let T' : HermitianMat d ℂ := 1 - T - have hT' : 0 ≤ T' ∧ T' ≤ 1 := by - refine ⟨by dsimp [T']; exact HermitianMat.zero_le_iff.mpr hT.2, ?_⟩ - dsimp [T'] - rw [sub_le_iff_le_add] - simpa using hT.1 - have hpq' : ((1 - p : Prob) : ℝ) < (1 - q : Prob) := by - rw [Prob.coe_one_minus, Prob.coe_one_minus] - linarith [lt_of_le_of_ne (le_of_not_gt hpq) (fun heq => hT_ne heq.symm)] - refine ⟨1 - p, 1 - q, hpq', (binaryPOVMOfEffectULift T' hT').measureDiscard, ?_, ?_⟩ <;> - rw [binaryPOVMOfEffectULift_measureDiscard_apply] <;> - congr 2 <;> - apply Subtype.ext <;> - simp [T', p, q, MState.exp_val_sub, MState.exp_val_one, Prob.coe_one_minus] - -private theorem exists_binary_postprocess {α β s r : Prob} - (hαs : (α : ℝ) ≤ s) (hsr : (s : ℝ) < r) (hrβ : (r : ℝ) ≤ β) : - ∃ a b : Prob, Prob.mix α a b = s ∧ Prob.mix β a b = r := by - let A : ℝ := α - let B : ℝ := β - let S : ℝ := s - let R : ℝ := r - have hAB : A < B := by dsimp [A, B, S, R] at *; linarith - let k : ℝ := (R - S) / (B - A) - have hk_nonneg : 0 ≤ k := by - dsimp [k] - exact div_nonneg (sub_nonneg.mpr (by dsimp [S, R]; exact hsr.le)) - (sub_nonneg.mpr hAB.le) - have hk_le_one : k ≤ 1 := by - dsimp [k] - rw [div_le_one (sub_pos.mpr hAB)] - dsimp [A, B, S, R] at * - linarith - let bR : ℝ := S - A * k - let aR : ℝ := bR + k - have hbR_nonneg : 0 ≤ bR := by - dsimp [bR, A, S] at * - linarith [mul_le_mul_of_nonneg_left hk_le_one α.2.1] - have hbR_le_one : bR ≤ 1 := by - dsimp [bR, S] - nlinarith [s.2.2, α.2.1, hk_nonneg] - have haR_nonneg : 0 ≤ aR := by dsimp [aR]; positivity - have haR_le_one : aR ≤ 1 := by - have hden_pos : 0 < B - A := sub_pos.mpr hAB - have hmain : - S * (B - A) + (1 - A) * (R - S) ≤ 1 * (B - A) := by - nlinarith [ - mul_le_mul_of_nonneg_right (show R ≤ B by dsimp [R, B] at hrβ ⊢; exact hrβ) - (show 0 ≤ 1 - A by dsimp [A]; linarith [α.2.2]), - mul_le_mul_of_nonpos_right (show A ≤ S by dsimp [A, S] at hαs ⊢; exact hαs) - (show B - 1 ≤ 0 by dsimp [B]; linarith [β.2.2])] - rw [show aR = (S * (B - A) + (1 - A) * (R - S)) / (B - A) by - dsimp [aR, bR, k] - field_simp [hden_pos.ne'] - ring, div_le_one hden_pos] - simpa using hmain - let a : Prob := ⟨aR, haR_nonneg, haR_le_one⟩ - let b : Prob := ⟨bR, hbR_nonneg, hbR_le_one⟩ - refine ⟨a, b, ?_, ?_⟩ - all_goals - ext - simp [Prob.mix, Mixable.mix, Mixable.mix_ab, Prob.coe_one_minus, a, b, aR, bR, k, A, B, S, R] - · - ring - · - field_simp [show (↑β : ℝ) - ↑α ≠ 0 by dsimp [A, B] at hAB; linarith] - ring - -section nontrivial -variable [RelEntropy.Nontrivial f] - -/-- From Tomamichel nontriviality, extract a strictly positive binary classical pair with -full-support states. This is the finite binary witness used in the proof of `faithful`. -/ -private theorem exists_positive_binary_pair : - ∃ p q : Prob, 0 < (p : ℝ) ∧ (p : ℝ) < q ∧ (q : ℝ) < 1 ∧ - (MState.ofClassical (uliftCoin.{u} p)).M.support = ⊤ ∧ - (MState.ofClassical (uliftCoin.{u} q)).M.support = ⊤ ∧ - 0 < f (MState.ofClassical (uliftCoin.{u} p)) - (MState.ofClassical (uliftCoin.{u} q)).M := by - obtain ⟨s, t, hs0, -, ht0, -, hs_order, hsSupport, htSupport, hpos⟩ : - ∃ s t : Prob, - 0 < (s : ℝ) ∧ (s : ℝ) < 1 / 2 ∧ - 0 < (t : ℝ) ∧ (t : ℝ) < 1 / 2 ∧ - (s : ℝ) < ((1 - t : Prob) : ℝ) ∧ - (MState.ofClassical (uliftCoin s)).M.support = ⊤ ∧ - (MState.ofClassical (uliftCoin (1 - t))).M.support = ⊤ ∧ - 0 < f (MState.ofClassical (uliftCoin s)) - (MState.ofClassical (uliftCoin (1 - t))).M := by - obtain ⟨d, instFintype, instDecidableEq, γ, ω, hγ, hω, hpos⟩ := - RelEntropy.Nontrivial.nontrivial (f := f) - letI : Fintype d := instFintype - letI : DecidableEq d := instDecidableEq - obtain ⟨s, t, hs0, hslt, ht0, htlt, hleft, hright⟩ : - ∃ s t : Prob, 0 < (s : ℝ) ∧ (s : ℝ) < 1 / 2 ∧ - 0 < (t : ℝ) ∧ (t : ℝ) < 1 / 2 ∧ - (t : ℝ) • γ.M ≤ (1 - (s : ℝ)) • ω.M ∧ - (s : ℝ) • ω.M ≤ (1 - (t : ℝ)) • γ.M := by - obtain ⟨Nγω, hNγω_pos, hγω⟩ := exists_le_nat_smul_of_fullSupport γ ω hω - obtain ⟨Nωγ, _, hωγ⟩ := exists_le_nat_smul_of_fullSupport ω γ hγ - let K : ℕ := Nat.max Nγω Nωγ - let a : ℝ := 1 / (K + 2 : ℝ) - have hden_pos : (0 : ℝ) < K + 2 := by positivity - have ha_pos : 0 < a := by dsimp [a]; positivity - have ha_lt_half : a < 1 / 2 := by - dsimp [a] - rw [div_lt_iff₀ hden_pos] - nlinarith [show (1 : ℝ) ≤ K by - exact_mod_cast le_trans hNγω_pos (le_max_left Nγω Nωγ)] - have hscale {N : ℕ} (hNK : N ≤ K) : a * (N + 1 : ℝ) ≤ 1 - a := by - dsimp [a] - rw [div_mul_eq_mul_div, one_sub_div hden_pos.ne', - div_le_div_iff_of_pos_right hden_pos] - nlinarith [show (N + 1 : ℝ) ≤ K + 1 by exact_mod_cast Nat.succ_le_succ hNK] - let p : Prob := ⟨a, ha_pos.le, by linarith [ha_lt_half]⟩ - refine ⟨p, p, by simpa [p] using ha_pos, by simpa [p] using ha_lt_half, - by simpa [p] using ha_pos, by simpa [p] using ha_lt_half, ?_, ?_⟩ - · simpa [p] using calc - a • γ.M ≤ a • ((Nγω + 1 : ℝ) • ω.M) := - smul_le_smul_of_nonneg_left hγω ha_pos.le - _ = (a * (Nγω + 1 : ℝ)) • ω.M := by rw [smul_smul] - _ ≤ (1 - a) • ω.M := smul_le_smul_of_nonneg_right - (hscale (le_max_left Nγω Nωγ)) ω.nonneg - · simpa [p] using calc - a • ω.M ≤ a • ((Nωγ + 1 : ℝ) • γ.M) := - smul_le_smul_of_nonneg_left hωγ ha_pos.le - _ = (a * (Nωγ + 1 : ℝ)) • γ.M := by rw [smul_smul] - _ ≤ (1 - a) • γ.M := smul_le_smul_of_nonneg_right - (hscale (le_max_right Nγω Nωγ)) γ.nonneg - have hden : 0 < 1 - (s : ℝ) - (t : ℝ) := by linarith - let τ : ULift.{u} (Fin 2) → MState d := fun i => - if i = ULift.up (0 : Fin 2) then - binaryPrepOne γ ω (s : ℝ) (t : ℝ) hden hleft - else - binaryPrepZero γ ω (s : ℝ) (t : ℝ) hden hright - let Λ : CPTPMap (ULift.{u} (Fin 2)) d := - CPTPMap.CPTP_of_choi_PSD_Tr - (M := cqPrepareChoi (d := d) τ) - (cqPrepareChoi_psd (d := d) τ) - (cqPrepareChoi_traceLeft (d := d) τ) - have hdenC : (1 - ((s : ℝ) : ℂ) - ((t : ℝ) : ℂ)) ≠ 0 := by exact_mod_cast hden.ne' - have hγprep : Λ (MState.ofClassical (uliftCoin s)) = γ := by - apply MState.ext_m - change MatrixMap.of_choi_matrix (cqPrepareChoi (d := d) τ) - (MState.ofClassical (uliftCoin s)).m = γ.m - rw [cqPrepare_apply_uliftCoin, Prob.coe_one_minus] - ext i j - simp [τ, binaryPrepOne, binaryPrepZero, MState.m, Matrix.add_apply, Matrix.sub_apply, - Matrix.smul_apply, -MState.mat_M] - field_simp [hdenC] - ring - have hωprep : Λ (MState.ofClassical (uliftCoin (1 - t))) = ω := by - apply MState.ext_m - change MatrixMap.of_choi_matrix (cqPrepareChoi (d := d) τ) - (MState.ofClassical (uliftCoin (1 - t))).m = ω.m - rw [cqPrepare_apply_uliftCoin, Prob.coe_one_minus, Prob.coe_one_minus] - ext i j - simp [τ, binaryPrepOne, binaryPrepZero, MState.m, Matrix.add_apply, Matrix.sub_apply, - Matrix.smul_apply, -MState.mat_M] - field_simp [hdenC] - ring - refine ⟨s, t, hs0, hslt, ht0, htlt, by rw [Prob.coe_one_minus]; linarith, - uliftCoin_support_top s hs0 (by linarith), - uliftCoin_support_top (1 - t) (by rw [Prob.coe_one_minus]; linarith) - (by rw [Prob.coe_one_minus]; linarith), ?_⟩ - exact lt_of_lt_of_le hpos <| by - simpa [hγprep, hωprep] using DPI (f := f) (MState.ofClassical (uliftCoin s)) - (MState.ofClassical (uliftCoin (1 - t))) Λ - exact ⟨s, 1 - t, hs0, hs_order, by rw [Prob.coe_one_minus]; linarith, - hsSupport, htSupport, hpos⟩ - -/-- A nontrivial relative entropy is **faithful**: it can distinguish when two states are equal. - -The proof (Tomamichel §5) goes by building a binary measurement that separates `ρ` from `σ`, -using DPI to reduce to a classical `Fin 2` distribution, then amplifying with `of_kron` until the -`Nontrivial` axiom forces a strictly positive value. The tensor-power separation step is formalized -via the finite classical likelihood test in `exists_dyadic_binary_effect_le_ge`. -/ -theorem faithful (ρ σ : MState d) : f ρ σ = 0 ↔ ρ = σ := by - constructor - · intro hzero - by_contra hne - obtain ⟨p, q, hpq, Λ, hρ, hσ⟩ := exists_binary_measurement_of_ne ρ σ hne - have hzero_binary : ∀ n, - f (dyadicStatePow (MState.ofClassical (uliftCoin p)) n) - (dyadicStatePow (MState.ofClassical (uliftCoin q)) n).M = 0 := by - intro n - induction n with - | zero => - simpa [dyadicStatePow] using - le_antisymm (by simpa [hρ, hσ, hzero] using RelEntropy.DPI (f := f) ρ σ Λ) bot_le - | succ n ih => - simpa [dyadicStatePow, ih] using - RelEntropy.of_kron (f := f) - (dyadicStatePow (MState.ofClassical (uliftCoin p)) n) - (dyadicStatePow (MState.ofClassical (uliftCoin q)) n) - (dyadicStatePow (MState.ofClassical (uliftCoin p)) n) - (dyadicStatePow (MState.ofClassical (uliftCoin q)) n) - obtain ⟨s, r, hs_pos, hsr, hr_lt_one, _, _, hpos⟩ := - exists_positive_binary_pair (f := f) - obtain ⟨n, T, hT, α, β, hpT, hqT, hαs, hrβ⟩ := - exists_dyadic_binary_effect_le_ge p q s r hpq hs_pos hr_lt_one - suffices 0 < f (dyadicStatePow (MState.ofClassical (uliftCoin p)) n) - (dyadicStatePow (MState.ofClassical (uliftCoin q)) n).M by - simp [hzero_binary n] at this - obtain ⟨a, b, hsmix, hrmix⟩ := exists_binary_postprocess hαs hsr hrβ - let Μ : CPTPMap (DyadicPow (ULift.{u} (Fin 2)) n) (ULift (Fin 2)) := - (binaryPOVMOfEffectULift T hT).measureDiscard - let Λ' : CPTPMap (DyadicPow (ULift.{u} (Fin 2)) n) (ULift (Fin 2)) := - (binaryClassicalPostprocess a b) ∘ₘ Μ - have hOut (x z y : Prob) - (hz : (dyadicStatePow (MState.ofClassical (uliftCoin x)) n).exp_val T = z) - (hy : Prob.mix z a b = y) : - Λ' (dyadicStatePow (MState.ofClassical (uliftCoin x)) n) = - MState.ofClassical (uliftCoin y) := by - have hΜ : Μ (dyadicStatePow (MState.ofClassical (uliftCoin x)) n) = - MState.ofClassical (uliftCoin z) := by - rw [binaryPOVMOfEffectULift_measureDiscard_apply] - exact congrArg (fun x => MState.ofClassical (uliftCoin x)) (Subtype.ext hz) - simpa [Λ', CPTPMap.compose_eq, hΜ, binaryClassicalPostprocess_apply] using - congrArg (fun x => MState.ofClassical (uliftCoin x)) hy - exact lt_of_lt_of_le hpos <| by - simpa [hOut p α s hpT hsmix, hOut q β r hqT hrmix] using DPI (f := f) - (dyadicStatePow (MState.ofClassical (uliftCoin p)) n) - (dyadicStatePow (MState.ofClassical (uliftCoin q)) n) Λ' - · rintro rfl - simp - -/-- In every system with at least two classical points, a nontrivial relative entropy has a -strictly positive value on some pair of full-support states. -/ -theorem exists_fullSupport_positive_of_two_le_card - (d : Type u) [Fintype d] [DecidableEq d] (hd : 2 ≤ Fintype.card d) : - ∃ (ρ σ : MState d), ρ.M.support = ⊤ ∧ σ.M.support = ⊤ ∧ 0 < f ρ σ := by - haveI : Nonempty d := Fintype.card_pos_iff.mp (lt_of_lt_of_le (by norm_num) hd) - let i : d := Classical.arbitrary d - let p : Prob := ⟨1 / 2, by norm_num⟩ - let ρ : MState d := p [MState.ofClassical (.constant i) ↔ MState.uniform] - refine ⟨ρ, MState.uniform, ?_, ?_, ?_⟩ - · haveI : ρ.M.NonSingular := HermitianMat.nonSingular_of_posDef <| by - dsimp [ρ] - exact MState.PosDef_mix_of_ne_one (hσ₂ := MState.uniform_posDef) p - (by dsimp [p]; norm_num [Prob.ext_iff]) - exact HermitianMat.nonSingular_support_top - · haveI : (MState.uniform : MState d).M.NonSingular := - HermitianMat.nonSingular_of_posDef MState.uniform_posDef - exact HermitianMat.nonSingular_support_top - · refine bot_lt_iff_ne_bot.mpr ((faithful (f := f) ρ MState.uniform).not.mpr ?_) - intro hρσ - have hmat := congrArg (fun τ : MState d => τ.M.mat) hρσ - simp [ρ, p, Mixable.mix, Mixable.mix_ab, MState.instMixable, - MState.uniform, MState.ofClassical, ProbDistribution.constant_eq, - ProbDistribution.uniform_def, HermitianMat.diagonal, Mixable.to_U] at hmat - have hdiag_re := congrArg Complex.re (congrFun (congrFun hmat i) i) - simp [Matrix.add_apply] at hdiag_re - norm_num at hdiag_re - nlinarith [inv_lt_one_of_one_lt₀ - (by exact_mod_cast (lt_of_lt_of_le one_lt_two hd) : (1 : ℝ) < Fintype.card d)] - -end nontrivial - - -/-- If `ρ ≤ exp x • σ`, then every axiomatized relative entropy is bounded by `x`. -/ -theorem le_of_le_exp (ρ σ : MState d) {x : ℝ} - (hx : 0 ≤ x) (h : ρ.M ≤ Real.exp x • σ.M) : - f ρ σ.M ≤ ENNReal.ofReal x := by - have hfin : f ρ σ.M ≠ ∞ := - ne_top_of_le_ne_top ENNReal.ofReal_ne_top <| - integer_bound_aux (f := f) (N := Nat.ceil (Real.exp x)) ρ σ <| by - exact h.trans <| smul_le_smul_of_nonneg_right - ((Nat.le_ceil _).trans (by norm_num)) σ.nonneg - by_contra hfx - let δ : ℝ := (f ρ σ.M).toReal - x - have hδ : 0 < δ := by - dsimp [δ]; linarith [(ENNReal.ofReal_lt_iff_lt_toReal hx hfin).1 (lt_of_not_ge hfx)] - let n : ℕ := Nat.ceil (Real.log 3 / δ) + 1 - have hgap : Real.log 3 < (((2 ^ n : ℕ) : ℝ)) * δ := by - exact (div_lt_iff₀ hδ).mp <| lt_of_lt_of_le - (show Real.log 3 / δ < (n : ℝ) by - dsimp [n] - exact lt_of_le_of_lt (Nat.le_ceil (Real.log 3 / δ)) - (by exact_mod_cast Nat.lt_succ_self (Nat.ceil (Real.log 3 / δ)))) - (by exact_mod_cast ((Nat.lt_two_pow_self : n < 2 ^ n).le) : (n : ℝ) ≤ (2 ^ n : ℕ)) - let y : ℝ := (((2 ^ n : ℕ) : ℝ)) * x - have hy_nonneg : 0 ≤ y := by dsimp [y]; positivity - have hpow_le : ∀ m, (dyadicStatePow ρ m).M ≤ - Real.exp ((((2 ^ m : ℕ) : ℝ)) * x) • (dyadicStatePow σ m).M := by - intro m - induction m with - | zero => - simpa [dyadicStatePow] using h - | succ m ih => - have hσ_nonneg : - 0 ≤ Real.exp ((((2 ^ m : ℕ) : ℝ)) * x) • (dyadicStatePow σ m).M := - smul_nonneg (by positivity) (dyadicStatePow σ m).nonneg - have hpow : - ((((2 ^ (m + 1) : ℕ) : ℝ)) * x) = - ((((2 ^ m : ℕ) : ℝ)) * x) + ((((2 ^ m : ℕ) : ℝ)) * x) := by - rw [pow_succ, Nat.cast_mul] - ring - have hunfold : (dyadicStatePow ρ (m + 1)).M - = (dyadicStatePow ρ m).M ⊗ₖ (dyadicStatePow ρ m).M := rfl - have hrhs : Real.exp (((((2 ^ m : ℕ) : ℝ)) * x) + ((((2 ^ m : ℕ) : ℝ)) * x)) • - (dyadicStatePow σ (m + 1)).M - = (Real.exp ((((2 ^ m : ℕ) : ℝ)) * x) • (dyadicStatePow σ m).M) ⊗ₖ - (Real.exp ((((2 ^ m : ℕ) : ℝ)) * x) • (dyadicStatePow σ m).M) := by - have hsk : - (Real.exp ((((2 ^ m : ℕ) : ℝ)) * x) • (dyadicStatePow σ m).M) ⊗ₖ - (Real.exp ((((2 ^ m : ℕ) : ℝ)) * x) • (dyadicStatePow σ m).M) = - (Real.exp ((((2 ^ m : ℕ) : ℝ)) * x) * Real.exp ((((2 ^ m : ℕ) : ℝ)) * x)) • - ((dyadicStatePow σ m).M ⊗ₖ (dyadicStatePow σ m).M) := by - ext1 - simp [Matrix.smul_kronecker, Matrix.kronecker_smul, smul_smul, mul_comm] - simpa [dyadicStatePow, MState.prod, Real.exp_add] using hsk.symm - rw [hunfold, hpow, hrhs] - exact HermitianMat.kronecker_self_mono (dyadicStatePow ρ m).nonneg hσ_nonneg ih - have hpow_bound' : - (((2 ^ n : ℕ) : ENNReal) * f ρ σ.M) ≤ - ENNReal.ofReal (Real.log (Nat.ceil (Real.exp y) + 1)) := by - simpa [dyadicStatePow_relEntropy (f := f) ρ σ n] using - integer_bound_aux (f := f) (N := Nat.ceil (Real.exp y)) - (dyadicStatePow ρ n) (dyadicStatePow σ n) (by - exact (hpow_le n).trans <| smul_le_smul_of_nonneg_right - (by dsimp [y]; exact (Nat.le_ceil _).trans (by norm_num)) - (dyadicStatePow σ n).nonneg) - have hpow_bound_real : - (((2 ^ n : ℕ) : ℝ)) * (f ρ σ.M).toReal ≤ - Real.log (Nat.ceil (Real.exp y) + 1 : ℝ) := by - calc - (((2 ^ n : ℕ) : ℝ)) * (f ρ σ.M).toReal - = ((((2 ^ n : ℕ) : ENNReal) * f ρ σ.M)).toReal := by - rw [ENNReal.toReal_mul, ENNReal.toReal_natCast] - _ ≤ (ENNReal.ofReal (Real.log (Nat.ceil (Real.exp y) + 1 : ℝ))).toReal := - (ENNReal.toReal_le_toReal (ENNReal.mul_ne_top (by simp) hfin) ENNReal.ofReal_ne_top).2 hpow_bound' - _ = Real.log (Nat.ceil (Real.exp y) + 1 : ℝ) := by - rw [ENNReal.toReal_ofReal (Real.log_nonneg (by norm_num))] - have hlog_upper : Real.log (Nat.ceil (Real.exp y) + 1 : ℝ) ≤ y + Real.log 3 := by - calc - Real.log (Nat.ceil (Real.exp y) + 1 : ℝ) ≤ Real.log (3 * Real.exp y) := - Real.log_le_log (by positivity) (by - nlinarith [(Nat.ceil_lt_add_one (Real.exp_nonneg y)).le, - (show (1 : ℝ) ≤ Real.exp y by simpa [Real.one_le_exp_iff] using hy_nonneg)]) - _ = y + Real.log 3 := by - rw [Real.log_mul (by positivity : (3 : ℝ) ≠ 0) (Real.exp_pos y).ne', Real.log_exp] - ring - have hlower : - y + Real.log 3 < (((2 ^ n : ℕ) : ℝ)) * (f ρ σ.M).toReal := by - dsimp [y, δ] at hgap - nlinarith - linarith - -/-- The relative max-entropy is a lower bound on all relative entropies. -/ -theorem le_max (ρ σ : MState d) : f ρ σ.M ≤ max ρ σ.M := by - by_cases hx : ∃ x : ℝ, ρ.M ≤ Real.exp x • σ.M - · obtain ⟨x, hx⟩ := hx - let y : ℝ := Max.max x 0 - have hy0 : 0 ≤ y := by simp [y] - have hy : ρ.M ≤ Real.exp y • σ.M := by - exact hx.trans <| smul_le_smul_of_nonneg_right - (Real.exp_le_exp.mpr (show x ≤ y by dsimp [y]; exact le_max_left _ _)) σ.nonneg - have hfin : f ρ σ.M ≠ ∞ := - ne_top_of_le_ne_top ENNReal.ofReal_ne_top (le_of_le_exp (f := f) ρ σ hy0 hy) - exact (ENNReal.toReal_le_toReal hfin - (by simp [max, (show ∃ x : ℝ, ρ.M ≤ Real.exp x • σ.M from ⟨x, hx⟩)])).1 <| by - rw [RelEntropy.toReal_max (ρ := ρ) (σ := σ.M)] - let S : Set ℝ := ((↑) '' {x : ℝ≥0 | ρ.M ≤ Real.exp x • σ.M}) - refine le_csInf ⟨(⟨y, hy0⟩ : ℝ≥0), ⟨⟨y, hy0⟩, hy, rfl⟩⟩ ?_ - intro a ha - rcases ha with ⟨z, hz, rfl⟩ - simpa [ENNReal.toReal_ofReal z.2] using - (ENNReal.toReal_le_toReal hfin ENNReal.ofReal_ne_top).2 - (le_of_le_exp (f := f) ρ σ z.2 hz) - · simp [max, hx] - -end bounds - end RelEntropy /-- The axioms for a well-behaved quantum entropy: it vanishes on pure states and is additive under tensor products. Captures the common features of the von Neumann, min-, max-, and α-Renyi entropies. -/ class Entropy (f : ∀ {d : Type u} [Fintype d] [DecidableEq d], MState d → ℝ≥0) where - /-- The entropy of a pure state is zero -/ + /-- The entropy of a pure state is zero. -/ of_const {d : Type u} [Fintype d] [DecidableEq d] (ψ : Ket d) : f (.pure ψ) = 0 - /-- Entropy is additive under tensor products -/ + /-- Entropy is additive under tensor products. -/ of_kron {d₁ d₂ : Type u} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] : ∀ (ρ : MState d₁) (σ : MState d₂), f (ρ ⊗ᴹ σ) = f ρ + f σ -- /-- Entropy is convex. TODO def? Or do we even need this? -/ diff --git a/QuantumInfo/Finite/AxiomatizedEntropy/Faithful.lean b/QuantumInfo/Finite/AxiomatizedEntropy/Faithful.lean new file mode 100644 index 000000000..fc183a33f --- /dev/null +++ b/QuantumInfo/Finite/AxiomatizedEntropy/Faithful.lean @@ -0,0 +1,565 @@ +/- +Copyright (c) 2026 Dennj Osele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Dennj Osele +-/ +module + +import QuantumInfo.Finite.ProductPower +public import QuantumInfo.ClassicalInfo.Hellinger +public import QuantumInfo.Finite.AxiomatizedEntropy.Bounds +public import QuantumInfo.Finite.POVM + +@[expose] public section + +/-! # Faithfulness of nontrivial axiomatized relative entropies + +This file contains the Tomamichel-style proof that a nontrivial axiomatized relative entropy is +faithful, together with the binary-channel and finite classical testing lemmas used by the proof. +-/ + +noncomputable section +universe u + +open ComplexOrder +open scoped NNReal +open scoped ENNReal +open scoped Kronecker +open scoped HermitianMat +open ProbDistribution + +variable (f : ∀ {d : Type u} [Fintype d] [DecidableEq d], MState d → HermitianMat d ℂ → ℝ≥0∞) + +namespace RelEntropy + +variable {d : Type u} [Fintype d] [DecidableEq d] + +/-- The output of Tomamichel's preparation channel on the first binary point. -/ +private def binaryPrepOne (γ ω : MState d) (s t : ℝ) (hden : 0 < 1 - s - t) + (h : t • γ.M ≤ (1 - s) • ω.M) : MState d where + M := (1 - s - t)⁻¹ • ((1 - s) • ω.M - t • γ.M) + nonneg := smul_nonneg (inv_nonneg.mpr hden.le) (sub_nonneg.mpr h) + tr := by + simpa [HermitianMat.trace_smul, HermitianMat.trace_sub, γ.tr, ω.tr] using + inv_mul_cancel₀ hden.ne' + +/-- The output of Tomamichel's preparation channel on the second binary point. -/ +private def binaryPrepZero (γ ω : MState d) (s t : ℝ) (hden : 0 < 1 - s - t) + (h : s • ω.M ≤ (1 - t) • γ.M) : MState d where + M := (1 - s - t)⁻¹ • ((1 - t) • γ.M - s • ω.M) + nonneg := smul_nonneg (inv_nonneg.mpr hden.le) (sub_nonneg.mpr h) + tr := by + simp [HermitianMat.trace_smul, HermitianMat.trace_sub, γ.tr, ω.tr] + field_simp [hden.ne'] + ring_nf + +/-- A binary coin lifted to the working universe. -/ +private def uliftCoin (p : Prob) : ProbDistribution (ULift.{u} (Fin 2)) := + (ProbDistribution.congr Equiv.ulift.symm) (.coin p) + +private theorem cqPrepare_apply_uliftCoin (τ : ULift (Fin 2) → MState d) (p : Prob) : + (CPTPMap.cqPrepare (d := d) τ (MState.ofClassical (uliftCoin p))).m = + (p : ℝ) • (τ (ULift.up (0 : Fin 2))).m + + ((1 - p : Prob) : ℝ) • (τ (ULift.up (1 : Fin 2))).m := by + rw [CPTPMap.cqPrepare_apply_ofClassical (d := d) τ (uliftCoin p)] + ext i j + simp only [Matrix.sum_apply, Matrix.smul_apply, Complex.real_smul] + have hsum : + (∑ x : ULift (Fin 2), ↑↑((uliftCoin p) x) * (τ x).m i j) = + ∑ y : Fin 2, ↑↑((ProbDistribution.coin p) y) * (τ (ULift.up y)).m i j := by + simpa [uliftCoin, ProbDistribution.congr_apply] using + (Equiv.sum_comp (Equiv.ulift : ULift (Fin 2) ≃ Fin 2) + (fun y : Fin 2 => ↑↑((ProbDistribution.coin p) y) * (τ (ULift.up y)).m i j)) + rw [hsum] + simp [Fin.sum_univ_two] + +private def binaryClassicalPostprocess (a b : Prob) : + CPTPMap (ULift (Fin 2)) (ULift (Fin 2)) := + let τ : ULift (Fin 2) → MState (ULift (Fin 2)) := fun i => + if i = ULift.up (0 : Fin 2) then MState.ofClassical (uliftCoin a) + else MState.ofClassical (uliftCoin b) + CPTPMap.cqPrepare (d := ULift (Fin 2)) τ + +private theorem binaryClassicalPostprocess_apply (a b p : Prob) : + binaryClassicalPostprocess a b (MState.ofClassical (uliftCoin p)) = + MState.ofClassical (uliftCoin (Prob.mix p a b)) := by + apply MState.ext_m + change (CPTPMap.cqPrepare (d := ULift (Fin 2)) + (fun i : ULift (Fin 2) => + if i = ULift.up (0 : Fin 2) then MState.ofClassical (uliftCoin a) + else MState.ofClassical (uliftCoin b)) + (MState.ofClassical (uliftCoin p))).m = + (MState.ofClassical (uliftCoin (Prob.mix p a b))).m + rw [cqPrepare_apply_uliftCoin] + ext i j + rcases i with ⟨i⟩ + rcases j with ⟨j⟩ + fin_cases i <;> fin_cases j + all_goals + simp [MState.m, MState.ofClassical, Matrix.add_apply, Prob.coe_one_minus, uliftCoin, + ProbDistribution.congr_apply] + rw [← HermitianMat.mat_apply, HermitianMat.diagonal_mat] + simp [Matrix.diagonal, Prob.mix, Mixable.mix, Mixable.mix_ab, Prob.coe_one_minus] + all_goals ring_nf + +private theorem uliftCoin_support_top (p : Prob) (hp0 : 0 < (p : ℝ)) (hp1 : (p : ℝ) < 1) : + (MState.ofClassical (uliftCoin p)).M.support = ⊤ := by + rw [← HermitianMat.nonSingular_iff_support_top] + apply HermitianMat.nonSingular_of_posDef + rw [MState.coe_ofClassical] + apply Matrix.PosDef.diagonal + intro i + rcases i with ⟨i⟩ + fin_cases i + · simpa [Complex.real_lt_real, uliftCoin, ProbDistribution.congr_apply] using hp0 + · simp [uliftCoin, ProbDistribution.congr_apply, Prob.coe_one_minus] + exact_mod_cast hp1 + +private def classicalIndicatorEffect {κ : Type u} [DecidableEq κ] (A : Set κ) : + HermitianMat κ ℂ := by classical exact HermitianMat.diagonal ℂ fun x => if x ∈ A then 1 else 0 + +private theorem ofClassical_exp_val_indicator + {κ : Type u} [Fintype κ] [DecidableEq κ] (dist : ProbDistribution κ) (A : Set κ) + [DecidablePred (fun x => x ∈ A)] : + (MState.ofClassical dist).exp_val (classicalIndicatorEffect A) = + ∑ x, if x ∈ A then (dist x : ℝ) else 0 := by + rw [classicalIndicatorEffect, MState.exp_val, MState.coe_ofClassical, + HermitianMat.inner_eq_re_trace] + simp [Matrix.trace, HermitianMat.diagonal] + exact Finset.sum_congr rfl fun _ _ => by split_ifs <;> simp + +private theorem exists_effect_exp_val_ne_of_ne (ρ σ : MState d) (hne : ρ ≠ σ) : + ∃ T : HermitianMat d ℂ, (0 ≤ T ∧ T ≤ 1) ∧ ρ.exp_val T ≠ σ.exp_val T := by + let A : HermitianMat d ℂ := ρ.M - σ.M + have hA_not_nonneg : ¬ 0 ≤ A := by + intro hA_nonneg + exact hne (MState.ext (eq_of_sub_eq_zero (HermitianMat.ext <| + (Matrix.PosSemidef.trace_eq_zero_iff (HermitianMat.zero_le_iff.mp hA_nonneg)).1 <| + (HermitianMat.trace_eq_zero_iff (A := A)).1 + (by simp [A, HermitianMat.trace_sub, ρ.tr, σ.tr])))) + let B : HermitianMat d ℂ := A⁻ + have hB_nonneg : 0 ≤ B := by + simpa [B] using HermitianMat.negPart_nonneg A + have hinner_neg : inner ℝ A B < 0 := by + simpa [B] using (HermitianMat.inner_negPart_neg_iff (A := A)).2 hA_not_nonneg + have hB_trace_pos : 0 < B.trace := by + refine lt_of_le_of_ne (HermitianMat.trace_nonneg hB_nonneg) ?_ + intro htrace + have hB_zero : B = 0 := HermitianMat.ext <| + (Matrix.PosSemidef.trace_eq_zero_iff (HermitianMat.zero_le_iff.mp hB_nonneg)).1 <| + (HermitianMat.trace_eq_zero_iff (A := B)).1 htrace.symm + rw [hB_zero] at hinner_neg + simp at hinner_neg + let T : HermitianMat d ℂ := B.trace⁻¹ • B + have hT_nonneg : 0 ≤ T := by + simpa [T] using smul_nonneg (inv_nonneg.mpr hB_trace_pos.le) hB_nonneg + have hT_le_one : T ≤ 1 := by + dsimp [T] + simpa [smul_smul, inv_mul_cancel₀ hB_trace_pos.ne'] using + smul_le_smul_of_nonneg_left (HermitianMat.le_trace_smul_one hB_nonneg) + (inv_nonneg.mpr hB_trace_pos.le) + refine ⟨T, ⟨hT_nonneg, hT_le_one⟩, fun hsame => ?_⟩ + have hzero : inner ℝ A T = 0 := by + simpa [A, MState.exp_val, inner_sub_left] using sub_eq_zero.mpr hsame + have hneg : inner ℝ A T < 0 := by + simpa [T, inner_smul_right] using + mul_neg_of_pos_of_neg (inv_pos.mpr hB_trace_pos) hinner_neg + linarith + +private theorem hellingerOverlap_uliftCoin (p q : Prob) : + hellingerOverlap (uliftCoin p) (uliftCoin q) = + Real.sqrt ((p : ℝ) * (q : ℝ)) + + Real.sqrt ((1 - (p : ℝ)) * (1 - (q : ℝ))) := by + change (∑ x : ULift (Fin 2), + Real.sqrt (((ProbDistribution.coin p) x.down : ℝ) * + ((ProbDistribution.coin q) x.down : ℝ))) = _ + simpa [Fin.sum_univ_two] using + (Equiv.sum_comp (Equiv.ulift : ULift (Fin 2) ≃ Fin 2) + fun y : Fin 2 => Real.sqrt (((ProbDistribution.coin p) y : ℝ) * + ((ProbDistribution.coin q) y : ℝ))) + +private theorem exists_likelihood_indicator_effect + {κ : Type u} [Fintype κ] [DecidableEq κ] (P Q : ProbDistribution κ) (s r : Prob) + (hoverlap_s : hellingerOverlap P Q ≤ (s : ℝ)) + (hoverlap_r : hellingerOverlap P Q ≤ 1 - (r : ℝ)) : + ∃ T : HermitianMat κ ℂ, (0 ≤ T ∧ T ≤ 1) ∧ + ∃ α β : Prob, + (MState.ofClassical P).exp_val T = α ∧ + (MState.ofClassical Q).exp_val T = β ∧ + (α : ℝ) ≤ s ∧ (r : ℝ) ≤ β := by + classical + let A : Set κ := {x | (P x : ℝ) ≤ Q x} + let T : HermitianMat κ ℂ := classicalIndicatorEffect A + have hT : 0 ≤ T ∧ T ≤ 1 := by + refine ⟨?_, ?_⟩ + · rw [HermitianMat.zero_le_iff] + simp [T, classicalIndicatorEffect, HermitianMat.diagonal_mat, Matrix.posSemidef_diagonal_iff] + exact fun i => by by_cases hi : i ∈ A <;> simp [hi] + · rw [← sub_nonneg] + rw [show T = HermitianMat.diagonal ℂ fun x => if x ∈ A then (1 : ℝ) else 0 from rfl, + ← HermitianMat.diagonal_one (𝕜 := ℂ), + ← HermitianMat.diagonal_sub, HermitianMat.zero_le_iff, HermitianMat.diagonal_mat, + Matrix.posSemidef_diagonal_iff] + exact fun i => by by_cases hi : i ∈ A <;> simp [hi] + refine ⟨T, hT, + ⟨(MState.ofClassical P).exp_val T, (MState.ofClassical P).exp_val_prob hT⟩, + ⟨(MState.ofClassical Q).exp_val T, (MState.ofClassical Q).exp_val_prob hT⟩, + rfl, rfl, ?_, ?_⟩ + · change (MState.ofClassical P).exp_val T ≤ (s : ℝ) + rw [ofClassical_exp_val_indicator] + exact (show ∑ x, (if (P x : ℝ) ≤ Q x then (P x : ℝ) else 0) ≤ + hellingerOverlap P Q by + rw [hellingerOverlap] + refine Finset.sum_le_sum ?_ + intro x _ + by_cases hx : (P x : ℝ) ≤ Q x + · simpa [hx] using Real.le_sqrt (P x).2.1 (mul_nonneg (P x).2.1 (Q x).2.1) |>.2 + (by simpa [pow_two] using mul_le_mul_of_nonneg_left hx (P x).2.1) + · simpa [hx] using Real.sqrt_nonneg ((P x : ℝ) * (Q x : ℝ))).trans hoverlap_s + · change (r : ℝ) ≤ (MState.ofClassical Q).exp_val T + rw [ofClassical_exp_val_indicator] + change (r : ℝ) ≤ ∑ x, (if (P x : ℝ) ≤ Q x then (Q x : ℝ) else 0) + have hcompl : ∑ x, (if (P x : ℝ) ≤ Q x then 0 else (Q x : ℝ)) ≤ + hellingerOverlap P Q := by + rw [hellingerOverlap] + refine Finset.sum_le_sum ?_ + intro x _ + by_cases hx : (P x : ℝ) ≤ Q x + · simpa [hx] using Real.sqrt_nonneg ((P x : ℝ) * (Q x : ℝ)) + · rw [mul_comm] + simpa [hx] using Real.le_sqrt (Q x).2.1 (mul_nonneg (Q x).2.1 (P x).2.1) |>.2 + (by simpa [pow_two] using + mul_le_mul_of_nonneg_left (le_of_not_ge hx) (Q x).2.1) + have htotal' : + (∑ x, (if (P x : ℝ) ≤ Q x then 0 else (Q x : ℝ))) + + (∑ x, (if (P x : ℝ) ≤ Q x then (Q x : ℝ) else 0)) = + 1 := by + rw [← Finset.sum_add_distrib] + convert Q.normalized using 1 + exact Finset.sum_congr rfl fun x _ => by by_cases hx : (P x : ℝ) ≤ Q x <;> simp [hx] + linarith + +private theorem exists_npow_binary_effect_le_ge + (p q s r : Prob) (hpq : (p : ℝ) < q) + (hs_pos : 0 < (s : ℝ)) (hr_lt_one : (r : ℝ) < 1) : + ∃ (n : ℕ) (T : HermitianMat (Fin n → ULift.{u} (Fin 2)) ℂ), + (0 ≤ T ∧ T ≤ 1) ∧ ∃ α β : Prob, + (MState.npow (MState.ofClassical (uliftCoin p)) n).exp_val T = α ∧ + (MState.npow (MState.ofClassical (uliftCoin q)) n).exp_val T = β ∧ + (α : ℝ) ≤ s ∧ (r : ℝ) ≤ β := by + let ε : ℝ := (s : ℝ) ⊓ (1 - (r : ℝ)) + have ha1 : hellingerOverlap (uliftCoin p) (uliftCoin q) < 1 := by + rw [hellingerOverlap_uliftCoin] + simpa [hellingerOverlap_coin] using hellingerOverlap_coin_lt_one p q hpq + obtain ⟨n, hn'⟩ := exists_pow_lt_of_lt_one + (show 0 < ε by simpa [ε] using lt_inf_iff.mpr ⟨hs_pos, sub_pos.mpr hr_lt_one⟩) ha1 + have hoverlap_lt : + hellingerOverlap (ProbDistribution.npow (uliftCoin p) n) + (ProbDistribution.npow (uliftCoin q) n) < ε := by + rwa [ProbDistribution.hellingerOverlap_npow] + obtain ⟨T, hT, α, β, hpT, hqT, hαs, hrβ⟩ := + exists_likelihood_indicator_effect + (ProbDistribution.npow (uliftCoin p) n) (ProbDistribution.npow (uliftCoin q) n) s r + (hoverlap_lt.le.trans inf_le_left) (hoverlap_lt.le.trans inf_le_right) + exact ⟨n, T, hT, α, β, by simpa [MState.ofClassical_npow] using hpT, + by simpa [MState.ofClassical_npow] using hqT, hαs, hrβ⟩ + +/-- Universe-lifted two-outcome POVM associated to an effect `0 ≤ T ≤ 1`. -/ +private def binaryPOVMOfEffectULift (T : HermitianMat d ℂ) (hT : 0 ≤ T ∧ T ≤ 1) : + POVM (ULift (Fin 2)) d where + mats i := if i = ULift.up (0 : Fin 2) then T else 1 - T + nonneg i := by + split + · exact hT.1 + · exact HermitianMat.zero_le_iff.mpr hT.2 + normalized := by + have hsum : + (∑ i : ULift (Fin 2), if i = ULift.up (0 : Fin 2) then T else 1 - T) = + ∑ i : Fin 2, if ULift.up i = ULift.up (0 : Fin 2) then T else 1 - T := by + refine Fintype.sum_equiv Equiv.ulift + (fun i : ULift (Fin 2) => if i = ULift.up (0 : Fin 2) then T else 1 - T) + (fun i : Fin 2 => if ULift.up i = ULift.up (0 : Fin 2) then T else 1 - T) ?_ + rintro ⟨x⟩ + rfl + rw [hsum] + simp [Fin.sum_univ_two] + +/-- Measuring a lifted binary effect and discarding the post-measurement state gives a lifted coin. -/ +private theorem binaryPOVMOfEffectULift_measureDiscard_apply + (T : HermitianMat d ℂ) (hT : 0 ≤ T ∧ T ≤ 1) (ρ : MState d) : + (binaryPOVMOfEffectULift T hT).measureDiscard ρ = + MState.ofClassical (uliftCoin ⟨ρ.exp_val T, ρ.exp_val_prob hT⟩) := by + rw [POVM.measureDiscard_apply] + congr 1 + let p : Prob := ⟨ρ.exp_val T, ρ.exp_val_prob hT⟩ + ext i + rcases i with ⟨i⟩ + fin_cases i + · let z : ULift.{u} (Fin 2) := ULift.up (0 : Fin 2) + change inner ℝ T ρ.M = ((uliftCoin p) z : ℝ) + simp [z, p, uliftCoin, ProbDistribution.congr_apply, MState.exp_val, HermitianMat.inner_comm] + · let o : ULift.{u} (Fin 2) := ULift.up (1 : Fin 2) + change inner ℝ (1 - T) ρ.M = ((uliftCoin p) o : ℝ) + simp [o, p, uliftCoin, ProbDistribution.congr_apply, Prob.coe_one_minus, + MState.exp_val, HermitianMat.inner_comm, inner_sub_right, HermitianMat.inner_one, ρ.tr] + +private theorem exists_binary_measurement_of_ne (ρ σ : MState d) (hne : ρ ≠ σ) : + ∃ p q : Prob, (p : ℝ) < (q : ℝ) ∧ + ∃ Λ : CPTPMap d (ULift.{u} (Fin 2)), + Λ ρ = MState.ofClassical (uliftCoin p) ∧ + Λ σ = MState.ofClassical (uliftCoin q) := by + obtain ⟨T, hT, hT_ne⟩ := exists_effect_exp_val_ne_of_ne ρ σ hne + let p : Prob := ⟨ρ.exp_val T, ρ.exp_val_prob hT⟩ + let q : Prob := ⟨σ.exp_val T, σ.exp_val_prob hT⟩ + by_cases hpq : (p : ℝ) < q + · exact ⟨p, q, hpq, (binaryPOVMOfEffectULift T hT).measureDiscard, + by rw [binaryPOVMOfEffectULift_measureDiscard_apply], + by rw [binaryPOVMOfEffectULift_measureDiscard_apply]⟩ + · let T' : HermitianMat d ℂ := 1 - T + have hT' : 0 ≤ T' ∧ T' ≤ 1 := by + refine ⟨by dsimp [T']; exact HermitianMat.zero_le_iff.mpr hT.2, ?_⟩ + dsimp [T'] + rw [sub_le_iff_le_add] + simpa using hT.1 + have hpq' : ((1 - p : Prob) : ℝ) < (1 - q : Prob) := by + rw [Prob.coe_one_minus, Prob.coe_one_minus] + linarith [lt_of_le_of_ne (le_of_not_gt hpq) (fun heq => hT_ne heq.symm)] + refine ⟨1 - p, 1 - q, hpq', (binaryPOVMOfEffectULift T' hT').measureDiscard, ?_, ?_⟩ <;> + rw [binaryPOVMOfEffectULift_measureDiscard_apply] <;> + congr 2 <;> + apply Subtype.ext <;> + simp [T', p, q, MState.exp_val_sub, MState.exp_val_one, Prob.coe_one_minus] + +private theorem exists_binary_postprocess {α β s r : Prob} + (hαs : (α : ℝ) ≤ s) (hsr : (s : ℝ) < r) (hrβ : (r : ℝ) ≤ β) : + ∃ a b : Prob, Prob.mix α a b = s ∧ Prob.mix β a b = r := by + let A : ℝ := α + let B : ℝ := β + let S : ℝ := s + let R : ℝ := r + have hAB : A < B := by dsimp [A, B, S, R] at *; linarith + let k : ℝ := (R - S) / (B - A) + have hk_nonneg : 0 ≤ k := by + dsimp [k] + exact div_nonneg (sub_nonneg.mpr (by dsimp [S, R]; exact hsr.le)) + (sub_nonneg.mpr hAB.le) + have hk_le_one : k ≤ 1 := by + dsimp [k] + rw [div_le_one (sub_pos.mpr hAB)] + dsimp [A, B, S, R] at * + linarith + let bR : ℝ := S - A * k + let aR : ℝ := bR + k + have hbR_nonneg : 0 ≤ bR := by + dsimp [bR, A, S] at * + linarith [mul_le_mul_of_nonneg_left hk_le_one α.2.1] + have hbR_le_one : bR ≤ 1 := by + dsimp [bR, S] + nlinarith [s.2.2, α.2.1, hk_nonneg] + have haR_nonneg : 0 ≤ aR := by dsimp [aR]; positivity + have haR_le_one : aR ≤ 1 := by + have hden_pos : 0 < B - A := sub_pos.mpr hAB + have hmain : + S * (B - A) + (1 - A) * (R - S) ≤ 1 * (B - A) := by + nlinarith [ + mul_le_mul_of_nonneg_right (show R ≤ B by dsimp [R, B] at hrβ ⊢; exact hrβ) + (show 0 ≤ 1 - A by dsimp [A]; linarith [α.2.2]), + mul_le_mul_of_nonpos_right (show A ≤ S by dsimp [A, S] at hαs ⊢; exact hαs) + (show B - 1 ≤ 0 by dsimp [B]; linarith [β.2.2])] + rw [show aR = (S * (B - A) + (1 - A) * (R - S)) / (B - A) by + dsimp [aR, bR, k] + field_simp [hden_pos.ne'] + ring, div_le_one hden_pos] + simpa using hmain + let a : Prob := ⟨aR, haR_nonneg, haR_le_one⟩ + let b : Prob := ⟨bR, hbR_nonneg, hbR_le_one⟩ + refine ⟨a, b, ?_, ?_⟩ + all_goals + ext + simp [Prob.mix, Mixable.mix, Mixable.mix_ab, Prob.coe_one_minus, a, b, aR, bR, k, A, B, S, R] + · + ring + · + field_simp [show (↑β : ℝ) - ↑α ≠ 0 by dsimp [A, B] at hAB; linarith] + ring + +/-- A full-support state dominates every other state up to an integer scalar. -/ +private theorem exists_le_nat_smul_of_fullSupport (ρ σ : MState d) + (hσ : σ.M.support = ⊤) : + ∃ N : ℕ, 0 < N ∧ ρ.M ≤ ((N + 1 : ℝ) • σ.M) := by + letI : σ.M.NonSingular := HermitianMat.nonSingular_iff_support_top.mpr hσ + have hexp : ∃ x : ℝ, ρ.M ≤ Real.exp x • σ.M := by + by_contra h + exact (RelEntropy.max_not_top ρ σ.M σ.nonneg).mpr + (by simp [HermitianMat.nonSingular_ker_bot]) (by simp [max, h]) + obtain ⟨x, hx⟩ := hexp + refine ⟨Nat.ceil (Real.exp x), Nat.ceil_pos.mpr (Real.exp_pos x), ?_⟩ + exact hx.trans <| smul_le_smul_of_nonneg_right ((Nat.le_ceil _).trans (by norm_num)) σ.nonneg + +section nontrivial +variable [RelEntropy f] [RelEntropy.Nontrivial f] + +/-- From Tomamichel nontriviality, extract a strictly positive binary classical pair with +full-support states. This is the finite binary witness used in the proof of `faithful`. -/ +private theorem exists_positive_binary_pair : + ∃ p q : Prob, 0 < (p : ℝ) ∧ (p : ℝ) < q ∧ (q : ℝ) < 1 ∧ + (MState.ofClassical (uliftCoin.{u} p)).M.support = ⊤ ∧ + (MState.ofClassical (uliftCoin.{u} q)).M.support = ⊤ ∧ + 0 < f (MState.ofClassical (uliftCoin.{u} p)) + (MState.ofClassical (uliftCoin.{u} q)).M := by + obtain ⟨s, t, hs0, -, ht0, -, hs_order, hsSupport, htSupport, hpos⟩ : + ∃ s t : Prob, + 0 < (s : ℝ) ∧ (s : ℝ) < 1 / 2 ∧ + 0 < (t : ℝ) ∧ (t : ℝ) < 1 / 2 ∧ + (s : ℝ) < ((1 - t : Prob) : ℝ) ∧ + (MState.ofClassical (uliftCoin s)).M.support = ⊤ ∧ + (MState.ofClassical (uliftCoin (1 - t))).M.support = ⊤ ∧ + 0 < f (MState.ofClassical (uliftCoin s)) + (MState.ofClassical (uliftCoin (1 - t))).M := by + obtain ⟨γ, ω, hγ, hω, hpos⟩ := + RelEntropy.Nontrivial.nontrivial (f := f) (ULift.{u} (Fin 2)) + obtain ⟨s, t, hs0, hslt, ht0, htlt, hleft, hright⟩ : + ∃ s t : Prob, 0 < (s : ℝ) ∧ (s : ℝ) < 1 / 2 ∧ + 0 < (t : ℝ) ∧ (t : ℝ) < 1 / 2 ∧ + (t : ℝ) • γ.M ≤ (1 - (s : ℝ)) • ω.M ∧ + (s : ℝ) • ω.M ≤ (1 - (t : ℝ)) • γ.M := by + obtain ⟨Nγω, hNγω_pos, hγω⟩ := exists_le_nat_smul_of_fullSupport γ ω hω + obtain ⟨Nωγ, _, hωγ⟩ := exists_le_nat_smul_of_fullSupport ω γ hγ + let K : ℕ := Nat.max Nγω Nωγ + let a : ℝ := 1 / (K + 2 : ℝ) + have hden_pos : (0 : ℝ) < K + 2 := by positivity + have ha_pos : 0 < a := by dsimp [a]; positivity + have ha_lt_half : a < 1 / 2 := by + dsimp [a] + rw [div_lt_iff₀ hden_pos] + nlinarith [show (1 : ℝ) ≤ K by + exact_mod_cast le_trans hNγω_pos (le_max_left Nγω Nωγ)] + have hscale {N : ℕ} (hNK : N ≤ K) : a * (N + 1 : ℝ) ≤ 1 - a := by + dsimp [a] + rw [div_mul_eq_mul_div, one_sub_div hden_pos.ne', + div_le_div_iff_of_pos_right hden_pos] + nlinarith [show (N + 1 : ℝ) ≤ K + 1 by exact_mod_cast Nat.succ_le_succ hNK] + let p : Prob := ⟨a, ha_pos.le, by linarith [ha_lt_half]⟩ + refine ⟨p, p, by simpa [p] using ha_pos, by simpa [p] using ha_lt_half, + by simpa [p] using ha_pos, by simpa [p] using ha_lt_half, ?_, ?_⟩ + · simpa [p] using calc + a • γ.M ≤ a • ((Nγω + 1 : ℝ) • ω.M) := + smul_le_smul_of_nonneg_left hγω ha_pos.le + _ = (a * (Nγω + 1 : ℝ)) • ω.M := by rw [smul_smul] + _ ≤ (1 - a) • ω.M := smul_le_smul_of_nonneg_right + (hscale (le_max_left Nγω Nωγ)) ω.nonneg + · simpa [p] using calc + a • ω.M ≤ a • ((Nωγ + 1 : ℝ) • γ.M) := + smul_le_smul_of_nonneg_left hωγ ha_pos.le + _ = (a * (Nωγ + 1 : ℝ)) • γ.M := by rw [smul_smul] + _ ≤ (1 - a) • γ.M := smul_le_smul_of_nonneg_right + (hscale (le_max_right Nγω Nωγ)) γ.nonneg + have hden : 0 < 1 - (s : ℝ) - (t : ℝ) := by linarith + let τ := fun i => + if i = ULift.up (0 : Fin 2) then + binaryPrepOne γ ω (s : ℝ) (t : ℝ) hden hleft + else + binaryPrepZero γ ω (s : ℝ) (t : ℝ) hden hright + let Λ := CPTPMap.cqPrepare τ + have hdenC : (1 - ((s : ℝ) : ℂ) - ((t : ℝ) : ℂ)) ≠ 0 := by exact_mod_cast hden.ne' + have hγprep : Λ (MState.ofClassical (uliftCoin s)) = γ := by + apply MState.ext_m + change (CPTPMap.cqPrepare τ (MState.ofClassical (uliftCoin s))).m = γ.m + rw [cqPrepare_apply_uliftCoin, Prob.coe_one_minus] + ext i j + simp [τ, binaryPrepOne, binaryPrepZero, MState.m, Matrix.add_apply, Matrix.sub_apply, + Matrix.smul_apply, -MState.mat_M] + field_simp [hdenC] + ring + have hωprep : Λ (MState.ofClassical (uliftCoin (1 - t))) = ω := by + apply MState.ext_m + change (CPTPMap.cqPrepare τ (MState.ofClassical (uliftCoin (1 - t)))).m = ω.m + rw [cqPrepare_apply_uliftCoin, Prob.coe_one_minus, Prob.coe_one_minus] + ext i j + simp [τ, binaryPrepOne, binaryPrepZero, MState.m, Matrix.add_apply, Matrix.sub_apply, + Matrix.smul_apply, -MState.mat_M] + field_simp [hdenC] + ring + refine ⟨s, t, hs0, hslt, ht0, htlt, by rw [Prob.coe_one_minus]; linarith, + uliftCoin_support_top s hs0 (by linarith), + uliftCoin_support_top (1 - t) (by rw [Prob.coe_one_minus]; linarith) + (by rw [Prob.coe_one_minus]; linarith), ?_⟩ + exact lt_of_lt_of_le hpos <| by + simpa [hγprep, hωprep] using DPI (f := f) (MState.ofClassical (uliftCoin s)) + (MState.ofClassical (uliftCoin (1 - t))) Λ + exact ⟨s, 1 - t, hs0, hs_order, by rw [Prob.coe_one_minus]; linarith, + hsSupport, htSupport, hpos⟩ + +/-- A nontrivial relative entropy is **faithful**: it can distinguish when two states are equal. + +The proof (Tomamichel §5) goes by building a binary measurement that separates `ρ` from `σ`, +using DPI to reduce to a classical `Fin 2` distribution, then amplifying with `of_kron` until the +`Nontrivial` axiom forces a strictly positive value. The tensor-power separation step is formalized +via the finite classical likelihood test in `exists_npow_binary_effect_le_ge`. -/ +theorem faithful (ρ σ : MState d) : f ρ σ = 0 ↔ ρ = σ := by + constructor + · intro hzero + by_contra hne + obtain ⟨p, q, hpq, Λ, hρ, hσ⟩ := exists_binary_measurement_of_ne ρ σ hne + let ρp := MState.ofClassical (uliftCoin p) + let σq := MState.ofClassical (uliftCoin q) + have hzero_one : f ρp σq.M = 0 := + le_antisymm (by simpa [ρp, σq, hρ, hσ, hzero] using DPI (f := f) ρ σ Λ) bot_le + obtain ⟨s, r, hs_pos, hsr, hr_lt_one, _, _, hpos⟩ := + exists_positive_binary_pair (f := f) + obtain ⟨n, T, hT, α, β, hpT, hqT, hαs, hrβ⟩ := + exists_npow_binary_effect_le_ge p q s r hpq hs_pos hr_lt_one + suffices 0 < f (MState.npow ρp n) (MState.npow σq n).M by + rw [RelEntropy.of_npow (f := f), hzero_one, mul_zero] at this + simp at this + obtain ⟨a, b, hsmix, hrmix⟩ := exists_binary_postprocess hαs hsr hrβ + let Μ := (binaryPOVMOfEffectULift T hT).measureDiscard + let Λ' := (binaryClassicalPostprocess a b) ∘ₘ Μ + have hOut (x z y : Prob) + (hz : (MState.npow (MState.ofClassical (uliftCoin x)) n).exp_val T = z) + (hy : Prob.mix z a b = y) : + Λ' (MState.npow (MState.ofClassical (uliftCoin x)) n) = + MState.ofClassical (uliftCoin y) := by + simpa [Λ', Μ, CPTPMap.compose_eq, binaryPOVMOfEffectULift_measureDiscard_apply, + binaryClassicalPostprocess_apply] using + (congrArg (fun z => MState.ofClassical (uliftCoin (Prob.mix z a b))) + (Subtype.ext hz)).trans (congrArg (fun x => MState.ofClassical (uliftCoin x)) hy) + exact lt_of_lt_of_le hpos <| by + simpa [ρp, σq, hOut p α s hpT hsmix, hOut q β r hqT hrmix] using + DPI (f := f) (MState.npow ρp n) (MState.npow σq n) Λ' + · rintro rfl + simp + +/-- In every system with at least two classical points, a nontrivial relative entropy has a +strictly positive value on some pair of full-support states. -/ +theorem exists_fullSupport_positive_of_two_le_card + (d : Type u) [Fintype d] [DecidableEq d] (hd : 2 ≤ Fintype.card d) : + ∃ (ρ σ : MState d), ρ.M.support = ⊤ ∧ σ.M.support = ⊤ ∧ 0 < f ρ σ := by + haveI : Nonempty d := Fintype.card_pos_iff.mp (lt_of_lt_of_le (by norm_num) hd) + let i : d := Classical.arbitrary d + let p : Prob := ⟨1 / 2, by norm_num⟩ + let ρ : MState d := p [MState.ofClassical (.constant i) ↔ MState.uniform] + refine ⟨ρ, MState.uniform, ?_, ?_, ?_⟩ + · haveI : ρ.M.NonSingular := HermitianMat.nonSingular_of_posDef <| by + dsimp [ρ] + exact MState.PosDef_mix_of_ne_one (hσ₂ := MState.uniform_posDef) p + (by dsimp [p]; norm_num [Prob.ext_iff]) + exact HermitianMat.nonSingular_support_top + · haveI : (MState.uniform : MState d).M.NonSingular := + HermitianMat.nonSingular_of_posDef MState.uniform_posDef + exact HermitianMat.nonSingular_support_top + · refine bot_lt_iff_ne_bot.mpr ((faithful (f := f) ρ MState.uniform).not.mpr ?_) + intro hρσ + have hmat := congrArg (fun τ : MState d => τ.M.mat) hρσ + simp [ρ, p, Mixable.mix, Mixable.mix_ab, MState.instMixable, + MState.uniform, MState.ofClassical, ProbDistribution.constant_eq, + ProbDistribution.uniform_def, HermitianMat.diagonal, Mixable.to_U] at hmat + have hdiag_re := congrArg Complex.re (congrFun (congrFun hmat i) i) + simp [Matrix.add_apply] at hdiag_re + norm_num at hdiag_re + nlinarith [inv_lt_one_of_one_lt₀ + (by exact_mod_cast (lt_of_lt_of_le one_lt_two hd) : (1 : ℝ) < Fintype.card d)] + +end nontrivial + +end RelEntropy diff --git a/QuantumInfo/Finite/AxiomatizedEntropy/Renyi.lean b/QuantumInfo/Finite/AxiomatizedEntropy/Renyi.lean index a421060e1..df57a3019 100644 --- a/QuantumInfo/Finite/AxiomatizedEntropy/Renyi.lean +++ b/QuantumInfo/Finite/AxiomatizedEntropy/Renyi.lean @@ -23,7 +23,7 @@ namespace AxiomatizedEntropy /-- A conservative wrapper around the actual quantum relative entropy. On normalized PSD inputs it agrees with `_root_.qRelativeEnt`; away from the state space we leave the value at `0`. -/ @[irreducible] -noncomputable def qRelativeEnt (ρ : MState d) (σ : HermitianMat d ℂ) : ENNReal := +noncomputable def qRelativeEntExtension (ρ : MState d) (σ : HermitianMat d ℂ) : ENNReal := open Classical in if hσ : σ.trace = 1 ∧ 0 ≤ σ then let σ' : MState d := { M := σ, nonneg := hσ.2, tr := hσ.1 } @@ -32,9 +32,9 @@ noncomputable def qRelativeEnt (ρ : MState d) (σ : HermitianMat d ℂ) : ENNRe 0 @[simp] -theorem qRelativeEnt_state (ρ σ : MState d) : - qRelativeEnt ρ (σ : HermitianMat d ℂ) = _root_.qRelativeEnt ρ σ := by - rw [qRelativeEnt, dif_pos ⟨σ.tr, σ.nonneg⟩] +theorem qRelativeEntExtension_state (ρ σ : MState d) : + qRelativeEntExtension ρ (σ : HermitianMat d ℂ) = _root_.qRelativeEnt ρ σ := by + rw [qRelativeEntExtension, dif_pos ⟨σ.tr, σ.nonneg⟩] private lemma uniform_log [Nonempty d] : (MState.uniform : MState d).M.log = @@ -44,15 +44,15 @@ private lemma uniform_log [Nonempty d] : funext _ simp [ProbDistribution.uniform_def, Real.log_inv] -instance : RelEntropy qRelativeEnt where +instance : RelEntropy qRelativeEntExtension where DPI := by intro d₁ d₂ _ _ _ _ ρ σ Λ - simpa [qRelativeEnt_state] using + simpa [qRelativeEntExtension_state] using (sandwichedRenyiEntropy_DPI (d₁ := d₁) (d₂ := d₂) (α := 1) (hα := le_rfl) (ρ := ρ) (σ := σ) (Φ := Λ)) of_kron := by intro d₁ d₂ _ _ _ _ ρ₁ σ₁ ρ₂ σ₂ - rw [qRelativeEnt_state, qRelativeEnt_state, qRelativeEnt_state] + rw [qRelativeEntExtension_state, qRelativeEntExtension_state, qRelativeEntExtension_state] exact _root_.qRelativeEnt_additive ρ₁ σ₁ ρ₂ σ₂ normalized := by intro d _ _ _ i @@ -76,11 +76,11 @@ instance : RelEntropy qRelativeEnt where have hq := _root_.qRelativeEnt_eq_neg_Sᵥₙ_add (ρ := MState.ofClassical (.constant i)) (σ := MState.uniform) rw [if_pos hker, Sᵥₙ_ofClassical, Hₛ_constant_eq_zero, hicul] at hq - simp [qRelativeEnt_state, hq, EReal.coe_nnreal_eq_coe_real] + simp [qRelativeEntExtension_state, hq, EReal.coe_nnreal_eq_coe_real] /-- Quantum relative entropy as `Tr[ρ (log ρ - log σ)]` when supports are correct. -/ -theorem qRelativeEnt_ker {ρ σ : MState d} (h : σ.M.ker ≤ ρ.M.ker) : - (qRelativeEnt ρ σ : EReal) = ⟪ρ.M, ρ.M.log - σ.M.log⟫ := by - simpa [qRelativeEnt_state] using (_root_.qRelativeEnt_ker (ρ := ρ) (σ := σ) h) +theorem qRelativeEntExtension_ker {ρ σ : MState d} (h : σ.M.ker ≤ ρ.M.ker) : + (qRelativeEntExtension ρ σ : EReal) = ⟪ρ.M, ρ.M.log - σ.M.log⟫ := by + simpa [qRelativeEntExtension_state] using (_root_.qRelativeEnt_ker (ρ := ρ) (σ := σ) h) end AxiomatizedEntropy diff --git a/QuantumInfo/Finite/CPTPMap.lean b/QuantumInfo/Finite/CPTPMap.lean index 6b169572a..b8048c258 100644 --- a/QuantumInfo/Finite/CPTPMap.lean +++ b/QuantumInfo/Finite/CPTPMap.lean @@ -7,6 +7,7 @@ module public import QuantumInfo.Finite.CPTPMap.Bundled public import QuantumInfo.Finite.CPTPMap.CPTP +public import QuantumInfo.Finite.CPTPMap.CQPrepare public import QuantumInfo.Finite.CPTPMap.Dual public import QuantumInfo.Finite.CPTPMap.MatrixMap public import QuantumInfo.Finite.CPTPMap.Unbundled diff --git a/QuantumInfo/Finite/CPTPMap/CQPrepare.lean b/QuantumInfo/Finite/CPTPMap/CQPrepare.lean new file mode 100644 index 000000000..53edcfcde --- /dev/null +++ b/QuantumInfo/Finite/CPTPMap/CQPrepare.lean @@ -0,0 +1,104 @@ +/- +Copyright (c) 2026 Dennj Osele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Dennj Osele +-/ +module + +public import QuantumInfo.Finite.CPTPMap.CPTP + +@[expose] public section + +/-! # Classical-to-quantum preparation channels + +This file defines the CPTP map that prepares a quantum state depending on a classical input. +-/ + +noncomputable section +universe u + +open ComplexOrder + +namespace CPTPMap + +variable {d : Type u} [Fintype d] [DecidableEq d] + +/-- The classical-to-quantum preparation channel associated to a family of output states. -/ +def cqPrepare {κ : Type u} [Fintype κ] [DecidableEq κ] (τ : κ → MState d) : + CPTPMap κ d := + let M : Matrix (d × κ) (d × κ) ℂ := + (∑ i, HermitianMat.kronecker (τ i).M (MState.ofClassical (.constant i)).M).mat + CPTP_of_choi_PSD_Tr + (M := M) + (by + change ((∑ i, + HermitianMat.kronecker (τ i).M (MState.ofClassical (.constant i)).M).mat).PosSemidef + have hnonneg : 0 ≤ + ∑ i, HermitianMat.kronecker (τ i).M (MState.ofClassical (.constant i)).M := + Finset.sum_nonneg fun i _ => + HermitianMat.kronecker_nonneg (τ i).nonneg (MState.ofClassical (.constant i)).nonneg + exact HermitianMat.zero_le_iff.mp hnonneg) + (by + let prepMap : MatrixMap κ d ℂ := { + toFun X := fun b₁ b₂ => ∑ i, X i i * (τ i).m b₁ b₂ + map_add' X Y := by + ext b₁ b₂ + simp [Matrix.add_apply, Finset.sum_add_distrib, add_mul] + map_smul' c X := by + ext b₁ b₂ + simp [Matrix.smul_apply, Finset.mul_sum, mul_assoc] } + have hchoi : prepMap.choi_matrix = M := by + ext ⟨b₁, a₁⟩ ⟨b₂, a₂⟩ + simp only [MatrixMap.choi_matrix, prepMap, Matrix.single, M, + HermitianMat.mat_finset_sum, Matrix.sum_apply] + refine Finset.sum_congr rfl fun x _ => ?_ + show (if a₁ = x ∧ a₂ = x then 1 else 0) * (τ x).m b₁ b₂ = + (τ x).m b₁ b₂ * + (HermitianMat.diagonal ℂ + (fun x₁ => ((ProbDistribution.constant x) x₁ : ℝ))).mat a₁ a₂ + rw [HermitianMat.diagonal_mat] + aesop (add simp [Matrix.diagonal, ProbDistribution.constant_eq, Ne.symm]) + rw [← hchoi, ← MatrixMap.IsTracePreserving_iff_trace_choi] + intro X + change ∑ x, ∑ i, X i i * (τ i).m x x = X.trace + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun i _ => ?_ + rw [← Finset.mul_sum, show ∑ x, (τ i).m x x = 1 by + simpa [Matrix.trace] using (MState.tr' (ρ := τ i))] + simp [Matrix.diag_apply]) + +/-- Applying a preparation channel to a classical distribution gives the corresponding mixture. -/ +theorem cqPrepare_apply_ofClassical {κ : Type u} [Fintype κ] [DecidableEq κ] + (τ : κ → MState d) (dist : ProbDistribution κ) : + (cqPrepare (d := d) τ (MState.ofClassical dist)).m = + ∑ i, (dist i : ℝ) • (τ i).m := by + let prepMap : MatrixMap κ d ℂ := { + toFun X := fun b₁ b₂ => ∑ i, X i i * (τ i).m b₁ b₂ + map_add' X Y := by + ext b₁ b₂ + simp [Matrix.add_apply, Finset.sum_add_distrib, add_mul] + map_smul' c X := by + ext b₁ b₂ + simp [Matrix.smul_apply, Finset.mul_sum, mul_assoc] } + have hchoi : prepMap.choi_matrix = + (∑ i, HermitianMat.kronecker (τ i).M (MState.ofClassical (.constant i)).M).mat := by + ext ⟨b₁, a₁⟩ ⟨b₂, a₂⟩ + simp only [MatrixMap.choi_matrix, prepMap, Matrix.single, + HermitianMat.mat_finset_sum, Matrix.sum_apply] + refine Finset.sum_congr rfl fun x _ => ?_ + show (if a₁ = x ∧ a₂ = x then 1 else 0) * (τ x).m b₁ b₂ = + (τ x).m b₁ b₂ * + (HermitianMat.diagonal ℂ + (fun x₁ => ((ProbDistribution.constant x) x₁ : ℝ))).mat a₁ a₂ + rw [HermitianMat.diagonal_mat] + aesop (add simp [Matrix.diagonal, ProbDistribution.constant_eq, Ne.symm]) + change MatrixMap.of_choi_matrix ((∑ i, HermitianMat.kronecker (τ i).M + (MState.ofClassical (.constant i)).M).mat) (MState.ofClassical dist).m = _ + rw [← hchoi, MatrixMap.choi_map_inv] + ext b₁ b₂ + change ∑ i, (Matrix.diagonal fun x => ((dist x : Prob) : ℂ)) i i * (τ i).m b₁ b₂ = + (∑ i, (dist i : ℝ) • (τ i).m) b₁ b₂ + rw [Matrix.sum_apply] + simp [Matrix.smul_apply] + +end CPTPMap diff --git a/QuantumInfo/Finite/Entropy/Relative.lean b/QuantumInfo/Finite/Entropy/Relative.lean index ea1b814df..26565decf 100644 --- a/QuantumInfo/Finite/Entropy/Relative.lean +++ b/QuantumInfo/Finite/Entropy/Relative.lean @@ -273,105 +273,6 @@ lemma HermitianMat.rpow_neg_mul_rpow_eq_supportProj convert congr_arg ( fun x : HermitianMat d ℂ => x.val ) h_cfc_eq using 1; exact congr_arg ( fun x : HermitianMat d ℂ => x.val ) ( supportProj_eq_cfc A ) -lemma HermitianMat.supportProj_mul_self (A : HermitianMat d ℂ) : - A.supportProj.mat * A.mat = A.mat := by - have h_supportProj_mul_A : ∀ (v : d → ℂ), (A.supportProj.val.mulVec (A.val.mulVec v)) = (A.val.mulVec v) := by - intro v - have h_range : WithLp.toLp 2 (A.val.mulVec v) ∈ LinearMap.range A.val.toEuclideanLin := by - exact ⟨ _, rfl ⟩ - have h_supportProj_mul_A : ∀ (v : EuclideanSpace ℂ d), v ∈ LinearMap.range A.val.toEuclideanLin → (A.supportProj.val.toEuclideanLin v) = v := by - intro v hv - have h_supportProj_mul_A : (A.supportProj.val.toEuclideanLin v) = (Submodule.orthogonalProjection (LinearMap.range A.val.toEuclideanLin) v) := by - simp only [val_eq_coe, Submodule.coe_orthogonalProjection_apply] - simp [supportProj, projector] - simp only [Submodule.starProjection] - simp [-Submodule.coe_orthogonalProjection_apply] - have key : ∀ (f : EuclideanSpace ℂ d →ₗ[ℂ] EuclideanSpace ℂ d), - Matrix.toEuclideanLin - ((LinearMap.toMatrix (EuclideanSpace.basisFun d ℂ).toBasis (EuclideanSpace.basisFun d ℂ).toBasis) f) = f := by - intro f - rw [Matrix.toEuclideanLin, Matrix.toLpLin_eq_toLin] - exact Matrix.toLin_toMatrix _ _ f - have hsup : A.support = (Matrix.toEuclideanLin (↑A : Matrix d d ℂ)).range := by - simp [HermitianMat.support, HermitianMat.lin] - rw [key, LinearMap.comp_apply, Submodule.subtype_apply, hsup] - rfl - rw [h_supportProj_mul_A] - exact Submodule.eq_starProjection_of_mem_of_inner_eq_zero (by simpa using hv) (by simp) - exact congr(WithLp.ofLp $(h_supportProj_mul_A _ h_range)) - exact Matrix.toLin'.injective ( LinearMap.ext fun v => by simpa using h_supportProj_mul_A v ) - -set_option backward.isDefEq.respectTransparency false in -lemma HermitianMat.inner_supportProj_self (A : HermitianMat d ℂ) : - ⟪A, A.supportProj⟫ = A.trace := by - simp only [trace, IsMaximalSelfAdjoint.RCLike_selfadjMap, Matrix.trace, Matrix.diag_apply, - mat_apply, map_sum, RCLike.re_to_complex] - simp only [inner, IsMaximalSelfAdjoint.RCLike_selfadjMap, RCLike.re_to_complex]; - convert congr_arg Complex.re ( congr_arg Matrix.trace ( HermitianMat.supportProj_mul_self A ) ) using 1; - · simp only [Matrix.trace, Matrix.diag_apply, Matrix.mul_apply, mat_apply, Complex.re_sum, - Complex.mul_re, Finset.sum_sub_distrib, mul_comm]; - exact congrArg₂ _ ( Finset.sum_comm ) ( Finset.sum_comm ); - · simp only [Matrix.trace, Matrix.diag_apply, mat_apply, Complex.re_sum] - -lemma HermitianMat.mul_supportProj_of_ker_le {A B : HermitianMat d ℂ} - (h : LinearMap.ker B.lin.toLinearMap ≤ LinearMap.ker A.lin.toLinearMap) : - A.mat * B.supportProj.mat = A.mat := by - -- Since $B.supportProj$ is the projection onto $range B$, we have $B.supportProj * B.mat = B.mat$. - have h_supportProj_mul_B : B.supportProj.mat * B.mat = B.mat := by - exact supportProj_mul_self B - have h_range_A_subset_range_B : LinearMap.range A.lin.toLinearMap ≤ LinearMap.range B.lin.toLinearMap := by - have h_orthogonal_complement : LinearMap.range (B.lin : EuclideanSpace ℂ d →ₗ[ℂ] EuclideanSpace ℂ d) = (LinearMap.ker (B.lin : EuclideanSpace ℂ d →ₗ[ℂ] EuclideanSpace ℂ d))ᗮ := by - have h_orthogonal_complement : ∀ (T : EuclideanSpace ℂ d →ₗ[ℂ] EuclideanSpace ℂ d), T = T.adjoint → LinearMap.range T = (LinearMap.ker T)ᗮ := by - intro T hT; - refine' Submodule.eq_of_le_of_finrank_eq _ _; - · rintro x ⟨y, rfl⟩ - rw [Submodule.mem_orthogonal' (LinearMap.ker T) (T y)] - intro z hz - rw [LinearMap.mem_ker] at hz - simp [← LinearMap.adjoint_inner_right, ← hT, hz] - · have := LinearMap.finrank_range_add_finrank_ker T; - have := Submodule.finrank_add_finrank_orthogonal (LinearMap.ker T) - linarith; - apply h_orthogonal_complement - simp - have h_orthogonal_complement_A : LinearMap.range (A.lin : EuclideanSpace ℂ d →ₗ[ℂ] EuclideanSpace ℂ d) ≤ (LinearMap.ker (A.lin : EuclideanSpace ℂ d →ₗ[ℂ] EuclideanSpace ℂ d))ᗮ := by - intro x hx y hy - simp_all only [LinearMap.mem_range, ContinuousLinearMap.coe_coe, LinearMap.mem_ker] - obtain ⟨ z, rfl ⟩ := hx; - have h_orthogonal_complement_A : ∀ (y z : EuclideanSpace ℂ d), ⟪y, A.lin z⟫_ℂ = ⟪A.lin y, z⟫_ℂ := by - simp - rw [ h_orthogonal_complement_A, hy, inner_zero_left ]; - exact h_orthogonal_complement.symm ▸ le_trans h_orthogonal_complement_A ( Submodule.orthogonal_le h ); - -- Since $B.supportProj$ is the projection onto $range B$, and $range A \subseteq range B$, we have $B.supportProj * A = A$. - have h_supportProj_mul_A : ∀ (v : EuclideanSpace ℂ d), B.supportProj.mat.mulVec (A.mat.mulVec v) = A.mat.mulVec v := by - intro v - obtain ⟨w, hw⟩ : WithLp.toLp 2 (A.mat.mulVec v) ∈ LinearMap.range B.lin.toLinearMap := by - exact h_range_A_subset_range_B ( Set.mem_range_self v ); - replace h_supportProj_mul_B := congr(Matrix.mulVec $h_supportProj_mul_B w) - replace hw := congr(WithLp.ofLp $hw) - simp only [ContinuousLinearMap.coe_coe] at hw - simpa only [← hw, ← Matrix.mulVec_mulVec] using h_supportProj_mul_B - -- By definition of matrix multiplication, if B.supportProj * A * v = A * v for all vectors v, then B.supportProj * A = A. - have h_matrix_eq : ∀ (M N : Matrix d d ℂ), (∀ v : EuclideanSpace ℂ d, M.mulVec (N.mulVec v) = N.mulVec v) → M * N = N := by - intro M N hMN - ext i j - specialize hMN (WithLp.toLp 2 ( Pi.single j 1 )) - replace hMN := congr_fun hMN i - aesop; - rw [← Matrix.conjTranspose_inj] - simp_all only [Matrix.mulVec_mulVec, Matrix.conjTranspose_mul, conjTranspose_mat, implies_true] - -set_option backward.isDefEq.respectTransparency false in -lemma HermitianMat.inner_supportProj_of_ker_le {A B : HermitianMat d ℂ} - (h : LinearMap.ker B.lin.toLinearMap ≤ LinearMap.ker A.lin.toLinearMap) : - ⟪A, B.supportProj⟫ = A.trace := by - rw [inner_def, mul_supportProj_of_ker_le h, trace] - -lemma supportProj_inner_density (h : σ.M.ker ≤ ρ.M.ker) : - ⟪σ.M.supportProj, ρ.M⟫_ℝ = 1 := by - rw [HermitianMat.inner_comm, HermitianMat.inner_supportProj_of_ker_le h] - simp - set_option backward.isDefEq.respectTransparency false in /- ⟪ρ.M.conj (σ.M ^ t).mat, σ.M ^ (-2 * t)⟫_ℝ = 1 for density matrices ρ, σ with ker(σ) ≤ ker(ρ). @@ -390,7 +291,8 @@ private lemma sandwiched_inner_eq_one (h : σ.M.ker ≤ ρ.M.ker) (t : ℝ) : rw [HermitianMat.inner_def, HermitianMat.conj_apply_mat, HermitianMat.conjTranspose_mat] rw [Matrix.trace_mul_comm, ← mul_assoc, ← mul_assoc, h_combine] rw [Matrix.trace_mul_cycle, h_support, ← HermitianMat.inner_def] - exact supportProj_inner_density h + rw [← ρ.tr, HermitianMat.inner_comm, HermitianMat.inner_def, + HermitianMat.mul_supportProj_of_ker_le h, HermitianMat.trace] private theorem sandwiched_trace_of_gt_1 (h : σ.M.ker ≤ ρ.M.ker) (hα : α > 1) : 1 ≤ ((ρ.M.conj (σ.M ^ ((1 - α)/(2 * α)) ).mat) ^ α).trace := by @@ -1476,10 +1378,14 @@ theorem sandwichedRelRentropy_additive_alpha_one_aux (ρ₁ σ₁ : MState d₁) constructor <;> apply HermitianMat.log_kron_with_proj; have h_inner_supportProj : ∀ (A : HermitianMat d₁ ℂ) (B : HermitianMat d₂ ℂ), ⟪A ⊗ₖ B, ρ₁ ⊗ᴹ ρ₂⟫ = ⟪A, ρ₁⟫ * ⟪B, ρ₂⟫ := by exact fun A B => HermitianMat.inner_kron A B ρ₁ ρ₂; - simp only [HermitianMat.ker] at h1 h2 + have h1_support : ⟪ρ₁.M, σ₁.M.supportProj⟫ = 1 := by + rw [← ρ₁.tr, HermitianMat.inner_def, HermitianMat.mul_supportProj_of_ker_le h1, + HermitianMat.trace] + have h2_support : ⟪ρ₂.M, σ₂.M.supportProj⟫ = 1 := by + rw [← ρ₂.tr, HermitianMat.inner_def, HermitianMat.mul_supportProj_of_ker_le h2, + HermitianMat.trace] simp_all only [inner_sub_right, inner_add_right, real_inner_comm, - HermitianMat.inner_supportProj_self, MState.tr, mul_one, one_mul, - HermitianMat.inner_supportProj_of_ker_le] + HermitianMat.inner_supportProj_self, MState.tr, mul_one, one_mul] abel /-- The Sandwiched Renyi Relative Entropy, defined with ln (nits). Note that at `α = 1` this definition @@ -2430,7 +2336,8 @@ private lemma HermitianMat.inner_log_sub_le_log_alpha (ρ : MState d) {σ₁ σ rw [h_log_smul] at h_log_mono simp only [add_comm, sub_eq_add_neg, neg_add_rev] at h_log_mono h_log_smul ⊢ have h_inner_support : ⟪ρ.M, σ₁.M.supportProj⟫ = 1 := by - rw [HermitianMat.inner_supportProj_of_ker_le hker₁, ρ.tr] + rw [← ρ.tr, HermitianMat.inner_def, HermitianMat.mul_supportProj_of_ker_le hker₁, + HermitianMat.trace] simp_all [← add_assoc, inner_add_right, inner_smul_right] set_option backward.isDefEq.respectTransparency false in diff --git a/QuantumInfo/Finite/ProductPower.lean b/QuantumInfo/Finite/ProductPower.lean new file mode 100644 index 000000000..ade975dc3 --- /dev/null +++ b/QuantumInfo/Finite/ProductPower.lean @@ -0,0 +1,198 @@ +/- +Copyright (c) 2026 Dennj Osele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Dennj Osele +-/ +module + +public import QuantumInfo.ClassicalInfo.Hellinger +public import QuantumInfo.Finite.AxiomatizedEntropy.Defs + +public import Mathlib.Data.Fin.Tuple.Basic + +/-! # Finite product powers + +This file contains product-power API for finite probability distributions and finite quantum +states, using the canonical coordinate type `Fin n → d`. +-/ + +@[expose] public section + +noncomputable section +universe u v + +open scoped BigOperators +open scoped ENNReal +open scoped Kronecker +open scoped HermitianMat +open ComplexOrder + +namespace ProbDistribution + +variable {ι : Type u} [Fintype ι] [DecidableEq ι] +variable {α : ι → Type v} [∀ i, Fintype (α i)] + +/-- Product of finitely many probability distributions, indexed by a Pi type. -/ +def piProd (P : ∀ i, ProbDistribution (α i)) : ProbDistribution (∀ i, α i) := + mk' (α := ∀ i, α i) (fun x => ∏ i, (P i (x i) : ℝ)) + (fun x => Finset.prod_nonneg fun i _ => (P i (x i)).2.1) + (by simpa using (Fintype.prod_sum (fun i x => ((P i) x : ℝ))).symm) + +@[simp] +theorem piProd_apply_coe (P : ∀ i, ProbDistribution (α i)) (x : ∀ i, α i) : + ((piProd P x : Prob) : ℝ) = ∏ i, (P i (x i) : ℝ) := + rfl + +variable {d : Type u} [Fintype d] + +/-- The `n`-fold independent product power of a probability distribution. -/ +def npow (P : ProbDistribution d) (n : ℕ) : ProbDistribution (Fin n → d) := + piProd fun _ => P + +@[simp] +theorem npow_apply_coe (P : ProbDistribution d) (n : ℕ) (x : Fin n → d) : + ((npow P n x : Prob) : ℝ) = ∏ i, (P (x i) : ℝ) := + rfl + +theorem hellingerOverlap_piProd (P Q : ∀ i, ProbDistribution (α i)) : + hellingerOverlap (piProd P) (piProd Q) = ∏ i, hellingerOverlap (P i) (Q i) := by + rw [hellingerOverlap] + calc + (∑ x : ∀ i, α i, + Real.sqrt (((piProd P x : Prob) : ℝ) * ((piProd Q x : Prob) : ℝ))) = + ∑ x : ∀ i, α i, ∏ i, Real.sqrt ((P i (x i) : ℝ) * (Q i (x i) : ℝ)) := by + refine Finset.sum_congr rfl fun x _ => ?_ + rw [piProd_apply_coe, piProd_apply_coe, ← Finset.prod_mul_distrib, + Real.sqrt_prod] + exact fun i _ => mul_nonneg (P i (x i)).2.1 (Q i (x i)).2.1 + _ = ∏ i, hellingerOverlap (P i) (Q i) := by + simpa [hellingerOverlap] using + (Fintype.prod_sum fun i x => Real.sqrt ((P i x : ℝ) * (Q i x : ℝ))).symm + +/-- Hellinger overlap of independent product powers. -/ +theorem hellingerOverlap_npow (P Q : ProbDistribution d) (n : ℕ) : + hellingerOverlap (npow P n) (npow Q n) = (hellingerOverlap P Q) ^ n := by + simpa [npow] using hellingerOverlap_piProd (fun _ : Fin n => P) fun _ : Fin n => Q + +end ProbDistribution + +namespace HermitianMat + +variable {m n : Type u} [Fintype m] [Fintype n] +variable {A B : HermitianMat m ℂ} {C D : HermitianMat n ℂ} + +omit [Fintype m] in +private theorem reindex_le_reindex_iff {m' : Type u} [Fintype m'] + (e : m ≃ m') (A B : HermitianMat m ℂ) : + A.reindex e ≤ B.reindex e ↔ A ≤ B := by + rw [HermitianMat.le_iff, HermitianMat.le_iff] + simp only [HermitianMat.reindex_sub, HermitianMat.mat_reindex] + change ((B - A).mat.submatrix e.symm e.symm).PosSemidef ↔ (B - A).mat.PosSemidef + exact Matrix.posSemidef_submatrix_equiv e.symm + +private theorem kronecker_mono (hA : 0 ≤ A) (hD : 0 ≤ D) + (hAB : A ≤ B) (hCD : C ≤ D) : + A ⊗ₖ C ≤ B ⊗ₖ D := by + rw [← sub_nonneg] + have hEq : B ⊗ₖ D - A ⊗ₖ C = A ⊗ₖ (D - C) + (B - A) ⊗ₖ D := by + ext ⟨i, k⟩ ⟨j, l⟩ + change (B ⊗ₖ D - A ⊗ₖ C).mat (i, k) (j, l) = + (A ⊗ₖ (D - C) + (B - A) ⊗ₖ D).mat (i, k) (j, l) + simp only [HermitianMat.mat_sub, HermitianMat.mat_add, HermitianMat.kronecker_mat, + Matrix.sub_apply, Matrix.add_apply, Matrix.kroneckerMap_apply] + ring + simpa [hEq] using add_nonneg + (HermitianMat.kronecker_nonneg hA (sub_nonneg.mpr hCD)) + (HermitianMat.kronecker_nonneg (sub_nonneg.mpr hAB) hD) + +end HermitianMat + +namespace MState + +variable {d : Type u} [Fintype d] [DecidableEq d] + +/-- Classical states commute with finite product powers. -/ +theorem ofClassical_npow (P : ProbDistribution d) (n : ℕ) : + (MState.ofClassical P) ⊗ᴹ^ n = MState.ofClassical (ProbDistribution.npow P n) := by + apply MState.ext_m + ext x y + change (∏ i : Fin n, if x i = y i then (((P (x i)) : Prob) : ℂ) else 0) = + if x = y then (((ProbDistribution.npow P n x) : Prob) : ℂ) else 0 + by_cases hxy : x = y + · subst y + rw [if_pos rfl] + simp only [↓reduceIte] + exact_mod_cast (ProbDistribution.npow_apply_coe P n x).symm + · obtain ⟨i, hi⟩ := Function.ne_iff.mp hxy + rw [if_neg hxy] + exact Finset.prod_eq_zero (Finset.mem_univ i) (by simp [hi]) + +def npowSuccEquiv (n : ℕ) (d : Type u) : + (Fin (n + 1) → d) ≃ (Fin n → d) × d := + (Fin.snocEquiv (fun _ : Fin (n + 1) => d)).symm.trans + (Equiv.prodComm d (Fin n → d)) + +/-- Product powers unfold by splitting off the last tensor factor. -/ +theorem npow_succ (ρ : MState d) (n : ℕ) : + MState.npow ρ (n + 1) = ((MState.npow ρ n) ⊗ᴹ ρ).relabel (npowSuccEquiv n d) := by + apply MState.ext_m + ext x y + simp [MState.npow, MState.piProd, MState.prod, MState.relabel_m, Matrix.piProd, + npowSuccEquiv, Fin.snocEquiv] + change (∏ i : Fin (n + 1), ρ.m (x i) (y i)) = + (∏ i : Fin n, ρ.m (x i.castSucc) (y i.castSucc)) * + ρ.m (x (Fin.last n)) (y (Fin.last n)) + rw [Fin.prod_univ_castSucc] + +/-- Product powers preserve exponential Loewner bounds. -/ +theorem npow_le_exp_smul {ρ σ : MState d} {x : ℝ} + (h : ρ.M ≤ Real.exp x • σ.M) : + ∀ n, (MState.npow ρ n).M ≤ Real.exp ((n : ℝ) * x) • (MState.npow σ n).M := by + intro n + induction n with + | zero => + have hσ0 : MState.npow σ 0 = MState.npow ρ 0 := by + apply MState.ext_m; ext x y; simp [MState.npow, MState.piProd, Matrix.piProd] + simp [hσ0] + | succ n ih => + rw [MState.npow_succ ρ n, MState.npow_succ σ n] + rw [MState.relabel_M, MState.relabel_M, ← HermitianMat.reindex_smul, + HermitianMat.reindex_le_reindex_iff] + have hscale : + ((Real.exp ((n : ℝ) * x) • (MState.npow σ n).M) ⊗ₖ + (Real.exp x • σ.M) : + HermitianMat ((Fin n → d) × d) ℂ) = + Real.exp (((n + 1 : ℕ) : ℝ) * x) • + ((MState.npow σ n).M ⊗ₖ σ.M) := by + ext1 + simp [Matrix.smul_kronecker, Matrix.kronecker_smul, smul_smul] + rw [mul_comm (Real.exp x), ← Real.exp_add] + ring_nf + simpa [MState.prod, hscale] using + HermitianMat.kronecker_mono (MState.npow ρ n).nonneg + (smul_nonneg (by positivity) σ.nonneg) ih h + +end MState + +namespace RelEntropy + +variable (f : ∀ {d : Type u} [Fintype d] [DecidableEq d], MState d → HermitianMat d ℂ → ℝ≥0∞) +variable {d : Type u} [Fintype d] [DecidableEq d] + +/-- Relative entropy is additive over finite product powers. -/ +theorem of_npow [RelEntropy f] (ρ σ : MState d) : + ∀ n, f (MState.npow ρ n) (MState.npow σ n).M = ((n : ℕ) : ENNReal) * f ρ σ := by + intro n + induction n with + | zero => + have hσ0 : MState.npow σ 0 = MState.npow ρ 0 := by + apply MState.ext_m + ext x y + simp [MState.npow, MState.piProd, Matrix.piProd] + simp [hσ0] + | succ n ih => + rw [MState.npow_succ ρ n, MState.npow_succ σ n] + rw [RelEntropy.relabel_eq (f := f) (MState.npowSuccEquiv n d), + RelEntropy.of_kron (f := f), ih, Nat.cast_succ, add_mul, one_mul, add_comm] + +end RelEntropy diff --git a/QuantumInfo/ForMathlib/HermitianMat/Proj.lean b/QuantumInfo/ForMathlib/HermitianMat/Proj.lean index 9e7ca0e1b..50e1ccb5a 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Proj.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Proj.lean @@ -210,6 +210,121 @@ theorem supportProj_eq_cfc : A.supportProj = A.cfc (if · = 0 then 0 else 1) := simp [ Finset.sum_ite, Finset.filter_eq, Finset.filter_and ]; rw [ Finset.sum_eq_single i ] <;> aesop +section ComplexSupport + +variable {d : Type*} [Fintype d] [DecidableEq d] + +open RealInnerProductSpace + +/-- The support projection acts as the identity on the range of a Hermitian matrix. -/ +lemma supportProj_mul_self (A : HermitianMat d ℂ) : + A.supportProj.mat * A.mat = A.mat := by + have h_supportProj_mul_A : + ∀ v : d → ℂ, A.supportProj.val.mulVec (A.val.mulVec v) = A.val.mulVec v := by + intro v + have h_range : WithLp.toLp 2 (A.val.mulVec v) ∈ LinearMap.range A.val.toEuclideanLin := by + exact ⟨ _, rfl ⟩ + have h_supportProj_mul_A : + ∀ v : EuclideanSpace ℂ d, + v ∈ LinearMap.range A.val.toEuclideanLin → A.supportProj.val.toEuclideanLin v = v := by + intro v hv + have h_supportProj_mul_A : + A.supportProj.val.toEuclideanLin v = + Submodule.orthogonalProjection (LinearMap.range A.val.toEuclideanLin) v := by + simp only [val_eq_coe, Submodule.coe_orthogonalProjection_apply] + simp [supportProj, projector] + simp only [Submodule.starProjection] + simp [-Submodule.coe_orthogonalProjection_apply] + have key : ∀ (f : EuclideanSpace ℂ d →ₗ[ℂ] EuclideanSpace ℂ d), + Matrix.toEuclideanLin + ((LinearMap.toMatrix (EuclideanSpace.basisFun d ℂ).toBasis + (EuclideanSpace.basisFun d ℂ).toBasis) f) = f := by + intro f + rw [Matrix.toEuclideanLin, Matrix.toLpLin_eq_toLin] + exact Matrix.toLin_toMatrix _ _ f + have hsup : A.support = (Matrix.toEuclideanLin (↑A : Matrix d d ℂ)).range := by + simp [HermitianMat.support, HermitianMat.lin] + rw [key, LinearMap.comp_apply, Submodule.subtype_apply, hsup] + rfl + rw [h_supportProj_mul_A] + exact Submodule.eq_starProjection_of_mem_of_inner_eq_zero (by simpa using hv) (by simp) + exact congr(WithLp.ofLp $(h_supportProj_mul_A _ h_range)) + exact Matrix.toLin'.injective (LinearMap.ext fun v => by simpa using h_supportProj_mul_A v) + +set_option backward.isDefEq.respectTransparency false in +/-- The trace of a Hermitian matrix is its inner product with its support projection. -/ +lemma inner_supportProj_self (A : HermitianMat d ℂ) : + ⟪A, A.supportProj⟫ = A.trace := by + simp only [trace, IsMaximalSelfAdjoint.RCLike_selfadjMap, Matrix.trace, Matrix.diag_apply, + mat_apply, map_sum, RCLike.re_to_complex] + simp only [inner, IsMaximalSelfAdjoint.RCLike_selfadjMap, RCLike.re_to_complex] + convert congr_arg Complex.re (congr_arg Matrix.trace (HermitianMat.supportProj_mul_self A)) using 1 + · simp only [Matrix.trace, Matrix.diag_apply, Matrix.mul_apply, mat_apply, Complex.re_sum, + Complex.mul_re, Finset.sum_sub_distrib, mul_comm] + exact congrArg₂ _ Finset.sum_comm Finset.sum_comm + · simp only [Matrix.trace, Matrix.diag_apply, mat_apply, Complex.re_sum] + +/-- If the kernel of `B` is contained in the kernel of `A`, then the support projection of `B` +acts as the identity on `A`. -/ +lemma mul_supportProj_of_ker_le {A B : HermitianMat d ℂ} + (h : B.ker ≤ A.ker) : + A.mat * B.supportProj.mat = A.mat := by + have h_supportProj_mul_B : B.supportProj.mat * B.mat = B.mat := by + exact supportProj_mul_self B + have h_range_A_subset_range_B : + LinearMap.range A.lin.toLinearMap ≤ LinearMap.range B.lin.toLinearMap := by + have h_orthogonal_complement : + LinearMap.range (B.lin : EuclideanSpace ℂ d →ₗ[ℂ] EuclideanSpace ℂ d) = + (LinearMap.ker (B.lin : EuclideanSpace ℂ d →ₗ[ℂ] EuclideanSpace ℂ d))ᗮ := by + have h_orthogonal_complement : + ∀ T : EuclideanSpace ℂ d →ₗ[ℂ] EuclideanSpace ℂ d, + T = T.adjoint → LinearMap.range T = (LinearMap.ker T)ᗮ := by + intro T hT + refine' Submodule.eq_of_le_of_finrank_eq _ _ + · rintro x ⟨y, rfl⟩ + rw [Submodule.mem_orthogonal' (LinearMap.ker T) (T y)] + intro z hz + rw [LinearMap.mem_ker] at hz + simp [← LinearMap.adjoint_inner_right, ← hT, hz] + · have := LinearMap.finrank_range_add_finrank_ker T + have := Submodule.finrank_add_finrank_orthogonal (LinearMap.ker T) + linarith + apply h_orthogonal_complement + simp + have h_orthogonal_complement_A : + LinearMap.range (A.lin : EuclideanSpace ℂ d →ₗ[ℂ] EuclideanSpace ℂ d) ≤ + (LinearMap.ker (A.lin : EuclideanSpace ℂ d →ₗ[ℂ] EuclideanSpace ℂ d))ᗮ := by + intro x hx y hy + simp_all only [LinearMap.mem_range, ContinuousLinearMap.coe_coe, LinearMap.mem_ker] + obtain ⟨z, rfl⟩ := hx + have h_orthogonal_complement_A : + ∀ y z : EuclideanSpace ℂ d, ⟪y, A.lin z⟫_ℂ = ⟪A.lin y, z⟫_ℂ := by + simp + rw [h_orthogonal_complement_A, hy, inner_zero_left] + exact h_orthogonal_complement.symm ▸ + le_trans h_orthogonal_complement_A (Submodule.orthogonal_le h) + have h_supportProj_mul_A : + ∀ v : EuclideanSpace ℂ d, B.supportProj.mat.mulVec (A.mat.mulVec v) = A.mat.mulVec v := by + intro v + obtain ⟨w, hw⟩ : WithLp.toLp 2 (A.mat.mulVec v) ∈ LinearMap.range B.lin.toLinearMap := by + exact h_range_A_subset_range_B (Set.mem_range_self v) + replace h_supportProj_mul_B := congr(Matrix.mulVec $h_supportProj_mul_B w) + replace hw := congr(WithLp.ofLp $hw) + simp only [ContinuousLinearMap.coe_coe] at hw + simpa only [← hw, ← Matrix.mulVec_mulVec] using h_supportProj_mul_B + have h_matrix_eq : + ∀ M N : Matrix d d ℂ, + (∀ v : EuclideanSpace ℂ d, M.mulVec (N.mulVec v) = N.mulVec v) → M * N = N := by + intro M N hMN + ext i j + specialize hMN (WithLp.toLp 2 (Pi.single j 1)) + replace hMN := congr_fun hMN i + aesop + rw [← Matrix.conjTranspose_inj] + simp_all only [Matrix.mulVec_mulVec, Matrix.conjTranspose_mul, conjTranspose_mat, implies_true] + +end ComplexSupport + /-- Projector onto the non-negative eigenspace of `B - A`. Accessible by the notation `{A ≤ₚ B}`, which is scoped to `HermitianMat`. This is the unique maximum operator `P` such that `P^2 = P` and `P * A * P ≤ P * B * P` in the Loewner order. -/