feat(analysis/seminorm): The norm as a seminorm, balanced and absorbe…

…nt lemmas (#11487)

This
* defines `norm_seminorm`, the norm as a seminorm. This is useful to translate seminorm lemmas to norm lemmas
* proves many lemmas about `balanced`, `absorbs`, `absorbent`
* generalizes many lemmas about the aforementioned predicates. In particular, `one_le_gauge_of_not_mem` now takes `(star_convex ℝ 0 s) (absorbs ℝ s {x})` instead of `(convex ℝ s) ((0 : E) ∈ s) (is_open s)`. The new `star_convex` lemmas justify that it's a generalization.
* proves `star_convex_zero_iff`
* proves `ne_zero_of_norm_ne_zero` and friends
* makes `x` implicit in `convex.star_convex`
* renames `balanced.univ` to `balanced_univ`

src/algebra/smul_with_zero.lean

@@ -159,6 +159,22 @@ def mul_action_with_zero.comp_hom (f : R' →*₀ R) : mul_action_with_zero R' M
 
 end monoid_with_zero
 
+section group_with_zero
+variables {α β : Type*} [group_with_zero α] [group_with_zero β] [mul_action_with_zero α β]
+
+lemma smul_inv₀ [smul_comm_class α β β] [is_scalar_tower α β β] (c : α) (x : β) :
+  (c • x)⁻¹ = c⁻¹ • x⁻¹ :=
+begin
+  obtain rfl | hc := eq_or_ne c 0,
+  { simp only [inv_zero, zero_smul] },
+  obtain rfl | hx := eq_or_ne x 0,
+  { simp only [inv_zero, smul_zero'] },
+  { refine (eq_inv_of_mul_left_eq_one _).symm,
+    rw [smul_mul_smul, inv_mul_cancel hc, inv_mul_cancel hx, one_smul] }
+end
+
+end group_with_zero
+
 /-- Scalar multiplication as a monoid homomorphism with zero. -/
 @[simps]
 def smul_monoid_with_zero_hom {α β : Type*} [monoid_with_zero α] [mul_zero_one_class β]

src/analysis/complex/circle.lean

@@ -57,7 +57,7 @@ by rw [mem_circle_iff_abs, complex.abs, real.sqrt_eq_one]
 
 @[simp] lemma norm_sq_eq_of_mem_circle (z : circle) : norm_sq z = 1 := by simp [norm_sq_eq_abs]
 
-lemma nonzero_of_mem_circle (z : circle) : (z:ℂ) ≠ 0 := nonzero_of_mem_unit_sphere z
+lemma ne_zero_of_mem_circle (z : circle) : (z:ℂ) ≠ 0 := ne_zero_of_mem_unit_sphere z
 
 instance : comm_group circle :=
 { inv := λ z, ⟨conj (z : ℂ), by simp⟩,
@@ -81,7 +81,7 @@ show ↑(z * w⁻¹) = (z:ℂ) * w⁻¹, by simp
 /-- The elements of the circle embed into the units. -/
 @[simps]
 def circle.to_units : circle →* units ℂ :=
-{ to_fun := λ x, units.mk0 x $ nonzero_of_mem_circle _,
+{ to_fun := λ x, units.mk0 x $ ne_zero_of_mem_circle _,
   map_one' := units.ext rfl,
   map_mul' := λ x y, units.ext rfl }
 

src/analysis/convex/star.lean

@@ -65,7 +65,8 @@ variables {𝕜 x s} {t : set E}
 lemma convex_iff_forall_star_convex : convex 𝕜 s ↔ ∀ x ∈ s, star_convex 𝕜 x s :=
 forall_congr $ λ x, forall_swap
 
-alias convex_iff_forall_star_convex ↔ convex.star_convex _
+lemma convex.star_convex (h : convex 𝕜 s) (hx : x ∈ s) : star_convex 𝕜 x s :=
+convex_iff_forall_star_convex.1 h _ hx
 
 lemma star_convex_iff_segment_subset : star_convex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → [x -[𝕜] y] ⊆ s :=
 begin
@@ -157,7 +158,7 @@ begin
 end
 
 lemma convex.star_convex_iff (hs : convex 𝕜 s) (h : s.nonempty) : star_convex 𝕜 x s ↔ x ∈ s :=
-⟨λ hxs, hxs.mem h, hs.star_convex _⟩
+⟨λ hxs, hxs.mem h, hs.star_convex⟩
 
 lemma star_convex_iff_forall_pos (hx : x ∈ s) :
   star_convex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s :=
@@ -302,6 +303,21 @@ end ordered_comm_semiring
 section ordered_ring
 variables [ordered_ring 𝕜]
 
+section add_comm_monoid
+variables [add_comm_monoid E] [smul_with_zero 𝕜 E]{s : set E}
+
+lemma star_convex_zero_iff :
+  star_convex 𝕜 0 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s :=
+begin
+  refine forall_congr (λ x, forall_congr $ λ hx, ⟨λ h a ha₀ ha₁, _, λ h a b ha hb hab, _⟩),
+  { simpa only [sub_add_cancel, eq_self_iff_true, forall_true_left, zero_add, smul_zero'] using
+      h (sub_nonneg_of_le ha₁) ha₀ },
+  { rw [smul_zero', zero_add],
+    exact h hb (by { rw ←hab, exact le_add_of_nonneg_left ha }) }
+end
+
+end add_comm_monoid
+
 section add_comm_group
 variables [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {x y : E} {s : set E}
 
@@ -441,11 +457,11 @@ open submodule
 lemma submodule.star_convex [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E]
   (K : submodule 𝕜 E) :
   star_convex 𝕜 (0 : E) K :=
- K.convex.star_convex _ K.zero_mem
+K.convex.star_convex K.zero_mem
 
 lemma subspace.star_convex [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E]
   (K : subspace 𝕜 E) :
   star_convex 𝕜 (0 : E) K :=
- K.convex.star_convex _ K.zero_mem
+K.convex.star_convex K.zero_mem
 
 end submodule

src/analysis/fourier.lean

@@ -85,7 +85,7 @@ section monomials
 continuous maps from `circle` to `ℂ`. -/
 @[simps] def fourier (n : ℤ) : C(circle, ℂ) :=
 { to_fun := λ z, z ^ n,
-  continuous_to_fun := continuous_subtype_coe.zpow n $ λ z, or.inl (nonzero_of_mem_circle z) }
+  continuous_to_fun := continuous_subtype_coe.zpow n $ λ z, or.inl (ne_zero_of_mem_circle z) }
 
 @[simp] lemma fourier_zero {z : circle} : fourier 0 z = 1 := rfl
 
@@ -94,7 +94,7 @@ by simp [← coe_inv_circle_eq_conj z]
 
 @[simp] lemma fourier_add {m n : ℤ} {z : circle} :
   fourier (m + n) z = (fourier m z) * (fourier n z) :=
-by simp [zpow_add₀ (nonzero_of_mem_circle z)]
+by simp [zpow_add₀ (ne_zero_of_mem_circle z)]
 
 /-- The subalgebra of `C(circle, ℂ)` generated by `z ^ n` for `n ∈ ℤ`; equivalently, polynomials in
 `z` and `conj z`. -/

src/analysis/inner_product_space/rayleigh.lean

@@ -70,7 +70,7 @@ begin
     { rw T.rayleigh_smul x this,
       exact hxT } },
   { rintros ⟨x, hx, hxT⟩,
-    exact ⟨x, nonzero_of_mem_sphere hr ⟨x, hx⟩, hxT⟩ },
+    exact ⟨x, ne_zero_of_mem_sphere hr.ne' ⟨x, hx⟩, hxT⟩ },
 end
 
 lemma supr_rayleigh_eq_supr_rayleigh_sphere {r : ℝ} (hr : 0 < r) :

src/analysis/normed/group/basic.lean

@@ -188,6 +188,8 @@ by { rw[←dist_zero_right], exact dist_nonneg }
 
 @[simp] lemma norm_zero : ∥(0 : E)∥ = 0 :=  by rw [← dist_zero_right, dist_self]
 
+lemma ne_zero_of_norm_ne_zero {g : E} : ∥g∥ ≠ 0 → g ≠ 0 := mt $ by { rintro rfl, exact norm_zero }
+
 @[nontriviality] lemma norm_of_subsingleton [subsingleton E] (x : E) : ∥x∥ = 0 :=
 by rw [subsingleton.elim x 0, norm_zero]
 
@@ -332,21 +334,11 @@ begin
   abel
 end
 
-lemma ne_zero_of_norm_pos {g : E} : 0 < ∥ g ∥ → g ≠ 0 :=
-begin
-  intros hpos hzero,
-  rw [hzero, norm_zero] at hpos,
-  exact lt_irrefl 0 hpos,
-end
+lemma ne_zero_of_mem_sphere {r : ℝ} (hr : r ≠ 0) (x : sphere (0 : E) r) : (x : E) ≠ 0 :=
+ne_zero_of_norm_ne_zero $ by rwa norm_eq_of_mem_sphere x
 
-lemma nonzero_of_mem_sphere {r : ℝ} (hr : 0 < r) (x : sphere (0:E) r) : (x:E) ≠ 0 :=
-begin
-  refine ne_zero_of_norm_pos _,
-  rwa norm_eq_of_mem_sphere x,
-end
-
-lemma nonzero_of_mem_unit_sphere (x : sphere (0:E) 1) : (x:E) ≠ 0 :=
-by { apply nonzero_of_mem_sphere, norm_num }
+lemma ne_zero_of_mem_unit_sphere (x : sphere (0:E) 1) : (x:E) ≠ 0 :=
+ne_zero_of_mem_sphere one_ne_zero _
 
 /-- We equip the sphere, in a seminormed group, with a formal operation of negation, namely the
 antipodal map. -/
@@ -559,6 +551,9 @@ lemma nndist_eq_nnnorm (a b : E) : nndist a b = ∥a - b∥₊ := nnreal.eq $ di
 @[simp] lemma nnnorm_zero : ∥(0 : E)∥₊ = 0 :=
 nnreal.eq norm_zero
 
+lemma ne_zero_of_nnnorm_ne_zero {g : E} : ∥g∥₊ ≠ 0 → g ≠ 0 :=
+mt $ by { rintro rfl, exact nnnorm_zero }
+
 lemma nnnorm_add_le (g h : E) : ∥g + h∥₊ ≤ ∥g∥₊ + ∥h∥₊ :=
 nnreal.coe_le_coe.1 $ norm_add_le g h
 
@@ -946,6 +941,8 @@ variables [normed_group E] [normed_group F]
 
 @[simp] lemma norm_eq_zero {g : E} : ∥g∥ = 0 ↔ g = 0 := norm_eq_zero_iff'
 
+lemma norm_ne_zero_iff {g : E} : ∥g∥ ≠ 0 ↔ g ≠ 0 := not_congr norm_eq_zero
+
 @[simp] lemma norm_pos_iff {g : E} : 0 < ∥ g ∥ ↔ g ≠ 0 := norm_pos_iff'
 
 @[simp] lemma norm_le_zero_iff {g : E} : ∥g∥ ≤ 0 ↔ g = 0 := norm_le_zero_iff'
@@ -962,6 +959,8 @@ norm_sub_eq_zero_iff.1 h
 @[simp] lemma nnnorm_eq_zero {a : E} : ∥a∥₊ = 0 ↔ a = 0 :=
 by rw [← nnreal.coe_eq_zero, coe_nnnorm, norm_eq_zero]
 
+lemma nnnorm_ne_zero_iff {g : E} : ∥g∥₊ ≠ 0 ↔ g ≠ 0 := not_congr nnnorm_eq_zero
+
 /-- An injective group homomorphism from an `add_comm_group` to a `normed_group` induces a
 `normed_group` structure on the domain.
 

src/analysis/normed_space/basic.lean

@@ -662,11 +662,11 @@ def homeomorph_unit_ball {E : Type*} [semi_normed_group E] [normed_space ℝ E]
 
 variables (α)
 
-lemma ne_neg_of_mem_sphere [char_zero α] {r : ℝ} (hr : 0 < r) (x : sphere (0:E) r) : x ≠ - x :=
-λ h, nonzero_of_mem_sphere hr x (eq_zero_of_eq_neg α (by { conv_lhs {rw h}, simp }))
+lemma ne_neg_of_mem_sphere [char_zero α] {r : ℝ} (hr : r ≠ 0) (x : sphere (0:E) r) : x ≠ - x :=
+λ h, ne_zero_of_mem_sphere hr x (eq_zero_of_eq_neg α (by { conv_lhs {rw h}, simp }))
 
 lemma ne_neg_of_mem_unit_sphere [char_zero α] (x : sphere (0:E) 1) : x ≠ - x :=
-ne_neg_of_mem_sphere α  (by norm_num) x
+ne_neg_of_mem_sphere α one_ne_zero x
 
 variables {α}
 
@@ -884,7 +884,7 @@ lemma normed_algebra.norm_one_class : norm_one_class 𝕜' :=
 
 lemma normed_algebra.zero_ne_one : (0:𝕜') ≠ 1 :=
 begin
-  refine (ne_zero_of_norm_pos _).symm,
+  refine (ne_zero_of_norm_ne_zero _).symm,
   rw normed_algebra.norm_one 𝕜 𝕜', norm_num,
 end
 

src/analysis/normed_space/spectrum.lean

@@ -67,7 +67,7 @@ lemma mem_resolvent_of_norm_lt {a : A} {k : 𝕜} (h : ∥a∥ < ∥k∥) :
   k ∈ ρ a :=
 begin
   rw [resolvent_set, set.mem_set_of_eq, algebra.algebra_map_eq_smul_one],
-  have hk : k ≠ 0 := ne_zero_of_norm_pos (by linarith [norm_nonneg a]),
+  have hk : k ≠ 0 := ne_zero_of_norm_ne_zero (by linarith [norm_nonneg a]),
   let ku := units.map (↑ₐ).to_monoid_hom (units.mk0 k hk),
   have hku : ∥-a∥ < ∥(↑ku⁻¹:A)∥⁻¹ := by simpa [ku, algebra_map_isometry] using h,
   simpa [ku, sub_eq_add_neg, algebra.algebra_map_eq_smul_one] using (ku.add (-a) hku).is_unit,