feat(analysis/calculus/deriv): prove deriv_inv at x = 0 as well (#8748)

* turn `differentiable_at_inv` and `differentiable_at_fpow` into `iff` lemmas;
* slightly weaker assumptions for `differentiable_within_at_fpow` etc;
* prove `deriv_inv` and `fderiv_inv` for all `x`;
* prove formulas for iterated derivs of `x⁻¹` and `x ^ m`, `m : int`;
* push `coe` in these formulas;

Author: urkud

src/algebra/big_operators/ring.lean

@@ -191,6 +191,22 @@ lemma prod_nat_cast (s : finset α) (f : α → ℕ) :
 
 end comm_semiring
 
+section comm_ring
+
+variables {R : Type*} [comm_ring R]
+
+lemma prod_range_cast_nat_sub (n k : ℕ) :
+  ∏ i in range k, (n - i : R) = (∏ i in range k, (n - i) : ℕ) :=
+begin
+  rw prod_nat_cast,
+  cases le_or_lt k n with hkn hnk,
+  { exact prod_congr rfl (λ i hi, (nat.cast_sub $ (mem_range.1 hi).le.trans hkn).symm) },
+  { rw ← mem_range at hnk,
+    rw [prod_eq_zero hnk, prod_eq_zero hnk]; simp }
+end
+
+end comm_ring
+
 /-- A product over all subsets of `s ∪ {x}` is obtained by multiplying the product over all subsets
 of `s`, and over all subsets of `s` to which one adds `x`. -/
 @[to_additive]

src/analysis/calculus/deriv.lean

@@ -1365,26 +1365,32 @@ theorem has_deriv_within_at_inv (x_ne_zero : x ≠ 0) (s : set 𝕜) :
   has_deriv_within_at (λx, x⁻¹) (-(x^2)⁻¹) s x :=
 (has_deriv_at_inv x_ne_zero).has_deriv_within_at
 
-lemma differentiable_at_inv (x_ne_zero : x ≠ 0) :
-  differentiable_at 𝕜 (λx, x⁻¹) x :=
-(has_deriv_at_inv x_ne_zero).differentiable_at
+lemma differentiable_at_inv :
+  differentiable_at 𝕜 (λx, x⁻¹) x ↔ x ≠ 0:=
+⟨λ H, normed_field.continuous_at_inv.1 H.continuous_at,
+  λ H, (has_deriv_at_inv H).differentiable_at⟩
 
 lemma differentiable_within_at_inv (x_ne_zero : x ≠ 0) :
   differentiable_within_at 𝕜 (λx, x⁻¹) s x :=
-(differentiable_at_inv x_ne_zero).differentiable_within_at
+(differentiable_at_inv.2 x_ne_zero).differentiable_within_at
 
 lemma differentiable_on_inv : differentiable_on 𝕜 (λx:𝕜, x⁻¹) {x | x ≠ 0} :=
 λx hx, differentiable_within_at_inv hx
 
-lemma deriv_inv (x_ne_zero : x ≠ 0) :
-  deriv (λx, x⁻¹) x = -(x^2)⁻¹ :=
-(has_deriv_at_inv x_ne_zero).deriv
+lemma deriv_inv : deriv (λx, x⁻¹) x = -(x^2)⁻¹ :=
+begin
+  rcases eq_or_ne x 0 with rfl|hne,
+  { simp [deriv_zero_of_not_differentiable_at (mt differentiable_at_inv.1 (not_not.2 rfl))] },
+  { exact (has_deriv_at_inv hne).deriv  }
+end
+
+@[simp] lemma deriv_inv' : deriv (λ x : 𝕜, x⁻¹) = λ x, -(x ^ 2)⁻¹ := funext (λ x, deriv_inv)
 
 lemma deriv_within_inv (x_ne_zero : x ≠ 0) (hxs : unique_diff_within_at 𝕜 s x) :
   deriv_within (λx, x⁻¹) s x = -(x^2)⁻¹ :=
 begin
-  rw differentiable_at.deriv_within (differentiable_at_inv x_ne_zero) hxs,
-  exact deriv_inv x_ne_zero
+  rw differentiable_at.deriv_within (differentiable_at_inv.2 x_ne_zero) hxs,
+  exact deriv_inv
 end
 
 lemma has_fderiv_at_inv (x_ne_zero : x ≠ 0) :
@@ -1395,15 +1401,15 @@ lemma has_fderiv_within_at_inv (x_ne_zero : x ≠ 0) :
   has_fderiv_within_at (λx, x⁻¹) (smul_right (1 : 𝕜 →L[𝕜] 𝕜) (-(x^2)⁻¹) : 𝕜 →L[𝕜] 𝕜) s x :=
 (has_fderiv_at_inv x_ne_zero).has_fderiv_within_at
 
-lemma fderiv_inv (x_ne_zero : x ≠ 0) :
+lemma fderiv_inv :
   fderiv 𝕜 (λx, x⁻¹) x = smul_right (1 : 𝕜 →L[𝕜] 𝕜) (-(x^2)⁻¹) :=
-(has_fderiv_at_inv x_ne_zero).fderiv
+by rw [← deriv_fderiv, deriv_inv]
 
 lemma fderiv_within_inv (x_ne_zero : x ≠ 0) (hxs : unique_diff_within_at 𝕜 s x) :
   fderiv_within 𝕜 (λx, x⁻¹) s x = smul_right (1 : 𝕜 →L[𝕜] 𝕜) (-(x^2)⁻¹) :=
 begin
-  rw differentiable_at.fderiv_within (differentiable_at_inv x_ne_zero) hxs,
-  exact fderiv_inv x_ne_zero
+  rw differentiable_at.fderiv_within (differentiable_at_inv.2 x_ne_zero) hxs,
+  exact fderiv_inv
 end
 
 variables {c : 𝕜 → 𝕜} {c' : 𝕜}
@@ -1444,7 +1450,7 @@ lemma deriv_within_inv' (hc : differentiable_within_at 𝕜 c s x) (hx : c x ≠
   deriv_within (λx, (c x)⁻¹) s x = - (deriv_within c s x) / (c x)^2 :=
 (hc.has_deriv_within_at.inv hx).deriv_within hxs
 
-@[simp] lemma deriv_inv' (hc : differentiable_at 𝕜 c x) (hx : c x ≠ 0) :
+@[simp] lemma deriv_inv'' (hc : differentiable_at 𝕜 c x) (hx : c x ≠ 0) :
   deriv (λx, (c x)⁻¹) x = - (deriv c x) / (c x)^2 :=
 (hc.has_deriv_at.inv hx).deriv
 
@@ -1732,21 +1738,6 @@ lemma deriv_within_pow (hxs : unique_diff_within_at 𝕜 s x) :
   deriv_within (λx, x^n) s x = (n : 𝕜) * x^(n-1) :=
 (has_deriv_within_at_pow n x s).deriv_within hxs
 
-lemma iter_deriv_pow' {k : ℕ} :
-  deriv^[k] (λx:𝕜, x^n) = λ x, (∏ i in finset.range k, (n - i) : ℕ) * x^(n-k) :=
-begin
-  induction k with k ihk,
-  { simp only [one_mul, finset.prod_range_zero, function.iterate_zero_apply, nat.sub_zero,
-      nat.cast_one] },
-  { simp only [function.iterate_succ_apply', ihk, finset.prod_range_succ],
-    ext x,
-    rw [((has_deriv_at_pow (n - k) x).const_mul _).deriv, nat.cast_mul, mul_assoc, nat.sub_sub] }
-end
-
-lemma iter_deriv_pow {k : ℕ} :
-  deriv^[k] (λx:𝕜, x^n) x = (∏ i in finset.range k, (n - i) : ℕ) * x^(n-k) :=
-congr_fun iter_deriv_pow' x
-
 lemma has_deriv_within_at.pow (hc : has_deriv_within_at c c' s x) :
   has_deriv_within_at (λ y, (c y)^n) ((n : 𝕜) * (c x)^(n-1) * c') s x :=
 (has_deriv_at_pow n (c x)).comp_has_deriv_within_at x hc
@@ -1784,10 +1775,9 @@ end pow
 
 section fpow
 /-! ### Derivative of `x ↦ x^m` for `m : ℤ` -/
-variables {x : 𝕜} {s : set 𝕜}
-variable {m : ℤ}
+variables {x : 𝕜} {s : set 𝕜} {m : ℤ}
 
-lemma has_strict_deriv_at_fpow (m : ℤ) (hx : x ≠ 0) :
+lemma has_strict_deriv_at_fpow (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) :
   has_strict_deriv_at (λx, x^m) ((m : 𝕜) * x^(m-1)) x :=
 begin
   have : ∀ m : ℤ, 0 < m → has_strict_deriv_at (λx, x^m) ((m:𝕜) * x^(m-1)) x,
@@ -1799,7 +1789,8 @@ begin
     norm_cast at hm,
     exact nat.succ_le_of_lt hm },
   rcases lt_trichotomy m 0 with hm|hm|hm,
-  { have := (has_strict_deriv_at_inv _).scomp _ (this (-m) (neg_pos.2 hm));
+  { have hx : x ≠ 0, from h.resolve_right hm.not_le,
+    have := (has_strict_deriv_at_inv _).scomp _ (this (-m) (neg_pos.2 hm));
       [skip, exact fpow_ne_zero_of_ne_zero hx _],
     simp only [(∘), fpow_neg, one_div, inv_inv', smul_eq_mul] at this,
     convert this using 1,
@@ -1809,43 +1800,80 @@ begin
   { exact this m hm }
 end
 
-lemma has_deriv_at_fpow (m : ℤ) (hx : x ≠ 0) :
+lemma has_deriv_at_fpow (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) :
   has_deriv_at (λx, x^m) ((m : 𝕜) * x^(m-1)) x :=
-(has_strict_deriv_at_fpow m hx).has_deriv_at
+(has_strict_deriv_at_fpow m x h).has_deriv_at
 
-theorem has_deriv_within_at_fpow (m : ℤ) (hx : x ≠ 0) (s : set 𝕜) :
+theorem has_deriv_within_at_fpow (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) (s : set 𝕜) :
   has_deriv_within_at (λx, x^m) ((m : 𝕜) * x^(m-1)) s x :=
-(has_deriv_at_fpow m hx).has_deriv_within_at
+(has_deriv_at_fpow m x h).has_deriv_within_at
 
-lemma differentiable_at_fpow (hx : x ≠ 0)  : differentiable_at 𝕜 (λx, x^m) x :=
-(has_deriv_at_fpow m hx).differentiable_at
+lemma differentiable_at_fpow : differentiable_at 𝕜 (λx, x^m) x ↔ x ≠ 0 ∨ 0 ≤ m :=
+⟨λ H, normed_field.continuous_at_fpow.1 H.continuous_at,
+  λ H, (has_deriv_at_fpow m x H).differentiable_at⟩
 
-lemma differentiable_within_at_fpow (hx : x ≠ 0) :
+lemma differentiable_within_at_fpow (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) :
   differentiable_within_at 𝕜 (λx, x^m) s x :=
-(differentiable_at_fpow hx).differentiable_within_at
+(differentiable_at_fpow.mpr h).differentiable_within_at
+
+lemma differentiable_on_fpow (m : ℤ) (s : set 𝕜) (h : (0 : 𝕜) ∉ s ∨ 0 ≤ m) :
+  differentiable_on 𝕜 (λx, x^m) s :=
+λ x hxs, differentiable_within_at_fpow m x $ h.imp_left $ ne_of_mem_of_not_mem hxs
 
-lemma differentiable_on_fpow (hs : (0:𝕜) ∉ s) : differentiable_on 𝕜 (λx, x^m) s :=
-λ x hxs, differentiable_within_at_fpow (λ hx, hs $ hx ▸ hxs)
+lemma deriv_fpow (m : ℤ) (x : 𝕜) : deriv (λ x, x ^ m) x = m * x ^ (m - 1) :=
+begin
+  by_cases H : x ≠ 0 ∨ 0 ≤ m,
+  { exact (has_deriv_at_fpow m x H).deriv },
+  { rw deriv_zero_of_not_differentiable_at (mt differentiable_at_fpow.1 H),
+    push_neg at H, rcases H with ⟨rfl, hm⟩,
+    rw [zero_fpow _ ((sub_one_lt _).trans hm).ne, mul_zero] }
+end
 
--- TODO : this is true at `x=0` as well
-lemma deriv_fpow (hx : x ≠ 0) : deriv (λx, x^m) x = (m : 𝕜) * x^(m-1) :=
-(has_deriv_at_fpow m hx).deriv
+@[simp] lemma deriv_fpow' (m : ℤ) : deriv (λ x : 𝕜, x ^ m) = λ x, m * x ^ (m - 1) :=
+funext $ deriv_fpow m
 
-lemma deriv_within_fpow (hxs : unique_diff_within_at 𝕜 s x) (hx : x ≠ 0) :
+lemma deriv_within_fpow (hxs : unique_diff_within_at 𝕜 s x) (h : x ≠ 0 ∨ 0 ≤ m) :
   deriv_within (λx, x^m) s x = (m : 𝕜) * x^(m-1) :=
-(has_deriv_within_at_fpow m hx s).deriv_within hxs
+(has_deriv_within_at_fpow m x h s).deriv_within hxs
+
+@[simp] lemma iter_deriv_fpow' (m : ℤ) (k : ℕ) :
+  deriv^[k] (λ x : 𝕜, x ^ m) = λ x, (∏ i in finset.range k, (m - i)) * x ^ (m - k) :=
+begin
+  induction k with k ihk,
+  { simp only [one_mul, int.coe_nat_zero, id, sub_zero, finset.prod_range_zero,
+      function.iterate_zero] },
+  { simp only [function.iterate_succ_apply', ihk, deriv_const_mul', deriv_fpow',
+      finset.prod_range_succ, int.coe_nat_succ, ← sub_sub, int.cast_sub, int.cast_coe_nat,
+      mul_assoc], }
+end
+
+lemma iter_deriv_fpow (m : ℤ) (x : 𝕜) (k : ℕ) :
+  deriv^[k] (λ y, y ^ m) x = (∏ i in finset.range k, (m - i)) * x ^ (m - k) :=
+congr_fun (iter_deriv_fpow' m k) x
 
-lemma iter_deriv_fpow {k : ℕ} (hx : x ≠ 0) :
-  deriv^[k] (λx:𝕜, x^m) x = (∏ i in finset.range k, (m - i) : ℤ) * x^(m-k) :=
+lemma iter_deriv_pow (n : ℕ) (x : 𝕜) (k : ℕ) :
+  deriv^[k] (λx:𝕜, x^n) x = (∏ i in finset.range k, (n - i)) * x^(n-k) :=
 begin
-  induction k with k ihk generalizing x hx,
-  { simp only [one_mul, finset.prod_range_zero, function.iterate_zero_apply, int.coe_nat_zero,
-      sub_zero, int.cast_one] },
-  { rw [function.iterate_succ', finset.prod_range_succ, int.cast_mul, mul_assoc,
-      int.coe_nat_succ, ← sub_sub, ← ((has_deriv_at_fpow _ hx).const_mul _).deriv],
-    exact filter.eventually_eq.deriv_eq (eventually.mono (is_open.mem_nhds is_open_ne hx) @ihk) }
+  simp only [← gpow_coe_nat, iter_deriv_fpow, int.cast_coe_nat],
+  cases le_or_lt k n with hkn hnk,
+  { rw int.coe_nat_sub hkn },
+  { have : ∏ i in finset.range k, (n - i : 𝕜) = 0,
+      from finset.prod_eq_zero (finset.mem_range.2 hnk) (sub_self _),
+    simp only [this, zero_mul] }
 end
 
+@[simp] lemma iter_deriv_pow' (n k : ℕ) :
+  deriv^[k] (λ x : 𝕜, x ^ n) = λ x, (∏ i in finset.range k, (n - i)) * x ^ (n - k) :=
+funext $ λ x, iter_deriv_pow n x k
+
+lemma iter_deriv_inv (k : ℕ) (x : 𝕜) :
+  deriv^[k] has_inv.inv x = (∏ i in finset.range k, (-1 - i)) * x ^ (-1 - k : ℤ) :=
+by simpa only [fpow_neg_one, int.cast_neg, int.cast_one] using iter_deriv_fpow (-1) x k
+
+@[simp] lemma iter_deriv_inv' (k : ℕ) :
+  deriv^[k] has_inv.inv = λ x : 𝕜, (∏ i in finset.range k, (-1 - i)) * x ^ (-1 - k : ℤ) :=
+funext (iter_deriv_inv k)
+
 end fpow
 
 /-! ### Upper estimates on liminf and limsup -/

src/analysis/convex/specific_functions.lean

@@ -35,19 +35,19 @@ begin
   { simp only [deriv_pow', differentiable.mul, differentiable_const, differentiable_pow] },
   { intro x,
     rcases nat.even.sub_even hn (nat.even_bit0 1) with ⟨k, hk⟩,
-    simp only [iter_deriv_pow, finset.prod_range_succ, finset.prod_range_zero, nat.sub_zero,
-      mul_one, hk, pow_mul', sq],
-    exact mul_nonneg (nat.cast_nonneg _) (mul_self_nonneg _) }
+    rw [iter_deriv_pow, finset.prod_range_cast_nat_sub, hk, pow_mul'],
+    exact mul_nonneg (nat.cast_nonneg _) (pow_two_nonneg _) }
 end
 
 /-- `x^n`, `n : ℕ` is convex on `[0, +∞)` for all `n` -/
 lemma convex_on_pow (n : ℕ) : convex_on (Ici 0) (λ x : ℝ, x^n) :=
 begin
-  apply convex_on_of_deriv2_nonneg (convex_Ici _) (continuous_pow n).continuous_on;
-    simp only [interior_Ici, differentiable_on_pow, deriv_pow',
-      differentiable_on_const, differentiable_on.mul, iter_deriv_pow],
-  intros x hx,
-  exact mul_nonneg (nat.cast_nonneg _) (pow_nonneg (le_of_lt hx) _)
+  apply convex_on_of_deriv2_nonneg (convex_Ici _) (continuous_pow n).continuous_on
+    differentiable_on_pow,
+  { simp only [deriv_pow'], exact differentiable_on_pow.const_mul _ },
+  { intros x hx,
+    rw [iter_deriv_pow, finset.prod_range_cast_nat_sub],
+    exact mul_nonneg (nat.cast_nonneg _) (pow_nonneg (interior_subset hx) _) }
 end
 
 lemma finset.prod_nonneg_of_card_nonpos_even
@@ -64,35 +64,29 @@ calc 0 ≤ (∏ x in s, ((if f x ≤ 0 then (-1:β) else 1) * f x)) :
 lemma int_prod_range_nonneg (m : ℤ) (n : ℕ) (hn : even n) :
   0 ≤ ∏ k in finset.range n, (m - k) :=
 begin
-  cases (le_or_lt ↑n m) with hnm hmn,
-  { exact finset.prod_nonneg (λ k hk, sub_nonneg.2 (le_trans
-      (int.coe_nat_le.2 $ le_of_lt $ finset.mem_range.1 hk) hnm)) },
-  cases le_or_lt 0 m with hm hm,
-  { lift m to ℕ using hm,
-    exact le_of_eq (eq.symm $ finset.prod_eq_zero
-      (finset.mem_range.2 $ int.coe_nat_lt.1 hmn) (sub_self _)) },
-  clear hmn,
-  apply finset.prod_nonneg_of_card_nonpos_even,
-  convert hn,
-  convert finset.card_range n,
-  ext k,
-  simp only [finset.mem_filter, finset.mem_range],
-  refine ⟨and.left, λ hk, ⟨hk, sub_nonpos.2 $ le_trans (le_of_lt hm) _⟩⟩,
-  exact int.coe_nat_nonneg k
+  rcases hn with ⟨n, rfl⟩,
+  induction n with n ihn, { simp },
+  rw [nat.succ_eq_add_one, mul_add, mul_one, bit0, ← add_assoc, finset.prod_range_succ,
+    finset.prod_range_succ, mul_assoc],
+  refine mul_nonneg ihn _, generalize : (1 + 1) * n = k,
+  cases le_or_lt m k with hmk hmk,
+  { have : m ≤ k + 1, from hmk.trans (lt_add_one ↑k).le,
+    exact mul_nonneg_of_nonpos_of_nonpos (sub_nonpos.2 hmk) (sub_nonpos.2 this) },
+  { exact mul_nonneg (sub_nonneg.2 hmk.le) (sub_nonneg.2 hmk) }
 end
 
 /-- `x^m`, `m : ℤ` is convex on `(0, +∞)` for all `m` -/
 lemma convex_on_fpow (m : ℤ) : convex_on (Ioi 0) (λ x : ℝ, x^m) :=
 begin
-  apply convex_on_of_deriv2_nonneg (convex_Ioi 0); try { rw [interior_Ioi] },
-  { exact (differentiable_on_fpow $ lt_irrefl _).continuous_on },
-  { exact differentiable_on_fpow (lt_irrefl _) },
-  { have : eq_on (deriv (λx:ℝ, x^m)) (λx, ↑m * x^(m-1)) (Ioi 0),
-      from λ x hx, deriv_fpow (ne_of_gt hx),
-    refine (differentiable_on_congr this).2 _,
-    exact (differentiable_on_fpow (lt_irrefl _)).const_mul _ },
+  have : ∀ n : ℤ, differentiable_on ℝ (λ x, x ^ n) (Ioi (0 : ℝ)),
+    from λ n, differentiable_on_fpow _ _ (or.inl $ lt_irrefl _),
+  apply convex_on_of_deriv2_nonneg (convex_Ioi 0);
+    try { simp only [interior_Ioi, deriv_fpow'] },
+  { exact (this _).continuous_on },
+  { exact this _ },
+  { exact (this _).const_mul _ },
   { intros x hx,
-    simp only [iter_deriv_fpow (ne_of_gt hx)],
+    simp only [iter_deriv_fpow, ← int.cast_coe_nat, ← int.cast_sub, ← int.cast_prod],
     refine mul_nonneg (int.cast_nonneg.2 _) (fpow_nonneg (le_of_lt hx) _),
     exact int_prod_range_nonneg _ _ (nat.even_bit0 1) }
 end
@@ -128,7 +122,7 @@ begin
   { intros x hx,
     rw [function.iterate_succ, function.iterate_one],
     change (deriv (deriv log)) x ≤ 0,
-    rw [deriv_log', deriv_inv (show x ≠ 0, by {rintro rfl, exact lt_irrefl 0 hx})],
+    rw [deriv_log', deriv_inv],
     exact neg_nonpos.mpr (inv_nonneg.mpr (sq_nonneg x)) }
 end
 
@@ -146,6 +140,6 @@ begin
   { intros x hx,
     rw [function.iterate_succ, function.iterate_one],
     change (deriv (deriv log)) x ≤ 0,
-    rw [deriv_log', deriv_inv (show x ≠ 0, by {rintro rfl, exact lt_irrefl 0 hx})],
+    rw [deriv_log', deriv_inv],
     exact neg_nonpos.mpr (inv_nonneg.mpr (sq_nonneg x)) }
 end