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..c7d405f82 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_of_one_le (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 diff --git a/QuantumInfo/Finite/CPTPMap/CPTP.lean b/QuantumInfo/Finite/CPTPMap/CPTP.lean index 88362e367..e4afd15d9 100644 --- a/QuantumInfo/Finite/CPTPMap/CPTP.lean +++ b/QuantumInfo/Finite/CPTPMap/CPTP.lean @@ -357,6 +357,16 @@ def prod (Λ₁ : CPTPMap dI₁ dO₁) (Λ₂ : CPTPMap dI₂ dO₂) : CPTPMap ( infixl:70 "⊗ᶜᵖ" => CPTPMap.prod +/-- Tensor products commute with channel application: +`(Λ₁ ⊗ᶜᵖ Λ₂) (ρ₁ ⊗ᴹ ρ₂) = Λ₁ ρ₁ ⊗ᴹ Λ₂ ρ₂`. -/ +@[simp] +theorem prod_apply_prod (Λ₁ : CPTPMap dI₁ dO₁) (Λ₂ : CPTPMap dI₂ dO₂) + (ρ₁ : MState dI₁) (ρ₂ : MState dI₂) : + (Λ₁ ⊗ᶜᵖ Λ₂) (ρ₁ ⊗ᴹ ρ₂) = (Λ₁ ρ₁) ⊗ᴹ (Λ₂ ρ₂) := by + apply MState.ext_m + simpa [CPTPMap.prod, MState.prod] using + MatrixMap.kron_map_of_kron_state Λ₁.map Λ₂.map ρ₁.m ρ₂.m + end prod section finprod diff --git a/QuantumInfo/Finite/CPTPMap/Dual.lean b/QuantumInfo/Finite/CPTPMap/Dual.lean index 4f250528a..eb9aeabb0 100644 --- a/QuantumInfo/Finite/CPTPMap/Dual.lean +++ b/QuantumInfo/Finite/CPTPMap/Dual.lean @@ -16,6 +16,7 @@ Definitions and theorems about the dual of a matrix map. -/ noncomputable section open ComplexOrder +open scoped Kronecker variable {dIn dOut : Type*} [Fintype dIn] [Fintype dOut] variable {R : Type*} [CommRing R] @@ -32,25 +33,83 @@ variable [DecidableEq dIn] [DecidableEq dOut] {M : MatrixMap dIn dOut 𝕜} called the adjoint of the map instead. -/ @[irreducible] def dual (M : MatrixMap dIn dOut R) : MatrixMap dOut dIn R := - let iso1 := (Module.Basis.toDualEquiv <| Matrix.stdBasis R dIn dIn).symm - let iso2 := (Module.Basis.toDualEquiv <| Matrix.stdBasis R dOut dOut) - iso1 ∘ₗ LinearMap.dualMap M ∘ₗ iso2 + let coordDual := + let iso1 := (Module.Basis.toDualEquiv <| Matrix.stdBasis R dIn dIn).symm + let iso2 := (Module.Basis.toDualEquiv <| Matrix.stdBasis R dOut dOut) + iso1 ∘ₗ LinearMap.dualMap M ∘ₗ iso2 + (Matrix.transposeLinearEquiv dIn dIn R R).toLinearMap ∘ₗ coordDual ∘ₗ + (Matrix.transposeLinearEquiv dOut dOut R R).toLinearMap /-- The defining property of a dual map: inner products are preserved on the opposite argument. -/ theorem Dual.trace_eq (M : MatrixMap dIn dOut R) (A : Matrix dIn dIn R) (B : Matrix dOut dOut R) : (M A * B).trace = (A * M.dual B).trace := by - unfold dual - dsimp [Matrix.trace] - rw [LinearMap.dualMap_apply'] - simp_rw [Matrix.mul_apply] - sorry + have hDualIn (X Y : Matrix dIn dIn R) : + ((Matrix.stdBasis R dIn dIn).toDualEquiv Y) X = (X * Y.transpose).trace := by + simp [Module.Basis.toDualEquiv_apply, Module.Basis.toDual, Matrix.trace, Matrix.mul_apply, + Matrix.stdBasis, Fintype.sum_prod_type, mul_comm] + have hDualOut (X Y : Matrix dOut dOut R) : + ((Matrix.stdBasis R dOut dOut).toDualEquiv Y) X = (X * Y.transpose).trace := by + simp [Module.Basis.toDualEquiv_apply, Module.Basis.toDual, Matrix.trace, Matrix.mul_apply, + Matrix.stdBasis, Fintype.sum_prod_type, mul_comm] + let coordDual : MatrixMap dOut dIn R := + let iso1 := (Module.Basis.toDualEquiv <| Matrix.stdBasis R dIn dIn).symm + let iso2 := (Module.Basis.toDualEquiv <| Matrix.stdBasis R dOut dOut) + iso1 ∘ₗ LinearMap.dualMap M ∘ₗ iso2 + rw [show (M A * B).trace = + ((Matrix.stdBasis R dOut dOut).toDualEquiv B.transpose) (M A) by + simpa using (hDualOut (M A) B.transpose).symm] + rw [show + ((Matrix.stdBasis R dOut dOut).toDualEquiv B.transpose) (M A) = + ((Matrix.stdBasis R dIn dIn).toDualEquiv (coordDual B.transpose)) A by + simp [coordDual]] + simpa [dual, coordDual] using hDualIn A (coordDual B.transpose) --all properties below should provable just from `inner_eq`, since the definition of `dual` itself -- is pretty hairy (and maybe could be improved...) /-- The dual of a `IsHermitianPreserving` map also `IsHermitianPreserving`. -/ -theorem IsHermitianPreserving.dual (h : M.IsHermitianPreserving) : M.dual.IsHermitianPreserving := by - sorry +theorem IsHermitianPreserving.dual {M : MatrixMap dIn dOut ℂ} (h : M.IsHermitianPreserving) : + M.dual.IsHermitianPreserving := by + have map_conjTranspose (x : Matrix dIn dIn ℂ) : + M (Matrix.conjTranspose x) = Matrix.conjTranspose (M x) := by + have hxstar : (realPart x : Matrix dIn dIn ℂ) - Complex.I • (imaginaryPart x : Matrix dIn dIn ℂ) = + Matrix.conjTranspose x := by + rw [← Matrix.star_eq_conjTranspose] + have hreal_star : (realPart (star x) : Matrix dIn dIn ℂ) = realPart x := by + rw [realPart_apply_coe, realPart_apply_coe, star_star, add_comm] + have himag_star : (imaginaryPart (star x) : Matrix dIn dIn ℂ) = -imaginaryPart x := by + rw [imaginaryPart_apply_coe, imaginaryPart_apply_coe, star_star] + module + have h := realPart_add_I_smul_imaginaryPart (star x : Matrix dIn dIn ℂ) + rw [hreal_star, himag_star, smul_neg] at h + simpa [sub_eq_add_neg] using h + calc + M (Matrix.conjTranspose x) = M (realPart x - Complex.I • imaginaryPart x) := by + rw [← hxstar] + _ = M (realPart x) - Complex.I • M (imaginaryPart x) := by + simp [sub_eq_add_neg, map_add, map_smul] + _ = Matrix.conjTranspose (M (realPart x) + Complex.I • M (imaginaryPart x)) := by + rw [Matrix.conjTranspose_add, Matrix.conjTranspose_smul] + rw [show Matrix.conjTranspose (M (realPart x)) = M (realPart x) by + simpa [Matrix.IsHermitian] using h (HermitianMat.H _)] + rw [show Matrix.conjTranspose (M (imaginaryPart x)) = M (imaginaryPart x) by + simpa [Matrix.IsHermitian] using h (HermitianMat.H _)] + simp [sub_eq_add_neg] + _ = Matrix.conjTranspose (M x) := by + congr 1 + simpa [map_add, map_smul] using congrArg M (realPart_add_I_smul_imaginaryPart x) + intro x hx + simpa [Matrix.IsHermitian] using show Matrix.conjTranspose (M.dual x) = M.dual x by + apply Matrix.ext_iff_trace_mul_left.mpr + intro A + have htrace2 := congrArg star (Dual.trace_eq M (Matrix.conjTranspose A) (Matrix.conjTranspose x)) + rw [← Matrix.trace_conjTranspose, ← Matrix.trace_conjTranspose] at htrace2 + rw [Matrix.conjTranspose_mul, Matrix.conjTranspose_mul, + Matrix.conjTranspose_conjTranspose, Matrix.conjTranspose_conjTranspose, + map_conjTranspose, hx, Matrix.conjTranspose_conjTranspose, + Matrix.trace_mul_comm x (M A), + Matrix.trace_mul_comm (Matrix.conjTranspose (M.dual x)) A] at htrace2 + exact htrace2.symm.trans (Dual.trace_eq M A x) open MatrixOrder set_option backward.isDefEq.respectTransparency false in @@ -72,7 +131,7 @@ theorem _root_.Matrix.PosSemidef.trace_mul_nonneg {n : Type*} [Fintype n] [Decid Finset.sum_nonneg fun i _ ↦ h.2 (Pi.single i 1) /-- The dual of a `IsPositive` map also `IsPositive`. -/ -theorem IsPositive.dual (h : M.IsPositive) : M.dual.IsPositive := by +theorem IsPositive.dual {M : MatrixMap dIn dOut ℂ} (h : M.IsPositive) : M.dual.IsPositive := by intro x hx rw [Matrix.posSemidef_iff_dotProduct_mulVec] at hx ⊢ use IsHermitianPreserving.dual h.IsHermitianPreserving hx.1 @@ -159,7 +218,26 @@ The dual of the identity map is the identity map. lemma dual_id : (MatrixMap.id dIn 𝕜).dual = MatrixMap.id dIn 𝕜 := by exact dual_unique (id dIn 𝕜) (id dIn 𝕜) fun A_1 => congrFun rfl -set_option maxHeartbeats 600000 in +private theorem matrix_mem_span_kronecker {A C : Type*} [Fintype A] [Fintype C] + [DecidableEq A] [DecidableEq C] (X : Matrix (A × C) (A × C) 𝕜) : + X ∈ Submodule.span 𝕜 + (Set.range (fun p : (Matrix A A 𝕜 × Matrix C C 𝕜) => p.1 ⊗ₖ p.2)) := by + rw [Matrix.matrix_eq_sum_single X] + refine Submodule.sum_mem _ fun ⟨a₁, c₁⟩ _ => + Submodule.sum_mem _ fun ⟨a₂, c₂⟩ _ => ?_ + rw [show Matrix.single (a₁, c₁) (a₂, c₂) (X (a₁, c₁) (a₂, c₂)) = + X (a₁, c₁) (a₂, c₂) • + ((Matrix.single a₁ a₂ 1 : Matrix A A 𝕜) ⊗ₖ + (Matrix.single c₁ c₂ 1 : Matrix C C 𝕜)) by + ext ⟨a, c⟩ ⟨a', c'⟩ + by_cases ha₁ : a₁ = a <;> by_cases hc₁ : c₁ = c <;> + by_cases ha₂ : a₂ = a' <;> by_cases hc₂ : c₂ = c' <;> + simp [Matrix.single, Matrix.kroneckerMap_apply, ha₁, hc₁, ha₂, hc₂]] + exact Submodule.smul_mem _ (X (a₁, c₁) (a₂, c₂)) <| + Submodule.subset_span ⟨ + ((Matrix.single a₁ a₂ 1 : Matrix A A 𝕜), + (Matrix.single c₁ c₂ 1 : Matrix C C 𝕜)), rfl⟩ + set_option backward.isDefEq.respectTransparency false in /-- The dual of a Kronecker product of maps is the Kronecker product of their duals. @@ -168,64 +246,34 @@ lemma dual_kron {A B C D : Type*} [Fintype A] [Fintype B] [Fintype C] [Fintype D [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D] (M : MatrixMap A B 𝕜) (N : MatrixMap C D 𝕜) : (M ⊗ₖₘ N).dual = M.dual ⊗ₖₘ N.dual := by - have h_trace : ∀ (X : Matrix (A × C) (A × C) 𝕜) (Y : Matrix (B × D) (B × D) 𝕜), ( (M ⊗ₖₘ N) X * Y ).trace = ( X * (M.dual ⊗ₖₘ N.dual) Y ).trace := by - -- By definition of dual, we know that $(M x1 * y1).trace = (x1 * M.dual y1).trace$ and $(N x2 * y2).trace = (x2 * N.dual y2).trace$. - have h_dual : ∀ (x1 : Matrix A A 𝕜) (y1 : Matrix B B 𝕜), (M x1 * y1).trace = (x1 * M.dual y1).trace := by - intro x1 y1 - convert MatrixMap.Dual.trace_eq M x1 y1 using 1 - have h_dual_N : ∀ (x2 : Matrix C C 𝕜) (y2 : Matrix D D 𝕜), (N x2 * y2).trace = (x2 * N.dual y2).trace := by - exact fun x2 y2 => MatrixMap.Dual.trace_eq N x2 y2; - intro X Y; - -- By definition of Kronecker product, we can write X and Y as sums of Kronecker products. - obtain ⟨X_sum, hX_sum⟩ : ∃ X_sum : Finset (Matrix A A 𝕜 × Matrix C C 𝕜), X = ∑ p ∈ X_sum, (Matrix.kroneckerMap (fun a b => a * b) p.1 p.2) := by - refine' ⟨ Finset.univ.image fun p : A × A × C × C => ( Matrix.of fun i j => if i = p.1 ∧ j = p.2.1 then X ( p.1, p.2.2.1 ) ( p.2.1, p.2.2.2 ) else 0, Matrix.of fun i j => if i = p.2.2.1 ∧ j = p.2.2.2 then 1 else 0 ), _ ⟩; - ext ⟨a, c⟩ ⟨a', c'⟩; - rw [ Finset.sum_apply, Finset.sum_apply ]; - rw [ Finset.sum_eq_single ( ( Matrix.of fun i j => if i = a ∧ j = a' then X ( a, c ) ( a', c' ) else 0, Matrix.of fun i j => if i = c ∧ j = c' then 1 else 0 ) ) ] <;> simp; - · intro a_1 b x x_1 x_2 x_3 a_2 a_3 a_4 - subst a_3 a_2 - contrapose! a_4; aesop; - · exact fun h => False.elim ( h a a' c c' ( by ext i j; aesop ) ( by ext i j; aesop ) ) - obtain ⟨Y_sum, hY_sum⟩ : ∃ Y_sum : Finset (Matrix B B 𝕜 × Matrix D D 𝕜), Y = ∑ p ∈ Y_sum, (Matrix.kroneckerMap (fun a b => a * b) p.1 p.2) := by - use Finset.image (fun p => (Matrix.of (fun i j => Y (i, p.1) (j, p.2)), Matrix.of (fun i j => if i = p.1 ∧ j = p.2 then 1 else 0))) (Finset.univ : Finset (D × D)); - ext ⟨i, j⟩ ⟨k, l⟩; simp [ Matrix.kroneckerMap ] ; - rw [ Finset.sum_image ] <;> simp [ Matrix.sum_apply ]; - · rw [ Finset.sum_eq_single ( j, l ) ] <;> aesop; - · intro p q h - subst hX_sum - simp_all only [Prod.mk.injEq, EmbeddingLike.apply_eq_iff_eq] - obtain ⟨fst, snd⟩ := p - obtain ⟨fst_1, snd_1⟩ := q - obtain ⟨left, right⟩ := h - simp_all only [Prod.mk.injEq] - apply And.intro - · have := congr_fun ( congr_fun right fst ) snd; aesop; - · replace right := congr_fun ( congr_fun right fst ) snd; aesop; - -- By linearity of the trace and the properties of the Kronecker product, we can expand both sides of the equation. - have h_expand : ∀ (x1 y1 : Matrix A A 𝕜) (x2 y2 : Matrix C C 𝕜) (x3 y3 : Matrix B B 𝕜) (x4 y4 : Matrix D D 𝕜), ( (M ⊗ₖₘ N) (Matrix.kroneckerMap (fun a b => a * b) x1 x2) * Matrix.kroneckerMap (fun a b => a * b) x3 x4 ).trace = ( Matrix.kroneckerMap (fun a b => a * b) x1 x2 * (M.dual ⊗ₖₘ N.dual) (Matrix.kroneckerMap (fun a b => a * b) x3 x4) ).trace := by - intro x1 y1 x2 y2 x3 y3 x4 y4 - simp [MatrixMap.kron_map_of_kron_state] - convert congr_arg₂ ( · * · ) ( h_dual x1 x3 ) ( h_dual_N x2 x4 ) using 1 <;> simp [ Matrix.trace, Matrix.mul_apply, Matrix.kroneckerMap_apply ] - · simp only [Finset.sum_sigma', Finset.sum_mul _ _ _, Finset.mul_sum]; - refine' Finset.sum_bij ( fun x _ => ⟨ ⟨ x.fst.1, x.snd.1 ⟩, ⟨ x.fst.2, x.snd.2 ⟩ ⟩ ) _ _ _ _ <;> simp [ mul_assoc, mul_comm, mul_left_comm ]; - · bound; - · exact fun b => ⟨ _, _, _, _, rfl ⟩; - · simp only [mul_assoc, Finset.mul_sum _ _ _, Finset.sum_mul]; - simp only [← Finset.sum_product', mul_left_comm]; - refine' Finset.sum_bij ( fun x _ => ( x.1.2, x.2.2, x.1.1, x.2.1 ) ) _ _ _ _ <;> simp; - simp_all [ Matrix.trace_sum, Finset.sum_mul _ _ _ ]; - simp [Matrix.mul_sum, h_expand] - apply dual_unique; assumption; + refine dual_unique _ _ ?_ + intro X Y + induction matrix_mem_span_kronecker X using Submodule.span_induction with + | mem X hX => + rcases hX with ⟨⟨x₁, x₂⟩, rfl⟩ + induction matrix_mem_span_kronecker Y using Submodule.span_induction with + | mem Y hY => + rcases hY with ⟨⟨y₁, y₂⟩, rfl⟩ + simp [MatrixMap.kron_map_of_kron_state, ← Matrix.mul_kronecker_mul, + Matrix.trace_kronecker, Dual.trace_eq M x₁ y₁, Dual.trace_eq N x₂ y₂] + | zero => simp + | add Y₁ Y₂ _ _ hY₁ hY₂ => + simpa [map_add, Matrix.mul_add] using congrArg₂ (· + ·) hY₁ hY₂ + | smul a Y _ hY => simpa [map_smul, Matrix.mul_smul] using congrArg (a • ·) hY + | zero => simp + | add X₁ X₂ _ _ hX₁ hX₂ => + simpa [map_add, Matrix.add_mul] using congrArg₂ (· + ·) hX₁ hX₂ + | smul a X _ hX => simpa [map_smul, smul_mul_assoc] using congrArg (a • ·) hX --The dual of a CompletelyPositive map is always CP, more generally it's k-positive -- see Lemma 3.1 of https://www.math.uwaterloo.ca/~krdavids/Preprints/CDPRpositivereal.pdf -theorem IsCompletelyPositive.dual (h : M.IsCompletelyPositive) : M.dual.IsCompletelyPositive := by +theorem IsCompletelyPositive.dual {M : MatrixMap dIn dOut ℂ} (h : M.IsCompletelyPositive) : M.dual.IsCompletelyPositive := by intro n - have h_dual_pos : (MatrixMap.dual (M ⊗ₖₘ MatrixMap.id (Fin n) 𝕜)).IsPositive := by + have h_dual_pos : (MatrixMap.dual (M ⊗ₖₘ MatrixMap.id (Fin n) ℂ)).IsPositive := by exact IsPositive.dual (h n); -- By definition of complete positivity, we know that $(M ⊗ₖₘ id) dually map = M.dual ⊗ₖₘ id.dual$. - have h_dual_kron : (MatrixMap.dual (M ⊗ₖₘ MatrixMap.id (Fin n) 𝕜)) = (MatrixMap.dual M) ⊗ₖₘ (MatrixMap.dual (MatrixMap.id (Fin n) 𝕜)) := by - convert dual_kron M ( MatrixMap.id ( Fin n ) 𝕜 ) using 1; + have h_dual_kron : (MatrixMap.dual (M ⊗ₖₘ MatrixMap.id (Fin n) ℂ)) = (MatrixMap.dual M) ⊗ₖₘ (MatrixMap.dual (MatrixMap.id (Fin n) ℂ)) := by + convert dual_kron M ( MatrixMap.id ( Fin n ) ℂ ) using 1; convert h_dual_pos using 1; rw [ h_dual_kron, dual_id ] @@ -263,43 +311,12 @@ lemma Module.Basis.toDualEquiv_symm_comp_dualMap_toDualEquiv {ι R M : Type*} [F set_option backward.isDefEq.respectTransparency false in @[simp] theorem dual_dual : M.dual.dual = M := by - rw [dual, dual] - simp only [← LinearMap.dualMap_comp_dualMap] - have h₁ : (Matrix.stdBasis 𝕜 dOut dOut).toDualEquiv.symm.toLinearMap ∘ₗ - ((Matrix.stdBasis 𝕜 dOut dOut).toDualEquiv).toLinearMap.dualMap = - (Module.evalEquiv 𝕜 (Matrix dOut dOut 𝕜)).symm.toLinearMap := by - apply Module.Basis.toDualEquiv_symm_comp_dualMap_toDualEquiv - have h₂ : (Matrix.stdBasis 𝕜 dIn dIn).toDualEquiv.symm.toLinearMap.dualMap ∘ₗ - (Matrix.stdBasis 𝕜 dIn dIn).toDualEquiv.toLinearMap = - (Module.evalEquiv 𝕜 (Matrix dIn dIn 𝕜)).toLinearMap := by - ext x y - simp - generalize Matrix.stdBasis 𝕜 dIn dIn = L - -- Since $L$ is a basis, we can write $y$ as a linear combination of the basis elements. - obtain ⟨c, hc⟩ : ∃ c : dIn × dIn → 𝕜, y = ∑ i, c i • L.toDual (L i) := by - have h_dual_basis : ∀ y : Module.Dual 𝕜 (Matrix dIn dIn 𝕜), ∃ c : dIn × dIn → 𝕜, y = ∑ i, c i • L.toDual (L i) := by - intro y - have h_dual_basis : y ∈ Submodule.span 𝕜 (Set.range (fun i => L.toDual (L i))) := by - have h_dual_basis : Submodule.span 𝕜 (Set.range (fun i => L.toDual (L i))) = ⊤ := by - refine' Submodule.eq_top_of_finrank_eq _; - rw [ finrank_span_eq_card ]; - · simp [ Module.finrank_eq_card_basis L ]; - · convert L.dualBasis.linearIndependent; - exact h_dual_basis.symm ▸ Submodule.mem_top - rw [ Finsupp.mem_span_range_iff_exists_finsupp ] at h_dual_basis; - exact ⟨ h_dual_basis.choose, by simpa [ Finsupp.sum_fintype ] using h_dual_basis.choose_spec.symm ⟩; - exact h_dual_basis y; - subst hc - simp [ map_sum, map_smul ]; - congr! 2; - simp [ Module.Basis.toDualEquiv ]; - simp [ Module.Basis.toDual ] - rw [← Module.Dual.eval_comp_comp_evalEquiv_eq] - rw [← Module.evalEquiv_toLinearMap] - simp only [← LinearMap.comp_assoc, LinearEquiv.comp_coe, LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, - LinearMap.id_comp, h₁] - simp only [LinearMap.comp_assoc, LinearEquiv.comp_coe, LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, - LinearMap.comp_id, h₂] + refine dual_unique (M := M.dual) (M' := M) ?_ + intro A B + calc + (M.dual A * B).trace = (B * M.dual A).trace := by rw [Matrix.trace_mul_comm] + _ = (M B * A).trace := by rw [Dual.trace_eq] + _ = (A * M B).trace := by rw [Matrix.trace_mul_comm] end MatrixMap diff --git a/QuantumInfo/Finite/CPTPMap/Unbundled.lean b/QuantumInfo/Finite/CPTPMap/Unbundled.lean index d5b51d867..b604242d1 100644 --- a/QuantumInfo/Finite/CPTPMap/Unbundled.lean +++ b/QuantumInfo/Finite/CPTPMap/Unbundled.lean @@ -6,6 +6,7 @@ Authors: Alex Meiburg module public import QuantumInfo.Finite.CPTPMap.MatrixMap +public import QuantumInfo.ForMathlib.MatrixNorm.TraceNorm /-! # Properties of Matrix Maps @@ -20,6 +21,8 @@ in Bundled.lean. @[expose] public section +open scoped Matrix MatrixOrder ComplexOrder Matrix.Norms.L2Operator CStarAlgebra + namespace MatrixMap variable {A B C D : Type*} [Fintype A] [Fintype B] [Fintype C] [Fintype D] @@ -727,6 +730,101 @@ theorem IsCompletelyPositive.exists_kraus (Φ : MatrixMap A B R) (hCP : Φ.IsCom rw [eq_iff_iff, iff_comm] exact MatrixMap.choi_matrix_inj.eq_iff +open scoped MatrixOrder in +/-- Kadison-Schwarz for completely positive subunital matrix maps. -/ +theorem cp_subunital_kadison_schwarz {M : MatrixMap A B ℂ} [DecidableEq B] + (hM : M.IsCompletelyPositive) (hM1 : M 1 ≤ (1 : Matrix B B ℂ)) + (X : Matrix A A ℂ) : + (M X)ᴴ * M X ≤ M (Xᴴ * X) := by + have hblock : + (Matrix.fromBlocks (M 1) (M X) ((M X)ᴴ) (M (Xᴴ * X))).PosSemidef := by + classical + obtain ⟨K, rfl⟩ := MatrixMap.IsCompletelyPositive.exists_kraus _ hM + rw [MatrixMap.of_kraus_eq_sum_conj] + convert Matrix.posSemidef_sum Finset.univ (fun k _ => by + simpa [MatrixMap.conj, Matrix.mul_assoc] using + Matrix.fromBlocks_gram_posSemidef (X * (K k)ᴴ) (K k)ᴴ) using 1 + ext i j + cases i <;> cases j <;> + simp [Matrix.sum_apply, Matrix.fromBlocks_apply₁₁, Matrix.fromBlocks_apply₁₂, + Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Matrix.conjTranspose_sum, + Matrix.mul_assoc] + have hgap_block : + (Matrix.fromBlocks (1 - M 1) 0 0 (0 : Matrix B B ℂ)).PosSemidef := by + have hnonneg : (0 : Matrix B B ℂ) ≤ 1 - M 1 := by simpa [sub_nonneg] using hM1 + rw [← show (CFC.sqrt (1 - M 1))ᴴ * CFC.sqrt (1 - M 1) = 1 - M 1 from by + rw [show (CFC.sqrt (1 - M 1))ᴴ = CFC.sqrt (1 - M 1) from by + simpa using (CFC.sqrt_nonneg (1 - M 1)).1.eq] + exact CFC.sqrt_mul_sqrt_self (1 - M 1) hnonneg] + simpa using Matrix.fromBlocks_gram_posSemidef + (0 : Matrix B B ℂ) (CFC.sqrt (1 - M 1)) + have hsum : + (Matrix.fromBlocks (1 : Matrix B B ℂ) (M X) ((M X)ᴴ) (M (Xᴴ * X))).PosSemidef := by + convert hblock.add hgap_block using 1 + ext i j + cases i <;> cases j <;> + simp [Matrix.fromBlocks, sub_eq_add_neg, add_left_comm, add_comm] + letI : Invertible (1 : Matrix B B ℂ) := invertibleOne + simpa [sub_nonneg] using + (Matrix.PosDef.fromBlocks₁₁ (B := M X) (D := M (Xᴴ * X)) + (hA := (Matrix.PosDef.one : (1 : Matrix B B ℂ).PosDef))).mp hsum + +open scoped MatrixOrder in +/-- A positive subunital matrix map is contractive on positive inputs. -/ +theorem positive_subunital_norm_apply_le {M : MatrixMap A B ℂ} [DecidableEq B] + (hM : M.IsPositive) (hM1 : M 1 ≤ (1 : Matrix B B ℂ)) + {X : Matrix A A ℂ} (hX : 0 ≤ X) : + ‖M X‖ ≤ ‖X‖ := by + have hXle : X ≤ ‖X‖ • (1 : Matrix A A ℂ) := by + classical + by_cases h : IsEmpty A + · simp [Subsingleton.elim X 0] + · letI : Nonempty A := not_isEmpty_iff.mp h + letI : Nontrivial (EuclideanSpace ℂ A →L[ℂ] EuclideanSpace ℂ A) := inferInstance + let e := Matrix.toEuclideanCLM (n := A) (𝕜 := ℂ) + have h' := IsSelfAdjoint.le_algebraMap_norm_self (a := e X) + (IsSelfAdjoint.of_nonneg (map_nonneg e hX)) + have hnorm_eq : ‖e X‖ = ‖X‖ := by + simpa [e] using Matrix.l2_opNorm_toEuclideanCLM X + have hs : + (algebraMap ℝ (EuclideanSpace ℂ A →L[ℂ] EuclideanSpace ℂ A)) ‖e X‖ = + e (‖X‖ • (1 : Matrix A A ℂ)) := by + rw [hnorm_eq, Algebra.algebraMap_eq_smul_one] + ext x i + change (((‖X‖ : ℂ) • x).ofLp i) = + (((‖X‖ : ℂ) • (1 : Matrix A A ℂ)) *ᵥ x.ofLp) i + rw [Matrix.smul_mulVec, Matrix.one_mulVec, WithLp.ofLp_smul] + exact (map_le_map_iff e).1 (h'.trans_eq hs) + have hM_bound' : M X ≤ ‖X‖ • (1 : Matrix B B ℂ) := + (show M X ≤ ‖X‖ • (M 1) by + simpa [sub_nonneg, map_sub, map_smul] using + (hM (by + simpa [sub_nonneg] using hXle : + (‖X‖ • (1 : Matrix A A ℂ) - X).PosSemidef)).nonneg).trans + (smul_le_smul_of_nonneg_left hM1 (norm_nonneg X)) + exact (Matrix.norm_le_norm_of_nonneg_of_le + ((hM (by simpa [Matrix.nonneg_iff_posSemidef] using hX)).nonneg) hM_bound').trans (by + rw [show (‖X‖ • (1 : Matrix B B ℂ)) = + ((‖X‖ : ℂ) • (1 : Matrix B B ℂ)) by ext i j; simp, norm_smul] + simpa using mul_le_mul_of_nonneg_left Matrix.norm_one_le_one (norm_nonneg X)) + +open scoped MatrixOrder in +/-- A completely positive subunital matrix map is contractive in operator norm. -/ +theorem cp_subunital_opNorm_le_one {M : MatrixMap A B ℂ} [DecidableEq B] + (hM : M.IsCompletelyPositive) (hM1 : M 1 ≤ (1 : Matrix B B ℂ)) + (X : Matrix A A ℂ) : + ‖M X‖ ≤ ‖X‖ := by + refine (sq_le_sq₀ (norm_nonneg (M X)) (norm_nonneg X)).mp ?_ + rw [show ‖M X‖ ^ 2 = ‖(M X)ᴴ * M X‖ by + simpa only [sq, Matrix.star_eq_conjTranspose] using + (CStarRing.norm_star_mul_self (x := M X)).symm, + show ‖X‖ ^ 2 = ‖Xᴴ * X‖ by + simpa only [sq, Matrix.star_eq_conjTranspose] using + (CStarRing.norm_star_mul_self (x := X)).symm] + exact (Matrix.norm_le_norm_of_nonneg_of_le (star_mul_self_nonneg (M X)) + (cp_subunital_kadison_schwarz hM hM1 X)).trans + (positive_subunital_norm_apply_le hM.IsPositive hM1 (star_mul_self_nonneg X)) + /-- The Kronecker product of two Kraus maps is the Kraus map of the Kronecker products of the operators. -/ diff --git a/QuantumInfo/Finite/Entropy/DPI.lean b/QuantumInfo/Finite/Entropy/DPI.lean index 0f70b6474..273f91724 100644 --- a/QuantumInfo/Finite/Entropy/DPI.lean +++ b/QuantumInfo/Finite/Entropy/DPI.lean @@ -6,7 +6,14 @@ Authors: Alex Meiburg module public import QuantumInfo.Finite.Entropy.Relative +public import QuantumInfo.Finite.CPTPMap.Dual +public import QuantumInfo.ForMathlib.Matrix public import QuantumInfo.ForMathlib.HermitianMat.Sqrt +public import QuantumInfo.ForMathlib.MatrixNorm.TraceNorm +public import Mathlib.Analysis.CStarAlgebra.Matrix +public import Mathlib.Analysis.CStarAlgebra.CStarMatrix +public import Mathlib.Analysis.CStarAlgebra.PositiveLinearMap +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order @[expose] public section @@ -30,55 +37,39 @@ The Data Processing Inequality (DPI) for the sandwiched Rényi relative entropy, as a consequence, the quantum relative entropy. -/ -open scoped Matrix ComplexOrder +open scoped Matrix MatrixOrder ComplexOrder Matrix.Norms.L2Operator CStarAlgebra open BigOperators -/-- The weighted norm \|X\|_{p, σ} defined in the paper. -/ -noncomputable def weighted_norm (p : ℝ) (σ : MState d) (X : Matrix d d ℂ) : ℝ := +/-- The weighted norm `‖X‖_{p,σ}` used internally in the interpolation proof. +This definition is only used below for `p = 1` and `p > 1`; at `p = 0` it is just Lean's +totalized expression, not a mathematical norm. -/ +private noncomputable def weighted_norm (p : ℝ) (σ : MState d) (X : Matrix d d ℂ) : ℝ := let σ_pow : HermitianMat d ℂ := σ.M.cfc (fun x => x ^ (1 / (2 * p))) schattenNorm (σ_pow.mat * X * σ_pow.mat) p -/-- The spectral norm (operator norm) of a matrix. -/ -noncomputable def spectralNorm_mat (A : Matrix d d ℂ) : ℝ := - if h : Finset.univ.Nonempty then - let A_dag_A : HermitianMat d ℂ := ⟨A.conjTranspose * A, by - have h := Matrix.isHermitian_mul_conjTranspose_self A.conjTranspose - rwa [Matrix.conjTranspose_conjTranspose] at h⟩ - Real.sqrt ((Finset.univ.image A_dag_A.H.eigenvalues).max' (Finset.Nonempty.image h _)) - else 0 - /-- The weighted norm for p = \infty. -/ -noncomputable def weighted_norm_infty (_ : MState d) (X : Matrix d d ℂ) : ℝ := - spectralNorm_mat X +private noncomputable def weighted_norm_infty (_ : MState d) (X : Matrix d d ℂ) : ℝ := + ‖X‖ /-- The map Γ_σ(X) = σ^{1/2} X σ^{1/2}. -/ -noncomputable def Gamma (σ : MState d) (X : Matrix d d ℂ) : Matrix d d ℂ := +private noncomputable def Gamma (σ : MState d) (X : Matrix d d ℂ) : Matrix d d ℂ := let σ_half : HermitianMat d ℂ := σ.M.cfc (fun x => x ^ (1/2 : ℝ)) σ_half.mat * X * σ_half.mat -/-- The inverse map Γ_σ^{-1}(X) = σ^{-1/2} X σ^{-1/2}. -/ -noncomputable def Gamma_inv (σ : MState d) (X : Matrix d d ℂ) : Matrix d d ℂ := +/-- The support inverse of `Γ_σ`, given by `σ^{-1/2} X σ^{-1/2}`. +For singular `σ` this is a pseudoinverse: composing with `Gamma σ` compresses to +`σ.M.supportProj`, not to the identity. -/ +private noncomputable def Gamma_inv (σ : MState d) (X : Matrix d d ℂ) : Matrix d d ℂ := let σ_inv_half : HermitianMat d ℂ := σ.M.cfc (fun x => x ^ (-1/2 : ℝ)) σ_inv_half.mat * X * σ_inv_half.mat /-- The operator T = Γ_{Φ(σ)}^{-1} ∘ Φ ∘ Γ_σ. -/ -noncomputable def T_op (Φ : CPTPMap d d₂) (σ : MState d) (X : Matrix d d ℂ) : Matrix d₂ d₂ ℂ := +private noncomputable def T_op (Φ : CPTPMap d d₂) (σ : MState d) + (X : Matrix d d ℂ) : Matrix d₂ d₂ ℂ := Gamma_inv (Φ σ) (Φ.map (Gamma σ X)) -/-- The induced norm of a map Ψ: M_d -> M_d2 with respect to weighted norms. -/ -noncomputable def induced_norm (p : ℝ) (σ : MState d) (Φ : CPTPMap d d₂) (Ψ : Matrix d d ℂ → Matrix d₂ d₂ ℂ) : ℝ := - sSup { weighted_norm p (Φ σ) (Ψ X) / weighted_norm p σ X | (X : Matrix d d ℂ) (_ : weighted_norm p σ X ≠ 0) } - -/- -The induced norm of a map Ψ with respect to the weighted infinity norm. --/ -noncomputable def induced_norm_infty_map (σ : MState d) (Φ : CPTPMap d d₂) (Ψ : Matrix d d ℂ → Matrix d₂ d₂ ℂ) : ℝ := - sSup { weighted_norm_infty (Φ σ) (Ψ X) / weighted_norm_infty σ X | (X : Matrix d d ℂ) (_ : weighted_norm_infty σ X ≠ 0) } - -/- -The operator T = Γ_{Φ(σ)}^{-1} ∘ Φ ∘ Γ_σ as a linear map. --/ -noncomputable def T_map (σ : MState d) (Φ : CPTPMap d d₂) : MatrixMap d d₂ ℂ := +/-- The operator `Γ_{Φ(σ)}^{-1} ∘ Φ ∘ Γ_σ` as a linear map. -/ +private noncomputable def T_map (σ : MState d) (Φ : CPTPMap d d₂) : MatrixMap d d₂ ℂ := { toFun := fun X => T_op Φ σ X, map_add' := fun X Y => by unfold T_op Gamma Gamma_inv @@ -90,159 +81,84 @@ noncomputable def T_map (σ : MState d) (Φ : CPTPMap d d₂) : MatrixMap d d₂ simp [mul_assoc] } -/- -Gamma_map is the conjugation by the square root of sigma. --/ -noncomputable def Gamma_map (σ : MState d) : MatrixMap d d ℂ := +/-- `Gamma` as a matrix map: conjugation by the square root of `σ`. -/ +private noncomputable def Gamma_map (σ : MState d) : MatrixMap d d ℂ := MatrixMap.conj (σ.M.cfc (fun x => x ^ (1/2 : ℝ))).mat -set_option backward.isDefEq.respectTransparency false in -lemma Gamma_map_eq (σ : MState d) (X : Matrix d d ℂ) : - Gamma_map σ X = Gamma σ X := by - ext; simp [ Gamma_map, Gamma ]; - apply_rules [ IsSelfAdjoint.cfc ] - -/- -Gamma_map is completely positive. --/ -lemma Gamma_map_CP (σ : MState d) : (Gamma_map σ).IsCompletelyPositive := by - have := @MatrixMap.conj_isCompletelyPositive; - exact this _ - -/- -Gamma_inv_map is the conjugation by the inverse square root of sigma. --/ -noncomputable def Gamma_inv_map (σ : MState d) : MatrixMap d d ℂ := +/-- `Gamma_inv` as a matrix map: conjugation by the inverse square root on the support. -/ +private noncomputable def Gamma_inv_map (σ : MState d) : MatrixMap d d ℂ := MatrixMap.conj (σ.M.cfc (fun x => x ^ (-1/2 : ℝ))).mat -set_option backward.isDefEq.respectTransparency false in -lemma Gamma_inv_map_eq (σ : MState d) (X : Matrix d d ℂ) : - Gamma_inv_map σ X = Gamma_inv σ X := by - simp [Gamma_inv_map, Gamma_inv]; - congr; - apply IsSelfAdjoint.cfc - -/- -The inverse square root of sigma. --/ -noncomputable def sigma_inv_sqrt (σ : MState d) : Matrix d d ℂ := - (σ.M.cfc (fun x => x ^ (-1/2 : ℝ))).mat - -/- -Gamma_inv_map is conjugation by sigma_inv_sqrt. --/ -lemma Gamma_inv_map_eq_conj (σ : MState d) : - Gamma_inv_map σ = MatrixMap.conj (sigma_inv_sqrt σ) := by - exact rfl - -/- -Gamma_inv_map is completely positive. --/ -lemma Gamma_inv_map_CP (σ : MState d) : (Gamma_inv_map σ).IsCompletelyPositive := by - convert MatrixMap.conj_isCompletelyPositive _; - · infer_instance; - · infer_instance - -/- -T_map is the composition of Gamma_inv_map, Phi, and Gamma_map. --/ -lemma T_map_eq_comp (σ : MState d) (Φ : CPTPMap d d₂) : +/-- `T_map` is the composition of `Gamma_inv_map`, `Φ`, and `Gamma_map`. -/ +private lemma T_map_eq_comp (σ : MState d) (Φ : CPTPMap d d₂) : T_map σ Φ = (Gamma_inv_map (Φ σ)).comp (Φ.map.comp (Gamma_map σ)) := by - ext; - unfold T_map; + ext + unfold T_map simp [T_op] - congr! 1; - · exact funext fun x => Gamma_inv_map_eq ( Φ σ ) x ▸ rfl; - · rw [ Gamma_map_eq ] + congr! 1 + · exact funext fun _ => by + simp [Gamma_inv_map, Gamma_inv] + congr + symm + apply IsSelfAdjoint.cfc + · ext + simp [Gamma_map, Gamma] + all_goals symm + apply_rules [IsSelfAdjoint.cfc] -/- -T_map is completely positive. --/ -lemma T_is_CP (σ : MState d) (Φ : CPTPMap d d₂) : +/-- `T_map` is completely positive. -/ +private lemma T_is_CP (σ : MState d) (Φ : CPTPMap d d₂) : (T_map σ Φ).IsCompletelyPositive := by - rw [ T_map_eq_comp ]; - apply MatrixMap.IsCompletelyPositive.comp; - · apply MatrixMap.IsCompletelyPositive.comp; - · exact Gamma_map_CP σ; - · exact Φ.cp; - · exact Gamma_inv_map_CP (Φ σ) - -/- -T_map is positive. --/ -lemma T_is_positive (σ : MState d) (Φ : CPTPMap d d₂) : - (T_map σ Φ).IsPositive := by - exact T_is_CP σ Φ |> fun h => h.IsPositive + rw [T_map_eq_comp] + exact + ((MatrixMap.conj_isCompletelyPositive _ : (Gamma_map σ).IsCompletelyPositive).comp + Φ.cp).comp (MatrixMap.conj_isCompletelyPositive _) -/- -The weighted 1-norm of X is the trace norm of Gamma(X). --/ -lemma weighted_norm_one_eq_trace_norm_Gamma (σ : MState d) (X : Matrix d d ℂ) : +/-- The weighted `1`-norm of `X` is the trace norm of `Gamma σ X`. -/ +private lemma weighted_norm_one_eq_trace_norm_Gamma (σ : MState d) (X : Matrix d d ℂ) : weighted_norm 1 σ X = schattenNorm (Gamma σ X) 1 := by - unfold weighted_norm Gamma; + unfold weighted_norm Gamma norm_num -/- -The induced norm of a super-operator between weighted Schatten spaces. --/ -noncomputable def general_induced_norm - (p q : ℝ) (σ : MState d) (σ' : MState d₂) - (Ψ : MatrixMap d d₂ ℂ) : ℝ := - sSup { weighted_norm q σ' (Ψ X) / weighted_norm p σ X | (X : Matrix d d ℂ) (_ : weighted_norm p σ X ≠ 0) } - -/- -Multiplication property for HermitianMat functional calculus. --/ -lemma HermitianMat.cfc_mul {d : Type*} [Fintype d] [DecidableEq d] - (A : HermitianMat d ℂ) (f g : ℝ → ℝ) : - (A.cfc f).mat * (A.cfc g).mat = (A.cfc (fun x => f x * g x)).mat := by - symm - apply mat_cfc_mul - -/- -Gamma of identity is sigma. --/ -set_option backward.isDefEq.respectTransparency false in -lemma Gamma_one (σ : MState d) : Gamma σ 1 = σ.M.mat := by +/-- `Gamma` sends the identity to `σ`. -/ +private lemma Gamma_one (σ : MState d) : Gamma σ 1 = σ.M.mat := by have h_gamma_one : (σ.M.cfc (fun x => x^(1/2 : ℝ))).mat * (σ.M.cfc (fun x => x^(1/2 : ℝ))).mat = σ.M.cfc (fun x => x^(1/2 : ℝ) * x^(1/2 : ℝ)) := by symm exact HermitianMat.mat_cfc_mul σ.M ( fun x => x ^ ( 1 / 2 : ℝ ) ) ( fun x => x ^ ( 1 / 2 : ℝ ) ) - convert h_gamma_one using 1; - · unfold Gamma; aesop; - · norm_num [ ← Real.sqrt_eq_rpow, Real.sqrt_mul_self ( show 0 ≤ _ from _ ) ]; + convert h_gamma_one using 1 + · unfold Gamma; aesop + · norm_num [ ← Real.sqrt_eq_rpow, Real.sqrt_mul_self ( show 0 ≤ _ from _ ) ] have h_gamma_one : ∀ x ∈ spectrum ℝ σ.m, Real.sqrt x * Real.sqrt x = x := by intro x hx; rw [ Real.mul_self_sqrt ] ; exact (by - rw [ spectrum.mem_iff ] at hx; - exact Matrix.PosSemidef.pos_of_mem_spectrum σ.psd x hx); - rw [ cfc ]; + rw [ spectrum.mem_iff ] at hx + exact Matrix.PosSemidef.pos_of_mem_spectrum σ.psd x hx) + rw [ cfc ] split_ifs <;> simp_all - · convert rfl; - convert cfcHom_id _; - ext x; aesop; + · convert rfl + convert cfcHom_id _ + ext x; aesop · exact False.elim ( ‹IsSelfAdjoint σ.m → ¬ContinuousOn ( fun x => Real.sqrt x * Real.sqrt x ) ( spectrum ℝ σ.m ) › σ.M.prop <| ContinuousOn.mul ( Real.continuous_sqrt.continuousOn ) ( Real.continuous_sqrt.continuousOn ) ) -/- -Gamma inverse of sigma is identity. --/ -lemma Gamma_inv_self (σ : MState d) (hσ : σ.m.PosDef) : +/-- For full-support `σ`, the support inverse sends `σ` to the identity. -/ +private lemma Gamma_inv_self (σ : MState d) (hσ : σ.m.PosDef) : Gamma_inv σ σ.M.mat = 1 := by - -- We use `HermitianMat.cfc_mul` and the fact that $x^{-1/2} * x * x^{-1/2} = 1$ for $x > 0$. + -- We use functional calculus and the fact that $x^{-1/2} * x * x^{-1/2} = 1$ for $x > 0$. have h_gamma_inv_sigma : (σ.M.cfc (fun x => x ^ (-1/2 : ℝ))).mat * (σ.M.mat) * (σ.M.cfc (fun x => x ^ (-1/2 : ℝ))).mat = (σ.M.cfc (fun x => x ^ (-1/2 : ℝ) * x * x ^ (-1/2 : ℝ))).mat := by have h_gamma_inv_sigma : (σ.M.cfc (fun x => x ^ (-1/2 : ℝ))).mat * (σ.M.cfc id).mat * (σ.M.cfc (fun x => x ^ (-1/2 : ℝ))).mat = (σ.M.cfc (fun x => x ^ (-1/2 : ℝ) * x * x ^ (-1/2 : ℝ))).mat := by have h_gamma_inv_sigma : ∀ (f g h : ℝ → ℝ), ContinuousOn f (spectrum ℝ σ.M.mat) → ContinuousOn g (spectrum ℝ σ.M.mat) → ContinuousOn h (spectrum ℝ σ.M.mat) → (σ.M.cfc f).mat * (σ.M.cfc g).mat * (σ.M.cfc h).mat = (σ.M.cfc (fun x => f x * g x * h x)).mat := by intro f g h hf hg hh have h_gamma_inv_sigma : (σ.M.cfc f).mat * (σ.M.cfc g).mat = (σ.M.cfc (fun x => f x * g x)).mat := by symm - convert HermitianMat.mat_cfc_mul σ.M f g using 1; - rw [ h_gamma_inv_sigma, ← HermitianMat.mat_cfc_mul ]; + convert HermitianMat.mat_cfc_mul σ.M f g using 1 + rw [ h_gamma_inv_sigma, ← HermitianMat.mat_cfc_mul ] congr! 2 have h : ∀ x ∈ spectrum ℝ σ.M.mat, x ≠ 0 := by norm_num intro x hx h_zero have h_eigenvalue : ∃ v : d → ℂ, v ≠ 0 ∧ σ.m.mulVec v = x • v := by simp_all [ spectrum.mem_iff] - contrapose! hx; - exact Matrix.PosDef.isUnit hσ; + contrapose! hx + exact Matrix.PosDef.isUnit hσ obtain ⟨ v, hv_ne_zero, hv_eigenvalue ⟩ := h_eigenvalue rw [Matrix.posDef_iff_dotProduct_mulVec] at hσ have := hσ.2 hv_ne_zero @@ -251,190 +167,1312 @@ lemma Gamma_inv_self (σ : MState d) (hσ : σ.m.PosDef) : · fun_prop · fun_prop · fun_prop - convert h_gamma_inv_sigma using 1; + convert h_gamma_inv_sigma using 1 ext i j ; simp [ Matrix.mul_apply] -- Since $x^{-1/2} * x * x^{-1/2} = 1$ for $x > 0$, we have $(σ.M.cfc (fun x => x ^ (-1/2 : ℝ))).mat * (σ.M.mat) * (σ.M.cfc (fun x => x ^ (-1/2 : ℝ))).mat = (σ.M.cfc (fun x => 1)).mat$. have h_gamma_inv_sigma_simplified : (σ.M.cfc (fun x => x ^ (-1/2 : ℝ))).mat * (σ.M.mat) * (σ.M.cfc (fun x => x ^ (-1/2 : ℝ))).mat = (σ.M.cfc (fun x => 1)).mat := by - convert h_gamma_inv_sigma using 1; - congr! 1; + convert h_gamma_inv_sigma using 1 + congr! 1 -- Since $x^{-1/2} * x * x^{-1/2} = 1$ for all $x > 0$, the functions are equal. have h_eq : ∀ x : ℝ, 0 < x → x ^ (-1 / 2 : ℝ) * x * x ^ (-1 / 2 : ℝ) = 1 := by intro x hx ring_nf - norm_num [ hx.ne' ]; - rw [ ← Real.rpow_natCast, ← Real.rpow_mul hx.le ] ; norm_num [ hx.ne' ]; - rw [ Real.rpow_neg_one, inv_mul_cancel₀ hx.ne' ]; - exact Eq.symm (HermitianMat.cfc_congr_of_posDef hσ h_eq); - convert h_gamma_inv_sigma_simplified using 1; + norm_num [ hx.ne' ] + rw [ ← Real.rpow_natCast, ← Real.rpow_mul hx.le ] ; norm_num [ hx.ne' ] + rw [ Real.rpow_neg_one, inv_mul_cancel₀ hx.ne' ] + exact Eq.symm (HermitianMat.cfc_congr_of_posDef hσ h_eq) + convert h_gamma_inv_sigma_simplified using 1 ext i j simp -/- -The matrix of the output state is the map applied to the input matrix. --/ -lemma CPTPMap_apply_MState_M (Φ : CPTPMap d d₂) (σ : MState d) : - (Φ σ).M.mat = Φ.map σ.M.mat := by - exact rfl - -/- -The map T is unital. --/ -theorem T_map_unital (σ : MState d) (Φ : CPTPMap d d₂) (hΦσ : (Φ σ).m.PosDef) : - (T_map σ Φ) 1 = 1 := by - dsimp [T_map, T_op] - rw [Gamma_one σ] - rw [← CPTPMap_apply_MState_M] - rw [Gamma_inv_self (Φ σ) hΦσ] - -/- -The map T is completely positive. --/ -theorem T_map_is_CP_proof (σ : MState d) (Φ : CPTPMap d d₂) : - (T_map σ Φ).IsCompletelyPositive := by - apply T_is_CP +private lemma Gamma_inv_self_supportProj (σ : MState d) : + Gamma_inv σ σ.M.mat = σ.M.supportProj.mat := by + change ((σ.M.cfc (fun x => x ^ (-1 / 2 : ℝ))).mat * σ.M.mat * + (σ.M.cfc (fun x => x ^ (-1 / 2 : ℝ))).mat) = σ.M.supportProj.mat + rw [show σ.M.mat = (σ.M.cfc id).mat from by simp, + ← HermitianMat.mat_cfc_mul σ.M (fun x => x ^ (-1 / 2 : ℝ)) id, + show (σ.M.cfc ((fun x => x ^ (-1 / 2 : ℝ)) * id)).mat + = (σ.M.cfc (fun x => x ^ (-1 / 2 : ℝ) * x)).mat from rfl, + ← HermitianMat.mat_cfc_mul σ.M _ (fun x => x ^ (-1 / 2 : ℝ)), + HermitianMat.supportProj_eq_cfc] + refine congrArg _ <| HermitianMat.cfc_congr_of_nonneg σ.nonneg fun x hx => ?_ + by_cases hx0 : x = 0 + · simp [hx0] + · have hxpos : 0 < x := hx.lt_of_ne (Ne.symm hx0) + show x ^ (-1 / 2 : ℝ) * x * x ^ (-1 / 2 : ℝ) = if x = 0 then 0 else 1 + simp only [hx0, if_false] + nth_rw 2 [← Real.rpow_one x] + rw [← Real.rpow_add hxpos, ← Real.rpow_add hxpos] + norm_num -/- -Gamma composed with Gamma inverse is identity. --/ -set_option backward.isDefEq.respectTransparency false in -lemma Gamma_Gamma_inv (σ : MState d) (hσ : σ.m.PosDef) (X : Matrix d d ℂ) : +/-- For full-support `σ`, `Gamma σ` composed with `Gamma_inv σ` is the identity. -/ +private lemma Gamma_Gamma_inv (σ : MState d) (hσ : σ.m.PosDef) (X : Matrix d d ℂ) : Gamma σ (Gamma_inv σ X) = X := by -- By definition of Gamma and Gamma_inv, we can simplify the expression. have h_simp : (σ.M.cfc (fun x => x ^ (1 / 2 : ℝ))).mat * (σ.M.cfc (fun x => x ^ (-1 / 2 : ℝ))).mat = 1 := by symm - convert HermitianMat.mat_cfc_mul _ _ _ using 1; + convert HermitianMat.mat_cfc_mul _ _ _ using 1 · have h_gamma_gamma_inv : ∀ x ∈ spectrum ℝ σ.M.mat, x ^ (1 / 2 : ℝ) * x ^ (-1 / 2 : ℝ) = 1 := by intro x hx have hx_pos : 0 < x := by - have := (Matrix.posDef_iff_dotProduct_mulVec.mp hσ).2; + have := (Matrix.posDef_iff_dotProduct_mulVec.mp hσ).2 obtain ⟨v, hv⟩ : ∃ v : d → ℂ, v ≠ 0 ∧ σ.m.mulVec v = x • v := by - rw [ spectrum.mem_iff ] at hx; - simp_all [ Matrix.isUnit_iff_isUnit_det ]; - obtain ⟨ v, hv ⟩ := Matrix.exists_mulVec_eq_zero_iff.mpr hx; - simp_all [ sub_eq_iff_eq_add, Matrix.sub_mulVec ]; - exact ⟨ v, hv.1, hv.2.symm.trans ( by ext i; erw [ Matrix.mulVec_diagonal ] ; aesop ) ⟩; - specialize this hv.1; - simp_all [ dotProduct]; - simp_all [ mul_assoc, mul_comm]; - simp_all [ mul_left_comm ( v _ ), Complex.mul_conj, Complex.normSq_eq_norm_sq ]; - norm_cast at this; - exact lt_of_not_ge fun hx' => this.not_ge <| Finset.sum_nonpos fun i _ => mul_nonpos_of_nonpos_of_nonneg hx' <| sq_nonneg _; - rw [ ← Real.rpow_add hx_pos ] ; norm_num; + rw [ spectrum.mem_iff ] at hx + simp_all [ Matrix.isUnit_iff_isUnit_det ] + obtain ⟨ v, hv ⟩ := Matrix.exists_mulVec_eq_zero_iff.mpr hx + simp_all [ sub_eq_iff_eq_add, Matrix.sub_mulVec ] + exact ⟨ v, hv.1, hv.2.symm.trans ( by ext i; erw [ Matrix.mulVec_diagonal ] ; aesop ) ⟩ + specialize this hv.1 + simp_all [ dotProduct] + simp_all [ mul_assoc, mul_comm] + simp_all [ mul_left_comm ( v _ ), Complex.mul_conj, Complex.normSq_eq_norm_sq ] + norm_cast at this + exact lt_of_not_ge fun hx' => this.not_ge <| Finset.sum_nonpos fun i _ => mul_nonpos_of_nonpos_of_nonneg hx' <| sq_nonneg _ + rw [ ← Real.rpow_add hx_pos ] ; norm_num rw [HermitianMat.cfc_congr (g := fun x ↦ 1)] · rw [ HermitianMat.cfc_const ] norm_num - · exact fun x hx => h_gamma_gamma_inv x hx; - unfold Gamma Gamma_inv; simp_all [ ← mul_assoc ] ; + · exact fun x hx => h_gamma_gamma_inv x hx + unfold Gamma Gamma_inv; simp_all [ ← mul_assoc ] simp_all [ mul_assoc, mul_eq_one_comm.mp h_simp ] -/- -If a Hermitian matrix is bounded by M*I, then all its eigenvalues are at most M. --/ -set_option backward.isDefEq.respectTransparency false in -theorem HermitianMat.le_smul_one_imp_eigenvalues_le (A : HermitianMat d ℂ) (M : ℝ) - (h : A ≤ M • (1 : HermitianMat d ℂ)) (i : d) : - A.H.eigenvalues i ≤ M := by - -- By definition of eigenvalues, for any unit vector $v$, we have $\langle v, A v \rangle \leq M$. - have h_eigenvalue_le_M_step : ∀ (v : EuclideanSpace ℂ d), ‖v‖ = 1 → ⟪v, .toLp 2 <| A.mat.mulVec v⟫_ℂ ≤ M := by - intro v hv - have h_inner : ⟪v, .toLp 2 <| A.mat.mulVec v⟫_ℂ ≤ ⟪v, .toLp 2 <| (M • 1 : Matrix d d ℂ).mulVec v⟫_ℂ := by - have h_inner : ⟪v, .toLp 2 <| ((M • 1 : Matrix d d ℂ) - A.mat).mulVec v⟫_ℂ ≥ 0 := by - have h_inner_le_M : ∀ (X : HermitianMat d ℂ), X ≥ 0 → ∀ (v : EuclideanSpace ℂ d), ⟪v, .toLp 2 <| X.mat.mulVec v⟫_ℂ ≥ 0 := by - intro X hX v - rw [ge_iff_le, HermitianMat.zero_le_iff, Matrix.posSemidef_iff_dotProduct_mulVec] at hX - have := hX.2 v - simp [ Matrix.mulVec, dotProduct ] at * - convert this using 1; - refine Finset.sum_congr rfl fun _ _ => ?_ - sorry - convert h_inner_le_M ⟨ _, _ ⟩ _ v; - all_goals norm_num [ HermitianMat.le_iff ] at *; - · convert h.1; - · exact h; - simp_all [ Matrix.sub_mulVec] - simp_all [ EuclideanSpace.norm_eq ]; - convert h_inner using 1; - simp [ Matrix.mulVec, dotProduct, inner ]; - simp [ Matrix.one_apply,mul_assoc]; - simp [ ← Finset.mul_sum]; - simp [ Complex.mul_conj, Complex.normSq_eq_norm_sq ]; - norm_cast ; aesop; - have := A.H.eigenvectorBasis.orthonormal; - have := this.1 i; - have := h_eigenvalue_le_M_step ( A.H.eigenvectorBasis i ) this; - rw [ show A.mat.mulVec _ = ( Matrix.IsHermitian.eigenvalues A.H i : ℂ ) • ( Matrix.IsHermitian.eigenvectorBasis A.H i ) from ?_ ] at this; - · simp_all - · convert A.H.mulVec_eigenvectorBasis i using 1 - -set_option maxHeartbeats 400000 in -open MatrixOrder in -/- -If all eigenvalues of a Hermitian matrix are at most M, then the matrix is bounded by M*I. --/ -theorem HermitianMat.eigenvalues_le_imp_le_smul_one (A : HermitianMat d ℂ) (M : ℝ) - (h : ∀ i, A.H.eigenvalues i ≤ M) : - A ≤ M • (1 : HermitianMat d ℂ) := by - have := A.H.spectral_theorem.symm; - -- Since $A$ is Hermitian, we can write it as $A = UDU^*$ where $U$ is unitary and $D$ is diagonal with eigenvalues $\lambda_i$. - have h_decomp : ∃ U : Matrix d d ℂ, U * star U = 1 ∧ ∃ D : HermitianMat d ℂ, A = U * D * star U ∧ ∀ i, D i i ≤ M := by - use A.H.eigenvectorUnitary - constructor; · simp - use HermitianMat.diagonal ℂ A.H.eigenvalues +private lemma Gamma_Gamma_inv_supportProj (σ : MState d) (X : Matrix d d ℂ) : + Gamma σ (Gamma_inv σ X) = σ.M.supportProj.mat * X * σ.M.supportProj.mat := by + have key (p : ℝ) (hp : p ≠ 0) : + (σ.M.cfc (fun x => x ^ p)).mat * (σ.M.cfc (fun x => x ^ (-p))).mat = σ.M.supportProj.mat ∧ + (σ.M.cfc (fun x => x ^ (-p))).mat * (σ.M.cfc (fun x => x ^ p)).mat = σ.M.supportProj.mat := by + refine ⟨?_, ?_⟩ + · simpa [HermitianMat.rpow_eq_cfc] using + HermitianMat.rpow_neg_mul_rpow_eq_supportProj (A := σ.M) σ.nonneg + (p := -p) (neg_ne_zero.mpr hp) + · simpa [HermitianMat.rpow_eq_cfc] using + HermitianMat.rpow_neg_mul_rpow_eq_supportProj (A := σ.M) σ.nonneg (p := p) hp + have hneg_half : + (σ.M.cfc (fun x => x ^ (-1 / 2 : ℝ))).mat = + (σ.M.cfc (fun x => x ^ (-(1 / 2 : ℝ)))).mat := by congr 1; ext x; norm_num + obtain ⟨h1, h2⟩ := key (1 / 2 : ℝ) (by norm_num) + unfold Gamma Gamma_inv + calc _ = ((σ.M.cfc (fun x => x ^ (1 / 2 : ℝ))).mat * + (σ.M.cfc (fun x => x ^ (-1 / 2 : ℝ))).mat) * X * + ((σ.M.cfc (fun x => x ^ (-1 / 2 : ℝ))).mat * + (σ.M.cfc (fun x => x ^ (1 / 2 : ℝ))).mat) := by simp [Matrix.mul_assoc] + _ = _ := by rw [hneg_half, h1, h2] + +private def spectralProj (A : HermitianMat d ℂ) (i : d) : Matrix d d ℂ := + A.H.eigenvectorUnitary.val * (Matrix.single i i 1) * A.H.eigenvectorUnitary.val.conjTranspose + +private def supportCpow (A : HermitianMat d ℂ) (z : ℂ) : Matrix d d ℂ := + ∑ i, (if A.H.eigenvalues i = 0 then 0 else ((A.H.eigenvalues i : ℂ) ^ z)) • spectralProj A i + +private lemma spectralProj_mul (A : HermitianMat d ℂ) (i j : d) : + spectralProj A i * spectralProj A j = if i = j then spectralProj A i else 0 := by + classical + have hU : A.H.eigenvectorUnitary.val.conjTranspose * A.H.eigenvectorUnitary.val = + (1 : Matrix d d ℂ) := by simp [Matrix.IsHermitian.eigenvectorUnitary] + unfold spectralProj + have heq : A.H.eigenvectorUnitary.val * Matrix.single i i (1 : ℂ) * + A.H.eigenvectorUnitary.val.conjTranspose * + (A.H.eigenvectorUnitary.val * Matrix.single j j (1 : ℂ) * + A.H.eigenvectorUnitary.val.conjTranspose) = + A.H.eigenvectorUnitary.val * + (Matrix.single i i (1 : ℂ) * Matrix.single j j 1) * + A.H.eigenvectorUnitary.val.conjTranspose := by + rw [show A.H.eigenvectorUnitary.val * Matrix.single i i (1 : ℂ) * + A.H.eigenvectorUnitary.val.conjTranspose * + (A.H.eigenvectorUnitary.val * Matrix.single j j (1 : ℂ) * + A.H.eigenvectorUnitary.val.conjTranspose) = + A.H.eigenvectorUnitary.val * Matrix.single i i 1 * + (A.H.eigenvectorUnitary.val.conjTranspose * A.H.eigenvectorUnitary.val) * + Matrix.single j j 1 * A.H.eigenvectorUnitary.val.conjTranspose + from by simp [Matrix.mul_assoc], hU, Matrix.mul_one] + simp [Matrix.mul_assoc] + rw [heq] + by_cases hij : i = j + · subst j; simp [Matrix.single_mul_single_same] + · simp [hij] + +private lemma supportCpow_zero (A : HermitianMat d ℂ) : + supportCpow A 0 = A.supportProj.mat := by + rw [A.supportProj_eq_cfc, HermitianMat.cfc_toMat_eq_sum_smul_proj] + simp [supportCpow, spectralProj] + +private lemma supportCpow_ofReal + (A : HermitianMat d ℂ) (hA : 0 ≤ A) {r : ℝ} (hr : 0 < r) : + supportCpow A (r : ℂ) = (A ^ r).mat := by + rw [HermitianMat.rpow_eq_cfc, HermitianMat.cfc_toMat_eq_sum_smul_proj] + refine Finset.sum_congr rfl fun i _ => ?_ + by_cases h0 : A.H.eigenvalues i = 0 + · simp [spectralProj, h0, hr.ne'] + · simp [spectralProj, h0] + rw [← Complex.ofReal_cpow ((HermitianMat.zero_le_iff.mp hA).eigenvalues_nonneg i) r] + rfl + +private lemma supportCpow_ofReal_ne_zero (A : HermitianMat d ℂ) (hA : 0 ≤ A) {r : ℝ} + (hr : r ≠ 0) : + supportCpow A (r : ℂ) = (A ^ r).mat := by + rw [HermitianMat.rpow_eq_cfc, HermitianMat.cfc_toMat_eq_sum_smul_proj] + refine Finset.sum_congr rfl fun i _ => ?_ + by_cases h0 : A.H.eigenvalues i = 0 + · simp [h0, spectralProj, Real.zero_rpow hr] + · simp [h0, spectralProj] + rw [← Complex.ofReal_cpow ((HermitianMat.zero_le_iff.mp hA).eigenvalues_nonneg i) r] + rfl + +private lemma supportCpow_mul (A : HermitianMat d ℂ) (z w : ℂ) : + supportCpow A z * supportCpow A w = supportCpow A (z + w) := by + unfold supportCpow + simp_rw [Finset.sum_mul, Finset.mul_sum] + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun i _ => ?_ + rw [Finset.sum_eq_single i] + · by_cases h0 : A.H.eigenvalues i = 0 + · simp [h0] + · simp [h0, spectralProj_mul, smul_smul, add_comm, + ← Complex.cpow_add _ _ (by exact_mod_cast h0 : (A.H.eigenvalues i : ℂ) ≠ 0)] + · intro j _ hij + simp [spectralProj_mul, hij] + · simp + +private lemma Gamma_supportCpow_shift + (σ : MState d) (a : ℂ) (X : Matrix d d ℂ) : + Gamma σ (supportCpow σ.M a * X * supportCpow σ.M a) = + supportCpow σ.M (((1 / 2 : ℝ) : ℂ) + a) * X * + supportCpow σ.M (((1 / 2 : ℝ) : ℂ) + a) := by + calc + Gamma σ (supportCpow σ.M a * X * supportCpow σ.M a) + = supportCpow σ.M (((1 / 2 : ℝ) : ℂ)) * + (supportCpow σ.M a * X * supportCpow σ.M a) * + supportCpow σ.M (((1 / 2 : ℝ) : ℂ)) := by + rw [supportCpow_ofReal σ.M σ.nonneg (r := 1 / 2) (by positivity)] + simp [Gamma, HermitianMat.rpow_eq_cfc] + _ = (supportCpow σ.M (((1 / 2 : ℝ) : ℂ)) * supportCpow σ.M a) * X * + (supportCpow σ.M a * supportCpow σ.M (((1 / 2 : ℝ) : ℂ))) := by + simp [Matrix.mul_assoc] + _ = supportCpow σ.M ((((1 / 2 : ℝ) : ℂ) + a)) * X * + supportCpow σ.M (a + (((1 / 2 : ℝ) : ℂ))) := by + rw [supportCpow_mul, supportCpow_mul] + _ = supportCpow σ.M ((((1 / 2 : ℝ) : ℂ) + a)) * X * + supportCpow σ.M ((((1 / 2 : ℝ) : ℂ) + a)) := by + rw [add_comm a (((1 / 2 : ℝ) : ℂ))] + +private lemma supportCpow_conjTranspose (A : HermitianMat d ℂ) (hA : 0 ≤ A) (z : ℂ) : + (supportCpow A z)ᴴ = supportCpow A (star z) := by + classical + unfold supportCpow + rw [Matrix.conjTranspose_sum] + refine Finset.sum_congr rfl ?_ + intro i hi + by_cases h0 : A.H.eigenvalues i = 0 + · simp [h0] + · have hpos : 0 < A.H.eigenvalues i := by + exact lt_of_le_of_ne (HermitianMat.eigenvalues_nonneg hA i) (Ne.symm h0) + have hcpow : + star (((A.H.eigenvalues i : ℂ) ^ z)) = ((A.H.eigenvalues i : ℂ) ^ (star z)) := by + simpa [Complex.conj_ofReal] using + (Complex.cpow_conj (x := (A.H.eigenvalues i : ℂ)) (n := z) + (by + simpa [Complex.arg_ofReal_of_nonneg hpos.le] using + (show (0 : ℝ) ≠ Real.pi by positivity))).symm + rw [Matrix.conjTranspose_smul, show (spectralProj A i)ᴴ = spectralProj A i from by + unfold spectralProj; simp [Matrix.mul_assoc]] + simp [h0, hcpow] + +private lemma supportCpow_diffContOnCl_strip (A : HermitianMat d ℂ) (l u : ℝ) : + DiffContOnCl ℂ (fun z : ℂ => supportCpow A z) + (Complex.HadamardThreeLines.verticalStrip l u) := by + classical + unfold supportCpow + refine Finset.induction_on Finset.univ ?_ ?_ + · simpa using (diffContOnCl_const : DiffContOnCl ℂ (fun _ : ℂ => (0 : Matrix d d ℂ)) + (Complex.HadamardThreeLines.verticalStrip l u)) + · intro a s ha hs + simp only [Finset.sum_insert ha] + by_cases h0 : A.H.eigenvalues a = 0 + · simpa [h0] using hs + · have hterm : + DiffContOnCl ℂ + (fun z : ℂ => + ((A.H.eigenvalues a : ℂ) ^ z) • spectralProj A a) + (Complex.HadamardThreeLines.verticalStrip l u) := by + simpa [h0] using + (((differentiable_id.const_cpow (Or.inl (by exact_mod_cast h0))).diffContOnCl).smul_const + (spectralProj A a)) + simpa [h0] using hterm.add hs + +private lemma supportProj_le_one (A : HermitianMat d ℂ) : + A.supportProj ≤ (1 : HermitianMat d ℂ) := by + rw [show (1 : HermitianMat d ℂ) = A.supportProj + A.kerProj by simp [add_comm]] + exact le_add_of_nonneg_right (a := A.supportProj) (by + simpa [HermitianMat.kerProj] using HermitianMat.projector_nonneg A.ker) + +private lemma traceNorm_le_of_dual_opNorm_le + {M : MatrixMap d d₂ ℂ} + (hdual : ∀ Z : Matrix d₂ d₂ ℂ, ‖M.dual Z‖ ≤ ‖Z‖) + (Y : Matrix d d ℂ) : + (M Y).traceNorm ≤ Y.traceNorm := by + obtain ⟨U, hU⟩ := (Matrix.traceNorm_eq_max_re_tr_U (M Y)).left + calc + (M Y).traceNorm = Complex.re ((U.val * M Y).trace) := by + simpa using hU.symm + _ = Complex.re ((M.dual U.val * Y).trace) := by + rw [Matrix.trace_mul_comm, MatrixMap.Dual.trace_eq, Matrix.trace_mul_comm] + _ ≤ ‖(M.dual U.val * Y).trace‖ := Complex.re_le_norm _ + _ ≤ (M.dual U.val * Y).traceNorm := Matrix.abs_trace_le_traceNorm _ + _ ≤ ‖M.dual U.val‖ * Y.traceNorm := Matrix.traceNorm_mul_le_opNorm_traceNorm _ _ + _ ≤ ‖U.val‖ * Y.traceNorm := + mul_le_mul_of_nonneg_right (hdual U.val) (Matrix.traceNorm_nonneg Y) + _ ≤ 1 * Y.traceNorm := by + refine mul_le_mul_of_nonneg_right ?_ (Matrix.traceNorm_nonneg Y) + by_cases h : IsEmpty d₂ + · have hU0 : U.val = 0 := Subsingleton.elim _ _ + simpa only [hU0, norm_zero] using (zero_le_one : (0 : ℝ) ≤ 1) + · letI : Nonempty d₂ := not_isEmpty_iff.mp h + have hU : U.valᴴ * U.val = (1 : Matrix d₂ d₂ ℂ) := by + ext i j + by_cases hij : i = j + · simpa [Matrix.one_apply, Matrix.star_eq_conjTranspose, hij] using + congrFun (congrFun U.prop.1 i) j + · simpa [Matrix.one_apply, Matrix.star_eq_conjTranspose, hij] using + congrFun (congrFun U.prop.1 i) j + have hU_sq : ‖U.val‖ * ‖U.val‖ = 1 := by + rw [← CStarRing.norm_star_mul_self (x := U.val), Matrix.star_eq_conjTranspose, hU] + simp + nlinarith [norm_nonneg U.val] + _ = Y.traceNorm := by simp + +private lemma norm_supportCpow_im_le_one (A : HermitianMat d₂ ℂ) (hA : 0 ≤ A) (t : ℝ) : + ‖supportCpow A (Complex.I * t)‖ ≤ 1 := by + let C := supportCpow A (Complex.I * t) + have hsq : ‖C‖ * ‖C‖ = ‖A.supportProj.mat‖ := by + rw [← CStarRing.norm_star_mul_self (x := C)] + simp [C, Matrix.star_eq_conjTranspose, supportCpow_conjTranspose _ hA, supportCpow_mul, + supportCpow_zero] + have hproj : ‖A.supportProj.mat‖ ≤ 1 := + (Matrix.norm_le_norm_of_nonneg_of_le + (by + simpa [HermitianMat.supportProj] using + (HermitianMat.projector_nonneg (S := A.support)).nonneg) + (by simpa using supportProj_le_one A)).trans Matrix.norm_one_le_one + nlinarith [norm_nonneg C] + +private lemma norm_supportCpow_mem_verticalClosedStrip_le_one + (σ : MState d) {z : ℂ} + (hz : z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1) : + ‖supportCpow σ.M z‖ ≤ 1 := by + have hz' : 0 ≤ z.re ∧ z.re ≤ 1 := by + simpa [Complex.HadamardThreeLines.verticalClosedStrip] using hz + rw [show z = (z.re : ℂ) + Complex.I * z.im by apply Complex.ext <;> simp, + ← supportCpow_mul] + calc + ‖supportCpow σ.M (z.re : ℂ) * supportCpow σ.M (Complex.I * z.im)‖ + ≤ ‖supportCpow σ.M (z.re : ℂ)‖ * ‖supportCpow σ.M (Complex.I * z.im)‖ := + norm_mul_le _ _ + _ ≤ ‖supportCpow σ.M (z.re : ℂ)‖ * 1 := + mul_le_mul_of_nonneg_left (norm_supportCpow_im_le_one σ.M σ.nonneg z.im) + (norm_nonneg _) + _ = ‖supportCpow σ.M (z.re : ℂ)‖ := by simp + _ ≤ 1 := by + by_cases hr0 : z.re = 0 + · simpa [hr0, supportCpow_zero] using + (Matrix.norm_le_norm_of_nonneg_of_le + (by + simpa [HermitianMat.supportProj] using + (HermitianMat.projector_nonneg (S := σ.M.support)).nonneg) + (by simpa using supportProj_le_one σ.M)).trans Matrix.norm_one_le_one + · have hr : 0 < z.re := lt_of_le_of_ne hz'.1 (Ne.symm hr0) + rw [supportCpow_ofReal σ.M σ.nonneg hr] + exact (Matrix.norm_le_norm_of_nonneg_of_le + (HermitianMat.zero_le_iff.mp (HermitianMat.rpow_nonneg σ.nonneg)).nonneg + (MState.rpow_le_one' (σ := σ) hr)).trans Matrix.norm_one_le_one + +private lemma exists_norm_supportCpow_le_on_verticalClosedStrip + (A : HermitianMat d ℂ) (hA : 0 ≤ A) (l u : ℝ) : + ∃ K : ℝ, ∀ z ∈ Complex.HadamardThreeLines.verticalClosedStrip l u, + ‖supportCpow A z‖ ≤ K := by + classical + let K : ℝ := ∑ i, + max + (if h0 : A.H.eigenvalues i = 0 then 0 else A.H.eigenvalues i ^ l) + (if h0 : A.H.eigenvalues i = 0 then 0 else A.H.eigenvalues i ^ u) * + ‖spectralProj A i‖ + refine ⟨K, ?_⟩ + intro z hz + have hz' : l ≤ z.re ∧ z.re ≤ u := by + simpa [Complex.HadamardThreeLines.verticalClosedStrip] using hz + rw [show z = (z.re : ℂ) + Complex.I * z.im by apply Complex.ext <;> simp, + ← supportCpow_mul] + calc + ‖supportCpow A (z.re : ℂ) * supportCpow A (Complex.I * z.im)‖ + ≤ ‖supportCpow A (z.re : ℂ)‖ * ‖supportCpow A (Complex.I * z.im)‖ := + norm_mul_le _ _ + _ ≤ ‖supportCpow A (z.re : ℂ)‖ * 1 := + mul_le_mul_of_nonneg_left (norm_supportCpow_im_le_one A hA z.im) (norm_nonneg _) + _ = ‖supportCpow A (z.re : ℂ)‖ := by simp + _ ≤ ∑ i, + ‖(if A.H.eigenvalues i = 0 then 0 else ((A.H.eigenvalues i : ℂ) ^ (z.re : ℂ))) • + spectralProj A i‖ := by + simpa [supportCpow] using norm_sum_le (s := Finset.univ) + (f := fun i => + (if A.H.eigenvalues i = 0 then 0 else ((A.H.eigenvalues i : ℂ) ^ (z.re : ℂ))) • + spectralProj A i) + _ ≤ K := by + unfold K + refine Finset.sum_le_sum ?_ + intro i _ + by_cases h0 : A.H.eigenvalues i = 0 + · simp [h0] + · have hpos : 0 < A.H.eigenvalues i := + lt_of_le_of_ne ((HermitianMat.zero_le_iff.mp hA).eigenvalues_nonneg i) + (Ne.symm (by simpa using h0)) + rw [norm_smul, show + ‖if A.H.eigenvalues i = 0 then 0 else ((A.H.eigenvalues i : ℂ) ^ (z.re : ℂ))‖ = + A.H.eigenvalues i ^ z.re by + simp [h0, Complex.norm_cpow_eq_rpow_re_of_pos hpos]] + refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _) + by_cases hle1 : A.H.eigenvalues i ≤ 1 + · simpa [h0] using + (Real.rpow_le_rpow_of_exponent_ge hpos hle1 hz'.1).trans + (le_max_left (A.H.eigenvalues i ^ l) (A.H.eigenvalues i ^ u)) + · simpa [h0] using + (Real.rpow_le_rpow_of_exponent_le (le_of_not_ge hle1) hz'.2).trans + (le_max_right (A.H.eigenvalues i ^ l) (A.H.eigenvalues i ^ u)) + +private lemma weighted_norm_one_T_map_le + (σ : MState d) (Φ : CPTPMap d d₂) (X : Matrix d d ℂ) : + weighted_norm 1 (Φ σ) ((T_map σ Φ) X) ≤ weighted_norm 1 σ X := by + let P : Matrix d₂ d₂ ℂ := (Φ σ).M.supportProj.mat + let Mcomp : MatrixMap d d₂ ℂ := (MatrixMap.conj P) ∘ₗ Φ.map + have hP : Pᴴ = P := by + simp [P] + have hMcomp_dual : Mcomp.dual = Φ.map.dual ∘ₗ MatrixMap.conj P := by + dsimp [Mcomp] + rw [show MatrixMap.dual (MatrixMap.conj P ∘ₗ Φ.map) = + Φ.map.dual ∘ₗ (MatrixMap.conj P).dual by + exact MatrixMap.dual_unique _ _ fun A B => by + change (MatrixMap.conj P (Φ.map A) * B).trace = + (A * Φ.map.dual ((MatrixMap.conj P).dual B)).trace + rw [MatrixMap.Dual.trace_eq (MatrixMap.conj P) (Φ.map A) B, + MatrixMap.Dual.trace_eq Φ.map A ((MatrixMap.conj P).dual B)], + show (MatrixMap.conj P).dual = MatrixMap.conj P by + exact MatrixMap.dual_unique _ _ fun A B => by + rw [show ((MatrixMap.conj P) A * B).trace = + ((A * Pᴴ * B) * P).trace by + simp [MatrixMap.conj, Matrix.mul_assoc] + rw [Matrix.trace_mul_comm] + simp [Matrix.mul_assoc]] + simp only [MatrixMap.conj, hP] + simp [Matrix.mul_assoc]] + have hconj1 : (MatrixMap.conj P) 1 ≤ (1 : Matrix d₂ d₂ ℂ) := by + dsimp [P] + simpa [MatrixMap.conj, hP, Matrix.mul_assoc, + show (Φ σ).M.supportProj.mat * (Φ σ).M.supportProj.mat = + (Φ σ).M.supportProj.mat by + rw [← pow_two, ← HermitianMat.mat_pow] + congr 1 + rw [HermitianMat.supportProj_eq_cfc, ← HermitianMat.cfc_pow, ← HermitianMat.cfc_comp] + exact HermitianMat.cfc_congr fun x _ => by by_cases hx0 : x = 0 <;> simp [hx0]] using + (supportProj_le_one (Φ σ).M) + have hMcomp_dual1 : Mcomp.dual 1 ≤ (1 : Matrix d d ℂ) := by + rw [hMcomp_dual, ← Φ.TP.dual.map_1] + simpa [map_sub, sub_nonneg] using + (MatrixMap.IsPositive.dual Φ.cp.IsPositive + (by simpa [sub_nonneg] using hconj1 : + (1 - (MatrixMap.conj P) 1).PosSemidef)).nonneg + have hMcomp_cp : Mcomp.IsCompletelyPositive := by + dsimp [Mcomp]; exact Φ.cp.comp (MatrixMap.conj_isCompletelyPositive P) + have hnorm_one (A : Matrix d d ℂ) : schattenNorm A 1 = A.traceNorm := by + rw [schattenNorm_eq_sum_singularValues_rpow _ zero_lt_one, Matrix.traceNorm_eq_sum_singularValues]; simp + have hnorm_one' (A : Matrix d₂ d₂ ℂ) : schattenNorm A 1 = A.traceNorm := by + rw [schattenNorm_eq_sum_singularValues_rpow _ zero_lt_one, Matrix.traceNorm_eq_sum_singularValues]; simp + calc + weighted_norm 1 (Φ σ) ((T_map σ Φ) X) + = (Gamma (Φ σ) ((T_map σ Φ) X)).traceNorm := by + simpa [hnorm_one'] using + weighted_norm_one_eq_trace_norm_Gamma (Φ σ) ((T_map σ Φ) X) + _ = (Mcomp (Gamma σ X)).traceNorm := by + simpa [Mcomp, MatrixMap.conj, P, hP, Matrix.mul_assoc] using + congrArg Matrix.traceNorm (by + unfold T_map T_op + simpa [Matrix.mul_assoc] using + Gamma_Gamma_inv_supportProj (σ := Φ σ) (X := Φ.map (Gamma σ X))) + _ ≤ (Gamma σ X).traceNorm := + traceNorm_le_of_dual_opNorm_le + (fun Z => MatrixMap.cp_subunital_opNorm_le_one (M := Mcomp.dual) + hMcomp_cp.dual hMcomp_dual1 Z) _ + _ = weighted_norm 1 σ X := by + simpa [hnorm_one] using (weighted_norm_one_eq_trace_norm_Gamma σ X).symm + +private lemma abs_trace_weighted_pair_le_right + (σ : MState d) (X Y : Matrix d d ℂ) : + ‖(Y * Gamma σ X).trace‖ ≤ weighted_norm 1 σ Y * weighted_norm_infty σ X := by + let S : Matrix d d ℂ := (σ.M.cfc (fun x => x ^ (1 / 2 : ℝ))).mat + calc + ‖(Y * Gamma σ X).trace‖ = ‖(X * Gamma σ Y).trace‖ := by + congr 1 + calc + (Y * Gamma σ X).trace = (Y * S * X * S).trace := by + simp [Gamma, S, Matrix.mul_assoc] + _ = ((S * Y * S) * X).trace := by + rw [show Y * S * X * S = ((Y * S * X) * S) by simp [Matrix.mul_assoc]] + rw [Matrix.trace_mul_comm] + simp [Matrix.mul_assoc] + _ = (X * Gamma σ Y).trace := by + rw [Matrix.trace_mul_comm] + simp [Gamma, S, Matrix.mul_assoc] + _ ≤ (X * Gamma σ Y).traceNorm := Matrix.abs_trace_le_traceNorm _ + _ ≤ ‖X‖ * (Gamma σ Y).traceNorm := Matrix.traceNorm_mul_le_opNorm_traceNorm _ _ + _ = weighted_norm 1 σ Y * weighted_norm_infty σ X := by + rw [weighted_norm_infty, weighted_norm_one_eq_trace_norm_Gamma] + simp [schattenNorm_eq_sum_singularValues_rpow _ zero_lt_one, + Matrix.traceNorm_eq_sum_singularValues, mul_comm] + +private lemma Gamma_Gamma_inv_density + {ρ σ : MState d} (h : σ.M.ker ≤ ρ.M.ker) : + Gamma σ (Gamma_inv σ ρ.M.mat) = ρ.M.mat := by + have hleft : ρ.M.mat * σ.M.supportProj.mat = ρ.M.mat := by + simpa using HermitianMat.mul_supportProj_of_ker_le (A := ρ.M) (B := σ.M) h + rw [Gamma_Gamma_inv_supportProj, + show σ.M.supportProj.mat * ρ.M.mat = ρ.M.mat by + simpa only [Matrix.conjTranspose_mul, HermitianMat.conjTranspose_mat] using + congrArg Matrix.conjTranspose hleft, + hleft] + +private lemma exists_le_exp_of_ker_le {ρ σ : MState d} (hker : σ.M.ker ≤ ρ.M.ker) : + ∃ x : ℝ, ρ.M ≤ Real.exp x • σ.M := by + open ComplexOrder in + let P := σ.M.supportProj + have hright : ρ.M.mat * P.mat = ρ.M.mat := by + simpa [P] using HermitianMat.mul_supportProj_of_ker_le (A := ρ.M) (B := σ.M) 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 σ.nonneg fun x _ => by + by_cases hx : x = 0 <;> simp [hx] + have hρ_le_P : ρ.M ≤ P := calc + ρ.M = ρ.M.conj P.mat := by + 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 α0 : ℝ := ∑ i, if σ.M.H.eigenvalues i = 0 then 0 else (σ.M.H.eigenvalues i)⁻¹ + have hterm j : 0 ≤ if σ.M.H.eigenvalues j = 0 then 0 else (σ.M.H.eigenvalues j)⁻¹ := by + split_ifs + · rfl + · exact inv_nonneg.mpr (HermitianMat.eigenvalues_nonneg σ.nonneg j) + have hα0_nonneg : 0 ≤ α0 := Finset.sum_nonneg fun i _ => hterm i + have hP_le : P ≤ α0 • σ.M := by + dsimp [P] + rw [← sub_nonneg, show α0 • σ.M = σ.M.cfc (fun x => α0 * x) from by simp [α0], + HermitianMat.supportProj_eq_cfc, ← HermitianMat.cfc_sub_apply, HermitianMat.cfc_nonneg_iff] + intro i + set y := σ.M.H.eigenvalues i + by_cases hy0 : y = 0 + · simp [hy0] + · have hy_pos := lt_of_le_of_ne (HermitianMat.eigenvalues_nonneg σ.nonneg i) (Ne.symm hy0) + have hsingle : y⁻¹ ≤ α0 := by + dsimp [α0] + have hith : (if σ.M.H.eigenvalues i = 0 then 0 else (σ.M.H.eigenvalues i)⁻¹) = y⁻¹ := by + rw [if_neg hy0] + rw [← hith] + exact Finset.single_le_sum (fun j _ => hterm j) (Finset.mem_univ i) + have hmul := mul_le_mul_of_nonneg_right hsingle hy_pos.le + simp [hy0] at hmul ⊢ + change y⁻¹ * y ≤ α0 * y at hmul + nlinarith [inv_mul_cancel₀ hy0] + refine ⟨Real.log (α0 + 1), ?_⟩ + rw [Real.exp_log (by positivity : (0 : ℝ) < α0 + 1)] + exact hρ_le_P.trans <| hP_le.trans <| + smul_le_smul_of_nonneg_right (by linarith) σ.nonneg + +private lemma weighted_norm_Gamma_inv_density_eq + (α : ℝ) (hα : 1 < α) (ρ σ : MState d) : + weighted_norm α σ (Gamma_inv σ ρ.M.mat) = + ((ρ.M.conj (σ.M ^ ((1 - α) / (2 * α))).mat) ^ α).trace ^ (1 / α) := by + let t : ℝ := (1 - α) / (2 * α) + have hα0 : α ≠ 0 := by linarith + have hsum_ne : (1 / (2 * α : ℝ)) + (-(1 / 2 : ℝ)) ≠ 0 := by + intro h0 + field_simp [hα0] at h0 + linarith + have hmul (p q : ℝ) (hpq : p + q ≠ 0) (ht : p + q = t) : + (σ.M ^ p).mat * (σ.M ^ q).mat = (σ.M ^ t).mat := by + rw [← ht] + simpa using (HermitianMat.mat_rpow_add (A := σ.M) σ.nonneg (p := p) (q := q) hpq).symm + have hleft := hmul (1 / (2 * α : ℝ)) (-(1 / 2 : ℝ)) hsum_ne + (by dsimp [t]; field_simp [hα0]; ring) + have hright := hmul (-(1 / 2 : ℝ)) (1 / (2 * α : ℝ)) + (by simpa [add_comm] using hsum_ne) (by dsimp [t]; field_simp [hα0]; ring) + calc + weighted_norm α σ (Gamma_inv σ ρ.M.mat) + = schattenNorm + (((σ.M ^ (1 / (2 * α : ℝ))).mat * (σ.M ^ (-(1 / 2 : ℝ))).mat) * + (ρ.M.mat * ((σ.M ^ (-(1 / 2 : ℝ))).mat * (σ.M ^ (1 / (2 * α : ℝ))).mat))) α := by + unfold weighted_norm Gamma_inv + simp only [HermitianMat.rpow_eq_cfc] + ring_nf + simp [Matrix.mul_assoc] + _ = schattenNorm ((σ.M ^ t).mat * (ρ.M.mat * (σ.M ^ t).mat)) α := by + rw [hleft, hright] + _ = schattenNorm ((ρ.M.conj (σ.M ^ t).mat).mat) α := by + simp [HermitianMat.conj_apply_mat, Matrix.mul_assoc] + _ = ((ρ.M.conj (σ.M ^ ((1 - α) / (2 * α))).mat) ^ α).trace ^ (1 / α) := by + simpa [t] using schattenNorm_hermitian_pow + (A := ρ.M.conj (σ.M ^ t).mat) (HermitianMat.conj_nonneg _ ρ.nonneg) + (p := α) (by linarith) + +private lemma weighted_norm_Gamma_inv_density_pos + (α : ℝ) (hα : 1 < α) {ρ σ : MState d} (hker : σ.M.ker ≤ ρ.M.ker) : + 0 < weighted_norm α σ (Gamma_inv σ ρ.M.mat) := by + have hcore_pos : + 0 < ρ.M.conj (σ.M ^ ((1 - α) / (2 * α))).mat := by + exact HermitianMat.conj_pos ρ.pos (by + grw [← hker] + exact HermitianMat.ker_rpow_le_of_nonneg σ.nonneg) + rw [weighted_norm_Gamma_inv_density_eq α hα ρ σ] + exact Real.rpow_pos_of_pos (HermitianMat.trace_pos (HermitianMat.rpow_pos hcore_pos)) _ + +private lemma sandwich_core_trace_eq_weighted_norm_rpow + (α : ℝ) (hα : 1 < α) (ρ σ : MState d) : + ((ρ.M.conj (σ.M ^ ((1 - α) / (2 * α))).mat) ^ α).trace = + weighted_norm α σ (Gamma_inv σ ρ.M.mat) ^ α := by + rw [weighted_norm_Gamma_inv_density_eq α hα ρ σ] + rw [← Real.rpow_mul + (HermitianMat.trace_nonneg (HermitianMat.rpow_nonneg (HermitianMat.conj_nonneg _ ρ.nonneg)))] + field_simp [show α ≠ 0 by linarith] + rw [Real.rpow_one] + +private lemma normalized_sandwich_core_trace_eq_one + (α : ℝ) (hα : 1 < α) {ρ σ : MState d} (hker : σ.M.ker ≤ ρ.M.ker) : + ((((weighted_norm α σ (Gamma_inv σ ρ.M.mat))⁻¹) • + (ρ.M.conj (σ.M ^ ((1 - α) / (2 * α))).mat)) ^ α).trace = 1 := by + let N := weighted_norm α σ (Gamma_inv σ ρ.M.mat) + let A := ρ.M.conj (σ.M ^ ((1 - α) / (2 * α))).mat + have hpos := weighted_norm_Gamma_inv_density_pos α hα hker + have hcore_nonneg : 0 ≤ A := by + simpa [A] using HermitianMat.conj_nonneg _ ρ.nonneg + have hsmul_rpow_eq : + (N⁻¹ • A) ^ α = N⁻¹ ^ α • (A ^ α) := by + set c := N⁻¹ + have hc_nonneg : 0 ≤ c := by dsimp [c]; simpa [N] using inv_nonneg.mpr hpos.le + rw [show c • A = A.cfc (fun x => c * x) from + (HermitianMat.cfc_const_mul_id (A := A) (r := c)).symm] + rw [HermitianMat.rpow_eq_cfc, ← HermitianMat.cfc_comp] + calc + A.cfc (((fun x => x ^ α) : ℝ → ℝ) ∘ fun x => c * x) + = A.cfc (fun x => c ^ α * x ^ α) := by + apply HermitianMat.cfc_congr_of_nonneg hcore_nonneg + intro x hx + rw [Function.comp_apply, Real.mul_rpow hc_nonneg hx] + _ = c ^ α • (A ^ α) := by + rw [HermitianMat.cfc_const_mul, HermitianMat.rpow_eq_cfc] + change ((N⁻¹ • A) ^ α).trace = 1 + rw [hsmul_rpow_eq, HermitianMat.trace_smul] + change N⁻¹ ^ α * (A ^ α).trace = 1 + rw [show (A ^ α).trace = N ^ α by + change ((ρ.M.conj (σ.M ^ ((1 - α) / (2 * α))).mat) ^ α).trace = N ^ α + rw [sandwich_core_trace_eq_weighted_norm_rpow α hα ρ σ]] + rw [Real.inv_rpow (by simpa [N] using hpos.le)] + exact inv_mul_cancel₀ (Real.rpow_pos_of_pos (by simpa [N] using hpos) α).ne' + +private lemma traceNorm_supportCpow_beta_add_im_le_one + {A : HermitianMat d ℂ} (β : ℝ) (hβ : 1 < β) (hA : 0 ≤ A) + (htrace : (A ^ β).trace = 1) (t : ℝ) : + (supportCpow A ((β : ℂ) + Complex.I * t)).traceNorm ≤ 1 := by + have hβ0 : 0 < β := lt_trans zero_lt_one hβ + calc + (supportCpow A ((β : ℂ) + Complex.I * t)).traceNorm + = (supportCpow A (β : ℂ) * supportCpow A (Complex.I * t)).traceNorm := by + rw [← supportCpow_mul] + _ ≤ (supportCpow A (β : ℂ)).traceNorm * ‖supportCpow A (Complex.I * t)‖ := + Matrix.traceNorm_mul_le_traceNorm_opNorm _ _ + _ ≤ (supportCpow A (β : ℂ)).traceNorm * 1 := + mul_le_mul_of_nonneg_left + (norm_supportCpow_im_le_one A hA t) (Matrix.traceNorm_nonneg _) + _ = (supportCpow A (β : ℂ)).traceNorm := by simp + _ = ((A ^ β).mat).traceNorm := by rw [supportCpow_ofReal A hA hβ0] + _ = 1 := by + have htraceC : ((A ^ β).trace : ℂ) = 1 := by exact_mod_cast htrace + have hnormC : (((A ^ β).mat).traceNorm : ℂ) = 1 := + (Matrix.PosSemidef.traceNorm_PSD_eq_trace + (HermitianMat.zero_le_iff.mp (HermitianMat.rpow_nonneg hA))).trans + ((HermitianMat.trace_eq_trace_rc (A := A ^ β)).symm.trans htraceC) + exact_mod_cast hnormC + +private lemma traceNorm_supportCpow_im_beta_add_sandwich_le_one + {n : Type*} [Fintype n] [DecidableEq n] + (β : ℝ) (hβ : 1 < β) (σ : MState n) (A : HermitianMat n ℂ) + (hA_nonneg : 0 ≤ A) (hA_trace1 : (A ^ β).trace = 1) (t s : ℝ) : + (supportCpow σ.M (Complex.I * t) * + supportCpow A ((β : ℂ) + Complex.I * s) * + supportCpow σ.M (Complex.I * t)).traceNorm ≤ 1 := by + calc + (supportCpow σ.M (Complex.I * t) * + supportCpow A ((β : ℂ) + Complex.I * s) * + supportCpow σ.M (Complex.I * t)).traceNorm + ≤ (supportCpow A ((β : ℂ) + Complex.I * s)).traceNorm := Matrix.traceNorm_sandwich_le + (norm_supportCpow_im_le_one σ.M σ.nonneg t) + _ ≤ 1 := traceNorm_supportCpow_beta_add_im_le_one β hβ hA_nonneg hA_trace1 s + +private lemma opNorm_supportCpow_im_sandwich_le_one + {n : Type*} [Fintype n] [DecidableEq n] + (σ : MState n) (A : HermitianMat n ℂ) (hA_nonneg : 0 ≤ A) (t s : ℝ) : + ‖supportCpow σ.M (Complex.I * t) * + supportCpow A (Complex.I * s) * + supportCpow σ.M (Complex.I * t)‖ ≤ 1 := by + calc + ‖supportCpow σ.M (Complex.I * t) * + supportCpow A (Complex.I * s) * + supportCpow σ.M (Complex.I * t)‖ + ≤ ‖supportCpow A (Complex.I * s)‖ := by + have hS := norm_supportCpow_im_le_one σ.M σ.nonneg t + calc ‖supportCpow σ.M (Complex.I * t) * supportCpow A (Complex.I * s) * + supportCpow σ.M (Complex.I * t)‖ + ≤ ‖supportCpow σ.M (Complex.I * t)‖ * + ‖supportCpow A (Complex.I * s) * supportCpow σ.M (Complex.I * t)‖ := by + rw [Matrix.mul_assoc]; exact norm_mul_le _ _ + _ ≤ 1 * ‖supportCpow A (Complex.I * s) * supportCpow σ.M (Complex.I * t)‖ := + mul_le_mul_of_nonneg_right hS (norm_nonneg _) + _ = ‖supportCpow A (Complex.I * s) * supportCpow σ.M (Complex.I * t)‖ := one_mul _ + _ ≤ ‖supportCpow A (Complex.I * s)‖ * ‖supportCpow σ.M (Complex.I * t)‖ := + norm_mul_le _ _ + _ ≤ ‖supportCpow A (Complex.I * s)‖ * 1 := + mul_le_mul_of_nonneg_left hS (norm_nonneg _) + _ = ‖supportCpow A (Complex.I * s)‖ := mul_one _ + _ ≤ 1 := norm_supportCpow_im_le_one A hA_nonneg s + +private lemma weighted_norm_infty_supportCpow_sandwich_bound {n : Type*} + [Fintype n] [DecidableEq n] {β Kσneg KA : ℝ} (hβ : 1 < β) (σ : MState n) + (A : HermitianMat n ℂ) + (hKσneg : ∀ z ∈ Complex.HadamardThreeLines.verticalClosedStrip (-1 / 2) 0, + ‖supportCpow σ.M z‖ ≤ Kσneg) + (hKA : ∀ z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 β, + ‖supportCpow A z‖ ≤ KA) + {z : ℂ} (hz : z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1) : + weighted_norm_infty σ + (supportCpow σ.M (-z / 2) * supportCpow A ((β : ℂ) * z) * + supportCpow σ.M (-z / 2)) ≤ + Kσneg * KA * Kσneg := by + have hzL : -z / 2 ∈ Complex.HadamardThreeLines.verticalClosedStrip (-1 / 2) 0 := by + simp [Complex.HadamardThreeLines.verticalClosedStrip, Set.mem_preimage] at hz ⊢ + constructor <;> linarith + have hzC : (β : ℂ) * z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 β := by + simp [Complex.HadamardThreeLines.verticalClosedStrip, Set.mem_preimage] at hz ⊢ + constructor <;> nlinarith [hz.1, hz.2, hβ] + let L : Matrix n n ℂ := supportCpow σ.M (-z / 2) + let M : Matrix n n ℂ := supportCpow A ((β : ℂ) * z) + dsimp [weighted_norm_infty, L, M] + have hL_nonneg : 0 ≤ ‖L‖ := norm_nonneg L + have hM_nonneg : 0 ≤ ‖M‖ := norm_nonneg M + have hL_bound : ‖L‖ ≤ Kσneg := hKσneg (-z / 2) hzL + have hM_bound : ‖M‖ ≤ KA := hKA ((β : ℂ) * z) hzC + have hKσneg_nonneg : 0 ≤ Kσneg := hL_nonneg.trans hL_bound + have hKA_nonneg : 0 ≤ KA := hM_nonneg.trans hM_bound + have hML : ‖M * L‖ ≤ ‖M‖ * ‖L‖ := norm_mul_le M L + have hLM : ‖L‖ * ‖M * L‖ ≤ ‖L‖ * (‖M‖ * ‖L‖) := + mul_le_mul_of_nonneg_left hML hL_nonneg + have hMK : ‖M‖ * ‖L‖ ≤ KA * Kσneg := + mul_le_mul hM_bound hL_bound hL_nonneg hKA_nonneg + have hright : ‖L‖ * (‖M‖ * ‖L‖) ≤ Kσneg * (KA * Kσneg) := + mul_le_mul hL_bound hMK (mul_nonneg hM_nonneg hL_nonneg) hKσneg_nonneg + calc + ‖L * M * L‖ ≤ ‖L‖ * ‖M * L‖ := by + rw [Matrix.mul_assoc]; exact norm_mul_le _ _ + _ ≤ ‖L‖ * (‖M‖ * ‖L‖) := hLM + _ ≤ Kσneg * (KA * Kσneg) := hright + _ = Kσneg * KA * Kσneg := by ring + +private lemma weighted_norm_one_supportCpow_sandwich_bound {n : Type*} + [Fintype n] [DecidableEq n] {β KA : ℝ} (hβ : 1 < β) + (σ : MState n) (A : HermitianMat n ℂ) + (hKA : ∀ z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 β, + ‖supportCpow A z‖ ≤ KA) + {z : ℂ} (hz : z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1) : + weighted_norm 1 σ + (supportCpow σ.M ((z - 1) / 2) * supportCpow A ((β : ℂ) * (1 - z)) * + supportCpow σ.M ((z - 1) / 2)) ≤ + Fintype.card n * KA := by + have hzhalf : z / 2 ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1 := by + simp [Complex.HadamardThreeLines.verticalClosedStrip, Set.mem_preimage] at hz ⊢ + constructor <;> linarith + have hzC : (β : ℂ) * (1 - z) ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 β := by + have hβpos : 0 < β := by linarith + have hzre : z.re ∈ Set.Icc (0 : ℝ) 1 := by + simpa [Complex.HadamardThreeLines.verticalClosedStrip] using hz + have hre : ((β : ℂ) * (1 - z)).re = β * (1 - z.re) := by + simp [Complex.mul_re, Complex.sub_re] + change ((β : ℂ) * (1 - z)).re ∈ Set.Icc (0 : ℝ) β + rw [hre] constructor - · exact this.symm - · simpa [HermitianMat.diagonal, ← HermitianMat.mat_apply] using h - obtain ⟨U, hU_unitary, D, hA_eq, hD_le⟩ := h_decomp; - have hA_le : U * D * star U ≤ U * (M • 1) * star U := by - have hD_le : D ≤ M • (1 : HermitianMat d ℂ) := by - sorry - have := HermitianMat.conj_mono (M := U) hD_le - simp only [conj, AddMonoidHom.coe_mk, ZeroHom.coe_mk] at this - replace this := Subtype.coe_le_coe.mpr this - simp only [mat_smul] at this - exact this - rw [ ← hA_eq ] at hA_le - simp only [Algebra.mul_smul_comm, mul_one, Algebra.smul_mul_assoc, hU_unitary] at hA_le - exact hA_le - -set_option backward.isDefEq.respectTransparency false in -/-- The block matrix [[1, X], [X†, X†X]] is positive semidefinite. -/ -theorem block_matrix_posSemidef {m n k : Type*} [Fintype m] [Fintype n] [Fintype k] - (X : Matrix k n ℂ) (Y : Matrix k m ℂ): - (Matrix.fromBlocks (Yᴴ * Y) (Yᴴ * X) (Xᴴ * Y) (Xᴴ * X)).PosSemidef := by - set Z : Matrix (m ⊕ n) (m ⊕ n) ℂ := Matrix.fromBlocks (Yᴴ * Y) (Yᴴ * X) (Xᴴ * Y) (Xᴴ * X) - have hZ : Z = Matrix.fromBlocks (m := k) Yᴴ 0 Xᴴ 0 * Matrix.fromBlocks Y X 0 0 := by - simp +zetaDelta [Matrix.fromBlocks_multiply] - have hZ : Z = (Matrix.fromBlocks (o := k) Y X 0 0)ᴴ * Matrix.fromBlocks Y X 0 0 := by - rw [hZ] - ext i j ; simp [ Matrix.mul_apply]; - cases i <;> cases j <;> simp [ Matrix.fromBlocks ]; - rw [hZ] - exact Matrix.posSemidef_conjTranspose_mul_self _ - -theorem block_matrix_one_posSemidef {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] - (X : Matrix m n ℂ) : - (Matrix.fromBlocks 1 X Xᴴ (Xᴴ * X)).PosSemidef := by - simpa using block_matrix_posSemidef X (1 : Matrix m m ℂ) - -/-- The Data Processing Inequality for the Sandwiched Renyi relative entropy. -Proved in `https://arxiv.org/pdf/1306.5920`. Seems kind of involved. -/ -theorem sandwichedRenyiEntropy_DPI (hα : 1 ≤ α) (ρ σ : MState d) (Φ : CPTPMap d d₂) : - D̃_ α(Φ ρ‖Φ σ) ≤ D̃_ α(ρ‖σ) := by - --If we want, we can prove this just for 1 < α, and then use continuity (above) to take the limit as - -- α → 1. - sorry + · exact mul_nonneg hβpos.le (sub_nonneg.mpr hzre.2) + · exact mul_le_of_le_one_right hβpos.le (sub_le_self 1 hzre.1) + rw [weighted_norm_one_eq_trace_norm_Gamma, + show schattenNorm (Gamma σ + (supportCpow σ.M ((z - 1) / 2) * supportCpow A ((β : ℂ) * (1 - z)) * + supportCpow σ.M ((z - 1) / 2))) 1 = + (Gamma σ (supportCpow σ.M ((z - 1) / 2) * + supportCpow A ((β : ℂ) * (1 - z)) * + supportCpow σ.M ((z - 1) / 2))).traceNorm from by + rw [schattenNorm_eq_sum_singularValues_rpow _ (by norm_num), + Matrix.traceNorm_eq_sum_singularValues]; simp] + let S : Matrix n n ℂ := supportCpow σ.M (z / 2) + let M : Matrix n n ℂ := supportCpow A ((β : ℂ) * (1 - z)) + have hGammaY : + Gamma σ (supportCpow σ.M ((z - 1) / 2) * M * + supportCpow σ.M ((z - 1) / 2)) = S * M * S := by + dsimp [S, M] + rw [Gamma_supportCpow_shift] + congr 1 <;> push_cast <;> ring_nf + rw [hGammaY] + dsimp [S, M] + calc (S * M * S).traceNorm + ≤ M.traceNorm := Matrix.traceNorm_sandwich_le + (norm_supportCpow_mem_verticalClosedStrip_le_one (σ := σ) hzhalf) + _ ≤ Fintype.card n * ‖M‖ := by + classical + rw [Matrix.traceNorm_eq_sum_singularValues] + calc + ∑ i : n, singularValues M i ≤ ∑ _i : n, ‖M‖ := + Finset.sum_le_sum fun i _ => Matrix.singularValues_le_opNorm M i + _ = Fintype.card n * ‖M‖ := by simp + _ ≤ Fintype.card n * KA := + mul_le_mul_of_nonneg_left (hKA _ hzC) (by positivity) ---Helps us track this one sorry for the GQSL -axiom sandwichedRenyiEntropy_DPI_ax : type_of% @sandwichedRenyiEntropy_DPI +private def interpXin (β : ℝ) (σ : MState d) (A : HermitianMat d ℂ) : + ℂ → Matrix d d ℂ := + fun z => supportCpow σ.M (-z / 2) * supportCpow A ((β : ℂ) * z) * + supportCpow σ.M (-z / 2) -/- -info: 'sandwichedRenyiEntropy_DPI_ax' depends on axioms: [propext, - sandwichedRenyiEntropy_DPI_ax, - Classical.choice, - Quot.sound] --/ +private def interpYout (β : ℝ) (τ : MState d₂) (A : HermitianMat d₂ ℂ) : + ℂ → Matrix d₂ d₂ ℂ := + fun z => supportCpow τ.M ((z - 1) / 2) * supportCpow A ((β : ℂ) * (1 - z)) * + supportCpow τ.M ((z - 1) / 2) -/- Removed due to module system. -#guard_msgs in -#print axioms sandwichedRenyiEntropy_DPI_ax --/ +private def interpTrace (τ : MState d₂) (T : MatrixMap d d₂ ℂ) + (Xin : ℂ → Matrix d d ℂ) (Yout : ℂ → Matrix d₂ d₂ ℂ) : ℂ → ℂ := + fun z => (Yout z * Gamma τ (T (Xin z))).trace + +private lemma interpTrace_diffContOnCl {β : ℝ} (hβ : 1 < β) + (σ : MState d) (τ : MState d₂) (T : MatrixMap d d₂ ℂ) + (Ain : HermitianMat d ℂ) (Aout : HermitianMat d₂ ℂ) : + DiffContOnCl ℂ (interpTrace τ T (interpXin β σ Ain) (interpYout β τ Aout)) + (Complex.HadamardThreeLines.verticalStrip 0 1) := by + have hXinL_dc : + DiffContOnCl ℂ (fun z : ℂ => supportCpow σ.M (-z / 2)) + (Complex.HadamardThreeLines.verticalStrip 0 1) := by + refine (supportCpow_diffContOnCl_strip σ.M (-1 / 2) 0).comp ?_ ?_ + · exact (by fun_prop : Differentiable ℂ (fun z : ℂ => -z / 2)).diffContOnCl + · intro z hz + simp [Complex.HadamardThreeLines.verticalStrip] at hz ⊢ + constructor <;> linarith + have hXinC_dc : + DiffContOnCl ℂ (fun z : ℂ => supportCpow Ain ((β : ℂ) * z)) + (Complex.HadamardThreeLines.verticalStrip 0 1) := by + refine (supportCpow_diffContOnCl_strip Ain 0 β).comp ?_ ?_ + · exact (by fun_prop : Differentiable ℂ (fun z : ℂ => (β : ℂ) * z)).diffContOnCl + · intro z hz + simp [Complex.HadamardThreeLines.verticalStrip] at hz ⊢ + constructor <;> nlinarith [hz.1, hz.2, hβ] + have hYoutL_dc : + DiffContOnCl ℂ (fun z : ℂ => supportCpow τ.M ((z - 1) / 2)) + (Complex.HadamardThreeLines.verticalStrip 0 1) := by + refine (supportCpow_diffContOnCl_strip τ.M (-1 / 2) 0).comp ?_ ?_ + · exact (by fun_prop : Differentiable ℂ (fun z : ℂ => (z - 1) / 2)).diffContOnCl + · intro z hz + simp [Complex.HadamardThreeLines.verticalStrip] at hz ⊢ + constructor <;> linarith + have hYoutC_dc : + DiffContOnCl ℂ (fun z : ℂ => supportCpow Aout ((β : ℂ) * (1 - z))) + (Complex.HadamardThreeLines.verticalStrip 0 1) := by + refine (supportCpow_diffContOnCl_strip Aout 0 β).comp ?_ ?_ + · exact (by fun_prop : Differentiable ℂ (fun z : ℂ => (β : ℂ) * (1 - z))).diffContOnCl + · intro z hz + simp [Complex.HadamardThreeLines.verticalStrip] at hz ⊢ + constructor <;> nlinarith [hz.1, hz.2, hβ] + have hXin_dc : + DiffContOnCl ℂ (interpXin β σ Ain) (Complex.HadamardThreeLines.verticalStrip 0 1) := by + dsimp [interpXin] + exact + ⟨(hXinL_dc.1.mul hXinC_dc.1).mul hXinL_dc.1, + (hXinL_dc.2.mul hXinC_dc.2).mul hXinL_dc.2⟩ + have hYout_dc : + DiffContOnCl ℂ (interpYout β τ Aout) + (Complex.HadamardThreeLines.verticalStrip 0 1) := by + dsimp [interpYout] + exact + ⟨(hYoutL_dc.1.mul hYoutC_dc.1).mul hYoutL_dc.1, + (hYoutL_dc.2.mul hYoutC_dc.2).mul hYoutL_dc.2⟩ + let L : Matrix d d ℂ →ₗ[ℂ] Matrix d₂ d₂ ℂ := + { toFun := fun X => Gamma τ (T X) + map_add' := by + intro X Y + simp only [Gamma, map_add, Matrix.mul_add, Matrix.add_mul] + map_smul' := by + intro c X + simp only [Gamma, map_smul, Matrix.mul_smul, Matrix.smul_mul, RingHom.id_apply] } + let G : Matrix d d ℂ →L[ℂ] Matrix d₂ d₂ ℂ := + { toLinearMap := L + cont := L.continuous_of_finiteDimensional } + let hGX_dc := G.differentiable.comp_diffContOnCl hXin_dc + let trCLM : Matrix d₂ d₂ ℂ →L[ℂ] ℂ := + { toLinearMap := Matrix.traceLinearMap d₂ ℂ ℂ + cont := (Matrix.traceLinearMap d₂ ℂ ℂ).continuous_of_finiteDimensional } + exact trCLM.differentiable.comp_diffContOnCl + ⟨hYout_dc.1.mul hGX_dc.1, hYout_dc.2.mul hGX_dc.2⟩ + +private lemma interpTrace_left_boundary_le_one {β : ℝ} (hβ : 1 < β) + (σ : MState d) (τ : MState d₂) (T : MatrixMap d d₂ ℂ) + (Ain : HermitianMat d ℂ) (Aout : HermitianMat d₂ ℂ) + (hAin_nonneg : 0 ≤ Ain) (hAout_nonneg : 0 ≤ Aout) + (hAout_trace1 : (Aout ^ β).trace = 1) + (hInf : ∀ X, weighted_norm_infty τ (T X) ≤ weighted_norm_infty σ X) : + ∀ z ∈ Complex.re ⁻¹' ({0} : Set ℝ), + ‖interpTrace τ T (interpXin β σ Ain) (interpYout β τ Aout) z‖ ≤ 1 := by + intro z hz + have hz0 : z.re = 0 := by simpa using hz + have hY1 : weighted_norm 1 τ (interpYout β τ Aout z) ≤ 1 := by + rw [weighted_norm_one_eq_trace_norm_Gamma, + show schattenNorm (Gamma τ (interpYout β τ Aout z)) 1 = + (Gamma τ (interpYout β τ Aout z)).traceNorm from by + rw [schattenNorm_eq_sum_singularValues_rpow _ (by norm_num), + Matrix.traceNorm_eq_sum_singularValues]; simp] + dsimp [interpYout] + rw [show Gamma τ + (supportCpow τ.M ((z - 1) / 2) * supportCpow Aout ((β : ℂ) * (1 - z)) * + supportCpow τ.M ((z - 1) / 2)) = + supportCpow τ.M (z / 2) * supportCpow Aout ((β : ℂ) * (1 - z)) * + supportCpow τ.M (z / 2) from by + have hz : (((2 : ℂ)⁻¹) + (z - 1) / 2) = z / 2 := by + apply Complex.ext <;> simp; ring + simpa [hz] using Gamma_supportCpow_shift (σ := τ) (a := (z - 1) / 2) + (X := supportCpow Aout ((β : ℂ) * (1 - z)))] + rw [show z / 2 = Complex.I * (z.im / 2) from by + apply Complex.ext <;> simp [hz0, div_eq_mul_inv], + show (β : ℂ) * (1 - z) = (β : ℂ) + Complex.I * (-β * z.im) from by + apply Complex.ext <;> simp [hz0]] + simpa using + (traceNorm_supportCpow_im_beta_add_sandwich_le_one β hβ τ Aout + hAout_nonneg hAout_trace1 (z.im / 2) (-β * z.im)) + have hX1 : weighted_norm_infty τ (T (interpXin β σ Ain z)) ≤ 1 := by + refine (hInf (interpXin β σ Ain z)).trans ?_ + dsimp [weighted_norm_infty, interpXin] + rw [show -z / 2 = Complex.I * (-(z.im / 2)) from by + apply Complex.ext <;> simp [hz0, div_eq_mul_inv], + show (β : ℂ) * z = Complex.I * (β * z.im) from by + apply Complex.ext <;> simp [hz0]] + simpa using + (opNorm_supportCpow_im_sandwich_le_one σ Ain hAin_nonneg (-(z.im / 2)) (β * z.im)) + exact (show ‖interpTrace τ T (interpXin β σ Ain) (interpYout β τ Aout) z‖ + ≤ weighted_norm 1 τ (interpYout β τ Aout z) * + weighted_norm_infty τ (T (interpXin β σ Ain z)) from by + simpa [interpTrace] using + abs_trace_weighted_pair_le_right (σ := τ) + (X := T (interpXin β σ Ain z)) (Y := interpYout β τ Aout z)).trans + (mul_le_one₀ hY1 (by dsimp [weighted_norm_infty]; exact norm_nonneg _) hX1) + +private lemma interpTrace_right_boundary_le_one {β : ℝ} (hβ : 1 < β) + (σ : MState d) (τ : MState d₂) (T : MatrixMap d d₂ ℂ) + (Ain : HermitianMat d ℂ) (Aout : HermitianMat d₂ ℂ) + (hAin_nonneg : 0 ≤ Ain) (hAout_nonneg : 0 ≤ Aout) + (hAin_trace1 : (Ain ^ β).trace = 1) + (h1 : ∀ X, weighted_norm 1 τ (T X) ≤ weighted_norm 1 σ X) : + ∀ z ∈ Complex.re ⁻¹' ({1} : Set ℝ), + ‖interpTrace τ T (interpXin β σ Ain) (interpYout β τ Aout) z‖ ≤ 1 := by + intro z hz + have hz1 : z.re = 1 := by simpa using hz + have hY1 : weighted_norm_infty τ (interpYout β τ Aout z) ≤ 1 := by + dsimp [weighted_norm_infty, interpYout] + rw [show (z - 1) / 2 = Complex.I * (z.im / 2) from by + apply Complex.ext <;> simp [hz1, div_eq_mul_inv], + show (β : ℂ) * (1 - z) = Complex.I * (-β * z.im) from by + apply Complex.ext <;> simp [hz1]] + simpa using + (opNorm_supportCpow_im_sandwich_le_one τ Aout hAout_nonneg (z.im / 2) (-β * z.im)) + have hX1 : weighted_norm 1 σ (interpXin β σ Ain z) ≤ 1 := by + rw [weighted_norm_one_eq_trace_norm_Gamma, + show schattenNorm (Gamma σ (interpXin β σ Ain z)) 1 = + (Gamma σ (interpXin β σ Ain z)).traceNorm from by + rw [schattenNorm_eq_sum_singularValues_rpow _ (by norm_num), + Matrix.traceNorm_eq_sum_singularValues]; simp] + dsimp [interpXin] + rw [show Gamma σ + (supportCpow σ.M (-z / 2) * supportCpow Ain ((β : ℂ) * z) * + supportCpow σ.M (-z / 2)) = + supportCpow σ.M (((1 : ℂ) - z) / 2) * supportCpow Ain ((β : ℂ) * z) * + supportCpow σ.M (((1 : ℂ) - z) / 2) from by + have hz : (((2 : ℂ)⁻¹) + (-z / 2)) = (((1 : ℂ) - z) / 2) := by + apply Complex.ext <;> simp; ring + simpa [hz] using Gamma_supportCpow_shift (σ := σ) (a := (-z / 2)) + (X := supportCpow Ain ((β : ℂ) * z))] + rw [show (((1 : ℂ) - z) / 2) = Complex.I * (-(z.im / 2)) from by + apply Complex.ext <;> simp [hz1, div_eq_mul_inv], + show (β : ℂ) * z = (β : ℂ) + Complex.I * (β * z.im) from by + apply Complex.ext <;> simp [hz1]] + simpa using + (traceNorm_supportCpow_im_beta_add_sandwich_le_one β hβ σ Ain + hAin_nonneg hAin_trace1 (-(z.im / 2)) (β * z.im)) + have hTX1 : weighted_norm 1 τ (T (interpXin β σ Ain z)) ≤ 1 := + (h1 (interpXin β σ Ain z)).trans hX1 + exact (show ‖interpTrace τ T (interpXin β σ Ain) (interpYout β τ Aout) z‖ + ≤ weighted_norm_infty τ (interpYout β τ Aout z) * + weighted_norm 1 τ (T (interpXin β σ Ain z)) from by + calc + ‖interpTrace τ T (interpXin β σ Ain) (interpYout β τ Aout) z‖ + ≤ (interpYout β τ Aout z * + Gamma τ (T (interpXin β σ Ain z))).traceNorm := by + simpa [interpTrace] using Matrix.abs_trace_le_traceNorm + (interpYout β τ Aout z * Gamma τ (T (interpXin β σ Ain z))) + _ ≤ ‖interpYout β τ Aout z‖ * + (Gamma τ (T (interpXin β σ Ain z))).traceNorm := + Matrix.traceNorm_mul_le_opNorm_traceNorm _ _ + _ = weighted_norm_infty τ (interpYout β τ Aout z) * + weighted_norm 1 τ (T (interpXin β σ Ain z)) := by + rw [weighted_norm_one_eq_trace_norm_Gamma, + show schattenNorm (Gamma τ (T (interpXin β σ Ain z))) 1 + = (Gamma τ (T (interpXin β σ Ain z))).traceNorm from by + rw [schattenNorm_eq_sum_singularValues_rpow _ (by norm_num), + Matrix.traceNorm_eq_sum_singularValues]; simp] + rfl).trans + (mul_le_one₀ hY1 (by unfold weighted_norm; exact schattenNorm_nonneg _ _) hTX1) + +private lemma weighted_norm_density_contraction_of_interpolation {β : ℝ} (hβ : 1 < β) + (ρ σ : MState d) (ω τ : MState d₂) (T : MatrixMap d d₂ ℂ) + (hker : σ.M.ker ≤ ρ.M.ker) (hker_out : τ.M.ker ≤ ω.M.ker) + (hTρ : Gamma τ (T (Gamma_inv σ ρ.M.mat)) = ω.M.mat) + (hInf : ∀ X, weighted_norm_infty τ (T X) ≤ weighted_norm_infty σ X) + (h1 : ∀ X, weighted_norm 1 τ (T X) ≤ weighted_norm 1 σ X) : + weighted_norm β τ (Gamma_inv τ ω.M.mat) ≤ + weighted_norm β σ (Gamma_inv σ ρ.M.mat) := by + have hβne : β ≠ 0 := by linarith + have hr_ne : ((1 - β) / (2 * β) : ℝ) ≠ 0 := by + exact div_ne_zero (sub_ne_zero.mpr hβ.ne) (mul_ne_zero two_ne_zero hβne) + set cin := weighted_norm β σ (Gamma_inv σ ρ.M.mat) + set cout := weighted_norm β τ (Gamma_inv τ ω.M.mat) + have hcin_pos : 0 < cin := by simpa [cin] using weighted_norm_Gamma_inv_density_pos β hβ hker + have hcout_pos : 0 < cout := by simpa [cout] using weighted_norm_Gamma_inv_density_pos β hβ hker_out + set Ain : HermitianMat d ℂ := (cin⁻¹) • (ρ.M.conj (σ.M ^ ((1 - β) / (2 * β))).mat) + set Aout : HermitianMat d₂ ℂ := (cout⁻¹) • (ω.M.conj (τ.M ^ ((1 - β) / (2 * β))).mat) + have hAin_nonneg : 0 ≤ Ain := by + simp only [Ain] + exact smul_nonneg (inv_nonneg.mpr hcin_pos.le) (HermitianMat.conj_nonneg _ ρ.nonneg) + have hAout_nonneg : 0 ≤ Aout := by + simp only [Aout] + exact smul_nonneg (inv_nonneg.mpr hcout_pos.le) (HermitianMat.conj_nonneg _ ω.nonneg) + have hAin_trace1 : (Ain ^ β).trace = 1 := by + simpa [Ain, cin] using normalized_sandwich_core_trace_eq_one β hβ hker + have hAout_trace1 : (Aout ^ β).trace = 1 := by + simpa [Aout, cout] using normalized_sandwich_core_trace_eq_one β hβ hker_out + let Xin : ℂ → Matrix d d ℂ := interpXin β σ Ain + let Yout : ℂ → Matrix d₂ d₂ ℂ := interpYout β τ Aout + let f : ℂ → ℂ := interpTrace τ T Xin Yout + have hθeval : f (((1 / β : ℝ) : ℂ)) = cout / cin := by + let r : ℝ := (1 - β) / (2 * β) + have hs_add : + ((-(1 / (2 * β : ℝ)) : ℂ)) + (r : ℂ) = ((-1 / 2 : ℝ) : ℂ) := by + exact_mod_cast (by + dsimp [r] + field_simp [hβne] + ring_nf : (-(1 / (2 * β : ℝ))) + r = (-1 / 2 : ℝ)) + have hs_add' : + (r : ℂ) + ((-(1 / (2 * β : ℝ)) : ℂ)) = ((-1 / 2 : ℝ) : ℂ) := by + simpa [add_comm] using hs_add + let Sneg : Matrix d d ℂ := supportCpow σ.M (((-1 / 2 : ℝ) : ℂ)) + have hXinθ : + Xin (((1 / β : ℝ) : ℂ)) = + cin⁻¹ • (Sneg * ρ.M.mat * Sneg) := by + calc + Xin (((1 / β : ℝ) : ℂ)) + = supportCpow σ.M ((-(1 / (2 * β : ℝ)) : ℂ)) * + Ain.mat * + supportCpow σ.M ((-(1 / (2 * β : ℝ)) : ℂ)) := by + dsimp [Xin, interpXin] + rw [show ((β : ℂ) * (((1 / β : ℝ) : ℂ))) = 1 from by + exact_mod_cast (by field_simp [hβne] : β * (1 / β : ℝ) = 1), + show supportCpow Ain (1 : ℂ) = Ain.mat from by + simpa using supportCpow_ofReal Ain hAin_nonneg zero_lt_one] + simp [div_eq_mul_inv] + _ = supportCpow σ.M ((-(1 / (2 * β : ℝ)) : ℂ)) * + ((cin⁻¹) • (((σ.M ^ ((1 - β) / (2 * β))).mat) * ρ.M.mat * + ((σ.M ^ ((1 - β) / (2 * β))).mat)ᴴ)) * + supportCpow σ.M ((-(1 / (2 * β : ℝ)) : ℂ)) := by + simp [Ain, HermitianMat.conj_apply_mat] + _ = cin⁻¹ • + (supportCpow σ.M ((-(1 / (2 * β : ℝ)) : ℂ)) * + supportCpow σ.M ((((1 - β) / (2 * β) : ℝ) : ℂ)) * + ρ.M.mat * + (supportCpow σ.M ((((1 - β) / (2 * β) : ℝ) : ℂ)) * + supportCpow σ.M ((-(1 / (2 * β : ℝ)) : ℂ)))) := by + rw [HermitianMat.conjTranspose_mat, + ← supportCpow_ofReal_ne_zero (A := σ.M) (hA := σ.nonneg) + (r := (1 - β) / (2 * β)) hr_ne] + simp [Matrix.mul_assoc] + _ = cin⁻¹ • + (supportCpow σ.M (((-1 / 2 : ℝ) : ℂ)) * + ρ.M.mat * + supportCpow σ.M (((-1 / 2 : ℝ) : ℂ))) := by + rw [supportCpow_mul, supportCpow_mul, hs_add, hs_add'] + _ = cin⁻¹ • (Sneg * ρ.M.mat * Sneg) := by + rfl + have hTθ : + Gamma τ (T (Xin (((1 / β : ℝ) : ℂ)))) = (cin⁻¹) • ω.M.mat := by + calc + Gamma τ (T (Xin (((1 / β : ℝ) : ℂ)))) + = Gamma τ (T (cin⁻¹ • (Sneg * ρ.M.mat * Sneg))) := by + rw [hXinθ] + _ = (cin⁻¹) • Gamma τ (T (Sneg * ρ.M.mat * Sneg)) := by + simp [Gamma, Matrix.mul_assoc] + _ = (cin⁻¹) • Gamma τ (T (Gamma_inv σ ρ.M.mat)) := by + rw [show Sneg * ρ.M.mat * Sneg = Gamma_inv σ ρ.M.mat by + dsimp [Sneg] + rw [supportCpow_ofReal_ne_zero σ.M σ.nonneg (by norm_num), Gamma_inv, + HermitianMat.rpow_eq_cfc]] + _ = (cin⁻¹) • ω.M.mat := by + rw [hTρ] + have hYθ : + Yout (((1 / β : ℝ) : ℂ)) = + supportCpow τ.M ((((1 - β) / (2 * β) : ℝ) : ℂ)) * + (Aout ^ (β - 1)).mat * + supportCpow τ.M ((((1 - β) / (2 * β) : ℝ) : ℂ)) := by + dsimp [Yout, interpYout] + rw [show ((((1 / β : ℝ) : ℂ) - 1) / 2) = ((((1 - β) / (2 * β) : ℝ) : ℂ)) by + exact_mod_cast (by field_simp [hβne] : + (((1 / β : ℝ) - 1) / 2) = ((1 - β) / (2 * β) : ℝ))] + rw [show ((β : ℂ) * (1 - (((1 / β : ℝ) : ℂ)))) = (β - 1 : ℂ) from by + exact_mod_cast (by field_simp [hβne] : β * (1 - (1 / β : ℝ)) = β - 1)] + rw [show supportCpow Aout ((β : ℂ) - 1) = (Aout ^ (β - 1)).mat from by + simpa using supportCpow_ofReal Aout hAout_nonneg (show 0 < β - 1 by linarith)] + have hBout : + supportCpow τ.M ((((1 - β) / (2 * β) : ℝ) : ℂ)) * ω.M.mat * + supportCpow τ.M ((((1 - β) / (2 * β) : ℝ) : ℂ)) = + cout • Aout.mat := by + rw [supportCpow_ofReal_ne_zero (A := τ.M) (hA := τ.nonneg) + (r := (1 - β) / (2 * β)) hr_ne] + simp [Aout, HermitianMat.conj_apply_mat, Matrix.mul_assoc, smul_smul, + show cout * cout⁻¹ = (1 : ℝ) by field_simp [hcout_pos.ne']] + have hpowmul : + (Aout ^ (β - 1)).mat * Aout.mat = (Aout ^ β).mat := by + calc + (Aout ^ (β - 1)).mat * Aout.mat = + supportCpow Aout (((β - 1 : ℝ) : ℂ)) * supportCpow Aout (1 : ℂ) := by + rw [supportCpow_ofReal Aout hAout_nonneg (by linarith), + show supportCpow Aout (1 : ℂ) = Aout.mat from by + simpa using supportCpow_ofReal Aout hAout_nonneg zero_lt_one] + _ = supportCpow Aout (β : ℂ) := by + rw [supportCpow_mul] + congr 1 + simp + _ = (Aout ^ β).mat := by + symm + rw [supportCpow_ofReal Aout hAout_nonneg (show 0 < β by linarith)] + let Sout : Matrix d₂ d₂ ℂ := + supportCpow τ.M ((((1 - β) / (2 * β) : ℝ) : ℂ)) + calc + f (((1 / β : ℝ) : ℂ)) + = ((Yout (((1 / β : ℝ) : ℂ))) * ((cin⁻¹) • ω.M.mat)).trace := by + dsimp [f, interpTrace] + rw [hTθ] + _ = cin⁻¹ * (Yout (((1 / β : ℝ) : ℂ)) * ω.M.mat).trace := by + simp + _ = cin⁻¹ * (((Sout * (Aout ^ (β - 1)).mat * Sout) * ω.M.mat).trace) := by + rw [hYθ] + _ = cin⁻¹ * (((Aout ^ (β - 1)).mat * (Sout * ω.M.mat * Sout)).trace) := by + congr 1 + let A : Matrix d₂ d₂ ℂ := (Aout ^ (β - 1)).mat + let R : Matrix d₂ d₂ ℂ := ω.M.mat + have hcyc : ((Sout * A * Sout) * R).trace = (A * (Sout * R * Sout)).trace := by + calc + ((Sout * A * Sout) * R).trace = (Sout * A * (Sout * R)).trace := by + rw [Matrix.mul_assoc] + _ = ((Sout * R) * Sout * A).trace := by + rw [Matrix.trace_mul_cycle] + _ = (A * (Sout * R) * Sout).trace := by + rw [Matrix.trace_mul_cycle] + _ = (A * ((Sout * R) * Sout)).trace := by + rw [Matrix.mul_assoc] + _ = (A * (Sout * R * Sout)).trace := rfl + simpa [A, R] using hcyc + _ = cin⁻¹ * (((Aout ^ (β - 1)).mat * (cout • Aout.mat)).trace) := by rw [hBout] + _ = cin⁻¹ * (cout * ((Aout ^ β).mat).trace) := by + rw [Matrix.mul_smul, Matrix.trace_smul] + simp [hpowmul] + _ = cin⁻¹ * (cout * 1) := by + rw [show ((Aout ^ β).mat).trace = (1 : ℂ) from by + exact (HermitianMat.trace_eq_trace_rc (A := Aout ^ β)).symm.trans + (show (((Aout ^ β).trace : ℂ) = 1) from by exact_mod_cast hAout_trace1)] + _ = cout / cin := by + calc + (((cin⁻¹ : ℝ) : ℂ) * (cout * 1)) + = ((cin : ℂ)⁻¹ * ((cout : ℂ) * 1)) := by simp + _ = (cout : ℂ) / cin := by simp [div_eq_mul_inv, mul_comm] + obtain ⟨Kσneg, hKσneg⟩ := + exists_norm_supportCpow_le_on_verticalClosedStrip σ.M σ.nonneg (-1 / 2) 0 + obtain ⟨KAin, hKAin⟩ := + exists_norm_supportCpow_le_on_verticalClosedStrip Ain hAin_nonneg 0 β + obtain ⟨KAout, hKAout⟩ := + exists_norm_supportCpow_le_on_verticalClosedStrip Aout hAout_nonneg 0 β + let KXin : ℝ := Kσneg * KAin * Kσneg + let KYout : ℝ := Fintype.card d₂ * KAout + have hB : + BddAbove ((norm ∘ f) '' Complex.HadamardThreeLines.verticalClosedStrip 0 1) := by + refine ⟨KYout * KXin, ?_⟩ + rintro _ ⟨z, hz, rfl⟩ + simpa [f, interpTrace] using + (abs_trace_weighted_pair_le_right (σ := τ) (X := T (Xin z)) (Y := Yout z)).trans + (mul_le_mul + (by + simpa [Yout, interpYout, KYout] using + (weighted_norm_one_supportCpow_sandwich_bound (β := β) hβ τ Aout hKAout hz)) + ((hInf (Xin z)).trans + (by + simpa [Xin, interpXin, KXin] using + (weighted_norm_infty_supportCpow_sandwich_bound (β := β) hβ σ Ain hKσneg + hKAin hz))) + (by dsimp [weighted_norm_infty]; exact norm_nonneg _) + (by + exact mul_nonneg (by positivity) <| le_trans (norm_nonneg _) <| hKAout 0 <| by + simp [Complex.HadamardThreeLines.verticalClosedStrip, show 0 ≤ β by linarith])) + have hfθ : + ‖f (((1 / β : ℝ) : ℂ))‖ ≤ 1 := by + simpa using + (Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip' + (f := f) (l := 0) (u := 1) (a := 1) (b := 1) zero_lt_one + (by + have hβpos : 0 < β := by linarith + simp [Complex.HadamardThreeLines.verticalClosedStrip, Set.mem_preimage] + constructor + · positivity + · simpa [one_div] using (div_le_one hβpos).2 (le_of_lt hβ)) + (by simpa [f, Xin, Yout] using interpTrace_diffContOnCl hβ σ τ T Ain Aout) hB + (by + simpa [f, Xin, Yout] using + interpTrace_left_boundary_le_one hβ σ τ T Ain Aout hAin_nonneg hAout_nonneg + hAout_trace1 hInf) + (by + simpa [f, Xin, Yout] using + interpTrace_right_boundary_le_one hβ σ τ T Ain Aout hAin_nonneg hAout_nonneg + hAin_trace1 h1)) + exact (div_le_one hcin_pos).mp <| by + have hnorm_ratio : ‖cout / cin‖ ≤ 1 := by + have hnorm_ratioC : ‖(((cout / cin : ℝ) : ℂ))‖ ≤ 1 := by + have hθeval' : f (((1 / β : ℝ) : ℂ)) = (((cout / cin : ℝ) : ℂ) : ℂ) := by + simpa using hθeval + rw [← hθeval'] + exact hfθ + simpa using hnorm_ratioC + rwa [Real.norm_eq_abs, abs_of_nonneg (by positivity : 0 ≤ cout / cin)] at hnorm_ratio + +private lemma sandwichedRenyiEntropy_DPI_hnorm {β : ℝ} (hβ : 1 < β) + (ρ σ : MState d) (Φ : CPTPMap d d₂) + (hker : σ.M.ker ≤ ρ.M.ker) (hker_map : (Φ σ).M.ker ≤ (Φ ρ).M.ker) : + weighted_norm β (Φ σ) (Gamma_inv (Φ σ) (Φ ρ).M.mat) ≤ + weighted_norm β σ (Gamma_inv σ ρ.M.mat) := by + refine weighted_norm_density_contraction_of_interpolation hβ ρ σ (Φ ρ) (Φ σ) + (T_map σ Φ) hker hker_map ?_ ?_ ?_ + · calc + Gamma (Φ σ) ((T_map σ Φ) (Gamma_inv σ ρ.M.mat)) + = Gamma (Φ σ) (Gamma_inv (Φ σ) (Φ ρ).M.mat) := by + rw [show (T_map σ Φ) (Gamma_inv σ ρ.M.mat) = + Gamma_inv (Φ σ) (Φ ρ).M.mat from by + dsimp [T_map, T_op] + rw [Gamma_Gamma_inv_density hker] + rfl] + _ = (Φ ρ).M.mat := Gamma_Gamma_inv_density hker_map + · intro X + dsimp [weighted_norm_infty] + exact MatrixMap.cp_subunital_opNorm_le_one (M := T_map σ Φ) (T_is_CP σ Φ) + (by + dsimp [T_map, T_op] + rw [Gamma_one] + change Gamma_inv (Φ σ) (Φ σ).M.mat ≤ 1 + rw [Gamma_inv_self_supportProj] + simpa using supportProj_le_one (Φ σ).M) X + · intro X + exact weighted_norm_one_T_map_le σ Φ X + +private lemma sandwichedRenyiEntropy_DPI_ker {β : ℝ} (hβ : 1 < β) + (ρ σ : MState d) (Φ : CPTPMap d d₂) (hker : σ.M.ker ≤ ρ.M.ker) : + D̃_ β(Φ ρ‖Φ σ) ≤ D̃_ β(ρ‖σ) := by + have hker_map : (Φ σ).M.ker ≤ (Φ ρ).M.ker := by + rcases exists_le_exp_of_ker_le hker with ⟨x, hx⟩ + have hmap : (Φ ρ).M ≤ Real.exp x • (Φ σ).M := by + have hdiff : (0 : Matrix d d ℂ) ≤ Real.exp x • σ.M.mat - ρ.M.mat := by + simpa [sub_nonneg] using hx + have h : (0 : Matrix d₂ d₂ ℂ) ≤ Φ.map (Real.exp x • σ.M.mat - ρ.M.mat) := + (Φ.cp.IsPositive (by simpa [Matrix.nonneg_iff_posSemidef] using hdiff)).nonneg + simpa [sub_nonneg, map_sub, map_smul] using h + exact HermitianMat.ker_le_of_le_smul (by positivity) (Φ ρ).nonneg hmap + set cin : ℝ := weighted_norm β σ (Gamma_inv σ ρ.M.mat) + set cout : ℝ := weighted_norm β (Φ σ) (Gamma_inv (Φ σ) (Φ ρ).M.mat) + have hcin_pos : 0 < cin := by + dsimp [cin]; exact weighted_norm_Gamma_inv_density_pos β hβ hker + have hcout_pos : 0 < cout := by + dsimp [cout]; exact weighted_norm_Gamma_inv_density_pos β hβ hker_map + have hnorm : cout ≤ cin := + sandwichedRenyiEntropy_DPI_hnorm hβ ρ σ Φ hker hker_map + have hβ0 : 0 < β := lt_trans zero_lt_one hβ + have hout : + D̃_ β(Φ ρ‖Φ σ) = ENNReal.ofReal (Real.log (cout ^ β) / (β - 1)) := by + have hnonneg : + 0 ≤ Real.log (cout ^ β) / (β - 1) := by + simpa [hβ.ne', cout, sandwich_core_trace_eq_weighted_norm_rpow β hβ (Φ ρ) (Φ σ)] using + (sandwichedRelRentropy_nonneg hβ0 hker_map) + unfold SandwichedRelRentropy + simpa [hβ0, hβ.ne', hker_map, cout, + sandwich_core_trace_eq_weighted_norm_rpow β hβ (Φ ρ) (Φ σ)] using + (ENNReal.ofReal_eq_coe_nnreal hnonneg).symm + have hin : + D̃_ β(ρ‖σ) = ENNReal.ofReal (Real.log (cin ^ β) / (β - 1)) := by + have hnonneg : + 0 ≤ Real.log (cin ^ β) / (β - 1) := by + simpa [hβ.ne', cin, sandwich_core_trace_eq_weighted_norm_rpow β hβ ρ σ] using + (sandwichedRelRentropy_nonneg hβ0 hker) + unfold SandwichedRelRentropy + simpa [hβ0, hβ.ne', hker, cin, + sandwich_core_trace_eq_weighted_norm_rpow β hβ ρ σ] using + (ENNReal.ofReal_eq_coe_nnreal hnonneg).symm + rw [hout, hin] + apply ENNReal.ofReal_le_ofReal + have hpow_le : cout ^ β ≤ cin ^ β := by + exact Real.rpow_le_rpow hcout_pos.le hnorm (by linarith) + have hpow_pos_out : 0 < cout ^ β := by + exact Real.rpow_pos_of_pos hcout_pos _ + have hpow_pos_in : 0 < cin ^ β := by + exact Real.rpow_pos_of_pos hcin_pos _ + have hlog_le : Real.log (cout ^ β) ≤ Real.log (cin ^ β) := by + exact Real.strictMonoOn_log.monotoneOn hpow_pos_out hpow_pos_in hpow_le + exact div_le_div_of_nonneg_right hlog_le (by linarith) + +/-- The high-parameter branch of the data processing inequality for sandwiched Rényi relative +entropy: for `1 ≤ α`, applying a CPTP map cannot increase `D̃_α`. + +The proof follows the Hadamard three-lines/interpolation argument for the sandwiched Rényi DPI +from Müller-Lennert et al. and Beigi, with the `α = 1` case obtained by right-continuity from +`α > 1`. -/ +theorem sandwichedRenyiEntropy_DPI_of_one_le + (hα : 1 ≤ α) (ρ σ : MState d) (Φ : CPTPMap d d₂) : + D̃_ α(Φ ρ‖Φ σ) ≤ D̃_ α(ρ‖σ) := by + have hstrict : ∀ {β : ℝ}, 1 < β → D̃_ β(Φ ρ‖Φ σ) ≤ D̃_ β(ρ‖σ) := by + intro β hβ + by_cases hker : σ.M.ker ≤ ρ.M.ker + · exact sandwichedRenyiEntropy_DPI_ker hβ ρ σ Φ hker + · have : D̃_ β(ρ‖σ) = ⊤ := by + unfold SandwichedRelRentropy; simp [show 0 < β from lt_trans zero_lt_one hβ, hker] + rw [this]; exact le_top + rcases eq_or_lt_of_le hα with rfl | hgt + · have hmono := nhdsWithin_mono (1 : ℝ) (Set.Ioi_subset_Ioi zero_le_one) + exact le_of_tendsto_of_tendsto + (((sandwichedRelRentropy.continuousOn (Φ ρ) (Φ σ)) 1 (by norm_num)).mono_left + hmono) + (((sandwichedRelRentropy.continuousOn ρ σ) 1 (by norm_num)).mono_left + hmono) + (by + filter_upwards [self_mem_nhdsWithin] with β hβ + exact hstrict hβ) + · exact hstrict hgt diff --git a/QuantumInfo/Finite/Entropy/Relative.lean b/QuantumInfo/Finite/Entropy/Relative.lean index ee1ac89f3..ea1b814df 100644 --- a/QuantumInfo/Finite/Entropy/Relative.lean +++ b/QuantumInfo/Finite/Entropy/Relative.lean @@ -20,7 +20,7 @@ variable [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] [DecidableEq dA₁] variable {𝕜 : Type*} [RCLike 𝕜] variable {α : ℝ} {ρ σ : MState d} -open scoped InnerProductSpace RealInnerProductSpace HermitianMat +open scoped Matrix ComplexOrder InnerProductSpace RealInnerProductSpace HermitianMat /-! To do relative entropies, we start with the _sandwiched Renyi Relative Entropy_ which is a nice general form. @@ -2133,10 +2133,178 @@ theorem qRelativeEnt_ne_top {ρ σ : MState d} [σ.M.NonSingular] : 𝐃(ρ‖σ rw [qRelativeEnt] finiteness +omit [DecidableEq dA] in +open HermitianMat in +private lemma inner_kron_one_eq_inner_traceRight + (A : HermitianMat dA ℂ) (M : HermitianMat (dA × dB) ℂ) : + ⟪A ⊗ₖ (1 : HermitianMat dB ℂ), M⟫ = ⟪A, M.traceRight⟫ := by + rw [inner_comm, inner_eq_re_trace, inner_eq_re_trace] + exact (congrArg Complex.re (Matrix.trace_mul_kron_one_right M.mat A.mat)).trans <| by + simpa using congrArg Complex.re (Matrix.trace_mul_comm M.traceRight.mat A.mat) + +omit [DecidableEq dB] in +open HermitianMat in +private lemma inner_one_kron_eq_inner_traceLeft + (B : HermitianMat dB ℂ) (M : HermitianMat (dA × dB) ℂ) : + ⟪(1 : HermitianMat dA ℂ) ⊗ₖ B, M⟫ = ⟪B, M.traceLeft⟫ := by + rw [inner_comm, inner_eq_re_trace, inner_eq_re_trace] + exact (congrArg Complex.re (Matrix.trace_mul_one_kron_right M.mat B.mat)).trans <| by + simpa using congrArg Complex.re (Matrix.trace_mul_comm M.traceLeft.mat B.mat) + +private lemma fixed_support_kron_right (ρ : MState (dA × dB)) + {x : EuclideanSpace ℂ (dA × dB)} (hx : x ∈ ρ.M.support) : + (ρ.traceRight.M.supportProj ⊗ₖ (1 : HermitianMat dB ℂ)).lin x = x := by + let K : HermitianMat (dA × dB) ℂ := ρ.traceRight.M.kerProj ⊗ₖ (1 : HermitianMat dB ℂ) + simpa [Matrix.toEuclideanLin, + show K.mat.toEuclideanLin x = 0 by + simpa [HermitianMat.lin] using + ((HermitianMat.inner_zero_iff ρ.nonneg (by + simpa [K] using HermitianMat.kronecker_nonneg + (by simpa [HermitianMat.kerProj] using + (HermitianMat.projector_nonneg (S := ρ.traceRight.M.ker))) + (by rw [HermitianMat.zero_le_iff]; exact Matrix.PosSemidef.one))).1 (by + rw [HermitianMat.inner_comm, inner_kron_one_eq_inner_traceRight, + HermitianMat.inner_comm] + simpa [K, MState.exp_val] using + (ρ.traceRight.exp_val_eq_zero_iff + (by simpa [HermitianMat.kerProj] using + (HermitianMat.projector_nonneg (S := ρ.traceRight.M.ker)))).2 + (by simp)) hx)] using + congrArg (fun T : HermitianMat (dA × dB) ℂ => T.mat.toEuclideanLin x) + (show K + ρ.traceRight.M.supportProj ⊗ₖ (1 : HermitianMat dB ℂ) = 1 by + simp only [K, ← HermitianMat.add_kronecker, + ρ.traceRight.M.kerProj_add_supportProj, HermitianMat.kronecker_one_one]) + +private lemma fixed_support_kron_left (ρ : MState (dA × dB)) + {x : EuclideanSpace ℂ (dA × dB)} (hx : x ∈ ρ.M.support) : + ((1 : HermitianMat dA ℂ) ⊗ₖ ρ.traceLeft.M.supportProj).lin x = x := by + let K : HermitianMat (dA × dB) ℂ := (1 : HermitianMat dA ℂ) ⊗ₖ ρ.traceLeft.M.kerProj + let P : HermitianMat (dA × dB) ℂ := (1 : HermitianMat dA ℂ) ⊗ₖ ρ.traceLeft.M.supportProj + have hK_nonneg : 0 ≤ K := by + dsimp [K] + exact HermitianMat.kronecker_nonneg + (by rw [HermitianMat.zero_le_iff]; exact Matrix.PosSemidef.one) + (by simpa [HermitianMat.kerProj] using + (HermitianMat.projector_nonneg (S := ρ.traceLeft.M.ker))) + have hsum : K + P = 1 := by + show K + P = 1 + simp only [K, P, ← HermitianMat.kronecker_add, ρ.traceLeft.M.kerProj_add_supportProj, + HermitianMat.kronecker_one_one] + simpa [P, Matrix.toEuclideanLin, + show K.mat.toEuclideanLin x = 0 by + simpa [HermitianMat.lin] using ((HermitianMat.inner_zero_iff ρ.nonneg hK_nonneg).1 (by + rw [HermitianMat.inner_comm, inner_one_kron_eq_inner_traceLeft] + rw [HermitianMat.inner_comm] + simpa [K, MState.exp_val] using + (ρ.traceLeft.exp_val_eq_zero_iff + (by simpa [HermitianMat.kerProj] using + (HermitianMat.projector_nonneg (S := ρ.traceLeft.M.ker)))).2 + (by simp)) hx)] using + congrArg (fun T : HermitianMat (dA × dB) ℂ => T.mat.toEuclideanLin x) hsum + /-- `I(A:B) = 𝐃(ρᴬᴮ‖ρᴬ ⊗ ρᴮ)` -/ theorem qMutualInfo_as_qRelativeEnt (ρ : MState (dA × dB)) : qMutualInfo ρ = (𝐃(ρ‖ρ.traceRight ⊗ᴹ ρ.traceLeft) : EReal) := by - sorry + have fixed_support_kron_prod : ∀ {x : EuclideanSpace ℂ (dA × dB)}, + x ∈ ρ.M.support → + (ρ.traceRight.M.supportProj ⊗ₖ ρ.traceLeft.M.supportProj).lin x = x := by + intro x hx + let A : Matrix (dA × dB) (dA × dB) ℂ := + Matrix.kroneckerMap (· * ·) ρ.traceRight.M.supportProj.mat (1 : Matrix dB dB ℂ) + let B : Matrix (dA × dB) (dA × dB) ℂ := + Matrix.kroneckerMap (· * ·) (1 : Matrix dA dA ℂ) ρ.traceLeft.M.supportProj.mat + have hxA' : A.toEuclideanLin x = x := by + simpa [A, HermitianMat.lin, Matrix.toEuclideanLin] using fixed_support_kron_right ρ hx + have hxB' : B.toEuclideanLin x = x := by + simpa [B, HermitianMat.lin, Matrix.toEuclideanLin] using fixed_support_kron_left ρ hx + have hmul : (A * B).toEuclideanLin x = x := by + simpa [A, B, Matrix.toEuclideanLin, Matrix.mulVec_mulVec] using + show A.toEuclideanLin (B.toEuclideanLin x) = x by rw [hxB', hxA'] + simpa [HermitianMat.lin, Matrix.toEuclideanLin, A, B, ← Matrix.mul_kronecker_mul] using hmul + have prod_marginals_ker_le : (ρ.traceRight ⊗ᴹ ρ.traceLeft).M.ker ≤ ρ.M.ker := by + let P : HermitianMat (dA × dB) ℂ := ρ.traceRight.M.supportProj ⊗ₖ ρ.traceLeft.M.supportProj + have hP : ρ.M.support ≤ P.support := by + intro x hx + exact ⟨x, by simpa [P] using fixed_support_kron_prod hx⟩ + have hkerP : P.ker ≤ ρ.M.ker := by + simpa [HermitianMat.support_orthogonal_eq_range] using Submodule.orthogonal_le hP + exact (show (ρ.traceRight ⊗ᴹ ρ.traceLeft).M.ker ≤ P.ker by + change LinearMap.ker + ((Matrix.kroneckerMap (· * ·) ρ.traceRight.M.mat ρ.traceLeft.M.mat).toEuclideanLin) + ≤ LinearMap.ker + ((Matrix.kroneckerMap (· * ·) ρ.traceRight.M.supportProj.mat + ρ.traceLeft.M.supportProj.mat).toEuclideanLin) + exact ker_kron_le_of_le _ _ _ _ + (by + simpa [HermitianMat.ker, HermitianMat.lin] using + (show ρ.traceRight.M.ker ≤ ρ.traceRight.M.supportProj.ker by simp)) + (by + simpa [HermitianMat.ker, HermitianMat.lin] using + (show ρ.traceLeft.M.ker ≤ ρ.traceLeft.M.supportProj.ker by simp))).trans hkerP + have right_mul_eq_of_fixed_support {Q ρM : HermitianMat (dA × dB) ℂ} + (hfix : ∀ x : EuclideanSpace ℂ (dA × dB), x ∈ ρM.support → Q.lin x = x) : + ρM.mat * Q.mat = ρM.mat := by + have hleft : Q.mat * ρM.mat = ρM.mat := by + rw [Matrix.ext_iff_mulVec] + intro v + have hv : WithLp.toLp 2 (ρM.mat.mulVec v) ∈ ρM.support := + Set.mem_range_self (WithLp.toLp 2 v) + simpa [Matrix.mulVec_mulVec, HermitianMat.lin, Matrix.toEuclideanLin] using hfix _ hv + simpa [Matrix.conjTranspose_mul, HermitianMat.conjTranspose_mat] using + congrArg Matrix.conjTranspose hleft + have inner_kron_support_right_eq (A : HermitianMat dA ℂ) : + ⟪ρ.M, A ⊗ₖ ρ.traceLeft.M.supportProj⟫ = ⟪ρ.M, A ⊗ₖ (1 : HermitianMat dB ℂ)⟫ := by + let Q : HermitianMat (dA × dB) ℂ := (1 : HermitianMat dA ℂ) ⊗ₖ ρ.traceLeft.M.supportProj + have hQ : ρ.M.mat * Q.mat = ρ.M.mat := by + apply right_mul_eq_of_fixed_support + intro x hx + simpa [Q] using fixed_support_kron_left ρ hx + have hmat : Q.mat * (A ⊗ₖ (1 : HermitianMat dB ℂ)).mat = + (A ⊗ₖ ρ.traceLeft.M.supportProj).mat := by + simp [Q, HermitianMat.kronecker_mat, ← Matrix.mul_kronecker_mul] + rw [HermitianMat.inner_eq_re_trace, HermitianMat.inner_eq_re_trace] + apply congrArg Complex.re + rw [← hmat, ← Matrix.mul_assoc, hQ] + have inner_support_kron_left_eq (B : HermitianMat dB ℂ) : + ⟪ρ.M, ρ.traceRight.M.supportProj ⊗ₖ B⟫ = ⟪ρ.M, (1 : HermitianMat dA ℂ) ⊗ₖ B⟫ := by + let Q : HermitianMat (dA × dB) ℂ := ρ.traceRight.M.supportProj ⊗ₖ (1 : HermitianMat dB ℂ) + have hQ : ρ.M.mat * Q.mat = ρ.M.mat := by + apply right_mul_eq_of_fixed_support + intro x hx + simpa [Q] using fixed_support_kron_right ρ hx + have hmat : Q.mat * ((1 : HermitianMat dA ℂ) ⊗ₖ B).mat = + (ρ.traceRight.M.supportProj ⊗ₖ B).mat := by + simp [Q, HermitianMat.kronecker_mat, ← Matrix.mul_kronecker_mul] + rw [HermitianMat.inner_eq_re_trace, HermitianMat.inner_eq_re_trace] + apply congrArg Complex.re + rw [← hmat, ← Matrix.mul_assoc, hQ] + rw [qRelativeEnt_ker prod_marginals_ker_le, qMutualInfo, + Sᵥₙ_eq_neg_trace_log, Sᵥₙ_eq_neg_trace_log, Sᵥₙ_eq_neg_trace_log] + rw [show (ρ.traceRight ⊗ᴹ ρ.traceLeft).M.log = + ρ.traceRight.M.log ⊗ₖ ρ.traceLeft.M.supportProj + + ρ.traceRight.M.supportProj ⊗ₖ ρ.traceLeft.M.log by + simpa [MState.prod] using + (HermitianMat.log_kron_with_proj (A := ρ.traceRight.M) (B := ρ.traceLeft.M)), + inner_sub_right, inner_add_right] + rw [show ⟪ρ.M.log, ρ.M⟫ = ⟪ρ.M, ρ.M.log⟫ by rw [HermitianMat.inner_comm]] + exact congrArg (fun x : ℝ => (x : EReal)) <| by + rw [show ⟪ρ.M, ρ.traceRight.M.log ⊗ₖ ρ.traceLeft.M.supportProj⟫ = + ⟪ρ.traceRight.M.log, ρ.traceRight.M⟫ by + calc + _ = ⟪ρ.M, ρ.traceRight.M.log ⊗ₖ (1 : HermitianMat dB ℂ)⟫ := + inner_kron_support_right_eq ρ.traceRight.M.log + _ = ⟪ρ.traceRight.M.log, ρ.traceRight.M⟫ := by + simpa [HermitianMat.inner_comm] using + inner_kron_one_eq_inner_traceRight ρ.traceRight.M.log ρ.M, + show ⟪ρ.M, ρ.traceRight.M.supportProj ⊗ₖ ρ.traceLeft.M.log⟫ = + ⟪ρ.traceLeft.M.log, ρ.traceLeft.M⟫ by + calc + _ = ⟪ρ.M, (1 : HermitianMat dA ℂ) ⊗ₖ ρ.traceLeft.M.log⟫ := + inner_support_kron_left_eq ρ.traceLeft.M.log + _ = ⟪ρ.traceLeft.M.log, ρ.traceLeft.M⟫ := by + simpa [HermitianMat.inner_comm] using + inner_one_kron_eq_inner_traceLeft ρ.traceLeft.M.log ρ.M] + ring /- Helper: If σ₂ ≤ α • σ₁ for density matrices, then α > 0. diff --git a/QuantumInfo/Finite/ResourceTheory/HypothesisTesting.lean b/QuantumInfo/Finite/ResourceTheory/HypothesisTesting.lean index c87c355d6..7f4333e31 100644 --- a/QuantumInfo/Finite/ResourceTheory/HypothesisTesting.lean +++ b/QuantumInfo/Finite/ResourceTheory/HypothesisTesting.lean @@ -431,7 +431,7 @@ theorem Ref81Lem5 (ρ σ : MState d) (ε : Prob) (hε : ε < 1) (α : ℝ) (hα rw [← hT₁] exact HermitianMat.inner_comm _ _ rw [hΦ₁, hΦ₂] - exact sandwichedRenyiEntropy_DPI_ax hα.le ρ σ Φ + exact sandwichedRenyiEntropy_DPI_of_one_le hα.le ρ σ Φ --If q = 1, this inequality is trivial by_cases hq₂ : q = 1 diff --git a/QuantumInfo/Finite/ResourceTheory/SteinsLemma.lean b/QuantumInfo/Finite/ResourceTheory/SteinsLemma.lean index b802ff7a3..8f7294b29 100644 --- a/QuantumInfo/Finite/ResourceTheory/SteinsLemma.lean +++ b/QuantumInfo/Finite/ResourceTheory/SteinsLemma.lean @@ -2139,10 +2139,7 @@ theorem limit_hypotesting_eq_limit_rel_entropy (ρ : MState (H i)) (ε : Prob) ( · exact RelativeEntResource.tendsto_ennreal ρ -- The regularized relative entropy of resource is not infinity /- -info: 'SteinsLemma.limit_hypotesting_eq_limit_rel_entropy' depends on axioms: [propext, - sandwichedRenyiEntropy_DPI_ax, - Classical.choice, - Quot.sound] +info: 'SteinsLemma.limit_hypotesting_eq_limit_rel_entropy' depends on axioms: [propext, Classical.choice, Quot.sound] -/ /- Commented out because of module system. diff --git a/QuantumInfo/ForMathlib/HermitianMat/Order.lean b/QuantumInfo/ForMathlib/HermitianMat/Order.lean index 7fe523973..0cacf9332 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Order.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Order.lean @@ -127,6 +127,28 @@ theorem kronecker_nonneg {A : HermitianMat m 𝕜} (hA : 0 ≤ A) (hB : 0 ≤ B) rw [zero_le_iff, kronecker_mat] classical exact (zero_le_iff.mp hA).PosSemidef_kronecker (zero_le_iff.mp hB) +/-- The self-Kronecker map `A ↦ A ⊗ₖ A` is monotone on nonnegative Hermitian matrices. -/ +theorem kronecker_self_mono (hA : 0 ≤ A) (hB : 0 ≤ B) (hAB : A ≤ B) : + A ⊗ₖ A ≤ B ⊗ₖ B := by + rw [← sub_nonneg] + have hAC : A ⊗ₖ B + -(A ⊗ₖ A) = A ⊗ₖ (B - A) := by + rw [show -(A ⊗ₖ A) = A ⊗ₖ (-A) by + symm + ext1 + simpa using (Matrix.kronecker_smul (-1 : 𝕜) A.mat A.mat)] + simpa [sub_eq_add_neg] using + (HermitianMat.kronecker_add (A := A) (B := B) (C := -A)).symm + have hEq : B ⊗ₖ B - A ⊗ₖ A = A ⊗ₖ (B - A) + (B - A) ⊗ₖ B := by + calc + B ⊗ₖ B - A ⊗ₖ A = (A + (B - A)) ⊗ₖ B - A ⊗ₖ A := by + rw [show A + (B - A) = B by abel] + _ = (A ⊗ₖ B + (B - A) ⊗ₖ B) - A ⊗ₖ A := by rw [HermitianMat.add_kronecker] + _ = (A ⊗ₖ B + -(A ⊗ₖ A)) + (B - A) ⊗ₖ B := by abel + _ = A ⊗ₖ (B - A) + (B - A) ⊗ₖ B := by rw [hAC] + simpa [hEq] using add_nonneg + (HermitianMat.kronecker_nonneg hA (sub_nonneg.mpr hAB)) + (HermitianMat.kronecker_nonneg (sub_nonneg.mpr hAB) hB) + /-- The Kronecker product of two positive Hermitian matrices is positive. -/ theorem kronecker_pos {A : HermitianMat m 𝕜} (hA : 0 < A) (hB : 0 < B) : 0 < A ⊗ₖ B := by apply lt_of_le_of_ne (kronecker_nonneg hA.le hB.le) @@ -484,6 +506,35 @@ theorem ker_le_of_le_smul {α : ℝ} [DecidableEq n] (hα : α ≠ 0) (hA : 0 rw [← ker_pos_smul B hα] exact ker_antitone hA hAB +/-- If a Hermitian matrix is bounded by `M * I`, then all its eigenvalues are at most `M`. -/ +theorem le_smul_one_imp_eigenvalues_le [DecidableEq n] (A : HermitianMat n ℂ) (M : ℝ) + (h : A ≤ M • (1 : HermitianMat n ℂ)) (i : n) : + A.H.eigenvalues i ≤ M := by + let v : n → ℂ := (A.H.eigenvectorBasis i).ofLp + have hv : star v ⬝ᵥ v = (1 : ℂ) := by + rw [show v = (A.H.eigenvectorBasis i).ofLp from rfl] + rw [dotProduct_comm, ← EuclideanSpace.inner_eq_star_dotProduct] + simp [A.H.eigenvectorBasis.orthonormal.1 i] + have hquad := (le_iff_mulVec_le_mulVec A (M • (1 : HermitianMat n ℂ))).mp h v + rw [show A.mat.mulVec v = (A.H.eigenvalues i : ℂ) • v from by + simpa [v] using A.H.mulVec_eigenvectorBasis i] at hquad + rw [dotProduct_smul, hv] at hquad + change (A.H.eigenvalues i : ℂ) • 1 ≤ + star v ⬝ᵥ ((M : ℂ) • (1 : Matrix n n ℂ)) *ᵥ v at hquad + have hquadC : (A.H.eigenvalues i : ℂ) ≤ (M : ℂ) := by + have hright : star v ⬝ᵥ ((M : ℂ) • (1 : Matrix n n ℂ)) *ᵥ v = (M : ℂ) := by + simpa [Matrix.smul_mulVec, hv] using (Algebra.algebraMap_eq_smul_one M).symm + simpa [Matrix.smul_mulVec, hv] using hquad.trans_eq hright + exact_mod_cast hquadC + +open MatrixOrder in +/-- If all eigenvalues of a Hermitian matrix are at most `M`, then it is bounded by `M * I`. -/ +theorem eigenvalues_le_imp_le_smul_one [DecidableEq n] (A : HermitianMat n ℂ) (M : ℝ) + (h : ∀ i, A.H.eigenvalues i ≤ M) : + A ≤ M • (1 : HermitianMat n ℂ) := by + simpa [HermitianMat.mat_one] using + (Matrix.PosSemidef.le_smul_one_of_eigenvalues_iff A.H M).mp h + --TODO: Positivity extensions for traceLeft, traceRight, rpow, nat powers, inverse function, -- the various `proj` function (in Proj.lean), and the inner product. diff --git a/QuantumInfo/ForMathlib/Matrix.lean b/QuantumInfo/ForMathlib/Matrix.lean index d640a2c1b..cb4befc0a 100644 --- a/QuantumInfo/ForMathlib/Matrix.lean +++ b/QuantumInfo/ForMathlib/Matrix.lean @@ -31,6 +31,18 @@ variable [RCLike 𝕜] [DecidableEq n] namespace Matrix +open scoped ComplexOrder MatrixOrder + +omit [DecidableEq n] in +/-- The block Gram matrix `[[YᴴY, YᴴX], [XᴴY, XᴴX]]` is positive semidefinite. -/ +theorem fromBlocks_gram_posSemidef {m n k : Type*} [Fintype m] [Fintype n] [Fintype k] + (X : Matrix k n ℂ) (Y : Matrix k m ℂ) : + (fromBlocks (Yᴴ * Y) (Yᴴ * X) (Xᴴ * Y) (Xᴴ * X)).PosSemidef := by + convert posSemidef_conjTranspose_mul_self + (fromBlocks Y X (0 : Matrix k m ℂ) (0 : Matrix k n ℂ)) using 1 + rw [fromBlocks_conjTranspose, fromBlocks_multiply] + simp + set_option backward.isDefEq.respectTransparency false in theorem zero_rank_eq_zero {A : Matrix n n 𝕜} [Fintype n] (hA : A.rank = 0) : A = 0 := by have h : ∀ v, A.mulVecLin v = 0 := by