ResidualNaturality.lean

1 import KomorebiSpace.SplitDefectCharts
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Cochain maps and the failure of repair to commute with presentation change
7 
8 The change of presentation intertwines the differentials. Chosen sections need
9 not intertwine. Their mismatch is an exact-valued bounded map, and it measures
10 precisely the discrepancy between the two orders of sampling and repair.
11 -/
12 universe u v w v' w' v'' w''
13 noncomputable section
14 namespace KomorebiSpace
15 namespace SplitDefect
16 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
17 variable {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
18 variable {R : Type w} [NormedAddCommGroup R] [NormedSpace 𝕜 R]
19 variable {F : Type v'} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
20 variable {T : Type w'} [NormedAddCommGroup T] [NormedSpace 𝕜 T]
21 variable {G : Type v''} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
22 variable {U : Type w''} [NormedAddCommGroup U] [NormedSpace 𝕜 U]
23 variable (d : E →L[𝕜] R) (D : F →L[𝕜] T)
24 
25 /-- A bounded change of candidate and residual coordinates that preserves the differential. -/
26 structure DefectMap where
27   candidate : E →L[𝕜] F
28   residual : R →L[𝕜] T
29   commutes : ∀ f, D (candidate f) = residual (d f)
30 
31 namespace DefectMap
32 variable {d D} (S : DefectMap d D)
33 
34 /-- Exact inputs remain exact; no section is used. -/
35 theorem preserves_exact (f : E) (hf : d f = 0) : D (S.candidate f) = 0 := by
36   rw [S.commutes, hf, map_zero]
37 
38 def coreMap : Core d →L[𝕜] Core D :=
39   (S.candidate.comp (Core d).subtypeL).codRestrict (Core D)
40     (fun f => S.preserves_exact f.val f.property)
41 
42 @[simp] theorem coreMap_apply (e : Core d) : (S.coreMap e : F) = S.candidate e.val := rfl
43 
44 theorem coreMap_bound (e : Core d) : ‖S.coreMap e‖ ≤ ‖S.candidate‖*‖e‖ :=
45   S.candidate.le_opNorm e.val
46 
47 def comp {d' : G →L[𝕜] U} (V : DefectMap D d') : DefectMap d d' where
48   candidate := V.candidate.comp S.candidate
49   residual := V.residual.comp S.residual
50   commutes f := by simp only [ContinuousLinearMap.comp_apply, V.commutes, S.commutes]
51 
52 @[simp] theorem comp_candidate {d' : G →L[𝕜] U} (V : DefectMap D d') (f : E) :
53     (S.comp V).candidate f = V.candidate (S.candidate f) := rfl
54 
55 @[simp] theorem comp_residual {d' : G →L[𝕜] U} (V : DefectMap D d') (r : R) :
56     (S.comp V).residual r = V.residual (S.residual r) := rfl
57 
58 variable (A : Section d) (B : Section D)
59 
60 /-- Choice mismatch; applying D gives zero by the cochain and section identities. -/
61 def mismatch : R →L[𝕜] F :=
62   S.candidate.comp A.lift - B.lift.comp S.residual
63 
64 @[simp] theorem mismatch_apply (r : R) :
65     S.mismatch A B r = S.candidate (A.lift r) - B.lift (S.residual r) := rfl
66 
67 @[simp] theorem mismatch_exact (r : R) : D (S.mismatch A B r) = 0 := by
68   rw [mismatch_apply, map_sub, S.commutes, A.right_inv, B.right_inv, sub_self]
69 
70 def coreMismatch : R →L[𝕜] Core D :=
71   (S.mismatch A B).codRestrict (Core D) (S.mismatch_exact A B)
72 
73 @[simp] theorem coreMismatch_apply (r : R) :
74     (S.coreMismatch A B r : F) = S.mismatch A B r := rfl
75 
76 /-- Exact formula for the noncommutativity of repair and presentation change. -/
77 theorem repair_change (f : E) :
78     B.project (S.candidate f) - S.candidate (A.project f) = S.mismatch A B (d f) := by
79   simp only [Section.project_apply, mismatch_apply, map_sub, S.commutes]
80   abel
81 
82 theorem repair_change_exact (f : E) :
83     D (B.project (S.candidate f) - S.candidate (A.project f)) = 0 := by
84   rw [repair_change]
85   exact S.mismatch_exact A B (d f)
86 
87 theorem repair_change_bound (f : E) :
88     ‖B.project (S.candidate f) - S.candidate (A.project f)‖ ≤
89       ‖S.mismatch A B‖ * ‖d f‖ := by
90   rw [repair_change]
91   exact (S.mismatch A B).le_opNorm _
92 
93 theorem mismatch_opNorm : ‖S.mismatch A B‖ ≤
94     ‖S.candidate‖*‖A.lift‖ + ‖B.lift‖*‖S.residual‖ := by
95   exact (norm_sub_le _ _).trans
96     (add_le_add (S.candidate.opNorm_comp_le _) (B.lift.opNorm_comp_le _))
97 
98 theorem repair_change_gain_bound (f : E) :
99     ‖B.project (S.candidate f) - S.candidate (A.project f)‖ ≤
100       (‖S.candidate‖*‖A.lift‖ + ‖B.lift‖*‖S.residual‖) * ‖d f‖ :=
101   (S.repair_change_bound A B f).trans
102     (mul_le_mul_of_nonneg_right (S.mismatch_opNorm A B) (norm_nonneg _))
103 
104 /-- Commutation of repair is equivalent to compatibility of the chosen sections. -/
105 theorem repair_natural_iff :
106     (∀ f, B.project (S.candidate f) = S.candidate (A.project f)) ↔
107       S.candidate.comp A.lift = B.lift.comp S.residual := by
108   constructor
109   · intro h
110     ext r
111     have hz : S.mismatch A B r = 0 := by
112       have hm := S.repair_change A B (A.lift r)
113       rw [A.right_inv, h, sub_self] at hm
114       exact hm.symm
115     exact sub_eq_zero.mp hz
116   · intro h f
117     apply sub_eq_zero.mp
118     rw [S.repair_change]
119     change (S.candidate.comp A.lift) (d f) - (B.lift.comp S.residual) (d f) = 0
120     rw [h, sub_self]
121 
122 /-- In coordinates, a cochain map is block triangular, not necessarily block diagonal. -/
123 theorem chart_formula (z : Core d × R) :
124     B.chart (S.candidate (A.chart.symm z)) =
125       (S.coreMap z.1 + S.coreMismatch A B z.2, S.residual z.2) := by
126   apply Prod.ext
127   · apply Subtype.ext
128     change B.project (S.candidate (z.1.val + A.lift z.2)) =
129       S.candidate z.1.val + (S.candidate (A.lift z.2) - B.lift (S.residual z.2))
130     rw [map_add, map_add, B.project_fixes _ (S.preserves_exact z.1.val z.1.property),
131       Section.project_apply, S.commutes, A.right_inv]
132   · change D (S.candidate (z.1.val + A.lift z.2)) = S.residual z.2
133     have hz : d z.1.val = 0 := z.1.property
134     rw [S.commutes, map_add, hz, A.right_inv, zero_add]
135 
136 /-- The mismatch satisfies an exact composition law for two presentation changes. -/
137 theorem mismatch_comp {d' : G →L[𝕜] U} (V : DefectMap D d')
138     (C : Section d') (r : R) :
139     (S.comp V).mismatch A C r =
140       V.candidate (S.mismatch A B r) + V.mismatch B C (S.residual r) := by
141   simp only [mismatch_apply, comp_candidate, comp_residual, map_sub]
142   abel
143 
144 /-- If residuals vanish along a sequence, the two repair routes approach one another. -/
145 theorem repair_discrepancy_tendsto_zero (f : ℕ → E)
146     (hf : Filter.Tendsto (fun n => d (f n)) Filter.atTop (nhds 0)) :
147     Filter.Tendsto (fun n => B.project (S.candidate (f n)) - S.candidate (A.project (f n)))
148       Filter.atTop (nhds 0) := by
149   have hc := ((S.mismatch A B).continuous.tendsto (0 : R)).comp hf
150   simpa only [map_zero, Function.comp_def, ← S.repair_change A B] using hc
151 
152 end DefectMap
153 end SplitDefect
154 end KomorebiSpace
155 end

Back to source controls