feat(analysis): x^y is smooth as a function of (x, y) (#8262)

src/analysis/calculus/extend_deriv.lean

@@ -200,3 +200,15 @@ begin
     exact (f_diff y (ne_of_lt hy)).deriv.symm },
   simpa using B.union A
 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 the derivative of `f` everywhere. -/
+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) (y : ℝ) :
+  has_deriv_at f (g y) y :=
+begin
+  rcases eq_or_ne y x with rfl|hne,
+  { exact has_deriv_at_of_has_deriv_at_of_ne f_diff hf hg },
+  { exact f_diff y hne }
+end

src/analysis/convex/specific_functions.lean

@@ -101,9 +101,8 @@ lemma convex_on_rpow {p : ℝ} (hp : 1 ≤ p) : convex_on (Ici 0) (λ x : ℝ, x
 begin
   have A : deriv (λ (x : ℝ), x ^ p) = λ x, p * x^(p-1), by { ext x, simp [hp] },
   apply convex_on_of_deriv2_nonneg (convex_Ici 0),
-  { apply (continuous_rpow_of_pos (λ _, lt_of_lt_of_le zero_lt_one hp)
-      continuous_id continuous_const).continuous_on },
-  { apply differentiable.differentiable_on, simp [hp] },
+  { exact continuous_on_id.rpow_const (λ x _, or.inr (zero_le_one.trans hp)) },
+  { exact (differentiable_rpow_const hp).differentiable_on },
   { rw A,
     assume x hx,
     replace hx : x ≠ 0, by { simp at hx, exact ne_of_gt hx },