refactor(analysis/normed_space/basic): change normed_space definition (#1112)

Author: sgouezel

src/analysis/asymptotics.lean

@@ -570,7 +570,7 @@ end
 theorem is_o_one_iff {f : α → β} {l : filter α} :
   is_o f (λ x, (1 : γ)) l ↔ tendsto f l (nhds 0) :=
 begin
-  rw [normed_space.tendsto_nhds_zero, is_o], split,
+  rw [normed_group.tendsto_nhds_zero, is_o], split,
   { intros h e epos,
     filter_upwards [h (e / 2) (half_pos epos)], simp,
     intros x hx,
@@ -656,7 +656,7 @@ scalar multiplication is multiplication.
 -/
 
 section
-variables {K : Type*} [normed_field K] [normed_space K β] [normed_group γ]
+variables {K : Type*} [normed_field K] [normed_group β] [normed_space K β] [normed_group γ]
 
 set_option class.instance_max_depth 43
 
@@ -697,7 +697,7 @@ end
 end
 
 section
-variables {K : Type*} [normed_group β] [normed_field K] [normed_space K γ]
+variables {K : Type*} [normed_group β] [normed_field K] [normed_group γ] [normed_space K γ]
 
 set_option class.instance_max_depth 43
 
@@ -720,7 +720,8 @@ end
 end
 
 section
-variables {K : Type*} [normed_field K] [normed_space K β] [normed_space K γ]
+variables {K : Type*} [normed_field K] [normed_group β] [normed_space K β]
+[normed_group γ] [normed_space K γ]
 
 set_option class.instance_max_depth 43
 

src/analysis/convex.lean

@@ -18,6 +18,7 @@ local attribute [instance] classical.prop_decidable
 
 open set
 
+section vector_space
 variables {α : Type*} {β : Type*} {ι : Sort _}
   [add_comm_group α] [vector_space ℝ α] [add_comm_group β] [vector_space ℝ β]
   (A : set α) (B : set α) (x : α)
@@ -748,12 +749,12 @@ calc
     add_le_add (mul_le_mul_of_nonneg_left (le_max_left _ _) ha) (mul_le_mul_of_nonneg_left (le_max_right _ _) hb)
   ... ≤ max (f x) (f y) : by rw [←add_mul, hab, one_mul]
 
-/- This instance is necessary to guide class instance search in the lemma below. -/
-noncomputable def real_normed_space.to_has_scalar (α : Type) [normed_space ℝ α] : has_scalar ℝ α :=
-mul_action.to_has_scalar ℝ α
-local attribute [instance] real_normed_space.to_has_scalar
+end vector_space
 
-lemma convex_on_dist {α : Type} [normed_space ℝ α] (z : α) (D : set α) (hD : convex D) :
+section normed_space
+variables {α : Type*} [normed_group α] [normed_space ℝ α]
+
+lemma convex_on_dist  (z : α) (D : set α) (hD : convex D) :
   convex_on D (λz', dist z' z) :=
 begin
   apply and.intro hD,
@@ -769,8 +770,10 @@ begin
       by simp [norm_smul, normed_group.dist_eq, real.norm_eq_abs, abs_of_nonneg ha, abs_of_nonneg hb]
 end
 
-lemma convex_ball {α : Type} [normed_space ℝ α] (a : α) (r : ℝ) : convex (metric.ball a r) :=
+lemma convex_ball (a : α) (r : ℝ) : convex (metric.ball a r) :=
 by simpa using convex_lt_of_convex_on univ (λb, dist b a) (convex_on_dist _  _ convex_univ) r
 
-lemma convex_closed_ball {α : Type} [normed_space ℝ α] (a : α) (r : ℝ) : convex (metric.closed_ball a r) :=
+lemma convex_closed_ball (a : α) (r : ℝ) : convex (metric.closed_ball a r) :=
 by simpa using convex_le_of_convex_on univ (λb, dist b a) (convex_on_dist _  _ convex_univ) r
+
+end normed_space

src/analysis/normed_space/banach.lean

@@ -14,12 +14,10 @@ local attribute [instance] classical.prop_decidable
 
 open function metric set filter finset
 
-class banach_space (α : Type*) (β : Type*) [normed_field α]
-  extends normed_space α β, complete_space β
-
 variables {k : Type*} [nondiscrete_normed_field k]
-variables {E : Type*} [banach_space k E]
-variables {F : Type*} [banach_space k F] {f : E → F}
+{E : Type*} [normed_group E] [complete_space E] [normed_space k E]
+{F : Type*} [normed_group F] [complete_space F] [normed_space k F]
+{f : E → F}
 include k
 
 set_option class.instance_max_depth 70

src/analysis/normed_space/basic.lean

@@ -46,6 +46,26 @@ def normed_group.of_add_dist' [has_norm α] [add_comm_group α] [metric_space α
     { rw [sub_eq_add_neg, ← add_right_neg y], apply H2 }
   end }
 
+/-- A normed group can be built from a norm that satisfies algebraic properties. This is
+formalised in this structure. -/
+structure normed_group.core (α : Type*) [add_comm_group α] [has_norm α] :=
+(norm_eq_zero_iff : ∀ x : α, ∥x∥ = 0 ↔ x = 0)
+(triangle : ∀ x y : α, ∥x + y∥ ≤ ∥x∥ + ∥y∥)
+(norm_neg : ∀ x : α, ∥-x∥ = ∥x∥)
+
+noncomputable def normed_group.of_core (α : Type*) [add_comm_group α] [has_norm α]
+  (C : normed_group.core α) : normed_group α :=
+{ dist := λ x y, ∥x - y∥,
+  dist_eq := assume x y, by refl,
+  dist_self := assume x, (C.norm_eq_zero_iff (x - x)).mpr (show x - x = 0, by simp),
+  eq_of_dist_eq_zero := assume x y h, show (x = y), from sub_eq_zero.mp $ (C.norm_eq_zero_iff (x - y)).mp h,
+  dist_triangle := assume x y z,
+    calc ∥x - z∥ = ∥x - y + (y - z)∥ : by simp
+            ... ≤ ∥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] } }
+
 section normed_group
 variables [normed_group α] [normed_group β]
 
@@ -120,7 +140,7 @@ by rw ←norm_neg; simp
 lemma ball_0_eq (ε : ℝ) : ball (0:α) ε = {x | ∥x∥ < ε} :=
 set.ext $ assume a, by simp
 
-theorem normed_space.tendsto_nhds_zero {f : γ → α} {l : filter γ} :
+theorem normed_group.tendsto_nhds_zero {f : γ → α} {l : filter γ} :
   tendsto f l (nhds 0) ↔ ∀ ε > 0, { x | ∥ f x ∥ < ε } ∈ l :=
 begin
   rw [metric.tendsto_nhds], simp only [normed_group.dist_eq, sub_zero],
@@ -158,7 +178,7 @@ nnreal.coe_le.2 $ dist_norm_norm_le g h
 
 end nnnorm
 
-instance prod.normed_group [normed_group β] : normed_group (α × β) :=
+instance prod.normed_group : normed_group (α × β) :=
 { norm := λx, max ∥x.1∥ ∥x.2∥,
   dist_eq := assume (x y : α × β),
     show max (dist x.1 y.1) (dist x.2 y.2) = (max ∥(x - y).1∥ ∥(x - y).2∥), by simp [dist_eq_norm] }
@@ -169,7 +189,7 @@ begin have : ∥x∥ = max (∥x.fst∥) (∥x.snd∥) := rfl, rw this, simp[le_
 lemma norm_snd_le (x : α × β) : ∥x.2∥ ≤ ∥x∥ :=
 begin have : ∥x∥ = max (∥x.fst∥) (∥x.snd∥) := rfl, rw this, simp[le_max_right] end
 
-instance fintype.normed_group {π : α → Type*} [fintype α] [∀i, normed_group (π i)] :
+instance fintype.normed_group {π : ι → Type*} [fintype ι] [∀i, normed_group (π i)] :
   normed_group (Πb, π b) :=
 { norm := λf, ((finset.sup finset.univ (λ b, nnnorm (f b)) : nnreal) : ℝ),
   dist_eq := assume x y,
@@ -364,15 +384,14 @@ by rw [real.norm_eq_abs, abs_of_nonneg (norm_nonneg _)]
 
 section normed_space
 
-class normed_space (α : Type*) (β : Type*) [normed_field α]
-  extends normed_group β, vector_space α β :=
-(norm_smul : ∀ (a:α) b, norm (a • b) = has_norm.norm a * norm b)
+class normed_space (α : Type*) (β : Type*) [normed_field α] [normed_group β]
+  extends vector_space α β :=
+(norm_smul : ∀ (a:α) (b:β), norm (a • b) = has_norm.norm a * norm b)
 
-variables [normed_field α]
+variables [normed_field α] [normed_group β]
 
 instance normed_field.to_normed_space : normed_space α α :=
-{ dist_eq := normed_field.dist_eq,
-  norm_smul := normed_field.norm_mul }
+{ norm_smul := normed_field.norm_mul }
 
 set_option class.instance_max_depth 43
 
@@ -382,7 +401,8 @@ normed_space.norm_smul s x
 lemma nnnorm_smul [normed_space α β] (s : α) (x : β) : nnnorm (s • x) = nnnorm s * nnnorm x :=
 nnreal.eq $ norm_smul s x
 
-variables {E : Type*} {F : Type*} [normed_space α E] [normed_space α F]
+variables {E : Type*} {F : Type*}
+[normed_group E] [normed_space α E] [normed_group F] [normed_space α F]
 
 lemma tendsto_smul {f : γ → α} { g : γ → F} {e : filter γ} {s : α} {b : F} :
   (tendsto f e (nhds s)) → (tendsto g e (nhds b)) → tendsto (λ x, (f x) • (g x)) e (nhds (s • b)) :=
@@ -462,41 +482,12 @@ instance : normed_space α (E × F) :=
   ..prod.normed_group,
   ..prod.vector_space }
 
-instance fintype.normed_space {ι : Type*} {E : ι → Type*} [fintype ι] [∀i, normed_space α (E i)] :
-  normed_space α (Πi, E i) :=
-{ norm := λf, ((finset.univ.sup (λb, nnnorm (f b)) : nnreal) : ℝ),
-  dist_eq :=
-    assume f g, congr_arg coe $ congr_arg (finset.sup finset.univ) $
-    by funext i; exact nndist_eq_nnnorm _ _,
-  norm_smul := λ a f,
+instance fintype.normed_space {E : ι → Type*} [fintype ι] [∀i, normed_group (E i)]
+  [∀i, normed_space α (E i)] : normed_space α (Πi, E i) :=
+{ norm_smul := λ a f,
     show (↑(finset.sup finset.univ (λ (b : ι), nnnorm (a • f b))) : ℝ) =
       nnnorm a * ↑(finset.sup finset.univ (λ (b : ι), nnnorm (f b))),
-    by simp only [(nnreal.coe_mul _ _).symm, nnreal.mul_finset_sup, nnnorm_smul],
-  ..metric_space_pi,
-  ..pi.vector_space α }
-
-/-- A normed space can be built from a norm that satisfies algebraic properties. This is
-formalised in this structure. -/
-structure normed_space.core (α : Type*) (β : Type*)
-  [normed_field α] [add_comm_group β] [has_scalar α β] [has_norm β] :=
-(norm_eq_zero_iff : ∀ x : β, ∥x∥ = 0 ↔ x = 0)
-(norm_smul : ∀ c : α, ∀ x : β, ∥c • x∥ = ∥c∥ * ∥x∥)
-(triangle : ∀ x y : β, ∥x + y∥ ≤ ∥x∥ + ∥y∥)
-
-noncomputable def normed_space.of_core (α : Type*) (β : Type*)
-  [normed_field α] [add_comm_group β] [vector_space α β] [has_norm β]
-  (C : normed_space.core α β) : normed_space α β :=
-{ dist := λ x y, ∥x - y∥,
-  dist_eq := assume x y, by refl,
-  dist_self := assume x, (C.norm_eq_zero_iff (x - x)).mpr (show x - x = 0, by simp),
-  eq_of_dist_eq_zero := assume x y h, show (x = y), from sub_eq_zero.mp $ (C.norm_eq_zero_iff (x - y)).mp h,
-  dist_triangle := assume x y z,
-    calc ∥x - z∥ = ∥x - y + (y - z)∥ : by simp
-            ... ≤ ∥x - y∥ + ∥y - z∥  : C.triangle _ _,
-  dist_comm := assume x y,
-    calc ∥x - y∥ = ∥ -(1 : α) • (y - x)∥ : by simp
-             ... = ∥y - x∥ : begin rw[C.norm_smul], simp end,
-  norm_smul := C.norm_smul }
+    by simp only [(nnreal.coe_mul _ _).symm, nnreal.mul_finset_sup, nnnorm_smul] }
 
 end normed_space
 

src/analysis/normed_space/bounded_linear_maps.lean

@@ -17,15 +17,15 @@ open filter (tendsto)
 open metric
 
 variables {k : Type*} [nondiscrete_normed_field k]
-variables {E : Type*} [normed_space k E]
-variables {F : Type*} [normed_space k F]
-variables {G : Type*} [normed_space k G]
+variables {E : Type*} [normed_group E] [normed_space k E]
+variables {F : Type*} [normed_group F] [normed_space k F]
+variables {G : Type*} [normed_group G] [normed_space k G]
 
+set_option class.instance_max_depth 70
 
-set_option class.instance_max_depth 80
-
-structure is_bounded_linear_map (k : Type*) [normed_field k] {E : Type*}
-  [normed_space k E] {F : Type*} [normed_space k F] (f : E → F)
+structure is_bounded_linear_map (k : Type*) [normed_field k]
+  {E : Type*} [normed_group E] [normed_space k E]
+  {F : Type*} [normed_group F] [normed_space k F] (f : E → F)
   extends is_linear_map k f : Prop :=
 (bound : ∃ M > 0, ∀ x : E, ∥ f x ∥ ≤ M * ∥ x ∥)
 
@@ -135,7 +135,7 @@ end
 end is_bounded_linear_map
 
 section
-set_option class.instance_max_depth 250
+set_option class.instance_max_depth 180
 
 lemma is_bounded_linear_map_prod_iso :
   is_bounded_linear_map k (λ(p : (E →L[k] F) × (E →L[k] G)),
@@ -271,10 +271,11 @@ def is_bounded_bilinear_map.deriv (h : is_bounded_bilinear_map k f) (p : E × F)
   ... = (C * ∥p.1∥ + C * ∥p.2∥) * ∥q∥ : by ring
 end
 
-set_option class.instance_max_depth 150
 @[simp] lemma is_bounded_bilinear_map_deriv_coe (h : is_bounded_bilinear_map k f) (p q : E × F) :
   h.deriv p q = f (p.1, q.2) + f (q.1, p.2) := rfl
 
+set_option class.instance_max_depth 95
+
 /-- Given a bounded bilinear map `f`, the map associating to a point `p` the derivative of `f` at
 `p` is itself a bounded linear map. -/
 lemma is_bounded_bilinear_map.is_bounded_linear_map_deriv (h : is_bounded_bilinear_map k f) :

src/analysis/normed_space/deriv.lean

@@ -65,9 +65,9 @@ set_option class.instance_max_depth 100
 section
 
 variables {k : Type*} [nondiscrete_normed_field k]
-variables {E : Type*} [normed_space k E]
-variables {F : Type*} [normed_space k F]
-variables {G : Type*} [normed_space k G]
+variables {E : Type*} [normed_group E] [normed_space k E]
+variables {F : Type*} [normed_group F] [normed_space k F]
+variables {G : Type*} [normed_group G] [normed_space k G]
 
 def has_fderiv_at_filter (f : E → F) (f' : E →L[k] F) (x : E) (L : filter E) :=
 is_o (λ x', f x' - f x - f' (x' - x)) (λ x', x' - x) L
@@ -1250,9 +1250,9 @@ end
 
 section
 
-variables {E : Type*} [normed_space ℝ E]
-variables {F : Type*} [normed_space ℝ F]
-variables {G : Type*} [normed_space ℝ G]
+variables {E : Type*} [normed_group E] [normed_space ℝ E]
+variables {F : Type*} [normed_group F] [normed_space ℝ F]
+variables {G : Type*} [normed_group G] [normed_space ℝ G]
 
 theorem has_fderiv_at_filter_real_equiv {f : E → F} {f' : E →L[ℝ] F} {x : E} {L : filter E} :
   tendsto (λ x' : E, ∥x' - x∥⁻¹ * ∥f x' - f x - f' (x' - x)∥) L (nhds 0) ↔

src/analysis/normed_space/operator_norm.lean

@@ -17,7 +17,10 @@ local attribute [instance] classical.prop_decidable
 set_option class.instance_max_depth 70
 
 variables {k : Type*} {E : Type*} {F : Type*} {G : Type*}
-[nondiscrete_normed_field k] [normed_space k E] [normed_space k F] [normed_space k G]
+[nondiscrete_normed_field k]
+[normed_group E] [normed_space k E]
+[normed_group F] [normed_space k F]
+[normed_group G] [normed_space k G]
 (c : k) (f g : E →L[k] F) (h : F →L[k] G) (x y z : E)
 include k
 
@@ -193,11 +196,23 @@ le_antisymm
         end)
       (λ heq, by { rw [←heq, zero_mul], exact hn }))))
 
+lemma op_norm_neg : ∥-f∥ = ∥f∥ := calc
+  ∥-f∥ = ∥(-1:k) • f∥ : by rw neg_one_smul
+  ... = ∥(-1:k)∥ * ∥f∥ : by rw op_norm_smul
+  ... = ∥f∥ : by simp
+
 /-- Continuous linear maps themselves form a normed space with respect to
     the operator norm. -/
+instance to_normed_group : normed_group (E →L[k] F) :=
+normed_group.of_core _ ⟨op_norm_zero_iff, op_norm_triangle, op_norm_neg⟩
+
+/- The next instance should be found automatically, but it is not.
+TODO: fix me -/
+instance to_normed_group_prod : normed_group (E →L[k] (F × G)) :=
+continuous_linear_map.to_normed_group
+
 instance to_normed_space : normed_space k (E →L[k] F) :=
-normed_space.of_core _ _
-  ⟨op_norm_zero_iff, op_norm_smul, op_norm_triangle⟩
+⟨op_norm_smul⟩
 
 /-- The operator norm is submultiplicative. -/
 lemma op_norm_comp_le : ∥comp h f∥ ≤ ∥h∥ * ∥f∥ :=