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 cover univ 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.
class MeasureTheory.IsFiniteMeasure {α : Type u_1} {m0 : } (μ : ) :

A measure μ is called finite if μ univ < ∞.

• measure_univ_lt_top : μ Set.univ <
Instances
theorem MeasureTheory.IsFiniteMeasure.measure_univ_lt_top {α : Type u_1} {m0 : } {μ : } [self : ] :
μ Set.univ <
theorem MeasureTheory.not_isFiniteMeasure_iff {α : Type u_1} {m0 : } {μ : } :
μ Set.univ =
instance MeasureTheory.Restrict.isFiniteMeasure {α : Type u_1} {m0 : } {s : Set α} (μ : ) [hs : Fact (μ s < )] :
Equations
• =
@[simp]
theorem MeasureTheory.measure_lt_top {α : Type u_1} {m0 : } (μ : ) (s : Set α) :
μ s <
instance MeasureTheory.isFiniteMeasureRestrict {α : Type u_1} {m0 : } (μ : ) (s : Set α) :
Equations
• =
@[simp]
theorem MeasureTheory.measure_ne_top {α : Type u_1} {m0 : } (μ : ) (s : Set α) :
μ s
theorem MeasureTheory.measure_compl_le_add_of_le_add {α : Type u_1} {m0 : } {μ : } {s : Set α} {t : Set α} (hs : ) (ht : ) {ε : ENNReal} (h : μ s μ t + ε) :
μ t μ s + ε
theorem MeasureTheory.measure_compl_le_add_iff {α : Type u_1} {m0 : } {μ : } {s : Set α} {t : Set α} (hs : ) (ht : ) {ε : ENNReal} :
μ s μ t + ε μ t μ s + ε
def MeasureTheory.measureUnivNNReal {α : Type u_1} {m0 : } (μ : ) :

The measure of the whole space with respect to a finite measure, considered as ℝ≥0.

Equations
• = (μ Set.univ).toNNReal
Instances For
@[simp]
theorem MeasureTheory.coe_measureUnivNNReal {α : Type u_1} {m0 : } (μ : ) :
= μ Set.univ
instance MeasureTheory.isFiniteMeasureZero {α : Type u_1} {m0 : } :
Equations
• =
@[instance 50]
instance MeasureTheory.isFiniteMeasureOfIsEmpty {α : Type u_1} {m0 : } {μ : } [] :
Equations
• =
@[simp]
theorem MeasureTheory.measureUnivNNReal_zero {α : Type u_1} {m0 : } :
instance MeasureTheory.isFiniteMeasureAdd {α : Type u_1} {m0 : } {μ : } {ν : } :
Equations
• =
instance MeasureTheory.isFiniteMeasureSMulNNReal {α : Type u_1} {m0 : } {μ : } {r : NNReal} :
Equations
• =
instance MeasureTheory.IsFiniteMeasure.average {α : Type u_1} {m0 : } {μ : } :
Equations
• =
instance MeasureTheory.isFiniteMeasureSMulOfNNRealTower {α : Type u_1} {m0 : } {μ : } {R : Type u_5} [] [] {r : R} :
Equations
• =
theorem MeasureTheory.isFiniteMeasure_of_le {α : Type u_1} {m0 : } {ν : } (μ : ) (h : ν μ) :
theorem MeasureTheory.Measure.isFiniteMeasure_map {α : Type u_1} {β : Type u_2} [] {m : } (μ : ) (f : αβ) :
@[simp]
theorem MeasureTheory.measureUnivNNReal_eq_zero {α : Type u_1} {m0 : } {μ : } :
μ = 0
theorem MeasureTheory.measureUnivNNReal_pos {α : Type u_1} {m0 : } {μ : } (hμ : μ 0) :
theorem MeasureTheory.Measure.le_of_add_le_add_left {α : Type u_1} {m0 : } {μ : } {ν₁ : } {ν₂ : } (A2 : μ + ν₁ μ + ν₂) :
ν₁ ν₂

le_of_add_le_add_left is normally applicable to OrderedCancelAddCommMonoid, but it holds for measures with the additional assumption that μ is finite.

theorem MeasureTheory.summable_measure_toReal {α : Type u_1} {m0 : } {μ : } [hμ : ] {f : Set α} (hf₁ : ∀ (i : ), MeasurableSet (f i)) (hf₂ : Pairwise (Disjoint on f)) :
Summable fun (x : ) => (μ (f x)).toReal
theorem MeasureTheory.ae_eq_univ_iff_measure_eq {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) :
s =ᵐ[μ] Set.univ μ s = μ Set.univ
theorem MeasureTheory.ae_iff_measure_eq {α : Type u_1} {m0 : } {μ : } {p : αProp} (hp : MeasureTheory.NullMeasurableSet {a : α | p a} μ) :
(∀ᵐ (a : α) ∂μ, p a) μ {a : α | p a} = μ Set.univ
theorem MeasureTheory.ae_mem_iff_measure_eq {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) :
(∀ᵐ (a : α) ∂μ, a s) μ s = μ Set.univ
theorem MeasureTheory.tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint {X : Type u_5} [] {μ : } {Es : Set X} (Es_mble : ∀ (i : ), ) (Es_disj : Pairwise fun (n m : ) => Disjoint (Es n) (Es m)) :
Filter.Tendsto (μ fun (n : ) => ⋃ (i : ), ⋃ (_ : i n), Es i) Filter.atTop (nhds 0)
theorem MeasureTheory.abs_toReal_measure_sub_le_measure_symmDiff' {α : Type u_1} {m0 : } {μ : } {s : Set α} {t : Set α} (hs : ) (ht : ) (hs' : μ s ) (ht' : μ t ) :
|(μ s).toReal - (μ t).toReal| (μ (symmDiff s t)).toReal
theorem MeasureTheory.abs_toReal_measure_sub_le_measure_symmDiff {α : Type u_1} {m0 : } {μ : } {s : Set α} {t : Set α} (hs : ) (ht : ) :
|(μ s).toReal - (μ t).toReal| (μ (symmDiff s t)).toReal
instance MeasureTheory.instIsFiniteMeasureSumMeasure {α : Type u_1} {ι : Type u_4} {m0 : } {s : } {μ : } [∀ (i : ι), ] :
MeasureTheory.IsFiniteMeasure (∑ is, μ i)
Equations
• =
instance MeasureTheory.instIsFiniteMeasureSumOfFinite {α : Type u_1} {ι : Type u_4} {m0 : } [] {μ : } [∀ (i : ι), ] :
Equations
• =
class MeasureTheory.IsZeroOrProbabilityMeasure {α : Type u_1} {m0 : } (μ : ) :

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.

• measure_univ : μ Set.univ = 0 μ Set.univ = 1
Instances
theorem MeasureTheory.IsZeroOrProbabilityMeasure.measure_univ {α : Type u_1} {m0 : } {μ : } [self : ] :
μ Set.univ = 0 μ Set.univ = 1
theorem MeasureTheory.isZeroOrProbabilityMeasure_iff {α : Type u_1} {m0 : } {μ : } :
μ Set.univ = 0 μ Set.univ = 1
theorem MeasureTheory.prob_le_one {α : Type u_1} {m0 : } {μ : } {s : Set α} :
μ s 1
@[simp]
theorem MeasureTheory.one_le_prob_iff {α : Type u_1} {m0 : } {s : Set α} {μ : } :
1 μ s μ s = 1
@[instance 100]
Equations
• =
Equations
• =
class MeasureTheory.IsProbabilityMeasure {α : Type u_1} {m0 : } (μ : ) :

A measure μ is called a probability measure if μ univ = 1.

• measure_univ : μ Set.univ = 1
Instances
@[simp]
theorem MeasureTheory.IsProbabilityMeasure.measure_univ {α : Type u_1} {m0 : } {μ : } [self : ] :
μ Set.univ = 1
theorem MeasureTheory.isProbabilityMeasure_iff {α : Type u_1} {m0 : } {μ : } :
μ Set.univ = 1
@[instance 100]
Equations
• =
theorem MeasureTheory.IsProbabilityMeasure.ne_zero {α : Type u_1} {m0 : } (μ : ) :
μ 0
@[instance 100]
instance MeasureTheory.IsProbabilityMeasure.neZero {α : Type u_1} {m0 : } (μ : ) :
Equations
• =
theorem MeasureTheory.IsProbabilityMeasure.ae_neBot {α : Type u_1} {m0 : } {μ : } :
.NeBot
theorem MeasureTheory.prob_add_prob_compl {α : Type u_1} {m0 : } {μ : } {s : Set α} (h : ) :
μ s + μ s = 1
instance MeasureTheory.isProbabilityMeasureSMul {α : Type u_1} {m0 : } {μ : } [] :
Equations
• =
theorem MeasureTheory.isProbabilityMeasure_map {α : Type u_1} {β : Type u_2} {m0 : } [] {μ : } {f : αβ} (hf : ) :
theorem MeasureTheory.prob_compl_eq_one_sub₀ {α : Type u_1} {m0 : } {μ : } {s : Set α} (h : ) :
μ s = 1 - μ s

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 ℝ.

theorem MeasureTheory.prob_compl_eq_one_sub {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) :
μ s = 1 - μ s

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 ℝ.

@[simp]
theorem MeasureTheory.prob_compl_eq_zero_iff₀ {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) :
μ s = 0 μ s = 1
@[simp]
theorem MeasureTheory.prob_compl_eq_zero_iff {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) :
μ s = 0 μ s = 1
@[simp]
theorem MeasureTheory.prob_compl_eq_one_iff₀ {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) :
μ s = 1 μ s = 0
@[simp]
theorem MeasureTheory.prob_compl_eq_one_iff {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) :
μ s = 1 μ s = 0
theorem MeasureTheory.mem_ae_iff_prob_eq_one₀ {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) :
μ s = 1
theorem MeasureTheory.mem_ae_iff_prob_eq_one {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) :
μ s = 1
theorem MeasureTheory.ae_iff_prob_eq_one {α : Type u_1} {m0 : } {μ : } {p : αProp} (hp : ) :
(∀ᵐ (a : α) ∂μ, p a) μ {a : α | p a} = 1
theorem MeasureTheory.isProbabilityMeasure_comap {α : Type u_1} {β : Type u_2} {m0 : } [] {μ : } {f : βα} (hf : ) (hf' : ∀ᵐ (a : α) ∂μ, a ) (hf'' : ∀ (s : Set β), MeasurableSet (f '' s)) :
theorem MeasurableEmbedding.isProbabilityMeasure_comap {α : Type u_1} {β : Type u_2} {m0 : } [] {μ : } {f : βα} (hf : ) (hf' : ∀ᵐ (a : α) ∂μ, a ) :
instance MeasureTheory.isProbabilityMeasure_map_up {α : Type u_1} {m0 : } {μ : } :
Equations
• =
instance MeasureTheory.isProbabilityMeasure_comap_down {α : Type u_1} {m0 : } {μ : } :
Equations
• =
Equations
• =
theorem MeasureTheory.eq_zero_or_isProbabilityMeasure {α : Type u_1} {m0 : } (μ : ) :
instance MeasureTheory.instIsZeroOrProbabilityMeasureMap {α : Type u_1} {β : Type u_2} {m0 : } [] {μ : } {f : αβ} :
Equations
• =
theorem MeasureTheory.prob_compl_lt_one_sub_of_lt_prob {α : Type u_1} {m0 : } {μ : } {s : Set α} {p : ENNReal} (hμs : p < μ s) (s_mble : ) :
μ s < 1 - p
theorem MeasureTheory.prob_compl_le_one_sub_of_le_prob {α : Type u_1} {m0 : } {μ : } {s : Set α} {p : ENNReal} (hμs : p μ s) (s_mble : ) :
μ s 1 - p
class MeasureTheory.NoAtoms {α : Type u_1} {m0 : } (μ : ) :

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
@[simp]
theorem MeasureTheory.NoAtoms.measure_singleton {α : Type u_1} {m0 : } {μ : } [self : ] (x : α) :
μ {x} = 0
theorem Set.Subsingleton.measure_zero {α : Type u_1} {m0 : } {s : Set α} (hs : s.Subsingleton) (μ : ) :
μ s = 0
theorem MeasureTheory.Measure.restrict_singleton' {α : Type u_1} {m0 : } {μ : } {a : α} :
μ.restrict {a} = 0
instance MeasureTheory.Measure.restrict.instNoAtoms {α : Type u_1} {m0 : } {μ : } (s : Set α) :
MeasureTheory.NoAtoms (μ.restrict s)
Equations
• =
theorem Set.Countable.measure_zero {α : Type u_1} {m0 : } {s : Set α} (h : s.Countable) (μ : ) :
μ s = 0
theorem Set.Countable.ae_not_mem {α : Type u_1} {m0 : } {s : Set α} (h : s.Countable) (μ : ) :
∀ᵐ (x : α) ∂μ, xs
theorem Set.Countable.measure_restrict_compl {α : Type u_1} {m0 : } {s : Set α} (h : s.Countable) (μ : ) :
μ.restrict s = μ
@[simp]
theorem MeasureTheory.restrict_compl_singleton {α : Type u_1} {m0 : } {μ : } (a : α) :
μ.restrict {a} = μ
theorem Set.Finite.measure_zero {α : Type u_1} {m0 : } {s : Set α} (h : s.Finite) (μ : ) :
μ s = 0
theorem Finset.measure_zero {α : Type u_1} {m0 : } (s : ) (μ : ) :
μ s = 0
theorem MeasureTheory.insert_ae_eq_self {α : Type u_1} {m0 : } {μ : } (a : α) (s : Set α) :
insert a s =ᵐ[μ] s
theorem MeasureTheory.Iio_ae_eq_Iic {α : Type u_1} {m0 : } {μ : } [] {a : α} :
=ᵐ[μ]
theorem MeasureTheory.Ioi_ae_eq_Ici {α : Type u_1} {m0 : } {μ : } [] {a : α} :
=ᵐ[μ]
theorem MeasureTheory.Ioo_ae_eq_Ioc {α : Type u_1} {m0 : } {μ : } [] {a : α} {b : α} :
theorem MeasureTheory.Ioc_ae_eq_Icc {α : Type u_1} {m0 : } {μ : } [] {a : α} {b : α} :
theorem MeasureTheory.Ioo_ae_eq_Ico {α : Type u_1} {m0 : } {μ : } [] {a : α} {b : α} :
theorem MeasureTheory.Ioo_ae_eq_Icc {α : Type u_1} {m0 : } {μ : } [] {a : α} {b : α} :
theorem MeasureTheory.Ico_ae_eq_Icc {α : Type u_1} {m0 : } {μ : } [] {a : α} {b : α} :
theorem MeasureTheory.Ico_ae_eq_Ioc {α : Type u_1} {m0 : } {μ : } [] {a : α} {b : α} :
theorem MeasureTheory.restrict_Iio_eq_restrict_Iic {α : Type u_1} {m0 : } {μ : } [] {a : α} :
μ.restrict (Set.Iio a) = μ.restrict (Set.Iic a)
theorem MeasureTheory.restrict_Ioi_eq_restrict_Ici {α : Type u_1} {m0 : } {μ : } [] {a : α} :
μ.restrict (Set.Ioi a) = μ.restrict (Set.Ici a)
theorem MeasureTheory.restrict_Ioo_eq_restrict_Ioc {α : Type u_1} {m0 : } {μ : } [] {a : α} {b : α} :
μ.restrict (Set.Ioo a b) = μ.restrict (Set.Ioc a b)
theorem MeasureTheory.restrict_Ioc_eq_restrict_Icc {α : Type u_1} {m0 : } {μ : } [] {a : α} {b : α} :
μ.restrict (Set.Ioc a b) = μ.restrict (Set.Icc a b)
theorem MeasureTheory.restrict_Ioo_eq_restrict_Ico {α : Type u_1} {m0 : } {μ : } [] {a : α} {b : α} :
μ.restrict (Set.Ioo a b) = μ.restrict (Set.Ico a b)
theorem MeasureTheory.restrict_Ioo_eq_restrict_Icc {α : Type u_1} {m0 : } {μ : } [] {a : α} {b : α} :
μ.restrict (Set.Ioo a b) = μ.restrict (Set.Icc a b)
theorem MeasureTheory.restrict_Ico_eq_restrict_Icc {α : Type u_1} {m0 : } {μ : } [] {a : α} {b : α} :
μ.restrict (Set.Ico a b) = μ.restrict (Set.Icc a b)
theorem MeasureTheory.restrict_Ico_eq_restrict_Ioc {α : Type u_1} {m0 : } {μ : } [] {a : α} {b : α} :
μ.restrict (Set.Ico a b) = μ.restrict (Set.Ioc a b)
theorem MeasureTheory.uIoc_ae_eq_interval {α : Type u_1} {m0 : } {μ : } [] {a : α} {b : α} :
Ι a b =ᵐ[μ] Set.uIcc a b
theorem MeasureTheory.ite_ae_eq_of_measure_zero {α : Type u_1} {m0 : } {μ : } {γ : Type u_5} (f : αγ) (g : αγ) (s : Set α) [DecidablePred fun (x : α) => x s] (hs_zero : μ s = 0) :
(fun (x : α) => if x s then f x else g x) =ᵐ[μ] g
theorem MeasureTheory.ite_ae_eq_of_measure_compl_zero {α : Type u_1} {m0 : } {μ : } {γ : Type u_5} (f : αγ) (g : αγ) (s : Set α) [DecidablePred fun (x : α) => x s] (hs_zero : μ s = 0) :
(fun (x : α) => if x s then f x else g x) =ᵐ[μ] f
def MeasureTheory.Measure.FiniteAtFilter {α : Type u_1} {_m0 : } (μ : ) (f : ) :

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 = sf, μ s <
Instances For
theorem MeasureTheory.Measure.finiteAtFilter_of_finite {α : Type u_1} {_m0 : } (μ : ) (f : ) :
μ.FiniteAtFilter f
theorem MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis {α : Type u_1} {ι : Type u_4} {m0 : } {μ : } {f : } (hμ : μ.FiniteAtFilter f) {p : ιProp} {s : ιSet α} (hf : f.HasBasis p s) :
∃ (i : ι), p i μ (s i) <
theorem MeasureTheory.Measure.finiteAtBot {α : Type u_1} {m0 : } (μ : ) :
μ.FiniteAtFilter
structure MeasureTheory.Measure.FiniteSpanningSetsIn {α : Type u_1} {m0 : } (μ : ) (C : Set (Set α)) :
Type u_1

μ 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.

• set : Set α
• set_mem : ∀ (i : ), self.set i C
• finite : ∀ (i : ), μ (self.set i) <
• spanning : ⋃ (i : ), self.set i = Set.univ
Instances For
theorem MeasureTheory.Measure.FiniteSpanningSetsIn.set_mem {α : Type u_1} {m0 : } {μ : } {C : Set (Set α)} (self : μ.FiniteSpanningSetsIn C) (i : ) :
self.set i C
theorem MeasureTheory.Measure.FiniteSpanningSetsIn.finite {α : Type u_1} {m0 : } {μ : } {C : Set (Set α)} (self : μ.FiniteSpanningSetsIn C) (i : ) :
μ (self.set i) <
theorem MeasureTheory.Measure.FiniteSpanningSetsIn.spanning {α : Type u_1} {m0 : } {μ : } {C : Set (Set α)} (self : μ.FiniteSpanningSetsIn C) :
⋃ (i : ), self.set i = Set.univ
class MeasureTheory.SFinite {α : Type u_1} {m0 : } (μ : ) :

A measure is called s-finite if it is a countable sum of finite measures.

• out' : ∃ (m : ), (∀ (n : ), )
Instances
theorem MeasureTheory.SFinite.out' {α : Type u_1} {m0 : } {μ : } [self : ] :
∃ (m : ), (∀ (n : ), )
noncomputable def MeasureTheory.sFiniteSeq {α : Type u_1} {m0 : } (μ : ) [h : ] :

A sequence of finite measures such that μ = sum (sFiniteSeq μ) (see sum_sFiniteSeq).

Equations
• = .choose
Instances For
instance MeasureTheory.isFiniteMeasure_sFiniteSeq {α : Type u_1} {m0 : } {μ : } [h : ] (n : ) :
Equations
• =
theorem MeasureTheory.sum_sFiniteSeq {α : Type u_1} {m0 : } (μ : ) [h : ] :
instance MeasureTheory.instSFiniteOfNatMeasure {α : Type u_1} {m0 : } :
Equations
• =
@[simp]
theorem MeasureTheory.sFiniteSeq_zero {α : Type u_1} {m0 : } (n : ) :
theorem MeasureTheory.sfinite_sum_of_countable {α : Type u_1} {ι : Type u_4} {m0 : } [] (m : ) [∀ (n : ι), ] :

A countable sum of finite measures is s-finite. This lemma is superseded by the instance below.

instance MeasureTheory.instSFiniteSumOfCountable {α : Type u_1} {ι : Type u_4} {m0 : } [] (m : ) [∀ (n : ι), ] :
Equations
• =
instance MeasureTheory.instSFiniteHAddMeasure {α : Type u_1} {m0 : } {μ : } {ν : } :
Equations
• =
instance MeasureTheory.instSFiniteRestrict {α : Type u_1} {m0 : } {μ : } (s : Set α) :
MeasureTheory.SFinite (μ.restrict s)
Equations
• =
theorem MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous {α : Type u_1} {m0 : } (μ : ) :
∃ (ν : ), μ.AbsolutelyContinuous ν ν.AbsolutelyContinuous μ

For an s-finite measure μ, there exists a finite measure ν such that each of μ and ν is absolutely continuous with respect to the other.

@[deprecated MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous]
theorem MeasureTheory.exists_absolutelyContinuous_isFiniteMeasure {α : Type u_1} {m0 : } (μ : ) :
∃ (ν : ), μ.AbsolutelyContinuous ν
class MeasureTheory.SigmaFinite {α : Type u_1} {m0 : } (μ : ) :

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
theorem MeasureTheory.SigmaFinite.out' {α : Type u_1} {m0 : } {μ : } [self : ] :
Nonempty (μ.FiniteSpanningSetsIn Set.univ)
theorem MeasureTheory.sigmaFinite_iff {α : Type u_1} {m0 : } {μ : } :
Nonempty (μ.FiniteSpanningSetsIn Set.univ)
theorem MeasureTheory.SigmaFinite.out {α : Type u_1} {m0 : } {μ : } (h : ) :
Nonempty (μ.FiniteSpanningSetsIn Set.univ)
def MeasureTheory.Measure.toFiniteSpanningSetsIn {α : Type u_1} {m0 : } (μ : ) [h : ] :
μ.FiniteSpanningSetsIn {s : Set α | }

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
def MeasureTheory.spanningSets {α : Type u_1} {m0 : } (μ : ) (i : ) :
Set α

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
theorem MeasureTheory.monotone_spanningSets {α : Type u_1} {m0 : } (μ : ) :
theorem MeasureTheory.measurable_spanningSets {α : Type u_1} {m0 : } (μ : ) (i : ) :
theorem MeasureTheory.measure_spanningSets_lt_top {α : Type u_1} {m0 : } (μ : ) (i : ) :
μ <
theorem MeasureTheory.iUnion_spanningSets {α : Type u_1} {m0 : } (μ : ) :
⋃ (i : ), = Set.univ
theorem MeasureTheory.isCountablySpanning_spanningSets {α : Type u_1} {m0 : } (μ : ) :
noncomputable def MeasureTheory.spanningSetsIndex {α : Type u_1} {m0 : } (μ : ) (x : α) :

spanningSetsIndex μ x is the least n : ℕ such that x ∈ spanningSets μ n.

Equations
Instances For
theorem MeasureTheory.measurable_spanningSetsIndex {α : Type u_1} {m0 : } (μ : ) :
theorem MeasureTheory.preimage_spanningSetsIndex_singleton {α : Type u_1} {m0 : } (μ : ) (n : ) :
theorem MeasureTheory.spanningSetsIndex_eq_iff {α : Type u_1} {m0 : } (μ : ) {x : α} {n : } :
theorem MeasureTheory.mem_disjointed_spanningSetsIndex {α : Type u_1} {m0 : } (μ : ) (x : α) :
theorem MeasureTheory.mem_spanningSetsIndex {α : Type u_1} {m0 : } (μ : ) (x : α) :
theorem MeasureTheory.mem_spanningSets_of_index_le {α : Type u_1} {m0 : } (μ : ) (x : α) {n : } (hn : ) :
theorem MeasureTheory.eventually_mem_spanningSets {α : Type u_1} {m0 : } (μ : ) (x : α) :
∀ᶠ (n : ) in Filter.atTop,
theorem MeasureTheory.sum_restrict_disjointed_spanningSets {α : Type u_1} {m0 : } (μ : ) (ν : ) :
(MeasureTheory.Measure.sum fun (n : ) => μ.restrict ) = μ
@[instance 100]
instance MeasureTheory.instSFiniteOfSigmaFinite {α : Type u_1} {m0 : } {μ : } :
Equations
• =
theorem MeasureTheory.Measure.forall_measure_inter_spanningSets_eq_zero {α : Type u_1} [] {μ : } (s : Set α) :
(∀ (n : ), μ (s ) = 0) μ s = 0

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.

theorem MeasureTheory.Measure.exists_measure_inter_spanningSets_pos {α : Type u_1} [] {μ : } (s : Set α) :
(∃ (n : ), 0 < μ (s )) 0 < μ s

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.

theorem MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀ {α : Type u_1} {ι : Type u_5} [] (μ : ) {ε : ENNReal} (ε_pos : 0 < ε) {As : ιSet α} (As_mble : ∀ (i : ι), ) (As_disj : ) (Union_As_finite : μ (⋃ (i : ι), As i) ) :
{i : ι | ε μ (As i)}.Finite

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.

theorem MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion {α : Type u_1} {ι : Type u_5} [] (μ : ) {ε : ENNReal} (ε_pos : 0 < ε) {As : ιSet α} (As_mble : ∀ (i : ι), MeasurableSet (As i)) (As_disj : Pairwise (Disjoint on As)) (Union_As_finite : μ (⋃ (i : ι), As i) ) :
{i : ι | ε μ (As i)}.Finite

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.

theorem Set.Infinite.meas_eq_top {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : s.Infinite) (h' : ∃ (ε : ENNReal), ε 0 xs, ε μ {x}) :
μ s =

If all elements of an infinite set have measure uniformly separated from zero, then the set has infinite measure.

theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ {α : Type u_1} {ι : Type u_5} :
∀ {x : } (μ : ) {As : ιSet α}, (∀ (i : ι), )μ (⋃ (i : ι), As i) {i : ι | 0 < μ (As i)}.Countable

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.

theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top {α : Type u_1} {ι : Type u_5} :
∀ {x : } (μ : ) {As : ιSet α}, (∀ (i : ι), MeasurableSet (As i))Pairwise (Disjoint on As)μ (⋃ (i : ι), As i) {i : ι | 0 < μ (As i)}.Countable

If the union of disjoint measurable sets has finite measure, then there are only countably many members of the union whose measure is positive.

theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion₀ {α : Type u_1} {ι : Type u_5} :
∀ {x : } {μ : } [inst : ] {As : ιSet α}, (∀ (i : ι), ){i : ι | 0 < μ (As i)}.Countable

In an s-finite space, among disjoint null-measurable sets, only countably many can have positive measure.

theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion {α : Type u_1} {ι : Type u_5} :
∀ {x : } {μ : } [inst : ] {As : ιSet α}, (∀ (i : ι), MeasurableSet (As i))Pairwise (Disjoint on As){i : ι | 0 < μ (As i)}.Countable

In an s-finite space, among disjoint measurable sets, only countably many can have positive measure.

theorem MeasureTheory.Measure.countable_meas_level_set_pos₀ {α : Type u_5} {β : Type u_6} :
∀ {x : } {μ : } [inst : ] [inst : ] [inst_1 : ] {g : αβ}, {t : β | 0 < μ {a : α | g a = t}}.Countable
theorem MeasureTheory.Measure.countable_meas_level_set_pos {α : Type u_5} {β : Type u_6} :
∀ {x : } {μ : } [inst : ] [inst : ] [inst_1 : ] {g : αβ}, {t : β | 0 < μ {a : α | g a = t}}.Countable
theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sum {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) {t : Set α} {m : } (hv : ∀ (n : ), (m n) t ) (hμ : ) :
μ ( s) = μ (t s)

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).

theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_cover {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) {t : Set α} {v : Set α} (hv : t ⋃ (n : ), v n) (h'v : ∀ (n : ), μ (t v n) ) :
μ ( 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).

theorem MeasureTheory.Measure.restrict_toMeasurable_of_cover {α : Type u_1} {m0 : } {μ : } {s : Set α} {v : Set α} (hv : s ⋃ (n : ), v n) (h'v : ∀ (n : ), μ (s v n) ) :
μ.restrict = μ.restrict s
theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) (t : Set α) :
μ ( 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.

@[simp]
theorem MeasureTheory.Measure.restrict_toMeasurable_of_sFinite {α : Type u_1} {m0 : } {μ : } (s : Set α) :
μ.restrict = μ.restrict s
theorem MeasureTheory.Measure.iSup_restrict_spanningSets_of_measurableSet {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) :
⨆ (i : ), (μ.restrict ) s = μ s

Auxiliary lemma for iSup_restrict_spanningSets.

theorem MeasureTheory.Measure.iSup_restrict_spanningSets {α : Type u_1} {m0 : } {μ : } (s : Set α) :
⨆ (i : ), (μ.restrict ) s = μ s
theorem MeasureTheory.Measure.exists_subset_measure_lt_top {α : Type u_1} {m0 : } {μ : } {s : Set α} {r : ENNReal} (hs : ) (h's : r < μ s) :
∃ (t : Set α), t s r < μ t μ t <

In a σ-finite space, any measurable set of measure > r contains a measurable subset of finite measure > r.

def MeasureTheory.Measure.FiniteSpanningSetsIn.mono' {α : Type u_1} {m0 : } {μ : } {C : Set (Set α)} {D : Set (Set α)} (h : μ.FiniteSpanningSetsIn C) (hC : C {s : Set α | μ s < } D) :
μ.FiniteSpanningSetsIn D

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
def MeasureTheory.Measure.FiniteSpanningSetsIn.mono {α : Type u_1} {m0 : } {μ : } {C : Set (Set α)} {D : Set (Set α)} (h : μ.FiniteSpanningSetsIn C) (hC : C D) :
μ.FiniteSpanningSetsIn D

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
theorem MeasureTheory.Measure.FiniteSpanningSetsIn.sigmaFinite {α : Type u_1} {m0 : } {μ : } {C : Set (Set α)} (h : μ.FiniteSpanningSetsIn C) :

If μ has finite spanning sets in the collection of measurable sets C, then μ is σ-finite.

theorem MeasureTheory.Measure.FiniteSpanningSetsIn.ext {α : Type u_1} {m0 : } {μ : } {ν : } {C : Set (Set α)} (hA : ) (hC : ) (h : μ.FiniteSpanningSetsIn C) (h_eq : sC, μ s = ν s) :
μ = ν

An extensionality for measures. It is ext_of_generateFrom_of_iUnion formulated in terms of FiniteSpanningSetsIn.

theorem MeasureTheory.Measure.FiniteSpanningSetsIn.isCountablySpanning {α : Type u_1} {m0 : } {μ : } {C : Set (Set α)} (h : μ.FiniteSpanningSetsIn C) :
theorem MeasureTheory.Measure.sigmaFinite_of_countable {α : Type u_1} {m0 : } {μ : } {S : Set (Set α)} (hc : S.Countable) (hμ : sS, μ s < ) (hU : ⋃₀ S = Set.univ) :
def MeasureTheory.Measure.FiniteSpanningSetsIn.ofLE {α : Type u_1} {m0 : } {μ : } {ν : } (h : ν μ) {C : Set (Set α)} (S : μ.FiniteSpanningSetsIn C) :
ν.FiniteSpanningSetsIn C

Given measures μ, ν where ν ≤ μ, FiniteSpanningSetsIn.ofLe provides the induced FiniteSpanningSet with respect to ν from a FiniteSpanningSet with respect to μ.

Equations
• = { set := S.set, set_mem := , finite := , spanning := }
Instances For
theorem MeasureTheory.Measure.sigmaFinite_of_le {α : Type u_1} {m0 : } {ν : } (μ : ) [hs : ] (h : ν μ) :
@[simp]
theorem MeasureTheory.Measure.add_right_inj {α : Type u_1} {m0 : } (μ : ) (ν₁ : ) (ν₂ : ) :
μ + ν₁ = μ + ν₂ ν₁ = ν₂
@[simp]
theorem MeasureTheory.Measure.add_left_inj {α : Type u_1} {m0 : } (μ : ) (ν₁ : ) (ν₂ : ) :
ν₁ + μ = ν₂ + μ ν₁ = ν₂
@[instance 100]
instance MeasureTheory.IsFiniteMeasure.toSigmaFinite {α : Type u_1} {_m0 : } (μ : ) :

Every finite measure is σ-finite.

Equations
• =
theorem MeasureTheory.sigmaFinite_bot_iff {α : Type u_1} (μ : ) :
instance MeasureTheory.Restrict.sigmaFinite {α : Type u_1} {m0 : } (μ : ) (s : Set α) :
Equations
• =
instance MeasureTheory.sum.sigmaFinite {α : Type u_1} {m0 : } {ι : Type u_5} [] (μ : ) [∀ (i : ι), ] :
Equations
• =
instance MeasureTheory.Add.sigmaFinite {α : Type u_1} {m0 : } (μ : ) (ν : ) :
Equations
• =
instance MeasureTheory.SMul.sigmaFinite {α : Type u_1} {m0 : } {μ : } (c : NNReal) :
Equations
• =
instance MeasureTheory.instSigmaFiniteRestrictUnionSet {α : Type u_1} {m0 : } {μ : } {s : Set α} {t : Set α} [MeasureTheory.SigmaFinite (μ.restrict s)] [MeasureTheory.SigmaFinite (μ.restrict t)] :
MeasureTheory.SigmaFinite (μ.restrict (s t))
Equations
• =
instance MeasureTheory.instSigmaFiniteRestrictInterSet {α : Type u_1} {m0 : } {μ : } {s : Set α} {t : Set α} [MeasureTheory.SigmaFinite (μ.restrict s)] :
MeasureTheory.SigmaFinite (μ.restrict (s t))
Equations
• =
instance MeasureTheory.instSigmaFiniteRestrictInterSet_1 {α : Type u_1} {m0 : } {μ : } {s : Set α} {t : Set α} [MeasureTheory.SigmaFinite (μ.restrict t)] :
MeasureTheory.SigmaFinite (μ.restrict (s t))
Equations
• =
theorem MeasureTheory.SigmaFinite.of_map {α : Type u_1} {β : Type u_2} {m0 : } [] (μ : ) {f : αβ} (hf : ) :
theorem MeasurableEmbedding.sigmaFinite_map {α : Type u_1} {β : Type u_2} {m0 : } [] {μ : } {f : αβ} (hf : ) :
theorem MeasurableEquiv.sigmaFinite_map {α : Type u_1} {β : Type u_2} {m0 : } [] {μ : } (f : α ≃ᵐ β) :
theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict' {α : Type u_1} {m0 : } {μ : } (ν : ) (P : αProp) (h : ∀ (s : Set α), μ s < ν s < ∀ᵐ (x : α) ∂μ.restrict s, P x) :
∀ᵐ (x : α) ∂μ, P x

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.

theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict {α : Type u_1} {m0 : } {μ : } (P : αProp) (h : ∀ (s : Set α), μ s < ∀ᵐ (x : α) ∂μ.restrict s, P x) :
∀ᵐ (x : α) ∂μ, P x

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.

class MeasureTheory.IsLocallyFiniteMeasure {α : Type u_1} {m0 : } [] (μ : ) :

A measure is called locally finite if it is finite in some neighborhood of each point.

• finiteAtNhds : ∀ (x : α), μ.FiniteAtFilter (nhds x)
Instances
theorem MeasureTheory.IsLocallyFiniteMeasure.finiteAtNhds {α : Type u_1} {m0 : } [] {μ : } [self : ] (x : α) :
μ.FiniteAtFilter (nhds x)
@[instance 100]
instance MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure {α : Type u_1} {m0 : } [] (μ : ) :
Equations
• =
theorem MeasureTheory.Measure.finiteAt_nhds {α : Type u_1} {m0 : } [] (μ : ) (x : α) :
μ.FiniteAtFilter (nhds x)
theorem MeasureTheory.Measure.smul_finite {α : Type u_1} {m0 : } (μ : ) {c : ENNReal} (hc : c ) :
theorem MeasureTheory.Measure.exists_isOpen_measure_lt_top {α : Type u_1} {m0 : } [] (μ : ) (x : α) :
∃ (s : Set α), x s μ s <
instance MeasureTheory.isLocallyFiniteMeasureSMulNNReal {α : Type u_1} {m0 : } [] (μ : ) (c : NNReal) :
Equations
• =
class MeasureTheory.IsFiniteMeasureOnCompacts {α : Type u_1} {m0 : } [] (μ : ) :

A measure μ is finite on compacts if any compact set K satisfies μ K < ∞.

• lt_top_of_isCompact : ∀ ⦃K : Set α⦄, μ K <
Instances
theorem MeasureTheory.IsFiniteMeasureOnCompacts.lt_top_of_isCompact {α : Type u_1} {m0 : } [] {μ : } [self : ] ⦃K : Set α :
μ K <
theorem IsCompact.measure_lt_top {α : Type u_1} {m0 : } [] {μ : } ⦃K : Set α (hK : ) :
μ K <

A compact subset has finite measure for a measure which is finite on compacts.

theorem IsCompact.measure_ne_top {α : Type u_1} {m0 : } [] {μ : } ⦃K : Set α (hK : ) :
μ K

A compact subset has finite measure for a measure which is finite on compacts.

theorem Bornology.IsBounded.measure_lt_top {α : Type u_1} {m0 : } [] {μ : } ⦃s : Set α (hs : ) :
μ s <

A bounded subset has finite measure for a measure which is finite on compact sets, in a proper space.

theorem MeasureTheory.measure_closedBall_lt_top {α : Type u_1} {m0 : } [] {μ : } {x : α} {r : } :
μ <
theorem MeasureTheory.measure_ball_lt_top {α : Type u_1} {m0 : } [] {μ : } {x : α} {r : } :
μ (Metric.ball x r) <
theorem MeasureTheory.IsFiniteMeasureOnCompacts.smul {α : Type u_1} {m0 : } [] (μ : ) {c : ENNReal} (hc : c ) :
instance MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal {α : Type u_1} {m0 : } [] (μ : ) (c : NNReal) :
Equations
• =
instance MeasureTheory.instIsFiniteMeasureOnCompactsRestrict {α : Type u_1} {m0 : } [] {μ : } {s : Set α} :
Equations
• =
@[instance 100]
instance MeasureTheory.CompactSpace.isFiniteMeasure {α : Type u_1} {m0 : } {μ : } [] [] :
Equations
• =
@[instance 100]
instance MeasureTheory.SigmaFinite.of_isFiniteMeasureOnCompacts {α : Type u_1} {m0 : } [] (μ : ) :
Equations
• =
@[instance 100]
instance MeasureTheory.sigmaFinite_of_locallyFinite {α : Type u_1} {m0 : } {μ : } [] :
Equations
• =
@[instance 100]

A measure which is finite on compact sets in a locally compact space is locally finite.

Equations
• =
theorem MeasureTheory.exists_pos_measure_of_cover {α : Type u_1} {ι : Type u_4} {m0 : } {μ : } [] {U : ιSet α} (hU : ⋃ (i : ι), U i = Set.univ) (hμ : μ 0) :
∃ (i : ι), 0 < μ (U i)
theorem MeasureTheory.exists_pos_preimage_ball {α : Type u_1} {δ : Type u_3} {m0 : } {μ : } (f : αδ) (x : δ) (hμ : μ 0) :
∃ (n : ), 0 < μ (f ⁻¹' Metric.ball x n)
theorem MeasureTheory.exists_pos_ball {α : Type u_1} {m0 : } {μ : } (x : α) (hμ : μ 0) :
∃ (n : ), 0 < μ (Metric.ball x n)
@[deprecated MeasureTheory.measure_null_of_locally_null]
theorem MeasureTheory.null_of_locally_null {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] {μ : F} [] (s : Set α) (hs : xs, u, μ u = 0) :
μ s = 0

If a set has zero measure in a neighborhood of each of its points, then it has zero measure in a second-countable space.

theorem MeasureTheory.exists_ne_forall_mem_nhds_pos_measure_preimage {α : Type u_1} {m0 : } {μ : } {β : Type u_5} [] [] [] {f : αβ} (h : ∀ (b : β), ∃ᵐ (x : α) ∂μ, f x b) :
∃ (a : β) (b : β), a b (∀ snhds a, 0 < μ (f ⁻¹' s)) tnhds b, 0 < μ (f ⁻¹' t)
theorem MeasureTheory.ext_on_measurableSpace_of_generate_finite {α : Type u_5} (m₀ : ) {μ : } {ν : } (C : Set (Set α)) (hμν : sC, μ s = ν s) {m : } (h : m m₀) (hA : ) (hC : ) (h_univ : μ Set.univ = ν Set.univ) {s : Set α} (hs : ) :
μ s = ν s

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.

theorem MeasureTheory.ext_of_generate_finite {α : Type u_1} {m0 : } {μ : } {ν : } (C : Set (Set α)) (hA : ) (hC : ) (hμν : sC, μ s = ν s) (h_univ : μ Set.univ = ν Set.univ) :
μ = ν

Two finite measures are equal if they are equal on the π-system generating the σ-algebra (and univ).

def MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed {α : Type u_1} {m0 : } {μ : } (S : μ.FiniteSpanningSetsIn {s : Set α | }) :
μ.FiniteSpanningSetsIn {s : Set α | }

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
theorem MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq {α : Type u_1} {m0 : } {μ : } (S : μ.FiniteSpanningSetsIn {s : Set α | }) :
S.disjointed.set = disjointed S.set
theorem MeasureTheory.Measure.exists_eq_disjoint_finiteSpanningSetsIn {α : Type u_1} {m0 : } (μ : ) (ν : ) :
∃ (S : μ.FiniteSpanningSetsIn {s : Set α | }) (T : ν.FiniteSpanningSetsIn {s : Set α | }), S.set = T.set Pairwise (Disjoint on S.set)
theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono {α : Type u_1} {m0 : } {μ : } {f : } {g : } (h : f g) :
μ.FiniteAtFilter gμ.FiniteAtFilter f
theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_left {α : Type u_1} {m0 : } {μ : } {f : } {g : } (h : μ.FiniteAtFilter f) :
μ.FiniteAtFilter (f g)
theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_right {α : Type u_1} {m0 : } {μ : } {f : } {g : } (h : μ.FiniteAtFilter g) :
μ.FiniteAtFilter (f g)
@[simp]
theorem MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff {α : Type u_1} {m0 : } {μ : } {f : } :
μ.FiniteAtFilter (f ) μ.FiniteAtFilter f
theorem MeasureTheory.Measure.FiniteAtFilter.of_inf_ae {α : Type u_1} {m0 : } {μ : } {f : } :
μ.FiniteAtFilter (f )μ.FiniteAtFilter f

Alias of the forward direction of MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff.

theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono_ae {α : Type u_1} {m0 : } {μ : } {f : } {g : } (h : g) (hg : μ.FiniteAtFilter g) :
μ.FiniteAtFilter f
theorem MeasureTheory.Measure.FiniteAtFilter.measure_mono {α : Type u_1} {m0 : } {μ : } {ν : } {f : } (h : μ ν) :
ν.FiniteAtFilter fμ.FiniteAtFilter f
theorem MeasureTheory.Measure.FiniteAtFilter.mono {α : Type u_1} {m0 : } {μ : } {ν : } {f : } {g : } (hf : f g) (hμ : μ ν) :
ν.FiniteAtFilter gμ.FiniteAtFilter f
theorem MeasureTheory.Measure.FiniteAtFilter.eventually {α : Type u_1} {m0 : } {μ : } {f : } (h : μ.FiniteAtFilter f) :
∀ᶠ (s : Set α) in f.smallSets, μ s <
theorem MeasureTheory.Measure.FiniteAtFilter.filterSup {α : Type u_1} {m0 : } {μ : } {f : } {g : } :
μ.FiniteAtFilter fμ.FiniteAtFilter gμ.FiniteAtFilter (f g)
theorem MeasureTheory.Measure.finiteAt_nhdsWithin {α : Type u_1} [] {_m0 : } (μ : ) (x : α) (s : Set α) :
μ.FiniteAtFilter (nhdsWithin x s)
@[simp]
theorem MeasureTheory.Measure.finiteAt_principal {α : Type u_1} {m0 : } {μ : } {s : Set α} :
μ.FiniteAtFilter μ s <
theorem MeasureTheory.Measure.isLocallyFiniteMeasure_of_le {α : Type u_1} [] {_m : } {μ : } {ν : } (h : ν μ) :
theorem IsCompact.exists_open_superset_measure_lt_top' {α : Type u_1} [] [] {μ : } {s : Set α} (h : ) (hμ : xs, μ.FiniteAtFilter (nhds x)) :
Us, μ U <

If s is a compact set and μ is finite at 𝓝 x for every x ∈ s, then s admits an open superset of finite measure.

theorem IsCompact.exists_open_superset_measure_lt_top {α : Type u_1} [] [] {s : Set α} (h : ) (μ : ) :
Us, μ U <

If s is a compact set and μ is a locally finite measure, then s admits an open superset of finite measure.

theorem IsCompact.measure_lt_top_of_nhdsWithin {α : Type u_1} [] [] {μ : } {s : Set α} (h : ) (hμ : xs, μ.FiniteAtFilter (nhdsWithin x s)) :
μ s <
theorem IsCompact.measure_zero_of_nhdsWithin {α : Type u_1} [] [] {μ : } {s : Set α} (hs : ) :
(∀ as, t, μ t = 0)μ s = 0
@[instance 100]
instance isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure {α : Type u_1} [] :
∀ {x : } {μ : } [inst : ],
Equations
• =
def MeasureTheory.Measure.finiteSpanningSetsInCompact {α : Type u_1} [] :
{x : } → (μ : ) → [inst : ] → μ.FiniteSpanningSetsIn {K : Set α | }

Compact covering of a σ-compact topological space as MeasureTheory.Measure.FiniteSpanningSetsIn.

Equations
• μ.finiteSpanningSetsInCompact = { set := , set_mem := , finite := , spanning := }
Instances For
def MeasureTheory.Measure.finiteSpanningSetsInOpen {α : Type u_1} [] :
{x : } → (μ : ) → [inst : ] → μ.FiniteSpanningSetsIn {K : Set α | }

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
theorem MeasureTheory.Measure.finiteSpanningSetsInOpen'_def {α : Type u_5} [] {m : } (μ : ) :
μ.finiteSpanningSetsInOpen' = let_fun H := ; H.some
@[irreducible]
noncomputable def MeasureTheory.Measure.finiteSpanningSetsInOpen' {α : Type u_5} [] {m : } (μ : ) :
μ.FiniteSpanningSetsIn {K : Set α | }

A locally finite measure on a second countable topological space admits a finite spanning sequence of open sets.

Equations
Instances For
theorem measure_Icc_lt_top {α : Type u_1} [] [] [] {m : } {μ : } {a : α} {b : α} :
μ (Set.Icc a b) <
theorem measure_Ico_lt_top {α : Type u_1} [] [] [] {m : } {μ : } {a : α} {b : α} :
μ (Set.Ico a b) <
theorem measure_Ioc_lt_top {α : Type u_1} [] [] [] {m : } {μ : } {a : α} {b : α} :
μ (Set.Ioc a b) <
theorem measure_Ioo_lt_top {α : Type u_1} [] [] [] {m : } {μ : } {a : α} {b : α} :
μ (Set.Ioo a b) <