Remove outparam in normed space (#844)

src/analysis/normed_space/basic.lean

@@ -330,7 +330,7 @@ by rw [real.norm_eq_abs, abs_of_nonneg (norm_nonneg _)]
 
 section normed_space
 
-class normed_space (α : out_param $ Type*) (β : Type*) [out_param $ normed_field α]
+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)
 
@@ -413,15 +413,17 @@ instance fintype.normed_space {ι : Type*} {E : ι → Type*} [fintype ι] [∀i
   ..metric_space_pi,
   ..pi.vector_space α }
 
-/-- A normed space can be build from a norm that satisfies algebraic properties. This is formalised in this structure. -/
+/-- 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*)
-  [out_param $ discrete_field α] [normed_field α] [add_comm_group β] [has_scalar α β] [has_norm β]:=
+  [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 α β :=
+  [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),
@@ -432,8 +434,7 @@ noncomputable def normed_space.of_core (α : Type*) (β : Type*)
   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
-}
+  norm_smul := C.norm_smul }
 
 end normed_space
 

src/analysis/normed_space/bounded_linear_maps.lean

@@ -28,7 +28,7 @@ variables {E : Type*} [normed_space k E]
 variables {F : Type*} [normed_space k F]
 variables {G : Type*} [normed_space k G]
 
-structure is_bounded_linear_map {k : Type*}
+structure is_bounded_linear_map (k : Type*)
   [normed_field k] {E : Type*} [normed_space k E] {F : Type*} [normed_space k F] (L : E → F)
   extends is_linear_map k L : Prop :=
 (bound : ∃ M, M > 0 ∧ ∀ x : E, ∥ L x ∥ ≤ M * ∥ x ∥)
@@ -37,79 +37,80 @@ include k
 
 lemma is_linear_map.with_bound
   {L : E → F} (hf : is_linear_map k L) (M : ℝ) (h : ∀ x : E, ∥ L x ∥ ≤ M * ∥ x ∥) :
-  is_bounded_linear_map L :=
+  is_bounded_linear_map k L :=
 ⟨ hf, classical.by_cases
   (assume : M ≤ 0, ⟨1, zero_lt_one, assume x,
     le_trans (h x) $ mul_le_mul_of_nonneg_right (le_trans this zero_le_one) (norm_nonneg x)⟩)
   (assume : ¬ M ≤ 0, ⟨M, lt_of_not_ge this, h⟩)⟩
 
 namespace is_bounded_linear_map
 
-def to_linear_map (f : E → F) (h : is_bounded_linear_map f) : E →ₗ[k] F :=
+def to_linear_map (f : E → F) (h : is_bounded_linear_map k f) : E →ₗ[k] F :=
 (is_linear_map.mk' _ h.to_is_linear_map)
 
-lemma zero : is_bounded_linear_map (λ (x:E), (0:F)) :=
+lemma zero : is_bounded_linear_map k (λ (x:E), (0:F)) :=
 (0 : E →ₗ F).is_linear.with_bound 0 $ by simp [le_refl]
 
-lemma id : is_bounded_linear_map (λ (x:E), x) :=
+lemma id : is_bounded_linear_map k (λ (x:E), x) :=
 linear_map.id.is_linear.with_bound 1 $ by simp [le_refl]
 
-lemma smul {f : E → F} (c : k) : is_bounded_linear_map f → is_bounded_linear_map (λ e, c • f e)
+set_option class.instance_max_depth 40
+lemma smul {f : E → F} (c : k) : is_bounded_linear_map k f → is_bounded_linear_map k (λ e, c • f e)
 | ⟨hf, ⟨M, hM, h⟩⟩ := (c • hf.mk' f).is_linear.with_bound (∥c∥ * M) $ assume x,
   calc ∥c • f x∥ = ∥c∥ * ∥f x∥ : norm_smul c (f x)
     ... ≤ ∥c∥ * (M * ∥x∥) : mul_le_mul_of_nonneg_left (h x) (norm_nonneg c)
     ... = (∥c∥ * M) * ∥x∥ : (mul_assoc _ _ _).symm
 
-lemma neg {f : E → F} (hf : is_bounded_linear_map f) : is_bounded_linear_map (λ e, -f e) :=
+lemma neg {f : E → F} (hf : is_bounded_linear_map k f) : is_bounded_linear_map k (λ e, -f e) :=
 begin
   rw show (λ e, -f e) = (λ e, (-1 : k) • f e), { funext, simp },
   exact smul (-1) hf
 end
 
 lemma add {f : E → F} {g : E → F} :
-  is_bounded_linear_map f → is_bounded_linear_map g → is_bounded_linear_map (λ e, f e + g e)
+  is_bounded_linear_map k f → is_bounded_linear_map k g → is_bounded_linear_map k (λ e, f e + g e)
 | ⟨hlf, Mf, hMf, hf⟩  ⟨hlg, Mg, hMg, hg⟩ := (hlf.mk' _ + hlg.mk' _).is_linear.with_bound (Mf + Mg) $ assume x,
   calc ∥f x + g x∥ ≤ ∥f x∥ + ∥g x∥ : norm_triangle _ _
     ... ≤ Mf * ∥x∥ + Mg * ∥x∥ : add_le_add (hf x) (hg x)
     ... ≤ (Mf + Mg) * ∥x∥ : by rw add_mul
 
-lemma sub {f : E → F} {g : E → F} (hf : is_bounded_linear_map f) (hg : is_bounded_linear_map g) :
-  is_bounded_linear_map (λ e, f e - g e) := add hf (neg hg)
+lemma sub {f : E → F} {g : E → F} (hf : is_bounded_linear_map k f) (hg : is_bounded_linear_map k g) :
+  is_bounded_linear_map k (λ e, f e - g e) := add hf (neg hg)
 
 lemma comp {f : E → F} {g : F → G} :
-  is_bounded_linear_map g → is_bounded_linear_map f → is_bounded_linear_map (g ∘ f)
+  is_bounded_linear_map k g → is_bounded_linear_map k f → is_bounded_linear_map k (g ∘ f)
 | ⟨hlg, Mg, hMg, hg⟩ ⟨hlf, Mf, hMf, hf⟩ := ((hlg.mk' _).comp (hlf.mk' _)).is_linear.with_bound (Mg * Mf) $ assume x,
   calc ∥g (f x)∥ ≤ Mg * ∥f x∥ : hg _
     ... ≤ Mg * (Mf * ∥x∥) : mul_le_mul_of_nonneg_left (hf _) (le_of_lt hMg)
     ... = Mg * Mf * ∥x∥ : (mul_assoc _ _ _).symm
 
-lemma tendsto {L : E → F} (x : E) : is_bounded_linear_map L → L →_{x} (L x)
+lemma tendsto {L : E → F} (x : E) : is_bounded_linear_map k L → L →_{x} (L x)
 | ⟨hL, M, hM, h_ineq⟩ := tendsto_iff_norm_tendsto_zero.2 $
   squeeze_zero (assume e, norm_nonneg _)
     (assume e, calc ∥L e - L x∥ = ∥hL.mk' L (e - x)∥ : by rw (hL.mk' _).map_sub e x; refl
       ... ≤ M*∥e-x∥ : h_ineq (e-x))
     (suffices (λ (e : E), M * ∥e - x∥) →_{x} (M * 0), by simpa,
       tendsto_mul tendsto_const_nhds (lim_norm _))
 
-lemma continuous {L : E → F} (hL : is_bounded_linear_map L) : continuous L :=
+lemma continuous {L : E → F} (hL : is_bounded_linear_map k L) : continuous L :=
 continuous_iff_continuous_at.2 $ assume x, hL.tendsto x
 
-lemma lim_zero_bounded_linear_map {L : E → F} (H : is_bounded_linear_map L) : (L →_{0} 0) :=
+lemma lim_zero_bounded_linear_map {L : E → F} (H : is_bounded_linear_map k L) : (L →_{0} 0) :=
 (H.1.mk' _).map_zero ▸ continuous_iff_continuous_at.1 H.continuous 0
 
 section
 open asymptotics filter
 
-theorem is_O_id {L : E → F} (h : is_bounded_linear_map L) (l : filter E) :
+theorem is_O_id {L : E → F} (h : is_bounded_linear_map k L) (l : filter E) :
   is_O L (λ x, x) l :=
 let ⟨M, Mpos, hM⟩ := h.bound in
 ⟨M, Mpos, mem_sets_of_superset univ_mem_sets (λ x _, hM x)⟩
 
-theorem is_O_comp {L : F → G} (h : is_bounded_linear_map L)
+theorem is_O_comp {L : F → G} (h : is_bounded_linear_map k L)
   {f : E → F} (l : filter E) : is_O (λ x', L (f x')) f l :=
 ((h.is_O_id ⊤).comp _).mono (map_le_iff_le_comap.mp lattice.le_top)
 
-theorem is_O_sub {L : E → F} (h : is_bounded_linear_map L) (l : filter E) (x : E) :
+theorem is_O_sub {L : E → F} (h : is_bounded_linear_map k L) (l : filter E) (x : E) :
   is_O (λ x', L (x' - x)) (λ x', x' - x) l :=
 is_O_comp h l
 
@@ -120,7 +121,7 @@ end is_bounded_linear_map
 -- Next lemma is stated for real normed space but it would work as soon as the base field is an extension of ℝ
 lemma bounded_continuous_linear_map
   {E : Type*} [normed_space ℝ E] {F : Type*} [normed_space ℝ F] {L : E → F}
-  (lin : is_linear_map ℝ L) (cont : continuous L) : is_bounded_linear_map L :=
+  (lin : is_linear_map ℝ L) (cont : continuous L) : is_bounded_linear_map ℝ L :=
 let ⟨δ, δ_pos, hδ⟩ := exists_delta_of_continuous cont zero_lt_one 0 in
 have HL0 : L 0 = 0, from (lin.mk' _).map_zero,
 have H : ∀{a}, ∥a∥ ≤ δ → ∥L a∥ < 1, by simpa only [HL0, dist_zero_right] using hδ,