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]
|