refactor(analysis/normed/group/basic): Replace normed_add_comm_group.core with group norms (#16238)

Delete `seminormed_add_comm_group.core`/`normed_add_comm_group.core` in favor of `add_group_norm`/`group_norm`. The former are unbundled prop versions of the latter, specialized to `∥ ∥`.

Author: YaelDillies

src/algebra/order/hom/basic.lean

@@ -56,6 +56,15 @@ export mul_le_add_hom_class (map_mul_le_add)
 
 attribute [simp] map_nonneg
 
+@[to_additive] lemma le_map_mul_map_div [group α] [comm_semigroup β] [has_le β]
+  [submultiplicative_hom_class F α β] (f : F) (a b : α) : f a ≤ f b * f (a / b) :=
+by simpa only [mul_comm, div_mul_cancel'] using map_mul_le_mul f (a / b) b
+
+@[to_additive]
+lemma le_map_div_mul_map_div [group α] [comm_semigroup β] [has_le β]
+  [submultiplicative_hom_class F α β] (f : F) (a b c: α) : f (a / c) ≤ f (a / b) * f (b / c) :=
+by simpa only [div_mul_div_cancel'] using map_mul_le_mul f (a / b) (b / c)
+
 @[to_additive] lemma le_map_add_map_div [group α] [add_comm_semigroup β] [has_le β]
   [mul_le_add_hom_class F α β] (f : F) (a b : α) : f a ≤ f b + f (a / b) :=
 by simpa only [add_comm, div_mul_cancel'] using map_mul_le_add f (a / b) b

src/analysis/complex/basic.lean

@@ -39,10 +39,11 @@ instance : has_norm ℂ := ⟨abs⟩
 @[simp] lemma norm_eq_abs (z : ℂ) : ∥z∥ = abs z := rfl
 
 instance : normed_add_comm_group ℂ :=
-normed_add_comm_group.of_core ℂ
-{ norm_eq_zero_iff := λ x, abs.eq_zero,
-  triangle := abs.add_le,
-  norm_neg := abs.map_neg }
+add_group_norm.to_normed_add_comm_group
+{ map_zero' := map_zero abs,
+  neg' := abs.map_neg,
+  eq_zero_of_map_eq_zero' := λ _, abs.eq_zero.1,
+  ..abs }
 
 instance : normed_field ℂ :=
 { norm := abs,

src/analysis/inner_product_space/basic.lean

@@ -325,32 +325,25 @@ end
 
 /-- Normed group structure constructed from an `inner_product_space.core` structure -/
 def to_normed_add_comm_group : normed_add_comm_group F :=
-normed_add_comm_group.of_core F
-{ norm_eq_zero_iff := assume x,
-  begin
-    split,
-    { intro H,
-      change sqrt (re ⟪x, x⟫) = 0 at H,
-      rw [sqrt_eq_zero inner_self_nonneg] at H,
-      apply (inner_self_eq_zero : ⟪x, x⟫ = 0 ↔ x = 0).mp,
-      rw ext_iff,
-      exact ⟨by simp [H], by simp [inner_self_im_zero]⟩ },
-    { rintro rfl,
-      change sqrt (re ⟪0, 0⟫) = 0,
-      simp only [sqrt_zero, inner_zero_right, add_monoid_hom.map_zero] }
-  end,
-  triangle := assume x y,
-  begin
+add_group_norm.to_normed_add_comm_group
+{ to_fun := λ x, sqrt (re ⟪x, x⟫),
+  map_zero' := by simp only [sqrt_zero, inner_zero_right, map_zero],
+  neg' := λ x, by simp only [inner_neg_left, neg_neg, inner_neg_right],
+  add_le' := λ x y, begin
     have h₁ : abs ⟪x, y⟫ ≤ ∥x∥ * ∥y∥ := abs_inner_le_norm _ _,
     have h₂ : re ⟪x, y⟫ ≤ abs ⟪x, y⟫ := re_le_abs _,
     have h₃ : re ⟪x, y⟫ ≤ ∥x∥ * ∥y∥ := by linarith,
     have h₄ : re ⟪y, x⟫ ≤ ∥x∥ * ∥y∥ := by rwa [←inner_conj_sym, conj_re],
     have : ∥x + y∥ * ∥x + y∥ ≤ (∥x∥ + ∥y∥) * (∥x∥ + ∥y∥),
     { simp [←inner_self_eq_norm_mul_norm, inner_add_add_self, add_mul, mul_add, mul_comm],
       linarith },
-    exact nonneg_le_nonneg_of_sq_le_sq (add_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) this
+    exact nonneg_le_nonneg_of_sq_le_sq (add_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) this,
   end,
-  norm_neg := λ x, by simp only [norm, inner_neg_left, neg_neg, inner_neg_right] }
+  eq_zero_of_map_eq_zero' := λ x hx, (inner_self_eq_zero : ⟪x, x⟫ = 0 ↔ x = 0).1 $ begin
+    change sqrt (re ⟪x, x⟫) = 0 at hx,
+    rw [sqrt_eq_zero inner_self_nonneg] at hx,
+    exact ext (by simp [hx]) (by simp [inner_self_im_zero]),
+  end }
 
 local attribute [instance] to_normed_add_comm_group
 

src/analysis/normed/group/basic.lean

@@ -81,28 +81,18 @@ def seminormed_add_comm_group.of_add_dist' [has_norm E] [add_comm_group E] [pseu
     { rw [sub_eq_add_neg, ← add_right_neg y], apply H2 }
   end }
 
-/-- A seminormed group can be built from a seminorm that satisfies algebraic properties. This is
-formalised in this structure. -/
-structure seminormed_add_comm_group.core (E : Type*) [add_comm_group E] [has_norm E] : Prop :=
-(norm_zero : ∥(0 : E)∥ = 0)
-(triangle : ∀ x y : E, ∥x + y∥ ≤ ∥x∥ + ∥y∥)
-(norm_neg : ∀ x : E, ∥-x∥ = ∥x∥)
-
-/-- Constructing a seminormed group from core properties of a seminorm, i.e., registering the
-pseudodistance and the pseudometric space structure from the seminorm properties. Note that in most
-cases this instance creates bad definitional equalities (e.g., it does not take into account
-a possibly existing `uniform_space` instance on `E`). -/
-def seminormed_add_comm_group.of_core (E : Type*) [add_comm_group E] [has_norm E]
-  (C : seminormed_add_comm_group.core E) : seminormed_add_comm_group E :=
-{ dist := λ x y, ∥x - y∥,
-  dist_eq := assume x y, by refl,
-  dist_self := assume x, by simp [C.norm_zero],
-  dist_triangle := assume x y z,
-    calc ∥x - z∥ = ∥x - y + (y - z)∥ : by rw sub_add_sub_cancel
-            ... ≤ ∥x - y∥ + ∥y - z∥  : C.triangle _ _,
-  dist_comm := assume x y,
-    calc ∥x - y∥ = ∥ -(y - x)∥ : by simp
-             ... = ∥y - x∥ : by { rw [C.norm_neg] } }
+/-- Construct a seminormed group from a seminorm, i.e., registering the pseudodistance and the
+pseudometric space structure from the seminorm properties. Note that in most cases this instance
+creates bad definitional equalities (e.g., it does not take into account a possibly existing
+`uniform_space` instance on `E`). -/
+def add_group_seminorm.to_seminormed_add_comm_group [add_comm_group E] (f : add_group_seminorm E) :
+  seminormed_add_comm_group E :=
+{ dist := λ x y, f (x - y),
+  norm := f,
+  dist_eq := λ x y, rfl,
+  dist_self := λ x, by simp only [sub_self, map_zero],
+  dist_triangle := le_map_sub_add_map_sub f,
+  dist_comm := map_sub_rev f }
 
 instance : normed_add_comm_group punit :=
 { norm := function.const _ 0,
@@ -1147,32 +1137,14 @@ def normed_add_comm_group.of_add_dist [has_norm E] [add_comm_group E] [metric_sp
     { have := H2 (x-y) 0 y, rwa [sub_add_cancel, zero_add] at this }
   end }
 
-/-- A normed group can be built from a norm that satisfies algebraic properties. This is
-formalised in this structure. -/
-structure normed_add_comm_group.core (E : Type*) [add_comm_group E] [has_norm E] : Prop :=
-(norm_eq_zero_iff : ∀ x : E, ∥x∥ = 0 ↔ x = 0)
-(triangle : ∀ x y : E, ∥x + y∥ ≤ ∥x∥ + ∥y∥)
-(norm_neg : ∀ x : E, ∥-x∥ = ∥x∥)
-
-/-- The `seminormed_add_comm_group.core` induced by a `normed_add_comm_group.core`. -/
-lemma normed_add_comm_group.core.to_seminormed_add_comm_group.core {E : Type*} [add_comm_group E]
-  [has_norm E]
-  (C : normed_add_comm_group.core E) : seminormed_add_comm_group.core E :=
-{ norm_zero := (C.norm_eq_zero_iff 0).2 rfl,
-  triangle := C.triangle,
-  norm_neg := C.norm_neg }
-
-/-- Constructing a normed group from core properties of a norm, i.e., registering the distance and
-the metric space structure from the norm properties. -/
-def normed_add_comm_group.of_core (E : Type*) [add_comm_group E] [has_norm E]
-  (C : normed_add_comm_group.core E) : normed_add_comm_group E :=
-{ eq_of_dist_eq_zero := λ x y h,
-  begin
-    rw [dist_eq_norm] at h,
-    exact sub_eq_zero.mp ((C.norm_eq_zero_iff _).1 h)
-  end
-  ..seminormed_add_comm_group.of_core E
-    (normed_add_comm_group.core.to_seminormed_add_comm_group.core C) }
+/-- Construct a normed group from a norm, i.e., registering the distance and the metric space
+structure from the norm properties. Note that in most cases this instance creates bad definitional
+equalities (e.g., it does not take into account a possibly existing `uniform_space` instance on
+`E`). -/
+def add_group_norm.to_normed_add_comm_group [add_comm_group E] (f : add_group_norm E) :
+  normed_add_comm_group E :=
+{ eq_of_dist_eq_zero := λ x y h, sub_eq_zero.1 $ eq_zero_of_map_eq_zero f h,
+  ..f.to_add_group_seminorm.to_seminormed_add_comm_group }
 
 variables [normed_add_comm_group E] [normed_add_comm_group F] {x y : E}
 

src/analysis/normed/group/hom.lean

@@ -438,14 +438,23 @@ coe_injective.add_comm_group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _
 /-- Normed group homomorphisms themselves form a seminormed group with respect to
     the operator norm. -/
 instance to_seminormed_add_comm_group : seminormed_add_comm_group (normed_add_group_hom V₁ V₂) :=
-seminormed_add_comm_group.of_core _ ⟨op_norm_zero, op_norm_add_le, op_norm_neg⟩
+add_group_seminorm.to_seminormed_add_comm_group
+{ to_fun := op_norm,
+  map_zero' := op_norm_zero,
+  neg' := op_norm_neg,
+  add_le' := op_norm_add_le }
 
 /-- Normed group homomorphisms themselves form a normed group with respect to
     the operator norm. -/
 instance to_normed_add_comm_group {V₁ V₂ : Type*} [normed_add_comm_group V₁]
   [normed_add_comm_group V₂] :
   normed_add_comm_group (normed_add_group_hom V₁ V₂) :=
-normed_add_comm_group.of_core _ ⟨λ f, op_norm_zero_iff, op_norm_add_le, op_norm_neg⟩
+add_group_norm.to_normed_add_comm_group
+{ to_fun := op_norm,
+  map_zero' := op_norm_zero,
+  neg' := op_norm_neg,
+  add_le' := op_norm_add_le,
+  eq_zero_of_map_eq_zero' := λ f, op_norm_zero_iff.1 }
 
 /-- Coercion of a `normed_add_group_hom` is an `add_monoid_hom`. Similar to `add_monoid_hom.coe_fn`.
 -/

src/analysis/normed_space/continuous_affine_map.lean

@@ -159,11 +159,16 @@ calc ∥f∥ = (max ∥f 0∥ ∥f.cont_linear∥) : by rw norm_def
     ... = ∥f.cont_linear∥ : max_eq_right (norm_nonneg _)
 
 noncomputable instance : normed_add_comm_group (V →A[𝕜] W) :=
-normed_add_comm_group.of_core _
-{ norm_eq_zero_iff := λ f,
-    begin
-      rw norm_def,
-      refine ⟨λ h₀, _, by { rintros rfl, simp, }⟩,
+add_group_norm.to_normed_add_comm_group
+{ to_fun := λ f, max ∥f 0∥ ∥f.cont_linear∥,
+  map_zero' := by simp,
+  neg' := λ f, by simp,
+  add_le' := λ f g, begin
+      simp only [pi.add_apply, add_cont_linear, coe_add, max_le_iff],
+      exact ⟨(norm_add_le _ _).trans (add_le_add (le_max_left _ _) (le_max_left _ _)),
+             (norm_add_le _ _).trans (add_le_add (le_max_right _ _) (le_max_right _ _))⟩,
+    end,
+  eq_zero_of_map_eq_zero' := λ f h₀, begin
       rcases max_eq_iff.mp h₀ with ⟨h₁, h₂⟩ | ⟨h₁, h₂⟩;
       rw h₁ at h₂,
       { rw [norm_le_zero_iff, cont_linear_eq_zero_iff_exists_const] at h₂,
@@ -176,14 +181,7 @@ normed_add_comm_group.of_core _
         simp only [function.const_apply, coe_const, norm_le_zero_iff] at h₂,
         rw h₂,
         refl, },
-    end,
-  triangle := λ f g,
-    begin
-      simp only [norm_def, pi.add_apply, add_cont_linear, coe_add, max_le_iff],
-      exact ⟨(norm_add_le _ _).trans (add_le_add (le_max_left _ _) (le_max_left _ _)),
-             (norm_add_le _ _).trans (add_le_add (le_max_right _ _) (le_max_right _ _))⟩,
-    end,
-  norm_neg := λ f, by simp [norm_def], }
+    end }
 
 instance : normed_space 𝕜 (V →A[𝕜] W) :=
 { norm_smul_le := λ t f, by simp only [norm_def, smul_cont_linear, coe_smul, pi.smul_apply,

src/analysis/normed_space/lp_space.lean

@@ -413,7 +413,7 @@ begin
     simpa [real.zero_rpow hp.ne'] using real.zero_rpow hp' }
 end
 
-lemma norm_eq_zero_iff ⦃f : lp E p⦄ : ∥f∥ = 0 ↔ f = 0 :=
+lemma norm_eq_zero_iff {f : lp E p} : ∥f∥ = 0 ↔ f = 0 :=
 begin
   classical,
   refine ⟨λ h, _, by { rintros rfl, exact norm_zero }⟩,
@@ -458,9 +458,11 @@ begin
 end
 
 instance [hp : fact (1 ≤ p)] : normed_add_comm_group (lp E p) :=
-normed_add_comm_group.of_core _
-{ norm_eq_zero_iff := norm_eq_zero_iff,
-  triangle := λ f g, begin
+add_group_norm.to_normed_add_comm_group
+{ to_fun := norm,
+  map_zero' := norm_zero,
+  neg' := norm_neg,
+  add_le' := λ f g, begin
     unfreezingI { rcases p.dichotomy with rfl | hp' },
     { casesI is_empty_or_nonempty α,
       { simp [lp.eq_zero' f] },
@@ -483,7 +485,7 @@ normed_add_comm_group.of_core _
       intros i,
       exact real.rpow_le_rpow (norm_nonneg _) (norm_add_le _ _) hp''.le },
   end,
-  norm_neg := norm_neg }
+  eq_zero_of_map_eq_zero' := λ f, norm_eq_zero_iff.1 }
 
 -- TODO: define an `ennreal` version of `is_conjugate_exponent`, and then express this inequality
 -- in a better version which also covers the case `p = 1, q = ∞`.

src/analysis/normed_space/multilinear.lean

@@ -344,17 +344,12 @@ cInf_le bounds_bdd_below
   ⟨add_nonneg (op_norm_nonneg _) (op_norm_nonneg _), λ x, by { rw add_mul,
     exact norm_add_le_of_le (le_op_norm _ _) (le_op_norm _ _) }⟩
 
+lemma op_norm_zero : ∥(0 : continuous_multilinear_map 𝕜 E G)∥ = 0 :=
+(op_norm_nonneg _).antisymm' $ op_norm_le_bound 0 le_rfl $ λ m, by simp
+
 /-- A continuous linear map is zero iff its norm vanishes. -/
 theorem op_norm_zero_iff : ∥f∥ = 0 ↔ f = 0 :=
-begin
-  split,
-  { assume h,
-    ext m,
-    simpa [h] using f.le_op_norm m },
-  { rintro rfl,
-    apply le_antisymm (op_norm_le_bound 0 le_rfl (λm, _)) (op_norm_nonneg _),
-    simp }
-end
+⟨λ h, by { ext m, simpa [h] using f.le_op_norm m }, by { rintro rfl, exact op_norm_zero }⟩
 
 section
 variables {𝕜' : Type*} [normed_field 𝕜'] [normed_space 𝕜' G] [smul_comm_class 𝕜 𝕜' G]
@@ -373,7 +368,12 @@ lemma op_norm_neg : ∥-f∥ = ∥f∥ := by { rw norm_def, apply congr_arg, ext
 /-- Continuous multilinear maps themselves form a normed space with respect to
     the operator norm. -/
 instance normed_add_comm_group : normed_add_comm_group (continuous_multilinear_map 𝕜 E G) :=
-normed_add_comm_group.of_core _ ⟨op_norm_zero_iff, op_norm_add_le, op_norm_neg⟩
+add_group_norm.to_normed_add_comm_group
+{ to_fun := norm,
+  map_zero' := op_norm_zero,
+  neg' := op_norm_neg,
+  add_le' := op_norm_add_le,
+  eq_zero_of_map_eq_zero' := λ f, f.op_norm_zero_iff.1 }
 
 /-- An alias of `continuous_multilinear_map.normed_add_comm_group` with non-dependent types to help
 typeclass search. -/

src/analysis/normed_space/operator_norm.lean

@@ -383,7 +383,11 @@ lemma op_norm_smul_le {𝕜' : Type*} [normed_field 𝕜'] [normed_space 𝕜' F
 /-- Continuous linear maps themselves form a seminormed space with respect to
     the operator norm. -/
 instance to_seminormed_add_comm_group : seminormed_add_comm_group (E →SL[σ₁₂] F) :=
-seminormed_add_comm_group.of_core _ ⟨op_norm_zero, λ x y, op_norm_add_le x y, op_norm_neg⟩
+add_group_seminorm.to_seminormed_add_comm_group
+{ to_fun := norm,
+  map_zero' := op_norm_zero,
+  add_le' := op_norm_add_le,
+  neg' := op_norm_neg }
 
 lemma nnnorm_def (f : E →SL[σ₁₂] F) : ∥f∥₊ = Inf {c | ∀ x, ∥f x∥₊ ≤ c * ∥x∥₊} :=
 begin
@@ -1222,9 +1226,7 @@ iff.intro
   (λ hn, continuous_linear_map.ext (λ x, norm_le_zero_iff.1
     (calc _ ≤ ∥f∥ * ∥x∥ : le_op_norm _ _
      ...     = _ : by rw [hn, zero_mul])))
-  (λ hf, le_antisymm (cInf_le bounds_bdd_below
-    ⟨le_rfl, λ _, le_of_eq (by { rw [zero_mul, hf], exact norm_zero })⟩)
-    (op_norm_nonneg _))
+  (by { rintro rfl, exact op_norm_zero })
 
 /-- If a normed space is non-trivial, then the norm of the identity equals `1`. -/
 @[simp] lemma norm_id [nontrivial E] : ∥id 𝕜 E∥ = 1 :=
@@ -1239,7 +1241,12 @@ instance norm_one_class [nontrivial E] : norm_one_class (E →L[𝕜] E) := ⟨n
 /-- Continuous linear maps themselves form a normed space with respect to
     the operator norm. -/
 instance to_normed_add_comm_group [ring_hom_isometric σ₁₂] : normed_add_comm_group (E →SL[σ₁₂] F) :=
-normed_add_comm_group.of_core _ ⟨λ f, op_norm_zero_iff f, op_norm_add_le, op_norm_neg⟩
+add_group_norm.to_normed_add_comm_group
+{ to_fun := norm,
+  map_zero' := op_norm_zero,
+  neg' := op_norm_neg,
+  add_le' := op_norm_add_le,
+  eq_zero_of_map_eq_zero' := λ f, (op_norm_zero_iff f).1 }
 
 /-- Continuous linear maps form a normed ring with respect to the operator norm. -/
 instance to_normed_ring : normed_ring (E →L[𝕜] E) :=

src/measure_theory/function/lp_space.lean

@@ -14,7 +14,7 @@ import topology.continuous_function.compact
 # ℒp space and Lp space
 
 This file describes properties of almost everywhere strongly measurable functions with finite
-seminorm, denoted by `snorm f p μ` and defined for `p:ℝ≥0∞` as `0` if `p=0`,
+seminorm, denoted by `snorm f p μ` and defined for `p:ℝ≥0∞` asmm_group (Lp E p μ) := `0` if `p=0`,
 `(∫ ∥f a∥^p ∂μ) ^ (1/p)` for `0 < p < ∞` and `ess_sup ∥f∥ μ` for `p=∞`.
 
 The Prop-valued `mem_ℒp f p μ` states that a function `f : α → E` has finite seminorm.
@@ -1727,10 +1727,11 @@ instance [hp : fact (1 ≤ p)] : normed_add_comm_group (Lp E p μ) :=
   edist_dist := λ f g, by
     rw [edist_def, dist_def, ←snorm_congr_ae (coe_fn_sub _ _),
       ennreal.of_real_to_real (snorm_ne_top (f - g))],
-  .. normed_add_comm_group.of_core (Lp E p μ)
-    { norm_eq_zero_iff := λ f, norm_eq_zero_iff (ennreal.zero_lt_one.trans_le hp.1),
-      triangle := begin
-        assume f g,
+  ..add_group_norm.to_normed_add_comm_group
+    { to_fun := (norm : Lp E p μ → ℝ),
+      map_zero' := norm_zero,
+      neg' := by simp,
+      add_le' := λ f g, begin
         simp only [norm_def],
         rw ← ennreal.to_real_add (snorm_ne_top f) (snorm_ne_top g),
         suffices h_snorm : snorm ⇑(f + g) p μ ≤ snorm ⇑f p μ + snorm ⇑g p μ,
@@ -1739,7 +1740,7 @@ instance [hp : fact (1 ≤ p)] : normed_add_comm_group (Lp E p μ) :=
         rw [snorm_congr_ae (coe_fn_add _ _)],
         exact snorm_add_le (Lp.ae_strongly_measurable f) (Lp.ae_strongly_measurable g) hp.1,
       end,
-      norm_neg := by simp } }
+      eq_zero_of_map_eq_zero' := λ f, (norm_eq_zero_iff $ ennreal.zero_lt_one.trans_le hp.1).1 } }
 
 -- check no diamond is created
 example [fact (1 ≤ p)] :