55 lines
1.4 KiB
Plaintext
55 lines
1.4 KiB
Plaintext
import Mathlib.Analysis.SpecialFunctions.Integrals
|
||
|
||
theorem intervalIntegral.intervalIntegrable_log'
|
||
{a : ℝ}
|
||
{b : ℝ}
|
||
{μ : MeasureTheory.Measure ℝ}
|
||
[MeasureTheory.IsLocallyFiniteMeasure μ]
|
||
(ha : 0 < a) :
|
||
IntervalIntegrable Real.log μ 0 a
|
||
:= by
|
||
|
||
sorry
|
||
|
||
theorem integral_log₀
|
||
{b : ℝ}
|
||
(hb : 0 < b) :
|
||
∫ (x : ℝ) in (0)..b, Real.log x = b * (Real.log b - 1) := by
|
||
apply?
|
||
exact integral_log h
|
||
|
||
|
||
open Real Nat Set Finset
|
||
|
||
open scoped Real Interval
|
||
|
||
--variable {a b : ℝ} (n : ℕ)
|
||
|
||
namespace intervalIntegral
|
||
|
||
--open MeasureTheory
|
||
|
||
--variable {f : ℝ → ℝ} {μ ν : Measure ℝ} [IsLocallyFiniteMeasure μ] (c d : ℝ)
|
||
|
||
#check integral_mul_deriv_eq_deriv_mul
|
||
|
||
theorem integral_log₁
|
||
(h : (0 : ℝ) ∉ [[a, b]]) :
|
||
∫ x in a..b, log x = b * log b - a * log a - b + a := by
|
||
|
||
have h' : ∀ x ∈ [[a, b]], x ≠ 0 :=
|
||
fun x (hx : x ∈ [[a, b]]) => ne_of_mem_of_not_mem hx h
|
||
have heq : ∀ x ∈ [[a, b]], x * x⁻¹ = 1 :=
|
||
fun x hx => mul_inv_cancel (h' x hx)
|
||
|
||
let A := fun x hx => hasDerivAt_log (h' x hx)
|
||
|
||
convert integral_mul_deriv_eq_deriv_mul A (fun x _ => hasDerivAt_id x)
|
||
|
||
convert integral_mul_deriv_eq_deriv_mul A
|
||
(fun x _ => hasDerivAt_id x) (continuousOn_inv₀.mono <|
|
||
subset_compl_singleton_iff.mpr h).intervalIntegrable
|
||
continuousOn_const.intervalIntegrable using 1 <;>
|
||
|
||
simp [integral_congr heq, mul_comm, ← sub_add]
|