RepairDynamics.lean

1 import KomorebiSpace.LinearExactification
2 import Mathlib.Analysis.Normed.Operator.NormedSpace
3 import Mathlib.Tactic.Linarith
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Constructed semantic-preserving repair dynamics
9 
10 A bounded correction operator constructs the approximation sequence. Residual
11 contraction is only required on residuals actually produced by candidates.
12 Existence of that operator is an explicit hypothesis, not a universal claim.
13 -/
14 universe u v w z
15 noncomputable section
16 namespace KomorebiSpace
17 namespace RepairDynamics
18 open Filter
19 open scoped Topology
20 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
21 variable {E : Type v} {R : Type w} {S : Type z}
22 variable [NormedAddCommGroup E] [NormedSpace 𝕜 E]
23 variable [NormedAddCommGroup R] [NormedSpace 𝕜 R]
24 variable [NormedAddCommGroup S] [NormedSpace 𝕜 S]
25 
26 def step (d : E →L[𝕜] R) (A : R →L[𝕜] E) (x : E) : E := x - A (d x)
27 
28 def orbit (d : E →L[𝕜] R) (A : R →L[𝕜] E) (x : E) : ℕ → E
29   | 0 => x
30   | n+1 => step d A (orbit d A x n)
31 
32 @[simp] theorem orbit_zero (d : E →L[𝕜] R) (A : R →L[𝕜] E) (x : E) :
33     orbit d A x 0 = x := rfl
34 
35 @[simp] theorem orbit_succ (d : E →L[𝕜] R) (A : R →L[𝕜] E) (x : E) (n : ℕ) :
36     orbit d A x (n+1) = step d A (orbit d A x n) := rfl
37 
38 @[simp] theorem step_residual (d : E →L[𝕜] R) (A : R →L[𝕜] E) (x : E) :
39     d (step d A x) = d x - d (A (d x)) := map_sub d _ _
40 
41 theorem step_semantics (d : E →L[𝕜] R) (p : E →L[𝕜] S) (A : R →L[𝕜] E)
42     (hp : ∀ r, p (A r) = 0) (x : E) : p (step d A x) = p x := by
43   simp [step, hp]
44 
45 theorem step_movement (d : E →L[𝕜] R) (A : R →L[𝕜] E) (x : E) :
46     dist x (step d A x) ≤ ‖A‖ * ‖d x‖ := by
47   calc
48     dist x (step d A x) = ‖A (d x)‖ := by simp [step]
49     _ ≤ ‖A‖ * ‖d x‖ := A.le_opNorm _
50 
51 theorem orbit_semantics (d : E →L[𝕜] R) (p : E →L[𝕜] S) (A : R →L[𝕜] E)
52     (hp : ∀ r, p (A r) = 0) (x : E) (n : ℕ) : p (orbit d A x n) = p x := by
53   induction n with
54   | zero => rfl
55   | succ n ih => exact (step_semantics d p A hp _).trans ih
56 
57 theorem step_fixes_exact (d : E →L[𝕜] R) (A : R →L[𝕜] E) (x : E)
58     (hx : d x = 0) : step d A x = x := by
59   simp [step, hx]
60 
61 theorem orbit_fixes_exact (d : E →L[𝕜] R) (A : R →L[𝕜] E) (x : E)
62     (hx : d x = 0) (n : ℕ) : orbit d A x n = x := by
63   induction n with
64   | zero => rfl
65   | succ n ih => simpa only [orbit_succ, ih] using step_fixes_exact d A x hx
66 
67 variable [CompleteSpace E]
68 
69 /-- The correction procedure constructs a convergent sequence and its exact limit. -/
70 theorem exactification_from_correction_operator
71     (d : E →L[𝕜] R) (p : E →L[𝕜] S) (A : R →L[𝕜] E)
72     (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q < 1)
73     (hp : ∀ r, p (A r) = 0)
74     (hcontract : ∀ x, ‖d x - d (A (d x))‖ ≤ q * ‖d x‖) (x : E) :
75     ∃ y, Tendsto (orbit d A x) atTop (𝓝 y) ∧ d y = 0 ∧ p y = p x ∧
76       ∀ n, dist (orbit d A x n) y ≤ (‖A‖ / (1-q)) * ‖d (orbit d A x n)‖ := by
77   apply LinearExactification.geometric_semantic_exactification d p (orbit d A x)
78     q ‖A‖ hq₀ hq₁ (norm_nonneg A)
79   · intro n
80     rw [orbit_succ, step_residual]
81     exact hcontract _
82   · intro n
83     exact step_movement d A _
84   · intro n
85     exact orbit_semantics d p A hp x n
86 
87 /-- Error bound and exact semantic repair without separately supplying an orbit. -/
88 theorem repair_exists
89     (d : E →L[𝕜] R) (p : E →L[𝕜] S) (A : R →L[𝕜] E)
90     (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q < 1)
91     (hp : ∀ r, p (A r) = 0)
92     (hcontract : ∀ x, ‖d x - d (A (d x))‖ ≤ q * ‖d x‖) (x : E) :
93     ∃ y, d y = 0 ∧ p y = p x ∧ dist x y ≤ (‖A‖ / (1-q)) * ‖d x‖ := by
94   obtain ⟨y, _, hd, hy, hb⟩ :=
95     exactification_from_correction_operator d p A q hq₀ hq₁ hp hcontract x
96   exact ⟨y, hd, hy, hb 0⟩
97 
98 /-- A semantic obstruction rules out a bounded correction operator of this strength. -/
99 theorem obstruction_vanishes
100     (d : E →L[𝕜] R) (p : E →L[𝕜] S) (A : R →L[𝕜] E)
101     (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q < 1)
102     (hp : ∀ r, p (A r) = 0)
103     (hcontract : ∀ x, ‖d x - d (A (d x))‖ ≤ q * ‖d x‖) (x : E) :
104     (LinearExactification.problem d p).obstruction x = 0 := by
105   obtain ⟨y, hd, hy, _⟩ := repair_exists d p A q hq₀ hq₁ hp hcontract x
106   exact ((LinearExactification.problem d p).flatten_iff x).mpr ⟨y, hd, hy⟩
107 
108 /-- Uniqueness requires semantic separation on exact elements, not just contraction. -/
109 theorem unique_repair
110     (d : E →L[𝕜] R) (p : E →L[𝕜] S) (A : R →L[𝕜] E)
111     (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q < 1)
112     (hp : ∀ r, p (A r) = 0)
113     (hcontract : ∀ x, ‖d x - d (A (d x))‖ ≤ q * ‖d x‖)
114     (hsep : ∀ a b, d a = 0 → d b = 0 → p a = p b → a = b) (x : E) :
115     ∃! y, d y = 0 ∧ p y = p x := by
116   obtain ⟨y, hd, hy, _⟩ := repair_exists d p A q hq₀ hq₁ hp hcontract x
117   refine ⟨y, ⟨hd, hy⟩, ?_⟩
118   intro z hz
119   exact hsep z y hz.1 hd (hz.2.trans hy.symm)
120 
121 end RepairDynamics
122 end KomorebiSpace
123 end

Back to source controls