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}
[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
- measure_theory.locally_integrable f μ = ∀ ⦃K : set X⦄, is_compact K → measure_theory.integrable_on f K μ
theorem
measure_theory.integrable.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}
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.locally_integrable.ae_strongly_measurable
{X : Type u_1}
{E : Type u_3}
[measurable_space X]
[topological_space X]
[normed_group E]
{f : X → E}
{μ : measure_theory.measure X}
[sigma_compact_space X]
(hf : measure_theory.locally_integrable f μ) :
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 ∈ 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_on.integrable_on_compact
{X : Type u_1}
{E : Type u_3}
[measurable_space X]
[topological_space X]
[normed_group E]
{f : X → E}
{μ : measure_theory.measure X}
[opens_measurable_space X]
[topological_space.metrizable_space X]
[measure_theory.is_locally_finite_measure μ]
{K : set 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.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}
[opens_measurable_space X]
[topological_space.metrizable_space X]
[measure_theory.is_locally_finite_measure μ]
(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}
[measurable_space X]
[topological_space X]
[normed_group E]
{f : X → E}
{μ : measure_theory.measure X}
[opens_measurable_space X]
[topological_space.metrizable_space X]
[measure_theory.is_locally_finite_measure μ]
{a b : 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_group E]
{f : X → E}
{μ : measure_theory.measure X}
[opens_measurable_space X]
[topological_space.metrizable_space X]
[measure_theory.is_locally_finite_measure μ]
{a b : 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_group E]
{f : X → E}
{μ : measure_theory.measure X}
[opens_measurable_space X]
[topological_space.metrizable_space X]
[measure_theory.is_locally_finite_measure μ]
{a b : X}
[preorder X]
[compact_Icc_space X]
(hf : continuous f) :
measure_theory.integrable_on f (set.Ioc a b) μ
theorem
continuous_on.integrable_on_interval
{X : Type u_1}
{E : Type u_3}
[measurable_space X]
[topological_space X]
[normed_group E]
{f : X → E}
{μ : measure_theory.measure X}
[opens_measurable_space X]
[topological_space.metrizable_space X]
[measure_theory.is_locally_finite_measure μ]
{a b : X}
[linear_order X]
[compact_Icc_space X]
(hf : continuous_on f (set.interval a b)) :
measure_theory.integrable_on f (set.interval a b) μ
theorem
continuous.integrable_on_interval
{X : Type u_1}
{E : Type u_3}
[measurable_space X]
[topological_space X]
[normed_group E]
{f : X → E}
{μ : measure_theory.measure X}
[opens_measurable_space X]
[topological_space.metrizable_space X]
[measure_theory.is_locally_finite_measure μ]
{a b : X}
[linear_order X]
[compact_Icc_space X]
(hf : continuous f) :
measure_theory.integrable_on f (set.interval a b) μ
theorem
continuous.integrable_on_interval_oc
{X : Type u_1}
{E : Type u_3}
[measurable_space X]
[topological_space X]
[normed_group E]
{f : X → E}
{μ : measure_theory.measure X}
[opens_measurable_space X]
[topological_space.metrizable_space X]
[measure_theory.is_locally_finite_measure μ]
{a b : X}
[linear_order X]
[compact_Icc_space X]
(hf : continuous f) :
measure_theory.integrable_on f (set.interval_oc a b) μ
theorem
continuous.integrable_of_has_compact_support
{X : Type u_1}
{E : Type u_3}
[measurable_space X]
[topological_space X]
[normed_group E]
{f : X → E}
{μ : measure_theory.measure X}
[opens_measurable_space X]
[topological_space.metrizable_space X]
[measure_theory.is_locally_finite_measure μ]
(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}
[measurable_space X]
[topological_space X]
[normed_group E]
{f : X → E}
{μ : measure_theory.measure X}
[borel_space X]
[topological_space.metrizable_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 μ]
{s : set X}
(hs : is_compact s)
(hmono : monotone_on f s) :
theorem
antitone_on.integrable_on_compact
{X : Type u_1}
{E : Type u_3}
[measurable_space X]
[topological_space X]
[normed_group E]
{f : X → E}
{μ : measure_theory.measure X}
[borel_space X]
[topological_space.metrizable_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 μ]
{s : set X}
(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_group E]
{f : X → E}
{μ : measure_theory.measure X}
[borel_space X]
[topological_space.metrizable_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_group E]
{f : X → E}
{μ : measure_theory.measure X}
[borel_space X]
[topological_space.metrizable_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) :