chore(analysis/calculus/mean_value): use nnnorm in a few lemmas (#8348)

Use `nnnorm` instead of `norm` and `C : nnreal` in lemmas about `lipschitz_on_with`. This way we can use them to prove any statement of the form `lipschitz_on_with C f s`, not only something of the form `lipschitz_on_with (real.to_nnreal C) f s`.

Author: urkud

src/analysis/calculus/mean_value.lean

@@ -515,14 +515,31 @@ end
 /-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C` on
 `s`, then the function is `C`-Lipschitz on `s`. Version with `has_fderiv_within` and
 `lipschitz_on_with`. -/
-theorem convex.lipschitz_on_with_of_norm_has_fderiv_within_le
-  (hf : ∀ x ∈ s, has_fderiv_within_at f (f' x) s x) (bound : ∀x∈s, ∥f' x∥ ≤ C)
-  (hs : convex s) : lipschitz_on_with (real.to_nnreal C) f s :=
+theorem convex.lipschitz_on_with_of_nnnorm_has_fderiv_within_le {C : ℝ≥0}
+  (hf : ∀ x ∈ s, has_fderiv_within_at f (f' x) s x) (bound : ∀x∈s, ∥f' x∥₊ ≤ C)
+  (hs : convex s) : lipschitz_on_with C f s :=
 begin
   rw lipschitz_on_with_iff_norm_sub_le,
   intros x x_in y y_in,
-  convert hs.norm_image_sub_le_of_norm_has_fderiv_within_le hf bound y_in x_in,
-  exact real.coe_to_nnreal C ((norm_nonneg $ f' x).trans $ bound x x_in)
+  exact hs.norm_image_sub_le_of_norm_has_fderiv_within_le hf bound y_in x_in
+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
+  (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 :=
+begin
+  obtain ⟨ε, ε0, hε⟩ :
+    ∃ ε > 0, ball x ε ∩ s ⊆ {y | has_fderiv_within_at f (f' y) s y ∧ ∥f' y∥₊ < K},
+    from mem_nhds_within_iff.1 (hder.and $ hcont.nnnorm.eventually (gt_mem_nhds hK)),
+  rw inter_comm at hε,
+  refine ⟨s ∩ ball x ε, inter_mem_nhds_within _ (ball_mem_nhds _ ε0), _⟩,
+  exact (hs.inter (convex_ball _ _)).lipschitz_on_with_of_nnnorm_has_fderiv_within_le
+    (λ y hy, (hε hy).1.mono (inter_subset_left _ _)) (λ y hy, (hε hy).2.le)
 end
 
 /-- The mean value theorem on a convex set: if the derivative of a function within this set is
@@ -536,10 +553,10 @@ bound xs ys
 /-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C` on
 `s`, then the function is `C`-Lipschitz on `s`. Version with `fderiv_within` and
 `lipschitz_on_with`. -/
-theorem convex.lipschitz_on_with_of_norm_fderiv_within_le
-  (hf : differentiable_on 𝕜 f s) (bound : ∀x∈s, ∥fderiv_within 𝕜 f s x∥ ≤ C)
-  (hs : convex s) : lipschitz_on_with (real.to_nnreal C) f s:=
-hs.lipschitz_on_with_of_norm_has_fderiv_within_le (λ x hx, (hf x hx).has_fderiv_within_at) bound
+theorem convex.lipschitz_on_with_of_nnnorm_fderiv_within_le {C : ℝ≥0}
+  (hf : differentiable_on 𝕜 f s) (bound : ∀ x ∈ s, ∥fderiv_within 𝕜 f s x∥₊ ≤ C)
+  (hs : convex s) : lipschitz_on_with C f s:=
+hs.lipschitz_on_with_of_nnnorm_has_fderiv_within_le (λ x hx, (hf x hx).has_fderiv_within_at) bound
 
 /-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C`,
 then the function is `C`-Lipschitz. Version with `fderiv`. -/
@@ -551,10 +568,10 @@ hs.norm_image_sub_le_of_norm_has_fderiv_within_le
 
 /-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C` on
 `s`, then the function is `C`-Lipschitz on `s`. Version with `fderiv` and `lipschitz_on_with`. -/
-theorem convex.lipschitz_on_with_of_norm_fderiv_le
-  (hf : ∀ x ∈ s, differentiable_at 𝕜 f x) (bound : ∀x∈s, ∥fderiv 𝕜 f x∥ ≤ C)
-  (hs : convex s) : lipschitz_on_with (real.to_nnreal C) f s :=
-hs.lipschitz_on_with_of_norm_has_fderiv_within_le
+theorem convex.lipschitz_on_with_of_nnnorm_fderiv_le {C : ℝ≥0}
+  (hf : ∀ x ∈ s, differentiable_at 𝕜 f x) (bound : ∀x∈s, ∥fderiv 𝕜 f x∥₊ ≤ C)
+  (hs : convex s) : lipschitz_on_with C f s :=
+hs.lipschitz_on_with_of_nnnorm_has_fderiv_within_le
 (λ x hx, (hf x hx).has_fderiv_at.has_fderiv_within_at) bound
 
 /-- Variant of the mean value inequality on a convex set, using a bound on the difference between
@@ -620,11 +637,11 @@ convex.norm_image_sub_le_of_norm_has_fderiv_within_le (λ x hx, (hf x hx).has_fd
 /-- The mean value theorem on a convex set in dimension 1: if the derivative of a function is
 bounded by `C` on `s`, then the function is `C`-Lipschitz on `s`.
 Version with `has_deriv_within` and `lipschitz_on_with`. -/
-theorem convex.lipschitz_on_with_of_norm_has_deriv_within_le
-  {f f' : ℝ → F} {C : ℝ} {s : set ℝ} (hs : convex s)
-  (hf : ∀ x ∈ s, has_deriv_within_at f (f' x) s x) (bound : ∀x∈s, ∥f' x∥ ≤ C) :
-  lipschitz_on_with (real.to_nnreal C) f s :=
-convex.lipschitz_on_with_of_norm_has_fderiv_within_le (λ x hx, (hf x hx).has_fderiv_within_at)
+theorem convex.lipschitz_on_with_of_nnnorm_has_deriv_within_le
+  {f f' : ℝ → F} {C : ℝ≥0} {s : set ℝ} (hs : convex s)
+  (hf : ∀ x ∈ s, has_deriv_within_at f (f' x) s x) (bound : ∀x∈s, ∥f' x∥₊ ≤ C) :
+  lipschitz_on_with C f s :=
+convex.lipschitz_on_with_of_nnnorm_has_fderiv_within_le (λ x hx, (hf x hx).has_fderiv_within_at)
 (λ x hx, le_trans (by simp) (bound x hx)) hs
 
 /-- The mean value theorem on a convex set in dimension 1: if the derivative of a function within
@@ -639,11 +656,11 @@ bound xs ys
 /-- The mean value theorem on a convex set in dimension 1: if the derivative of a function is
 bounded by `C` on `s`, then the function is `C`-Lipschitz on `s`.
 Version with `deriv_within` and `lipschitz_on_with`. -/
-theorem convex.lipschitz_on_with_of_norm_deriv_within_le
-  {f : ℝ → F} {C : ℝ} {s : set ℝ} (hs : convex s)
-  (hf : differentiable_on ℝ f s) (bound : ∀x∈s, ∥deriv_within f s x∥ ≤ C) :
-  lipschitz_on_with (real.to_nnreal C) f s :=
-hs.lipschitz_on_with_of_norm_has_deriv_within_le (λ x hx, (hf x hx).has_deriv_within_at) bound
+theorem convex.lipschitz_on_with_of_nnnorm_deriv_within_le
+  {f : ℝ → F} {C : ℝ≥0} {s : set ℝ} (hs : convex s)
+  (hf : differentiable_on ℝ f s) (bound : ∀x∈s, ∥deriv_within f s x∥₊ ≤ C) :
+  lipschitz_on_with C f s :=
+hs.lipschitz_on_with_of_nnnorm_has_deriv_within_le (λ x hx, (hf x hx).has_deriv_within_at) bound
 
 /-- The mean value theorem on a convex set in dimension 1: if the derivative of a function is
 bounded by `C`, then the function is `C`-Lipschitz. Version with `deriv`. -/
@@ -656,10 +673,10 @@ hs.norm_image_sub_le_of_norm_has_deriv_within_le
 /-- The mean value theorem on a convex set in dimension 1: if the derivative of a function is
 bounded by `C` on `s`, then the function is `C`-Lipschitz on `s`.
 Version with `deriv` and `lipschitz_on_with`. -/
-theorem convex.lipschitz_on_with_of_norm_deriv_le {f : ℝ → F} {C : ℝ} {s : set ℝ}
-  (hf : ∀ x ∈ s, differentiable_at ℝ f x) (bound : ∀x∈s, ∥deriv f x∥ ≤ C)
-  (hs : convex s) : lipschitz_on_with (real.to_nnreal C) f s :=
-hs.lipschitz_on_with_of_norm_has_deriv_within_le
+theorem convex.lipschitz_on_with_of_nnnorm_deriv_le {f : ℝ → F} {C : ℝ≥0} {s : set ℝ}
+  (hf : ∀ x ∈ s, differentiable_at ℝ f x) (bound : ∀x∈s, ∥deriv f x∥₊ ≤ C)
+  (hs : convex s) : lipschitz_on_with C f s :=
+hs.lipschitz_on_with_of_nnnorm_has_deriv_within_le
 (λ x hx, (hf x hx).has_deriv_at.has_deriv_within_at) bound
 
 /-! ### Functions `[a, b] → ℝ`. -/

src/analysis/calculus/parametric_integral.lean

@@ -196,11 +196,10 @@ begin
   have : ∀ᵐ a ∂μ, lipschitz_on_with (real.nnabs (bound a)) (λ x, F x a) (ball x₀ ε),
   { apply (h_diff.and h_bound).mono,
     rintros a ⟨ha_deriv, ha_bound⟩,
-    have bound_nonneg : 0 ≤ bound a := (norm_nonneg (F' x₀ a)).trans (ha_bound x₀ x₀_in),
-    rw show real.nnabs (bound a) = real.to_nnreal (bound a), by simp [bound_nonneg],
-    apply convex.lipschitz_on_with_of_norm_has_fderiv_within_le _ ha_bound (convex_ball _ _),
-    intros x x_in,
-    exact (ha_deriv x x_in).has_fderiv_within_at, },
+    refine (convex_ball _ _).lipschitz_on_with_of_nnnorm_has_fderiv_within_le
+      (λ x x_in, (ha_deriv x x_in).has_fderiv_within_at) (λ x x_in, _),
+    rw [← nnreal.coe_le_coe, coe_nnnorm, nnreal.coe_nnabs],
+    exact (ha_bound x x_in).trans (le_abs_self _) },
   exact (has_fderiv_at_of_dominated_loc_of_lip ε_pos hF_meas hF_int
                                                hF'_meas this bound_integrable diff_x₀).2
 end
@@ -254,10 +253,10 @@ begin
   have : ∀ᵐ a ∂μ, lipschitz_on_with (real.nnabs (bound a)) (λ (x : ℝ), F x a) (ball x₀ ε),
   { apply (h_diff.and h_bound).mono,
     rintros a ⟨ha_deriv, ha_bound⟩,
-    have bound_nonneg : 0 ≤ bound a := (norm_nonneg (F' x₀ a)).trans (ha_bound x₀ x₀_in),
-    rw show real.nnabs (bound a) = real.to_nnreal (bound a), by simp [bound_nonneg],
-    apply convex.lipschitz_on_with_of_norm_has_deriv_within_le (convex_ball _ _)
-    (λ x x_in, (ha_deriv x x_in).has_deriv_within_at) ha_bound },
+    refine (convex_ball _ _).lipschitz_on_with_of_nnnorm_has_deriv_within_le
+      (λ x x_in, (ha_deriv x x_in).has_deriv_within_at) (λ x x_in, _),
+    rw [← nnreal.coe_le_coe, coe_nnnorm, nnreal.coe_nnabs],
+    exact (ha_bound x x_in).trans (le_abs_self _) },
   exact has_deriv_at_of_dominated_loc_of_lip ε_pos hF_meas hF_int hF'_meas this
         bound_integrable diff_x₀
 end

src/analysis/normed_space/operator_norm.lean

@@ -1195,6 +1195,12 @@ begin
       ... ≤ ∥smul_right c f∥ * ∥x∥ : le_op_norm _ _ } },
 end
 
+/-- The non-negative norm of the tensor product of a scalar linear map and of an element of a normed
+space is the product of the non-negative norms. -/
+@[simp] lemma nnnorm_smul_right_apply (c : E →L[𝕜] 𝕜) (f : F) :
+  ∥smul_right c f∥₊ = ∥c∥₊ * ∥f∥₊ :=
+nnreal.eq $ c.norm_smul_right_apply f
+
 variables (𝕜 E F)
 
 /-- `continuous_linear_map.smul_right` as a continuous trilinear map:

src/data/real/nnreal.lean

@@ -785,11 +785,7 @@ lemma real.nnabs_of_nonneg {x : ℝ} (h : 0 ≤ x) : real.nnabs x = real.to_nnre
 by { ext, simp [real.coe_to_nnreal x h, abs_of_nonneg h] }
 
 lemma real.coe_to_nnreal_le (x : ℝ) : (real.to_nnreal x : ℝ) ≤ abs x :=
-begin
-  by_cases h : 0 ≤ x,
-  { simp [h, real.coe_to_nnreal x h, le_abs_self] },
-  { simp [real.to_nnreal, h, le_abs_self, abs_nonneg] }
-end
+max_le (le_abs_self _) (abs_nonneg _)
 
 lemma cast_nat_abs_eq_nnabs_cast (n : ℤ) :
   (n.nat_abs : ℝ≥0) = real.nnabs n :=