BanLat/Normed.lean
All source files · Download exact source
SHA-256: 50017cb69948b8e4059c65e502f1ec3f631ce7d92e5104343156e84f6aade33b
1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Basic6import Mathlib.Analysis.Convex.Combination7import Mathlib.Analysis.LocallyConvex.WeakSpace8import Mathlib.Analysis.Normed.Order.Lattice9import Mathlib.Analysis.Normed.Module.Completion10import Mathlib.Data.Fintype.Order11import Mathlib.Topology.Order.MonotoneConvergence1213/-!14# Normed vector lattices and Banach lattices1516A **normed vector lattice** is a real vector lattice whose norm satisfies the solid17axiom: `|x| ≤ |y|` implies `‖x‖ ≤ ‖y‖`. This single condition encodes compatibility18between the norm and the lattice structure. A **Banach lattice** is a normed vector19lattice whose norm is complete. This file develops the basic topology of normed20vector lattices, including continuity of lattice operations, closedness of the21positive cone, boundedness of order intervals, and monotone convergence facts.22-/2324/-- A normed vector lattice is a real vector lattice equipped with a lattice norm:25a norm satisfying `|x| ≤ |y| → ‖x‖ ≤ ‖y‖`. -/26class NormedVectorLattice (X : Type*) [NormedAddCommGroup X] [Lattice X]27 [IsOrderedAddMonoid X] extends VectorLattice X, HasSolidNorm X, NormSMulClass ℝ X2829namespace NormedVectorLattice3031variable {X : Type*} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]32 [NormedVectorLattice X]3334/-- A normed vector lattice is a normed space over `ℝ`. -/35instance instNormedSpace : NormedSpace ℝ X where36 norm_smul_le a x := (norm_smul a x).le3738/-! ### Continuity of lattice operations -/3940/-- Supremum is jointly norm-continuous. -/41theorem continuous_sup : Continuous (fun p : X × X => p.1 ⊔ p.2) :=42 ContinuousSup.continuous_sup4344/-- Infimum is jointly norm-continuous. -/45theorem continuous_inf : Continuous (fun p : X × X => p.1 ⊓ p.2) :=46 ContinuousInf.continuous_inf4748/-- The absolute value map is Lipschitz with constant 1; in particular it is continuous. -/49theorem lipschitzWith_abs : LipschitzWith 1 (|·| : X → X) :=50 LipschitzWith.of_dist_le_mul fun a b => by51 simp only [NNReal.coe_one, one_mul, dist_eq_norm]52 exact norm_abs_sub_abs a b5354/-- The norm of the positive part is bounded by the norm. -/55theorem norm_posPart_le (x : X) : ‖x⁺‖ ≤ ‖x‖ := by56 refine norm_le_norm_of_abs_le_abs ?_57 rw [abs_of_nonneg (posPart_nonneg x)]58 exact posPart_le_abs x5960/-! ### Archimedean property -/6162/-- Every normed vector lattice is Archimedean in the vector-lattice sense: the only63non-negative element all of whose multiples are bounded is zero. -/64instance instIsVLArchimedean : IsVLArchimedean X := by65 apply isVLArchimedean_of_eq_zero_of_nonneg_of_forall_nsmul_le66 intro x y hx h67 by_contra hne68 have hxpos : (0 : ℝ) < ‖x‖ := norm_pos_iff.mpr hne69 obtain ⟨n, hn⟩ := exists_lt_nsmul hxpos ‖y‖70 have h1 : ‖n • x‖ ≤ ‖y‖ := by71 apply norm_le_norm_of_abs_le_abs72 calc |n • x| = n • x := abs_of_nonneg (nsmul_nonneg hx n)73 _ ≤ y := h n74 _ ≤ |y| := le_abs_self y75 rw [show (n • x : X) = (↑n : ℝ) • x from (Nat.cast_smul_eq_nsmul ℝ n x).symm,76 norm_smul, Real.norm_natCast] at h177 simp only [nsmul_eq_mul] at hn78 linarith7980/-! ### Closed positive cone and order topology -/8182/-- The order relation is closed in a normed vector lattice. -/83instance instOrderClosedTopology : OrderClosedTopology X :=84 HasSolidNorm.orderClosedTopology8586/-- The positive cone `{x | 0 ≤ x}` is norm-closed. -/87theorem isClosed_nonneg_cone : IsClosed {x : X | 0 ≤ x} := isClosed_nonneg8889/-- Inequalities are preserved under norm limits: if `u n ≤ v n` for all `n`, and90`u n → a`, `v n → b` in norm, then `a ≤ b`. -/91theorem le_of_tendsto_of_tendsto {u v : ℕ → X} {a b : X}92 (hu : Filter.Tendsto u Filter.atTop (nhds a))93 (hv : Filter.Tendsto v Filter.atTop (nhds b))94 (h : ∀ n, u n ≤ v n) : a ≤ b :=95 le_of_tendsto_of_tendsto' hu hv h9697/-! ### Monotone Convergence Lemma -/9899/-- Monotone Convergence Lemma: an increasing sequence converging in norm is a least100upper bound for its range. -/101theorem isLUB_of_monotone_tendsto {u : ℕ → X} {l : X}102 (hmono : Monotone u) (hlim : Filter.Tendsto u Filter.atTop (nhds l)) :103 IsLUB (Set.range u) l :=104 isLUB_of_tendsto_atTop hmono hlim105106/-- Antitone Convergence Lemma: a decreasing sequence converging in norm is a greatest107lower bound for its range. -/108theorem isGLB_of_antitone_tendsto {u : ℕ → X} {l : X}109 (hanti : Antitone u) (hlim : Filter.Tendsto u Filter.atTop (nhds l)) :110 IsGLB (Set.range u) l :=111 isGLB_of_tendsto_atTop hanti hlim112113/-! ### Weak convergence of monotone nets -/114115private theorem mem_closure_convexHull_tail_of_weak_tendsto116 {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]117 {u : ι → X} {x : X}118 (hweak : Filter.Tendsto (fun i => (toWeakSpace ℝ X) (u i)) Filter.atTop119 (nhds ((toWeakSpace ℝ X) x))) (i : ι) :120 x ∈ closure (convexHull ℝ (u '' Set.Ici i)) := by121 have hx : (toWeakSpace ℝ X) x ∈122 closure (toWeakSpace ℝ X '' convexHull ℝ (u '' Set.Ici i)) := by123 apply mem_closure_of_tendsto hweak124 filter_upwards [Filter.Ici_mem_atTop i] with j hj125 exact ⟨u j, subset_convexHull ℝ _ ⟨j, hj, rfl⟩, rfl⟩126 rw [← (convex_convexHull ℝ (u '' Set.Ici i)).toWeakSpace_closure ℝ] at hx127 obtain ⟨y, hy, hyx⟩ := hx128 simpa only [(toWeakSpace ℝ X).injective hyx] using hy129130private theorem tendsto_of_monotone_weak_tendsto_aux131 {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]132 {u : ι → X} {x : X} (hmono : Monotone u)133 (hweak : Filter.Tendsto (fun i => (toWeakSpace ℝ X) (u i)) Filter.atTop134 (nhds ((toWeakSpace ℝ X) x))) :135 Filter.Tendsto u Filter.atTop (nhds x) := by136 classical137 have hle (i : ι) : u i ≤ x := by138 apply closure_minimal _ isClosed_Ici139 (mem_closure_convexHull_tail_of_weak_tendsto hweak i)140 apply convexHull_min _ (convex_Ici (u i))141 rintro _ ⟨j, hij, rfl⟩142 exact hmono hij143 rw [Metric.tendsto_nhds]144 intro ε hε145 let i₀ : ι := Classical.choice inferInstance146 obtain ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.mp147 (mem_closure_convexHull_tail_of_weak_tendsto hweak i₀) ε hε148 obtain ⟨κ, hκ, w, z, hw, hw_one, hz, hwy⟩ :=149 mem_convexHull_iff_exists_fintype.mp hy150 letI : Fintype κ := hκ151 let r : κ → ι := fun a => (hz a).choose152 have hzr (a : κ) : u (r a) = z a := (hz a).choose_spec.2153 obtain ⟨j, hj⟩ := Finite.exists_le r154 have hyj : y ≤ u j := by155 rw [← hwy]156 calc157 ∑ a, w a • z a ≤ ∑ a, w a • u j := by158 apply Finset.sum_le_sum159 intro a _160 apply smul_le_smul_of_nonneg_left _ (hw a)161 calc z a = u (r a) := (hzr a).symm162 _ ≤ u j := hmono (hj a)163 _ = (∑ a, w a) • u j := by rw [Finset.sum_smul]164 _ = u j := by rw [hw_one, one_smul]165 have hxy_norm : ‖x - y‖ < ε := by simpa only [dist_eq_norm] using hxy166 have hnorm_j : ‖x - u j‖ < ε := by167 refine (norm_le_norm_of_abs_le_abs ?_).trans_lt hxy_norm168 rw [abs_of_nonneg (sub_nonneg.mpr (hle j)),169 abs_of_nonneg (sub_nonneg.mpr (hyj.trans (hle j)))]170 exact sub_le_sub_left hyj x171 filter_upwards [Filter.Ici_mem_atTop j] with k hjk172 rw [dist_eq_norm, norm_sub_rev]173 refine (norm_le_norm_of_abs_le_abs ?_).trans_lt hnorm_j174 rw [abs_of_nonneg (sub_nonneg.mpr (hle k)),175 abs_of_nonneg (sub_nonneg.mpr (hle j))]176 exact sub_le_sub_left (hmono hjk) x177178/-- **Dini's theorem**: a monotone net in a normed vector lattice that converges weakly179converges in norm. -/180theorem tendsto_of_monotone_weak_tendsto181 {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]182 {u : ι → X} {x : X} (hmono : Monotone u ∨ Antitone u)183 (hweak : Filter.Tendsto (fun i => (toWeakSpace ℝ X) (u i)) Filter.atTop184 (nhds ((toWeakSpace ℝ X) x))) :185 Filter.Tendsto u Filter.atTop (nhds x) := by186 rcases hmono with hmono | hanti187 · exact tendsto_of_monotone_weak_tendsto_aux hmono hweak188 · have hneg_mono : Monotone fun i => -u i := fun _ _ hij => neg_le_neg (hanti hij)189 have hneg_weak :190 Filter.Tendsto (fun i => (toWeakSpace ℝ X) (-u i)) Filter.atTop191 (nhds ((toWeakSpace ℝ X) (-x))) := by192 simpa using hweak.neg193 have hneg := tendsto_of_monotone_weak_tendsto_aux hneg_mono hneg_weak194 simpa using hneg.neg195196/-! ### Closed and bounded intervals -/197198/-- Order intervals are norm-closed. -/199theorem isClosed_interval (a b : X) : IsClosed (Set.Icc a b) := isClosed_Icc200201/-- Every element `x ∈ [a, b]` satisfies `‖x‖ ≤ ‖|a| ⊔ |b|‖`. In particular, every202order interval is norm-bounded. -/203theorem norm_le_norm_abs_sup_abs_of_mem_Icc {a b x : X} (hx : x ∈ Set.Icc a b) :204 ‖x‖ ≤ ‖|a| ⊔ |b|‖ := by205 rw [← norm_abs_eq_norm x]206 apply norm_le_norm_of_abs_le_abs207 rw [abs_of_nonneg (le_sup_of_le_left (abs_nonneg a))]208 rw [abs]209 apply sup_le210 · rw [abs]211 apply sup_le212 · exact le_trans hx.2 (le_trans (le_abs_self b) le_sup_right)213 · exact le_trans (neg_le_neg hx.1) (le_trans (neg_le_abs a) le_sup_left)214 · exact le_trans (neg_nonpos_of_nonneg (abs_nonneg x))215 (le_sup_of_le_left (abs_nonneg a))216217/-- Order-bounded sets are norm-bounded. -/218theorem isBounded_of_bddBelow_bddAbove {s : Set X}219 (hl : BddBelow s) (hu : BddAbove s) : Bornology.IsBounded s := by220 obtain ⟨a, ha⟩ := hl221 obtain ⟨b, hb⟩ := hu222 rw [Metric.isBounded_iff_subset_closedBall (0 : X)]223 exact ⟨‖|a| ⊔ |b|‖, fun x hx => by224 simp only [Metric.mem_closedBall, dist_zero_right]225 exact norm_le_norm_abs_sup_abs_of_mem_Icc ⟨ha hx, hb hx⟩⟩226227end NormedVectorLattice228229/-!230## Banach lattices231-/232233/-- A Banach lattice is a normed vector lattice with a complete norm. -/234class BanachLattice (X : Type*) [NormedAddCommGroup X] [Lattice X]235 [IsOrderedAddMonoid X] extends NormedVectorLattice X, CompleteSpace X236237/-- The real numbers form a normed vector lattice over themselves. -/238noncomputable instance : NormedVectorLattice ℝ where239240/-- The real numbers form a Banach lattice over themselves. -/241noncomputable instance : BanachLattice ℝ where242243/-!244## Completion of a normed vector lattice245246The metric completion of a normed vector lattice carries a compatible lattice structure247making it again a normed vector lattice; being complete, it is a Banach lattice.248-/249250section Completion251252open UniformSpace253254variable {X : Type*} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]255 [NormedVectorLattice X]256257private lemma uniformContinuous₂_sup_completion :258 UniformContinuous fun p : X × X => p.1 ⊔ p.2 := by259 have h : (fun p : X × X => p.1 ⊔ p.2) = fun p : X × X => p.1 + (p.2 - p.1)⁺ := by260 funext p261 exact sup_eq_add_posPart p.1 p.2262 rw [h]263 exact uniformContinuous_fst.add264 (lipschitzWith_posPart.uniformContinuous.comp (uniformContinuous_snd.sub uniformContinuous_fst))265266private lemma uniformContinuous₂_inf_completion :267 UniformContinuous fun p : X × X => p.1 ⊓ p.2 := by268 have h : (fun p : X × X => p.1 ⊓ p.2) = fun p : X × X => -((-p.1) ⊔ (-p.2)) := by269 funext p270 rw [neg_sup, neg_neg, neg_neg]271 rw [h]272 exact (uniformContinuous₂_sup_completion.comp273 (uniformContinuous_fst.neg.prodMk uniformContinuous_snd.neg)).neg274275/-- The completion of a normed vector lattice is a lattice. -/276noncomputable instance instLatticeCompletion : Lattice (Completion X) := by277 letI : Max (Completion X) := ⟨Completion.map₂ (fun x y : X => x ⊔ y)⟩278 letI : Min (Completion X) := ⟨Completion.map₂ (fun x y : X => x ⊓ y)⟩279 have coe_sup : ∀ x y : X, ((x ⊔ y : X) : Completion X) =280 (x : Completion X) ⊔ (y : Completion X) := fun x y => by281 rw [show (x : Completion X) ⊔ (y : Completion X) =282 Completion.map₂ (fun x y : X => x ⊔ y) x y from rfl,283 Completion.map₂_coe_coe x y (fun x y : X => x ⊔ y) uniformContinuous₂_sup_completion]284 have coe_inf : ∀ x y : X, ((x ⊓ y : X) : Completion X) =285 (x : Completion X) ⊓ (y : Completion X) := fun x y => by286 rw [show (x : Completion X) ⊓ (y : Completion X) =287 Completion.map₂ (fun x y : X => x ⊓ y) x y from rfl,288 Completion.map₂_coe_coe x y (fun x y : X => x ⊓ y) uniformContinuous₂_inf_completion]289 refine Lattice.mk' ?sup_comm ?sup_assoc ?inf_comm ?inf_assoc ?sup_inf_self ?inf_sup_self290 · intro x y291 refine Completion.induction_on₂ x y ?_ ?_292 · exact isClosed_eq (Completion.continuous_map₂ continuous_fst continuous_snd)293 (Completion.continuous_map₂ continuous_snd continuous_fst)294 · intro x y295 rw [← coe_sup, ← coe_sup, sup_comm]296 · intro x y z297 refine Completion.induction_on₃ x y z ?_ ?_298 · exact isClosed_eq299 (Completion.continuous_map₂300 (Completion.continuous_map₂ continuous_fst (continuous_fst.comp continuous_snd))301 (continuous_snd.comp continuous_snd))302 (Completion.continuous_map₂ continuous_fst303 (Completion.continuous_map₂ (continuous_fst.comp continuous_snd)304 (continuous_snd.comp continuous_snd)))305 · intro x y z306 rw [← coe_sup, ← coe_sup, ← coe_sup, ← coe_sup, sup_assoc]307 · intro x y308 refine Completion.induction_on₂ x y ?_ ?_309 · exact isClosed_eq (Completion.continuous_map₂ continuous_fst continuous_snd)310 (Completion.continuous_map₂ continuous_snd continuous_fst)311 · intro x y312 rw [← coe_inf, ← coe_inf, inf_comm]313 · intro x y z314 refine Completion.induction_on₃ x y z ?_ ?_315 · exact isClosed_eq316 (Completion.continuous_map₂317 (Completion.continuous_map₂ continuous_fst (continuous_fst.comp continuous_snd))318 (continuous_snd.comp continuous_snd))319 (Completion.continuous_map₂ continuous_fst320 (Completion.continuous_map₂ (continuous_fst.comp continuous_snd)321 (continuous_snd.comp continuous_snd)))322 · intro x y z323 rw [← coe_inf, ← coe_inf, ← coe_inf, ← coe_inf, inf_assoc]324 · intro x y325 refine Completion.induction_on₂ x y ?_ ?_326 · exact isClosed_eq327 (Completion.continuous_map₂ continuous_fst328 (Completion.continuous_map₂ continuous_fst continuous_snd))329 continuous_fst330 · intro x y331 rw [← coe_inf, ← coe_sup, sup_inf_self]332 · intro x y333 refine Completion.induction_on₂ x y ?_ ?_334 · exact isClosed_eq335 (Completion.continuous_map₂ continuous_fst336 (Completion.continuous_map₂ continuous_fst continuous_snd))337 continuous_fst338 · intro x y339 rw [← coe_sup, ← coe_inf, inf_sup_self]340341/-- The inclusion of a normed vector lattice into its completion preserves suprema. -/342@[norm_cast]343theorem coe_sup_completion (x y : X) :344 ((x ⊔ y : X) : Completion X) = (x : Completion X) ⊔ (y : Completion X) := by345 rw [show (x : Completion X) ⊔ (y : Completion X) =346 Completion.map₂ (fun x y : X => x ⊔ y) x y from rfl,347 Completion.map₂_coe_coe x y (fun x y : X => x ⊔ y) uniformContinuous₂_sup_completion]348349/-- The inclusion of a normed vector lattice into its completion preserves infima. -/350@[norm_cast]351theorem coe_inf_completion (x y : X) :352 ((x ⊓ y : X) : Completion X) = (x : Completion X) ⊓ (y : Completion X) := by353 rw [show (x : Completion X) ⊓ (y : Completion X) =354 Completion.map₂ (fun x y : X => x ⊓ y) x y from rfl,355 Completion.map₂_coe_coe x y (fun x y : X => x ⊓ y) uniformContinuous₂_inf_completion]356357/-- The inclusion of a normed vector lattice into its completion preserves absolute values. -/358@[norm_cast]359theorem coe_abs_completion (x : X) :360 ((|x| : X) : Completion X) = |(x : Completion X)| := by361 rw [abs, abs, ← Completion.coe_neg, ← coe_sup_completion]362363private theorem completion_sup_add (x y z : Completion X) :364 (x + z) ⊔ (y + z) = (x ⊔ y) + z := by365 refine Completion.induction_on₃ x y z ?_ ?_366 · exact isClosed_eq367 (Completion.continuous_map₂368 (Completion.continuous_map₂ continuous_fst (continuous_snd.comp continuous_snd))369 (Completion.continuous_map₂ (continuous_fst.comp continuous_snd)370 (continuous_snd.comp continuous_snd)))371 (Completion.continuous_map₂372 (Completion.continuous_map₂ continuous_fst (continuous_fst.comp continuous_snd))373 (continuous_snd.comp continuous_snd))374 · intro x y z375 rw [← Completion.coe_add, ← Completion.coe_add, ← coe_sup_completion,376 ← coe_sup_completion, ← Completion.coe_add, add_comm x z, add_comm y z,377 add_comm (x ⊔ y) z, ← add_sup]378379/-- The order on the completion of a normed vector lattice is compatible with addition. -/380noncomputable instance instIsOrderedAddMonoidCompletion :381 IsOrderedAddMonoid (Completion X) := by382 refine383 { add_le_add_left := fun x y hxy z => ?_384 add_le_add_right := fun x y hxy z => ?_ }385 · rw [← sup_eq_right] at hxy ⊢386 rw [completion_sup_add, hxy]387 · rw [← sup_eq_right] at hxy ⊢388 rw [add_comm z x, add_comm z y, completion_sup_add, hxy]389390private theorem completion_smul_sup_of_nonneg {r : ℝ} (hr : 0 ≤ r)391 (x y : Completion X) : r • (x ⊔ y) = r • x ⊔ r • y := by392 refine Completion.induction_on₂ x y ?_ ?_393 · exact isClosed_eq394 ((Completion.continuous_map₂ continuous_fst continuous_snd).const_smul r)395 (Completion.continuous_map₂ (continuous_fst.const_smul r) (continuous_snd.const_smul r))396 · intro x y397 rw [← coe_sup_completion, ← Completion.coe_smul, ← Completion.coe_smul,398 ← Completion.coe_smul, ← coe_sup_completion, nonneg_smul_sup x y r hr]399400noncomputable instance instVectorLatticeCompletion : VectorLattice (Completion X) where401 smul_le_smul_of_nonneg_left := by402 intro r hr x y hxy403 rw [← sup_eq_right] at hxy ⊢404 rw [← completion_smul_sup_of_nonneg hr, hxy]405406private theorem continuous_sup_completion :407 Continuous fun p : Completion X × Completion X => p.1 ⊔ p.2 :=408 Completion.continuous_map₂ continuous_fst continuous_snd409410private theorem continuous_inf_completion :411 Continuous fun p : Completion X × Completion X => p.1 ⊓ p.2 :=412 Completion.continuous_map₂ continuous_fst continuous_snd413414private theorem continuous_abs_completion :415 Continuous (|·| : Completion X → Completion X) := by416 change Continuous fun x : Completion X ↦ x ⊔ -x417 exact (continuous_sup_completion.comp (continuous_id.prodMk continuous_neg)).congr fun x ↦ by418 rw [Function.comp_apply, id_eq]419420omit [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] in421private lemma exists_seq_coe_tendsto (a : Completion X) :422 ∃ u : ℕ → X, Filter.Tendsto (fun n => ((u n : Completion X))) Filter.atTop (nhds a) := by423 have ha : a ∈ closure (Set.range ((↑) : X → Completion X)) := by424 rw [(Completion.denseRange_coe (α := X)).closure_range]425 exact Set.mem_univ a426 obtain ⟨x, hxr, hxl⟩ := mem_closure_iff_seq_limit.mp ha427 choose u hu using hxr428 exact ⟨u, by simpa only [hu] using hxl⟩429430/-- The completion of a normed vector lattice has a solid norm. -/431noncomputable instance instHasSolidNormCompletion : HasSolidNorm (Completion X) where432 solid := by433 intro a b hab434 have ha_le : a ≤ |b| := (abs_le'.mp hab).1435 have ha_ge : -|b| ≤ a := neg_le.mp (abs_le'.mp hab).2436 obtain ⟨u, hu⟩ := exists_seq_coe_tendsto a437 obtain ⟨v, hv⟩ := exists_seq_coe_tendsto b438 have hclampcont : Continuous fun p : Completion X × Completion X =>439 (p.1 ⊔ -|p.2|) ⊓ |p.2| := by440 have habs2 : Continuous fun p : Completion X × Completion X => |p.2| :=441 continuous_abs_completion.comp continuous_snd442 have hsup : Continuous fun p : Completion X × Completion X => p.1 ⊔ -|p.2| :=443 continuous_sup_completion.comp (continuous_fst.prodMk habs2.neg)444 exact continuous_inf_completion.comp (hsup.prodMk habs2)445 have hcoe : ∀ n, ((((u n ⊔ -|v n|) ⊓ |v n| : X)) : Completion X)446 = (↑(u n) ⊔ -|↑(v n)|) ⊓ |↑(v n)| := fun n => by447 rw [coe_inf_completion, coe_sup_completion, Completion.coe_neg, coe_abs_completion]448 have hprod : Filter.Tendsto (fun n => ((↑(u n), ↑(v n)) : Completion X × Completion X))449 Filter.atTop (nhds (a, b)) := hu.prodMk_nhds hv450 have hclamp : Filter.Tendsto (fun n => (↑(u n) ⊔ -|↑(v n)|) ⊓ |↑(v n)|)451 Filter.atTop (nhds ((a ⊔ -|b|) ⊓ |b|)) := (hclampcont.tendsto (a, b)).comp hprod452 rw [sup_eq_left.mpr ha_ge, inf_eq_left.mpr ha_le] at hclamp453 have hwlim : Filter.Tendsto454 (fun n => (((u n ⊔ -|v n|) ⊓ |v n| : X) : Completion X)) Filter.atTop (nhds a) := by455 simpa only [hcoe] using hclamp456 have hnorm_w : Filter.Tendsto457 (fun n => ‖(((u n ⊔ -|v n|) ⊓ |v n| : X) : Completion X)‖) Filter.atTop (nhds ‖a‖) :=458 (continuous_norm.tendsto a).comp hwlim459 have hnorm_v : Filter.Tendsto (fun n => ‖((v n : Completion X))‖) Filter.atTop (nhds ‖b‖) :=460 (continuous_norm.tendsto b).comp hv461 refine le_of_tendsto_of_tendsto' hnorm_w hnorm_v (fun n => ?_)462 rw [Completion.norm_coe, Completion.norm_coe]463 refine HasSolidNorm.solid ?_464 have hc_le : (u n ⊔ -|v n|) ⊓ |v n| ≤ |v n| := inf_le_right465 have hneg_le : -|v n| ≤ (u n ⊔ -|v n|) ⊓ |v n| :=466 le_inf le_sup_right (le_trans (neg_nonpos_of_nonneg (abs_nonneg (v n))) (abs_nonneg (v n)))467 rw [abs_le']468 exact ⟨hc_le, by rwa [neg_le]⟩469470/-- The completion of a normed vector lattice is a normed vector lattice. -/471noncomputable instance instNormedVectorLatticeCompletion :472 NormedVectorLattice (Completion X) where473474/-- **The completion of a normed vector lattice is a Banach lattice.** -/475noncomputable instance instBanachLatticeCompletion : BanachLattice (Completion X) where476477/-- The canonical inclusion into the completion preserves the isometry to `toComplₗᵢ`; it is478an isometry from `X` into its completion. -/479theorem isometry_coe_completion : Isometry ((↑) : X → Completion X) := by480 rw [← Completion.coe_toComplₗᵢ (𝕜 := ℝ)]481 exact (Completion.toComplₗᵢ (𝕜 := ℝ)).isometry482483end Completion484