BanachTowerExactification.lean

1 import KomorebiSpace.BanachTowers
2 import KomorebiSpace.RepairProjection
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Actual bounded-tower exactification
8 
9 The algebraic tower differential and the Banach-space convergence theorem are
10 connected here. The protected observable is a complete operator at a chosen
11 resolution level. Realization is in the explicitly constructed inverse limit,
12 not an unspecified underlying object. A correction operator is input data.
13 -/
14 universe u v
15 noncomputable section
16 namespace KomorebiSpace
17 namespace BanachTower
18 open Filter
19 open scoped Topology NNReal ENNReal
20 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
21 variable (X Y : BanachTower.{u,v} 𝕜)
22 
23 /-- Exactification of an actual sequence of bounded resolution transports. -/
24 theorem geometric_exactification
25     (f : ℕ → Candidates X Y) (k : ℕ) (q C : ℝ)
26     (hq₀ : 0 ≤ q) (hq₁ : q < 1) (hC : 0 ≤ C)
27     (hdec : ∀ n, ‖differential X Y (f (n+1))‖ ≤ q * ‖differential X Y (f n)‖)
28     (hstep : ∀ n, dist (f n) (f (n+1)) ≤ C * ‖differential X Y (f n)‖)
29     (hkeep : ∀ n, f n k = f 0 k) :
30     ∃ g, Tendsto f atTop (𝓝 g) ∧ Exact X Y g ∧ g k = f 0 k ∧
31       ∀ n, dist (f n) g ≤ (C / (1-q)) * ‖differential X Y (f n)‖ := by
32   obtain ⟨g, hlim, hd, hk, hbound⟩ :=
33     LinearExactification.geometric_semantic_exactification
34       (differential X Y) (evaluation X Y k) f q C hq₀ hq₁ hC hdec hstep hkeep
35   exact ⟨g, hlim, (exact_iff_differential_zero X Y g).mpr hd, hk, hbound⟩
36 
37 /-- The sup-norm error controls every finite-resolution operator error. -/
38 theorem coordinate_dist_le (f g : Candidates X Y) (n : ℕ) :
39     dist (f n) (g n) ≤ dist f g := by
40   simpa only [dist_eq_norm, lp.coeFn_sub, Pi.sub_apply] using
41     lp.norm_apply_le_norm ENNReal.top_ne_zero (f-g) n
42 
43 /-- A nonzero protected level rules out the vacuous zero repair. -/
44 theorem nonzero_of_protected_level (f g : Candidates X Y) (k : ℕ)
45     (hkeep : g k = f k) (hnonzero : f k ≠ 0) : g ≠ 0 := by
46   intro hz
47   apply hnonzero
48   rw [← hkeep, hz]
49   rfl
50 
51 /-- A bounded correction operator produces an exact tower transport. -/
52 theorem repair_by_operator
53     (A : Residuals X Y →L[𝕜] Candidates X Y) (k : ℕ)
54     (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q < 1)
55     (hkeep : ∀ r, A r k = 0)
56     (hcontract : ∀ f : Candidates X Y,
57       ‖differential X Y f - differential X Y (A (differential X Y f))‖ ≤
58         q * ‖differential X Y f‖)
59     (f : Candidates X Y) :
60     ∃ g, Tendsto (RepairDynamics.orbit (differential X Y) A f) atTop (𝓝 g) ∧
61       Exact X Y g ∧ g k = f k ∧
62       ∀ n, dist (RepairDynamics.orbit (differential X Y) A f n) g ≤
63         (‖A‖ / (1-q)) *
64           ‖differential X Y (RepairDynamics.orbit (differential X Y) A f n)‖ := by
65   obtain ⟨g, hlim, hd, hk, hbound⟩ :=
66     RepairDynamics.exactification_from_correction_operator
67       (differential X Y) (evaluation X Y k) A q hq₀ hq₁ hkeep hcontract f
68   exact ⟨g, hlim, (exact_iff_differential_zero X Y g).mpr hd, hk, hbound⟩
69 
70 /-- The repaired tower realizes an actual map of coherent inverse-limit points. -/
71 theorem repair_and_realize
72     (A : Residuals X Y →L[𝕜] Candidates X Y) (k : ℕ)
73     (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q < 1)
74     (hkeep : ∀ r, A r k = 0)
75     (hcontract : ∀ f : Candidates X Y,
76       ‖differential X Y f - differential X Y (A (differential X Y f))‖ ≤
77         q * ‖differential X Y f‖)
78     (f : Candidates X Y) :
79     ∃ g : Candidates X Y, ∃ F : X.Point → Y.Point,
80       Exact X Y g ∧ g k = f k ∧
81       Tendsto (RepairDynamics.orbit (differential X Y) A f) atTop (𝓝 g) ∧
82       dist f g ≤ (‖A‖ / (1-q)) * ‖differential X Y f‖ ∧
83       (∀ x n, (F x).val n = g n (x.val n)) ∧
84       ∀ x, (F x).val k = f k (x.val k) := by
85   obtain ⟨g, hlim, hexact, hk, hb⟩ :=
86     repair_by_operator X Y A k q hq₀ hq₁ hkeep hcontract f
87   refine ⟨g, onLimit X Y g hexact, hexact, hk, hlim, hb 0, ?_, ?_⟩
88   · intro x n
89     rfl
90   · intro x
91     change g k (x.val k) = f k (x.val k)
92     rw [hk]
93 
94 /-- Canonicity of repair requires separation by the protected level. -/
95 theorem unique_repair_of_separation
96     (A : Residuals X Y →L[𝕜] Candidates X Y) (k : ℕ)
97     (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q < 1)
98     (hkeep : ∀ r, A r k = 0)
99     (hcontract : ∀ f : Candidates X Y,
100       ‖differential X Y f - differential X Y (A (differential X Y f))‖ ≤
101         q * ‖differential X Y f‖)
102     (hsep : ∀ a b : Candidates X Y, Exact X Y a → Exact X Y b → a k = b k → a = b)
103     (f : Candidates X Y) :
104     ∃! g : Candidates X Y, Exact X Y g ∧ g k = f k := by
105   obtain ⟨g, _, hg, hk, _⟩ := repair_by_operator X Y A k q hq₀ hq₁ hkeep hcontract f
106   refine ⟨g, ⟨hg, hk⟩, ?_⟩
107   intro z hz
108   exact hsep z g hz.1 hg (hz.2.trans hk.symm)
109 
110 /-- The abstract limiting projector instantiated on actual tower candidates. -/
111 def exactificationProjection (k : ℕ)
112     (B : RepairDynamics.Scheme (differential X Y) (evaluation X Y k)) :
113     Candidates X Y →L[𝕜] Candidates X Y := B.projection
114 
115 theorem projection_exact_preserving_idempotent (k : ℕ)
116     (B : RepairDynamics.Scheme (differential X Y) (evaluation X Y k))
117     (f : Candidates X Y) :
118     Exact X Y (exactificationProjection X Y k B f) ∧
119       exactificationProjection X Y k B f k = f k ∧
120       exactificationProjection X Y k B (exactificationProjection X Y k B f) =
121         exactificationProjection X Y k B f := by
122   exact ⟨(exact_iff_differential_zero X Y _).mpr (B.limit_exact f),
123     B.limit_semantics f, B.projection_idempotent f⟩
124 
125 /-- The stability bound includes the proved sizes of the actual bonding maps. -/
126 theorem projection_stability_bound (k : ℕ)
127     (B : RepairDynamics.Scheme (differential X Y) (evaluation X Y k)) :
128     ‖exactificationProjection X Y k B‖ ≤
129       1 + (‖B.correction‖ / (1-B.rate)) * ((X.bound : ℝ) + Y.bound) := by
130   have hC : 0 ≤ ‖B.correction‖ / (1-B.rate) :=
131     div_nonneg (norm_nonneg _) (le_of_lt (sub_pos.mpr B.rate_lt_one))
132   calc
133     ‖exactificationProjection X Y k B‖ ≤
134         1 + (‖B.correction‖ / (1-B.rate)) * ‖differential X Y‖ := B.projection_bound
135     _ ≤ 1 + (‖B.correction‖ / (1-B.rate)) * ((X.bound : ℝ) + Y.bound) :=
136       add_le_add le_rfl (mul_le_mul_of_nonneg_left (differential_opNorm X Y) hC)
137 
138 end BanachTower
139 end KomorebiSpace
140 end

Back to source controls