Documentation

Mathlib.MeasureTheory.Measure.Filter

This file provides some properties of ae the filter of sets whose complement has measure 0. Most of these properties are in this file because they either require the module structure or the lattice structure of the space of measures.

We also define cofinite the filter of sets whose complement has finite measure.

Tags #

measure, almost everywhere, cofinite

@[simp]

theorem MeasureTheory.ae_eq_bot {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} :

ae μ = ⊥ ↔ μ = 0

@[simp]

theorem MeasureTheory.ae_neBot {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} :

(ae μ).NeBot ↔ μ ≠ 0

instance MeasureTheory.instNeBotAeMeasureOfNeZero {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [NeZero μ] :

@[simp]

theorem MeasureTheory.ae_zero {α : Type u_1} {mα : MeasurableSpace α} :

theorem MeasureTheory.ae_mono {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} (h : μ ≤ ν) :

ae μ ≤ ae ν

instance MeasureTheory.instIsMeasurablyGeneratedAeMeasure {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} :

(ae μ).IsMeasurablyGenerated

theorem MeasureTheory.AEDisjoint.of_le {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} {s t : Set α} (h : AEDisjoint μ s t) (h' : ν ≤ μ) :

AEDisjoint ν s t

theorem MeasureTheory.NullMeasurableSet.mono {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} {s : Set α} (h : NullMeasurableSet s μ) (h' : ν ≤ μ) :

NullMeasurableSet s ν

theorem MeasureTheory.NullMeasurableSet.smul_measure {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {s : Set α} (h : NullMeasurableSet s μ) (c : ENNReal) :

NullMeasurableSet s (c • μ)

theorem MeasureTheory.nullMeasurableSet_smul_measure_iff {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {s : Set α} {c : ENNReal} (hc : c ≠ 0) :

NullMeasurableSet s (c • μ) ↔ NullMeasurableSet s μ

theorem AEMeasurable.mono_measure {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α} {f : α → β} (h : AEMeasurable f μ) (h' : ν ≤ μ) :

AEMeasurable f ν

theorem MeasureTheory.Measure.measure_support_eq_zero_iff {α : Type u_1} {mα : MeasurableSpace α} {E : Type u_3} [Zero E] (μ : Measure α := by volume_tac) {f : α → E} :

μ (Function.support f) = 0 ↔ f =ᵐ[μ] 0

The `cofinite` filter #

def MeasureTheory.Measure.cofinite {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) :

The filter of sets s such that sᶜ has finite measure.

Equations

μ.cofinite = Filter.comk (fun (x : Set α) => μ x < ⊤) ⋯ ⋯ ⋯

Instances For

theorem MeasureTheory.Measure.mem_cofinite {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {s : Set α} :

s ∈ μ.cofinite ↔ μ sᶜ < ⊤

theorem MeasureTheory.Measure.compl_mem_cofinite {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {s : Set α} :

sᶜ ∈ μ.cofinite ↔ μ s < ⊤

theorem MeasureTheory.Measure.eventually_cofinite {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {p : α → Prop} :

(∀ᶠ (x : α) in μ.cofinite, p x) ↔ μ {x : α | ¬p x} < ⊤

instance MeasureTheory.Measure.instIsMeasurablyGeneratedCofinite {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} :

μ.cofinite.IsMeasurablyGenerated

theorem MeasureTheory.Measure.cofinite_le_ae {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} :

μ.cofinite ≤ ae μ