Locally integrable functions #
A function is called locally integrable (measure_theory.locally_integrable
) if it is integrable
on every compact subset of its domain.
This file contains properties of locally integrable functions and of integrability results on compact sets.
Main statements #
continuous.locally_integrable
: A continuous function is locally integrable.
A function f : X → E
is locally integrable if it is integrable on all compact sets.
See measure_theory.locally_integrable_iff
for the justification of this name.
Equations
- measure_theory.locally_integrable f μ = ∀ ⦃K : set X⦄, is_compact K → measure_theory.integrable_on f K μ
If a function is integrable at 𝓝[s] x
for each point x
of a compact set s
, then it is
integrable on s
.
A function f
continuous on a compact set K
is integrable on this set with respect to any
locally finite measure.
A continuous function f
is locally integrable with respect to any locally finite measure.
A continuous function with compact support is integrable on the whole space.