feat(analysis/normed/order/lattice): add has_solid_norm (#18554)

See [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Solid)

Co-authored-by: Yaël Dillies

Author: xroblot

src/algebra/order/lattice_group.lean

@@ -7,6 +7,8 @@ import algebra.group_power.basic -- Needed for squares
 import algebra.order.group.abs
 import tactic.nth_rewrite
 
+import order.closure
+
 /-!
 # Lattice ordered groups
 
@@ -454,3 +456,26 @@ begin
 end
 
 end lattice_ordered_comm_group
+
+namespace lattice_ordered_add_comm_group
+
+variables {β : Type u} [lattice β] [add_comm_group β]
+
+section solid
+
+/-- A subset `s ⊆ β`, with `β` an `add_comm_group` with a `lattice` structure, is solid if for
+all `x ∈ s` and all `y ∈ β` such that `|y| ≤ |x|`, then `y ∈ s`. -/
+def is_solid (s : set β) : Prop := ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, |y| ≤ |x| → y ∈ s
+
+/-- The solid closure of a subset `s` is the smallest superset of `s` that is solid. -/
+def solid_closure (s : set β) : set β := {y | ∃ x ∈ s, |y| ≤ |x|}
+
+lemma is_solid_solid_closure (s : set β) : is_solid (solid_closure s) :=
+λ x ⟨y, hy, hxy⟩ z hzx, ⟨y, hy, hzx.trans hxy⟩
+
+lemma solid_closure_min (s t : set β) (h1 : s ⊆ t) (h2 : is_solid t) : solid_closure s ⊆ t :=
+λ _ ⟨_, hy, hxy⟩, h2 (h1 hy) hxy
+
+end solid
+
+end lattice_ordered_add_comm_group

src/analysis/normed/order/lattice.lean

@@ -31,30 +31,48 @@ normed, lattice, ordered, group
 -/
 
 /-!
-### Normed lattice orderd groups
+### Normed lattice ordered groups
 
 Motivated by the theory of Banach Lattices, this section introduces normed lattice ordered groups.
 -/
 
 local notation (name := abs) `|`a`|` := abs a
 
+section solid_norm
+
+/-- Let `α` be an `add_comm_group` with a `lattice` structure. A norm on `α` is *solid* if, for `a`
+and `b` in `α`, with absolute values `|a|` and `|b|` respectively, `|a| ≤ |b|` implies `‖a‖ ≤ ‖b‖`.
+-/
+class has_solid_norm (α : Type*) [normed_add_comm_group α] [lattice α] : Prop :=
+(solid : ∀ ⦃x y : α⦄, |x| ≤ |y| → ‖x‖ ≤ ‖y‖)
+
+variables {α : Type*} [normed_add_comm_group α] [lattice α] [has_solid_norm α]
+
+lemma norm_le_norm_of_abs_le_abs  {a b : α} (h : |a| ≤ |b|) : ‖a‖ ≤ ‖b‖ := has_solid_norm.solid h
+
+/-- If `α` has a solid norm, then the balls centered at the origin of `α` are solid sets. -/
+lemma lattice_ordered_add_comm_group.is_solid_ball (r : ℝ) :
+  lattice_ordered_add_comm_group.is_solid (metric.ball (0 : α) r) :=
+λ _ hx _ hxy, mem_ball_zero_iff.mpr ((has_solid_norm.solid hxy).trans_lt (mem_ball_zero_iff.mp hx))
+
+instance : has_solid_norm ℝ := ⟨λ _ _, id⟩
+
+instance : has_solid_norm ℚ := ⟨λ _ _ _, by simpa only [norm, ← rat.cast_abs, rat.cast_le]⟩
+
+end solid_norm
+
 /--
 Let `α` be a normed commutative group equipped with a partial order covariant with addition, with
 respect which `α` forms a lattice. Suppose that `α` is *solid*, that is to say, for `a` and `b` in
 `α`, with absolute values `|a|` and `|b|` respectively, `|a| ≤ |b|` implies `‖a‖ ≤ ‖b‖`. Then `α` is
 said to be a normed lattice ordered group.
 -/
 class normed_lattice_add_comm_group (α : Type*)
-  extends normed_add_comm_group α, lattice α :=
+  extends normed_add_comm_group α, lattice α, has_solid_norm α :=
 (add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
-(solid : ∀ a b : α, |a| ≤ |b| → ‖a‖ ≤ ‖b‖)
-
-lemma solid {α : Type*} [normed_lattice_add_comm_group α] {a b : α} (h : |a| ≤ |b|) : ‖a‖ ≤ ‖b‖ :=
-normed_lattice_add_comm_group.solid a b h
 
 instance : normed_lattice_add_comm_group ℝ :=
-{ add_le_add_left := λ _ _ h _, add_le_add le_rfl h,
-  solid := λ _ _, id, }
+{ add_le_add_left := λ _ _ h _, add_le_add le_rfl h,}
 
 /--
 A normed lattice ordered group is an ordered additive commutative group
@@ -64,7 +82,7 @@ instance normed_lattice_add_comm_group_to_ordered_add_comm_group {α : Type*}
   [h : normed_lattice_add_comm_group α] : ordered_add_comm_group α := { ..h }
 
 variables {α : Type*} [normed_lattice_add_comm_group α]
-open lattice_ordered_comm_group
+open lattice_ordered_comm_group has_solid_norm
 
 lemma dual_solid (a b : α) (h: b⊓-b ≤ a⊓-a) : ‖a‖ ≤ ‖b‖ :=
 begin

src/measure_theory/function/lp_order.lean

@@ -94,7 +94,7 @@ instance [fact (1 ≤ p)] : normed_lattice_add_comm_group (Lp E p μ) :=
     refine snorm_mono_ae _,
     filter_upwards [hfg, Lp.coe_fn_abs f, Lp.coe_fn_abs g] with x hx hxf hxg,
     rw [hxf, hxg] at hx,
-    exact solid hx,
+    exact has_solid_norm.solid hx,
   end,
   ..Lp.lattice, ..Lp.normed_add_comm_group, }
 

src/topology/continuous_function/bounded.lean

@@ -1328,7 +1328,7 @@ instance : normed_lattice_add_comm_group (α →ᵇ β) :=
   solid :=
   begin
     intros f g h,
-    have i1: ∀ t, ‖f t‖ ≤ ‖g t‖ := λ t, solid (h t),
+    have i1: ∀ t, ‖f t‖ ≤ ‖g t‖ := λ t, has_solid_norm.solid (h t),
     rw norm_le (norm_nonneg _),
     exact λ t, (i1 t).trans (norm_coe_le_norm g t),
   end,