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.

source

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

Prop

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

measure_univ_lt_top : ↑↑μ Set.univ < ⊤

Instances

source

theorem MeasureTheory.not_isFiniteMeasure_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} :

¬MeasureTheory.IsFiniteMeasure μ ↔ ↑↑μ Set.univ = ⊤

source

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

MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.restrict μ s)

Equations

⋯ = ⋯

source

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

↑↑μ s < ⊤

source

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

MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.restrict μ s)

Equations

⋯ = ⋯

source

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

↑↑μ s ≠ ⊤

source

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ᶜ + ε

source

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 + ε

source

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

source

@[simp]

theorem MeasureTheory.coe_measureUnivNNReal {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] :

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

source

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

MeasureTheory.IsFiniteMeasure 0

Equations

⋯ = ⋯

source

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

MeasureTheory.IsFiniteMeasure μ

Equations

⋯ = ⋯

source

@[simp]

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

MeasureTheory.measureUnivNNReal 0 = 0

source

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

MeasureTheory.IsFiniteMeasure (μ + ν)

Equations

⋯ = ⋯

source

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

MeasureTheory.IsFiniteMeasure (r • μ)

Equations

⋯ = ⋯

source

instance MeasureTheory.IsFiniteMeasure.average {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} :

MeasureTheory.IsFiniteMeasure ((↑↑μ Set.univ)⁻¹ • μ)

Equations

⋯ = ⋯

source

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

⋯ = ⋯

source

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

MeasureTheory.IsFiniteMeasure ν

source

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

source

@[simp]

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

MeasureTheory.measureUnivNNReal μ = 0 ↔ μ = 0

source

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

0 < MeasureTheory.measureUnivNNReal μ

source

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.

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Instances

source

theorem MeasureTheory.isProbabilityMeasure_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} :

MeasureTheory.IsProbabilityMeasure μ ↔ ↑↑μ Set.univ = 1

source

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

MeasureTheory.IsFiniteMeasure μ

Equations

⋯ = ⋯

source

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

μ ≠ 0

source

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

NeZero μ

Equations

⋯ = ⋯

source

theorem MeasureTheory.IsProbabilityMeasure.ae_neBot {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] :

Filter.NeBot (MeasureTheory.Measure.ae μ)

source

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

↑↑μ s + ↑↑μ sᶜ = 1

source

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

↑↑μ s ≤ 1

source

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

MeasureTheory.IsProbabilityMeasure ((↑↑μ Set.univ)⁻¹ • μ)

Equations

⋯ = ⋯

source

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

source

@[simp]

theorem MeasureTheory.one_le_prob_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] :

1 ≤ ↑↑μ s ↔ ↑↑μ s = 1

source

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

source

theorem MeasureTheory.prob_compl_eq_one_sub {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (hs : MeasurableSet s) :

↑↑μ sᶜ = 1 - ↑↑μ s

source

@[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

source

@[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

source

@[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

source

@[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

source

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

source

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

source

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

source

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

source

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

source

instance MeasureTheory.isProbabilityMeasure_map_up {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] :

MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map ULift.up μ)

Equations

⋯ = ⋯

source

instance MeasureTheory.isProbabilityMeasure_comap_down {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] :

MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.comap ULift.down μ)

Equations

⋯ = ⋯

source

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

Instances

source

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

↑↑μ s = 0

source

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

MeasureTheory.Measure.restrict μ {a} = 0

source

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

MeasureTheory.NoAtoms (MeasureTheory.Measure.restrict μ s)

Equations

⋯ = ⋯

source

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

↑↑μ s = 0

source

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

∀ᵐ (x : α) ∂μ, x ∉ s

source

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ᶜ = μ

source

@[simp]

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

MeasureTheory.Measure.restrict μ {a}ᶜ = μ

source

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

↑↑μ s = 0

source

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

↑↑μ ↑s = 0

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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

source

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

source

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

source

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

source

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

MeasureTheory.Measure.FiniteAtFilter μ f

source

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

source

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

MeasureTheory.Measure.FiniteAtFilter μ ⊥

source

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

source

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

Instances

source

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 ⋯

Instances For

MeasureTheory.isFiniteMeasure_sFiniteSeq

source

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

MeasureTheory.IsFiniteMeasure (MeasureTheory.sFiniteSeq μ n)

Equations

⋯ = ⋯

source

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

MeasureTheory.Measure.sum (MeasureTheory.sFiniteSeq μ) = μ

source

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.

source

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

⋯ = ⋯

source

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)

Instances

source

theorem MeasureTheory.sigmaFinite_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} :

MeasureTheory.SigmaFinite μ ↔ Nonempty (MeasureTheory.Measure.FiniteSpanningSetsIn μ Set.univ)

source

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

Nonempty (MeasureTheory.Measure.FiniteSpanningSetsIn μ Set.univ)

source

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

source

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

source

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

Monotone (MeasureTheory.spanningSets μ)

source

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

MeasurableSet (MeasureTheory.spanningSets μ i)

source

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

↑↑μ (MeasureTheory.spanningSets μ i) < ⊤

source

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

⋃ (i : ℕ), MeasureTheory.spanningSets μ i = Set.univ

source

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

IsCountablySpanning (Set.range (MeasureTheory.spanningSets μ))

source

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 ⋯

source

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

Measurable (MeasureTheory.spanningSetsIndex μ)

source

theorem MeasureTheory.preimage_spanningSetsIndex_singleton {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (n : ℕ) :

MeasureTheory.spanningSetsIndex μ ⁻¹' {n} = disjointed (MeasureTheory.spanningSets μ) n

source

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

source

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

x ∈ disjointed (MeasureTheory.spanningSets μ) (MeasureTheory.spanningSetsIndex μ x)

source

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

x ∈ MeasureTheory.spanningSets μ (MeasureTheory.spanningSetsIndex μ x)

source

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

source

theorem MeasureTheory.eventually_mem_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (x : α) :

∀ᶠ (n : ℕ) in Filter.atTop, x ∈ MeasureTheory.spanningSets μ n

source

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)) = μ

source

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

MeasureTheory.SFinite μ

Equations

⋯ = ⋯

source

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

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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

source

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

source

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

source

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

source

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

source

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.

source

@[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

source

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

source

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 ⋯

source

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.

source

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.

source

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

IsCountablySpanning C

source

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 μ

source

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

source

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

MeasureTheory.SigmaFinite ν

source

@[simp]

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

μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂

source

@[simp]

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

ν₁ + μ = ν₂ + μ ↔ ν₁ = ν₂

source

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

MeasureTheory.SigmaFinite μ

Every finite measure is σ-finite.

Equations

⋯ = ⋯

source

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

MeasureTheory.SigmaFinite μ ↔ MeasureTheory.IsFiniteMeasure μ

source

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

MeasureTheory.SigmaFinite (MeasureTheory.Measure.restrict μ s)

Equations

⋯ = ⋯

source

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

⋯ = ⋯

source

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

MeasureTheory.SigmaFinite (μ + ν)

Equations

⋯ = ⋯

source

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

MeasureTheory.SigmaFinite (c • μ)

Equations

⋯ = ⋯

source

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 μ

source

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

source

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.

source

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.

source

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)

Instances

source

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

MeasureTheory.IsLocallyFiniteMeasure μ

Equations

⋯ = ⋯

source

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

MeasureTheory.Measure.FiniteAtFilter μ (nhds x)

source

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

MeasureTheory.IsFiniteMeasure (c • μ)

source

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

source

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

MeasureTheory.IsLocallyFiniteMeasure (c • μ)

Equations

⋯ = ⋯

source

theorem MeasureTheory.Measure.isTopologicalBasis_isOpen_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] :

TopologicalSpace.IsTopologicalBasis {s : Set α | IsOpen s ∧ ↑↑μ s < ⊤}

source

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

Instances

source

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.

source

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.

source

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.

source

theorem MeasureTheory.measure_closedBall_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ} :

↑↑μ (Metric.closedBall x r) < ⊤

source

theorem MeasureTheory.measure_ball_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ} :

↑↑μ (Metric.ball x r) < ⊤

source

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

MeasureTheory.IsFiniteMeasureOnCompacts (c • μ)

source

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

MeasureTheory.IsFiniteMeasureOnCompacts (c • μ)

Equations

⋯ = ⋯

source

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

MeasureTheory.IsFiniteMeasureOnCompacts (MeasureTheory.Measure.restrict μ s)

Equations

⋯ = ⋯

source

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

MeasureTheory.IsFiniteMeasure μ

Equations

⋯ = ⋯

source

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

MeasureTheory.SigmaFinite μ

Equations

⋯ = ⋯

source

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

MeasureTheory.SigmaFinite μ

Equations

⋯ = ⋯

source

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

⋯ = ⋯

source

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)

source

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)

source

theorem MeasureTheory.exists_pos_ball {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PseudoMetricSpace α] (x : α) (hμ : μ ≠ 0) :

∃ (n : ℕ), 0 < ↑↑μ (Metric.ball x ↑n)

source

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.

source

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

source

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)

source

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.

source

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

source

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

source

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

source

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)

source

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

source

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)

source

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)

source

@[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

source

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.

source

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

source

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

source

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

source

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

source

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)

source

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

MeasureTheory.Measure.FiniteAtFilter μ (nhdsWithin x s)

source

@[simp]

theorem MeasureTheory.Measure.finiteAt_principal {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} :

MeasureTheory.Measure.FiniteAtFilter μ (Filter.principal s) ↔ ↑↑μ s < ⊤

source

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

MeasureTheory.IsLocallyFiniteMeasure ν

source

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.

source

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.

source

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

source

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

source

instance isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure {α : Type u_1} [TopologicalSpace α] :

∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsLocallyFiniteMeasure μ], MeasureTheory.IsFiniteMeasureOnCompacts μ

Equations

⋯ = ⋯

source

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

MeasureTheory.IsFiniteMeasure μ ↔ MeasureTheory.IsFiniteMeasureOnCompacts μ

source

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

source

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

source

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

source

@[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

source

theorem measure_Icc_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} :

↑↑μ (Set.Icc a b) < ⊤

source

theorem measure_Ico_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} :

↑↑μ (Set.Ico a b) < ⊤

source

theorem measure_Ioc_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} :

↑↑μ (Set.Ioc a b) < ⊤

source

theorem measure_Ioo_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} :

↑↑μ (Set.Ioo a b) < ⊤

Documentation

Mathlib.MeasureTheory.Measure.Typeclasses

Classes of measures #