Classes of measures

We introduce the following typeclasses for measures:

• IsProbabilityMeasure μ: μ univ = 1;
• IsFiniteMeasure μ: μ univ < ∞;
• 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 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : Prop

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

• measure_univ_lt_top : ↑↑μ Set.univ < ⊤

theorem MeasureTheory.not_isFiniteMeasure_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : ¬MeasureTheory.IsFiniteMeasure μ ↔ ↑↑μ Set.univ = ⊤

instance MeasureTheory.Restrict.isFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (μ : MeasureTheory.Measure α) [hs : Fact (↑↑μ s < ⊤)] : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.restrict μ s)

Equations

• ⋯ = ⋯

theorem MeasureTheory.measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (s : Set α) : ↑↑μ s < ⊤

instance MeasureTheory.isFiniteMeasureRestrict {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α) [h : MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.restrict μ s)

Equations

• ⋯ = ⋯

theorem MeasureTheory.measure_ne_top {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (s : Set α) : ↑↑μ s ≠ ⊤

theorem MeasureTheory.measure_compl_le_add_of_le_add {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasurableSet s) (ht : MeasurableSet t) {ε : ENNReal} (h : ↑↑μ s ≤ ↑↑μ t + ε) : ↑↑μ tᶜ ≤ ↑↑μ sᶜ + ε

theorem MeasureTheory.measure_compl_le_add_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasurableSet s) (ht : MeasurableSet t) {ε : ENNReal} : ↑↑μ sᶜ ≤ ↑↑μ tᶜ + ε ↔ ↑↑μ t ≤ ↑↑μ s + ε

def MeasureTheory.measureUnivNNReal {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : NNReal

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

Equations

• MeasureTheory.measureUnivNNReal μ = (↑↑μ Set.univ).toNNReal

@[simp]

theorem MeasureTheory.coe_measureUnivNNReal {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] : ↑(MeasureTheory.measureUnivNNReal μ) = ↑↑μ Set.univ

instance MeasureTheory.isFiniteMeasureZero {α : Type u_1} {m0 : MeasurableSpace α} : MeasureTheory.IsFiniteMeasure 0

Equations

• ⋯ = ⋯

instance MeasureTheory.isFiniteMeasureOfIsEmpty {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [IsEmpty α] : MeasureTheory.IsFiniteMeasure μ

Equations

• ⋯ = ⋯

@[simp]

theorem MeasureTheory.measureUnivNNReal_zero {α : Type u_1} {m0 : MeasurableSpace α} : MeasureTheory.measureUnivNNReal 0 = 0

instance MeasureTheory.isFiniteMeasureAdd {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : MeasureTheory.IsFiniteMeasure (μ + ν)

Equations

• ⋯ = ⋯

instance MeasureTheory.isFiniteMeasureSMulNNReal {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {r : NNReal} : MeasureTheory.IsFiniteMeasure (r • μ)

Equations

• ⋯ = ⋯

instance MeasureTheory.IsFiniteMeasure.average {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.IsFiniteMeasure ((↑↑μ Set.univ)⁻¹ • μ)

Equations

• ⋯ = ⋯

instance MeasureTheory.isFiniteMeasureSMulOfNNRealTower {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_5} [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal ENNReal] [IsScalarTower R ENNReal ENNReal] [MeasureTheory.IsFiniteMeasure μ] {r : R} : MeasureTheory.IsFiniteMeasure (r • μ)

Equations

• ⋯ = ⋯

theorem MeasureTheory.isFiniteMeasure_of_le {α : Type u_1} {m0 : MeasurableSpace α} {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (h : ν ≤ μ) : MeasureTheory.IsFiniteMeasure ν

theorem MeasureTheory.Measure.isFiniteMeasure_map {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : α → β) : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.map f μ)

@[simp]

theorem MeasureTheory.measureUnivNNReal_eq_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.measureUnivNNReal μ = 0 ↔ μ = 0

theorem MeasureTheory.measureUnivNNReal_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ ≠ 0) : 0 < MeasureTheory.measureUnivNNReal μ

theorem MeasureTheory.Measure.le_of_add_le_add_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν₁ : MeasureTheory.Measure α} {ν₂ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [hμ : MeasureTheory.IsFiniteMeasure μ] {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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasureTheory.NullMeasurableSet s μ) : s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ ↔ ↑↑μ s = ↑↑μ Set.univ

theorem MeasureTheory.ae_iff_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) : (∀ᵐ (a : α) ∂μ, a ∈ s) ↔ ↑↑μ s = ↑↑μ Set.univ

theorem MeasureTheory.abs_toReal_measure_sub_le_measure_symmDiff' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasurableSet s) (ht : MeasurableSet t) : |(↑↑μ s).toReal - (↑↑μ t).toReal| ≤ (↑↑μ (symmDiff s t)).toReal

class MeasureTheory.IsProbabilityMeasure {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : Prop

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

• measure_univ : ↑↑μ Set.univ = 1

theorem MeasureTheory.isProbabilityMeasure_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.IsProbabilityMeasure μ ↔ ↑↑μ Set.univ = 1

instance MeasureTheory.IsProbabilityMeasure.toIsFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.IsFiniteMeasure μ

Equations

• ⋯ = ⋯

theorem MeasureTheory.IsProbabilityMeasure.ne_zero {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : μ ≠ 0

instance MeasureTheory.IsProbabilityMeasure.neZero {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : NeZero μ

Equations

• ⋯ = ⋯

theorem MeasureTheory.IsProbabilityMeasure.ae_neBot {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] : Filter.NeBot (MeasureTheory.Measure.ae μ)

theorem MeasureTheory.prob_add_prob_compl {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (h : MeasurableSet s) : ↑↑μ s + ↑↑μ sᶜ = 1

theorem MeasureTheory.prob_le_one {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] : ↑↑μ s ≤ 1

instance MeasureTheory.isProbabilityMeasureSMul {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] : MeasureTheory.IsProbabilityMeasure ((↑↑μ Set.univ)⁻¹ • μ)

Equations

• ⋯ = ⋯

theorem MeasureTheory.isProbabilityMeasure_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {f : α → β} (hf : AEMeasurable f μ) : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map f μ)

@[simp]

theorem MeasureTheory.one_le_prob_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] : 1 ≤ ↑↑μ s ↔ ↑↑μ s = 1

theorem MeasureTheory.prob_compl_eq_one_sub₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (h : MeasureTheory.NullMeasurableSet s μ) : ↑↑μ 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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (hs : MeasurableSet s) : ↑↑μ 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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (hs : MeasureTheory.NullMeasurableSet s μ) : ↑↑μ sᶜ = 0 ↔ ↑↑μ s = 1

@[simp]

theorem MeasureTheory.prob_compl_eq_zero_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (hs : MeasurableSet s) : ↑↑μ sᶜ = 0 ↔ ↑↑μ s = 1

@[simp]

theorem MeasureTheory.prob_compl_eq_one_iff₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (hs : MeasureTheory.NullMeasurableSet s μ) : ↑↑μ sᶜ = 1 ↔ ↑↑μ s = 0

@[simp]

theorem MeasureTheory.prob_compl_eq_one_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (hs : MeasurableSet s) : ↑↑μ sᶜ = 1 ↔ ↑↑μ s = 0

theorem MeasureTheory.mem_ae_iff_prob_eq_one₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (hs : MeasureTheory.NullMeasurableSet s μ) : s ∈ MeasureTheory.Measure.ae μ ↔ ↑↑μ s = 1

theorem MeasureTheory.mem_ae_iff_prob_eq_one {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (hs : MeasurableSet s) : s ∈ MeasureTheory.Measure.ae μ ↔ ↑↑μ s = 1

theorem MeasureTheory.ae_iff_prob_eq_one {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {p : α → Prop} (hp : Measurable p) : (∀ᵐ (a : α) ∂μ, p a) ↔ ↑↑μ {a : α | p a} = 1

theorem MeasureTheory.isProbabilityMeasure_comap {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {f : β → α} (hf : Function.Injective f) (hf' : ∀ᵐ (a : α) ∂μ, a ∈ Set.range f) (hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)) : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.comap f μ)

theorem MeasurableEmbedding.isProbabilityMeasure_comap {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {f : β → α} (hf : MeasurableEmbedding f) (hf' : ∀ᵐ (a : α) ∂μ, a ∈ Set.range f) : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.comap f μ)

instance MeasureTheory.isProbabilityMeasure_map_up {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map ULift.up μ)

Equations

• ⋯ = ⋯

instance MeasureTheory.isProbabilityMeasure_comap_down {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.comap ULift.down μ)

Equations

• ⋯ = ⋯

class MeasureTheory.NoAtoms {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : Prop

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

theorem Set.Subsingleton.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (hs : Set.Subsingleton s) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] : ↑↑μ s = 0

theorem MeasureTheory.Measure.restrict_singleton' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] {a : α} : MeasureTheory.Measure.restrict μ {a} = 0

instance MeasureTheory.Measure.restrict.instNoAtoms {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] (s : Set α) : MeasureTheory.NoAtoms (MeasureTheory.Measure.restrict μ s)

Equations

• ⋯ = ⋯

theorem Set.Countable.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : Set.Countable s) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] : ↑↑μ s = 0

theorem Set.Countable.ae_not_mem {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : Set.Countable s) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] : ∀ᵐ (x : α) ∂μ, x ∉ s

theorem Set.Countable.measure_restrict_compl {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : Set.Countable s) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] : MeasureTheory.Measure.restrict μ sᶜ = μ

@[simp]

theorem MeasureTheory.restrict_compl_singleton {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] (a : α) : MeasureTheory.Measure.restrict μ {a}ᶜ = μ

theorem Set.Finite.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : Set.Finite s) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] : ↑↑μ s = 0

theorem Finset.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} (s : Finset α) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] : ↑↑μ ↑s = 0

theorem MeasureTheory.insert_ae_eq_self {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] (a : α) (s : Set α) : insert a s =ᶠ[MeasureTheory.Measure.ae μ] s

theorem MeasureTheory.Iio_ae_eq_Iic {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} : Set.Iio a =ᶠ[MeasureTheory.Measure.ae μ] Set.Iic a

theorem MeasureTheory.Ioi_ae_eq_Ici {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} : Set.Ioi a =ᶠ[MeasureTheory.Measure.ae μ] Set.Ici a

theorem MeasureTheory.Ioo_ae_eq_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : Set.Ioo a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Ioc a b

theorem MeasureTheory.Ioc_ae_eq_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : Set.Ioc a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Icc a b

theorem MeasureTheory.Ioo_ae_eq_Ico {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : Set.Ioo a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Ico a b

theorem MeasureTheory.Ioo_ae_eq_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : Set.Ioo a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Icc a b

theorem MeasureTheory.Ico_ae_eq_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : Set.Ico a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Icc a b

theorem MeasureTheory.Ico_ae_eq_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : Set.Ico a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Ioc a b

theorem MeasureTheory.restrict_Iio_eq_restrict_Iic {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} : MeasureTheory.Measure.restrict μ (Set.Iio a) = MeasureTheory.Measure.restrict μ (Set.Iic a)

theorem MeasureTheory.restrict_Ioi_eq_restrict_Ici {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} : MeasureTheory.Measure.restrict μ (Set.Ioi a) = MeasureTheory.Measure.restrict μ (Set.Ici a)

theorem MeasureTheory.restrict_Ioo_eq_restrict_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : MeasureTheory.Measure.restrict μ (Set.Ioo a b) = MeasureTheory.Measure.restrict μ (Set.Ioc a b)

theorem MeasureTheory.restrict_Ioc_eq_restrict_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : MeasureTheory.Measure.restrict μ (Set.Ioc a b) = MeasureTheory.Measure.restrict μ (Set.Icc a b)

theorem MeasureTheory.restrict_Ioo_eq_restrict_Ico {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : MeasureTheory.Measure.restrict μ (Set.Ioo a b) = MeasureTheory.Measure.restrict μ (Set.Ico a b)

theorem MeasureTheory.restrict_Ioo_eq_restrict_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : MeasureTheory.Measure.restrict μ (Set.Ioo a b) = MeasureTheory.Measure.restrict μ (Set.Icc a b)

theorem MeasureTheory.restrict_Ico_eq_restrict_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : MeasureTheory.Measure.restrict μ (Set.Ico a b) = MeasureTheory.Measure.restrict μ (Set.Icc a b)

theorem MeasureTheory.restrict_Ico_eq_restrict_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : MeasureTheory.Measure.restrict μ (Set.Ico a b) = MeasureTheory.Measure.restrict μ (Set.Ioc a b)

theorem MeasureTheory.uIoc_ae_eq_interval {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [LinearOrder α] {a : α} {b : α} : Ι a b =ᶠ[MeasureTheory.Measure.ae μ] Set.uIcc a b

theorem MeasureTheory.ite_ae_eq_of_measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {γ : 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) =ᶠ[MeasureTheory.Measure.ae μ] g

theorem MeasureTheory.ite_ae_eq_of_measure_compl_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {γ : 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) =ᶠ[MeasureTheory.Measure.ae μ] f

def MeasureTheory.Measure.FiniteAtFilter {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : Filter α) : Prop

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

• MeasureTheory.Measure.FiniteAtFilter μ f = ∃ s ∈ f, ↑↑μ s < ⊤

theorem MeasureTheory.Measure.finiteAtFilter_of_finite {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : Filter α) : MeasureTheory.Measure.FiniteAtFilter μ f

theorem MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} (hμ : MeasureTheory.Measure.FiniteAtFilter μ f) {p : ι → Prop} {s : ι → Set α} (hf : Filter.HasBasis f p s) : ∃ (i : ι), p i ∧ ↑↑μ (s i) < ⊤

theorem MeasureTheory.Measure.finiteAtBot {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : MeasureTheory.Measure.FiniteAtFilter μ ⊥

structure MeasureTheory.Measure.FiniteSpanningSetsIn {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (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

class MeasureTheory.SFinite {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : Prop

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

noncomputable def MeasureTheory.sFiniteSeq {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [h : MeasureTheory.SFinite μ] : ℕ → MeasureTheory.Measure α

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

Equations

• MeasureTheory.sFiniteSeq μ = Exists.choose ⋯

instance MeasureTheory.isFiniteMeasure_sFiniteSeq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [h : MeasureTheory.SFinite μ] (n : ℕ) : MeasureTheory.IsFiniteMeasure (MeasureTheory.sFiniteSeq μ n)

Equations

• ⋯ = ⋯

theorem MeasureTheory.sum_sFiniteSeq {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [h : MeasureTheory.SFinite μ] : MeasureTheory.Measure.sum (MeasureTheory.sFiniteSeq μ) = μ

theorem MeasureTheory.sfinite_sum_of_countable {α : Type u_1} {m0 : MeasurableSpace α} {ι : Type u_5} [Countable ι] (m : ι → MeasureTheory.Measure α) [∀ (n : ι), MeasureTheory.IsFiniteMeasure (m n)] : MeasureTheory.SFinite (MeasureTheory.Measure.sum m)

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

instance MeasureTheory.instSFiniteSum {α : Type u_1} {m0 : MeasurableSpace α} {ι : Type u_5} [Countable ι] (m : ι → MeasureTheory.Measure α) [∀ (n : ι), MeasureTheory.SFinite (m n)] : MeasureTheory.SFinite (MeasureTheory.Measure.sum m)

Equations

• ⋯ = ⋯

class MeasureTheory.SigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : Prop

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 (MeasureTheory.Measure.FiniteSpanningSetsIn μ Set.univ)

theorem MeasureTheory.sigmaFinite_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.SigmaFinite μ ↔ Nonempty (MeasureTheory.Measure.FiniteSpanningSetsIn μ Set.univ)

theorem MeasureTheory.SigmaFinite.out {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.SigmaFinite μ) : Nonempty (MeasureTheory.Measure.FiniteSpanningSetsIn μ Set.univ)

def MeasureTheory.Measure.toFiniteSpanningSetsIn {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [h : MeasureTheory.SigmaFinite μ] : MeasureTheory.Measure.FiniteSpanningSetsIn μ {s : Set α | MeasurableSet s}

If μ is σ-finite it has finite spanning sets in the collection of all measurable sets.

Equations

• MeasureTheory.Measure.toFiniteSpanningSetsIn μ = { set := fun (n : ℕ) => MeasureTheory.toMeasurable μ ((Nonempty.some ⋯).set n), set_mem := ⋯, finite := ⋯, spanning := ⋯ }

def MeasureTheory.spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (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

• MeasureTheory.spanningSets μ i = Set.Accumulate (MeasureTheory.Measure.toFiniteSpanningSetsIn μ).set i

theorem MeasureTheory.monotone_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : Monotone (MeasureTheory.spanningSets μ)

theorem MeasureTheory.measurable_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (i : ℕ) : MeasurableSet (MeasureTheory.spanningSets μ i)

theorem MeasureTheory.measure_spanningSets_lt_top {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (i : ℕ) : ↑↑μ (MeasureTheory.spanningSets μ i) < ⊤

theorem MeasureTheory.iUnion_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : ⋃ (i : ℕ), MeasureTheory.spanningSets μ i = Set.univ

theorem MeasureTheory.isCountablySpanning_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : IsCountablySpanning (Set.range (MeasureTheory.spanningSets μ))

noncomputable def MeasureTheory.spanningSetsIndex {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (x : α) : ℕ

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

Equations

• MeasureTheory.spanningSetsIndex μ x = Nat.find ⋯

theorem MeasureTheory.measurable_spanningSetsIndex {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : Measurable (MeasureTheory.spanningSetsIndex μ)

theorem MeasureTheory.preimage_spanningSetsIndex_singleton {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (n : ℕ) : MeasureTheory.spanningSetsIndex μ ⁻¹' {n} = disjointed (MeasureTheory.spanningSets μ) n

theorem MeasureTheory.spanningSetsIndex_eq_iff {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] {x : α} {n : ℕ} : MeasureTheory.spanningSetsIndex μ x = n ↔ x ∈ disjointed (MeasureTheory.spanningSets μ) n

theorem MeasureTheory.mem_disjointed_spanningSetsIndex {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (x : α) : x ∈ disjointed (MeasureTheory.spanningSets μ) (MeasureTheory.spanningSetsIndex μ x)

theorem MeasureTheory.mem_spanningSetsIndex {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (x : α) : x ∈ MeasureTheory.spanningSets μ (MeasureTheory.spanningSetsIndex μ x)

theorem MeasureTheory.mem_spanningSets_of_index_le {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (x : α) {n : ℕ} (hn : MeasureTheory.spanningSetsIndex μ x ≤ n) : x ∈ MeasureTheory.spanningSets μ n

theorem MeasureTheory.eventually_mem_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (x : α) : ∀ᶠ (n : ℕ) in Filter.atTop, x ∈ MeasureTheory.spanningSets μ n

theorem MeasureTheory.sum_restrict_disjointed_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : (MeasureTheory.Measure.sum fun (n : ℕ) => MeasureTheory.Measure.restrict μ (disjointed (MeasureTheory.spanningSets μ) n)) = μ

instance MeasureTheory.instSFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] : MeasureTheory.SFinite μ

Equations

• ⋯ = ⋯

theorem MeasureTheory.Measure.iSup_restrict_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.SigmaFinite μ] (hs : MeasurableSet s) : ⨆ (i : ℕ), ↑↑(MeasureTheory.Measure.restrict μ (MeasureTheory.spanningSets μ i)) s = ↑↑μ s

theorem MeasureTheory.Measure.exists_subset_measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.SigmaFinite μ] {r : ENNReal} (hs : MeasurableSet s) (h's : r < ↑↑μ s) : ∃ (t : Set α), MeasurableSet t ∧ t ⊆ s ∧ r < ↑↑μ t ∧ ↑↑μ t < ⊤

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

theorem MeasureTheory.Measure.forall_measure_inter_spanningSets_eq_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (s : Set α) : (∀ (n : ℕ), ↑↑μ (s ∩ MeasureTheory.spanningSets μ n) = 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} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (s : Set α) : (∃ (n : ℕ), 0 < ↑↑μ (s ∩ MeasureTheory.spanningSets μ n)) ↔ 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} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {ε : ENNReal} (ε_pos : 0 < ε) {As : ι → Set α} (As_mble : ∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) (As_disj : Pairwise (MeasureTheory.AEDisjoint μ on As)) (Union_As_finite : ↑↑μ (⋃ (i : ι), As i) ≠ ⊤) : Set.Finite {i : ι | ε ≤ ↑↑μ (As i)}

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} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {ε : ENNReal} (ε_pos : 0 < ε) {As : ι → Set α} (As_mble : ∀ (i : ι), MeasurableSet (As i)) (As_disj : Pairwise (Disjoint on As)) (Union_As_finite : ↑↑μ (⋃ (i : ι), As i) ≠ ⊤) : Set.Finite {i : ι | ε ≤ ↑↑μ (As i)}

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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] {s : Set α} (hs : Set.Infinite s) (h' : ∃ (ε : ENNReal), ε ≠ 0 ∧ ∀ x ∈ s, ε ≤ ↑↑μ {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 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ι → Set α}, (∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) → Pairwise (MeasureTheory.AEDisjoint μ on As) → ↑↑μ (⋃ (i : ι), As i) ≠ ⊤ → Set.Countable {i : ι | 0 < ↑↑μ (As i)}

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 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ι → Set α}, (∀ (i : ι), MeasurableSet (As i)) → Pairwise (Disjoint on As) → ↑↑μ (⋃ (i : ι), As i) ≠ ⊤ → Set.Countable {i : ι | 0 < ↑↑μ (As i)}

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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ] {As : ι → Set α}, (∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) → Pairwise (MeasureTheory.AEDisjoint μ on As) → Set.Countable {i : ι | 0 < ↑↑μ (As i)}

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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ] {As : ι → Set α}, (∀ (i : ι), MeasurableSet (As i)) → Pairwise (Disjoint on As) → Set.Countable {i : ι | 0 < ↑↑μ (As i)}

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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ] [inst : MeasurableSpace β] [inst_1 : MeasurableSingletonClass β] {g : α → β}, MeasureTheory.NullMeasurable g μ → Set.Countable {t : β | 0 < ↑↑μ {a : α | g a = t}}

theorem MeasureTheory.Measure.countable_meas_level_set_pos {α : Type u_5} {β : Type u_6} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ] [inst : MeasurableSpace β] [inst_1 : MeasurableSingletonClass β] {g : α → β}, Measurable g → Set.Countable {t : β | 0 < ↑↑μ {a : α | g a = t}}

theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sum {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) {t : Set α} {m : ℕ → MeasureTheory.Measure α} (hv : ∀ (n : ℕ), ↑↑(m n) t ≠ ⊤) (hμ : μ = MeasureTheory.Measure.sum m) : ↑↑μ (MeasureTheory.toMeasurable μ t ∩ 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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) {t : Set α} {v : ℕ → Set α} (hv : t ⊆ ⋃ (n : ℕ), v n) (h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤) : ↑↑μ (MeasureTheory.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).

theorem MeasureTheory.Measure.restrict_toMeasurable_of_cover {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {v : ℕ → Set α} (hv : s ⊆ ⋃ (n : ℕ), v n) (h'v : ∀ (n : ℕ), ↑↑μ (s ∩ v n) ≠ ⊤) : MeasureTheory.Measure.restrict μ (MeasureTheory.toMeasurable μ s) = MeasureTheory.Measure.restrict μ s

theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {s : Set α} (hs : MeasurableSet s) (t : Set α) : ↑↑μ (MeasureTheory.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.

@[simp]

theorem MeasureTheory.Measure.restrict_toMeasurable_of_sFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (s : Set α) : MeasureTheory.Measure.restrict μ (MeasureTheory.toMeasurable μ s) = MeasureTheory.Measure.restrict μ s

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

If μ has finite spanning sets in C and C ∩ {s | μ s < ∞} ⊆ D then μ has finite spanning sets in D.

Equations

• MeasureTheory.Measure.FiniteSpanningSetsIn.mono' h hC = { set := h.set, set_mem := ⋯, finite := ⋯, spanning := ⋯ }

def MeasureTheory.Measure.FiniteSpanningSetsIn.mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)} {D : Set (Set α)} (h : MeasureTheory.Measure.FiniteSpanningSetsIn μ C) (hC : C ⊆ D) : MeasureTheory.Measure.FiniteSpanningSetsIn μ D

If μ has finite spanning sets in C and C ⊆ D then μ has finite spanning sets in D.

Equations

• MeasureTheory.Measure.FiniteSpanningSetsIn.mono h hC = MeasureTheory.Measure.FiniteSpanningSetsIn.mono' h ⋯

theorem MeasureTheory.Measure.FiniteSpanningSetsIn.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)} (h : MeasureTheory.Measure.FiniteSpanningSetsIn μ C) : MeasureTheory.SigmaFinite μ

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

theorem MeasureTheory.Measure.FiniteSpanningSetsIn.ext {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {C : Set (Set α)} (hA : m0 = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) (h : MeasureTheory.Measure.FiniteSpanningSetsIn μ C) (h_eq : ∀ s ∈ C, ↑↑μ 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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)} (h : MeasureTheory.Measure.FiniteSpanningSetsIn μ C) : IsCountablySpanning C

theorem MeasureTheory.Measure.sigmaFinite_of_countable {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {S : Set (Set α)} (hc : Set.Countable S) (hμ : ∀ s ∈ S, ↑↑μ s < ⊤) (hU : ⋃₀ S = Set.univ) : MeasureTheory.SigmaFinite μ

def MeasureTheory.Measure.FiniteSpanningSetsIn.ofLE {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : ν ≤ μ) {C : Set (Set α)} (S : MeasureTheory.Measure.FiniteSpanningSetsIn μ C) : MeasureTheory.Measure.FiniteSpanningSetsIn ν C

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 := ⋯ }

theorem MeasureTheory.Measure.sigmaFinite_of_le {α : Type u_1} {m0 : MeasurableSpace α} {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure α) [hs : MeasureTheory.SigmaFinite μ] (h : ν ≤ μ) : MeasureTheory.SigmaFinite ν

@[simp]

theorem MeasureTheory.Measure.add_right_inj {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν₁ : MeasureTheory.Measure α) (ν₂ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂

@[simp]

theorem MeasureTheory.Measure.add_left_inj {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν₁ : MeasureTheory.Measure α) (ν₂ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : ν₁ + μ = ν₂ + μ ↔ ν₁ = ν₂

instance MeasureTheory.IsFiniteMeasure.toSigmaFinite {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.SigmaFinite μ

Every finite measure is σ-finite.

Equations

• ⋯ = ⋯

theorem MeasureTheory.sigmaFinite_bot_iff {α : Type u_1} (μ : MeasureTheory.Measure α) : MeasureTheory.SigmaFinite μ ↔ MeasureTheory.IsFiniteMeasure μ

instance MeasureTheory.Restrict.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (s : Set α) : MeasureTheory.SigmaFinite (MeasureTheory.Measure.restrict μ s)

Equations

• ⋯ = ⋯

instance MeasureTheory.sum.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} {ι : Type u_5} [Finite ι] (μ : ι → MeasureTheory.Measure α) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] : MeasureTheory.SigmaFinite (MeasureTheory.Measure.sum μ)

Equations

• ⋯ = ⋯

instance MeasureTheory.Add.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : MeasureTheory.SigmaFinite (μ + ν)

Equations

• ⋯ = ⋯

instance MeasureTheory.SMul.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (c : NNReal) : MeasureTheory.SigmaFinite (c • μ)

Equations

• ⋯ = ⋯

theorem MeasureTheory.SigmaFinite.of_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] (μ : MeasureTheory.Measure α) {f : α → β} (hf : AEMeasurable f μ) (h : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ)) : MeasureTheory.SigmaFinite μ

theorem MeasurableEquiv.sigmaFinite_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} (f : α ≃ᵐ β) (h : MeasureTheory.SigmaFinite μ) : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map (⇑f) μ)

theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (P : α → Prop) (h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ↑↑ν s < ⊤ → ∀ᵐ (x : α) ∂MeasureTheory.Measure.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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (P : α → Prop) (h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ᵐ (x : α) ∂MeasureTheory.Measure.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 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) : Prop

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

• finiteAtNhds : ∀ (x : α), MeasureTheory.Measure.FiniteAtFilter μ (nhds x)

instance MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.IsLocallyFiniteMeasure μ

Equations

• ⋯ = ⋯

theorem MeasureTheory.Measure.finiteAt_nhds {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (x : α) : MeasureTheory.Measure.FiniteAtFilter μ (nhds x)

theorem MeasureTheory.Measure.smul_finite {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] {c : ENNReal} (hc : c ≠ ⊤) : MeasureTheory.IsFiniteMeasure (c • μ)

theorem MeasureTheory.Measure.exists_isOpen_measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (x : α) : ∃ (s : Set α), x ∈ s ∧ IsOpen s ∧ ↑↑μ s < ⊤

instance MeasureTheory.isLocallyFiniteMeasureSMulNNReal {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (c : NNReal) : MeasureTheory.IsLocallyFiniteMeasure (c • μ)

Equations

• ⋯ = ⋯

theorem MeasureTheory.Measure.isTopologicalBasis_isOpen_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] : TopologicalSpace.IsTopologicalBasis {s : Set α | IsOpen s ∧ ↑↑μ s < ⊤}

class MeasureTheory.IsFiniteMeasureOnCompacts {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) : Prop

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

• lt_top_of_isCompact : ∀ ⦃K : Set α⦄, IsCompact K → ↑↑μ K < ⊤

theorem IsCompact.measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃K : Set α⦄ (hK : IsCompact K) : ↑↑μ K < ⊤

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

theorem IsCompact.measure_ne_top {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃K : Set α⦄ (hK : IsCompact K) : ↑↑μ 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 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃s : Set α⦄ (hs : Bornology.IsBounded s) : ↑↑μ 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 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ} : ↑↑μ (Metric.closedBall x r) < ⊤

theorem MeasureTheory.measure_ball_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ} : ↑↑μ (Metric.ball x r) < ⊤

theorem MeasureTheory.IsFiniteMeasureOnCompacts.smul {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasureOnCompacts μ] {c : ENNReal} (hc : c ≠ ⊤) : MeasureTheory.IsFiniteMeasureOnCompacts (c • μ)

instance MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (c : NNReal) : MeasureTheory.IsFiniteMeasureOnCompacts (c • μ)

Equations

• ⋯ = ⋯

instance MeasureTheory.instIsFiniteMeasureOnCompactsRestrict {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {s : Set α} : MeasureTheory.IsFiniteMeasureOnCompacts (MeasureTheory.Measure.restrict μ s)

Equations

• ⋯ = ⋯

instance MeasureTheory.CompactSpace.isFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [CompactSpace α] [MeasureTheory.IsFiniteMeasureOnCompacts μ] : MeasureTheory.IsFiniteMeasure μ

Equations

• ⋯ = ⋯

instance MeasureTheory.SigmaFinite.of_isFiniteMeasureOnCompacts {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] [SigmaCompactSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : MeasureTheory.SigmaFinite μ

Equations

• ⋯ = ⋯

instance MeasureTheory.sigmaFinite_of_locallyFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [SecondCountableTopology α] [MeasureTheory.IsLocallyFiniteMeasure μ] : MeasureTheory.SigmaFinite μ

Equations

• ⋯ = ⋯

instance MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [WeaklyLocallyCompactSpace α] [MeasureTheory.IsFiniteMeasureOnCompacts μ] : MeasureTheory.IsLocallyFiniteMeasure μ

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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PseudoMetricSpace δ] (f : α → δ) (x : δ) (hμ : μ ≠ 0) : ∃ (n : ℕ), 0 < ↑↑μ (f ⁻¹' Metric.ball x ↑n)

theorem MeasureTheory.exists_pos_ball {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PseudoMetricSpace α] (x : α) (hμ : μ ≠ 0) : ∃ (n : ℕ), 0 < ↑↑μ (Metric.ball x ↑n)

theorem MeasureTheory.null_of_locally_null {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [SecondCountableTopology α] (s : Set α) (hs : ∀ x ∈ s, ∃ u ∈ nhdsWithin x s, ↑↑μ 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_mem_forall_mem_nhdsWithin_pos_measure {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [SecondCountableTopology α] {s : Set α} (hs : ↑↑μ s ≠ 0) : ∃ x ∈ s, ∀ t ∈ nhdsWithin x s, 0 < ↑↑μ t

theorem MeasureTheory.exists_ne_forall_mem_nhds_pos_measure_preimage {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [TopologicalSpace β] [T1Space β] [SecondCountableTopology β] [Nonempty β] {f : α → β} (h : ∀ (b : β), ∃ᵐ (x : α) ∂μ, f x ≠ b) : ∃ (a : β) (b : β), a ≠ b ∧ (∀ s ∈ nhds a, 0 < ↑↑μ (f ⁻¹' s)) ∧ ∀ t ∈ nhds b, 0 < ↑↑μ (f ⁻¹' t)

theorem MeasureTheory.ext_on_measurableSpace_of_generate_finite {α : Type u_5} (m₀ : MeasurableSpace α) {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (C : Set (Set α)) (hμν : ∀ s ∈ C, ↑↑μ s = ↑↑ν s) {m : MeasurableSpace α} (h : m ≤ m₀) (hA : m = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) (h_univ : ↑↑μ Set.univ = ↑↑ν Set.univ) {s : Set α} (hs : MeasurableSet s) : ↑↑μ 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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (C : Set (Set α)) (hA : m0 = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) [MeasureTheory.IsFiniteMeasure μ] (hμν : ∀ s ∈ C, ↑↑μ 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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (S : MeasureTheory.Measure.FiniteSpanningSetsIn μ {s : Set α | MeasurableSet s}) : MeasureTheory.Measure.FiniteSpanningSetsIn μ {s : Set α | MeasurableSet s}

Given S : μ.FiniteSpanningSetsIn {s | MeasurableSet s}, FiniteSpanningSetsIn.disjointed provides a FiniteSpanningSetsIn {s | MeasurableSet s} such that its underlying sets are pairwise disjoint.

Equations

• MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed S = { set := disjointed S.set, set_mem := ⋯, finite := ⋯, spanning := ⋯ }

theorem MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (S : MeasureTheory.Measure.FiniteSpanningSetsIn μ {s : Set α | MeasurableSet s}) : (MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed S).set = disjointed S.set

theorem MeasureTheory.Measure.exists_eq_disjoint_finiteSpanningSetsIn {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : ∃ (S : MeasureTheory.Measure.FiniteSpanningSetsIn μ {s : Set α | MeasurableSet s}) (T : MeasureTheory.Measure.FiniteSpanningSetsIn ν {s : Set α | MeasurableSet s}), S.set = T.set ∧ Pairwise (Disjoint on S.set)

theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} {g : Filter α} (h : f ≤ g) : MeasureTheory.Measure.FiniteAtFilter μ g → MeasureTheory.Measure.FiniteAtFilter μ f

theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} {g : Filter α} (h : MeasureTheory.Measure.FiniteAtFilter μ f) : MeasureTheory.Measure.FiniteAtFilter μ (f ⊓ g)

theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} {g : Filter α} (h : MeasureTheory.Measure.FiniteAtFilter μ g) : MeasureTheory.Measure.FiniteAtFilter μ (f ⊓ g)

@[simp]

theorem MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} : MeasureTheory.Measure.FiniteAtFilter μ (f ⊓ MeasureTheory.Measure.ae μ) ↔ MeasureTheory.Measure.FiniteAtFilter μ f

theorem MeasureTheory.Measure.FiniteAtFilter.of_inf_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} : MeasureTheory.Measure.FiniteAtFilter μ (f ⊓ MeasureTheory.Measure.ae μ) → MeasureTheory.Measure.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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} {g : Filter α} (h : f ⊓ MeasureTheory.Measure.ae μ ≤ g) (hg : MeasureTheory.Measure.FiniteAtFilter μ g) : MeasureTheory.Measure.FiniteAtFilter μ f

theorem MeasureTheory.Measure.FiniteAtFilter.measure_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : Filter α} (h : μ ≤ ν) : MeasureTheory.Measure.FiniteAtFilter ν f → MeasureTheory.Measure.FiniteAtFilter μ f

theorem MeasureTheory.Measure.FiniteAtFilter.mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : Filter α} {g : Filter α} (hf : f ≤ g) (hμ : μ ≤ ν) : MeasureTheory.Measure.FiniteAtFilter ν g → MeasureTheory.Measure.FiniteAtFilter μ f

theorem MeasureTheory.Measure.FiniteAtFilter.eventually {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} (h : MeasureTheory.Measure.FiniteAtFilter μ f) : ∀ᶠ (s : Set α) in Filter.smallSets f, ↑↑μ s < ⊤

theorem MeasureTheory.Measure.FiniteAtFilter.filterSup {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} {g : Filter α} : MeasureTheory.Measure.FiniteAtFilter μ f → MeasureTheory.Measure.FiniteAtFilter μ g → MeasureTheory.Measure.FiniteAtFilter μ (f ⊔ g)

theorem MeasureTheory.Measure.finiteAt_nhdsWithin {α : Type u_1} [TopologicalSpace α] {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (x : α) (s : Set α) : MeasureTheory.Measure.FiniteAtFilter μ (nhdsWithin x s)

@[simp]

theorem MeasureTheory.Measure.finiteAt_principal {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} : MeasureTheory.Measure.FiniteAtFilter μ (Filter.principal s) ↔ ↑↑μ s < ⊤

theorem MeasureTheory.Measure.isLocallyFiniteMeasure_of_le {α : Type u_1} [TopologicalSpace α] {_m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [H : MeasureTheory.IsLocallyFiniteMeasure μ] (h : ν ≤ μ) : MeasureTheory.IsLocallyFiniteMeasure ν

theorem IsCompact.exists_open_superset_measure_lt_top' {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h : IsCompact s) (hμ : ∀ x ∈ s, MeasureTheory.Measure.FiniteAtFilter μ (nhds x)) : ∃ U ⊇ s, IsOpen U ∧ ↑↑μ 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} [TopologicalSpace α] [MeasurableSpace α] {s : Set α} (h : IsCompact s) (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] : ∃ U ⊇ s, IsOpen U ∧ ↑↑μ 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} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h : IsCompact s) (hμ : ∀ x ∈ s, MeasureTheory.Measure.FiniteAtFilter μ (nhdsWithin x s)) : ↑↑μ s < ⊤

theorem IsCompact.measure_zero_of_nhdsWithin {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : IsCompact s) : (∀ a ∈ s, ∃ t ∈ nhdsWithin a s, ↑↑μ t = 0) → ↑↑μ s = 0

instance isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure {α : Type u_1} [TopologicalSpace α] : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsLocallyFiniteMeasure μ], MeasureTheory.IsFiniteMeasureOnCompacts μ

Equations

• ⋯ = ⋯

theorem isFiniteMeasure_iff_isFiniteMeasureOnCompacts_of_compactSpace {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [CompactSpace α] : MeasureTheory.IsFiniteMeasure μ ↔ MeasureTheory.IsFiniteMeasureOnCompacts μ

def MeasureTheory.Measure.finiteSpanningSetsInCompact {α : Type u_1} [TopologicalSpace α] [SigmaCompactSpace α] : {x : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [inst : MeasureTheory.IsLocallyFiniteMeasure μ] → MeasureTheory.Measure.FiniteSpanningSetsIn μ {K : Set α | IsCompact K}

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

Equations

• MeasureTheory.Measure.finiteSpanningSetsInCompact μ = { set := compactCovering α, set_mem := ⋯, finite := ⋯, spanning := ⋯ }

def MeasureTheory.Measure.finiteSpanningSetsInOpen {α : Type u_1} [TopologicalSpace α] [SigmaCompactSpace α] : {x : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [inst : MeasureTheory.IsLocallyFiniteMeasure μ] → MeasureTheory.Measure.FiniteSpanningSetsIn μ {K : Set α | IsOpen K}

A locally finite measure on a σ-compact topological space admits a finite spanning sequence of open sets.

Equations

• MeasureTheory.Measure.finiteSpanningSetsInOpen μ = { set := fun (n : ℕ) => Exists.choose ⋯, set_mem := ⋯, finite := ⋯, spanning := ⋯ }

theorem MeasureTheory.Measure.finiteSpanningSetsInOpen'_def {α : Type u_5} [TopologicalSpace α] [SecondCountableTopology α] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] : MeasureTheory.Measure.finiteSpanningSetsInOpen' μ = let_fun H := ⋯; Nonempty.some H

@[irreducible]

noncomputable def MeasureTheory.Measure.finiteSpanningSetsInOpen' {α : Type u_5} [TopologicalSpace α] [SecondCountableTopology α] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] : MeasureTheory.Measure.FiniteSpanningSetsIn μ {K : Set α | IsOpen K}

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

Equations

• @MeasureTheory.Measure.finiteSpanningSetsInOpen' = wrapped✝.1

theorem measure_Icc_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} : ↑↑μ (Set.Icc a b) < ⊤

theorem measure_Ico_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} : ↑↑μ (Set.Ico a b) < ⊤

theorem measure_Ioc_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} : ↑↑μ (Set.Ioc a b) < ⊤

theorem measure_Ioo_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} : ↑↑μ (Set.Ioo a b) < ⊤