Fix warnings and proved DMChannel.on_fin and conj_unitary_eigenvalue_equiv

ClassicalInfo/Channel.lean

@@ -49,22 +49,23 @@ def product : Channel (A × C) (B × D) :=
  output distribution `Distribution O`, and this process is applied
  independently on each symbol in the list. -/
 structure DMChannel where
-  symb_dist : I → Distribution O
+  symb_dist : I → ProbDistribution O
 
 namespace DMChannel
 
 /-- Apply a discrete memoryless channel to an n-character string. -/
-def on_fin (C : DMChannel I O) {n : ℕ} (is : Fin n → I) : Distribution (Fin n → O) :=
-  ⟨fun os ↦ ∏ k, C.symb_dist (is k) (os k), by
-    -- change ∑ os in Fintype.piFinset fun x => (Finset.univ : Finset O), ∏ k : Fin n, ((C.symb_dist (is k)) (os k) : ℝ) = 1
-    -- have : ∀i, Finset.sum Finset.univ (C.symb_dist i) = 1 :=
-    --   fun i ↦ Distribution.prop <| C.symb_dist i
-    -- rw [Finset.sum_prod_piFinset]
-    -- simp [this]
-    sorry⟩
+def on_fin (C : DMChannel I O) {n : ℕ} (is : Fin n → I) : ProbDistribution (Fin n → O) :=
+  ProbDistribution.mk' (fun os ↦ ∏ k, (C.symb_dist (is k) (os k) : ℝ))
+    (fun _ ↦ Finset.prod_nonneg fun k _ ↦ Prob.zero_le_coe)
+    (by
+      have h := Finset.sum_prod_piFinset (Finset.univ : Finset O)
+        (fun (k : Fin n) (j : O) ↦ ((C.symb_dist (is k)) j : ℝ))
+      simp only [Fintype.piFinset_univ] at h
+      simp only [h]
+      exact Finset.prod_eq_one fun k _ ↦ ProbDistribution.normalized (C.symb_dist (is k)))
 
 /-- Apply a discrete memoryless channel to a list. -/
-def on_list (C : DMChannel I O) (is : List I) : Distribution (Fin (is.length) → O) :=
-  C.on_fin is.get
+def on_list (C : DMChannel I O) (is : List I) : ProbDistribution (Fin (is.length) → O) :=
+  on_fin I O C is.get
 
 end DMChannel

QuantumInfo/Finite/CPTPMap/Dual.lean

@@ -54,7 +54,8 @@ theorem _root_.Matrix.PosSemidef.trace_mul_nonneg {n : Type*} [Fintype n] [Decid
     0 ≤ (A * B).trace := by
   open scoped Matrix in
   obtain ⟨sqrtB, rfl⟩ : ∃ sqrtB : Matrix n n 𝕜, B = sqrtBᴴ * sqrtB := by
-    exact Matrix.posSemidef_iff_eq_conjTranspose_mul_self.mp hB;
+    open MatrixOrder in
+    exact CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hB.nonneg
   simp only [← Matrix.mul_assoc, ← Matrix.trace_mul_comm sqrtB]
   have h : (sqrtB * A * sqrtBᴴ).PosSemidef := by
     convert hA.conjTranspose_mul_mul_same sqrtBᴴ using 1

QuantumInfo/Finite/CPTPMap/Unbundled.lean

@@ -352,10 +352,12 @@ theorem kron_kronecker_const {C : Matrix d d R} (h : C.PosSemidef) {h₁ h₂ :
   intros n x hx
   have h_kronecker_pos : (x ⊗ₖ C).PosSemidef := by
     -- Since $x$ and $C$ are positive semidefinite, there exist matrices $U$ and $V$ such that $x = U^*U$ and $C = V^*V$.
-    obtain ⟨U, hU⟩ : ∃ U : Matrix (A × Fin n) (A × Fin n) R, x = star U * U :=
-      Matrix.posSemidef_iff_eq_conjTranspose_mul_self.mp hx
-    obtain ⟨V, hV⟩ : ∃ V : Matrix d d R, C = star V * V :=
-      Matrix.posSemidef_iff_eq_conjTranspose_mul_self.mp h
+    obtain ⟨U, hU⟩ : ∃ U : Matrix (A × Fin n) (A × Fin n) R, x = star U * U := by
+      classical
+      open MatrixOrder in exact CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx.nonneg
+    obtain ⟨V, hV⟩ : ∃ V : Matrix d d R, C = star V * V := by
+      classical
+      open MatrixOrder in exact CStarAlgebra.nonneg_iff_eq_star_mul_self.mp h.nonneg
     -- $W = (U \otimes V)^* (U \otimes V)$ is positive semidefinite.
     have hW_pos : (U ⊗ₖ V).conjTranspose * (U ⊗ₖ V) = x ⊗ₖ C := by
       rw [Matrix.kroneckerMap_conjTranspose, ← Matrix.mul_kronecker_mul]
@@ -596,7 +598,9 @@ theorem conj_isCompletelyPositive (M : Matrix B A R) : (conj M).IsCompletelyPosi
       simp +contextual [ eq_comm ];
     simp only [ h_inner ];
     simpa only [ mul_assoc, mul_comm, mul_left_comm ] using h_reindex
-  obtain ⟨m', rfl⟩ := Matrix.posSemidef_iff_eq_conjTranspose_mul_self.mp h
+  obtain ⟨m', rfl⟩ := by
+    classical
+    open MatrixOrder in exact CStarAlgebra.nonneg_iff_eq_star_mul_self.mp h.nonneg
   convert Matrix.posSemidef_conjTranspose_mul_self (m' * (M ⊗ₖ 1 : Matrix (B × Fin n) (A × Fin n) R).conjTranspose) using 1
   simp only [Matrix.conjTranspose_mul, Matrix.conjTranspose_conjTranspose, Matrix.mul_assoc]
   rw [Matrix.mul_assoc, Matrix.mul_assoc]

QuantumInfo/Finite/POVM.lean

@@ -112,7 +112,7 @@ theorem measurementMap_apply_hermitianMat (Λ : POVM X d) (m : HermitianMat d 
   congr!
   ext i j
   simp only [HermitianMat.diagonal, mat_mk, diagonal_apply, single, of_apply]
-  split_ifs <;> (try grind) <;> norm_num
+  split_ifs <;> grind
 
 /-- A POVM leads to a distribution of outcomes on any given mixed state ρ. -/
 def measure (Λ : POVM X d) (ρ : MState d) : ProbDistribution X := .mk'

QuantumInfo/ForMathlib/ContinuousLinearMap.lean

@@ -3,10 +3,8 @@ Copyright (c) 2025 Alex Meiburg. All rights reserved.
 Released under MIT license as described in the file LICENSE.
 Authors: Alex Meiburg
 -/
---For the first three lemmas
 import Mathlib.Topology.Algebra.Module.LinearMap
 
---For the third lemma
 import Mathlib.Analysis.CStarAlgebra.Classes
 import Mathlib.Analysis.InnerProductSpace.Spectrum
 import Mathlib.Order.CompletePartialOrder
@@ -17,16 +15,6 @@ variable {R S : Type*} [Semiring R] [Semiring S] (σ : R →+* S) (M M₂ : Type
 variable [TopologicalSpace M] [AddCommMonoid M] [TopologicalSpace M₂] [AddCommMonoid M₂]
 variable [Module R M] [Module S M₂]
 
---These two theorems might look a bit silly as aliases of `LinearMap.____`, but they don't `simp` on their
---TODO: I think we can remove these now that we've bumped to Lean 4.28.0
-@[simp]
-theorem range_zero [RingHomSurjective σ] : (0 : M →SL[σ] M₂).range = ⊥ := by
-  simp
-
-@[simp]
-theorem ker_zero : (0 : M →SL[σ] M₂).ker = ⊤ := by
-  simp
-
 theorem ker_mk (f : M →ₛₗ[σ] M₂) (hf : Continuous f.toFun) :
     (ContinuousLinearMap.mk f hf).ker = LinearMap.ker f := by
   rfl

QuantumInfo/ForMathlib/HermitianMat/Basic.lean

@@ -726,7 +726,7 @@ theorem conj_ne_zero {A : HermitianMat d 𝕜} {M : Matrix d₂ d 𝕜} (hA : A
 theorem conj_ne_zero_iff {A : HermitianMat d 𝕜} {M : Matrix d₂ d 𝕜}
     (h : LinearMap.ker M.toEuclideanLin ≤ A.ker) : A.conj M ≠ 0 ↔ A ≠ 0  := by
   refine ⟨?_, (conj_ne_zero · h)⟩
-  intro h rfl; simp at h--should be grind[= map_zero] but I don't know why. TODO.
+  intro h rfl; grind
 
 section spectrum
 

QuantumInfo/ForMathlib/HermitianMat/Inner.lean

@@ -243,7 +243,7 @@ private theorem inner_zero_iff_aux_lemma [DecidableEq n] (hA₁ : A.mat.PosSemid
             simp_all only [Matrix.zero_apply, map_zero, mul_zero, add_zero, Finset.sum_const_zero]
         exact h_trace_zero_iff _;
       convert h_trace_zero_iff using 3
-      simp [ hC, hD, Matrix.mul_assoc ];
+      simp [ Matrix.mul_assoc ];
       rw [ ← Matrix.trace_mul_comm ]
       have h_trace_cyclic : Matrix.trace (D.conjTranspose * D * C.conjTranspose * C) = Matrix.trace (C * D.conjTranspose * D * C.conjTranspose) := by
         rw [ ← Matrix.trace_mul_comm ]
@@ -269,7 +269,7 @@ private theorem inner_zero_iff_aux_lemma [DecidableEq n] (hA₁ : A.mat.PosSemid
       ext i j
       specialize hAB_zero (EuclideanSpace.single j 1)
       have h1 := hAB_zero
-      simp only [LinearMap.mem_ker, Matrix.toEuclideanLin, Matrix.toLpLin_apply, Matrix.mulVec_mulVec] at h1
+      simp only [Matrix.toEuclideanLin, Matrix.toLpLin_apply, Matrix.mulVec_mulVec] at h1
       have h2 := congr_fun (congrArg WithLp.ofLp h1) i
       simp only [WithLp.ofLp_toLp, WithLp.ofLp_zero, EuclideanSpace.single] at h2
       simpa [Matrix.mul_apply, Matrix.mulVec, dotProduct, Pi.single_apply] using h2
@@ -495,8 +495,7 @@ theorem norm_one : ‖(1 : HermitianMat d 𝕜)‖ = √(Fintype.card d : ℝ) :
   rw [norm_eq_sqrt_real_inner (F := HermitianMat d 𝕜)]
   congr 1
   simp only [inner_def, mat_one, Matrix.one_apply, Matrix.trace, Matrix.diag_apply,
-    Matrix.mul_apply, star_one, one_mul, Finset.sum_ite_eq', Finset.mem_univ, ↑reduceIte,
-    map_one, Finset.sum_const, Finset.card_univ, smul_eq_mul, mul_one]
+    ↑reduceIte, Finset.sum_const, Finset.card_univ, mul_one]
   simp [selfadjMap]
 
 theorem norm_eq_trace_sq : ‖A‖ ^ 2 = (A.mat ^ 2).trace := by

QuantumInfo/ForMathlib/HermitianMat/Jordan.lean

@@ -130,8 +130,8 @@ scoped instance : NonUnitalNonAssocRing (HermitianMat d 𝕜) where
 
 variable [Invertible (2 : 𝕜)] [DecidableEq d]
 
---TODO: Upgrade this to NonAssocCommRing, see #28604 in Mathlib
-scoped instance : NonAssocRing (HermitianMat d 𝕜) where
+scoped instance : NonAssocCommRing (HermitianMat d 𝕜) where
+  mul_comm := HermitianMat.symmMul_comm
 
 end field
 

QuantumInfo/ForMathlib/HermitianMat/LogExp.lean

@@ -135,8 +135,9 @@ The inverse function is operator antitone for positive definite matrices.
 open ComplexOrder in
 theorem inv_antitone (hA : A.mat.PosDef) (h : A ≤ B) : B⁻¹ ≤ A⁻¹ := by
   -- Since $B - A$ is positive semidefinite, we can write it as $C^*C$ for some matrix $C$.
-  obtain ⟨C, hC⟩ : ∃ C : Matrix d d 𝕜, B.mat - A.mat = C.conjTranspose * C :=
-    Matrix.posSemidef_iff_eq_conjTranspose_mul_self.mp h
+  obtain ⟨C, hC⟩ : ∃ C : Matrix d d 𝕜, B.mat - A.mat = C.conjTranspose * C := by
+    open MatrixOrder in
+    exact CStarAlgebra.nonneg_iff_eq_star_mul_self.mp (le_iff.mp h).nonneg
   -- Using the fact that $B = A + C^*C$, we can write $B^{-1}$ as $(A + C^*C)^{-1}$.
   have h_inv_posDef : (1 + C * A.mat⁻¹ * C.conjTranspose).PosDef := by
     exact Matrix.PosDef.one.add_posSemidef (hA.inv.posSemidef.mul_mul_conjTranspose_same C)

QuantumInfo/ForMathlib/HermitianMat/NonSingular.lean

@@ -100,7 +100,7 @@ theorem nonSingular_iff_ker_bot : NonSingular A ↔ A.ker = ⊥ := by
     have hm : (WithLp.toLp 2 y) ∈ A.ker := (mem_ker_iff_mulVec_zero A _).mpr hy
     rw [h] at hm
     have := (Submodule.mem_bot (R := 𝕜)).mp hm
-    simp [WithLp.toLp] at this
+    simp at this
     exact this
   specialize @h_inj x 0
   simp_all

QuantumInfo/ForMathlib/HermitianMat/Proj.lean

@@ -94,15 +94,15 @@ theorem projector_eq_sum_rankOne (b : OrthonormalBasis ι 𝕜 S) :
   unfold projector;
   ext i j;
   field_simp;
-  simp +decide [ Matrix.vecMulVec, LinearMap.toMatrix_apply ];
+  simp +decide [ Matrix.vecMulVec ];
   -- By definition of orthogonal projection, we can write the projection of $e_j$ onto $S$ as $\sum_{k} \langle e_j, b_k \rangle b_k$.
   have h_proj : ∀ j : n, S.orthogonalProjection (EuclideanSpace.single j 1) = ∑ k, (star (b k |>.1 j)) • (b k |>.1) := by
     intro j
     have h_proj : S.orthogonalProjection (EuclideanSpace.single j 1) = ∑ k, (inner 𝕜 (b k |>.1) (EuclideanSpace.single j 1)) • (b k |>.1) := by
       convert b.sum_repr ( S.orthogonalProjection ( EuclideanSpace.single j 1 ) ) using 1;
       constructor <;> intro h <;> simp_all +decide [ Subtype.ext_iff, b.repr_apply_apply ];
-    convert h_proj using 3 ; simp +decide [ inner, EuclideanSpace.inner_single_right ];
-  convert congr_arg ( fun x : EuclideanSpace ( _ ) n => x i ) ( h_proj j ) using 1 <;> simp +decide [ LinearMap.toMatrix_apply, Matrix.mulVec, dotProduct ];
+    convert h_proj using 3 ; simp +decide [ inner ];
+  convert congr_arg ( fun x : EuclideanSpace ( _ ) n => x i ) ( h_proj j ) using 1 ; simp +decide;
   simp +decide [ Matrix.sum_apply, mul_comm ]
 
 /--
@@ -116,32 +116,32 @@ lemma projector_support_eq_sum : A.supportProj.mat =
     · intro x hx;
       -- By definition of $A.support$, we know that $x$ is in the orthogonal complement of the kernel of $A$.
       have h_orthogonal_complement : x ∈ (A.ker : Submodule (𝕜) (EuclideanSpace (𝕜) n))ᗮ := by
-        convert hx using 1;
-        exact?;
+        convert hx using 1
+        exact ker_orthogonal_eq_support A
       -- By definition of $A.ker$, we know that $x$ is orthogonal to all eigenvectors with zero eigenvalues.
       have h_orthogonal_zero_eigenvalues : ∀ i, A.H.eigenvalues i = 0 → inner (𝕜) (A.H.eigenvectorBasis i) x = 0 := by
         intro i hi
         have h_eigenvector_zero : A.mat.mulVec (A.H.eigenvectorBasis i) = 0 := by
           have := A.H.mulVec_eigenvectorBasis i; aesop;
-        convert h_orthogonal_complement ( A.H.eigenvectorBasis i ) _ using 1;
-        exact?;
+        convert h_orthogonal_complement ( A.H.eigenvectorBasis i ) _ using 1
+        exact (mem_ker_iff_mulVec_zero A ((H A).eigenvectorBasis i)).mpr h_eigenvector_zero
       -- By definition of $A.ker$, we know that $x$ can be written as a linear combination of eigenvectors with non-zero eigenvalues.
       have h_decomp : x = ∑ i, (inner (𝕜) (A.H.eigenvectorBasis i) x) • A.H.eigenvectorBasis i := by
-        exact?;
+        exact Eq.symm (OrthonormalBasis.sum_repr' (H A).eigenvectorBasis x)
       rw [ h_decomp ];
-      exact Submodule.sum_mem _ fun i _ => if hi : A.H.eigenvalues i = 0 then by simp +decide [ hi, h_orthogonal_zero_eigenvalues i hi ] else Submodule.smul_mem _ _ ( Submodule.subset_span ⟨ i, hi, rfl ⟩ );
+      exact Submodule.sum_mem _ fun i _ => if hi : A.H.eigenvalues i = 0 then by simp +decide [ h_orthogonal_zero_eigenvalues i hi ] else Submodule.smul_mem _ _ ( Submodule.subset_span ⟨ i, hi, rfl ⟩ );
     · rw [ Submodule.span_le, Set.image_subset_iff ];
       intro i hi;
       simp_all +decide [ HermitianMat.support ];
       use (1 / A.H.eigenvalues i) • A.H.eigenvectorBasis i;
-      convert congr_arg ( fun x => ( 1 / A.H.eigenvalues i ) • x ) ( A.H.mulVec_eigenvectorBasis i ) using 1 ; simp +decide [ hi, Matrix.mulVec_smul ];
-      simp +decide [ funext_iff, Matrix.mulVec, dotProduct ];
-      exact?;
+      convert congr_arg ( fun x => ( 1 / A.H.eigenvalues i ) • x ) ( A.H.mulVec_eigenvectorBasis i ) using 1 ; simp +decide [ hi ];
+      simp +decide [ funext_iff, Matrix.mulVec, dotProduct ]
+      exact PiLp.ext_iff
   have h_orthonormal_basis : ∃ b : OrthonormalBasis {i : n | A.H.eigenvalues i ≠ 0} (𝕜) (Submodule.span (𝕜) (Set.image (fun i => A.H.eigenvectorBasis i) {i | A.H.eigenvalues i ≠ 0})), ∀ i, b i = A.H.eigenvectorBasis i := by
     refine' ⟨ _, _ ⟩;
     refine' OrthonormalBasis.mk _ _;
     use fun i => ⟨ A.H.eigenvectorBasis i, Submodule.subset_span ( Set.mem_image_of_mem _ i.2 ) ⟩;
-    all_goals simp +decide [ Orthonormal, Subtype.ext_iff ];
+    all_goals simp +decide [ Orthonormal ];
     · intro i j hij; have := A.H.eigenvectorBasis.orthonormal; simp_all +decide [ orthonormal_iff_ite ] ;
       exact fun h => hij <| Subtype.ext h;
     · rw [ Submodule.eq_top_iff' ];

QuantumInfo/ForMathlib/HermitianMat/Schatten.lean

@@ -42,12 +42,12 @@ lemma schattenNorm_nonneg (A : Matrix d d ℂ) (p : ℝ) :
     0 ≤ schattenNorm A p := by
   by_cases hp : p = 0 <;> simp +decide [ *, schattenNorm ];
   by_cases h₁ : 0 ≤ RCLike.re ( Matrix.trace ( Matrix.IsHermitian.cfc ( Matrix.isHermitian_mul_conjTranspose_self A.conjTranspose ) fun x => x ^ ( p / 2 ) ) ) <;> simp_all +decide [ Real.rpow_nonneg ];
-  contrapose! h₁; simp_all +decide [ mul_comm, Matrix.trace ] ; ring_nf; norm_num [ Real.exp_nonneg, Real.log_nonneg ] ; (
+  contrapose! h₁; simp_all +decide [ Matrix.trace ] ; ring_nf; norm_num [ Real.exp_nonneg, Real.log_nonneg ] ; (
   refine' Finset.sum_nonneg fun i _ => _ ; norm_num [ Matrix.IsHermitian.cfc ] ; ring_nf ; norm_num [ Real.exp_nonneg, Real.log_nonneg ] ; (
   simp +decide [ Matrix.mul_apply, Matrix.diagonal ] ; ring_nf ; norm_num [ Real.exp_nonneg, Real.log_nonneg ] ; (
-  exact Finset.sum_nonneg fun _ _ => add_nonneg ( mul_nonneg ( sq_nonneg _ ) ( Real.rpow_nonneg ( by
-    exact? ) _ ) ) ( mul_nonneg ( Real.rpow_nonneg ( by
-    exact? ) _ ) ( sq_nonneg _ ) ))));
+  exact Finset.sum_nonneg fun _ _ => add_nonneg ( mul_nonneg ( sq_nonneg _ ) ( Real.rpow_nonneg (
+    Matrix.eigenvalues_conjTranspose_mul_self_nonneg A _) _ ) ) ( mul_nonneg ( Real.rpow_nonneg (
+    Matrix.eigenvalues_conjTranspose_mul_self_nonneg A _) _ ) ( sq_nonneg _ ) ))));
 
 lemma schattenNorm_pow_eq
   (A : HermitianMat d ℂ) (hA : 0 ≤ A) (p k : ℝ) (hp : 0 < p) (hk : 0 < k) :
@@ -97,9 +97,9 @@ For nonneg eigenvalue λ and p > 0, (√λ)^p = λ^{p/2}.
 PROVIDED SOLUTION
 We have √y = y^{1/2} (by Real.sqrt_eq_rpow). So (√y)^p = (y^{1/2})^p = y^{(1/2)·p} = y^{p/2} by Real.rpow_mul (since y ≥ 0). Use rw [Real.sqrt_eq_rpow, ← Real.rpow_mul hy]; ring_nf.
 -/
-lemma sqrt_rpow_eq_rpow_half {y p : ℝ} (hy : 0 ≤ y) (hp : 0 < p) :
+lemma sqrt_rpow_eq_rpow_half {y p : ℝ} (hy : 0 ≤ y) (_hp : 0 < p) :
     Real.sqrt y ^ p = y ^ (p / 2) := by
-  rw [ Real.sqrt_eq_rpow, ← Real.rpow_mul hy ] ; ring
+  rw [ Real.sqrt_eq_rpow, ← Real.rpow_mul hy ] ; ring_nf
 
 /-
 PROBLEM
@@ -129,7 +129,7 @@ lemma schattenNorm_rpow_eq_sum_singularValues (A : Matrix d d ℂ) {p : ℝ} (hp
   · convert schattenNorm_trace_as_eigenvalue_sum A p using 1
     generalize_proofs at *;
     refine' Finset.sum_congr rfl fun i _ => _;
-    unfold singularValues; rw [ Real.sqrt_eq_rpow, ← Real.rpow_mul ( _ ) ] ; ring;
+    unfold singularValues; rw [ Real.sqrt_eq_rpow, ← Real.rpow_mul ( _ ) ] ; ring_nf;
     simp +zetaDelta at *;
     exact Matrix.eigenvalues_conjTranspose_mul_self_nonneg A i;
   · have h_nonneg : ∀ i : d, 0 ≤ ((Matrix.isHermitian_mul_conjTranspose_self A.conjTranspose).eigenvalues i) ^ (p / 2) := by

QuantumInfo/ForMathlib/IsMaximalSelfAdjoint.lean

@@ -3,7 +3,7 @@ Copyright (c) 2025 Alex Meiburg. All rights reserved.
 Released under MIT license as described in the file LICENSE.
 Authors: Alex Meiburg
 -/
-import Mathlib.Analysis.Matrix
+import Mathlib.Analysis.Matrix.Normed
 
 /- We want to have `HermitianMat.trace` give 𝕜 when 𝕜 is already a TrivialStar field, but give the "clean" type
 otherwise -- for instance, ℝ when the input field is ℂ. This typeclass lets us do so. -/