doc(analysis/normed_space): docstrings

jlpaca · jlpaca · commit a0369fd89d4d · 2019-03-29T16:48:04.000Z
diff --git a/src/analysis/normed_space/bounded_linear_maps.lean b/src/analysis/normed_space/bounded_linear_maps.lean
@@ -69,7 +69,6 @@ lemma has_pos_bound : ∃ M > 0, ∀ x, ∥f x∥ ≤ M * ∥x∥ :=
   ⟨max 1 M, lt_of_lt_of_le zero_lt_one (le_max_left 1 _), λ _, le_trans
   (hf _) (mul_le_mul_of_nonneg_right (le_max_right _ _) (norm_nonneg _))⟩
 
--- some lemmas about things having bounds and things being bounds
 lemma ratio_has_pos_bound : ∃ M > 0, ∀ x, ∥f x∥ / ∥x∥ ≤ M :=
   let ⟨M, hMp, hMb⟩ := has_pos_bound f in ⟨M, hMp,
   λ x, or.elim (lt_or_eq_of_le (norm_nonneg x))
@@ -79,11 +78,12 @@ lemma ratio_has_pos_bound : ∃ M > 0, ∀ x, ∥f x∥ / ∥x∥ ≤ M :=
 def of_linear_map_of_bounded {f : E →ₗ[k] F}
   (h : ∃ M, ∀ x, ∥f x∥ ≤ M * ∥x∥) : E →L[k] F := ⟨f, h⟩
 
--- the zero map and the identity maps are bounded
+/-- the zero map is bounded.     -/
 def zero : E →L[k] F := ⟨0, 0, λ x, by rw zero_mul; exact le_of_eq norm_zero⟩
+/-- the identity map is bounded. -/
 def id   : E →L[k] E := ⟨linear_map.id, 1, λ x, le_of_eq (one_mul _).symm⟩
 
--- boundedness respects a bunch of operations
+/-- the composition of two bounded linear maps is bounded. -/
 def comp (g : F →L[k] G) (f : E →L[k] F) : E →L[k] G :=
   ⟨linear_map.comp g.to_linear_map f.to_linear_map,
   let ⟨Mg, hMgp, hMgb⟩ := has_pos_bound g in
@@ -139,8 +139,6 @@ instance : vector_space k (E →L[k] F) := {
   smul_add  := λ _ _ _, ext $ λ _, smul_add _ _ _
 }
 
-
--- endomorphism algebra
 instance : ring (E →L[k] E) := {
   mul := (*),
   one := 1,
@@ -165,7 +163,7 @@ instance : algebra k (E →L[k] E) := {
   commutes' := λ _ _, ext $ λ _, map_smul _ _ _,
 }
 
--- a bounded linear map is continuous.
+/-- bounded linear maps are continuous. -/
 lemma tendsto (x : E): f →_{x} (f x) :=
   tendsto_iff_norm_tendsto_zero.2 $ let ⟨M, hf⟩ := f.bounded in
   (squeeze_zero (λ _, norm_nonneg _)
@@ -175,50 +173,12 @@ lemma tendsto (x : E): f →_{x} (f x) :=
 protected theorem continuous : continuous f :=
   continuous_iff_continuous_at.2 (tendsto f)
 
-/-
-theorem of_continuous_linear_map (f : E →ₗ[k] F) (hf : continuous f)
-  (hk : normed_field.nontrivial k) : E →L[k] F :=
-  ⟨f,
-  let ⟨ϖ, hϖn, hϖ⟩ := hk in
-    have hϖp  : 0 < ∥ϖ∥, from (norm_pos_iff _).2 hϖn,
-    have hltϖ : 1 < ∥ϖ∥⁻¹, from one_lt_inv hϖp hϖ,
-
-  let ⟨δ, hδp, hδ⟩ :=
-    exists_delta_of_continuous hf ((norm_pos_iff _).2 hϖn) 0 in
-
-  ⟨δ⁻¹, λ x, or.elim (lt_or_eq_of_le (norm_nonneg x))
-
-  (λ hxp,
-  have hδx : δ⁻¹ * ∥x∥ > 0, from mul_pos (inv_pos hδp) hxp,
-  have hη  : ∀ c : ℝ, c > 0 → ∃ η : k, c < ∥η∥ ∧ ∥η∥ ≤ c * ∥ϖ∥⁻¹, from
-  (λ c hcp, let ⟨n, hltn, hnlt⟩ := exists_int_pow_near hcp hltϖ in
-    ⟨ϖ⁻¹^(n + 1),
-    by rwa [normed_field.norm_fpow, norm_inv],
-    begin
-      have tmp : ∥ϖ∥⁻¹ ≠ 0, from _,
-      rw [normed_field.norm_fpow, norm_inv, fpow_add tmp, fpow_one],
-      exact mul_le_mul_of_nonneg_right hltn (le_of_lt (inv_pos hϖp)),
-    end⟩),
-  let ⟨η, hltη, hηlt⟩ := hη _ (mul_pos (inv_pos hδp) hxp) in
-
-    have hηp : 0 < ∥η∥, from lt_trans hδx hltη,
-    have hηn : η ≠ 0, from (norm_pos_iff _).1 hηp,
-    have hηx : ∥η⁻¹ • x∥ ≤ δ, from le_of_lt (by
-      erw [norm_smul, norm_inv, mul_comm, div_lt_iff hηp,
-      mul_comm, ←div_lt_iff hδp]; rwa [mul_comm] at hltη),
-
-    have hfηx : ∥f (η⁻¹ • x)∥ ≤ ∥ϖ∥,
-      by simp [dist_eq_norm] at hδ; exact le_of_lt (hδ _ hηx),
-
-  calc ∥f x∥ = _ : linear_map.norm_mul_map_smul f η x hηn
-  ...        ≤ ∥η∥ * ∥ϖ∥ : mul_le_mul_of_nonneg_left hfηx (norm_nonneg _)
-  ...        ≤ δ⁻¹ * ∥x∥ : by erw [le_div_iff hϖp] at hηlt; exact hηlt)
-  (λ heq,
-    have hf : f.to_fun 0 = 0, from linear_map.map_zero f,
-    by rw [←heq, (norm_eq_zero _).1 heq.symm, hf, mul_zero, norm_zero])⟩⟩
--/
 end bounded_linear_map
 
+
+-- deriv.lean is dependent on `is_bounded_linear_map`
+-- and has not yet been refactored.
+
 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 :=
diff --git a/src/analysis/normed_space/operator_norm.lean b/src/analysis/normed_space/operator_norm.lean
@@ -20,7 +20,6 @@ import topology.metric_space.lipschitz
 variable  {k : Type*}
 variables {E : Type*} {F : Type*} {G : Type*}
 
--- refactor : formulation for bundled bounded_linear_map
 section op_norm
 
 variable  [normed_field k]
@@ -35,7 +34,8 @@ noncomputable def op_norm  := real.Inf { c | c ≥ 0 ∧ ∀ x, ∥f x∥ ≤ c
 
 noncomputable instance : has_norm (bounded_linear_map k E F) := ⟨op_norm⟩
 
--- so that invocations of real.Inf_le make sense:
+-- so that invocations of real.Inf_le make sense: the set of
+-- bounds is nonempty and bounded below.
 lemma bounds_nonempty {f : bounded_linear_map k E F} :
   ∃ c, c ∈ { c | c ≥ 0 ∧ ∀ x, ∥f x∥ ≤ c * ∥x∥ } :=
   let ⟨M, hMp, hMb⟩ := f.has_pos_bound in ⟨M, le_of_lt hMp, hMb⟩
@@ -54,12 +54,12 @@ lemma le_op_norm : ∥f x∥ ≤ ∥f∥ * ∥x∥ :=
     ((real.le_Inf _ bounds_nonempty bounds_bdd_below).2
     (λ c ⟨_, hc⟩, div_le_of_le_mul hlt (by rw mul_comm; exact hc _))))
 
--- results about bounding the unit ball. (naming conventions?)
 lemma ratio_le_op_norm : ∥f x∥ / ∥x∥ ≤ ∥f∥ :=
   (or.elim (lt_or_eq_of_le (norm_nonneg _))
   (λ hlt, div_le_of_le_mul hlt (by rw mul_comm; exact le_op_norm _))
   (λ heq, by rw [←heq, div_zero]; exact op_norm_nonneg _))
 
+/-- the image of the unit ball under a bounded linear map is bounded. -/
 lemma unit_le_op_norm : ∥x∥ ≤ 1 → ∥f x∥ ≤ ∥f∥ :=
   λ hx, by rw [←(mul_one ∥f∥)];
   calc _ ≤ (op_norm f) * ∥x∥ : le_op_norm _
@@ -94,18 +94,18 @@ lemma op_norm_smul : ∥c • f∥ = ∥c∥ * ∥f∥ :=
             (by rw [ mul_comm, ←norm_smul ]; exact hc _))⟩))
         (λ heq, by rw [←heq, zero_mul]; exact hn))))
 
--- the bounded linear maps themselves form a normed space w/ the op norm
+/-- bounded linear maps themselves form a normed space w/ the op norm -/
 noncomputable instance : normed_space k (bounded_linear_map k E F) :=
   normed_space.of_core _ _ ⟨op_norm_eq_zero, op_norm_smul, op_norm_triangle⟩
 
--- operator norm is submultiplicative
+/-- operator norm is submultiplicative. -/
 lemma op_norm_comp_le : ∥comp h f∥ ≤ ∥h∥ * ∥f∥ :=
   (real.Inf_le _
   bounds_bdd_below ⟨mul_nonneg (op_norm_nonneg _) (op_norm_nonneg _),
   λ x, by rw mul_assoc; calc _ ≤ ∥h∥ * ∥f x∥: le_op_norm _
   ... ≤ _ : mul_le_mul_of_nonneg_left (le_op_norm _) (op_norm_nonneg _)⟩)
 
--- bounded linear maps are lipschitz continuous
+/-- bounded linear maps are lipschitz continuous. -/
 theorem lipschitz : lipschitz_with ∥f∥ f :=
   ⟨op_norm_nonneg _, λ x y, by rw [ dist_eq_norm, dist_eq_norm, ←map_sub];
   exact le_op_norm _⟩
