Classes for s-finite measures #
We introduce the following typeclasses for measures:
SFinite μ: the measureμcan be written as a countable sum of finite measures;SigmaFinite μ: there exists a countable collection of sets that coverunivwhereμis finite.
A measure is called s-finite if it is a countable sum of finite measures.
- out' : ∃ (m : ℕ → Measure α), (∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ μ = Measure.sum m
Instances
A sequence of finite measures such that μ = sum (sfiniteSeq μ) (see sum_sfiniteSeq).
Equations
Instances For
A countable sum of finite measures is s-finite. This lemma is superseded by the instance below.
For an s-finite measure μ, there exists a finite measure ν
such that each of μ and ν is absolutely continuous with respect to the other.
A measure μ is called σ-finite if there is a countable collection of sets
{ A i | i ∈ ℕ } such that μ (A i) < ∞ and ⋃ i, A i = s.
- out' : Nonempty (μ.FiniteSpanningSetsIn Set.univ)
Instances
If μ is σ-finite it has finite spanning sets in the collection of all measurable sets.
Equations
- μ.toFiniteSpanningSetsIn = { set := fun (n : ℕ) => MeasureTheory.toMeasurable μ (⋯.some.set n), set_mem := ⋯, finite := ⋯, spanning := ⋯ }
Instances For
A noncomputable way to get a monotone collection of sets that span univ and have finite
measure using Classical.choose. This definition satisfies monotonicity in addition to all other
properties in SigmaFinite.
Equations
Instances For
spanningSetsIndex μ x is the least n : ℕ such that x ∈ spanningSets μ n.
Equations
Instances For
A set in a σ-finite space has zero measure if and only if its intersection with all members of the countable family of finite measure spanning sets has zero measure.
A set in a σ-finite space has positive measure if and only if its intersection with some member of the countable family of finite measure spanning sets has positive measure.
If the union of a.e.-disjoint null-measurable sets has finite measure, then there are only finitely many members of the union whose measure exceeds any given positive number.
If the union of disjoint measurable sets has finite measure, then there are only finitely many members of the union whose measure exceeds any given positive number.
If all elements of an infinite set have measure uniformly separated from zero, then the set has infinite measure.
If the union of a.e.-disjoint null-measurable sets has finite measure, then there are only countably many members of the union whose measure is positive.
If the union of disjoint measurable sets has finite measure, then there are only countably many members of the union whose measure is positive.
In an s-finite space, among disjoint null-measurable sets, only countably many can have positive measure.
In an s-finite space, among disjoint measurable sets, only countably many can have positive measure.
Given a family of measurable sets, its measurable union is its union modulo sets of measure
zero. It is well defined up to measure 0. For instance, the measurable union of all the singleton
sets in ℝ is empty (while the usual union would be the whole space).
This lemma shows the existence of a measurable union, writing it as the union of a countable
subfamily.
If a measure μ is the sum of a countable family mₙ, and a set t has finite measure for
each mₙ, then its measurable superset toMeasurable μ t (which has the same measure as t)
satisfies, for any measurable set s, the equality μ (toMeasurable μ t ∩ s) = μ (t ∩ s).
If a set t is covered by a countable family of finite measure sets, then its measurable
superset toMeasurable μ t (which has the same measure as t) satisfies,
for any measurable set s, the equality μ (toMeasurable μ t ∩ s) = μ (t ∩ s).
The measurable superset toMeasurable μ t of t (which has the same measure as t)
satisfies, for any measurable set s, the equality μ (toMeasurable μ t ∩ s) = μ (t ∩ s).
This only holds when μ is s-finite -- for example for σ-finite measures. For a version without
this assumption (but requiring that t has finite measure), see measure_toMeasurable_inter.
Auxiliary lemma for iSup_restrict_spanningSets.
In a σ-finite space, any measurable set of measure > r contains a measurable subset of
finite measure > r.
If μ has finite spanning sets in C and C ∩ {s | μ s < ∞} ⊆ D then μ has finite spanning
sets in D.
Instances For
If μ has finite spanning sets in C and C ⊆ D then μ has finite spanning sets in D.
Instances For
If μ has finite spanning sets in the collection of measurable sets C, then μ is σ-finite.
An extensionality for measures. It is ext_of_generateFrom_of_iUnion formulated in terms of
FiniteSpanningSetsIn.
Given measures μ, ν where ν ≤ μ, FiniteSpanningSetsIn.ofLe provides the induced
FiniteSpanningSet with respect to ν from a FiniteSpanningSet with respect to μ.
Equations
- MeasureTheory.Measure.FiniteSpanningSetsIn.ofLE h S = { set := S.set, set_mem := ⋯, finite := ⋯, spanning := ⋯ }
Instances For
Every finite measure is σ-finite.
A measure on a countable space is sigma-finite iff it gives finite mass to every singleton.
See measure_singleton_lt_top for the forward direction without the countability assumption.
Similar to ae_of_forall_measure_lt_top_ae_restrict, but where you additionally get the
hypothesis that another σ-finite measure has finite values on s.
To prove something for almost all x w.r.t. a σ-finite measure, it is sufficient to show that
this holds almost everywhere in sets where the measure has finite value.
Given S : μ.FiniteSpanningSetsIn {s | MeasurableSet s},
FiniteSpanningSetsIn.disjointed provides a FiniteSpanningSetsIn {s | MeasurableSet s}
such that its underlying sets are pairwise disjoint.
Equations
- S.disjointed = { set := disjointed S.set, set_mem := ⋯, finite := ⋯, spanning := ⋯ }