# mathlib3documentation

measure_theory.function.locally_integrable

# Locally integrable functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A function is called locally integrable (measure_theory.locally_integrable) if it is integrable on a neighborhood of every point. More generally, it is locally integrable on s if it is locally integrable on a neighbourhood within s of any point of s.

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.
• continuous_on.locally_integrable_on: A function which is continuous on s is locally integrable on s.
def measure_theory.locally_integrable_on {X : Type u_1} {E : Type u_3} (f : X E) (s : set X) (μ : . "volume_tac") :
Prop

A function f : X → E is locally integrable on s, for s ⊆ X, if for every x ∈ s there is a neighbourhood of x within s on which f is integrable. (Note this is, in general, strictly weaker than local integrability with respect to μ.restrict s.)

Equations
theorem measure_theory.locally_integrable_on.mono {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {s : set X} (hf : μ) {t : set X} (hst : t s) :
theorem measure_theory.locally_integrable_on.norm {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {s : set X} (hf : μ) :
theorem measure_theory.integrable_on.locally_integrable_on {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {s : set X} (hf : μ) :
theorem measure_theory.locally_integrable_on.integrable_on_is_compact {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {s : set X} (hf : μ) (hs : is_compact s) :

If a function is locally integrable on a compact set, then it is integrable on that set.

theorem measure_theory.locally_integrable_on.integrable_on_compact_subset {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {s : set X} (hf : μ) {t : set X} (hst : t s) (ht : is_compact t) :
theorem measure_theory.locally_integrable_on.ae_strongly_measurable {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {s : set X} (hf : μ) :
theorem measure_theory.locally_integrable_on_iff {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {s : set X} [t2_space X] (hs : ) :
(k : set X), k s

If s is either open, or closed, then f is locally integrable on s iff it is integrable on every compact subset contained in s.

def measure_theory.locally_integrable {X : Type u_1} {E : Type u_3} (f : X E) (μ : . "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
theorem measure_theory.locally_integrable_on_univ {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} :
theorem measure_theory.locally_integrable.locally_integrable_on {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} (hf : μ) (s : set X) :
theorem measure_theory.integrable.locally_integrable {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} (hf : μ) :
theorem measure_theory.locally_integrable_on_of_locally_integrable_restrict {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {s : set X} (hf : (μ.restrict s)) :

If f is locally integrable with respect to μ.restrict s, it is locally integrable on s. (See locally_integrable_on_iff_locally_integrable_restrict for an iff statement when s is closed.)

If s is closed, being locally integrable on s wrt μ is equivalent to being locally integrable with respect to μ.restrict s. For the one-way implication without assuming s closed, see locally_integrable_on_of_locally_integrable_restrict.

theorem measure_theory.locally_integrable.integrable_on_is_compact {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {k : set X} (hf : μ) (hk : is_compact k) :

If a function is locally integrable, then it is integrable on any compact set.

theorem measure_theory.locally_integrable.integrable_on_nhds_is_compact {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} (hf : μ) {k : set X} (hk : is_compact k) :
(u : set X), k u

If a function is locally integrable, then it is integrable on an open neighborhood of any compact set.

theorem measure_theory.locally_integrable_iff {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X}  :
(k : set X),
theorem measure_theory.locally_integrable.ae_strongly_measurable {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} (hf : μ) :
theorem measure_theory.locally_integrable_const {X : Type u_1} {E : Type u_3} {μ : measure_theory.measure X} (c : E) :
theorem measure_theory.locally_integrable_on_const {X : Type u_1} {E : Type u_3} {μ : measure_theory.measure X} {s : set X} (c : E) :
theorem measure_theory.locally_integrable.indicator {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} (hf : μ) {s : set X} (hs : measurable_set s) :
theorem measure_theory.locally_integrable_map_homeomorph {X : Type u_1} {Y : Type u_2} {E : Type u_3} [borel_space X] [borel_space Y] (e : X ≃ₜ Y) {f : Y E} {μ : measure_theory.measure X} :
theorem continuous.locally_integrable {X : Type u_1} {E : Type u_3} {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.locally_integrable_on {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {K : set X} (hf : K) (hK : measurable_set K) :

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

theorem continuous_on.integrable_on_compact {X : Type u_1} {E : Type u_3} {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_on.integrable_on_Icc {X : Type u_1} {E : Type u_3} {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} {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} {f : X E} {μ : measure_theory.measure X} {a b : X} [preorder X] (hf : continuous f) :
μ
theorem continuous_on.integrable_on_uIcc {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {a b : X} [linear_order X] (hf : (set.uIcc a b)) :
μ
theorem continuous.integrable_on_uIcc {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {a b : X} [linear_order X] (hf : continuous f) :
μ
theorem continuous.integrable_on_uIoc {X : Type u_1} {E : Type u_3} {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} {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_of_measure_ne_top {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {s : set X} [borel_space X] (hmono : s) {a b : X} (ha : a) (hb : b) (hs : μ s ) (h's : measurable_set s) :
theorem monotone_on.integrable_on_is_compact {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {s : set X} [borel_space X] (hs : is_compact s) (hmono : s) :
theorem antitone_on.integrable_on_of_measure_ne_top {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {s : set X} [borel_space X] (hanti : s) {a b : X} (ha : a) (hb : b) (hs : μ s ) (h's : measurable_set s) :
theorem antione_on.integrable_on_is_compact {X : Type u_1} {E : Type u_3} {f : X E} {μ : measure_theory.measure X} {s : set X} [borel_space X] (hs : is_compact s) (hanti : s) :
theorem monotone.locally_integrable {X : Type u_1} {E : Type u_3} {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} {f : X E} {μ : measure_theory.measure X} [borel_space X] (hanti : antitone f) :
theorem measure_theory.integrable_on.mul_continuous_on_of_subset {X : Type u_1} {R : Type u_4} {μ : measure_theory.measure X} {A K : set X} [normed_ring R] {g g' : X R} (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} {R : Type u_4} {μ : measure_theory.measure X} {K : set X} [normed_ring R] {g g' : X R} [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} {R : Type u_4} {μ : measure_theory.measure X} {A K : set X} [normed_ring R] {g g' : X R} (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} {R : Type u_4} {μ : measure_theory.measure X} {K : set X} [normed_ring R] {g g' : X R} [t2_space X] (hg : K) (hg' : μ) (hK : is_compact K) :
measure_theory.integrable_on (λ (x : X), g x * g' x) K μ
theorem measure_theory.integrable_on.continuous_on_smul {X : Type u_1} {E : Type u_3} {μ : measure_theory.measure X} {K : set X} {𝕜 : Type u_5} [normed_field 𝕜] [ E] [t2_space X] {g : X E} (hg : μ) {f : X 𝕜} (hf : K) (hK : is_compact K) :
measure_theory.integrable_on (λ (x : X), f x g x) K μ
theorem measure_theory.integrable_on.smul_continuous_on {X : Type u_1} {E : Type u_3} {μ : measure_theory.measure X} {K : set X} {𝕜 : Type u_5} [normed_field 𝕜] [ E] [t2_space X] {f : X 𝕜} (hf : μ) {g : X E} (hg : K) (hK : is_compact K) :
measure_theory.integrable_on (λ (x : X), f x g x) K μ
theorem measure_theory.locally_integrable_on.continuous_on_mul {X : Type u_1} {R : Type u_4} {μ : measure_theory.measure X} [t2_space X] [normed_ring R] {f g : X R} {s : set X} (hf : μ) (hg : s) (hs : is_open s) :
measure_theory.locally_integrable_on (λ (x : X), g x * f x) s μ
theorem measure_theory.locally_integrable_on.mul_continuous_on {X : Type u_1} {R : Type u_4} {μ : measure_theory.measure X} [t2_space X] [normed_ring R] {f g : X R} {s : set X} (hf : μ) (hg : s) (hs : is_open s) :
measure_theory.locally_integrable_on (λ (x : X), f x * g x) s μ
theorem measure_theory.locally_integrable_on.continuous_on_smul {X : Type u_1} {E : Type u_3} {μ : measure_theory.measure X} [t2_space X] {𝕜 : Type u_2} [normed_field 𝕜] [ E] {f : X E} {g : X 𝕜} {s : set X} (hs : is_open s) (hf : μ) (hg : s) :
measure_theory.locally_integrable_on (λ (x : X), g x f x) s μ
theorem measure_theory.locally_integrable_on.smul_continuous_on {X : Type u_1} {E : Type u_3} {μ : measure_theory.measure X} [t2_space X] {𝕜 : Type u_2} [normed_field 𝕜] [ E] {f : X 𝕜} {g : X E} {s : set X} (hs : is_open s) (hf : μ) (hg : s) :
measure_theory.locally_integrable_on (λ (x : X), f x g x) s μ