feat(topology/continuous_function/bounded): continuous bounded real-valued functions form a normed vector lattice (#10322)

feat(topology/continuous_function/bounded): continuous bounded real-valued functions form a normed vector lattice



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

Author: mans0954

src/analysis/normed_space/lattice_ordered_group.lean

@@ -49,6 +49,9 @@ class normed_lattice_add_comm_group (α : Type*)
 lemma solid {α : Type*} [normed_lattice_add_comm_group α] {a b : α} (h : |a| ≤ |b|) : ∥a∥ ≤ ∥b∥ :=
 normed_lattice_add_comm_group.solid a b h
 
+noncomputable instance : normed_lattice_add_comm_group ℝ :=
+{ add_le_add_left := λ _ _ h _, add_le_add le_rfl h,
+  solid := λ _ _, id, }
 /--
 A normed lattice ordered group is an ordered additive commutative group
 -/
@@ -114,6 +117,21 @@ begin
         exact abs_inf_sub_inf_le_abs _ _ _, } },
 end
 
+lemma norm_sup_sub_sup_le_add_norm (a b c d : α) : ∥a ⊔ b - (c ⊔ d)∥ ≤ ∥a - c∥ + ∥b - d∥ :=
+begin
+  rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)],
+  refine le_trans (solid _) (norm_add_le (|a - c|) (|b - d|)),
+  rw abs_of_nonneg (|a - c| + |b - d|) (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d))),
+  calc |a ⊔ b - (c ⊔ d)| =
+    |a ⊔ b - (c ⊔ b) + (c ⊔ b - (c ⊔ d))| : by rw sub_add_sub_cancel
+  ... ≤ |a ⊔ b - (c ⊔ b)| + |c ⊔ b - (c ⊔ d)| : abs_add_le _ _
+  ... ≤ |a -c| + |b - d| : by
+    { apply add_le_add,
+      { exact abs_sup_sub_sup_le_abs _ _ _, },
+      { rw [@sup_comm _ _ c, @sup_comm _ _ c],
+        exact abs_sup_sub_sup_le_abs _ _ _, } },
+end
+
 /--
 Let `α` be a normed lattice ordered group. Then the infimum is jointly continuous.
 -/
@@ -139,41 +157,3 @@ topological_lattice.mk
 lemma norm_abs_sub_abs (a b : α) :
   ∥ |a| - |b| ∥ ≤ ∥a-b∥ :=
 solid (lattice_ordered_comm_group.abs_abs_sub_abs_le _ _)
-
-lemma norm_two_inf_sub_two_inf_le (a b c d : α) :
-  ∥2•(a⊓b)-2•(c⊓d)∥ ≤ 2*∥a - c∥ + 2*∥b - d∥ :=
-calc ∥2•(a⊓b) - 2•(c⊓d)∥ = ∥(a + b - |b - a|) - (c + d - |d - c|)∥ :
-    by rw [lattice_ordered_comm_group.two_inf_eq_add_sub_abs_sub,
-      lattice_ordered_comm_group.two_inf_eq_add_sub_abs_sub]
-  ... = ∥(a + b - |b - a|) - c - d + |d - c|∥      : by abel
-  ... = ∥(a - c + (b - d))  + (|d - c| - |b - a|)∥ : by abel
-  ... ≤ ∥a - c + (b - d)∥ + ∥|d - c| - |b - a|∥    :
-    by apply norm_add_le (a - c + (b - d)) (|d - c| - |b - a|)
-  ... ≤ (∥a - c∥ + ∥b - d∥) + ∥|d - c| - |b - a|∥   : by exact add_le_add_right (norm_add_le _ _) _
-  ... ≤ (∥a - c∥ + ∥b - d∥) + ∥ d - c - (b - a) ∥   :
-    by exact add_le_add_left (norm_abs_sub_abs _ _) _
-  ... = (∥a - c∥ + ∥b - d∥) + ∥ a - c - (b - d) ∥ :
-    by { rw [sub_sub_assoc_swap, sub_sub_assoc_swap, add_comm (a-c), ← add_sub_assoc], simp, abel, }
-  ... ≤ (∥a - c∥ + ∥b - d∥) + (∥ a - c ∥ + ∥ b - d ∥) :
-    by apply add_le_add_left (norm_sub_le (a-c) (b-d) )
-  ... = 2*∥a - c∥ + 2*∥b - d∥ :
-    by { ring, }
-
-lemma norm_two_sup_sub_two_sup_le (a b c d : α) :
-  ∥2•(a⊔b)-2•(c⊔d)∥ ≤ 2*∥a - c∥ + 2*∥b - d∥ :=
-calc ∥2•(a⊔b) - 2•(c⊔d)∥ = ∥(a + b + |b - a|) - (c + d + |d - c|)∥ :
-    by rw [lattice_ordered_comm_group.two_sup_eq_add_add_abs_sub,
-      lattice_ordered_comm_group.two_sup_eq_add_add_abs_sub]
-  ... = ∥(a + b + |b - a|) - c - d - |d - c|∥      : by abel
-  ... = ∥(a - c + (b - d))  + (|b - a| - |d - c|)∥ : by abel
-  ... ≤ ∥a - c + (b - d)∥ + ∥|b - a| - |d - c|∥    :
-    by apply norm_add_le (a - c + (b - d)) (|b - a| - |d - c|)
-  ... ≤ (∥a - c∥ + ∥b - d∥) + ∥|b - a| - |d - c|∥   : by exact add_le_add_right (norm_add_le _ _) _
-  ... ≤ (∥a - c∥ + ∥b - d∥) + ∥ b - a - (d - c) ∥   :
-    by exact add_le_add_left (norm_abs_sub_abs _ _) _
-  ... = (∥a - c∥ + ∥b - d∥) + ∥ b - d - (a - c) ∥ :
-    by { rw [sub_sub_assoc_swap, sub_sub_assoc_swap, add_comm (b-d), ← add_sub_assoc], simp, abel, }
-  ... ≤ (∥a - c∥ + ∥b - d∥) + (∥ b - d ∥ + ∥ a - c ∥) :
-    by apply add_le_add_left (norm_sub_le (b-d) (a-c)  )
-  ... = 2*∥a - c∥ + 2*∥b - d∥ :
-    by { ring, }

src/topology/continuous_function/bounded.lean

@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel, Mario Carneiro, Yury Kudryashov, Heather Macbeth
 -/
 import analysis.normed_space.operator_norm
 import topology.continuous_function.algebra
+import analysis.normed_space.lattice_ordered_group
 
 /-!
 # Bounded continuous functions
@@ -1017,4 +1018,72 @@ module over the algebra of bounded continuous functions from `α` to `𝕜`. -/
 
 end normed_algebra
 
+section normed_lattice_ordered_group
+
+variables [topological_space α] [normed_lattice_add_comm_group β]
+
+instance : partial_order (α →ᵇ β) := partial_order.lift (λ f, f.to_fun) (by tidy)
+
+/--
+Continuous normed lattice group valued functions form a meet-semilattice
+-/
+instance : semilattice_inf (α →ᵇ β) :=
+{ inf := λ f g,
+  { to_fun := λ t, f t ⊓ g t,
+    continuous_to_fun := f.continuous.inf g.continuous,
+    bounded' := begin
+      cases f.bounded' with C₁ hf,
+      cases g.bounded' with C₂ hg,
+      refine ⟨C₁ + C₂, λ x y, _⟩,
+      simp_rw normed_group.dist_eq at hf hg ⊢,
+      exact (norm_inf_sub_inf_le_add_norm _ _ _ _).trans (add_le_add (hf _ _) (hg _ _)),
+    end },
+  inf_le_left := λ f g, continuous_map.le_def.mpr (λ _, inf_le_left),
+  inf_le_right := λ f g, continuous_map.le_def.mpr (λ _, inf_le_right),
+  le_inf := λ f g₁ g₂ w₁ w₂, continuous_map.le_def.mpr (λ _, le_inf (continuous_map.le_def.mp w₁ _)
+    (continuous_map.le_def.mp w₂ _)),
+  ..bounded_continuous_function.partial_order }
+
+instance : semilattice_sup (α →ᵇ β) :=
+{ sup := λ f g,
+  { to_fun := λ t, f t ⊔ g t,
+    continuous_to_fun := f.continuous.sup g.continuous,
+    bounded' := begin
+      cases f.bounded' with C₁ hf,
+      cases g.bounded' with C₂ hg,
+      refine ⟨C₁ + C₂, λ x y, _⟩,
+      simp_rw normed_group.dist_eq at hf hg ⊢,
+      exact (norm_sup_sub_sup_le_add_norm _ _ _ _).trans (add_le_add (hf _ _) (hg _ _)),
+    end },
+  le_sup_left := λ f g, continuous_map.le_def.mpr (λ _, le_sup_left),
+  le_sup_right := λ f g, continuous_map.le_def.mpr (λ _, le_sup_right),
+  sup_le := λ f g₁ g₂ w₁ w₂, continuous_map.le_def.mpr (λ _, sup_le (continuous_map.le_def.mp w₁ _)
+    (continuous_map.le_def.mp w₂ _)),
+  ..bounded_continuous_function.partial_order }
+
+instance  : lattice (α →ᵇ β) :=
+{ .. bounded_continuous_function.semilattice_sup, .. bounded_continuous_function.semilattice_inf }
+
+@[simp] lemma coe_fn_sup (f g : α →ᵇ β) : ⇑(f ⊔ g) = f ⊔ g := rfl
+
+@[simp] lemma coe_fn_abs (f : α →ᵇ β) : ⇑|f| = |f| := rfl
+
+instance : normed_lattice_add_comm_group (α →ᵇ β) :=
+{ add_le_add_left := begin
+    intros f g h₁ h t,
+    simp only [coe_to_continuous_fun, pi.add_apply, add_le_add_iff_left, coe_add,
+      continuous_map.to_fun_eq_coe],
+    exact h₁ _,
+  end,
+  solid :=
+  begin
+    intros f g h,
+    have i1: ∀ t, ∥f t∥ ≤ ∥g t∥ := λ t, solid (h t),
+    rw norm_le (norm_nonneg _),
+    exact λ t, (i1 t).trans (norm_coe_le_norm g t),
+  end,
+  ..bounded_continuous_function.lattice, }
+
+end normed_lattice_ordered_group
+
 end bounded_continuous_function