refactor(analysis/normed_space): use lt in rescale_to_shell, DRY (#…

…4969)

* Use strict inequality for the upper bound in `rescale_to_shell`.
* Deduplicate some proofs about operator norm.
* Add `linear_map.bound_of_shell`, `continuous_linear_map.op_norm_le_of_shell`, and `continuous_linear_map.op_norm_le_of_shell'`.

src/analysis/calculus/fderiv.lean

@@ -454,7 +454,7 @@ as this statement is empty. -/
 lemma has_fderiv_within_at_of_not_mem_closure (h : x ∉ closure s) :
   has_fderiv_within_at f f' s x :=
 begin
-  simp [mem_closure_iff_nhds_within_ne_bot, ne_bot] at h,
+  simp only [mem_closure_iff_nhds_within_ne_bot, ne_bot, ne.def, not_not] at h,
   simp [has_fderiv_within_at, has_fderiv_at_filter, h, is_o, is_O_with],
 end
 

src/analysis/normed_space/banach.lean

@@ -52,12 +52,12 @@ begin
     exacts [inv_nonneg.2 (div_nonneg (le_of_lt εpos) (by norm_num)), n.cast_nonneg] },
   { by_cases hy : y = 0,
     { use 0, simp [hy] },
-    { rcases rescale_to_shell hc (half_pos εpos) hy with ⟨d, hd, ydle, leyd, dinv⟩,
+    { rcases rescale_to_shell hc (half_pos εpos) hy with ⟨d, hd, ydlt, leyd, dinv⟩,
       let δ := ∥d∥ * ∥y∥/4,
       have δpos : 0 < δ :=
         div_pos (mul_pos (norm_pos_iff.2 hd) (norm_pos_iff.2 hy)) (by norm_num),
       have : a + d • y ∈ ball a ε,
-        by simp [dist_eq_norm, lt_of_le_of_lt ydle (half_lt_self εpos)],
+        by simp [dist_eq_norm, lt_of_le_of_lt ydlt.le (half_lt_self εpos)],
       rcases metric.mem_closure_iff.1 (H this) _ δpos with ⟨z₁, z₁im, h₁⟩,
       rcases (mem_image _ _ _).1 z₁im with ⟨x₁, hx₁, xz₁⟩,
       rw ← xz₁ at h₁,

src/analysis/normed_space/basic.lean

@@ -955,7 +955,7 @@ open normed_field
 any shell of width `∥c∥`. Also recap information on the norm of the rescaling element that shows
 up in applications. -/
 lemma rescale_to_shell {c : α} (hc : 1 < ∥c∥) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : x ≠ 0) :
-  ∃d:α, d ≠ 0 ∧ ∥d • x∥ ≤ ε ∧ (ε/∥c∥ ≤ ∥d • x∥) ∧ (∥d∥⁻¹ ≤ ε⁻¹ * ∥c∥ * ∥x∥) :=
+  ∃d:α, d ≠ 0 ∧ ∥d • x∥ < ε ∧ (ε/∥c∥ ≤ ∥d • x∥) ∧ (∥d∥⁻¹ ≤ ε⁻¹ * ∥c∥ * ∥x∥) :=
 begin
   have xεpos : 0 < ∥x∥/ε := div_pos (norm_pos_iff.2 hx) εpos,
   rcases exists_int_pow_near xεpos hc with ⟨n, hn⟩,
@@ -964,9 +964,9 @@ begin
   refine ⟨(c^(n+1))⁻¹, _, _, _, _⟩,
   show (c ^ (n + 1))⁻¹  ≠ 0,
     by rwa [ne.def, inv_eq_zero, ← ne.def, ← norm_pos_iff],
-  show ∥(c ^ (n + 1))⁻¹ • x∥ ≤ ε,
-  { rw [norm_smul, norm_inv, ← div_eq_inv_mul, div_le_iff cnpos, mul_comm, norm_fpow],
-    exact (div_le_iff εpos).1 (le_of_lt (hn.2)) },
+  show ∥(c ^ (n + 1))⁻¹ • x∥ < ε,
+  { rw [norm_smul, norm_inv, ← div_eq_inv_mul, div_lt_iff cnpos, mul_comm, norm_fpow],
+    exact (div_lt_iff εpos).1 (hn.2) },
   show ε / ∥c∥ ≤ ∥(c ^ (n + 1))⁻¹ • x∥,
   { rw [div_le_iff cpos, norm_smul, norm_inv, norm_fpow, fpow_add (ne_of_gt cpos),
         fpow_one, mul_inv_rev', mul_comm, ← mul_assoc, ← mul_assoc, mul_inv_cancel (ne_of_gt cpos),

src/analysis/normed_space/multilinear.lean

@@ -114,7 +114,7 @@ begin
     rw [f.map_coord_zero i hi, norm_zero],
     exact mul_nonneg (le_of_lt C_pos) (prod_nonneg (λi hi, norm_nonneg _)) },
   { push_neg at h,
-    have : ∀i, ∃d:𝕜, d ≠ 0 ∧ ∥d • m i∥ ≤ δ ∧ (δ/∥c∥ ≤ ∥d • m i∥) ∧ (∥d∥⁻¹ ≤ δ⁻¹ * ∥c∥ * ∥m i∥) :=
+    have : ∀i, ∃d:𝕜, d ≠ 0 ∧ ∥d • m i∥ < δ ∧ (δ/∥c∥ ≤ ∥d • m i∥) ∧ (∥d∥⁻¹ ≤ δ⁻¹ * ∥c∥ * ∥m i∥) :=
       λi, rescale_to_shell hc δ_pos (h i),
     choose d hd using this,
     have A : 0 ≤ 1 + ∥f 0∥ := add_nonneg zero_le_one (norm_nonneg _),
@@ -127,7 +127,7 @@ begin
       ... = (∏ i, ∥d i∥⁻¹) * ∥f (λi, d i • m i)∥ :
         by { rw [norm_smul, normed_field.norm_prod], congr' with i, rw normed_field.norm_inv }
       ... ≤ (∏ i, ∥d i∥⁻¹) * (1 + ∥f 0∥) :
-        mul_le_mul_of_nonneg_left (H ((pi_norm_le_iff (le_of_lt δ_pos)).2 (λi, (hd i).2.1)))
+        mul_le_mul_of_nonneg_left (H ((pi_norm_le_iff (le_of_lt δ_pos)).2 (λi, (hd i).2.1.le)))
           (prod_nonneg B)
       ... ≤ (∏ i, δ⁻¹ * ∥c∥ * ∥m i∥) * (1 + ∥f 0∥) :
         mul_le_mul_of_nonneg_right (prod_le_prod B (λi hi, (hd i).2.2.2)) A

src/analysis/normed_space/operator_norm.lean

@@ -158,36 +158,35 @@ variables [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 
 (c : 𝕜) (f g : E →L[𝕜] F) (h : F →L[𝕜] G) (x y z : E)
 include 𝕜
 
-/-- A continuous linear map between normed spaces is bounded when the field is nondiscrete.
-The continuity ensures boundedness on a ball of some radius `δ`. The nondiscreteness is then
-used to rescale any element into an element of norm in `[δ/C, δ]`, whose image has a controlled norm.
-The norm control for the original element follows by rescaling. -/
+lemma linear_map.bound_of_shell (f : E →ₗ[𝕜] F) {ε C : ℝ} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ∥c∥)
+  (hf : ∀ x, ε / ∥c∥ ≤ ∥x∥ → ∥x∥ < ε → ∥f x∥ ≤ C * ∥x∥) (x : E) :
+  ∥f x∥ ≤ C * ∥x∥ :=
+begin
+  by_cases hx : x = 0, { simp [hx] },
+  rcases rescale_to_shell hc ε_pos hx with ⟨δ, hδ, δxle, leδx, δinv⟩,
+  simpa only [f.map_smul, norm_smul, mul_left_comm C, mul_le_mul_left (norm_pos_iff.2 hδ)]
+    using hf (δ • x) leδx δxle
+end
+
+/-- A continuous linear map between normed spaces is bounded when the field is nondiscrete. The
+continuity ensures boundedness on a ball of some radius `ε`. The nondiscreteness is then used to
+rescale any element into an element of norm in `[ε/C, ε]`, whose image has a controlled norm. The
+norm control for the original element follows by rescaling. -/
 lemma linear_map.bound_of_continuous (f : E →ₗ[𝕜] F) (hf : continuous f) :
   ∃ C, 0 < C ∧ (∀ x : E, ∥f x∥ ≤ C * ∥x∥) :=
 begin
   have : continuous_at f 0 := continuous_iff_continuous_at.1 hf _,
-  rcases metric.tendsto_nhds_nhds.1 this 1 zero_lt_one with ⟨ε, ε_pos, hε⟩,
-  let δ := ε/2,
-  have δ_pos : δ > 0 := half_pos ε_pos,
-  have H : ∀{a}, ∥a∥ ≤ δ → ∥f a∥ ≤ 1,
-  { assume a ha,
-    have : dist (f a) (f 0) ≤ 1,
-    { apply le_of_lt (hε _),
-      rw [dist_eq_norm, sub_zero],
-      exact lt_of_le_of_lt ha (half_lt_self ε_pos) },
-    simpa using this },
+  rcases (nhds_basis_closed_ball.tendsto_iff nhds_basis_closed_ball).1 this 1 zero_lt_one
+    with ⟨ε, ε_pos, hε⟩,
+  simp only [mem_closed_ball, dist_zero_right, f.map_zero] at hε,
   rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
-  refine ⟨δ⁻¹ * ∥c∥, mul_pos (inv_pos.2 δ_pos) (lt_trans zero_lt_one hc), (λx, _)⟩,
-  by_cases h : x = 0,
-  { simp only [h, norm_zero, mul_zero, linear_map.map_zero] },
-  { rcases rescale_to_shell hc δ_pos h with ⟨d, hd, dxle, ledx, dinv⟩,
-    calc ∥f x∥
-      = ∥f ((d⁻¹ * d) • x)∥ : by rwa [inv_mul_cancel, one_smul]
-      ... = ∥d∥⁻¹ * ∥f (d • x)∥ :
-        by rw [mul_smul, linear_map.map_smul, norm_smul, normed_field.norm_inv]
-      ... ≤ ∥d∥⁻¹ * 1 :
-        mul_le_mul_of_nonneg_left (H dxle) (by { rw ← normed_field.norm_inv, exact norm_nonneg _ })
-      ... ≤ δ⁻¹ * ∥c∥ * ∥x∥ : by { rw mul_one, exact dinv } }
+  refine ⟨ε⁻¹ * ∥c∥, mul_pos (inv_pos.2 ε_pos) (lt_trans zero_lt_one hc), _⟩,
+  suffices : ∀ x, ε / ∥c∥ ≤ ∥x∥ → ∥x∥ < ε → ∥f x∥ ≤ ε⁻¹ * ∥c∥ * ∥x∥,
+    from f.bound_of_shell ε_pos hc this,
+  intros x hle hlt,
+  refine (hε _ hlt.le).trans _,
+  rwa [mul_assoc, ← div_le_iff' (inv_pos.2 ε_pos), div_eq_mul_inv, inv_inv', one_mul,
+    ← div_le_iff' (zero_lt_one.trans hc)]
 end
 
 namespace continuous_linear_map
@@ -263,6 +262,9 @@ classical.by_cases
 theorem le_op_norm_of_le {c : ℝ} {x} (h : ∥x∥ ≤ c) : ∥f x∥ ≤ ∥f∥ * c :=
 le_trans (f.le_op_norm x) (mul_le_mul_of_nonneg_left h f.op_norm_nonneg)
 
+theorem le_of_op_norm_le {c : ℝ} (h : ∥f∥ ≤ c) (x : E) : ∥f x∥ ≤ c * ∥x∥ :=
+(f.le_op_norm x).trans (mul_le_mul_of_nonneg_right h (norm_nonneg x))
+
 /-- continuous linear maps are Lipschitz continuous. -/
 theorem lipschitz : lipschitz_with ⟨∥f∥, op_norm_nonneg f⟩ f :=
 lipschitz_with.of_dist_le_mul $ λ x y,
@@ -284,22 +286,31 @@ theorem op_norm_le_of_lipschitz {f : E →L[𝕜] F} {K : nnreal} (hf : lipschit
   ∥f∥ ≤ K :=
 f.op_norm_le_bound K.2 $ λ x, by simpa only [dist_zero_right, f.map_zero] using hf.dist_le_mul x 0
 
+lemma op_norm_le_of_shell {f : E →L[𝕜] F} {ε C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C)
+  {c : 𝕜} (hc : 1 < ∥c∥) (hf : ∀ x, ε / ∥c∥ ≤ ∥x∥ → ∥x∥ < ε → ∥f x∥ ≤ C * ∥x∥) :
+  ∥f∥ ≤ C :=
+f.op_norm_le_bound hC $ (f : E →ₗ[𝕜] F).bound_of_shell ε_pos hc hf
+
 lemma op_norm_le_of_ball {f : E →L[𝕜] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C)
   (hf : ∀ x ∈ ball (0 : E) ε, ∥f x∥ ≤ C * ∥x∥) : ∥f∥ ≤ C :=
 begin
-  apply f.op_norm_le_bound hC,
-  intros x,
   rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
-  by_cases hx : x = 0, { simp [hx] },
-  rcases rescale_to_shell hc (half_pos ε_pos) hx with ⟨δ, hδ, δxle, leδx, δinv⟩,
-  have δx_in : δ • x ∈ ball (0 : E) ε,
-  { rw [mem_ball, dist_eq_norm, sub_zero],
-    linarith },
-  calc ∥f x∥ = ∥f ((1/δ) • δ • x)∥ : by simp [hδ, smul_smul]
-  ... = ∥1/δ∥ * ∥f (δ • x)∥ : by simp [norm_smul]
-  ... ≤ ∥1/δ∥ * (C*∥δ • x∥) : mul_le_mul_of_nonneg_left _ (norm_nonneg _)
-  ... = C * ∥x∥ : by { rw norm_smul, field_simp [hδ], ring },
-  exact hf _ δx_in
+  refine op_norm_le_of_shell ε_pos hC hc (λ x _ hx, hf x _),
+  rwa ball_0_eq
+end
+
+lemma op_norm_le_of_shell' {f : E →L[𝕜] F} {ε C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C)
+  {c : 𝕜} (hc : ∥c∥ < 1) (hf : ∀ x, ε * ∥c∥ ≤ ∥x∥ → ∥x∥ < ε → ∥f x∥ ≤ C * ∥x∥) :
+  ∥f∥ ≤ C :=
+begin
+  by_cases h0 : c = 0,
+  { refine op_norm_le_of_ball ε_pos hC (λ x hx, hf x _ _),
+    { simp [h0] },
+    { rwa ball_0_eq at hx } },
+  { rw [← inv_inv' c, normed_field.norm_inv,
+      inv_lt_one_iff_of_pos (norm_pos_iff.2 $ inv_ne_zero h0)] at hc,
+    refine op_norm_le_of_shell ε_pos hC hc _,
+    rwa [normed_field.norm_inv, div_eq_mul_inv, inv_inv'] }
 end
 
 lemma op_norm_eq_of_bounds {φ : E →L[𝕜] F} {M : ℝ} (M_nonneg : 0 ≤ M)
@@ -427,17 +438,16 @@ by a positive factor.-/
 theorem antilipschitz_of_uniform_embedding (hf : uniform_embedding f) :
   ∃ K, antilipschitz_with K f :=
 begin
-  obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ) (H : ε > 0), ∀ {x y : E}, dist (f x) (f y) < ε → dist x y < 1, from
-    (uniform_embedding_iff.1 hf).2.2 1 zero_lt_one,
+  obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ) (H : ε > 0), ∀ {x y : E}, dist (f x) (f y) < ε → dist x y < 1,
+    from (uniform_embedding_iff.1 hf).2.2 1 zero_lt_one,
   let δ := ε/2,
   have δ_pos : δ > 0 := half_pos εpos,
   have H : ∀{x}, ∥f x∥ ≤ δ → ∥x∥ ≤ 1,
   { assume x hx,
     have : dist x 0 ≤ 1,
-    { apply le_of_lt,
-      apply hε,
-      simp [dist_eq_norm],
-      exact lt_of_le_of_lt hx (half_lt_self εpos) },
+    { refine (hε _).le,
+      rw [f.map_zero, dist_zero_right],
+      exact hx.trans_lt (half_lt_self εpos) },
     simpa using this },
   rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
   refine ⟨⟨δ⁻¹, _⟩ * nnnorm c, f.to_linear_map.antilipschitz_of_bound $ λx, _⟩,
@@ -446,9 +456,9 @@ begin
   { have : f x = f 0, by { simp [hx] },
     have : x = 0 := (uniform_embedding_iff.1 hf).1 this,
     simp [this] },
-  { rcases rescale_to_shell hc δ_pos hx with ⟨d, hd, dxle, ledx, dinv⟩,
-    have : ∥f (d • x)∥ ≤ δ, by simpa,
-    have : ∥d • x∥ ≤ 1 := H this,
+  { rcases rescale_to_shell hc δ_pos hx with ⟨d, hd, dxlt, ledx, dinv⟩,
+    rw [← f.map_smul d] at dxlt,
+    have : ∥d • x∥ ≤ 1 := H dxlt.le,
     calc ∥x∥ = ∥d∥⁻¹ * ∥d • x∥ :
       by rwa [← normed_field.norm_inv, ← norm_smul, ← mul_smul, inv_mul_cancel, one_smul]
     ... ≤ ∥d∥⁻¹ * 1 :