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 every compact subset of its domain.

This file contains properties of locally integrable functions and of 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_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 all compact sets. See measure_theory.locally_integrable_iff for the justification of this name.

Equations
theorem measure_theory.locally_integrable_iff {X : Type u_1} {E : Type u_3} [measurable_space X] [topological_space X] [normed_group E] {f : X → E} {μ : measure_theory.measure X} [locally_compact_space X] :
measure_theory.locally_integrable f μ ∀ (x : X), ∃ (U : set X) (H : U nhds x), measure_theory.integrable_on f U μ
theorem measure_theory.integrable_on.mul_continuous_on_of_subset {X : Type u_1} [measurable_space X] [topological_space X] {μ : measure_theory.measure X} [opens_measurable_space X] {A K : set X} {g g' : X → } (hg : measure_theory.integrable_on g A μ) (hg' : continuous_on g' K) (hA : measurable_set A) (hK : is_compact K) (hAK : A K) :
measure_theory.integrable_on (λ (x : X), g x * g' x) A μ
theorem measure_theory.integrable_on.mul_continuous_on {X : Type u_1} [measurable_space X] [topological_space X] {μ : measure_theory.measure X} [opens_measurable_space X] {K : set X} {g g' : X → } [t2_space X] (hg : measure_theory.integrable_on g K μ) (hg' : continuous_on g' K) (hK : is_compact K) :
measure_theory.integrable_on (λ (x : X), g x * g' x) K μ
theorem measure_theory.integrable_on.continuous_on_mul_of_subset {X : Type u_1} [measurable_space X] [topological_space X] {μ : measure_theory.measure X} [opens_measurable_space X] {A K : set X} {g g' : X → } (hg : continuous_on g K) (hg' : measure_theory.integrable_on g' A μ) (hK : is_compact K) (hA : measurable_set A) (hAK : A K) :
measure_theory.integrable_on (λ (x : X), g x * g' x) A μ
theorem measure_theory.integrable_on.continuous_on_mul {X : Type u_1} [measurable_space X] [topological_space X] {μ : measure_theory.measure X} [opens_measurable_space X] {K : set X} {g g' : X → } [t2_space X] (hg : continuous_on g K) (hg' : measure_theory.integrable_on g' K μ) (hK : is_compact K) :
measure_theory.integrable_on (λ (x : X), g x * g' x) K μ
theorem is_compact.integrable_on_of_nhds_within {X : Type u_1} {E : Type u_3} [measurable_space X] [topological_space X] [normed_group E] {f : X → E} {μ : measure_theory.measure X} {K : set X} (hK : is_compact K) (hf : ∀ (x : X), x Kmeasure_theory.integrable_at_filter f (nhds_within x 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.