mathlib documentation

measure_theory.function.locally_integrable

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 #

def measure_theory.locally_integrable {X : Type u_1} {E : Type u_3} [measurable_space X] [topological_space X] [normed_add_comm_group E] (f : X E) (μ : measure_theory.measure X . "volume_tac") :
Prop

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

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.