feat(analysis/special_function/integrals): integral of x ^ r, r : ℝ, and x ^ n, n : ℤ (#10650)

Also generalize `has_deriv_at.div_const` etc.

Author: urkud

src/analysis/calculus/deriv.lean

@@ -1486,7 +1486,8 @@ end inverse
 section division
 /-! ### Derivative of `x ↦ c x / d x` -/
 
-variables {c d : 𝕜 → 𝕜} {c' d' : 𝕜}
+variables {𝕜' : Type*} [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
+  {c d : 𝕜 → 𝕜'} {c' d' : 𝕜'}
 
 lemma has_deriv_within_at.div
   (hc : has_deriv_within_at c c' s x) (hd : has_deriv_within_at d d' s x) (hx : d x ≠ 0) :
@@ -1545,28 +1546,40 @@ lemma deriv_within_div
   deriv (λx, c x / d x) x = ((deriv c x) * d x - c x * (deriv d x)) / (d x)^2 :=
 ((hc.has_deriv_at).div (hd.has_deriv_at) hx).deriv
 
-lemma differentiable_within_at.div_const (hc : differentiable_within_at 𝕜 c s x) {d : 𝕜} :
+lemma has_deriv_at.div_const (hc : has_deriv_at c c' x) (d : 𝕜') :
+  has_deriv_at (λ x, c x / d) (c' / d) x :=
+by simpa only [div_eq_mul_inv] using hc.mul_const d⁻¹
+
+lemma has_deriv_within_at.div_const (hc : has_deriv_within_at c c' s x) (d : 𝕜') :
+  has_deriv_within_at (λ x, c x / d) (c' / d) s x :=
+by simpa only [div_eq_mul_inv] using hc.mul_const d⁻¹
+
+lemma has_strict_deriv_at.div_const (hc : has_strict_deriv_at c c' x) (d : 𝕜') :
+  has_strict_deriv_at (λ x, c x / d) (c' / d) x :=
+by simpa only [div_eq_mul_inv] using hc.mul_const d⁻¹
+
+lemma differentiable_within_at.div_const (hc : differentiable_within_at 𝕜 c s x) {d : 𝕜'} :
   differentiable_within_at 𝕜 (λx, c x / d) s x :=
-by simp [div_eq_inv_mul, differentiable_within_at.const_mul, hc]
+(hc.has_deriv_within_at.div_const _).differentiable_within_at
 
-@[simp] lemma differentiable_at.div_const (hc : differentiable_at 𝕜 c x) {d : 𝕜} :
+@[simp] lemma differentiable_at.div_const (hc : differentiable_at 𝕜 c x) {d : 𝕜'} :
   differentiable_at 𝕜 (λ x, c x / d) x :=
-by simpa only [div_eq_mul_inv] using (hc.has_deriv_at.mul_const d⁻¹).differentiable_at
+(hc.has_deriv_at.div_const _).differentiable_at
 
-lemma differentiable_on.div_const (hc : differentiable_on 𝕜 c s) {d : 𝕜} :
+lemma differentiable_on.div_const (hc : differentiable_on 𝕜 c s) {d : 𝕜'} :
   differentiable_on 𝕜 (λx, c x / d) s :=
-by simp [div_eq_inv_mul, differentiable_on.const_mul, hc]
+λ x hx, (hc x hx).div_const
 
-@[simp] lemma differentiable.div_const (hc : differentiable 𝕜 c) {d : 𝕜} :
+@[simp] lemma differentiable.div_const (hc : differentiable 𝕜 c) {d : 𝕜'} :
   differentiable 𝕜 (λx, c x / d) :=
-by simp [div_eq_inv_mul, differentiable.const_mul, hc]
+λ x, (hc x).div_const
 
-lemma deriv_within_div_const (hc : differentiable_within_at 𝕜 c s x) {d : 𝕜}
+lemma deriv_within_div_const (hc : differentiable_within_at 𝕜 c s x) {d : 𝕜'}
   (hxs : unique_diff_within_at 𝕜 s x) :
   deriv_within (λx, c x / d) s x = (deriv_within c s x) / d :=
 by simp [div_eq_inv_mul, deriv_within_const_mul, hc, hxs]
 
-@[simp] lemma deriv_div_const (d : 𝕜) :
+@[simp] lemma deriv_div_const (d : 𝕜') :
   deriv (λx, c x / d) x = (deriv c x) / d :=
 by simp only [div_eq_mul_inv, deriv_mul_const_field]
 

src/analysis/special_functions/integrals.lean

@@ -44,6 +44,14 @@ variables {f : ℝ → ℝ} {μ ν : measure ℝ} [is_locally_finite_measure μ]
 lemma interval_integrable_pow : interval_integrable (λ x, x^n) μ a b :=
 (continuous_pow n).interval_integrable a b
 
+lemma interval_integrable_zpow {n : ℤ} (h : 0 ≤ n ∨ (0 : ℝ) ∉ [a, b]) :
+  interval_integrable (λ x, x ^ n) μ a b :=
+(continuous_on_id.zpow n $ λ x hx, h.symm.imp (ne_of_mem_of_not_mem hx) id).interval_integrable
+
+lemma interval_integrable_rpow {r : ℝ} (h : 0 ≤ r ∨ (0 : ℝ) ∉ [a, b]) :
+  interval_integrable (λ x, x ^ r) μ a b :=
+(continuous_on_id.rpow_const $ λ x hx, h.symm.imp (ne_of_mem_of_not_mem hx) id).interval_integrable
+
 @[simp]
 lemma interval_integrable_id : interval_integrable (λ x, x) μ a b :=
 continuous_id.interval_integrable a b
@@ -164,17 +172,33 @@ open interval_integral
 
 /-! ### Integrals of simple functions -/
 
-@[simp]
-lemma integral_pow : ∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1) :=
+lemma integral_rpow {r : ℝ} (h : 0 ≤ r ∨ r ≠ -1 ∧ (0 : ℝ) ∉ [a, b]) :
+  ∫ x in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) :=
 begin
-  have hderiv : deriv (λ x : ℝ, x ^ (n + 1) / (n + 1)) = λ x, x ^ n,
-  { ext,
-    have hne : (n + 1 : ℝ) ≠ 0 := by exact_mod_cast succ_ne_zero n,
-    simp [mul_div_assoc, mul_div_cancel' _ hne] },
-  rw integral_deriv_eq_sub' _ hderiv;
-  norm_num [div_sub_div_same, continuous_on_pow],
+  suffices : ∀ x ∈ [a, b], has_deriv_at (λ x : ℝ, x ^ (r + 1) / (r + 1)) (x ^ r) x,
+  { rw sub_div,
+    exact integral_eq_sub_of_has_deriv_at this (interval_integrable_rpow (h.imp_right and.right)) },
+  intros x hx,
+  have hx' : x ≠ 0 ∨ 1 ≤ r + 1,
+    from h.symm.imp (λ h, ne_of_mem_of_not_mem hx h.2) (le_add_iff_nonneg_left _).2,
+  convert (real.has_deriv_at_rpow_const hx').div_const (r + 1),
+  rw [add_sub_cancel, mul_div_cancel_left],
+  rw [ne.def, ← eq_neg_iff_add_eq_zero],
+  rintro rfl,
+  apply (@zero_lt_one ℝ _ _).not_le,
+  simpa using h
 end
 
+lemma integral_zpow {n : ℤ} (h : 0 ≤ n ∨ n ≠ -1 ∧ (0 : ℝ) ∉ [a, b]) :
+  ∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1) :=
+begin
+  replace h : 0 ≤ (n : ℝ) ∨ (n : ℝ) ≠ -1 ∧ (0 : ℝ) ∉ [a, b], by exact_mod_cast h,
+  exact_mod_cast integral_rpow h
+end
+
+@[simp] lemma integral_pow : ∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1) :=
+by simpa using integral_zpow (or.inl (int.coe_nat_nonneg n))
+
 /-- Integral of `|x - a| ^ n` over `Ι a b`. This integral appears in the proof of the
 Picard-Lindelöf/Cauchy-Lipschitz theorem. -/
 lemma integral_pow_abs_sub_interval_oc :

src/analysis/special_functions/pow.lean

@@ -470,11 +470,11 @@ by simpa using rpow_add_nat hx y 1
 lemma rpow_sub_one {x : ℝ} (hx : x ≠ 0) (y : ℝ) : x ^ (y - 1) = x ^ y / x :=
 by simpa using rpow_sub_nat hx y 1
 
-@[simp] lemma rpow_int_cast (x : ℝ) (n : ℤ) : x ^ (n : ℝ) = x ^ n :=
+@[simp, norm_cast] lemma rpow_int_cast (x : ℝ) (n : ℤ) : x ^ (n : ℝ) = x ^ n :=
 by simp only [rpow_def, ← complex.of_real_zpow, complex.cpow_int_cast,
   complex.of_real_int_cast, complex.of_real_re]
 
-@[simp] lemma rpow_nat_cast (x : ℝ) (n : ℕ) : x ^ (n : ℝ) = x ^ n :=
+@[simp, norm_cast] lemma rpow_nat_cast (x : ℝ) (n : ℕ) : x ^ (n : ℝ) = x ^ n :=
 rpow_int_cast x n
 
 lemma rpow_neg_one (x : ℝ) : x ^ (-1 : ℝ) = x⁻¹ :=