ConstantTower.lean

1 import KomorebiSpace.BanachTowers
2 
3 set_option autoImplicit false
4 
5 /-!
6 # A non-vacuous canonical model
7 
8 For a tower with identity bonding maps, exact transports are precisely constant
9 operator families. Every bounded candidate has a unique exact repair preserving
10 its level-zero operator. No residual-proportional error estimate is asserted.
11 -/
12 universe u v
13 noncomputable section
14 open scoped NNReal ENNReal
15 namespace KomorebiSpace
16 namespace BanachTower
17 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
18 variable (E F : Type v) [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
19 variable [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
20 
21 def constant : BanachTower.{u,v} 𝕜 where
22   Obj _ := E
23   down _ := ContinuousLinearMap.id 𝕜 E
24   bound := 1
25   down_bound _ := ContinuousLinearMap.norm_id_le
26 
27 variable {E F}
28 
29 def constantCandidate (T : E →L[𝕜] F) :
30     Candidates (constant (𝕜 := 𝕜) E) (constant (𝕜 := 𝕜) F) :=
31   ⟨fun _ => T, memℓp_infty ⟨‖T‖, by rintro _ ⟨n, rfl⟩; exact le_rfl⟩⟩
32 
33 @[simp] theorem constantCandidate_apply (T : E →L[𝕜] F) (n : ℕ) :
34     constantCandidate T n = T := rfl
35 
36 theorem constantCandidate_exact (T : E →L[𝕜] F) :
37     Exact (constant E) (constant F) (constantCandidate T) := by
38   intro n
39   ext x
40   rfl
41 
42 /-- A characterization of all exact maps, not merely a chosen example. -/
43 theorem constant_exact_iff
44     (f : Candidates (constant (𝕜 := 𝕜) E) (constant (𝕜 := 𝕜) F)) :
45     Exact (constant E) (constant F) f ↔ ∀ n, f n = f 0 := by
46   constructor
47   · intro hf n
48     induction n with
49     | zero => rfl
50     | succ n ih =>
51       have hn : f (n+1) = f n := by
52         ext x
53         exact congrArg (fun T : E →L[𝕜] F => T x) (hf n)
54       exact hn.trans ih
55   · intro hf n
56     ext x
57     change f (n+1) x = f n x
58     rw [hf (n+1), hf n]
59     rfl
60 
61 /-- Uniqueness follows from the actual identity-tower structure. -/
62 theorem constant_unique_repair
63     (f : Candidates (constant (𝕜 := 𝕜) E) (constant (𝕜 := 𝕜) F)) :
64     ∃! g : Candidates (constant (𝕜 := 𝕜) E) (constant (𝕜 := 𝕜) F),
65       Exact (constant E) (constant F) g ∧ g 0 = f 0 := by
66   refine ⟨constantCandidate (f 0), ⟨constantCandidate_exact _, rfl⟩, ?_⟩
67   intro g hg
68   apply lp.ext
69   funext n
70   exact ((constant_exact_iff g).mp hg.1 n).trans hg.2
71 
72 /-- The inverse limit of an identity tower is actually its underlying Banach space. -/
73 def constantPointEquiv : (constant (𝕜 := 𝕜) E).Point ≃ E where
74   toFun x := x.val 0
75   invFun x := ⟨fun _ => x, fun _ => rfl⟩
76   left_inv x := by
77     apply Subtype.ext
78     funext n
79     change x.val 0 = x.val n
80     induction n with
81     | zero => rfl
82     | succ n ih =>
83       have hn : x.val (n+1) = x.val n := x.property n
84       exact ih.trans hn.symm
85   right_inv _ := rfl
86 
87 /-- After these equivalences, realization recovers the supplied operator exactly. -/
88 theorem constant_realization (T : E →L[𝕜] F) (x : E) :
89     constantPointEquiv
90       (onLimit (constant E) (constant F) (constantCandidate T)
91         (constantCandidate_exact T) (constantPointEquiv.symm x)) = T x := rfl
92 
93 end BanachTower
94 end KomorebiSpace
95 end

Back to source controls