BanachTowers.lean

1 import KomorebiSpace.TowerCorrection
2 import Mathlib.Analysis.Normed.Lp.lpSpace
3 import Mathlib.Analysis.Normed.Operator.NormedSpace
4 import Mathlib.Algebra.Category.ModuleCat.Basic
5 import Mathlib.Tactic.Linarith
6 import Mathlib.Tactic.Positivity
7 
8 set_option autoImplicit false
9 
10 /-!
11 # Bounded Banach tower transports
12 
13 The candidate space is the dependent l-infinity product of continuous linear
14 operator spaces. Bonding maps have a supplied uniform bound. The actual
15 naturality differential is constructed as a continuous linear map with a
16 proved operator bound, rather than supplied as an unrelated analytic map.
17 -/
18 universe u v
19 noncomputable section
20 open scoped NNReal ENNReal
21 namespace KomorebiSpace
22 
23 structure BanachTower (𝕜 : Type u) [NontriviallyNormedField 𝕜] where
24   Obj : ℕ → Type v
25   [normed : ∀ n, NormedAddCommGroup (Obj n)]
26   [space : ∀ n, NormedSpace 𝕜 (Obj n)]
27   [complete : ∀ n, CompleteSpace (Obj n)]
28   down : ∀ n, Obj (n + 1) →L[𝕜] Obj n
29   bound : ℝ≥0
30   down_bound : ∀ n, ‖down n‖ ≤ (bound : ℝ)
31 
32 attribute [instance] BanachTower.normed BanachTower.space BanachTower.complete
33 
34 namespace BanachTower
35 open CategoryTheory
36 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
37 variable (X Y : BanachTower.{u,v} 𝕜)
38 
39 abbrev Candidates := lp (fun n => X.Obj n →L[𝕜] Y.Obj n) (∞ : ℝ≥0∞)
40 abbrev Residuals := lp (fun n => X.Obj (n+1) →L[𝕜] Y.Obj n) (∞ : ℝ≥0∞)
41 
42 /-- Explicit check that no candidate-space completeness is being postulated. -/
43 theorem candidates_complete : CompleteSpace (Candidates X Y) := inferInstance
44 
45 def rawDefect (f : Candidates X Y) (n : ℕ) : X.Obj (n+1) →L[𝕜] Y.Obj n :=
46   (Y.down n).comp (f (n+1)) - (f n).comp (X.down n)
47 
48 theorem rawDefect_bound (f : Candidates X Y) (n : ℕ) :
49     ‖rawDefect X Y f n‖ ≤ ((X.bound : ℝ) + Y.bound) * ‖f‖ := by
50   have hfn := lp.norm_apply_le_norm ENNReal.top_ne_zero f n
51   have hfs := lp.norm_apply_le_norm ENNReal.top_ne_zero f (n+1)
52   calc
53     ‖rawDefect X Y f n‖ ≤ ‖(Y.down n).comp (f (n+1))‖ +
54         ‖(f n).comp (X.down n)‖ := norm_sub_le _ _
55     _ ≤ ‖Y.down n‖ * ‖f (n+1)‖ + ‖f n‖ * ‖X.down n‖ :=
56       add_le_add ((Y.down n).opNorm_comp_le _) ((f n).opNorm_comp_le _)
57     _ ≤ (Y.bound : ℝ) * ‖f‖ + ‖f‖ * (X.bound : ℝ) :=
58       add_le_add
59         (mul_le_mul (Y.down_bound n) hfs (norm_nonneg _) (NNReal.coe_nonneg _))
60         (mul_le_mul hfn (X.down_bound n) (norm_nonneg _) (norm_nonneg _))
61     _ = ((X.bound : ℝ) + Y.bound) * ‖f‖ := by ring
62 
63 /-- Boundedness of the actual defect family. -/
64 theorem rawDefect_mem (f : Candidates X Y) :
65     Memℓp (rawDefect X Y f) (∞ : ℝ≥0∞) := by
66   apply memℓp_infty
67   refine ⟨((X.bound : ℝ) + Y.bound) * ‖f‖, ?_⟩
68   rintro _ ⟨n, rfl⟩
69   exact rawDefect_bound X Y f n
70 
71 def differentialLinear : Candidates X Y →ₗ[𝕜] Residuals X Y where
72   toFun f := ⟨rawDefect X Y f, rawDefect_mem X Y f⟩
73   map_add' f g := by
74     apply lp.ext
75     funext n
76     change rawDefect X Y (f + g) n = rawDefect X Y f n + rawDefect X Y g n
77     ext x
78     simp only [rawDefect, lp.coeFn_add, Pi.add_apply, ContinuousLinearMap.comp_apply,
79       sub_apply, add_apply, map_add]
80     abel
81   map_smul' c f := by
82     apply lp.ext
83     funext n
84     ext x
85     simp [rawDefect, smul_sub]
86 
87 theorem differentialLinear_bound (f : Candidates X Y) :
88     ‖differentialLinear X Y f‖ ≤ ((X.bound : ℝ) + Y.bound) * ‖f‖ := by
89   apply lp.norm_le_of_forall_le (by positivity)
90   exact rawDefect_bound X Y f
91 
92 /-- The residual operator used by analytic exactification is now constructed. -/
93 def differential : Candidates X Y →L[𝕜] Residuals X Y :=
94   (differentialLinear X Y).mkContinuous ((X.bound : ℝ) + Y.bound)
95     (differentialLinear_bound X Y)
96 
97 @[simp] theorem differential_apply (f : Candidates X Y) (n : ℕ) :
98     differential X Y f n =
99       (Y.down n).comp (f (n+1)) - (f n).comp (X.down n) := rfl
100 
101 theorem differential_bound (f : Candidates X Y) :
102     ‖differential X Y f‖ ≤ ((X.bound : ℝ) + Y.bound) * ‖f‖ :=
103   differentialLinear_bound X Y f
104 
105 theorem differential_opNorm :
106     ‖differential X Y‖ ≤ (X.bound : ℝ) + Y.bound :=
107   ContinuousLinearMap.opNorm_le_bound _ (by positivity) (differential_bound X Y)
108 
109 /-- A genuinely continuous semantic observable: protect the entire level-n operator. -/
110 def evaluation (n : ℕ) : Candidates X Y →L[𝕜] (X.Obj n →L[𝕜] Y.Obj n) :=
111   lp.evalCLM 𝕜 (fun n => X.Obj n →L[𝕜] Y.Obj n) ∞ n
112 
113 @[simp] theorem evaluation_apply (f : Candidates X Y) (n : ℕ) :
114     evaluation X Y n f = f n := rfl
115 
116 theorem evaluation_bound (f : Candidates X Y) (n : ℕ) :
117     ‖evaluation X Y n f‖ ≤ ‖f‖ :=
118   lp.norm_apply_le_norm ENNReal.top_ne_zero f n
119 
120 def Exact (f : Candidates X Y) : Prop :=
121   ∀ n, (Y.down n).comp (f (n+1)) = (f n).comp (X.down n)
122 
123 theorem exact_iff_differential_zero (f : Candidates X Y) :
124     Exact X Y f ↔ differential X Y f = 0 := by
125   constructor
126   · intro h
127     apply lp.ext
128     funext n
129     exact sub_eq_zero.mpr (h n)
130   · intro h n
131     have he := congrArg (fun g : Residuals X Y => g n) h
132     exact sub_eq_zero.mp he
133 
134 /-- Forget norms and continuity, preserving the actual bonding maps. -/
135 def algebraic : Tower (ModuleCat.{v} 𝕜) where
136   obj n := ModuleCat.of 𝕜 (X.Obj n)
137   down n := ModuleCat.ofHom (X.down n).toLinearMap
138 
139 def algebraicPreHom (f : Candidates X Y) : Tower.PreHom X.algebraic Y.algebraic where
140   app n := ModuleCat.ofHom (f n).toLinearMap
141 
142 theorem exact_iff_algebraic (f : Candidates X Y) :
143     Exact X Y f ↔ (algebraicPreHom X Y f).Exact := by
144   constructor
145   · intro h n
146     ext x
147     exact congrArg (fun T : X.Obj (n+1) →L[𝕜] Y.Obj n => T x) (h n)
148   · intro h n
149     ext x
150     exact congrArg (fun T : ModuleCat.of 𝕜 (X.Obj (n+1)) ⟶
151       ModuleCat.of 𝕜 (Y.Obj n) => T x) (h n)
152 
153 def exactHom (f : Candidates X Y) (hf : Exact X Y f) :
154     Tower.ExactHom X.algebraic Y.algebraic :=
155   ⟨algebraicPreHom X Y f, (exact_iff_algebraic X Y f).mp hf⟩
156 
157 /-- Actual inverse-limit points, with adjacent compatibility. -/
158 def Point := {x : ∀ n, X.Obj n // ∀ n, X.down n (x (n+1)) = x n}
159 
160 /-- Exact bounded tower maps act on the entire inverse-limit point type. -/
161 def onLimit (f : Candidates X Y) (hf : Exact X Y f) (x : X.Point) : Y.Point :=
162   ⟨fun n => f n (x.val n), by
163     intro n
164     have h := congrArg (fun T : X.Obj (n+1) →L[𝕜] Y.Obj n => T (x.val (n+1))) (hf n)
165     change Y.down n (f (n+1) (x.val (n+1))) = f n (x.val n)
166     exact h.trans (congrArg (f n) (x.property n))⟩
167 
168 @[simp] theorem onLimit_coordinate (f : Candidates X Y) (hf : Exact X Y f)
169     (x : X.Point) (n : ℕ) : (onLimit X Y f hf x).val n = f n (x.val n) := rfl
170 
171 theorem onLimit_unique (f : Candidates X Y) (hf : Exact X Y f)
172     (g : X.Point → Y.Point) (hg : ∀ x n, (g x).val n = f n (x.val n)) :
173     g = onLimit X Y f hf := by
174   funext x
175   apply Subtype.ext
176   funext n
177   exact hg x n
178 
179 end BanachTower
180 end KomorebiSpace
181 end

Back to source controls