LinearExactification.lean

1 import KomorebiSpace.Exactification
2 import KomorebiSpace.Correction
3 import Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
4 import Mathlib.Analysis.Normed.Module.Basic
5 
6 set_option autoImplicit false
7 
8 /-!
9 # Exactification preserving mathematical meaning
10 
11 A continuous linear residual d and a continuous linear semantic map p are kept
12 separate. Converging controlled corrections with p(fₙ)=p(f₀) yield an actual
13 x with d(x)=0 and p(x)=p(f₀), and annihilate the constrained obstruction class.
14 -/
15 universe u v w z
16 namespace KomorebiSpace
17 namespace LinearExactification
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] [CompleteSpace E]
23 variable [NormedAddCommGroup R] [NormedSpace 𝕜 R]
24 variable [NormedAddCommGroup S] [NormedSpace 𝕜 S]
25 
26 /-- The abstract obstruction quotient instantiated by genuine continuous linear maps. -/
27 def problem (d : E →L[𝕜] R) (p : E →L[𝕜] S) : CorrectionProblem E R S :=
28   ⟨d.toAddMonoidHom, p.toAddMonoidHom⟩
29 
30 omit [CompleteSpace E] in
31 theorem semantic_limit (p : E →L[𝕜] S) (f : ℕ → E) {x : E}
32     (hx : Tendsto f atTop (𝓝 x)) (hsem : ∀ n, p (f n) = p (f 0)) :
33     p x = p (f 0) := by
34   have hp : Tendsto (fun n => p (f n)) atTop (𝓝 (p x)) :=
35     p.continuous.continuousAt.tendsto.comp hx
36   have hs : Tendsto (fun n => p (f n)) atTop (𝓝 (p (f 0))) := by
37     simpa only [hsem] using
38       (tendsto_const_nhds : Tendsto (fun _ : ℕ => p (f 0)) atTop (𝓝 (p (f 0))))
39   exact tendsto_nhds_unique hp hs
40 
41 /-- Main realization theorem in the complete normed linear model. -/
42 theorem summable_semantic_exactification (d : E →L[𝕜] R) (p : E →L[𝕜] S)
43     (f : ℕ → E) (b : ℕ → ℝ) (hb : Summable b)
44     (hstep : ∀ n, dist (f n) (f (n+1)) ≤ b n)
45     (hvanish : Tendsto (fun n => ‖d (f n)‖) atTop (𝓝 0))
46     (hsem : ∀ n, p (f n) = p (f 0)) :
47     ∃ x, Tendsto f atTop (𝓝 x) ∧ d x = 0 ∧ p x = p (f 0) ∧
48       ∀ n, dist (f n) x ≤ ∑' k, b (n+k) := by
49   obtain ⟨x, hx, hz, htail⟩ := Exactification.summable_exactification
50     (fun y => ‖d y‖) (fun _ => norm_nonneg _) d.continuous.norm.lowerSemicontinuous
51     f b hb hstep hvanish
52   exact ⟨x, hx, norm_eq_zero.mp hz, semantic_limit p f hx hsem, htail⟩
53 
54 theorem geometric_semantic_exactification (d : E →L[𝕜] R) (p : E →L[𝕜] S)
55     (f : ℕ → E) (q C : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q < 1) (hC : 0 ≤ C)
56     (hdec : ∀ n, ‖d (f (n+1))‖ ≤ q * ‖d (f n)‖)
57     (hstep : ∀ n, dist (f n) (f (n+1)) ≤ C * ‖d (f n)‖)
58     (hsem : ∀ n, p (f n) = p (f 0)) :
59     ∃ x, Tendsto f atTop (𝓝 x) ∧ d x = 0 ∧ p x = p (f 0) ∧
60       ∀ n, dist (f n) x ≤ (C/(1-q)) * ‖d (f n)‖ := by
61   obtain ⟨x, hx, hz, htail⟩ := Exactification.geometric_exactification
62     (fun y => ‖d y‖) (fun _ => norm_nonneg _) d.continuous.norm.lowerSemicontinuous
63     f q C hq₀ hq₁ hC hdec hstep
64   exact ⟨x, hx, norm_eq_zero.mp hz, semantic_limit p f hx hsem, htail⟩
65 
66 /-- Controlled semantic-preserving exactification forces the obstruction to vanish. -/
67 theorem controlled_obstruction_vanishes (d : E →L[𝕜] R) (p : E →L[𝕜] S)
68     (f : ℕ → E) (b : ℕ → ℝ) (hb : Summable b)
69     (hstep : ∀ n, dist (f n) (f (n+1)) ≤ b n)
70     (hvanish : Tendsto (fun n => ‖d (f n)‖) atTop (𝓝 0))
71     (hsem : ∀ n, p (f n) = p (f 0)) :
72     (problem d p).obstruction (f 0) = 0 := by
73   obtain ⟨x, _, hd, hp, _⟩ := summable_semantic_exactification d p f b hb hstep hvanish hsem
74   exact ((problem d p).flatten_iff (f 0)).2 ⟨x, hd, hp⟩
75 
76 end LinearExactification
77 end KomorebiSpace

Back to source controls