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 onsis locally integrable ons.
def
measure_theory.locally_integrable_on
{X : Type u_1}
{E : Type u_3}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
(f : X → E)
(s : set X)
(μ : measure_theory.measure 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
- measure_theory.locally_integrable_on f s μ = ∀ (x : X), x ∈ s → measure_theory.integrable_at_filter f (nhds_within x s) μ
theorem
measure_theory.locally_integrable_on.mono
{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}
{s : set X}
(hf : measure_theory.locally_integrable_on f s μ)
{t : set X}
(hst : t ⊆ s) :
theorem
measure_theory.locally_integrable_on.norm
{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}
{s : set X}
(hf : measure_theory.locally_integrable_on f s μ) :
measure_theory.locally_integrable_on (λ (x : X), ‖f x‖) s μ
theorem
measure_theory.integrable_on.locally_integrable_on
{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}
{s : set X}
(hf : measure_theory.integrable_on f s μ) :
theorem
measure_theory.locally_integrable_on.integrable_on_is_compact
{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}
{s : set X}
(hf : measure_theory.locally_integrable_on f s μ)
(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}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{f : X → E}
{μ : measure_theory.measure X}
{s : set X}
(hf : measure_theory.locally_integrable_on f s μ)
{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}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{f : X → E}
{μ : measure_theory.measure X}
{s : set X}
[topological_space.second_countable_topology X]
(hf : measure_theory.locally_integrable_on f s μ) :
theorem
measure_theory.locally_integrable_on_iff
{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}
{s : set X}
[locally_compact_space X]
[t2_space X]
(hs : is_closed s ∨ is_open s) :
measure_theory.locally_integrable_on f s μ ↔ ∀ (k : set X), k ⊆ s → is_compact k → measure_theory.integrable_on f k μ
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}
[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
- measure_theory.locally_integrable f μ = ∀ (x : X), measure_theory.integrable_at_filter f (nhds x) μ
theorem
measure_theory.locally_integrable_on_univ
{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} :
theorem
measure_theory.locally_integrable.locally_integrable_on
{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}
(hf : measure_theory.locally_integrable f μ)
(s : set X) :
theorem
measure_theory.integrable.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}
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.locally_integrable_on_of_locally_integrable_restrict
{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}
{s : set X}
[opens_measurable_space X]
(hf : measure_theory.locally_integrable f (μ.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.)
theorem
measure_theory.locally_integrable_on_iff_locally_integrable_restrict
{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}
{s : set X}
[opens_measurable_space X]
(hs : is_closed s) :
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}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{f : X → E}
{μ : measure_theory.measure X}
{k : set X}
(hf : measure_theory.locally_integrable f μ)
(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}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{f : X → E}
{μ : measure_theory.measure X}
(hf : measure_theory.locally_integrable f μ)
{k : set X}
(hk : is_compact k) :
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}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{f : X → E}
{μ : measure_theory.measure X}
[locally_compact_space X] :
measure_theory.locally_integrable f μ ↔ ∀ (k : set X), is_compact k → measure_theory.integrable_on f k μ
theorem
measure_theory.locally_integrable.ae_strongly_measurable
{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}
[topological_space.second_countable_topology X]
(hf : measure_theory.locally_integrable f μ) :
theorem
measure_theory.locally_integrable_const
{X : Type u_1}
{E : Type u_3}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{μ : measure_theory.measure X}
[measure_theory.is_locally_finite_measure μ]
(c : E) :
measure_theory.locally_integrable (λ (x : X), c) μ
theorem
measure_theory.locally_integrable_on_const
{X : Type u_1}
{E : Type u_3}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{μ : measure_theory.measure X}
{s : set X}
[measure_theory.is_locally_finite_measure μ]
(c : E) :
measure_theory.locally_integrable_on (λ (x : X), c) s μ
theorem
measure_theory.locally_integrable.indicator
{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}
(hf : measure_theory.locally_integrable f μ)
{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}
[measurable_space X]
[topological_space X]
[measurable_space Y]
[topological_space Y]
[normed_add_comm_group E]
[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}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{f : X → E}
{μ : measure_theory.measure X}
[opens_measurable_space X]
[measure_theory.is_locally_finite_measure μ]
[second_countable_topology_either X E]
(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}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{f : X → E}
{μ : measure_theory.measure X}
[opens_measurable_space X]
[measure_theory.is_locally_finite_measure μ]
{K : set X}
[second_countable_topology_either X E]
(hf : continuous_on f 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}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{f : X → E}
{μ : measure_theory.measure X}
[opens_measurable_space X]
[measure_theory.is_locally_finite_measure μ]
{K : set X}
[topological_space.metrizable_space X]
(hK : is_compact K)
(hf : continuous_on f 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}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{f : X → E}
{μ : measure_theory.measure X}
[opens_measurable_space X]
[measure_theory.is_locally_finite_measure μ]
{a b : X}
[topological_space.metrizable_space X]
[preorder X]
[compact_Icc_space X]
(hf : continuous_on f (set.Icc a b)) :
measure_theory.integrable_on f (set.Icc a b) μ
theorem
continuous.integrable_on_Icc
{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}
[opens_measurable_space X]
[measure_theory.is_locally_finite_measure μ]
{a b : X}
[topological_space.metrizable_space X]
[preorder X]
[compact_Icc_space X]
(hf : continuous f) :
measure_theory.integrable_on f (set.Icc a b) μ
theorem
continuous.integrable_on_Ioc
{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}
[opens_measurable_space X]
[measure_theory.is_locally_finite_measure μ]
{a b : X}
[topological_space.metrizable_space X]
[preorder X]
[compact_Icc_space X]
(hf : continuous f) :
measure_theory.integrable_on f (set.Ioc a b) μ
theorem
continuous_on.integrable_on_uIcc
{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}
[opens_measurable_space X]
[measure_theory.is_locally_finite_measure μ]
{a b : X}
[topological_space.metrizable_space X]
[linear_order X]
[compact_Icc_space X]
(hf : continuous_on f (set.uIcc a b)) :
measure_theory.integrable_on f (set.uIcc a b) μ
theorem
continuous.integrable_on_uIcc
{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}
[opens_measurable_space X]
[measure_theory.is_locally_finite_measure μ]
{a b : X}
[topological_space.metrizable_space X]
[linear_order X]
[compact_Icc_space X]
(hf : continuous f) :
measure_theory.integrable_on f (set.uIcc a b) μ
theorem
continuous.integrable_on_uIoc
{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}
[opens_measurable_space X]
[measure_theory.is_locally_finite_measure μ]
{a b : X}
[topological_space.metrizable_space X]
[linear_order X]
[compact_Icc_space X]
(hf : continuous f) :
measure_theory.integrable_on f (set.uIoc a b) μ
theorem
continuous.integrable_of_has_compact_support
{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}
[opens_measurable_space X]
[measure_theory.is_locally_finite_measure μ]
[topological_space.metrizable_space 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}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{f : X → E}
{μ : measure_theory.measure X}
{s : set X}
[borel_space X]
[conditionally_complete_linear_order X]
[conditionally_complete_linear_order E]
[order_topology X]
[order_topology E]
[topological_space.second_countable_topology E]
(hmono : monotone_on f s)
{a b : X}
(ha : is_least s a)
(hb : is_greatest s b)
(hs : ⇑μ s ≠ ⊤)
(h's : measurable_set s) :
theorem
monotone_on.integrable_on_is_compact
{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}
{s : set X}
[borel_space X]
[conditionally_complete_linear_order X]
[conditionally_complete_linear_order E]
[order_topology X]
[order_topology E]
[topological_space.second_countable_topology E]
[measure_theory.is_finite_measure_on_compacts μ]
(hs : is_compact s)
(hmono : monotone_on f s) :
theorem
antitone_on.integrable_on_of_measure_ne_top
{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}
{s : set X}
[borel_space X]
[conditionally_complete_linear_order X]
[conditionally_complete_linear_order E]
[order_topology X]
[order_topology E]
[topological_space.second_countable_topology E]
(hanti : antitone_on f s)
{a b : X}
(ha : is_least s a)
(hb : is_greatest s b)
(hs : ⇑μ s ≠ ⊤)
(h's : measurable_set s) :
theorem
antione_on.integrable_on_is_compact
{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}
{s : set X}
[borel_space X]
[conditionally_complete_linear_order X]
[conditionally_complete_linear_order E]
[order_topology X]
[order_topology E]
[topological_space.second_countable_topology E]
[measure_theory.is_finite_measure_on_compacts μ]
(hs : is_compact s)
(hanti : antitone_on f s) :
theorem
monotone.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}
[borel_space X]
[conditionally_complete_linear_order X]
[conditionally_complete_linear_order E]
[order_topology X]
[order_topology E]
[topological_space.second_countable_topology E]
[measure_theory.is_locally_finite_measure μ]
(hmono : monotone f) :
theorem
antitone.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}
[borel_space X]
[conditionally_complete_linear_order X]
[conditionally_complete_linear_order E]
[order_topology X]
[order_topology E]
[topological_space.second_countable_topology E]
[measure_theory.is_locally_finite_measure μ]
(hanti : antitone f) :
theorem
measure_theory.integrable_on.mul_continuous_on_of_subset
{X : Type u_1}
{R : Type u_4}
[measurable_space X]
[topological_space X]
{μ : measure_theory.measure X}
[opens_measurable_space X]
{A K : set X}
[normed_ring R]
[second_countable_topology_either X R]
{g g' : X → R}
(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}
{R : Type u_4}
[measurable_space X]
[topological_space X]
{μ : measure_theory.measure X}
[opens_measurable_space X]
{K : set X}
[normed_ring R]
[second_countable_topology_either X R]
{g g' : X → R}
[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}
{R : Type u_4}
[measurable_space X]
[topological_space X]
{μ : measure_theory.measure X}
[opens_measurable_space X]
{A K : set X}
[normed_ring R]
[second_countable_topology_either X R]
{g g' : X → R}
(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}
{R : Type u_4}
[measurable_space X]
[topological_space X]
{μ : measure_theory.measure X}
[opens_measurable_space X]
{K : set X}
[normed_ring R]
[second_countable_topology_either X R]
{g g' : X → R}
[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
measure_theory.integrable_on.continuous_on_smul
{X : Type u_1}
{E : Type u_3}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{μ : measure_theory.measure X}
[opens_measurable_space X]
{K : set X}
{𝕜 : Type u_5}
[normed_field 𝕜]
[normed_space 𝕜 E]
[t2_space X]
[second_countable_topology_either X 𝕜]
{g : X → E}
(hg : measure_theory.integrable_on g K μ)
{f : X → 𝕜}
(hf : continuous_on f 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}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{μ : measure_theory.measure X}
[opens_measurable_space X]
{K : set X}
{𝕜 : Type u_5}
[normed_field 𝕜]
[normed_space 𝕜 E]
[t2_space X]
[second_countable_topology_either X E]
{f : X → 𝕜}
(hf : measure_theory.integrable_on f K μ)
{g : X → E}
(hg : continuous_on g 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}
[measurable_space X]
[topological_space X]
{μ : measure_theory.measure X}
[opens_measurable_space X]
[locally_compact_space X]
[t2_space X]
[normed_ring R]
[second_countable_topology_either X R]
{f g : X → R}
{s : set X}
(hf : measure_theory.locally_integrable_on f s μ)
(hg : continuous_on g 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}
[measurable_space X]
[topological_space X]
{μ : measure_theory.measure X}
[opens_measurable_space X]
[locally_compact_space X]
[t2_space X]
[normed_ring R]
[second_countable_topology_either X R]
{f g : X → R}
{s : set X}
(hf : measure_theory.locally_integrable_on f s μ)
(hg : continuous_on g 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}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{μ : measure_theory.measure X}
[opens_measurable_space X]
[locally_compact_space X]
[t2_space X]
{𝕜 : Type u_2}
[normed_field 𝕜]
[second_countable_topology_either X 𝕜]
[normed_space 𝕜 E]
{f : X → E}
{g : X → 𝕜}
{s : set X}
(hs : is_open s)
(hf : measure_theory.locally_integrable_on f s μ)
(hg : continuous_on g 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}
[measurable_space X]
[topological_space X]
[normed_add_comm_group E]
{μ : measure_theory.measure X}
[opens_measurable_space X]
[locally_compact_space X]
[t2_space X]
{𝕜 : Type u_2}
[normed_field 𝕜]
[second_countable_topology_either X E]
[normed_space 𝕜 E]
{f : X → 𝕜}
{g : X → E}
{s : set X}
(hs : is_open s)
(hf : measure_theory.locally_integrable_on f s μ)
(hg : continuous_on g s) :
measure_theory.locally_integrable_on (λ (x : X), f x • g x) s μ