chore(analysis/normed_space/basic): continuous_at.norm etc (#5411)

Add variants of the lemma that the norm is continuous.  Also rewrite a few proofs, and rename three lemmas:

* `lim_norm` -> `tendsto_norm_sub_self`
* `lim_norm_zero` -> `tendsto_norm_zero`
* `lim_norm_zero'` -> `tendsto_norm_zero'`



Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>

src/analysis/calculus/fderiv.lean

@@ -2255,7 +2255,7 @@ begin
   { refine (inverse_add_norm_diff_second_order x).trans_is_o ((is_o_norm_norm).mp _),
     simp only [normed_field.norm_pow, norm_norm],
     have h12 : 1 < 2 := by norm_num,
-    convert (asymptotics.is_o_pow_pow h12).comp_tendsto lim_norm_zero,
+    convert (asymptotics.is_o_pow_pow h12).comp_tendsto tendsto_norm_zero,
     ext, simp },
   have h_lim : tendsto (λ (y:R), y - x) (𝓝 x) (𝓝 0),
   { refine tendsto_zero_iff_norm_tendsto_zero.mpr _,

src/analysis/normed_space/basic.lean

@@ -381,14 +381,12 @@ lemma norm_le_pi_norm {π : ι → Type*} [fintype ι] [∀i, normed_group (π i
 (pi_norm_le_iff (norm_nonneg x)).1 (le_refl _) i
 
 lemma tendsto_iff_norm_tendsto_zero {f : ι → β} {a : filter ι} {b : β} :
-  tendsto f a (𝓝 b) ↔ tendsto (λ e, ∥ f e - b ∥) a (𝓝 0) :=
-by rw tendsto_iff_dist_tendsto_zero ; simp only [(dist_eq_norm _ _).symm]
+  tendsto f a (𝓝 b) ↔ tendsto (λ e, ∥f e - b∥) a (𝓝 0) :=
+by { convert tendsto_iff_dist_tendsto_zero, simp [dist_eq_norm] }
 
 lemma tendsto_zero_iff_norm_tendsto_zero {f : γ → β} {a : filter γ} :
-  tendsto f a (𝓝 0) ↔ tendsto (λ e, ∥ f e ∥) a (𝓝 0) :=
-have tendsto f a (𝓝 0) ↔ tendsto (λ e, ∥ f e - 0 ∥) a (𝓝 0) :=
-  tendsto_iff_norm_tendsto_zero,
-by simpa
+  tendsto f a (𝓝 0) ↔ tendsto (λ e, ∥f e∥) a (𝓝 0) :=
+by simp [tendsto_iff_norm_tendsto_zero]
 
 /-- Special case of the sandwich theorem: if the norm of `f` is eventually bounded by a real
 function `g` which tends to `0`, then `f` tends to `0`.
@@ -409,35 +407,67 @@ lemma squeeze_zero_norm {f : γ → α} {g : γ → ℝ} {t₀ : filter γ}
   tendsto f t₀ (𝓝 0) :=
 squeeze_zero_norm' (eventually_of_forall h) h'
 
-lemma lim_norm (x : α) : tendsto (λg : α, ∥g - x∥) (𝓝 x) (𝓝 0) :=
-tendsto_iff_norm_tendsto_zero.1 (continuous_iff_continuous_at.1 continuous_id x)
+lemma tendsto_norm_sub_self (x : α) : tendsto (λ g : α, ∥g - x∥) (𝓝 x) (𝓝 0) :=
+by simpa [dist_eq_norm] using tendsto_id.dist (tendsto_const_nhds : tendsto (λ g, (x:α)) (𝓝 x) _)
 
-lemma lim_norm_zero : tendsto (λg : α, ∥g∥) (𝓝 0) (𝓝 0) :=
-by simpa using lim_norm (0:α)
+lemma tendsto_norm {x : α} : tendsto (λg : α, ∥g∥) (𝓝 x) (𝓝 ∥x∥) :=
+by simpa using tendsto_id.dist (tendsto_const_nhds : tendsto (λ g, (0:α)) _ _)
 
-lemma continuous_norm : continuous (λg:α, ∥g∥) :=
-begin
-  rw continuous_iff_continuous_at,
-  intro x,
-  rw [continuous_at, tendsto_iff_dist_tendsto_zero],
-  exact squeeze_zero (λ t, abs_nonneg _) (λ t, abs_norm_sub_norm_le _ _) (lim_norm x)
-end
+lemma tendsto_norm_zero : tendsto (λg : α, ∥g∥) (𝓝 0) (𝓝 0) :=
+by simpa using tendsto_norm_sub_self (0:α)
 
-lemma filter.tendsto.norm {β : Type*} {l : filter β} {f : β → α} {a : α} (h : tendsto f l (𝓝 a)) :
-  tendsto (λ x, ∥f x∥) l (𝓝 ∥a∥) :=
-tendsto.comp continuous_norm.continuous_at h
-
-lemma continuous.norm [topological_space γ] {f : γ → α} (hf : continuous f) :
-  continuous (λ x, ∥f x∥) :=
-continuous_norm.comp hf
+lemma continuous_norm : continuous (λg:α, ∥g∥) :=
+by simpa using continuous_id.dist (continuous_const : continuous (λ g, (0:α)))
 
 lemma continuous_nnnorm : continuous (nnnorm : α → ℝ≥0) :=
 continuous_subtype_mk _ continuous_norm
 
-lemma filter.tendsto.nnnorm {β : Type*} {l : filter β} {f : β → α} {a : α} (h : tendsto f l (𝓝 a)) :
+lemma tendsto_norm_nhds_within_zero : tendsto (norm : α → ℝ) (𝓝[{0}ᶜ] 0) (𝓝[set.Ioi 0] 0) :=
+(continuous_norm.tendsto' (0 : α) 0 norm_zero).inf $ tendsto_principal_principal.2 $
+  λ x, norm_pos_iff.2
+
+section
+
+variables {l : filter γ} {f : γ → α} {a : α}
+
+lemma filter.tendsto.norm {a : α} (h : tendsto f l (𝓝 a)) : tendsto (λ x, ∥f x∥) l (𝓝 ∥a∥) :=
+tendsto_norm.comp h
+
+lemma filter.tendsto.nnnorm (h : tendsto f l (𝓝 a)) :
   tendsto (λ x, nnnorm (f x)) l (𝓝 (nnnorm a)) :=
 tendsto.comp continuous_nnnorm.continuous_at h
 
+end
+
+section
+
+variables [topological_space γ] {f : γ → α} {s : set γ} {a : γ} {b : α}
+
+lemma continuous.norm (h : continuous f) : continuous (λ x, ∥f x∥) := continuous_norm.comp h
+
+lemma continuous.nnnorm (h : continuous f) : continuous (λ x, nnnorm (f x)) :=
+continuous_nnnorm.comp h
+
+lemma continuous_at.norm (h : continuous_at f a) : continuous_at (λ x, ∥f x∥) a := h.norm
+
+lemma continuous_at.nnnorm (h : continuous_at f a) : continuous_at (λ x, nnnorm (f x)) a := h.nnnorm
+
+lemma continuous_within_at.norm (h : continuous_within_at f s a) :
+  continuous_within_at (λ x, ∥f x∥) s a :=
+h.norm
+
+lemma continuous_within_at.nnnorm (h : continuous_within_at f s a) :
+  continuous_within_at (λ x, nnnorm (f x)) s a :=
+h.nnnorm
+
+lemma continuous_on.norm (h : continuous_on f s) : continuous_on (λ x, ∥f x∥) s :=
+λ x hx, (h x hx).norm
+
+lemma continuous_on.nnnorm (h : continuous_on f s) : continuous_on (λ x, nnnorm (f x)) s :=
+λ x hx, (h x hx).nnnorm
+
+end
+
 /-- If `∥y∥→∞`, then we can assume `y≠x` for any fixed `x`. -/
 lemma eventually_ne_of_tendsto_norm_at_top {l : filter γ} {f : γ → α}
   (h : tendsto (λ y, ∥f y∥) l at_top) (x : α) :
@@ -600,7 +630,7 @@ instance normed_ring_top_monoid [normed_ring α] : has_continuous_mul α :=
 instance normed_top_ring [normed_ring α] : topological_ring α :=
 ⟨ continuous_iff_continuous_at.2 $ λ x, tendsto_iff_norm_tendsto_zero.2 $
     have ∀ e : α, -e - -x = -(e - x), by intro; simp,
-    by simp only [this, norm_neg]; apply lim_norm ⟩
+    by simp only [this, norm_neg]; apply tendsto_norm_sub_self ⟩
 
 /-- A normed field is a field with a norm satisfying ∥x y∥ = ∥x∥ ∥y∥. -/
 class normed_field (α : Type*) extends has_norm α, field α, metric_space α :=

src/analysis/normed_space/bounded_linear_maps.lean

@@ -114,7 +114,7 @@ tendsto_iff_norm_tendsto_zero.2 $
       calc ∥f e - f x∥ = ∥hf.mk' f (e - x)∥ : by rw (hf.mk' _).map_sub e x; refl
                    ... ≤ M * ∥e - x∥        : hM (e - x))
     (suffices tendsto (λ (e : E), M * ∥e - x∥) (𝓝 x) (𝓝 (M * 0)), by simpa,
-      tendsto_const_nhds.mul (lim_norm _))
+      tendsto_const_nhds.mul (tendsto_norm_sub_self _))
 
 lemma continuous (hf : is_bounded_linear_map 𝕜 f) : continuous f :=
 continuous_iff_continuous_at.2 $ λ _, hf.tendsto _

src/analysis/specific_limits.lean

@@ -69,13 +69,13 @@ lemma nat.tendsto_pow_at_top_at_top_of_one_lt {m : ℕ} (h : 1 < m) :
 nat.sub_add_cancel (le_of_lt h) ▸
   tendsto_add_one_pow_at_top_at_top_of_pos (nat.sub_pos_of_lt h)
 
-lemma lim_norm_zero' {𝕜 : Type*} [normed_group 𝕜] :
+lemma tendsto_norm_zero' {𝕜 : Type*} [normed_group 𝕜] :
   tendsto (norm : 𝕜 → ℝ) (𝓝[{x | x ≠ 0}] 0) (𝓝[set.Ioi 0] 0) :=
-lim_norm_zero.inf $ tendsto_principal_principal.2 $ λ x hx, norm_pos_iff.2 hx
+tendsto_norm_zero.inf $ tendsto_principal_principal.2 $ λ x hx, norm_pos_iff.2 hx
 
 lemma normed_field.tendsto_norm_inverse_nhds_within_0_at_top {𝕜 : Type*} [normed_field 𝕜] :
   tendsto (λ x:𝕜, ∥x⁻¹∥) (𝓝[{x | x ≠ 0}] 0) at_top :=
-(tendsto_inv_zero_at_top.comp lim_norm_zero').congr $ λ x, (normed_field.norm_inv x).symm
+(tendsto_inv_zero_at_top.comp tendsto_norm_zero').congr $ λ x, (normed_field.norm_inv x).symm
 
 lemma tendsto_pow_at_top_nhds_0_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
   tendsto (λn:ℕ, r^n) at_top (𝓝 0) :=

src/topology/basic.lean

@@ -1000,6 +1000,12 @@ lemma continuous.tendsto {f : α → β} (hf : continuous f) (x) :
 ((nhds_basis_opens x).tendsto_iff $ nhds_basis_opens $ f x).2 $
   λ t ⟨hxt, ht⟩, ⟨f ⁻¹' t, ⟨hxt, ht.preimage hf⟩, subset.refl _⟩
 
+/-- A version of `continuous.tendsto` that allows one to specify a simpler form of the limit.
+E.g., one can write `continuous_exp.tendsto' 0 1 exp_zero`. -/
+lemma continuous.tendsto' {f : α → β} (hf : continuous f) (x : α) (y : β) (h : f x = y) :
+  tendsto f (𝓝 x) (𝓝 y) :=
+h ▸ hf.tendsto x
+
 lemma continuous.continuous_at {f : α → β} {x : α} (h : continuous f) :
   continuous_at f x :=
 h.tendsto x