From 0256d13c39245d63aeb7434cdcb170c3456da384 Mon Sep 17 00:00:00 2001
From: mehatamm <mati@ehatamm.com>
Date: Wed, 1 Oct 2025 10:58:38 -0400
Subject: [PATCH] Conjugation is positive

---
 QuantumInfo/Finite/CPTPMap/Unbundled.lean | 40 ++++++++++++++++++++---
 QuantumInfo/ForMathlib/Matrix.lean        |  3 +-
 2 files changed, 38 insertions(+), 5 deletions(-)

diff --git a/QuantumInfo/Finite/CPTPMap/Unbundled.lean b/QuantumInfo/Finite/CPTPMap/Unbundled.lean
index 43f0312..ab0b01b 100644
--- a/QuantumInfo/Finite/CPTPMap/Unbundled.lean
+++ b/QuantumInfo/Finite/CPTPMap/Unbundled.lean
@@ -299,15 +299,47 @@ theorem _root_.MatrixMap.choi_PSD_iff_CP_map [DecidableEq A] (M : MatrixMap A B
     ext
     simp [choi_matrix] --TODO: `choi_matrix 0 = 0` as simp
 
-/-- The act of conjugating (not necessarily by a unitary, just by any matrix at all) is completely positive. -/
-theorem conj_isCompletelyPositive (M : Matrix B A R) :
-  IsCompletelyPositive {
+
+def conj_map (M : Matrix B A R): MatrixMap A B R := {
     toFun := fun (x : Matrix A A R) ↦ M * x * M.conjTranspose,
     map_add' x y := by rw [Matrix.mul_add, Matrix.add_mul]
     map_smul' r x := by rw [RingHom.id_apply, Matrix.mul_smul, Matrix.smul_mul]
-  } := by
+  }
+
+
+omit [DecidableEq A] in theorem conj_isPositive (M : Matrix B A R) :
+  MatrixMap.IsPositive (conj_map M) := by
+  intro X hX
+  constructor
+  · simp [conj_map]
+    unfold Matrix.IsHermitian
+    simp [hX.1.eq, Matrix.mul_assoc]
+  · intro x
+    simp [conj_map]
+    rw [Matrix.mul_assoc, ←Matrix.mulVec_mulVec, Matrix.dotProduct_mulVec]
+    rw [←(star_star (Matrix.vecMul _ _)), Matrix.star_vecMul, star_star]
+    rw [←Matrix.mulVec_mulVec]
+    apply hX.2
+
+theorem conj_tensorIsConj {n : ℕ} (M : Matrix B A R):
+  (conj_map M) ⊗ₖₘ (LinearMap.id : MatrixMap (Fin n) (Fin n) R) =
+  conj_map (M ⊗ₖ (1 : Matrix (Fin n) (Fin n) R)) := by
   sorry
 
+
+/-- The act of conjugating (not necessarily by a unitary, just by any matrix at all) is completely positive. -/
+
+theorem conj_isCompletelyPositive (M : Matrix B A R) :
+  IsCompletelyPositive (conj_map M) := by
+  intro n
+  rw [conj_tensorIsConj]
+  apply conj_isPositive
+
+
+
+
+
+
 /-- The channel X ↦ ∑ k : κ, (M k) * X * (M k)ᴴ formed by Kraus operators M : κ → Matrix B A R
 is completely positive -/
 theorem of_kraus_isCompletelyPositive {κ : Type*} [Fintype κ] (M : κ → Matrix B A R) :
diff --git a/QuantumInfo/ForMathlib/Matrix.lean b/QuantumInfo/ForMathlib/Matrix.lean
index ba75610..83150cf 100644
--- a/QuantumInfo/ForMathlib/Matrix.lean
+++ b/QuantumInfo/ForMathlib/Matrix.lean
@@ -86,12 +86,13 @@ section Kronecker
 open Kronecker
 
 variable [CommRing R] [StarRing R]
-variable (A : Matrix m m R) (B : Matrix n n R)
+variable{m m' n'} (A : Matrix m m' R) (B : Matrix n n' R)
 
 omit [DecidableEq n] in
 theorem kroneckerMap_conjTranspose : (A ⊗ₖ B)ᴴ = (Aᴴ ⊗ₖ Bᴴ) := by
   ext; simp
 
+
 variable {A : Matrix m m R} {B : Matrix n n R}
 variable (hA : A.IsHermitian) (hB : B.IsHermitian)