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 #
continuous.locally_integrable: A continuous function is locally integrable.
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.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.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.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_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.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
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]
[normed_ring R]
[second_countable_topology_either X R]
{A K : set X}
{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]
[normed_ring R]
[second_countable_topology_either X R]
{K : set X}
{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]
[normed_ring R]
[second_countable_topology_either X R]
{A K : set X}
{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]
[normed_ring R]
[second_countable_topology_either X R]
{K : set X}
{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
is_compact.integrable_on_of_nhds_within
{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}
(hK : is_compact K)
(hf : ∀ (x : X), x ∈ K → measure_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.
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.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}
[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]
{s : set X}
(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}
[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]
{s : set X}
[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}
[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]
{s : set X}
(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}
[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]
{s : set X}
[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) :