SplitTowerCoordinates.lean

1 import KomorebiSpace.SplitTowerSemantics
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Residual-semantic coordinates as a continuous linear equivalence
7 
8 For split towers with a strict propagation gap, candidate transports are
9 continuously linearly equivalent to protected semantic data times residuals.
10 The forward map is (observable, differential). Its inverse is the explicit
11 exact repair plus the explicit residual correction.
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 : Splitting Y)
22 
23 /-- Valid protected profiles are exactly the fixed points of the observable. -/
24 def semanticSpace : Submodule 𝕜 (Candidates X Y) :=
25   LinearMap.ker ((L.observable X - ContinuousLinearMap.id 𝕜 _).toLinearMap)
26 
27 @[simp] theorem mem_semanticSpace (s : Candidates X Y) :
28     s ∈ L.semanticSpace X ↔ L.observable X s = s := by
29   change L.observable X s - s = 0 ↔ _
30   exact sub_eq_zero
31 
32 variable (hgap : (L.bound : ℝ) * X.bound < 1)
33 
34 /-- A genuine bijective linear coordinate map, with an explicit inverse. -/
35 def coordinateEquiv : Candidates X Y ≃ₗ[𝕜] (L.semanticSpace X × Residuals X Y) where
36   toFun f := (⟨L.observable X f, (L.mem_semanticSpace X _).mpr
37     (L.observable_idempotent X f)⟩, differential X Y f)
38   invFun z := L.repair X hgap z.1.val + L.correction X hgap z.2
39   left_inv f := by
40     apply L.residual_observable_injective X
41     · simp
42     · simp
43   right_inv z := by
44     apply Prod.ext
45     · apply Subtype.ext
46       change L.observable X (L.repair X hgap z.1.val + L.correction X hgap z.2) = z.1.val
47       simp only [map_add, repair_preserves_observable, observable_correction, add_zero]
48       exact (L.mem_semanticSpace X _).mp z.1.property
49     · change differential X Y (L.repair X hgap z.1.val + L.correction X hgap z.2) = z.2
50       simp
51   map_add' f g := by
52     apply Prod.ext
53     · apply Subtype.ext
54       exact map_add (L.observable X) f g
55     · exact map_add (differential X Y) f g
56   map_smul' c f := by
57     apply Prod.ext
58     · apply Subtype.ext
59       exact map_smul (L.observable X) c f
60     · exact map_smul (differential X Y) c f
61 
62 @[simp] theorem coordinate_semantics (f : Candidates X Y) :
63     ((L.coordinateEquiv X hgap f).1 : Candidates X Y) = L.observable X f := rfl
64 
65 @[simp] theorem coordinate_residual (f : Candidates X Y) :
66     (L.coordinateEquiv X hgap f).2 = differential X Y f := rfl
67 
68 @[simp] theorem coordinate_inverse (z : L.semanticSpace X × Residuals X Y) :
69     (L.coordinateEquiv X hgap).symm z =
70       L.repair X hgap z.1.val + L.correction X hgap z.2 := rfl
71 
72 theorem coordinate_bound (f : Candidates X Y) :
73     ‖L.coordinateEquiv X hgap f‖ ≤
74       max (1 + (L.bound : ℝ) * Y.bound) ((X.bound : ℝ) + Y.bound) * ‖f‖ := by
75   change max ‖L.observable X f‖ ‖differential X Y f‖ ≤ _
76   apply max_le
77   · exact (L.observable_bound X f).trans
78       (mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg f))
79   · exact (differential_bound X Y f).trans
80       (mul_le_mul_of_nonneg_right (le_max_right _ _) (norm_nonneg f))
81 
82 theorem coordinate_inverse_bound (z : L.semanticSpace X × Residuals X Y) :
83     ‖(L.coordinateEquiv X hgap).symm z‖ ≤
84       (‖L.repair X hgap‖ + ‖L.correction X hgap‖) * ‖z‖ := by
85   have h1 : ‖z.1.val‖ ≤ ‖z‖ := le_max_left _ _
86   have h2 : ‖z.2‖ ≤ ‖z‖ := le_max_right _ _
87   calc
88     ‖(L.coordinateEquiv X hgap).symm z‖ ≤
89         ‖L.repair X hgap z.1.val‖ + ‖L.correction X hgap z.2‖ := norm_add_le _ _
90     _ ≤ ‖L.repair X hgap‖ * ‖z.1.val‖ + ‖L.correction X hgap‖ * ‖z.2‖ :=
91       add_le_add ((L.repair X hgap).le_opNorm _) ((L.correction X hgap).le_opNorm _)
92     _ ≤ ‖L.repair X hgap‖ * ‖z‖ + ‖L.correction X hgap‖ * ‖z‖ :=
93       add_le_add (mul_le_mul_of_nonneg_left h1 (norm_nonneg _))
94         (mul_le_mul_of_nonneg_left h2 (norm_nonneg _))
95     _ = (‖L.repair X hgap‖ + ‖L.correction X hgap‖) * ‖z‖ := by ring
96 
97 /-- The coordinate system preserves both linear and topological structure. -/
98 def coordinates : Candidates X Y ≃L[𝕜] (L.semanticSpace X × Residuals X Y) :=
99   (L.coordinateEquiv X hgap).toContinuousLinearEquivOfBounds
100     (max (1 + (L.bound : ℝ) * Y.bound) ((X.bound : ℝ) + Y.bound))
101     (‖L.repair X hgap‖ + ‖L.correction X hgap‖)
102     (L.coordinate_bound X hgap) (L.coordinate_inverse_bound X hgap)
103 
104 /-- In these coordinates, exactness is exactly the zero residual slice. -/
105 theorem exact_iff_zero_residual_coordinate (f : Candidates X Y) :
106     Exact X Y f ↔ (L.coordinates X hgap f).2 = 0 :=
107   exact_iff_differential_zero X Y f
108 
109 /-- Repair keeps the semantic coordinate and sets the residual coordinate to zero. -/
110 theorem coordinates_repair (f : Candidates X Y) :
111     L.coordinates X hgap (L.repair X hgap f) = ((L.coordinates X hgap f).1, 0) := by
112   apply Prod.ext
113   · apply Subtype.ext
114     exact L.repair_preserves_observable X hgap f
115   · exact L.repair_differential_zero X hgap f
116 
117 /-- Correction inserts a residual without changing any protected coordinate. -/
118 theorem coordinates_correction (r : Residuals X Y) :
119     L.coordinates X hgap (L.correction X hgap r) = (0, r) := by
120   apply Prod.ext
121   · apply Subtype.ext
122     exact L.observable_correction X hgap r
123   · exact L.differential_correction X hgap r
124 
125 end Splitting
126 end BanachTower
127 end KomorebiSpace
128 end

Back to source controls