Classes of measures #
We introduce the following typeclasses for measures:
IsProbabilityMeasure μ
:μ univ = 1
;IsFiniteMeasure μ
:μ univ < ∞
;IsZeroOrProbabilityMeasure μ
:μ univ = 0 ∨ μ univ = 1
;SigmaFinite μ
: there exists a countable collection of sets that coveruniv
whereμ
is finite;SFinite μ
: the measureμ
can be written as a countable sum of finite measures;IsLocallyFiniteMeasure μ
:∀ x, ∃ s ∈ 𝓝 x, μ s < ∞
;NoAtoms μ
:∀ x, μ {x} = 0
; possibly should be redefined as∀ s, 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s
.
A measure μ
is called finite if μ univ < ∞
.
Instances
The measure of the whole space with respect to a finite measure, considered as ℝ≥0
.
Equations
- MeasureTheory.measureUnivNNReal μ = (μ Set.univ).toNNReal
Instances For
le_of_add_le_add_left
is normally applicable to OrderedCancelAddCommMonoid
,
but it holds for measures with the additional assumption that μ is finite.
A measure μ
is zero or a probability measure if μ univ = 0
or μ univ = 1
. This class
of measures appears naturally when conditioning on events, and many results which are true for
probability measures hold more generally over this class.
Instances
A measure μ
is called a probability measure if μ univ = 1
.
- measure_univ : μ Set.univ = 1
Instances
Note that this is not quite as useful as it looks because the measure takes values in ℝ≥0∞
.
Thus the subtraction appearing is the truncated subtraction of ℝ≥0∞
, rather than the
better-behaved subtraction of ℝ
.
Note that this is not quite as useful as it looks because the measure takes values in ℝ≥0∞
.
Thus the subtraction appearing is the truncated subtraction of ℝ≥0∞
, rather than the
better-behaved subtraction of ℝ
.
Measure μ
has no atoms if the measure of each singleton is zero.
NB: Wikipedia assumes that for any measurable set s
with positive μ
-measure,
there exists a measurable t ⊆ s
such that 0 < μ t < μ s
. While this implies μ {x} = 0
,
the converse is not true.
- measure_singleton : ∀ (x : α), μ {x} = 0
Instances
A measure is called finite at filter f
if it is finite at some set s ∈ f
.
Equivalently, it is eventually finite at s
in f.small_sets
.
Instances For
μ
has finite spanning sets in C
if there is a countable sequence of sets in C
that have
finite measures. This structure is a type, which is useful if we want to record extra properties
about the sets, such as that they are monotone.
SigmaFinite
is defined in terms of this: μ
is σ-finite if there exists a sequence of
finite spanning sets in the collection of all measurable sets.
Instances For
A measure is called s-finite if it is a countable sum of finite measures.
- out' : ∃ (m : ℕ → MeasureTheory.Measure α), (∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (m n)) ∧ μ = MeasureTheory.Measure.sum m
Instances
A sequence of finite measures such that μ = sum (sfiniteSeq μ)
(see sum_sfiniteSeq
).
Equations
- MeasureTheory.sfiniteSeq μ = ⋯.choose
Instances For
Alias of MeasureTheory.sfiniteSeq
.
A sequence of finite measures such that μ = sum (sfiniteSeq μ)
(see sum_sfiniteSeq
).
Instances For
Alias of MeasureTheory.sum_sfiniteSeq
.
Alias of MeasureTheory.sfiniteSeq_le
.
Alias of MeasureTheory.sfiniteSeq_zero
.
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
- MeasureTheory.spanningSets μ i = Set.Accumulate μ.toFiniteSpanningSetsIn.set i
Instances For
Alias of MeasureTheory.measurableSet_spanningSets
.
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.
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
.
Equations
- h.mono' hC = { set := h.set, set_mem := ⋯, finite := ⋯, spanning := ⋯ }
Instances For
If μ
has finite spanning sets in C
and C ⊆ D
then μ
has finite spanning sets in D
.
Equations
- h.mono hC = h.mono' ⋯
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.
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.
A measure is called locally finite if it is finite in some neighborhood of each point.
- finiteAtNhds : ∀ (x : α), μ.FiniteAtFilter (nhds x)
Instances
A measure μ
is finite on compacts if any compact set K
satisfies μ K < ∞
.
Instances
A compact subset has finite measure for a measure which is finite on compacts.
A compact subset has finite measure for a measure which is finite on compacts.
A bounded subset has finite measure for a measure which is finite on compact sets, in a proper space.
A measure which is finite on compact sets in a locally compact space is locally finite.
If a set has zero measure in a neighborhood of each of its points, then it has zero measure in a second-countable space.
If two finite measures give the same mass to the whole space and coincide on a π-system made of measurable sets, then they coincide on all sets in the σ-algebra generated by the π-system.
Two finite measures are equal if they are equal on the π-system generating the σ-algebra
(and univ
).
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 := ⋯ }
Instances For
Alias of the forward direction of MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff
.
If s
is a compact set and μ
is finite at 𝓝 x
for every x ∈ s
, then s
admits an open
superset of finite measure.
If s
is a compact set and μ
is a locally finite measure, then s
admits an open superset of
finite measure.
Compact covering of a σ
-compact topological space as
MeasureTheory.Measure.FiniteSpanningSetsIn
.
Equations
- μ.finiteSpanningSetsInCompact = { set := compactCovering α, set_mem := ⋯, finite := ⋯, spanning := ⋯ }
Instances For
A locally finite measure on a σ
-compact topological space admits a finite spanning sequence
of open sets.
Equations
Instances For
A locally finite measure on a second countable topological space admits a finite spanning sequence of open sets.
Equations
- μ.finiteSpanningSetsInOpen' = let_fun H := ⋯; H.some