feat(analysis/normed_space/enorm): define extended norm (leanprover-c…

…ommunity#2897)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/analysis/normed_space/basic.lean

@@ -208,7 +208,7 @@ def nnnorm (a : α) : nnreal := ⟨norm a, norm_nonneg a⟩
 
 lemma nndist_eq_nnnorm (a b : α) : nndist a b = nnnorm (a - b) := nnreal.eq $ dist_eq_norm _ _
 
-lemma nnnorm_eq_zero {a : α} : nnnorm a = 0 ↔ a = 0 :=
+@[simp] lemma nnnorm_eq_zero {a : α} : nnnorm a = 0 ↔ a = 0 :=
 by simp only [nnreal.eq_iff.symm, nnreal.coe_zero, coe_nnnorm, norm_eq_zero]
 
 @[simp] lemma nnnorm_zero : nnnorm (0 : α) = 0 :=
@@ -494,6 +494,8 @@ eq_of_mul_eq_mul_left (ne_of_gt (norm_pos_iff.2 (by simp))) this
 @[simp] lemma norm_mul [normed_field α] (a b : α) : ∥a * b∥ = ∥a∥ * ∥b∥ :=
 normed_field.norm_mul' a b
 
+@[simp] lemma nnnorm_one [normed_field α] : nnnorm (1:α) = 1 := nnreal.eq $ by simp
+
 instance normed_field.is_monoid_hom_norm [normed_field α] : is_monoid_hom (norm : α → ℝ) :=
 { map_one := norm_one, map_mul := norm_mul }
 
@@ -516,6 +518,9 @@ end
 @[simp] lemma norm_inv {α : Type*} [normed_field α] (a : α) : ∥a⁻¹∥ = ∥a∥⁻¹ :=
 by simp only [inv_eq_one_div, norm_div, norm_one]
 
+@[simp] lemma nnnorm_inv {α : Type*} [normed_field α] (a : α) : nnnorm (a⁻¹) = (nnnorm a)⁻¹ :=
+nnreal.eq $ by simp
+
 @[simp] lemma norm_fpow {α : Type*} [normed_field α] (a : α) : ∀n : ℤ,
   ∥a^n∥ = ∥a∥^n
 | (n : ℕ) := norm_pow a n
@@ -637,9 +642,19 @@ lemma continuous_at.div [topological_space α] [normed_field β] {f : α → β}
   continuous_at (λ x, f x / g x) x :=
 hf.div hg hnz
 
-lemma real.norm_eq_abs (r : ℝ) : norm r = abs r := rfl
+namespace real
+
+lemma norm_eq_abs (r : ℝ) : ∥r∥ = abs r := rfl
+
+@[simp] lemma norm_coe_nat (n : ℕ) : ∥(n : ℝ)∥ = n := abs_of_nonneg n.cast_nonneg
+
+@[simp] lemma nnnorm_coe_nat (n : ℕ) : nnnorm (n : ℝ) = n := nnreal.eq $ by simp
+
+@[simp] lemma norm_two : ∥(2:ℝ)∥ = 2 := abs_of_pos (@two_pos ℝ _)
+
+@[simp] lemma nnnorm_two : nnnorm (2:ℝ) = 2 := nnreal.eq $ by simp
 
-@[simp] lemma real.norm_two : ∥(2:ℝ)∥ = 2 := abs_of_pos (@two_pos ℝ _)
+end real
 
 @[simp] lemma norm_norm [normed_group α] (x : α) : ∥∥x∥∥ = ∥x∥ :=
 by rw [real.norm_eq_abs, abs_of_nonneg (norm_nonneg _)]

src/analysis/normed_space/enorm.lean

@@ -0,0 +1,186 @@
+/-
+Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Yury G. Kudryashov
+-/
+import analysis.normed_space.basic
+
+/-!
+# Extended norm
+
+In this file we define a structure `enorm 𝕜 V` representing an extended norm (i.e., a norm that can
+take the value `∞`) on a vector space `V` over a normed field `𝕜`. We do not use `class` for
+an `enorm` because the same space can have more than one extended norm. For example, the space of
+measurable functions `f : α → ℝ` has a family of `L_p` extended norms.
+
+We prove some basic inequalities, then define
+
+* `emetric_space` structure on `V` corresponding to `e : enorm 𝕜 V`;
+* the subspace of vectors with finite norm, called `e.finite_subspace`;
+* a `normed_space` structure on this space.
+
+The last definition is an instance because the type involves `e`.
+
+## Implementation notes
+
+We do not define extended normed groups. They can be added to the chain once someone will need them.
+
+## Tags
+
+normed space, extended norm
+-/
+
+local attribute [instance, priority 1001] classical.prop_decidable
+
+/-- Extended norm on a vector space. As in the case of normed spaces, we require only
+`∥c • x∥ ≤ ∥c∥ * ∥x∥` in the definition, then prove an equality in `map_smul`. -/
+structure enorm (𝕜 : Type*) (V : Type*) [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] :=
+(to_fun : V → ennreal)
+(eq_zero' : ∀ x, to_fun x = 0 → x = 0)
+(map_add_le' : ∀ x y : V, to_fun (x + y) ≤ to_fun x + to_fun y)
+(map_smul_le' : ∀ (c : 𝕜) (x : V), to_fun (c • x) ≤ nnnorm c * to_fun x)
+
+namespace enorm
+
+variables {𝕜 : Type*} {V : Type*} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V]
+  (e : enorm 𝕜 V)
+
+instance : has_coe_to_fun (enorm 𝕜 V) := ⟨_, enorm.to_fun⟩
+
+lemma coe_fn_injective ⦃e₁ e₂ : enorm 𝕜 V⦄ (h : ⇑e₁ = e₂) : e₁ = e₂ :=
+by cases e₁; cases e₂; congr; exact h
+
+@[ext] lemma ext {e₁ e₂ : enorm 𝕜 V} (h : ∀ x, e₁ x = e₂ x) : e₁ = e₂ :=
+coe_fn_injective $ funext h
+
+lemma ext_iff {e₁ e₂ : enorm 𝕜 V} : e₁ = e₂ ↔ ∀ x, e₁ x = e₂ x :=
+⟨λ h x, h ▸ rfl, ext⟩
+
+@[simp] lemma map_smul (c : 𝕜) (x : V) : e (c • x) = nnnorm c * e x :=
+le_antisymm (e.map_smul_le' c x) $
+begin
+  by_cases hc : c = 0, { simp [hc] },
+  calc (nnnorm c : ennreal) * e x = nnnorm c * e (c⁻¹ • c • x) : by rw [inv_smul_smul' hc]
+  ... ≤ nnnorm c * (nnnorm (c⁻¹) * e (c • x)) : _
+  ... = e (c • x) : _,
+  { exact ennreal.mul_le_mul (le_refl _) (e.map_smul_le' _ _) },
+  { rw [← mul_assoc, normed_field.nnnorm_inv, ennreal.coe_inv,
+     ennreal.mul_inv_cancel _ ennreal.coe_ne_top, one_mul]; simp [hc] }
+end
+
+@[simp] lemma map_zero : e 0 = 0 :=
+by { rw [← zero_smul 𝕜 (0:V), e.map_smul], norm_num }
+
+@[simp] lemma eq_zero_iff {x : V} : e x = 0 ↔ x = 0 :=
+⟨e.eq_zero' x, λ h, h.symm ▸ e.map_zero⟩
+
+@[simp] lemma map_neg (x : V) : e (-x) = e x :=
+calc e (-x) = nnnorm (-1:𝕜) * e x : by rw [← map_smul, neg_one_smul]
+        ... = e x                 : by simp
+
+lemma map_sub_rev (x y : V) : e (x - y) = e (y - x) :=
+by rw [← neg_sub, e.map_neg]
+
+lemma map_add_le (x y : V) : e (x + y) ≤ e x + e y := e.map_add_le' x y
+
+lemma map_sub_le (x y : V) : e (x - y) ≤ e x + e y :=
+calc e (x - y) ≤ e x + e (-y) : e.map_add_le x (-y)
+           ... = e x + e y    : by rw [e.map_neg]
+
+instance : partial_order (enorm 𝕜 V) :=
+{ le := λ e₁ e₂, ∀ x, e₁ x ≤ e₂ x,
+  le_refl := λ e x, le_refl _,
+  le_trans := λ e₁ e₂ e₃ h₁₂ h₂₃ x, le_trans (h₁₂ x) (h₂₃ x),
+  le_antisymm := λ e₁ e₂ h₁₂ h₂₁, ext $ λ x, le_antisymm (h₁₂ x) (h₂₁ x) }
+
+/-- The `enorm` sending each non-zero vector to infinity. -/
+noncomputable instance : has_top (enorm 𝕜 V) :=
+⟨{ to_fun := λ x, if x = 0 then 0 else ⊤,
+   eq_zero' := λ x, by { split_ifs; simp [*] },
+   map_add_le' := λ x y,
+     begin
+       split_ifs with hxy hx hy hy hx hy hy; try { simp [*] },
+       simpa [hx, hy] using hxy
+     end,
+   map_smul_le' := λ c x,
+     begin
+       split_ifs with hcx hx hx; simp only [smul_eq_zero, not_or_distrib] at hcx,
+       { simp only [mul_zero, le_refl] },
+       { have : c = 0, by tauto,
+         simp [this] },
+       { tauto },
+       { simp [hcx.1] }
+     end }⟩
+
+noncomputable instance : inhabited (enorm 𝕜 V) := ⟨⊤⟩
+
+lemma top_map {x : V} (hx : x ≠ 0) : (⊤ : enorm 𝕜 V) x = ⊤ := if_neg hx
+
+noncomputable instance : semilattice_sup_top (enorm 𝕜 V) :=
+{ le := (≤),
+  lt := (<),
+  top := ⊤,
+  le_top := λ e x, if h : x = 0 then by simp [h] else by simp [top_map h],
+  sup := λ e₁ e₂,
+  { to_fun := λ x, max (e₁ x) (e₂ x),
+    eq_zero' := λ x h, e₁.eq_zero_iff.1 (ennreal.max_eq_zero_iff.1 h).1,
+    map_add_le' := λ x y, max_le
+      (le_trans (e₁.map_add_le _ _) $ add_le_add' (le_max_left _ _) (le_max_left _ _))
+      (le_trans (e₂.map_add_le _ _) $ add_le_add' (le_max_right _ _) (le_max_right _ _)),
+    map_smul_le' := λ c x, le_of_eq $ by simp only [map_smul, ennreal.mul_max] },
+  le_sup_left := λ e₁ e₂ x, le_max_left _ _,
+  le_sup_right := λ e₁ e₂ x, le_max_right _ _,
+  sup_le := λ e₁ e₂ e₃ h₁ h₂ x, max_le (h₁ x) (h₂ x),
+  .. enorm.partial_order }
+
+@[simp, norm_cast] lemma coe_max (e₁ e₂ : enorm 𝕜 V) : ⇑(e₁ ⊔ e₂) = λ x, max (e₁ x) (e₂ x) := rfl
+
+@[norm_cast]
+lemma max_map (e₁ e₂ : enorm 𝕜 V) (x : V) : (e₁ ⊔ e₂) x = max (e₁ x) (e₂ x) := rfl
+
+/-- Structure of an `emetric_space` defined by an extended norm. -/
+def emetric_space : emetric_space V :=
+{ edist := λ x y, e (x - y),
+  edist_self := λ x, by simp,
+  eq_of_edist_eq_zero := λ x y, by simp [sub_eq_zero],
+  edist_comm := e.map_sub_rev,
+  edist_triangle := λ x y z,
+    calc e (x - z) = e ((x - y) + (y - z)) : by rw [sub_add_sub_cancel]
+               ... ≤ e (x - y) + e (y - z) : e.map_add_le (x - y) (y - z) }
+
+/-- The subspace of vectors with finite enorm. -/
+def finite_subspace : subspace 𝕜 V :=
+{ carrier := {x | e x < ⊤},
+  zero    := by simp,
+  add     := λ x y hx hy, lt_of_le_of_lt (e.map_add_le x y) (ennreal.add_lt_top.2 ⟨hx, hy⟩),
+  smul    := λ c x hx,
+    calc e (c • x) = nnnorm c * e x : e.map_smul c x
+               ... < ⊤              : ennreal.mul_lt_top ennreal.coe_lt_top hx }
+
+/-- Metric space structure on `e.finite_subspace`. We use `emetric_space.to_metric_space_of_dist`
+to ensure that this definition agrees with `e.emetric_space`. -/
+instance : metric_space e.finite_subspace :=
+begin
+  letI := e.emetric_space,
+  refine emetric_space.to_metric_space_of_dist _ (λ x y, _) (λ x y, rfl),
+  change e (x - y) ≠ ⊤,
+  rw [← ennreal.lt_top_iff_ne_top],
+  exact lt_of_le_of_lt (e.map_sub_le x y) (ennreal.add_lt_top.2 ⟨x.2, y.2⟩)
+end
+
+lemma finite_dist_eq (x y : e.finite_subspace) : dist x y = (e (x - y)).to_real := rfl
+
+lemma finite_edist_eq (x y : e.finite_subspace) : edist x y = e (x - y) := rfl
+
+/-- Normed group instance on `e.finite_subspace`. -/
+instance : normed_group e.finite_subspace :=
+{ norm := λ x, (e x).to_real,
+  dist_eq := λ x y, rfl }
+
+lemma finite_norm_eq (x : e.finite_subspace) : ∥x∥ = (e x).to_real := rfl
+
+/-- Normed space instance on `e.finite_subspace`. -/
+instance : normed_space 𝕜 e.finite_subspace :=
+{ norm_smul_le := λ c x, le_of_eq $ by simp [finite_norm_eq, ← ennreal.to_real_mul_to_real] }
+
+end enorm