SplitTowerCanonicity.lean

1 import KomorebiSpace.SplitDefectCharts
2 import KomorebiSpace.SplitTowerCoordinates
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Canonicity for the actual split-tower differential
8 
9 Two valid target splittings yield different possible repairs but the same
10 exact core, residual space, and subspace of seed-plus-kernel profiles.
11 The intrinsic exact-core charts change by bounded triangular shears.
12 -/
13 universe u v
14 noncomputable section
15 open scoped NNReal ENNReal
16 namespace KomorebiSpace
17 namespace BanachTower
18 namespace Splitting
19 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
20 variable (X : BanachTower.{u,v} 𝕜) {Y : BanachTower.{u,v} 𝕜}
21 variable (L M N : Splitting Y)
22 
23 /-- The seed-plus-innovation profile space has a splitting-independent description. -/
24 theorem semanticSpace_characterization (f : Candidates X Y) :
25     f ∈ L.semanticSpace X ↔ ∀ n, (Y.down n).comp (f (n+1)) = 0 := by
26   rw [L.mem_semanticSpace X]
27   constructor
28   · intro hf n
29     have hn := congrArg (fun a : Candidates X Y => a (n+1)) hf
30     change L.innovation X f n = f (n+1) at hn
31     rw [← hn]
32     exact L.innovation_down X f n
33   · intro hf
34     apply lp.ext
35     funext n
36     cases n with
37     | zero => rfl
38     | succ n =>
39       change f (n+1) - (L.up n).comp ((Y.down n).comp (f (n+1))) = f (n+1)
40       rw [hf n]
41       simp
42 
43 /-- Profile values depend on the splitting, but their possible-value subspace does not. -/
44 theorem semanticSpace_eq : L.semanticSpace X = M.semanticSpace X := by
45   ext f
46   rw [L.semanticSpace_characterization X, M.semanticSpace_characterization X]
47 
48 @[simp] theorem observable_cross (f : Candidates X Y) :
49     L.observable X (M.observable X f) = M.observable X f := by
50   apply (L.mem_semanticSpace X _).mp
51   rw [L.semanticSpace_eq X M]
52   exact (M.mem_semanticSpace X _).mpr (M.observable_idempotent X f)
53 
54 variable (hL : (L.bound : ℝ) * X.bound < 1)
55 variable (hM : (M.bound : ℝ) * X.bound < 1)
56 variable (hN : (N.bound : ℝ) * X.bound < 1)
57 
58 /-- The previously constructed correction is a section of the actual differential. -/
59 def defectSection : SplitDefect.Section (differential X Y) where
60   lift := L.correction X hL
61   right_inv := L.differential_correction X hL
62 
63 @[simp] theorem defectSection_project (f : Candidates X Y) :
64     (L.defectSection X hL).project f = L.repair X hL f := rfl
65 
66 /-- The first factor here is the intrinsic exact core, independent of L. -/
67 def coreCoordinates : Candidates X Y ≃L[𝕜]
68     (SplitDefect.Core (differential X Y) × Residuals X Y) :=
69   (L.defectSection X hL).chart
70 
71 @[simp] theorem coreCoordinates_exact (f : Candidates X Y) :
72     (L.coreCoordinates X hL f).1.val = L.repair X hL f := rfl
73 
74 @[simp] theorem coreCoordinates_residual (f : Candidates X Y) :
75     (L.coreCoordinates X hL f).2 = differential X Y f := rfl
76 
77 /-- A change of splitting does not change the residual coordinate. -/
78 def coreTransition : (SplitDefect.Core (differential X Y) × Residuals X Y) ≃L[𝕜]
79     (SplitDefect.Core (differential X Y) × Residuals X Y) :=
80   (L.defectSection X hL).transition (M.defectSection X hM)
81 
82 theorem coreTransition_formula (z : SplitDefect.Core (differential X Y) × Residuals X Y) :
83     L.coreTransition X M hL hM z =
84       (z.1 + (L.defectSection X hL).difference (M.defectSection X hM) z.2, z.2) :=
85   (L.defectSection X hL).transition_formula (M.defectSection X hM) z
86 
87 theorem coreTransition_cocycle (z : SplitDefect.Core (differential X Y) × Residuals X Y) :
88     M.coreTransition X N hM hN (L.coreTransition X M hL hM z) =
89       L.coreTransition X N hL hN z :=
90   (L.defectSection X hL).transition_cocycle (M.defectSection X hM)
91     (N.defectSection X hN) z
92 
93 /-- Difference of two corrections is an exact transport family. -/
94 theorem correction_difference_exact (r : Residuals X Y) :
95     Exact X Y (L.correction X hL r - M.correction X hM r) := by
96   apply (exact_iff_differential_zero X Y _).mpr
97   simp
98 
99 theorem repair_change (f : Candidates X Y) :
100     M.repair X hM f - L.repair X hL f =
101       (L.correction X hL - M.correction X hM) (differential X Y f) := by
102   simp only [repair_apply, sub_apply]
103   abel
104 
105 theorem repair_change_norm (f : Candidates X Y) :
106     ‖M.repair X hM f - L.repair X hL f‖ ≤
107       ‖L.correction X hL - M.correction X hM‖ * ‖differential X Y f‖ := by
108   rw [L.repair_change X M hL hM f]
109   exact (L.correction X hL - M.correction X hM).le_opNorm _
110 
111 theorem repair_change_gain_bound (f : Candidates X Y) :
112     ‖M.repair X hM f - L.repair X hL f‖ ≤
113       (L.gain X + M.gain X) * ‖differential X Y f‖ := by
114   apply (L.repair_change_norm X M hL hM f).trans
115   apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)
116   exact (norm_sub_le _ _).trans
117     (add_le_add (L.correction_opNorm X hL) (M.correction_opNorm X hM))
118 
119 @[simp] theorem repair_cross (f : Candidates X Y) :
120     L.repair X hL (M.repair X hM f) = M.repair X hM f :=
121   L.repair_fixes_exact X hL _ (M.repair_exact X hM f)
122 
123 theorem repairs_commute_iff :
124     (L.repair X hL).comp (M.repair X hM) =
125       (M.repair X hM).comp (L.repair X hL) ↔
126     L.repair X hL = M.repair X hM :=
127   (L.defectSection X hL).projects_commute_iff (M.defectSection X hM)
128 
129 /-- Two charts coincide on exact inputs even when their repairs differ elsewhere. -/
130 theorem repairs_agree_on_exact (f : Candidates X Y) (hf : Exact X Y f) :
131     L.repair X hL f = M.repair X hM f := by
132   rw [L.repair_fixes_exact X hL f hf, M.repair_fixes_exact X hM f hf]
133 
134 end Splitting
135 end BanachTower
136 end KomorebiSpace
137 end

Back to source controls