feat(analysis/special_functions/pow): rpow is differentiable (#2930)

Differentiability of the real power function `x ↦ x^p`. Also register the lemmas about the composition with a function to make sure that the simplifier can handle automatically the differentiability of `x ↦ (f x)^p` and more complicated expressions involving powers.

Author: sgouezel

src/analysis/calculus/extend_deriv.lean

@@ -165,7 +165,7 @@ end
 
 /-- If a function is differentiable on the left of a point `a : ℝ`, continuous at `a`, and
 its derivative also converges at `a`, then `f` is differentiable on the left at `a`. -/
-lemma has_fderiv_at_interval_right_endpoint_of_tendsto_deriv {s : set ℝ} {e : E} {a : ℝ} {f : ℝ → E}
+lemma has_deriv_at_interval_right_endpoint_of_tendsto_deriv {s : set ℝ} {e : E} {a : ℝ} {f : ℝ → E}
   (f_diff : differentiable_on ℝ f s) (f_lim : continuous_within_at f s a)
   (hs : s ∈ nhds_within a (Iio a))
   (f_lim' : tendsto (λx, deriv f x) (nhds_within a (Iio a)) (𝓝 e)) :
@@ -199,3 +199,35 @@ begin
     exact has_fderiv_at_boundary_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff' },
   exact this.nhds_within (mem_nhds_within_Iic_iff_exists_Icc_subset.2 ⟨b, ba, subset.refl _⟩)
 end
+
+/-- If a real function `f` has a derivative `g` everywhere but at a point, and `f` and `g` are
+continuous at this point, then `g` is also the derivative of `f` at this point. -/
+lemma has_deriv_at_of_has_deriv_at_of_ne {f g : ℝ → E} {x : ℝ}
+  (f_diff : ∀ y ≠ x, has_deriv_at f (g y) y)
+  (hf : continuous_at f x) (hg : continuous_at g x) :
+  has_deriv_at f (g x) x :=
+begin
+  have A : has_deriv_within_at f (g x) (Ici x) x,
+  { have diff : differentiable_on ℝ f (Ioi x) :=
+      λy hy, (f_diff y (ne_of_gt hy)).differentiable_at.differentiable_within_at,
+    -- next line is the nontrivial bit of this proof, appealing to differentiability
+    -- extension results.
+    apply has_deriv_at_interval_left_endpoint_of_tendsto_deriv diff hf.continuous_within_at
+      self_mem_nhds_within,
+    have : tendsto g (nhds_within x (Ioi x)) (𝓝 (g x)) := tendsto_inf_left hg,
+    apply this.congr' _,
+    apply mem_sets_of_superset self_mem_nhds_within (λy hy, _),
+    exact (f_diff y (ne_of_gt hy)).deriv.symm },
+  have B : has_deriv_within_at f (g x) (Iic x) x,
+  { have diff : differentiable_on ℝ f (Iio x) :=
+      λy hy, (f_diff y (ne_of_lt hy)).differentiable_at.differentiable_within_at,
+    -- next line is the nontrivial bit of this proof, appealing to differentiability
+    -- extension results.
+    apply has_deriv_at_interval_right_endpoint_of_tendsto_deriv diff hf.continuous_within_at
+      self_mem_nhds_within,
+    have : tendsto g (nhds_within x (Iio x)) (𝓝 (g x)) := tendsto_inf_left hg,
+    apply this.congr' _,
+    apply mem_sets_of_superset self_mem_nhds_within (λy hy, _),
+    exact (f_diff y (ne_of_lt hy)).deriv.symm },
+  simpa using B.union A
+end

src/analysis/special_functions/exp_log.lean

@@ -207,6 +207,9 @@ by { rw [log, dif_pos hx], exact classical.some_spec (exists_exp_eq_of_pos ((abs
 lemma exp_log (hx : 0 < x) : exp (log x) = x :=
 by { rw exp_log_eq_abs (ne_of_gt hx), exact abs_of_pos hx }
 
+lemma exp_log_of_neg (hx : x < 0) : exp (log x) = -x :=
+by { rw exp_log_eq_abs (ne_of_lt hx), exact abs_of_neg hx }
+
 @[simp] lemma log_exp (x : ℝ) : log (exp x) = x :=
 exp_injective $ exp_log (exp_pos x)
 

src/analysis/special_functions/pow.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Sébastien Gouëzel
 -/
 import analysis.special_functions.trigonometric
+import analysis.calculus.extend_deriv
 
 /-!
 # Power function on `ℂ`, `ℝ` and `ℝ⁺`
@@ -68,6 +69,9 @@ end
 lemma cpow_neg (x y : ℂ) : x ^ -y = (x ^ y)⁻¹ :=
 by simp [cpow_def]; split_ifs; simp [exp_neg]
 
+lemma cpow_neg_one (x : ℂ) : x ^ (-1 : ℂ) = x⁻¹ :=
+by simpa using cpow_neg x 1
+
 @[simp] lemma cpow_nat_cast (x : ℂ) : ∀ (n : ℕ), x ^ (n : ℂ) = x ^ n
 | 0       := by simp
 | (n + 1) := if hx : x = 0 then by simp only [hx, pow_succ,
@@ -217,13 +221,46 @@ by simp [rpow_def, *]
 
 @[simp] lemma one_rpow (x : ℝ) : (1 : ℝ) ^ x = 1 := by simp [rpow_def]
 
+lemma zero_rpow_le_one (x : ℝ) : (0 : ℝ) ^ x ≤ 1 :=
+by { by_cases h : x = 0; simp [h, zero_le_one] }
+
+lemma zero_rpow_nonneg (x : ℝ) : 0 ≤ (0 : ℝ) ^ x :=
+by { by_cases h : x = 0; simp [h, zero_le_one] }
+
 lemma rpow_nonneg_of_nonneg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : 0 ≤ x ^ y :=
 by rw [rpow_def_of_nonneg hx];
   split_ifs; simp only [zero_le_one, le_refl, le_of_lt (exp_pos _)]
 
-lemma rpow_add {x : ℝ} (y z : ℝ) (hx : 0 < x) : x ^ (y + z) = x ^ y * x ^ z :=
+lemma rpow_add {x : ℝ} (hx : 0 < x) (y z : ℝ) : x ^ (y + z) = x ^ y * x ^ z :=
 by simp only [rpow_def_of_pos hx, mul_add, exp_add]
 
+lemma rpow_add' {x : ℝ} (hx : 0 ≤ x) {y z : ℝ} (h : y + z ≠ 0) : x ^ (y + z) = x ^ y * x ^ z :=
+begin
+  rcases le_iff_eq_or_lt.1 hx with H|pos,
+  { simp only [← H, h, rpow_eq_zero_iff_of_nonneg, true_and, zero_rpow, eq_self_iff_true, ne.def,
+               not_false_iff, zero_eq_mul],
+    by_contradiction F,
+    push_neg at F,
+    apply h,
+    simp [F] },
+  { exact rpow_add pos _ _ }
+end
+
+/-- For `0 ≤ x`, the only problematic case in the equality `x ^ y * x ^ z = x ^ (y + z)` is for
+`x = 0` and `y + z = 0`, where the right hand side is `1` while the left hand side can vanish.
+The inequality is always true, though, and given in this lemma. -/
+lemma le_rpow_add {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) : x ^ y * x ^ z ≤ x ^ (y + z) :=
+begin
+  rcases le_iff_eq_or_lt.1 hx with H|pos,
+  { by_cases h : y + z = 0,
+    { simp only [H.symm, h, rpow_zero],
+      calc (0 : ℝ) ^ y * 0 ^ z ≤ 1 * 1 :
+        mul_le_mul (zero_rpow_le_one y) (zero_rpow_le_one z) (zero_rpow_nonneg z) zero_le_one
+      ... = 1 : by simp },
+    { simp [rpow_add', ← H, h] } },
+  { simp [rpow_add pos] }
+end
+
 lemma rpow_mul {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) : x ^ (y * z) = (x ^ y) ^ z :=
 by rw [← complex.of_real_inj, complex.of_real_cpow (rpow_nonneg_of_nonneg hx _),
     complex.of_real_cpow hx, complex.of_real_mul, complex.cpow_mul, complex.of_real_cpow hx];
@@ -241,6 +278,12 @@ by simp only [rpow_def, (complex.of_real_pow _ _).symm, complex.cpow_nat_cast,
 by simp only [rpow_def, (complex.of_real_fpow _ _).symm, complex.cpow_int_cast,
   complex.of_real_int_cast, complex.of_real_re]
 
+lemma rpow_neg_one (x : ℝ) : x ^ (-1 : ℝ) = x⁻¹ :=
+begin
+  suffices H : x ^ ((-1 : ℤ) : ℝ) = x⁻¹, by exact_mod_cast H,
+  simp only [rpow_int_cast, fpow_one, fpow_neg],
+end
+
 lemma mul_rpow {x y z : ℝ} (h : 0 ≤ x) (h₁ : 0 ≤ y) : (x*y)^z = x^z * y^z :=
 begin
   iterate 3 { rw real.rpow_def_of_nonneg }, split_ifs; simp * at *,
@@ -437,6 +480,64 @@ lemma continuous_rpow_of_pos (h : ∀a, 0 < g a) (hf : continuous f) (hg : conti
 
 end prove_rpow_is_continuous
 
+section prove_rpow_is_differentiable
+
+lemma has_deriv_at_rpow_of_pos {x : ℝ} (h : 0 < x) (p : ℝ) :
+  has_deriv_at (λ x, x^p) (p * x^(p-1)) x :=
+begin
+  have : has_deriv_at (λ x, exp (log x * p)) (p * x^(p-1)) x,
+  { convert (has_deriv_at_exp _).comp x ((has_deriv_at_log (ne_of_gt h)).mul_const p) using 1,
+    field_simp [rpow_def_of_pos h, mul_sub, exp_sub, exp_log h, ne_of_gt h],
+    ring },
+  apply this.congr_of_mem_nhds,
+  have : set.Ioi (0 : ℝ) ∈ 𝓝 x := mem_nhds_sets is_open_Ioi h,
+  exact filter.eventually_of_mem this (λ y hy, rpow_def_of_pos hy _)
+end
+
+lemma has_deriv_at_rpow_of_neg {x : ℝ} (h : x < 0) (p : ℝ) :
+  has_deriv_at (λ x, x^p) (p * x^(p-1)) x :=
+begin
+  have : has_deriv_at (λ x, exp (log x * p) * cos (p * π)) (p * x^(p-1)) x,
+  { convert ((has_deriv_at_exp _).comp x ((has_deriv_at_log (ne_of_lt h)).mul_const p)).mul_const _
+      using 1,
+    field_simp [rpow_def_of_neg h, mul_sub, exp_sub, sub_mul, cos_sub, exp_log_of_neg h, ne_of_lt h],
+    ring },
+  apply this.congr_of_mem_nhds,
+  have : set.Iio (0 : ℝ) ∈ 𝓝 x := mem_nhds_sets is_open_Iio h,
+  exact filter.eventually_of_mem this (λ y hy, rpow_def_of_neg hy _)
+end
+
+lemma has_deriv_at_rpow {x : ℝ} (h : x ≠ 0) (p : ℝ) :
+  has_deriv_at (λ x, x^p) (p * x^(p-1)) x :=
+begin
+  rcases lt_trichotomy x 0 with H|H|H,
+  { exact has_deriv_at_rpow_of_neg H p },
+  { exact (h H).elim },
+  { exact has_deriv_at_rpow_of_pos H p },
+end
+
+lemma has_deriv_at_rpow_zero_of_one_le {p : ℝ} (h : 1 ≤ p) :
+  has_deriv_at (λ x, x^p) (p * (0 : ℝ)^(p-1)) 0 :=
+begin
+  apply has_deriv_at_of_has_deriv_at_of_ne (λ x hx, has_deriv_at_rpow hx p),
+  { exact (continuous_rpow_of_pos (λ _, (lt_of_lt_of_le zero_lt_one h))
+      continuous_id continuous_const).continuous_at },
+  { rcases le_iff_eq_or_lt.1 h with rfl|h,
+    { simp [continuous_const.continuous_at] },
+    { exact (continuous_const.mul (continuous_rpow_of_pos (λ _, sub_pos_of_lt h)
+        continuous_id continuous_const)).continuous_at } }
+end
+
+lemma has_deriv_at_rpow_of_one_le (x : ℝ) {p : ℝ} (h : 1 ≤ p) :
+  has_deriv_at (λ x, x^p) (p * x^(p-1)) x :=
+begin
+  by_cases hx : x = 0,
+  { rw hx, exact has_deriv_at_rpow_zero_of_one_le h },
+  { exact has_deriv_at_rpow hx p }
+end
+
+end prove_rpow_is_differentiable
+
 section sqrt
 
 lemma sqrt_eq_rpow : sqrt = λx:ℝ, x ^ (1/(2:ℝ)) :=
@@ -456,6 +557,163 @@ end sqrt
 
 end real
 
+section differentiability
+open real
+
+variables {f : ℝ → ℝ} {x f' : ℝ} {s : set ℝ} (p : ℝ)
+/- Differentiability statements for the power of a function, when the function does not vanish
+and the exponent is arbitrary-/
+
+lemma has_deriv_within_at.rpow (hf : has_deriv_within_at f f' s x) (hx : f x ≠ 0) :
+  has_deriv_within_at (λ y, (f y)^p) (f' * p * (f x)^(p-1)) s x :=
+begin
+  convert (has_deriv_at_rpow hx p).comp_has_deriv_within_at x hf using 1,
+  ring
+end
+
+lemma has_deriv_at.rpow (hf : has_deriv_at f f' x) (hx : f x ≠ 0) :
+  has_deriv_at (λ y, (f y)^p) (f' * p * (f x)^(p-1)) x :=
+begin
+  rw ← has_deriv_within_at_univ at *,
+  exact hf.rpow p hx
+end
+
+lemma differentiable_within_at.rpow (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0) :
+  differentiable_within_at ℝ (λx, (f x)^p) s x :=
+(hf.has_deriv_within_at.rpow p hx).differentiable_within_at
+
+@[simp] lemma differentiable_at.rpow (hf : differentiable_at ℝ f x) (hx : f x ≠ 0) :
+  differentiable_at ℝ (λx, (f x)^p) x :=
+(hf.has_deriv_at.rpow p hx).differentiable_at
+
+lemma differentiable_on.rpow (hf : differentiable_on ℝ f s) (hx : ∀ x ∈ s, f x ≠ 0) :
+  differentiable_on ℝ (λx, (f x)^p) s :=
+λx h, (hf x h).rpow p (hx x h)
+
+@[simp] lemma differentiable.rpow (hf : differentiable ℝ f) (hx : ∀ x, f x ≠ 0) :
+  differentiable ℝ (λx, (f x)^p) :=
+λx, (hf x).rpow p (hx x)
+
+lemma deriv_within_rpow (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0)
+  (hxs : unique_diff_within_at ℝ s x) :
+  deriv_within (λx, (f x)^p) s x = (deriv_within f s x) * p * (f x)^(p-1) :=
+(hf.has_deriv_within_at.rpow p hx).deriv_within hxs
+
+@[simp] lemma deriv_rpow (hf : differentiable_at ℝ f x) (hx : f x ≠ 0) :
+  deriv (λx, (f x)^p) x = (deriv f x) * p * (f x)^(p-1) :=
+(hf.has_deriv_at.rpow p hx).deriv
+
+/- Differentiability statements for the power of a function, when the function may vanish
+but the exponent is at least one. -/
+
+variable {p}
+
+lemma has_deriv_within_at.rpow_of_one_le (hf : has_deriv_within_at f f' s x) (hp : 1 ≤ p) :
+  has_deriv_within_at (λ y, (f y)^p) (f' * p * (f x)^(p-1)) s x :=
+begin
+  convert (has_deriv_at_rpow_of_one_le (f x) hp).comp_has_deriv_within_at x hf using 1,
+  ring
+end
+
+lemma has_deriv_at.rpow_of_one_le (hf : has_deriv_at f f' x) (hp : 1 ≤ p) :
+  has_deriv_at (λ y, (f y)^p) (f' * p * (f x)^(p-1)) x :=
+begin
+  rw ← has_deriv_within_at_univ at *,
+  exact hf.rpow_of_one_le hp
+end
+
+lemma differentiable_within_at.rpow_of_one_le (hf : differentiable_within_at ℝ f s x) (hp : 1 ≤ p) :
+  differentiable_within_at ℝ (λx, (f x)^p) s x :=
+(hf.has_deriv_within_at.rpow_of_one_le hp).differentiable_within_at
+
+@[simp] lemma differentiable_at.rpow_of_one_le (hf : differentiable_at ℝ f x) (hp : 1 ≤ p) :
+  differentiable_at ℝ (λx, (f x)^p) x :=
+(hf.has_deriv_at.rpow_of_one_le hp).differentiable_at
+
+lemma differentiable_on.rpow_of_one_le (hf : differentiable_on ℝ f s) (hp : 1 ≤ p) :
+  differentiable_on ℝ (λx, (f x)^p) s :=
+λx h, (hf x h).rpow_of_one_le hp
+
+@[simp] lemma differentiable.rpow_of_one_le (hf : differentiable ℝ f) (hp : 1 ≤ p) :
+  differentiable ℝ (λx, (f x)^p) :=
+λx, (hf x).rpow_of_one_le hp
+
+lemma deriv_within_rpow_of_one_le (hf : differentiable_within_at ℝ f s x) (hp : 1 ≤ p)
+  (hxs : unique_diff_within_at ℝ s x) :
+  deriv_within (λx, (f x)^p) s x = (deriv_within f s x) * p * (f x)^(p-1) :=
+(hf.has_deriv_within_at.rpow_of_one_le hp).deriv_within hxs
+
+@[simp] lemma deriv_rpow_of_one_le (hf : differentiable_at ℝ f x) (hp : 1 ≤ p) :
+  deriv (λx, (f x)^p) x = (deriv f x) * p * (f x)^(p-1) :=
+(hf.has_deriv_at.rpow_of_one_le hp).deriv
+
+/- Differentiability statements for the square root of a function, when the function does not
+vanish -/
+
+lemma has_deriv_within_at.sqrt (hf : has_deriv_within_at f f' s x) (hx : f x ≠ 0) :
+  has_deriv_within_at (λ y, sqrt (f y)) (f' / (2 * sqrt (f x))) s x :=
+begin
+  simp only [sqrt_eq_rpow],
+  convert hf.rpow (1/2) hx,
+  rcases lt_trichotomy (f x) 0 with H|H|H,
+  { have A : (f x)^((1:ℝ)/2) = 0,
+    { rw rpow_def_of_neg H,
+      have : cos (1/2 * π) = 0, by { convert cos_pi_div_two using 2, ring },
+      rw [this],
+      simp },
+    have B : f x ^ ((1:ℝ) / 2 - 1) = 0,
+    { rw rpow_def_of_neg H,
+      have : cos (π/2 - π) = 0, by simp [cos_sub],
+      have : cos (((1:ℝ)/2 - 1) * π) = 0, by { convert this using 2, ring },
+      rw this,
+      simp },
+    rw [A, B],
+    simp },
+  { exact (hx H).elim },
+  { have A : 0 < (f x)^((1:ℝ)/2) := rpow_pos_of_pos H _,
+    have B : (f x) ^ (-(1:ℝ)) = (f x)^(-((1:ℝ)/2)) * (f x)^(-((1:ℝ)/2)),
+    { rw [← rpow_add H],
+      congr,
+      norm_num },
+    rw [sub_eq_add_neg, rpow_add H, B, rpow_neg (le_of_lt H)],
+    field_simp [hx, ne_of_gt A],
+    ring }
+end
+
+lemma has_deriv_at.sqrt (hf : has_deriv_at f f' x) (hx : f x ≠ 0) :
+  has_deriv_at (λ y, sqrt (f y)) (f' / (2 * sqrt(f x))) x :=
+begin
+  rw ← has_deriv_within_at_univ at *,
+  exact hf.sqrt hx
+end
+
+lemma differentiable_within_at.sqrt (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0) :
+  differentiable_within_at ℝ (λx, sqrt (f x)) s x :=
+(hf.has_deriv_within_at.sqrt hx).differentiable_within_at
+
+@[simp] lemma differentiable_at.sqrt (hf : differentiable_at ℝ f x) (hx : f x ≠ 0) :
+  differentiable_at ℝ (λx, sqrt (f x)) x :=
+(hf.has_deriv_at.sqrt hx).differentiable_at
+
+lemma differentiable_on.sqrt (hf : differentiable_on ℝ f s) (hx : ∀ x ∈ s, f x ≠ 0) :
+  differentiable_on ℝ (λx, sqrt (f x)) s :=
+λx h, (hf x h).sqrt (hx x h)
+
+@[simp] lemma differentiable.sqrt (hf : differentiable ℝ f) (hx : ∀ x, f x ≠ 0) :
+  differentiable ℝ (λx, sqrt (f x)) :=
+λx, (hf x).sqrt (hx x)
+
+lemma deriv_within_sqrt (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0)
+  (hxs : unique_diff_within_at ℝ s x) :
+  deriv_within (λx, sqrt (f x)) s x = (deriv_within f s x) / (2 * sqrt (f x)) :=
+(hf.has_deriv_within_at.sqrt hx).deriv_within hxs
+
+@[simp] lemma deriv_sqrt (hf : differentiable_at ℝ f x) (hx : f x ≠ 0) :
+  deriv (λx, sqrt (f x)) x = (deriv f x) / (2 * sqrt (f x)) :=
+(hf.has_deriv_at.sqrt hx).deriv
+
+end differentiability
+
 namespace nnreal
 
 /-- The nonnegative real power function `x^y`, defined for `x : nnreal` and `y : ℝ ` as the
@@ -489,7 +747,7 @@ by { rw ← nnreal.coe_eq, exact real.rpow_one _ }
 by { rw ← nnreal.coe_eq, exact real.one_rpow _ }
 
 lemma rpow_add {x : nnreal} (hx : 0 < x) (y z : ℝ) : x ^ (y + z) = x ^ y * x ^ z :=
-by { rw ← nnreal.coe_eq, exact real.rpow_add _ _ hx }
+by { rw ← nnreal.coe_eq, exact real.rpow_add hx _ _  }
 
 lemma rpow_mul (x : nnreal) (y z : ℝ) : x ^ (y * z) = (x ^ y) ^ z :=
 by { rw ← nnreal.coe_eq, exact real.rpow_mul x.2 y z }