feat(analysis/special_functions/integrals): integral_log (#7732)

The integral of the (real) logarithmic function over the interval `[a, b]`, provided that `0 ∉ interval a b`.

Author: benjamindavidson

src/analysis/special_functions/integrals.lean

@@ -9,7 +9,7 @@ import measure_theory.interval_integral
 # Integration of specific interval integrals
 
 This file contains proofs of the integrals of various specific functions. This includes:
-* Integrals of simple functions, such as `id`, `pow`, `exp`, `inv`
+* Integrals of simple functions, such as `id`, `pow`, `inv`, `exp`, `log`
 * Integrals of some trigonometric functions, such as `sin`, `cos`, `1 / (1 + x^2)`
 * The integral of `cos x ^ 2 - sin x ^ 2`
 * Reduction formulae for the integrals of `sin x ^ n` and `cos x ^ n` for `n ≥ 2`
@@ -195,10 +195,6 @@ by simpa using integral_pow 1
 lemma integral_one : ∫ x in a..b, (1 : ℝ) = b - a :=
 by simp only [mul_one, smul_eq_mul, integral_const]
 
-@[simp]
-lemma integral_exp : ∫ x in a..b, exp x = exp b - exp a :=
-by rw integral_deriv_eq_sub'; norm_num [continuous_on_exp]
-
 @[simp]
 lemma integral_inv (h : (0:ℝ) ∉ interval a b) : ∫ x in a..b, x⁻¹ = log (b / a) :=
 begin
@@ -225,6 +221,30 @@ by simp only [one_div, integral_inv_of_pos ha hb]
 lemma integral_one_div_of_neg (ha : a < 0) (hb : b < 0) : ∫ x : ℝ in a..b, 1/x = log (b / a) :=
 by simp only [one_div, integral_inv_of_neg ha hb]
 
+@[simp]
+lemma integral_exp : ∫ x in a..b, exp x = exp b - exp a :=
+by rw integral_deriv_eq_sub'; norm_num [continuous_on_exp]
+
+@[simp]
+lemma integral_log (h : (0:ℝ) ∉ interval a b) :
+  ∫ x in a..b, log x = b * log b - a * log a - b + a :=
+begin
+  obtain ⟨h', heq⟩ := ⟨λ x hx, ne_of_mem_of_not_mem hx h, λ x hx, mul_inv_cancel (h' x hx)⟩,
+  convert integral_mul_deriv_eq_deriv_mul (λ x hx, has_deriv_at_log (h' x hx))
+    (λ x hx, has_deriv_at_id x) (continuous_on_inv'.mono $ subset_compl_singleton_iff.mpr h)
+      continuous_on_const using 1; simp [integral_congr heq, mul_comm, ← sub_add],
+end
+
+@[simp]
+lemma integral_log_of_pos (ha : 0 < a) (hb : 0 < b) :
+  ∫ x in a..b, log x = b * log b - a * log a - b + a :=
+integral_log $ not_mem_interval_of_lt ha hb
+
+@[simp]
+lemma integral_log_of_neg (ha : a < 0) (hb : b < 0) :
+  ∫ x in a..b, log x = b * log b - a * log a - b + a :=
+integral_log $ not_mem_interval_of_gt ha hb
+
 @[simp]
 lemma integral_sin : ∫ x in a..b, sin x = cos a - cos b :=
 by rw integral_deriv_eq_sub' (λ x, -cos x); norm_num [continuous_on_sin]

test/integration.lean

@@ -37,6 +37,9 @@ example : ∫ x in 0..π, cos x ^ 2 - sin x ^ 2 = 0 := by simp [integral_cos_sq_
 /- the exponential function -/
 example : ∫ x in 0..2, -exp x = 1 - exp 2 := by simp
 
+/- the logarithmic function -/
+example : ∫ x in 1..2, log x = 2 * log 2 - 1 := by { norm_num, ring }
+
 /- linear combinations (e.g. polynomials) -/
 example : ∫ x : ℝ in 0..2, 6*x^5 + 3*x^4 + x^3 - 2*x^2 + x - 7 = 1048 / 15 := by norm_num
 example : ∫ x : ℝ in 0..1, exp x + 9 * x^8 + x^3 - x/2 + (1 + x^2)⁻¹ = exp 1 + π / 4 := by norm_num