From 287c15b206500799acd90a2cf75e3b19d8acdfbb Mon Sep 17 00:00:00 2001 From: Dennj Osele Date: Thu, 30 Apr 2026 18:22:54 +0100 Subject: [PATCH] feat(CPTPMap): close 6 sorries around piProd MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit MatrixMap: - exists_kraus: prove via explicit Kraus decomposition over ((B × A) × A) × B (now requires [StarRing R] [Fintype B]). - Basis.piTensorProduct: drop the local opaque stub and use Mathlib's PiTensorProduct.Basis. - Add choi_matrix_piProd characterising the Choi matrix of piProd. Unbundled: - Add IsTracePreserving.piProd. - Discharge IsCompletelyPositive.piProd via choi_matrix_piProd and Matrix.PosSemidef.piProd. CPTP: - Fill CPTPMap.piProd.TP using IsTracePreserving.piProd (needs maxRecDepth 1000). - fin_1_piProd: replace the sorry-in-type statement with the real equality using ofEquiv (Equiv.funUnique (Fin 1) _) and prove it. --- QuantumInfo/Finite/CPTPMap/CPTP.lean | 23 ++++- QuantumInfo/Finite/CPTPMap/MatrixMap.lean | 101 +++++++++++++++------- QuantumInfo/Finite/CPTPMap/Unbundled.lean | 40 ++++++++- 3 files changed, 127 insertions(+), 37 deletions(-) diff --git a/QuantumInfo/Finite/CPTPMap/CPTP.lean b/QuantumInfo/Finite/CPTPMap/CPTP.lean index 88362e367..5c115a960 100644 --- a/QuantumInfo/Finite/CPTPMap/CPTP.lean +++ b/QuantumInfo/Finite/CPTPMap/CPTP.lean @@ -365,18 +365,35 @@ variable {ι : Type u} [DecidableEq ι] [fι : Fintype ι] variable {dI : ι → Type v} [∀(i :ι), Fintype (dI i)] [∀(i :ι), DecidableEq (dI i)] variable {dO : ι → Type w} [∀(i :ι), Fintype (dO i)] [∀(i :ι), DecidableEq (dO i)] +set_option maxRecDepth 1000 in /-- Finitely-indexed tensor products of CPTPMaps. -/ def piProd (Λi : (i:ι) → CPTPMap (dI i) (dO i)) : CPTPMap ((i:ι) → dI i) ((i:ι) → dO i) where toLinearMap := MatrixMap.piProd (fun i ↦ (Λi i).map) cp := MatrixMap.IsCompletelyPositive.piProd (fun i ↦ (Λi i).cp) - TP := sorry + TP := MatrixMap.IsTracePreserving.piProd (fun i ↦ (Λi i).TP) theorem fin_1_piProd {dI : Fin 1 → Type v} [Fintype (dI 0)] [DecidableEq (dI 0)] {dO : Fin 1 → Type w} [Fintype (dO 0)] [DecidableEq (dO 0)] (Λi : (i : Fin 1) → CPTPMap (dI 0) (dO 0)) : - piProd Λi = sorry ∘ₘ ((Λi 1) ∘ₘ sorry) := - sorry --TODO: permutations + piProd Λi = + ofEquiv (Equiv.funUnique (Fin 1) (dO 0)).symm ∘ₘ + ((Λi 1) ∘ₘ ofEquiv (Equiv.funUnique (Fin 1) (dI 0))) := by + apply CPTPMap.ext + change MatrixMap.piProd (fun i ↦ (Λi i).map) = + MatrixMap.submatrix ℂ (Equiv.funUnique (Fin 1) (dO 0)) ∘ₗ + ((Λi 1).map ∘ₗ MatrixMap.submatrix ℂ (Equiv.funUnique (Fin 1) (dI 0)).symm) + apply MatrixMap.choi_equiv.injective + conv_lhs => rw [MatrixMap.choi_equiv_apply, MatrixMap.choi_matrix_piProd] + rw [MatrixMap.choi_equiv_apply] + ext ⟨i, a⟩ ⟨j, b⟩ + simp only [Matrix.reindex_apply, Matrix.piProd, Matrix.of_apply, + Fintype.prod_subsingleton _ (0 : Fin 1), + MatrixMap.choi_matrix, LinearMap.comp_apply, + MatrixMap.submatrix_apply, Matrix.submatrix_apply, Matrix.single] + convert rfl + ext + simp [funext_iff] /-- The tensor product of composed maps is the composition of the tensor products. diff --git a/QuantumInfo/Finite/CPTPMap/MatrixMap.lean b/QuantumInfo/Finite/CPTPMap/MatrixMap.lean index b6f23ad41..78e88d7e5 100644 --- a/QuantumInfo/Finite/CPTPMap/MatrixMap.lean +++ b/QuantumInfo/Finite/CPTPMap/MatrixMap.lean @@ -7,6 +7,7 @@ module public import Mathlib.LinearAlgebra.TensorProduct.Matrix public import Mathlib.LinearAlgebra.PiTensorProduct +public import Mathlib.LinearAlgebra.PiTensorProduct.Basis public import Mathlib.Data.Set.Card public import Mathlib.Algebra.Module.LinearMap.Basic public import QuantumInfo.ForMathlib @@ -127,11 +128,47 @@ def of_kraus (M N : κ → Matrix B A R) : MatrixMap A B R := map_smul' r x := by rw [RingHom.id_apply, Matrix.mul_smul, Matrix.smul_mul] } -def exists_kraus (Φ : MatrixMap A B R) : ∃ r : ℕ, ∃ (M N : Fin r → Matrix B A R), Φ = of_kraus M N := - sorry - end kraus +section kraus_exists + +variable [CommSemiring R] [StarRing R] [Fintype B] + +theorem exists_kraus (Φ : MatrixMap A B R) : + ∃ r : ℕ, ∃ (M N : Fin r → Matrix B A R), Φ = of_kraus M N := by + classical + let K := ((B × A) × A) × B + let M₀ : K → Matrix B A R := fun (((b, a₁), a₂), b₂) => + Matrix.single b a₁ (Φ (Matrix.single a₁ a₂ (1 : R)) b b₂) + let N₀ : K → Matrix B A R := fun (((_, _), a₂), b₂) => Matrix.single b₂ a₂ (1 : R) + let e : Fin (Fintype.card K) ≃ K := (Fintype.equivFin _).symm + refine ⟨Fintype.card K, M₀ ∘ e, N₀ ∘ e, ?_⟩ + apply choi_matrix_inj + ext ⟨j₁, i₁⟩ ⟨j₂, i₂⟩ + simp only [choi_matrix, of_kraus, LinearMap.coe_sum, LinearMap.coe_mk, AddHom.coe_mk, + Finset.sum_apply] + have hsum_reindex : + (∑ x : Fin (Fintype.card K), + (M₀ ∘ e) x * Matrix.single i₁ i₂ (1 : R) * ((N₀ ∘ e) x).conjTranspose) j₁ j₂ + = + ∑ y : K, (M₀ y * Matrix.single i₁ i₂ (1 : R) * (N₀ y).conjTranspose) j₁ j₂ := by + rw [Matrix.sum_apply] + exact e.sum_comp + (fun y : K => (M₀ y * Matrix.single i₁ i₂ (1 : R) * (N₀ y).conjTranspose) j₁ j₂) + rw [hsum_reindex, Fintype.sum_prod_type, Fintype.sum_prod_type, Fintype.sum_prod_type] + simp [M₀, N₀, Matrix.mul_apply, Matrix.single, ite_and] + rw [Finset.sum_eq_single i₂] + · rw [Finset.sum_eq_single j₂] + · simp + · intro b hb hbj + simp [hbj, star_zero] + · simp + · intro a ha ha_ne + simp [ha_ne, star_zero] + · simp + +end kraus_exists + section submatrix variable {A B : Type*} (R : Type*) [Semiring R] @@ -358,43 +395,42 @@ theorem id_kron_submatrix [CommSemiring R] (f : B → A) : end kron section pi -section basis - ---Missing from Mathlib - -variable {ι : Type*} -variable {R : Type*} [CommSemiring R] -variable {s : ι → Type*} [∀ i, AddCommMonoid (s i)] [∀ i, Module R (s i)] -variable {L : ι → Type* } - -/-- Like `Basis.tensorProduct`, but for `PiTensorProduct` -/ -noncomputable opaque _root_.Module.Basis.piTensorProduct [∀i, Fintype (L i)] - (b : (i:ι) → Module.Basis (L i) R (s i)) : - Module.Basis ((i:ι) → L i) R (PiTensorProduct R s) := - --Marking as opaque so that ATPs don't run into unpacking the sorried data. - --TODO: This is actually defined appropriately in a later Mathlib version. - Finsupp.basisSingleOne.map sorry - -end basis - variable {R : Type*} [CommSemiring R] -variable {ι : Type u} [DecidableEq ι] [fι : Fintype ι] +variable {ι : Type u} [DecidableEq ι] [Fintype ι] variable {dI : ι → Type v} [∀i, Fintype (dI i)] [∀i, DecidableEq (dI i)] variable {dO : ι → Type w} [∀i, Fintype (dO i)] [∀i, DecidableEq (dO i)] /-- Finite Pi-type tensor product of MatrixMaps. Defined as `PiTensorProduct.tprod` of the underlying Linear maps. Notation `⨂ₜₘ[R] i, f i`, eventually. -/ noncomputable def piProd (Λi : ∀ i, MatrixMap (dI i) (dO i) R) : MatrixMap (∀i, dI i) (∀i, dO i) R := - let map₁ := PiTensorProduct.map Λi; - let map₂ := LinearMap.toMatrix - (Module.Basis.piTensorProduct (fun i ↦ Matrix.stdBasis R (dI i) (dI i))) - (Module.Basis.piTensorProduct (fun i ↦ Matrix.stdBasis R (dO i) (dO i))) map₁ - let r₁ : ((i : ι) → dO i × dO i) ≃ ((i : ι) → dO i) × ((i : ι) → dO i) := Equiv.arrowProdEquivProdArrow _ dO dO - let r₂ : ((i : ι) → dI i × dI i) ≃ ((i : ι) → dI i) × ((i : ι) → dI i) := Equiv.arrowProdEquivProdArrow _ dI dI - let map₃ := Matrix.reindex r₁ r₂ map₂; Matrix.toLin (Matrix.stdBasis R ((i:ι) → dI i) ((i:ι) → dI i)) - (Matrix.stdBasis R ((i:ι) → dO i) ((i:ι) → dO i)) map₃ + (Matrix.stdBasis R ((i:ι) → dO i) ((i:ι) → dO i)) + (Matrix.reindex (Equiv.arrowProdEquivProdArrow _ dO dO) + (Equiv.arrowProdEquivProdArrow _ dI dI) + (LinearMap.toMatrix + (_root_.Basis.piTensorProduct (fun i ↦ Matrix.stdBasis R (dI i) (dI i))) + (_root_.Basis.piTensorProduct (fun i ↦ Matrix.stdBasis R (dO i) (dO i))) + (PiTensorProduct.map Λi))) + +theorem choi_matrix_piProd (Λi : ∀ i, MatrixMap (dI i) (dO i) R) : + (MatrixMap.piProd Λi).choi_matrix = + Matrix.reindex + (Equiv.arrowProdEquivProdArrow ι dO dI) + (Equiv.arrowProdEquivProdArrow ι dO dI) + (Matrix.piProd (fun i => (Λi i).choi_matrix)) := by + ext x y + simp [MatrixMap.choi_matrix, Matrix.piProd] + rw [MatrixMap.piProd, ← Matrix.stdBasis_eq_single (R := R) x.2 y.2, + Matrix.toLin_self, Matrix.sum_apply, Finset.sum_eq_single (x.1, y.1)] + · simp [Matrix.reindex_apply, LinearMap.toMatrix_apply, Matrix.stdBasis, + ← Matrix.single_eq_of_single_single] + · intro z _ hz + rw [Matrix.stdBasis_eq_single] + simp [Matrix.single] + intro hz1 hz2 + exact False.elim (hz (Prod.ext hz1 hz2)) + · simp -- notation3:100 "⨂ₜₘ "(...)", "r:(scoped f => tprod R f) => r -- syntax (name := bigsum) "∑ " bigOpBinders ("with " term)? ", " term:67 : term @@ -409,7 +445,6 @@ theorem piProd_comp [∀ i, Fintype (d₃ i)] [∀ i, DecidableEq (d₃ i)] (Λ₁ : ∀ i, MatrixMap (d₁ i) (d₂ i) R) (Λ₂ : ∀ i, MatrixMap (d₂ i) (d₃ i) R) : piProd (fun i ↦ (Λ₂ i) ∘ₗ (Λ₁ i)) = (piProd Λ₂) ∘ₗ (piProd Λ₁) := by - simp [piProd, PiTensorProduct.map_comp, ← Matrix.toLin_mul] - rw [← LinearMap.toMatrix_comp] + simp [piProd, PiTensorProduct.map_comp, ← Matrix.toLin_mul, ← LinearMap.toMatrix_comp] end pi diff --git a/QuantumInfo/Finite/CPTPMap/Unbundled.lean b/QuantumInfo/Finite/CPTPMap/Unbundled.lean index d5b51d867..4499e92bd 100644 --- a/QuantumInfo/Finite/CPTPMap/Unbundled.lean +++ b/QuantumInfo/Finite/CPTPMap/Unbundled.lean @@ -121,6 +121,41 @@ theorem kron {M₁ : MatrixMap A B R} {M₂ : MatrixMap C D R} (h₁ : M₁.IsTr · exact Matrix.trace_single_eq_of_ne _ _ _ h simp [h_simp] +section piProd + +variable {ι : Type u} [DecidableEq ι] [Fintype ι] +variable {dI : ι → Type v} [∀ i, Fintype (dI i)] [∀ i, DecidableEq (dI i)] +variable {dO : ι → Type w} [∀ i, Fintype (dO i)] [∀ i, DecidableEq (dO i)] +variable {R : Type*} [CommSemiring R] + +/-- The `MatrixMap.piProd` product of IsTracePreserving maps is also trace preserving. -/ +theorem piProd {Λi : ∀ i, MatrixMap (dI i) (dO i) R} (h₁ : ∀ i, (Λi i).IsTracePreserving) : + (MatrixMap.piProd Λi).IsTracePreserving := by + rw [IsTracePreserving_iff_trace_choi, MatrixMap.choi_matrix_piProd] + ext f g + simp [Matrix.traceLeft, Matrix.piProd, Matrix.reindex_apply] + have htrace : ∀ i, (Λi i).choi_matrix.traceLeft = 1 := fun i => + (IsTracePreserving_iff_trace_choi (Λi i)).1 (h₁ i) + have hprod : ∀ a b : ∀ i, dI i, + (∑ x : ∀ i, dO i, ∏ i, (Λi i).choi_matrix (x i, a i) (x i, b i)) = + ∏ i, ∑ x, (Λi i).choi_matrix (x, a i) (x, b i) := fun a b => by + simpa using + (Fintype.prod_sum (f := fun i x => (Λi i).choi_matrix (x, a i) (x, b i))).symm + by_cases hfg : f = g + · subst hfg + rw [hprod] + have hdiag : ∀ i, ∑ x, (Λi i).choi_matrix (x, f i) (x, f i) = 1 := fun i => by + simpa [Matrix.traceLeft] using congrFun₂ (htrace i) (f i) (f i) + simp [hdiag] + · obtain ⟨i, hi⟩ := Function.ne_iff.mp hfg + have hfactor : ∑ x, (Λi i).choi_matrix (x, f i) (x, g i) = 0 := by + simpa [Matrix.traceLeft, Matrix.one_apply, hi] + using congrFun₂ (htrace i) (f i) (g i) + rw [hprod, Finset.prod_eq_zero (Finset.mem_univ i) hfactor] + simp [hfg] + +end piProd + variable {S : Type*} [CommSemiring S] [Star S] [DecidableEq A] in set_option backward.isDefEq.respectTransparency false in /-- The channel X ↦ ∑ k : κ, (M k) * X * (N k)ᴴ formed by Kraus operators M, N : κ → Matrix B A R @@ -784,7 +819,10 @@ variable {dO : ι → Type w} [∀i, Fintype (dO i)] [∀i, DecidableEq (dO i)] /-- The `MatrixMap.piProd` product of IsCompletelyPositive maps is also completely positive. -/ theorem piProd {Λi : ∀ i, MatrixMap (dI i) (dO i) R} (h₁ : ∀ i, (Λi i).IsCompletelyPositive) : IsCompletelyPositive (MatrixMap.piProd Λi) := by - sorry + rw [choi_PSD_iff_CP_map, MatrixMap.choi_matrix_piProd] + convert Matrix.PosSemidef.submatrix + (Matrix.PosSemidef.piProd (fun i => (choi_PSD_iff_CP_map (Λi i)).1 (h₁ i))) + (Equiv.arrowProdEquivProdArrow ι dO dI).symm using 1 end piProd