# mathlibdocumentation

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 #

• continuous.locally_integrable: A continuous function is locally integrable.
def measure_theory.locally_integrable {X : Type u_1} {E : Type u_3} [normed_group E] (f : X → E) (μ : . "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
• = ∀ ⦃K : set X⦄,
theorem measure_theory.integrable.locally_integrable {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} (hf : μ) :
theorem measure_theory.locally_integrable.ae_strongly_measurable {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} (hf : μ) :
theorem measure_theory.locally_integrable_iff {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X}  :
∀ (x : X), ∃ (U : set X) (H : U nhds x),
theorem measure_theory.integrable_on.mul_continuous_on_of_subset {X : Type u_1} {μ : measure_theory.measure X} {A K : set X} {g g' : X → } (hg : μ) (hg' : 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} {μ : measure_theory.measure X} {K : set X} {g g' : X → } [t2_space X] (hg : μ) (hg' : 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} {μ : measure_theory.measure X} {A K : set X} {g g' : X → } (hg : K) (hg' : μ) (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} {μ : measure_theory.measure X} {K : set X} {g g' : X → } [t2_space X] (hg : K) (hg' : μ) (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} [normed_group E] {f : X → E} {μ : measure_theory.measure X} {K : set X} (hK : is_compact K) (hf : ∀ (x : X), 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.

theorem continuous_on.integrable_on_compact {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} {K : set X} (hK : is_compact K) (hf : K) :

A function f continuous on a compact set K is integrable on this set with respect to any locally finite measure.

theorem continuous.locally_integrable {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} (hf : continuous f) :

A continuous function f is locally integrable with respect to any locally finite measure.

theorem continuous_on.integrable_on_Icc {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} {a b : X} [preorder X] (hf : (set.Icc a b)) :
μ
theorem continuous.integrable_on_Icc {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} {a b : X} [preorder X] (hf : continuous f) :
μ
theorem continuous.integrable_on_Ioc {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} {a b : X} [preorder X] (hf : continuous f) :
μ
theorem continuous_on.integrable_on_interval {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} {a b : X} [linear_order X] (hf : b)) :
μ
theorem continuous.integrable_on_interval {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} {a b : X} [linear_order X] (hf : continuous f) :
μ
theorem continuous.integrable_on_interval_oc {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} {a b : X} [linear_order X] (hf : continuous f) :
theorem continuous.integrable_of_has_compact_support {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} (hf : continuous f) (hcf : has_compact_support f) :

A continuous function with compact support is integrable on the whole space.

theorem monotone_on.integrable_on_compact {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} [borel_space X] {s : set X} (hs : is_compact s) (hmono : s) :
theorem antitone_on.integrable_on_compact {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} [borel_space X] {s : set X} (hs : is_compact s) (hanti : s) :
theorem monotone.locally_integrable {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} [borel_space X] (hmono : monotone f) :
theorem antitone.locally_integrable {X : Type u_1} {E : Type u_3} [normed_group E] {f : X → E} {μ : measure_theory.measure X} [borel_space X] (hanti : antitone f) :