From 82dd2999ae4e8c588ee8f015169eebb14575a6ee Mon Sep 17 00:00:00 2001
From: Ruizsolveall <ruizizchen@gmail.com>
Date: Tue, 4 Nov 2025 00:36:47 +0000
Subject: [PATCH] feat(Finite): add experimental Euclidean-space KetEuc and
 optKet

---
 QuantumInfo/Finite/UnitaryAction.lean | 47 +++++++++++++++++++++++++++
 QuantumInfo/Finite/new_Braket.lean    | 33 +++++++++++++++++++
 2 files changed, 80 insertions(+)
 create mode 100644 QuantumInfo/Finite/UnitaryAction.lean
 create mode 100644 QuantumInfo/Finite/new_Braket.lean

diff --git a/QuantumInfo/Finite/UnitaryAction.lean b/QuantumInfo/Finite/UnitaryAction.lean
new file mode 100644
index 0000000..275309e
--- /dev/null
+++ b/QuantumInfo/Finite/UnitaryAction.lean
@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2025 Alex Meiburg. All rights reserved.
+Released under MIT license as described in the file LICENSE.
+Authors: Alex Meiburg, Rodolfo Soldati, Ruize Chen
+-/
+
+import QuantumInfo.Finite.new_Braket
+import QuantumInfo.Finite.Unitary
+import Mathlib
+
+variable {d : Type*} [Fintype d] [DecidableEq d]
+open Matrix
+
+/-- Apply a unitary `U : 𝐔[d]` to a ket `ψ : KetEuc d`.
+We view the matrix as a unitary continuous linear map on `EuclideanSpace ℂ d`,
+then use `unitary.norm_map` to show normalization is preserved. -/
+noncomputable def optKet (U: 𝐔[d]) (ψ : KetEuc d): KetEuc d where
+  vec :=  Matrix.mulVec (U : Matrix d d ℂ) ψ.vec
+  normalized' := by
+    have hU: LinearMap.toContinuousLinearMap (U : Matrix d d ℂ).toEuclideanLin ∈ unitary (EuclideanSpace ℂ d →L[ℂ] EuclideanSpace ℂ d) := by
+      rw [unitary, Submonoid.mem_mk, Subsemigroup.mem_mk]
+      have hU1 := Matrix.UnitaryGroup.star_mul_self U
+      have hU2 :  (U : Matrix d d ℂ) * star (U : Matrix d d ℂ) = 1:= mul_eq_one_comm.mp hU1
+      constructor
+      · ext x ex
+        simp only [ContinuousLinearMap.coe_mul, Function.comp_apply, ContinuousLinearMap.one_apply]
+        rw [ContinuousLinearMap.star_eq_adjoint]
+        erw [LinearMap.coe_toContinuousLinearMap' (U : Matrix d d ℂ).mulVecLin]
+        rw [← ContinuousLinearMap.coe_coe, ← LinearMap.adjoint_eq_toCLM_adjoint,
+          mulVecBilin_apply, ← Matrix.toEuclideanLin_conjTranspose_eq_adjoint,
+          Matrix.toEuclideanLin_apply, PiLp.toLp_apply, WithLp.ofLp, id_eq, mulVec_mulVec]
+        erw [hU1]
+        rw [one_mulVec]
+      · ext x ex
+        rw [ContinuousLinearMap.coe_mul, LinearMap.coe_toContinuousLinearMap',
+          Function.comp_apply, ContinuousLinearMap.one_apply, ContinuousLinearMap.star_eq_adjoint]
+        erw [LinearMap.coe_toContinuousLinearMap' (U : Matrix d d ℂ).mulVecLin]
+        rw [← ContinuousLinearMap.coe_coe, ← LinearMap.adjoint_eq_toCLM_adjoint,
+          mulVecBilin_apply, ← Matrix.toEuclideanLin_conjTranspose_eq_adjoint,
+            Matrix.toEuclideanLin_apply, WithLp.ofLp, WithLp.toLp, id_eq, mulVec_mulVec, id_eq]
+        erw [hU2]
+        rw [one_mulVec]
+    let Umap: unitary (EuclideanSpace ℂ d →L[ℂ] EuclideanSpace ℂ d) := ⟨(U : Matrix d d ℂ).mulVecLin.toContinuousLinearMap,hU⟩
+    have hUU := unitary.norm_map Umap ψ.vec
+    simp only at hUU
+    rw [← ψ.normalized', ← hUU]
+    rfl
diff --git a/QuantumInfo/Finite/new_Braket.lean b/QuantumInfo/Finite/new_Braket.lean
new file mode 100644
index 0000000..47c22e6
--- /dev/null
+++ b/QuantumInfo/Finite/new_Braket.lean
@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2025 Alex Meiburg. All rights reserved.
+Released under MIT license as described in the file LICENSE.
+Authors: Alex Meiburg, Rodolfo Soldati, Ruize Chen
+-/
+
+import Mathlib
+import QuantumInfo.ForMathlib
+import ClassicalInfo.Distribution
+/-!
+A minimal EuclideanSpace-based `Ket` type (experimental).
+-/
+noncomputable section
+open scoped Matrix
+
+section
+variable (d : Type*) [Fintype d]
+
+/-- Experimental Euclidean-space Ket: a unit vector in `EuclideanSpace ℂ d`. -/
+structure KetEuc where
+  vec : EuclideanSpace ℂ d
+  normalized' : ‖vec‖ = 1
+end
+
+namespace NewBraket
+variable {d : Type*} [Fintype d]
+
+@[simp] theorem KetEuc.norm_one (ψ : KetEuc d) : ‖ψ.vec‖ = 1 := ψ.normalized'
+end NewBraket
+
+/-- lowercase alias for quick experiments (if you want) -/
+abbrev ket (d : Type*) [Fintype d] := KetEuc d
+end