Raw matrix frames and their tensor realization

Lax342547.RawFrames · concepts/Lax342547/RawFrames.lean · lax-342547

proven

Loading review…

Natural Language Statement

Lemma

The four matrices $P,Q,X,Y$ satisfy the full-frame injectivity and Gram constraints (2.13). The tensor embedding is $Z\mapsto PZQ^T$ . The channel contraction is $\operatorname{tr}(XY^T\xi)$ , equal to the entrywise pairing $\langle YX^T,\xi\rangle$ in (2.15).

Concept map

2 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

lem✓Lax342547.RawFrames

⊢Lax342547Proofs.RawFrames.tensor_realization

Lean source view on GitHub

Show types on hover

1	import Lax342547.MomentSpace
2	import Mathlib.LinearAlgebra.Matrix.Trace
3
4	/-!
5	---
6	title: Raw matrix frames and their tensor realization
7	type: lemma
8	---
9	The four matrices $P,Q,X,Y$ satisfy the full-frame injectivity and
10	Gram constraints (2.13). The tensor embedding is $Z\mapsto PZQ^T$ .
11	The channel contraction is $\operatorname{tr}(XY^T\xi)$ , equal to
12	the entrywise pairing $\langle YX^T,\xi\rangle$ in (2.15).
13	-/
14
15	namespace Lax342547.RawFrames
16
17	open Lax342547.MomentSpace
18
19	variable (B H N : Type) [Fintype B] [Fintype H] [Fintype N]
20
21	structure Frame (E : Matrix B B Binary) where
22	P : Matrix N B Binary
23	Q : Matrix N B Binary
24	X : Matrix N H Binary
25	Y : Matrix N H Binary
26	plus_injective : Function.Injective
27	(fun z : (B → Binary) × (H → Binary) => P.mulVec z.1 + X.mulVec z.2)
28	minus_injective : Function.Injective
29	(fun z : (B → Binary) × (H → Binary) => Q.mulVec z.1 + Y.mulVec z.2)
30	gram : P.transpose * Q = E
31	plus_annihilator : X.transpose * Q = 0
32	minus_annihilator : P.transpose * Y = 0
33
34	variable {B H N}
35
36	abbrev FrameData := Matrix N B Binary × Matrix N B Binary × Matrix N H Binary × Matrix N H Binary
37
38	def frameData {E : Matrix B B Binary} (F : Frame B H N E) : FrameData (B := B) (H := H) (N := N) :=
39	(F.P, F.Q, F.X, F.Y)
40
41	theorem frameData_injective {E : Matrix B B Binary} :
42	Function.Injective (frameData (E := E) (H := H) (N := N)) := by
43	intro F G h
44	cases F
45	cases G
46	simp only [frameData, Prod.mk.injEq] at h
47	obtain ⟨hP, hQ, hX, hY⟩ := h
48	cases hP
49	cases hQ
50	cases hX
51	cases hY
52	rfl
53
54	noncomputable instance {E : Matrix B B Binary} : Fintype (Frame B H N E) :=
55	by classical exact Fintype.ofInjective frameData frameData_injective
56
57	def sandwich (P Q : Matrix N B Binary) : Matrix B B Binary →ₗ[Binary] Matrix N N Binary where
58	toFun Z := P * Z * Q.transpose
59	map_add' Z W := by simp [Matrix.mul_add, Matrix.add_mul]
60	map_smul' c Z := by simp [Matrix.mul_smul, Matrix.smul_mul]
61
62	def contraction {E : Matrix B B Binary} (F : Frame B H N E) :
63	Matrix N N Binary →ₗ[Binary] Binary where
64	toFun Z := Matrix.trace (F.X * F.Y.transpose * Z)
65	map_add' Z W := by simp [Matrix.mul_add, Matrix.trace_add]
66	map_smul' c Z := by simp [Matrix.mul_smul, Matrix.trace_smul]
67
68	variable {Comp : Type}
69
70	def profileMap {E : Matrix B B Binary} (F : Comp → Frame B H N E) :
71	(Comp → Matrix B B Binary) →ₗ[Binary] (Comp → Matrix N N Binary) where
72	toFun x e := sandwich (F e).P (F e).Q (x e)
73	map_add' x y := by ext e i j; simp
74	map_smul' c x := by ext e i j; simp
75
76	def profileContraction [Fintype Comp] {E : Matrix B B Binary} (F : Comp → Frame B H N E) :
77	(Comp → Matrix N N Binary) →ₗ[Binary] Binary :=
78	∑ e, (contraction (F e)).comp (LinearMap.proj e)
79
80	axiom tensor_realization {E : Matrix B B Binary} (F : Comp → Frame B H N E) [Fintype Comp] :
81	Function.Injective (profileMap F) ∧
82	∀ x, profileContraction F (profileMap F x) = 0
83
84	end Lax342547.RawFrames
85