AtlasReconciliation.lean

1 import KomorebiLSM.WeightedReconciliation
2 import Mathlib.Analysis.Normed.Module.Basic
3 
4 /-! P21: reconcile in one object space and transport the norm through the actual
5 realizable subspace. Ambient redundant coordinates are not assumed valid. -/
6 set_option autoImplicit false
7 open scoped BigOperators
8 namespace Komorebi.LSM.Reconciliation
9 universe u v w
10 
11 structure LinearAtlas (X : Type u) (C : Type v)
12     [AddCommGroup X] [Module ℝ X] [AddCommGroup C] [Module ℝ C] where
13   analysis : X →ₗ[ℝ] C
14   synthesis : C →ₗ[ℝ] X
15   reconstruct : ∀ x, synthesis (analysis x)=x
16 
17 namespace LinearAtlas
18 variable {X : Type u} [AddCommGroup X] [Module ℝ X]
19 variable {C : Type v} [AddCommGroup C] [Module ℝ C]
20 variable {D : Type w} [AddCommGroup D] [Module ℝ D]
21 
22 abbrev Coeff (a : LinearAtlas X C) := LinearMap.range a.analysis
23 
24 def encode (a : LinearAtlas X C) : X →ₗ[ℝ] a.Coeff := a.analysis.rangeRestrict
25 
26 def decode (a : LinearAtlas X C) : a.Coeff →ₗ[ℝ] X := a.synthesis.domRestrict a.analysis.range
27 
28 @[simp] theorem decode_encode (a : LinearAtlas X C) (x : X) : a.decode (a.encode x)=x :=
29   a.reconstruct x
30 
31 @[simp] theorem encode_decode (a : LinearAtlas X C) (c : a.Coeff) : a.encode (a.decode c)=c := by
32   apply Subtype.ext
33   obtain ⟨x,hx⟩ := c.property
34   change a.analysis (a.synthesis c.val)=c.val
35   rw [← hx,a.reconstruct]
36 
37 theorem decode_injective (a : LinearAtlas X C) : Function.Injective a.decode := by
38   intro x y h
39   have h' := congrArg a.encode h
40   simpa only [encode_decode] using h'
41 
42 theorem decode_surjective (a : LinearAtlas X C) : Function.Surjective a.decode := by
43   intro x
44   exact ⟨a.encode x,a.decode_encode x⟩
45 
46 def transport (a : LinearAtlas X C) (b : LinearAtlas X D) : a.Coeff →ₗ[ℝ] b.Coeff :=
47   b.encode.comp a.decode
48 
49 @[simp] theorem decode_transport (a : LinearAtlas X C) (b : LinearAtlas X D) (c : a.Coeff) :
50     b.decode (a.transport b c)=a.decode c := b.decode_encode (a.decode c)
51 
52 /-- The repaired output lies in the realizable subspace even for an arbitrary
53 ambient input. -/
54 def repaired (a : LinearAtlas X C) (L : X →ₗ[ℝ] X) : C →ₗ[ℝ] C :=
55   a.analysis.comp (L.comp a.synthesis)
56 
57 theorem repaired_consistent (a : LinearAtlas X C) (L : X →ₗ[ℝ] X) (c : C) :
58     a.repaired L c ∈ a.analysis.range := ⟨L (a.synthesis c), rfl⟩
59 
60 theorem repaired_intertwines (a : LinearAtlas X C) (b : LinearAtlas X D)
61     (L : X →ₗ[ℝ] X) (c : C) :
62     b.repaired L (b.analysis (a.synthesis c)) = b.analysis (a.synthesis (a.repaired L c)) := by
63   simp only [repaired, LinearMap.comp_apply, a.reconstruct, b.reconstruct]
64 
65 def objectFit (a : LinearAtlas X C) (G : C →ₗ[ℝ] C) : X →ₗ[ℝ] X :=
66   a.synthesis.comp (G.comp a.analysis)
67 
68 end LinearAtlas
69 
70 section Norms
71 namespace LinearAtlas
72 variable {X : Type u} [NormedAddCommGroup X] [NormedSpace ℝ X]
73 variable {C : Type v} [AddCommGroup C] [Module ℝ C]
74 variable {D : Type w} [AddCommGroup D] [Module ℝ D]
75 
76 /-- This constructs a genuine normed additive group, not just a displayed formula. -/
77 @[instance_reducible] noncomputable def coeffNormed (a : LinearAtlas X C) : NormedAddCommGroup a.Coeff :=
78   NormedAddCommGroup.induced _ X a.decode a.decode_injective
79 
80 @[instance_reducible] noncomputable def coeffNormedSpace (a : LinearAtlas X C) :
81     letI := a.coeffNormed
82     NormedSpace ℝ a.Coeff := by
83   letI := a.coeffNormed
84   exact NormedSpace.induced ℝ a.Coeff X a.decode
85 
86 theorem pullback_norm (a : LinearAtlas X C) (c : a.Coeff) :
87     letI := a.coeffNormed
88     ‖c‖=‖a.synthesis c.val‖ := rfl
89 
90 theorem transport_isometry (a : LinearAtlas X C) (b : LinearAtlas X D) :
91     letI := a.coeffNormed
92     letI := b.coeffNormed
93     Isometry (a.transport b) := by
94   let := a.coeffNormed
95   let := b.coeffNormed
96   apply Isometry.of_dist_eq
97   intro c d
98   change dist (b.decode (a.transport b c)) (b.decode (a.transport b d)) = dist (a.decode c) (a.decode d)
99   rw [a.decode_transport b, a.decode_transport b]
100 
101 /-- Every Lipschitz constant is preserved in both directions. This states
102 coordinate equality of induced Lipschitz bounds, not merely one inequality. -/
103 theorem represented_lipschitz_iff (a : LinearAtlas X C) (b : LinearAtlas X D)
104     (L : X → X) (K : NNReal) :
105     letI := a.coeffNormed
106     letI := b.coeffNormed
107     LipschitzWith K (fun c : a.Coeff => b.encode (L (a.decode c))) ↔ LipschitzWith K L := by
108   let := a.coeffNormed
109   let := b.coeffNormed
110   constructor
111   · intro h
112     apply LipschitzWith.of_dist_le_mul
113     intro x y
114     have hb := h.dist_le_mul (a.encode x) (a.encode y)
115     change dist (b.decode (b.encode (L (a.decode (a.encode x)))))
116       (b.decode (b.encode (L (a.decode (a.encode y))))) ≤
117       (K:ℝ)*dist (a.decode (a.encode x)) (a.decode (a.encode y)) at hb
118     simpa only [LinearAtlas.decode_encode] using hb
119   · intro h
120     apply LipschitzWith.of_dist_le_mul
121     intro c d
122     change dist (b.decode (b.encode (L (a.decode c)))) (b.decode (b.encode (L (a.decode d)))) ≤
123       (K:ℝ)*dist (a.decode c) (a.decode d)
124     simpa only [LinearAtlas.decode_encode] using h.dist_le_mul (a.decode c) (a.decode d)
125 
126 end LinearAtlas
127 end Norms
128 
129 section Family
130 variable {X : Type u} [AddCommGroup X] [Module ℝ X]
131 variable {I : Type*} [Fintype I] {C : I → Type v}
132 variable [∀ i, AddCommGroup (C i)] [∀ i, Module ℝ (C i)]
133 
134 noncomputable def reconciledOperator (atlas : (i : I) → LinearAtlas X (C i))
135     (G : (i : I) → C i →ₗ[ℝ] C i) (w : I → ℝ) : X →ₗ[ℝ] X :=
136   weightedMean w (fun i => (atlas i).objectFit (G i))
137 
138 theorem coherent_reconciled_family (atlas : (i : I) → LinearAtlas X (C i))
139     (G : (i : I) → C i →ₗ[ℝ] C i) (w : I → ℝ) (i j : I) (c : C i) :
140     (atlas j).repaired (reconciledOperator atlas G w) ((atlas j).analysis ((atlas i).synthesis c)) =
141       (atlas j).analysis ((atlas i).synthesis ((atlas i).repaired (reconciledOperator atlas G w) c)) :=
142   (atlas i).repaired_intertwines (atlas j) (reconciledOperator atlas G w) c
143 
144 end Family
145 
146 section CoordinateObjective
147 variable {X : Type*} [AddCommGroup X] [Module ℝ X]
148 variable {I J : Type*} [Fintype I] [Fintype J]
149 
150 /-- A finite matrix coordinate equivalence transports the Frobenius objective
151 back to actual linear operators. An orthonormal basis supplies the usual
152 Hilbert-space Frobenius interpretation. -/
153 theorem operator_frobenius_variance
154     (coord : (X →ₗ[ℝ] X) ≃ₗ[ℝ] Matrix J J ℝ) (L : I → X →ₗ[ℝ] X)
155     (w : I → ℝ) (total : ∑ i, w i=1) (M : X →ₗ[ℝ] X) :
156     frobeniusCost w (fun i => coord (L i)) (coord M) =
157       frobeniusSq (coord (M-weightedMean w L))+
158       frobeniusCost w (fun i => coord (L i)) (coord (weightedMean w L)) := by
159   have hmean : coord (weightedMean w L)=weightedMean w (fun i => coord (L i)) := by
160     simp only [weightedMean,map_sum,map_smul]
161   rw [map_sub,hmean]
162   exact frobenius_variance_identity w (fun i => coord (L i)) total (coord M)
163 
164 theorem operator_unique_frobenius_minimizer
165     (coord : (X →ₗ[ℝ] X) ≃ₗ[ℝ] Matrix J J ℝ) (L : I → X →ₗ[ℝ] X)
166     (w : I → ℝ) (total : ∑ i, w i=1) :
167     ∃! M : X →ₗ[ℝ] X, ∀ N,
168       frobeniusCost w (fun i => coord (L i)) (coord M) ≤
169       frobeniusCost w (fun i => coord (L i)) (coord N) := by
170   have hmin : ∀ N,
171       frobeniusCost w (fun i => coord (L i)) (coord (weightedMean w L)) ≤
172       frobeniusCost w (fun i => coord (L i)) (coord N) := by
173     intro N
174     rw [operator_frobenius_variance coord L w total N]
175     exact le_add_of_nonneg_left (frobeniusSq_nonneg _)
176   refine ⟨weightedMean w L,hmin,?_⟩
177   intro M hM
178   have h := hM (weightedMean w L)
179   rw [operator_frobenius_variance coord L w total M] at h
180   have hz : frobeniusSq (coord (M-weightedMean w L))=0 := by
181     linarith [frobeniusSq_nonneg (coord (M-weightedMean w L))]
182   have hc := (frobeniusSq_eq_zero_iff _).mp hz
183   apply sub_eq_zero.mp
184   apply coord.injective
185   simpa using hc
186 
187 end CoordinateObjective
188 end Komorebi.LSM.Reconciliation

Back to source controls