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 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : Prop

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

• measure_univ_lt_top : μ Set.univ < ⊤

theorem MeasureTheory.IsFiniteMeasure.measure_univ_lt_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.IsFiniteMeasure μ] : μ 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 (μ.restrict s)

Equations

• ⋯ = ⋯

@[simp]

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 (μ.restrict s)

Equations

• ⋯ = ⋯

@[simp]

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 50]

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 =ᵐ[μ] 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.tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint {X : Type u_5} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] {Es : ℕ → Set X} (Es_mble : ∀ (i : ℕ), MeasureTheory.NullMeasurableSet (Es 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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (ht : MeasureTheory.NullMeasurableSet 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 : MeasureTheory.NullMeasurableSet s μ) (ht : MeasureTheory.NullMeasurableSet t μ) : |(μ s).toReal - (μ t).toReal| ≤ (μ (symmDiff s t)).toReal

instance MeasureTheory.instIsFiniteMeasureSumMeasure {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {s : Finset ι} {μ : ι → MeasureTheory.Measure α} [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] : MeasureTheory.IsFiniteMeasure (∑ i ∈ s, μ i)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

theorem MeasureTheory.IsZeroOrProbabilityMeasure.measure_univ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.IsZeroOrProbabilityMeasure μ] : μ Set.univ = 0 ∨ μ Set.univ = 1

theorem MeasureTheory.isZeroOrProbabilityMeasure_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.IsZeroOrProbabilityMeasure μ ↔ μ Set.univ = 0 ∨ μ Set.univ = 1

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

@[simp]

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

@[instance 100]

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

Equations

• ⋯ = ⋯

instance MeasureTheory.instIsZeroOrProbabilityMeasureOfNatMeasure {α : Type u_1} {m0 : MeasurableSpace α} : MeasureTheory.IsZeroOrProbabilityMeasure 0

Equations

• ⋯ = ⋯

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

@[simp]

theorem MeasureTheory.IsProbabilityMeasure.measure_univ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.IsProbabilityMeasure μ] : μ Set.univ = 1

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

@[instance 100]

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

Equations

• ⋯ = ⋯

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

@[instance 100]

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 μ] : (MeasureTheory.ae μ).NeBot

theorem MeasureTheory.prob_add_prob_compl {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (h : MeasurableSet s) : μ s + μ 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 μ)

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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem MeasureTheory.eq_zero_or_isProbabilityMeasure {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsZeroOrProbabilityMeasure μ] : μ = 0 ∨ MeasureTheory.IsProbabilityMeasure μ

instance MeasureTheory.instIsZeroOrProbabilityMeasureMap {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.IsZeroOrProbabilityMeasure μ] {f : α → β} : MeasureTheory.IsZeroOrProbabilityMeasure (MeasureTheory.Measure.map f μ)

Equations

• ⋯ = ⋯

theorem MeasureTheory.prob_compl_lt_one_sub_of_lt_prob {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsZeroOrProbabilityMeasure μ] {p : ENNReal} (hμs : p < μ s) (s_mble : MeasurableSet s) : μ sᶜ < 1 - p

theorem MeasureTheory.prob_compl_le_one_sub_of_le_prob {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsZeroOrProbabilityMeasure μ] {p : ENNReal} (hμs : p ≤ μ s) (s_mble : MeasurableSet s) : μ sᶜ ≤ 1 - p

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

@[simp]

theorem MeasureTheory.NoAtoms.measure_singleton {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.NoAtoms μ] (x : α) : μ {x} = 0

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

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

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

Equations

• ⋯ = ⋯

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

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

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

@[simp]

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

theorem Set.Finite.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : s.Finite) (μ : 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 =ᵐ[μ] s

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

theorem MeasureTheory.Ioi_ae_eq_Ici {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} : Set.Ioi a =ᵐ[μ] 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 =ᵐ[μ] 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 =ᵐ[μ] 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 =ᵐ[μ] 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 =ᵐ[μ] 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 =ᵐ[μ] 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 =ᵐ[μ] Set.Ioc a b

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

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

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

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

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

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

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

theorem MeasureTheory.restrict_Ico_eq_restrict_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : μ.restrict (Set.Ico a b) = μ.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 =ᵐ[μ] 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) =ᵐ[μ] 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) =ᵐ[μ] 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

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

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

theorem MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} (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 : MeasurableSpace α} (μ : 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

theorem MeasureTheory.Measure.FiniteSpanningSetsIn.set_mem {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)} (self : μ.FiniteSpanningSetsIn C) (i : ℕ) : self.set i ∈ C

theorem MeasureTheory.Measure.FiniteSpanningSetsIn.finite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)} (self : μ.FiniteSpanningSetsIn C) (i : ℕ) : μ (self.set i) < ⊤

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

theorem MeasureTheory.SFinite.out' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.SFinite μ] : ∃ (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 μ = ⋯.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 μ) = μ

instance MeasureTheory.instSFiniteOfNatMeasure {α : Type u_1} {m0 : MeasurableSpace α} : MeasureTheory.SFinite 0

Equations

• ⋯ = ⋯

@[simp]

theorem MeasureTheory.sFiniteSeq_zero {α : Type u_1} {m0 : MeasurableSpace α} (n : ℕ) : MeasureTheory.sFiniteSeq 0 n = 0

theorem MeasureTheory.sfinite_sum_of_countable {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} [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 superseded by the instance below.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : ∃ (ν : MeasureTheory.Measure α), MeasureTheory.IsFiniteMeasure ν ∧ μ.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 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : ∃ (ν : MeasureTheory.Measure α), MeasureTheory.IsFiniteMeasure ν ∧ μ.AbsolutelyContinuous ν

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

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

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

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

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

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

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 μ.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.Measure α) [MeasureTheory.SigmaFinite ν] : (MeasureTheory.Measure.sum fun (n : ℕ) => μ.restrict (disjointed (MeasureTheory.spanningSets ν) n)) = μ

@[instance 100]

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

Equations

• ⋯ = ⋯

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) ≠ ⊤) : {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} [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) ≠ ⊤) : {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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] {s : Set α} (hs : s.Infinite) (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) ≠ ⊤ → {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 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ] {As : ι → Set α}, (∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) → Pairwise (MeasureTheory.AEDisjoint μ on As) → {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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ] {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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ] [inst : MeasurableSpace β] [inst_1 : MeasurableSingletonClass β] {g : α → β}, MeasureTheory.NullMeasurable g μ → {t : β | 0 < μ {a : α | g a = t}}.Countable

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 → {t : β | 0 < μ {a : α | g a = t}}.Countable

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) ≠ ⊤) : μ.restrict (MeasureTheory.toMeasurable μ s) = μ.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 α) : μ.restrict (MeasureTheory.toMeasurable μ s) = μ.restrict s

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

Auxiliary lemma for iSup_restrict_spanningSets.

theorem MeasureTheory.Measure.iSup_restrict_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (s : Set α) : ⨆ (i : ℕ), (μ.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.

def MeasureTheory.Measure.FiniteSpanningSetsIn.mono' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {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 := ⋯ }

def MeasureTheory.Measure.FiniteSpanningSetsIn.mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {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' ⋯

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

theorem MeasureTheory.Measure.sigmaFinite_of_countable {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {S : Set (Set α)} (hc : S.Countable) (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 : μ.FiniteSpanningSetsIn C) : ν.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 100]

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

• ⋯ = ⋯

instance MeasureTheory.instSigmaFiniteRestrictUnionSet {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} [MeasureTheory.SigmaFinite (μ.restrict s)] : MeasureTheory.SigmaFinite (μ.restrict (s ∩ t))

Equations

• ⋯ = ⋯

instance MeasureTheory.instSigmaFiniteRestrictInterSet_1 {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {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 : MeasurableSpace α} [MeasurableSpace β] (μ : MeasureTheory.Measure α) {f : α → β} (hf : AEMeasurable f μ) (h : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ)) : MeasureTheory.SigmaFinite μ

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

theorem MeasurableEquiv.sigmaFinite_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} (f : α ≃ᵐ β) [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 : α) ∂μ.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 : α) ∂μ.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 : α), μ.FiniteAtFilter (nhds x)

theorem MeasureTheory.IsLocallyFiniteMeasure.finiteAtNhds {α : Type u_1} {m0 : MeasurableSpace α} : ∀ {inst : TopologicalSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.IsLocallyFiniteMeasure μ] (x : α), μ.FiniteAtFilter (nhds x)

@[instance 100]

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 : α) : μ.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 MeasureTheory.IsFiniteMeasureOnCompacts.lt_top_of_isCompact {α : Type u_1} {m0 : MeasurableSpace α} : ∀ {inst : TopologicalSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃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 (μ.restrict s)

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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)

@[deprecated MeasureTheory.measure_null_of_locally_null]

theorem MeasureTheory.null_of_locally_null {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} [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_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 : μ.FiniteSpanningSetsIn {s : Set α | MeasurableSet s}) : μ.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

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

theorem MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (S : μ.FiniteSpanningSetsIn {s : Set α | MeasurableSet s}) : S.disjointed.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 : μ.FiniteSpanningSetsIn {s : Set α | MeasurableSet s}) (T : ν.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) : μ.FiniteAtFilter g → μ.FiniteAtFilter f

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

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

@[simp]

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

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

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

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

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

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

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

@[simp]

theorem MeasureTheory.Measure.finiteAt_principal {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} : μ.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, μ.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, μ.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 100]

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 μ] → μ.FiniteSpanningSetsIn {K : Set α | IsCompact K}

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

Equations

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

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

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

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

@[irreducible]

noncomputable def MeasureTheory.Measure.finiteSpanningSetsInOpen' {α : Type u_5} [TopologicalSpace α] [SecondCountableTopology α] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] : μ.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) < ⊤