feat(analysis/calculus): strictly differentiable (or C^1) map is loca…

…lly Lipschitz (#8362)

src/analysis/calculus/fderiv.lean

@@ -352,6 +352,25 @@ protected lemma has_strict_fderiv_at.differentiable_at (hf : has_strict_fderiv_a
   differentiable_at 𝕜 f x :=
 hf.has_fderiv_at.differentiable_at
 
+/-- If `f` is strictly differentiable at `x` with derivative `f'` and `K > ∥f'∥₊`, then `f` is
+`K`-Lipschitz in a neighborhood of `x`. -/
+lemma has_strict_fderiv_at.exists_lipschitz_on_with_of_nnnorm_lt (hf : has_strict_fderiv_at f f' x)
+  (K : ℝ≥0) (hK : ∥f'∥₊ < K) : ∃ s ∈ 𝓝 x, lipschitz_on_with K f s :=
+begin
+  have := hf.add_is_O_with (f'.is_O_with_comp _ _) hK,
+  simp only [sub_add_cancel, is_O_with] at this,
+  rcases exists_nhds_square this with ⟨U, Uo, xU, hU⟩,
+  exact ⟨U, Uo.mem_nhds xU, lipschitz_on_with_iff_norm_sub_le.2 $
+    λ x hx y hy, hU (mk_mem_prod hx hy)⟩
+end
+
+/-- If `f` is strictly differentiable at `x` with derivative `f'`, then `f` is Lipschitz in a
+neighborhood of `x`. See also `has_strict_fderiv_at.exists_lipschitz_on_with_of_nnnorm_lt` for a
+more precise statement. -/
+lemma has_strict_fderiv_at.exists_lipschitz_on_with (hf : has_strict_fderiv_at f f' x) :
+  ∃ K (s ∈ 𝓝 x), lipschitz_on_with K f s :=
+(no_top _).imp hf.exists_lipschitz_on_with_of_nnnorm_lt
+
 /-- Directional derivative agrees with `has_fderiv`. -/
 lemma has_fderiv_at.lim (hf : has_fderiv_at f f' x) (v : E) {α : Type*} {c : α → 𝕜}
   {l : filter α} (hc : tendsto (λ n, ∥c n∥) l at_top) :

src/analysis/calculus/mean_value.lean

@@ -525,10 +525,12 @@ begin
 end
 
 /-- Let `s` be a convex set in a real normed vector space `E`, let `f : E → G` be a function
-differentiable within `s` in a neighborhood of `x : E` with derivative `f'`. Suppose that `f'`
-is continuous within `s` at `x`. Then for any number `K : ℝ≥0` larger than `∥f' x∥₊`, `f` is
-`K`-Lipschitz on some neighborhood of `x` within `s`. -/
-lemma convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at_of_continuous_within_at
+differentiable within `s` in a neighborhood of `x : E` with derivative `f'`. Suppose that `f'` is
+continuous within `s` at `x`. Then for any number `K : ℝ≥0` larger than `∥f' x∥₊`, `f` is
+`K`-Lipschitz on some neighborhood of `x` within `s`. See also
+`convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at` for a version that claims
+existence of `K` instead of an explicit estimate. -/
+lemma convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at_of_nnnorm_lt
   (hs : convex s) {f : E → G} (hder : ∀ᶠ y in 𝓝[s] x, has_fderiv_within_at f (f' y) s y)
   (hcont : continuous_within_at f' s x) (K : ℝ≥0) (hK : ∥f' x∥₊ < K) :
   ∃ t ∈ 𝓝[s] x, lipschitz_on_with K f t :=
@@ -542,6 +544,19 @@ begin
     (λ y hy, (hε hy).1.mono (inter_subset_left _ _)) (λ y hy, (hε hy).2.le)
 end
 
+/-- Let `s` be a convex set in a real normed vector space `E`, let `f : E → G` be a function
+differentiable within `s` in a neighborhood of `x : E` with derivative `f'`. Suppose that `f'` is
+continuous within `s` at `x`. Then for any number `K : ℝ≥0` larger than `∥f' x∥₊`, `f` is Lipschitz
+on some neighborhood of `x` within `s`. See also
+`convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at_of_nnnorm_lt` for a version
+with an explicit estimate on the Lipschitz constant. -/
+lemma convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at
+  (hs : convex s) {f : E → G} (hder : ∀ᶠ y in 𝓝[s] x, has_fderiv_within_at f (f' y) s y)
+  (hcont : continuous_within_at f' s x) :
+  ∃ K (t ∈ 𝓝[s] x), lipschitz_on_with K f t :=
+(no_top _).imp $
+  hs.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at_of_nnnorm_lt hder hcont
+
 /-- The mean value theorem on a convex set: if the derivative of a function within this set is
 bounded by `C`, then the function is `C`-Lipschitz. Version with `fderiv_within`. -/
 theorem convex.norm_image_sub_le_of_norm_fderiv_within_le

src/analysis/calculus/times_cont_diff.lean

@@ -156,7 +156,7 @@ derivative, differentiability, higher derivative, `C^n`, multilinear, Taylor ser
 -/
 
 noncomputable theory
-open_locale classical big_operators
+open_locale classical big_operators nnreal
 
 local notation `∞` := (⊤ : with_top ℕ)
 
@@ -165,7 +165,7 @@ universes u v w
 local attribute [instance, priority 1001]
 normed_group.to_add_comm_group normed_space.to_module add_comm_group.to_add_comm_monoid
 
-open set fin
+open set fin filter
 open_locale topological_space
 
 variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
@@ -2714,6 +2714,65 @@ lemma times_cont_diff.has_strict_deriv_at
   has_strict_deriv_at f (deriv f x) x :=
 hf.times_cont_diff_at.has_strict_deriv_at hn
 
+/-- If `f` has a formal Taylor series `p` up to order `1` on `{x} ∪ s`, where `s` is a convex set,
+and `∥p x 1∥₊ < K`, then `f` is `K`-Lipschitz in a neighborhood of `x` within `s`. -/
+lemma has_ftaylor_series_up_to_on.exists_lipschitz_on_with_of_nnnorm_lt {E F : Type*}
+  [normed_group E] [normed_space ℝ E] [normed_group F] [normed_space ℝ F] {f : E → F}
+  {p : E → formal_multilinear_series ℝ E F} {s : set E} {x : E}
+  (hf : has_ftaylor_series_up_to_on 1 f p (insert x s)) (hs : convex s) (K : ℝ≥0)
+  (hK : ∥p x 1∥₊ < K) :
+  ∃ t ∈ 𝓝[s] x, lipschitz_on_with K f t :=
+begin
+  set f' := λ y, continuous_multilinear_curry_fin1 ℝ E F (p y 1),
+  have hder : ∀ y ∈ s, has_fderiv_within_at f (f' y) s y,
+    from λ y hy, (hf.has_fderiv_within_at le_rfl (subset_insert x s hy)).mono (subset_insert x s),
+  have hcont : continuous_within_at f' s x,
+    from (continuous_multilinear_curry_fin1 ℝ E F).continuous_at.comp_continuous_within_at
+      ((hf.cont _ le_rfl _ (mem_insert _ _)).mono (subset_insert x s)),
+  replace hK : ∥f' x∥₊ < K, by simpa only [linear_isometry_equiv.nnnorm_map],
+  exact hs.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at_of_nnnorm_lt
+    (eventually_nhds_within_iff.2 $ eventually_of_forall hder) hcont K hK
+end
+
+/-- If `f` has a formal Taylor series `p` up to order `1` on `{x} ∪ s`, where `s` is a convex set,
+then `f` is Lipschitz in a neighborhood of `x` within `s`. -/
+lemma has_ftaylor_series_up_to_on.exists_lipschitz_on_with {E F : Type*}
+  [normed_group E] [normed_space ℝ E] [normed_group F] [normed_space ℝ F] {f : E → F}
+  {p : E → formal_multilinear_series ℝ E F} {s : set E} {x : E}
+  (hf : has_ftaylor_series_up_to_on 1 f p (insert x s)) (hs : convex s) :
+  ∃ K (t ∈ 𝓝[s] x), lipschitz_on_with K f t :=
+(no_top _).imp $ hf.exists_lipschitz_on_with_of_nnnorm_lt hs
+
+/-- If `f` is `C^1` within a conves set `s` at `x`, then it is Lipschitz on a neighborhood of `x`
+within `s`. -/
+lemma times_cont_diff_within_at.exists_lipschitz_on_with {E F : Type*} [normed_group E]
+  [normed_space ℝ E] [normed_group F] [normed_space ℝ F] {f : E → F} {s : set E}
+  {x : E} (hf : times_cont_diff_within_at ℝ 1 f s x) (hs : convex s) :
+  ∃ (K : ℝ≥0) (t ∈ 𝓝[s] x), lipschitz_on_with K f t :=
+begin
+  rcases hf 1 le_rfl with ⟨t, hst, p, hp⟩,
+  rcases metric.mem_nhds_within_iff.mp hst with ⟨ε, ε0, hε⟩,
+  replace hp : has_ftaylor_series_up_to_on 1 f p (metric.ball x ε ∩ insert x s) := hp.mono hε,
+  clear hst hε t,
+  rw [← insert_eq_of_mem (metric.mem_ball_self ε0), ← insert_inter] at hp,
+  rcases hp.exists_lipschitz_on_with ((convex_ball _ _).inter hs) with ⟨K, t, hst, hft⟩,
+  rw [inter_comm, ← nhds_within_restrict' _ (metric.ball_mem_nhds _ ε0)] at hst,
+  exact ⟨K, t, hst, hft⟩
+end
+
+/-- If `f` is `C^1` at `x` and `K > ∥fderiv 𝕂 f x∥`, then `f` is `K`-Lipschitz in a neighborhood of
+`x`. -/
+lemma times_cont_diff_at.exists_lipschitz_on_with_of_nnnorm_lt {f : E' → F'} {x : E'}
+  (hf : times_cont_diff_at 𝕂 1 f x) (K : ℝ≥0) (hK : ∥fderiv 𝕂 f x∥₊ < K) :
+  ∃ t ∈ 𝓝 x, lipschitz_on_with K f t :=
+(hf.has_strict_fderiv_at le_rfl).exists_lipschitz_on_with_of_nnnorm_lt K hK
+
+/-- If `f` is `C^1` at `x`, then `f` is Lipschitz in a neighborhood of `x`. -/
+lemma times_cont_diff_at.exists_lipschitz_on_with {f : E' → F'} {x : E'}
+  (hf : times_cont_diff_at 𝕂 1 f x) :
+  ∃ K (t ∈ 𝓝 x), lipschitz_on_with K f t :=
+(hf.has_strict_fderiv_at le_rfl).exists_lipschitz_on_with
+
 end real
 
 section deriv

src/analysis/normed_space/basic.lean

@@ -401,7 +401,7 @@ end
 /-- A homomorphism `f` of seminormed groups is Lipschitz, if there exists a constant `C` such that
 for all `x`, one has `∥f x∥ ≤ C * ∥x∥`. The analogous condition for a linear map of
 (semi)normed spaces is in `normed_space.operator_norm`. -/
-lemma add_monoid_hom.lipschitz_of_bound (f :α →+ β) (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
+lemma add_monoid_hom.lipschitz_of_bound (f : α →+ β) (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
   lipschitz_with (real.to_nnreal C) f :=
 lipschitz_with.of_dist_le' $ λ x y, by simpa only [dist_eq_norm, f.map_sub] using h (x - y)
 
@@ -413,6 +413,10 @@ lemma lipschitz_on_with.norm_sub_le {f : α → β} {C : ℝ≥0} {s : set α} (
   {x y : α} (x_in : x ∈ s) (y_in : y ∈ s) : ∥f x - f y∥ ≤ C * ∥x - y∥ :=
 lipschitz_on_with_iff_norm_sub_le.mp h x x_in y y_in
 
+lemma lipschitz_with_iff_norm_sub_le {f : α → β} {C : ℝ≥0} :
+  lipschitz_with C f ↔ ∀ x y, ∥f x - f y∥ ≤ C * ∥x - y∥ :=
+by simp only [lipschitz_with_iff_dist_le_mul, dist_eq_norm]
+
 /-- A homomorphism `f` of seminormed groups is continuous, if there exists a constant `C` such that
 for all `x`, one has `∥f x∥ ≤ C * ∥x∥`.
 The analogous condition for a linear map of normed spaces is in `normed_space.operator_norm`. -/
@@ -542,6 +546,10 @@ lemma nnnorm_sum_le {β} : ∀(s : finset β) (f : β → α),
   ∥∑ a in s, f a∥₊ ≤ ∑ a in s, ∥f a∥₊ :=
 finset.le_sum_of_subadditive nnnorm nnnorm_zero nnnorm_add_le
 
+lemma add_monoid_hom.lipschitz_of_bound_nnnorm (f : α →+ β) (C : ℝ≥0) (h : ∀ x, ∥f x∥₊ ≤ C * ∥x∥₊) :
+  lipschitz_with C f :=
+@real.to_nnreal_coe C ▸ f.lipschitz_of_bound C h
+
 end nnnorm
 
 lemma lipschitz_with.neg {α : Type*} [pseudo_emetric_space α] {K : ℝ≥0} {f : α → β}

src/analysis/normed_space/operator_norm.lean

@@ -40,7 +40,11 @@ variables [normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜
 
 lemma linear_map.lipschitz_of_bound (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
   lipschitz_with (real.to_nnreal C) f :=
-lipschitz_with.of_dist_le' $ λ x y, by simpa only [dist_eq_norm, f.map_sub] using h (x - y)
+f.to_add_monoid_hom.lipschitz_of_bound C h
+
+lemma linear_map.lipschitz_of_bound_nnnorm (C : ℝ≥0) (h : ∀ x, ∥f x∥₊ ≤ C * ∥x∥₊) :
+  lipschitz_with C f :=
+f.to_add_monoid_hom.lipschitz_of_bound_nnnorm C h
 
 theorem linear_map.antilipschitz_of_bound {K : ℝ≥0} (h : ∀ x, ∥x∥ ≤ K * ∥f x∥) :
   antilipschitz_with K f :=
@@ -159,18 +163,7 @@ theorem bound : ∃ C, 0 < C ∧ (∀ x : E, ∥f x∥ ≤ C * ∥x∥) :=
 f.to_linear_map.bound_of_continuous f.2
 
 section
-open asymptotics filter
-
-theorem is_O_id (l : filter E) : is_O f (λ x, x) l :=
-let ⟨M, hMp, hM⟩ := f.bound in is_O_of_le' l hM
-
-theorem is_O_comp {α : Type*} (g : F →L[𝕜] G) (f : α → F) (l : filter α) :
-  is_O (λ x', g (f x')) f l :=
-(g.is_O_id ⊤).comp_tendsto le_top
-
-theorem is_O_sub (f : E →L[𝕜] F) (l : filter E) (x : E) :
-  is_O (λ x', f (x' - x)) (λ x', x' - x) l :=
-f.is_O_comp _ l
+open filter
 
 /-- A linear map which is a homothety is a continuous linear map.
     Since the field `𝕜` need not have `ℝ` as a subfield, this theorem is not directly deducible from
@@ -233,11 +226,6 @@ 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,
-  by { rw [dist_eq_norm, dist_eq_norm, ←map_sub], apply le_op_norm }
-
 lemma ratio_le_op_norm : ∥f x∥ / ∥x∥ ≤ ∥f∥ :=
 div_le_of_nonneg_of_le_mul (norm_nonneg _) f.op_norm_nonneg (le_op_norm _ _)
 
@@ -300,8 +288,8 @@ le_antisymm (φ.op_norm_le_bound M_nonneg h_above)
 
 /-- The operator norm satisfies the triangle inequality. -/
 theorem op_norm_add_le : ∥f + g∥ ≤ ∥f∥ + ∥g∥ :=
-show ∥f + g∥ ≤ (coe : ℝ≥0 → ℝ) (⟨_, f.op_norm_nonneg⟩ + ⟨_, g.op_norm_nonneg⟩),
-from op_norm_le_of_lipschitz (f.lipschitz.add g.lipschitz)
+(f + g).op_norm_le_bound (add_nonneg f.op_norm_nonneg g.op_norm_nonneg) $
+  λ x, (norm_add_le_of_le (f.le_op_norm x) (g.le_op_norm x)).trans_eq (add_mul _ _ _).symm
 
 /-- The norm of the `0` operator is `0`. -/
 theorem op_norm_zero : ∥(0 : E →L[𝕜] F)∥ = 0 :=
@@ -352,6 +340,12 @@ instance to_semi_normed_ring : semi_normed_ring (E →L[𝕜] E) :=
 { norm_mul := op_norm_comp_le,
   .. continuous_linear_map.to_semi_normed_group }
 
+theorem le_op_nnnorm : ∥f x∥₊ ≤ ∥f∥₊ * ∥x∥₊ := f.le_op_norm x
+
+/-- continuous linear maps are Lipschitz continuous. -/
+theorem lipschitz : lipschitz_with ∥f∥₊ f :=
+(f : E →ₗ[𝕜] F).lipschitz_of_bound_nnnorm _ f.le_op_nnnorm
+
 theorem le_op_norm₂ (f : E →L[𝕜] F →L[𝕜] G) (x : E) (y : F) :
   ∥f x y∥ ≤ ∥f∥ * ∥x∥ * ∥y∥ :=
 (f x).le_of_op_norm_le (f.le_op_norm x) y
@@ -396,6 +390,34 @@ f.to_linear_map.to_add_monoid_hom.isometry_iff_norm
 
 end op_norm
 
+section is_O
+
+open asymptotics
+
+theorem is_O_with_id (l : filter E) : is_O_with ∥f∥ f (λ x, x) l :=
+is_O_with_of_le' _ f.le_op_norm
+
+theorem is_O_id (l : filter E) : is_O f (λ x, x) l :=
+(f.is_O_with_id l).is_O
+
+theorem is_O_with_comp {α : Type*} (g : F →L[𝕜] G) (f : α → F) (l : filter α) :
+  is_O_with ∥g∥ (λ x', g (f x')) f l :=
+(g.is_O_with_id ⊤).comp_tendsto le_top
+
+theorem is_O_comp {α : Type*} (g : F →L[𝕜] G) (f : α → F) (l : filter α) :
+  is_O (λ x', g (f x')) f l :=
+(g.is_O_with_comp f l).is_O
+
+theorem is_O_with_sub (f : E →L[𝕜] F) (l : filter E) (x : E) :
+  is_O_with ∥f∥ (λ x', f (x' - x)) (λ x', x' - x) l :=
+f.is_O_with_comp _ l
+
+theorem is_O_sub (f : E →L[𝕜] F) (l : filter E) (x : E) :
+  is_O (λ x', f (x' - x)) (λ x', x' - x) l :=
+f.is_O_comp _ l
+
+end is_O
+
 end continuous_linear_map
 
 namespace linear_isometry
@@ -716,7 +738,7 @@ namespace continuous_linear_equiv
 
 variables (e : E ≃L[𝕜] F)
 
-protected lemma lipschitz : lipschitz_with (nnnorm (e : E →L[𝕜] F)) e :=
+protected lemma lipschitz : lipschitz_with (∥(e : E →L[𝕜] F)∥₊) e :=
 (e : E →L[𝕜] F).lipschitz
 
 theorem is_O_comp {α : Type*} (f : α → E) (l : filter α) :