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.
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,
- 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
A continuous function
f is locally integrable with respect to any locally finite measure.
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.