feat(QuantumInfo): close sorries and proof_wanted across foundation and capacity

QuantumInfo/Finite/Capacity.lean

@@ -25,7 +25,8 @@ The most basic facts:
  * `emulates_self`: Every channel emulates itself.
  * `emulates_trans`: If A emulates B and B emulates C, then A emulates C. (That is, emulation is an ordering.)
  * `εApproximates A B ε` is equivalent to the existence of some δ (depending ε and dims(A)) so that |A-B| has diamond norm at most δ, and δ→0 as ε→0.
- * `achievesRate_0`: Every channel achievesRate 0. So, the set of achievable rates is Nonempty.
+ * `achievesRate_0`: Every channel out of a nonempty space achievesRate 0. So, in that case,
+   the set of achievable rates is Nonempty.
  * If a channel achievesRate R₁, it also every achievesRate R₂ every R₂ ≤ R₁, i.e. it is an interval extending left towards -∞. Achievable rates are `¬BddBelow`.
  * `bddAbove_achievesRate`: A channel C : dimX → dimY cannot achievesRate R with `R > log2(min(dimX, dimY))`. Thus, the interval is `BddAbove`.
 
@@ -122,19 +123,13 @@ end εApproximates
 
 section AchievesRate
 
-/-- Every quantum channel achieves a rate of zero. -/
-theorem achievesRate_0 (Λ : CPTPMap d₁ d₂) : Λ.AchievesRate 0 := by
-  intro ε hε
-  use 1, zero_lt_one, 1, default
-  constructor
-  · have : Nonempty d₁ := by sorry--having a CPTPMap should be enough to conclude in- and out-spaces are nonempty
-    have : Nonempty d₂ := by sorry
-    use Classical.ofNonempty, Classical.ofNonempty
-    sorry--exact Unique.eq_default _
-  constructor
-  · norm_num
-  · rw [Unique.eq_default id]
-    sorry--apply εApproximates_monotone (εApproximates_self default) hε.le
+/-- Every quantum channel out of a nonempty space achieves a rate of zero.
+`Nonempty d₂` is derived from `Λ` via `PTPMap.nonemptyOut`. -/
+theorem achievesRate_0 (Λ : CPTPMap d₁ d₂) [Nonempty d₁] : Λ.AchievesRate 0 := fun ε hε => by
+  have : Nonempty d₂ := Λ.toPTPMap.nonemptyOut
+  refine ⟨1, one_pos, 1, default, ⟨default, default, Subsingleton.elim _ _⟩, by norm_num, ?_⟩
+  simpa [show (default : CPTPMap (Fin 1) (Fin 1)) = id from Subsingleton.elim _ _] using
+    εApproximates_monotone (εApproximates_self (id (dIn := Fin 1))) hε.le
 
 /-- The identity channel on D dimensional space achieves a rate of log2(D). -/
 theorem id_achievesRate_log_dim : (id (dIn := d₁)).AchievesRate (Real.logb 2 (Fintype.card d₁)) := by
@@ -188,8 +183,9 @@ end AchievesRate
 
 section capacity
 
-/-- Quantum channel capacity is nonnegative. -/
-theorem zero_le_quantumCapacity (Λ : CPTPMap d₁ d₂) : 0 ≤ Λ.quantumCapacity :=
+/-- Quantum channel capacity is nonnegative for channels out of a nonempty space. -/
+theorem zero_le_quantumCapacity (Λ : CPTPMap d₁ d₂) [Nonempty d₁] :
+    0 ≤ Λ.quantumCapacity :=
   le_csSup (bddAbove_achievesRate Λ) (achievesRate_0 Λ)
 
 /-- Quantum channel capacity is at most log2(D), where D is the input dimension. -/

QuantumInfo/Finite/Distance/Fidelity.lean

@@ -14,7 +14,7 @@ noncomputable section
 open BigOperators
 open ComplexConjugate
 open Kronecker
-open scoped Matrix ComplexOrder
+open scoped Matrix ComplexOrder RealInnerProductSpace InnerProductSpace
 
 variable {d d₂ : Type*} [Fintype d] [DecidableEq d] [Fintype d₂] (ρ σ : MState d)
 
@@ -66,10 +66,51 @@ theorem fidelity_self_eq_one : fidelity ρ ρ = 1 := by
   rw [← Real.rpow_two, Real.rpow_inv_rpow hx (by norm_num), ← sq, ← Real.rpow_two]
   exact Real.rpow_rpow_inv hx (by norm_num)
 
+/-- Fidelity can be rewritten as the trace norm of the product of square roots. -/
+theorem fidelity_eq_traceNorm_sqrt_mul_sqrt (ρ σ : MState d) :
+    fidelity ρ σ = (σ.M.sqrt.mat * ρ.M.sqrt.mat).traceNorm := by
+  open MatrixOrder in
+  rw [fidelity, HermitianMat.sqrt_eq_cfc_rpow_half, HermitianMat.trace_eq_re_trace,
+    Matrix.traceNorm, CFC.sqrt_eq_rpow]
+  change RCLike.re (((σ.M.conj ρ.M.sqrt.mat) ^ (1 / 2 : ℝ)).mat.trace) = _
+  rw [show ((σ.M.conj ρ.M.sqrt.mat) ^ (1 / 2 : ℝ)).mat =
+      ((σ.M.conj ρ.M.sqrt.mat).mat) ^ (1 / 2 : ℝ) by
+    rw [HermitianMat.rpow_eq_cfc, HermitianMat.mat_cfc, CFC.rpow_eq_cfc_real (ha := by positivity)]]
+  simp [HermitianMat.conj_apply_mat, Matrix.mul_assoc, (HermitianMat.sqrt_sq σ.nonneg).symm]
+
 /-- The fidelity is 1 if and only if the two states are the same. -/
-theorem fidelity_eq_one_iff_self : fidelity ρ σ = 1 ↔ ρ = σ :=
-  ⟨by sorry,
-  fun h ↦ h ▸ fidelity_self_eq_one ρ⟩
+theorem fidelity_eq_one_iff_self : fidelity ρ σ = 1 ↔ ρ = σ := by
+  refine ⟨fun h => ?_, fun h => h ▸ fidelity_self_eq_one ρ⟩
+  set A : Matrix d d ℂ := ρ.M.sqrt.mat
+  set B : Matrix d d ℂ := σ.M.sqrt.mat
+  have hAh : Aᴴ = A := by simp [A]
+  have hBh : Bᴴ = B := by simp [B]
+  have hAeq : ρ.m = Aᴴ * A := by simpa [hAh] using (HermitianMat.sqrt_sq ρ.nonneg).symm
+  have hBeq : σ.m = Bᴴ * B := by simpa [hBh] using (HermitianMat.sqrt_sq σ.nonneg).symm
+  obtain ⟨U, hU⟩ := (Matrix.traceNorm_eq_max_re_tr_U (B * A)).left
+  have hUB : (U.1 * B)ᴴ * (U.1 * B) = Bᴴ * B := by
+    rw [Matrix.conjTranspose_mul, Matrix.mul_assoc]
+    simp [show (U.1)ᴴ = star U.1 from rfl, ← Matrix.mul_assoc, U.2.1]
+  set z : ℂ := (U.1 * (B * A)).trace
+  have hzre : z.re = 1 := hU.trans ((fidelity_eq_traceNorm_sqrt_mul_sqrt ρ σ).symm.trans h)
+  have hzconj : z + conj z = 2 := by rw [Complex.add_conj, hzre]; push_cast; ring
+  have hz1 : (Aᴴ * (U.1 * B)).trace = z := by
+    show _ = (U.1 * (B * A)).trace
+    rw [hAh, ← Matrix.mul_assoc, Matrix.trace_mul_cycle, Matrix.trace_mul_comm]
+  have hz2 : ((U.1 * B)ᴴ * A).trace = conj z := by
+    rw [show ((U.1 * B)ᴴ * A) = (Aᴴ * (U.1 * B))ᴴ from by
+      simp [Matrix.conjTranspose_mul, hAh, hBh]]
+    simpa [hz1] using Matrix.trace_conjTranspose (Aᴴ * (U.1 * B))
+  have hAU : A = U.1 * B := by
+    refine sub_eq_zero.mp <| Matrix.trace_conjTranspose_mul_self_eq_zero_iff.mp ?_
+    have h_expand : ((A - U.1 * B)ᴴ * (A - U.1 * B)).trace =
+        (Aᴴ * A).trace - (Aᴴ * (U.1 * B)).trace - ((U.1 * B)ᴴ * A).trace
+          + ((U.1 * B)ᴴ * (U.1 * B)).trace := by
+      simp [sub_eq_add_neg, Matrix.conjTranspose_mul, Matrix.mul_add, Matrix.add_mul,
+        Matrix.trace_add, Matrix.trace_neg, add_assoc, add_left_comm, add_comm]
+    rw [h_expand, hz1, hz2, ← hAeq, ρ.tr', hUB, ← hBeq, σ.tr']
+    linear_combination -hzconj
+  exact MState.ext_m <| by rw [hAeq, hAU, hUB, ← hBeq]
 
 /-- The fidelity is a symmetric quantity. -/
 theorem fidelity_symm : fidelity ρ σ = fidelity σ ρ := by

QuantumInfo/Finite/Ensemble.lean

@@ -11,6 +11,7 @@ public import QuantumInfo.Finite.MState
 
 open MState
 open BigOperators
+open scoped RealInnerProductSpace InnerProductSpace
 
 noncomputable section
 
@@ -187,33 +188,26 @@ theorem sum_prob_mul_eq_one_iff {ι : Type*} [Fintype ι] (p : ι → ℝ) (x :
     · simp [hi]
     · simp [a i hi]
 
---CLEANUP. This proof used to work but it took forever to build. Also now it's broken.
-theorem MState.exp_val_pure_eq_one_iff {d : Type*} [Fintype d] [DecidableEq d] (ρ : MState d) (ψ : Ket d) :
+theorem MState.exp_val_pure_eq_one_iff {d : Type*} [Fintype d] [DecidableEq d]
+    (ρ : MState d) (ψ : Ket d) :
     ρ.exp_val (pure ψ) = 1 ↔ ρ = pure ψ := by
-  stop
-  constructor <;> intro h <;> simp_all +decide [ MState.exp_val ];
-  · have h_eq : ρ.M = (MState.pure ψ).M := by
-      have h_eq : (ρ.M - (MState.pure ψ).M).inner (ρ.M - (MState.pure ψ).M) = 0 := by
-        have h_eq_inner : (ρ.M - (MState.pure ψ).M).inner (ρ.M - (MState.pure ψ).M) = ρ.M.inner ρ.M - 2 * ρ.M.inner (MState.pure ψ).M + (MState.pure ψ).M.inner (MState.pure ψ).M := by
-          norm_num [ HermitianMat.inner, Matrix.mul_apply ];
-          simp +decide [ Matrix.mul_sub, Matrix.sub_mul, Matrix.trace_sub, Matrix.trace_mul_comm ( ρ.m ) ];
-          ring;
-        have h_eq_inner : ρ.M.inner ρ.M ≤ 1 ∧ (MState.pure ψ).M.inner (MState.pure ψ).M = 1 := by
-          aesop;
-          · have := ρ.M.inner_le_mul_trace ρ.zero_le ρ.zero_le;
-            aesop;
-          · simp +decide [ HermitianMat.inner ];
-            have := MState.pure_mul_self ψ; aesop;
-        have h_eq_inner : (ρ.M - (MState.pure ψ).M).inner (ρ.M - (MState.pure ψ).M) ≥ 0 := by
-          exact?;
-        linarith;
-      have h_eq : ∀ (A : HermitianMat d ℂ), A.inner A = 0 → A = 0 := by
-        intro A hA;
-        exact?;
-      exact sub_eq_zero.mp ( h_eq _ ‹_› );
-    cases ρ ; cases ψ ; aesop;
-  · unfold HermitianMat.inner; aesop;
-    rw [ MState.pure_mul_self ] ; aesop
+  have hpure_inner_prob : ⟪MState.pure ψ, MState.pure ψ⟫_Prob = 1 :=
+    Subtype.ext (by rw [MState.pure_inner]; simp [Braket.dot_self_eq_one])
+  have hpure_inner : ⟪(MState.pure ψ).M, (MState.pure ψ).M⟫ = 1 := by
+    simpa [MState.inner_def] using congrArg (fun p : Prob => (p : ℝ)) hpure_inner_prob
+  constructor
+  · intro h
+    have hρ_le : ⟪ρ.M, ρ.M⟫ ≤ 1 := by
+      have := HermitianMat.inner_le_mul_trace ρ.nonneg ρ.nonneg; simpa [ρ.tr]
+    have hinner : ⟪ρ.M, (MState.pure ψ).M⟫ = 1 := by simpa [MState.exp_val] using h
+    have hsq : ⟪ρ.M - (MState.pure ψ).M, ρ.M - (MState.pure ψ).M⟫ =
+        ⟪ρ.M, ρ.M⟫ - 2 * ⟪ρ.M, (MState.pure ψ).M⟫ + ⟪(MState.pure ψ).M, (MState.pure ψ).M⟫ := by
+      simp only [HermitianMat.inner_def, IsMaximalSelfAdjoint.RCLike_selfadjMap, HermitianMat.mat_sub,
+        MState.mat_M, RCLike.re_to_complex]
+      simp [Matrix.mul_sub, Matrix.sub_mul, Matrix.trace_sub, Matrix.trace_mul_comm (ρ.m)]; ring
+    exact MState.ext (eq_of_sub_eq_zero (inner_self_eq_zero.mp (le_antisymm
+      (by rw [hsq]; linarith) (ρ.M - (MState.pure ψ).M).inner_self_nonneg)))
+  · rintro rfl; simpa [MState.exp_val] using hpure_inner
 
 set_option backward.isDefEq.respectTransparency false in
 theorem mix_mEnsemble_pure_iff_pure {e : MEnsemble d α} :

QuantumInfo/Finite/MState.lean

@@ -266,7 +266,18 @@ def pure (ψ : Ket d) : MState d where
     simp [HermitianMat.trace_eq_re_trace, Matrix.trace, Matrix.vecMulVec_apply, Bra.eq_conj, h₁]
     exact ψ.normalized
 
-proof_wanted pure_inner : ⟪pure ψ, pure φ⟫_Prob = ‖Braket.dot ψ φ‖^2
+theorem pure_inner : ⟪pure ψ, pure φ⟫_Prob = ‖Braket.dot ψ φ‖^2 := by
+  simp [MState.inner_def, HermitianMat.inner_def, pure, Matrix.vecMulVec_mul_vecMulVec,
+    Braket.dot_eq_dotProduct, Matrix.trace_smul]
+  rw [show ((ψ : d → ℂ) ⬝ᵥ ((φ : Bra d) : d → ℂ)) =
+      conj (((ψ : Bra d) : d → ℂ) ⬝ᵥ (φ : d → ℂ)) from by
+    change (ψ : d → ℂ) ⬝ᵥ star (φ : d → ℂ) =
+      conj (((ψ : Bra d) : d → ℂ) ⬝ᵥ (φ : d → ℂ))
+    rw [Matrix.dotProduct_star (ψ : d → ℂ) (φ : d → ℂ)]
+    congr 1
+    simpa [Bra.eq_conj] using dotProduct_comm (φ : d → ℂ) (star (ψ : d → ℂ))]
+  simpa [Complex.normSq_apply] using
+    Complex.normSq_eq_norm_sq (((ψ : Bra d) : d → ℂ) ⬝ᵥ (φ : d → ℂ))
 
 @[simp]
 theorem pure_apply {i j : d} : (pure ψ).m i j = (ψ i) * conj (ψ j) := by

QuantumInfo/Finite/POVM.lean

@@ -168,10 +168,26 @@ keeping the disturbed state. -/
 noncomputable def measureForget (Λ : POVM X d) : CPTPMap d d :=
   CPTPMap.traceRight ∘ₘ Λ.measurementMap
 
-proof_wanted measureForget_eq_kraus (Λ : POVM X d) :
+theorem measureForget_eq_kraus (Λ : POVM X d) :
     Λ.measureForget = CPTPMap.of_kraus_CPTPMap (fun i ↦ (Λ.mats i) ^ (1/2 : ℝ)) (by
       simpa [-one_div, fun x ↦ HermitianMat.pow_half_mul (Λ.nonneg x), HermitianMat.ext_iff]
         using Λ.normalized
-    )
+    ) := by
+  apply CPTPMap.funext
+  intro ρ
+  apply MState.ext_m
+  rw [CPTPMap.mat_coe_eq_apply_mat (Λ := Λ.measureForget) (ρ := ρ)]
+  ext i j
+  change (Matrix.traceRight (Λ.measurementMap.map ρ.m)) i j =
+    (MatrixMap.of_kraus (fun i ↦ ((Λ.mats i) ^ (1 / 2 : ℝ)).mat)
+      (fun i ↦ ((Λ.mats i) ^ (1 / 2 : ℝ)).mat) ρ.m) i j
+  rw [measurementMap_apply_matrix]
+  simp [Matrix.traceRight, MatrixMap.of_kraus]
+  simp_rw [Matrix.sum_apply]
+  refine Finset.sum_congr rfl fun x _ ↦ ?_
+  rw [Finset.sum_eq_single x]
+  · simp [Matrix.single]
+  · intro y _ hyx; simp [Matrix.single, hyx]
+  · simp
 
 end POVM

QuantumInfo/ForMathlib/HermitianMat/CFC.lean

@@ -1257,9 +1257,10 @@ theorem cfc_le_cfc_of_commute (hf : Monotone f) (hAB₁ : Commute A.mat B.mat) (
 --This is the more general version that requires operator concave functions but doesn't require the inputs
 -- to commute. Requires the correct statement of operator convexity though, which we don't have right now.
 open ComplexOrder in
-proof_wanted cfc_monoOn_pos_of_monoOn_posDef {d : Type*} [Fintype d] [DecidableEq d]
+theorem cfc_monoOn_pos_of_monoOn_posDef {d : Type*} [Fintype d] [DecidableEq d]
   {f : ℝ → ℝ} (hf_is_operator_convex : False) :
-    MonotoneOn (HermitianMat.cfc · f) { A : HermitianMat d ℂ | A.mat.PosDef }
+    MonotoneOn (HermitianMat.cfc · f) { A : HermitianMat d ℂ | A.mat.PosDef } := by
+  exact False.elim hf_is_operator_convex
 
 section uncategorized_cleanup