ExactCoordinates.lean

1 import KomorebiVerification.ProjectorCore
2 
3 /-!
4 # Exact packet coordinates for a complete projector family
5 
6 The packet space below is defined independently as the finite product of the
7 actual ranges of the projectors.  It is not defined as the image of analysis,
8 and synthesis is the direct sum of the packet values rather than an
9 inverse-by-definition.  Idempotence, pairwise orthogonality, and completeness
10 therefore do the mathematical work in the two inverse laws.
11 -/
12 
13 set_option autoImplicit false
14 
15 namespace Komorebi.Foundation.LinearProjectorFamily
16 
17 universe u v w
18 
19 variable {R : Type u} {M : Type v} {ι : Type w}
20 variable [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι]
21 
22 /-- The explicit product of the projector ranges. -/
23 abbrev PacketSpace (P : LinearProjectorFamily R M ι) : Type max v w :=
24   (i : ι) → LinearMap.range (P.proj i)
25 
26 /-- Analysis, with each projected value certified to lie in its projector range. -/
27 def rangeAnalysis (P : LinearProjectorFamily R M ι) : M →ₗ[R] PacketSpace P where
28   toFun x i := ⟨P.proj i x, ⟨x, rfl⟩⟩
29   map_add' x y := by
30     funext i
31     apply Subtype.ext
32     exact (P.proj i).map_add x y
33   map_smul' c x := by
34     funext i
35     apply Subtype.ext
36     exact (P.proj i).map_smul c x
37 
38 /-- Synthesis is the direct finite sum of packet values. -/
39 def rangeSynthesis (P : LinearProjectorFamily R M ι) : PacketSpace P →ₗ[R] M where
40   toFun packets := ∑ i, (packets i : M)
41   map_add' packets packets' := by
42     simp only [Pi.add_apply, Submodule.coe_add, Finset.sum_add_distrib]
43   map_smul' c packets := by
44     simp only [Pi.smul_apply, SetLike.val_smul, Finset.smul_sum, RingHom.id_apply]
45 
46 @[simp] theorem proj_packet_self
47     (P : LinearProjectorFamily R M ι) (packets : PacketSpace P) (i : ι) :
48     P.proj i (packets i : M) = (packets i : M) := by
49   rcases (packets i).property with ⟨x, hx⟩
50   rw [← hx]
51   exact P.idempotent i x
52 
53 theorem proj_packet_eq_zero
54     (P : LinearProjectorFamily R M ι) (packets : PacketSpace P)
55     {i j : ι} (hij : i ≠ j) :
56     P.proj i (packets j : M) = 0 := by
57   rcases (packets j).property with ⟨x, hx⟩
58   rw [← hx]
59   exact P.orthogonal hij x
60 
61 /-- Completeness proves that synthesizing analyzed coordinates returns the input. -/
62 @[simp] theorem rangeSynthesis_rangeAnalysis
63     (P : LinearProjectorFamily R M ι) (x : M) :
64     P.rangeSynthesis (P.rangeAnalysis x) = x := by
65   change (∑ i, P.proj i x) = x
66   exact P.complete x
67 
68 /-- Idempotence and orthogonality prove that analysis recovers every range packet. -/
69 @[simp] theorem rangeAnalysis_rangeSynthesis
70     (P : LinearProjectorFamily R M ι) (packets : PacketSpace P) :
71     P.rangeAnalysis (P.rangeSynthesis packets) = packets := by
72   classical
73   funext i
74   apply Subtype.ext
75   change P.proj i (∑ j, (packets j : M)) = (packets i : M)
76   rw [map_sum, Finset.sum_eq_single i]
77   · exact P.proj_packet_self packets i
78   · intro j _ hji
79     exact P.proj_packet_eq_zero packets hji.symm
80   · simp
81 
82 /-- Exact linear coordinates in the independent product of projector ranges. -/
83 def exactPacketCoordinates
84     (P : LinearProjectorFamily R M ι) : M ≃ₗ[R] PacketSpace P where
85   toFun := P.rangeAnalysis
86   invFun := P.rangeSynthesis
87   left_inv := P.rangeSynthesis_rangeAnalysis
88   right_inv := P.rangeAnalysis_rangeSynthesis
89   map_add' := (P.rangeAnalysis).map_add
90   map_smul' := (P.rangeAnalysis).map_smul
91 
92 @[simp] theorem exactPacketCoordinates_apply
93     (P : LinearProjectorFamily R M ι) (x : M) :
94     P.exactPacketCoordinates x = P.rangeAnalysis x := rfl
95 
96 @[simp] theorem exactPacketCoordinates_symm_apply
97     (P : LinearProjectorFamily R M ι) (packets : PacketSpace P) :
98     P.exactPacketCoordinates.symm packets = P.rangeSynthesis packets := rfl
99 
100 end Komorebi.Foundation.LinearProjectorFamily
101 
102 #print axioms Komorebi.Foundation.LinearProjectorFamily.rangeSynthesis_rangeAnalysis
103 #print axioms Komorebi.Foundation.LinearProjectorFamily.rangeAnalysis_rangeSynthesis
104 #print axioms Komorebi.Foundation.LinearProjectorFamily.exactPacketCoordinates

Back to source controls