feat(analysis/normed/group/seminorm): Group norms (#16237)

Define (additive) group norms, which are group seminorms `f` such that `f x = 0 → x = 0` (resp. `f x = 0 → x = 1`), along with their hom classes.

src/analysis/normed/group/seminorm.lean

@@ -9,23 +9,25 @@ import data.real.nnreal
 /-!
 # Group seminorms
 
-This file defines seminorms in a group. A group seminorm is a function to the reals which is
-positive-semidefinite and subadditive.
+This file defines norms and seminorms in a group. A group seminorm is a function to the reals which
+is positive-semidefinite and subadditive. A norm further only maps zero to zero.
 
 ## Main declarations
 
 * `add_group_seminorm`: A function `f` from an additive group `G` to the reals that preserves zero,
   takes nonnegative values, is subadditive and such that `f (-x) = f x` for all `x`.
 * `group_seminorm`: A function `f` from a group `G` to the reals that sends one to zero, takes
   nonnegative values, is submultiplicative and such that `f x⁻¹ = f x` for all `x`.
+* `add_group_norm`: A seminorm `f` such that `f x = 0 → x = 0` for all `x`.
+* `group_norm`: A seminorm `f` such that `f x = 0 → x = 1` for all `x`.
 
 ## References
 
 * [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966]
 
 ## Tags
 
-seminorm
+norm, seminorm
 -/
 
 set_option old_structure_cmd true
@@ -50,7 +52,20 @@ structure group_seminorm (G : Type*) [group G] :=
 (mul_le' : ∀ x y, to_fun (x * y) ≤ to_fun x + to_fun y)
 (inv' : ∀ x, to_fun x⁻¹ = to_fun x)
 
-attribute [nolint doc_blame] add_group_seminorm.to_zero_hom
+/-- A norm on an additive group `G` is a function `f : G → ℝ` that preserves zero, is subadditive
+and such that `f (-x) = f x` and `f x = 0 → x = 0` for all `x`. -/
+@[protect_proj]
+structure add_group_norm (G : Type*) [add_group G] extends add_group_seminorm G :=
+(eq_zero_of_map_eq_zero' : ∀ x, to_fun x = 0 → x = 0)
+
+/-- A seminorm on a group `G` is a function `f : G → ℝ` that sends one to zero, is submultiplicative
+and such that `f x⁻¹ = f x` and `f x = 0 → x = 1` for all `x`. -/
+@[protect_proj, to_additive]
+structure group_norm (G : Type*) [group G] extends group_seminorm G :=
+(eq_one_of_map_eq_zero' : ∀ x, to_fun x = 0 → x = 1)
+
+attribute [nolint doc_blame] add_group_seminorm.to_zero_hom  add_group_norm.to_add_group_seminorm
+  group_norm.to_group_seminorm
 
 /-- `add_group_seminorm_class F α` states that `F` is a type of seminorms on the additive group `α`.
 
@@ -69,21 +84,39 @@ class group_seminorm_class (F : Type*) (α : out_param $ Type*) [group α]
 (map_one_eq_zero (f : F) : f 1 = 0)
 (map_inv_eq_map (f : F) (a : α) : f a⁻¹ = f a)
 
-attribute [to_additive] group_seminorm_class.to_mul_le_add_hom_class
+/-- `add_group_norm_class F α` states that `F` is a type of norms on the additive group `α`.
+
+You should extend this class when you extend `add_group_norm`. -/
+class add_group_norm_class (F : Type*) (α : out_param $ Type*) [add_group α]
+  extends add_group_seminorm_class F α :=
+(eq_zero_of_map_eq_zero (f : F) {a : α} : f a = 0 → a = 0)
+
+/-- `group_norm_class F α` states that `F` is a type of norms on the group `α`.
+
+You should extend this class when you extend `group_norm`. -/
+@[to_additive]
+class group_norm_class (F : Type*) (α : out_param $ Type*) [group α]
+  extends group_seminorm_class F α :=
+(eq_one_of_map_eq_zero (f : F) {a : α} : f a = 0 → a = 1)
 
 export add_group_seminorm_class (map_neg_eq_map)
-export group_seminorm_class (map_one_eq_zero map_inv_eq_map)
+       group_seminorm_class     (map_one_eq_zero map_inv_eq_map)
+       add_group_norm_class     (eq_zero_of_map_eq_zero)
+       group_norm_class         (eq_one_of_map_eq_zero)
 
 attribute [simp, to_additive map_zero] map_one_eq_zero
 attribute [simp] map_neg_eq_map
 attribute [simp, to_additive] map_inv_eq_map
+attribute [to_additive] group_seminorm_class.to_mul_le_add_hom_class
+attribute [to_additive] group_norm.to_group_seminorm
+attribute [to_additive] group_norm_class.to_group_seminorm_class
 
 @[priority 100] -- See note [lower instance priority]
 instance add_group_seminorm_class.to_zero_hom_class [add_group E] [add_group_seminorm_class F E] :
   zero_hom_class F E ℝ :=
 { ..‹add_group_seminorm_class F E› }
 
-section group
+section group_seminorm_class
 variables [group E] [group_seminorm_class F E] (f : F) (x y : E)
 include E
 
@@ -95,7 +128,7 @@ by { rw [div_eq_mul_inv, ←map_inv_eq_map f y], exact map_mul_le_add _ _ _ }
 @[to_additive] lemma le_map_add_map_div' : f x ≤ f y + f (y / x) :=
 by simpa only [add_comm, map_div_rev, div_mul_cancel'] using map_mul_le_add f (x / y) y
 
-end group
+end group_seminorm_class
 
 @[to_additive, priority 100] -- See note [lower instance priority]
 instance group_seminorm_class.to_nonneg_hom_class [group E] [group_seminorm_class F E] :
@@ -104,6 +137,22 @@ instance group_seminorm_class.to_nonneg_hom_class [group E] [group_seminorm_clas
     (by { rw [two_mul, ←map_one_eq_zero f, ←div_self' a], exact map_div_le_add _ _ _ }) two_pos,
   ..‹group_seminorm_class F E› }
 
+section group_norm_class
+variables [group E] [group_norm_class F E] (f : F) {x : E}
+include E
+
+@[to_additive] lemma map_pos_of_ne_one (hx : x ≠ 1) : 0 < f x :=
+(map_nonneg _ _).lt_of_ne $ λ h, hx $ eq_one_of_map_eq_zero _ h.symm
+
+@[simp, to_additive] lemma map_eq_zero_iff_eq_one : f x = 0 ↔ x = 1 :=
+⟨eq_one_of_map_eq_zero _, by { rintro rfl, exact map_one_eq_zero _ }⟩
+
+@[to_additive] lemma map_ne_zero_iff_ne_one : f x ≠ 0 ↔ x ≠ 1 := (map_eq_zero_iff_eq_one _).not
+
+end group_norm_class
+
+/-! ### Seminorms -/
+
 namespace group_seminorm
 section group
 variables [group E] [group F] [group G] {p q : group_seminorm E}
@@ -205,7 +254,7 @@ variables [comm_group E] [comm_group F] (p q : group_seminorm E) (x y : E)
 @[to_additive] lemma comp_mul_le (f g : F →* E) : p.comp (f * g) ≤ p.comp f + p.comp g :=
 λ _, map_mul_le_add p _ _
 
-@[to_additive] private lemma mul_bdd_below_range_add {p q : group_seminorm E} {x : E} :
+@[to_additive] lemma mul_bdd_below_range_add {p q : group_seminorm E} {x : E} :
   bdd_below (range $ λ y, p y + q (x / y)) :=
 ⟨0, by { rintro _ ⟨x, rfl⟩, exact add_nonneg (map_nonneg p _) (map_nonneg q _) }⟩
 
@@ -245,6 +294,20 @@ namespace add_group_seminorm
 variables [add_group E] [has_smul R ℝ] [has_smul R ℝ≥0] [is_scalar_tower R ℝ≥0 ℝ]
   (p : add_group_seminorm E)
 
+instance [decidable_eq E] : has_one (add_group_seminorm E) :=
+⟨{ to_fun := λ x, if x = 0 then 0 else 1,
+  map_zero' := if_pos rfl,
+  add_le' := λ x y, begin
+    by_cases hx : x = 0,
+    { rw [if_pos hx, hx, zero_add, zero_add] },
+    { rw if_neg hx,
+      refine le_add_of_le_of_nonneg _ _; split_ifs; norm_num }
+  end,
+  neg' := λ x, by simp_rw neg_eq_zero }⟩
+
+@[simp] lemma apply_one [decidable_eq E] (x : E) :
+  (1 : add_group_seminorm E) x = if x = 0 then 0 else 1 := rfl
+
 /-- Any action on `ℝ` which factors through `ℝ≥0` applies to an `add_group_seminorm`. -/
 instance : has_smul R (add_group_seminorm E) :=
 ⟨λ r p,
@@ -277,6 +340,21 @@ end add_group_seminorm
 namespace group_seminorm
 variables [group E] [has_smul R ℝ] [has_smul R ℝ≥0] [is_scalar_tower R ℝ≥0 ℝ]
 
+@[to_additive add_group_seminorm.has_one]
+instance [decidable_eq E] : has_one (group_seminorm E) :=
+⟨{ to_fun := λ x, if x = 1 then 0 else 1,
+  map_one' := if_pos rfl,
+  mul_le' := λ x y, begin
+    by_cases hx : x = 1,
+    { rw [if_pos hx, hx, one_mul, zero_add] },
+    { rw if_neg hx,
+      refine le_add_of_le_of_nonneg _ _; split_ifs; norm_num }
+  end,
+  inv' := λ x, by simp_rw inv_eq_one }⟩
+
+@[simp, to_additive add_group_seminorm.apply_one] lemma apply_one [decidable_eq E] (x : E) :
+  (1 : group_seminorm E) x = if x = 1 then 0 else 1 := rfl
+
 /-- Any action on `ℝ` which factors through `ℝ≥0` applies to an `add_group_seminorm`. -/
 @[to_additive add_group_seminorm.has_smul] instance : has_smul R (group_seminorm E) :=
 ⟨λ r p,
@@ -309,3 +387,87 @@ from λ x y, by simpa only [←smul_eq_mul, ←nnreal.smul_def, smul_one_smul 
 ext $ λ x, real.smul_max _ _
 
 end group_seminorm
+
+/-! ### Norms -/
+
+namespace group_norm
+section group
+variables [group E] [group F] [group G] {p q : group_norm E}
+
+@[to_additive] instance group_norm_class : group_norm_class (group_norm E) E :=
+{ coe := λ f, f.to_fun,
+  coe_injective' := λ f g h, by cases f; cases g; congr',
+  map_one_eq_zero := λ f, f.map_one',
+  map_mul_le_add := λ f, f.mul_le',
+  map_inv_eq_map := λ f, f.inv',
+  eq_one_of_map_eq_zero := λ f, f.eq_one_of_map_eq_zero' }
+
+/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
+directly. -/
+@[to_additive "Helper instance for when there's too many metavariables to apply
+`fun_like.has_coe_to_fun` directly. "]
+instance : has_coe_to_fun (group_norm E) (λ _, E → ℝ) := fun_like.has_coe_to_fun
+
+@[ext, to_additive] lemma ext : (∀ x, p x = q x) → p = q := fun_like.ext p q
+
+@[to_additive] instance : partial_order (group_norm E) :=
+partial_order.lift _ fun_like.coe_injective
+
+@[to_additive] lemma le_def : p ≤ q ↔ (p : E → ℝ) ≤ q := iff.rfl
+@[to_additive] lemma lt_def : p < q ↔ (p : E → ℝ) < q := iff.rfl
+
+@[simp, to_additive] lemma coe_le_coe : (p : E → ℝ) ≤ q ↔ p ≤ q := iff.rfl
+@[simp, to_additive] lemma coe_lt_coe : (p : E → ℝ) < q ↔ p < q := iff.rfl
+
+variables (p q) (f : F →* E)
+
+@[to_additive] instance : has_add (group_norm E) :=
+⟨λ p q, { eq_one_of_map_eq_zero' := λ x hx, of_not_not $ λ h,
+            hx.not_gt $ add_pos (map_pos_of_ne_one p h) (map_pos_of_ne_one q h),
+          ..p.to_group_seminorm + q.to_group_seminorm }⟩
+
+@[simp, to_additive] lemma coe_add : ⇑(p + q) = p + q := rfl
+@[simp, to_additive] lemma add_apply (x : E) : (p + q) x = p x + q x := rfl
+
+-- TODO: define `has_Sup`
+@[to_additive] noncomputable instance : has_sup (group_norm E) :=
+⟨λ p q,
+  { eq_one_of_map_eq_zero' := λ x hx, of_not_not $ λ h, hx.not_gt $
+      lt_sup_iff.2 $ or.inl $ map_pos_of_ne_one p h,
+    ..p.to_group_seminorm ⊔ q.to_group_seminorm }⟩
+
+@[simp, to_additive] lemma coe_sup : ⇑(p ⊔ q) = p ⊔ q := rfl
+@[simp, to_additive] lemma sup_apply (x : E) : (p ⊔ q) x = p x ⊔ q x := rfl
+
+@[to_additive] noncomputable instance : semilattice_sup (group_norm E) :=
+fun_like.coe_injective.semilattice_sup _ coe_sup
+
+end group
+end group_norm
+
+namespace add_group_norm
+variables [add_group E] [decidable_eq E]
+
+instance : has_one (add_group_norm E) :=
+⟨{ eq_zero_of_map_eq_zero' := λ x, zero_ne_one.ite_eq_left_iff.1,
+  ..(1 : add_group_seminorm E) }⟩
+
+@[simp] lemma apply_one (x : E) : (1 : add_group_norm E) x = if x = 0 then 0 else 1 := rfl
+
+instance : inhabited (add_group_norm E) := ⟨1⟩
+
+end add_group_norm
+
+namespace group_norm
+variables [group E] [decidable_eq E]
+
+@[to_additive add_group_norm.has_one] instance : has_one (group_norm E) :=
+⟨{ eq_one_of_map_eq_zero' := λ x, zero_ne_one.ite_eq_left_iff.1,
+  ..(1 : group_seminorm E) }⟩
+
+@[simp, to_additive add_group_norm.apply_one]
+lemma apply_one (x : E) : (1 : group_norm E) x = if x = 1 then 0 else 1 := rfl
+
+@[to_additive] instance : inhabited (group_norm E) := ⟨1⟩
+
+end group_norm