Classes for finite measures #
We introduce the following typeclasses for measures:
IsFiniteMeasure μ
:μ univ < ∞
;IsLocallyFiniteMeasure μ
:∀ x, ∃ s ∈ 𝓝 x, μ 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
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 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
.
Equations
- μ.FiniteAtFilter f = ∃ s ∈ f, μ s < ⊤
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 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
).
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
- μ.finiteSpanningSetsInOpen = { set := fun (n : ℕ) => ⋯.choose, set_mem := ⋯, finite := ⋯, spanning := ⋯ }
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