theorem Real.log_locallyBoundedOn : IsLocallyBoundedOn log (Set.Ioi 0)

theorem Real.log_locallyIntegrableOn : MeasureTheory.LocallyIntegrableOn log {0}ᶜ MeasureTheory.volume