Transfer.lean

1 import Mathlib.Algebra.Module.Submodule.LinearMap
2 import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
3 
4 /-! P4 with actual linear maps between possibly different spaces.
5 Completeness and the intermediate idempotence assumptions are explicit.
6 No orthogonality or finite-dimensionality is needed for these identities.
7 -/
8 set_option autoImplicit false
9 open scoped BigOperators
10 namespace Komorebi.LSM
11 universe u v w t
12 variable {R : Type u} [Semiring R]
13 variable {X : Type v} [AddCommMonoid X] [Module R X]
14 variable {Y : Type w} [AddCommMonoid Y] [Module R Y]
15 variable {Z : Type t} [AddCommMonoid Z] [Module R Z]
16 
17 /-- A typed input-to-output transfer block. -/
18 def transferBlock (P : X →ₗ[R] X) (L : X →ₗ[R] Y) (Q : Y →ₗ[R] Y) :
19     X →ₗ[R] Y := Q.comp (L.comp P)
20 
21 theorem transfer_reconstruction {I J : Type*} [Fintype I] [Fintype J]
22     (P : I → X →ₗ[R] X) (Q : J → Y →ₗ[R] Y) (L : X →ₗ[R] Y)
23     (hP : ∑ i, P i = LinearMap.id) (hQ : ∑ j, Q j = LinearMap.id) :
24     L = ∑ j, ∑ i, transferBlock (P i) L (Q j) := by
25   calc
26     L = (∑ j, Q j).comp (L.comp (∑ i, P i)) := by rw [hP, hQ]; simp
27     _ = _ := by
28       ext x
29       simp only [transferBlock, LinearMap.comp_apply, LinearMap.sum_apply, map_sum]
30       exact Finset.sum_comm
31 
32 theorem transfer_refinement {I J : Type*} [Fintype I] [Fintype J]
33     (P : X →ₗ[R] X) (Q : Y →ₗ[R] Y)
34     (p : I → X →ₗ[R] X) (q : J → Y →ₗ[R] Y) (L : X →ₗ[R] Y)
35     (hp : P = ∑ i, p i) (hq : Q = ∑ j, q j) :
36     transferBlock P L Q = ∑ j, ∑ i, transferBlock (p i) L (q j) := by
37   rw [hp, hq]
38   ext x
39   simp only [transferBlock, LinearMap.comp_apply, LinearMap.sum_apply, map_sum]
40   exact Finset.sum_comm
41 
42 theorem transfer_composition {J : Type*} [Fintype J]
43     (P : X →ₗ[R] X) (Q : J → Y →ₗ[R] Y) (S : Z →ₗ[R] Z)
44     (L : X →ₗ[R] Y) (M : Y →ₗ[R] Z)
45     (hQ : ∑ j, Q j = LinearMap.id)
46     (idem : ∀ j y, Q j (Q j y) = Q j y) :
47     transferBlock P (M.comp L) S =
48       ∑ j, (transferBlock (Q j) M S).comp (transferBlock P L (Q j)) := by
49   ext x
50   simp only [transferBlock, LinearMap.comp_apply, LinearMap.sum_apply, idem]
51   have h (y : Y) : (∑ j, Q j y) = y := by
52     simpa only [LinearMap.sum_apply, LinearMap.id_apply] using
53       congrArg (fun f : Y →ₗ[R] Y => f y) hQ
54   rw [← map_sum, ← map_sum, h]
55 
56 /-- One layer of complete refinement preserves the operator sum.
57 This is not the full tree/antichain or Pythagoras theorem of P3. -/
58 theorem refinement_sum {I J : Type*} [Fintype I] [Fintype J]
59     (P : I → X →ₗ[R] X) (p : I → J → X →ₗ[R] X)
60     (complete : ∑ i, P i = LinearMap.id)
61     (split : ∀ i, ∑ j, p i j = P i) :
62     (∑ i, ∑ j, p i j) = LinearMap.id := by
63   simp only [split, complete]
64 
65 theorem packet_reconstruction {I : Type*} [Fintype I]
66     (P : I → X →ₗ[R] X) (complete : ∑ i, P i = LinearMap.id) (x : X) :
67     (∑ i, P i x) = x := by
68   simpa only [LinearMap.sum_apply, LinearMap.id_apply] using
69     congrArg (fun f : X →ₗ[R] X => f x) complete
70 
71 end Komorebi.LSM

Back to source controls