English
The real logarithm is interval-integrable on any interval not passing through zero.
Русский
Логарифм по Лебегу интегрируем на любом интервале, не пересекающем ноль.
LaTeX
$$$\text{IntervalIntegrable } \log \text{ на любом интервале без 0}$$$
Lean4
/-- The real logarithm is interval integrable (with respect to the volume measure) on every interval.
See `intervalIntegrable_log` for a version applying to any locally finite measure, but with an
additional hypothesis on the interval.
-/
@[simp]
theorem intervalIntegrable_log' : IntervalIntegrable log volume a b := by
-- Log is even, so it suffices to consider the case 0 < a and b = 0
apply intervalIntegrable_of_even (log_neg_eq_log · |>.symm)
intro x hx
apply IntervalIntegrable.trans (b := 1)
· -- Show integrability on [0…1] using non-negativity of the derivative
rw [← neg_neg log]
apply IntervalIntegrable.neg
apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
· exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg
· intro s ⟨hs, _⟩
norm_num at *
simpa using (hasDerivAt_id s).sub (hasDerivAt_mul_log hs.ne.symm)
· intro s ⟨hs₁, hs₂⟩
norm_num at *
exact (log_nonpos_iff hs₁.le).mpr hs₂.le
· -- Show integrability on [1…t] by continuity
apply ContinuousOn.intervalIntegrable
apply Real.continuousOn_log.mono
apply Set.notMem_uIcc_of_lt zero_lt_one at hx
simpa
