Locally integrable functions #
A function is called locally integrable (measure_theory.locally_integrable
) if it is integrable
on a neighborhood of every point.
This file contains properties of locally integrable functions and 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 a neighborhood of every
point. In particular, it is integrable on all compact sets,
see locally_integrable.integrable_on_is_compact
.
Equations
- measure_theory.locally_integrable f μ = ∀ (x : X), measure_theory.integrable_at_filter f (nhds x) μ
If a function is locally integrable, then it is integrable on an open neighborhood of any compact set.
If a function is locally integrable, then it is integrable on any compact set.
If a function is integrable at 𝓝[s] x
for each point x
of a compact set s
, then it is
integrable on s
.
A continuous function f
is locally integrable with respect to any locally finite measure.
A function f
continuous on a compact set K
is integrable on this set with respect to any
locally finite measure.
A continuous function with compact support is integrable on the whole space.