Physlib

PhyslibAlpha.Mathematics.MeasureTheory.RegularMeasure

Regular measures

i. Overview

A measure is regular when the measure of a set is approximated by compact sets from inside and by open sets from outside. For finite measures on a Hausdorff space the inner approximation is enough. Inner regularity passes to smaller measures, along continuous maps and to measurable subsets, and so regularity does too.

ii. Key results

- `MeasureTheory.Measure.InnerRegular.of_le` proves that a measure below a finite inner regular measure is inner regular. - `MeasureTheory.Measure.Regular.of_innerRegular` proves that a finite inner regular measure is regular. - `MeasureTheory.Measure.Regular.map_of_continuous` proves that regularity passes along continuous maps. - `MeasureTheory.Measure.InnerRegular.comap_subtype` proves that inner regularity passes to measurable subsets.

iii. Table of contents

  • A. Measures below inner regular measures
  • B. Regularity from inner regularity

A. Measures below inner regular measures

B. Regularity from inner regularity

5 declarations

theorem

If ν≤μ\nu \le \mu and μ\mu is finite and inner regular, then ν\nu is inner regular

Let α\alpha be a Hausdorff space where every open set is measurable. Let μ\mu be a finite, inner regular measure on α\alpha. If ν\nu is a measure on α\alpha such that ν≤μ\nu \le \mu (meaning ν(A)≤μ(A)\nu(A) \le \mu(A) for every measurable set AA), then ν\nu is also inner regular.

theorem

Finite inner regular measures are regular

Let α\alpha be a Hausdorff space equipped with the Borel σ\sigma-algebra. If μ\mu is a finite inner regular measure on α\alpha, then μ\mu is a regular measure.

theorem

ν≤μ  ⟹  ν\nu \leq \mu \implies \nu is regular for finite inner regular μ\mu on a Hausdorff space

Let α\alpha be a Hausdorff space equipped with the Borel σ\sigma-algebra. Let μ\mu be a finite, inner regular measure on α\alpha. If ν\nu is another measure such that ν≤μ\nu \leq \mu (meaning ν(A)≤μ(A)\nu(A) \leq \mu(A) for all measurable sets AA), then ν\nu is a regular measure.

theorem

The pushforward of a finite regular measure along a continuous map is regular

Let α\alpha be a topological space and β\beta be a Hausdorff (T2T_2) topological space, both equipped with their Borel σ\sigma-algebras. Let μ\mu be a finite regular measure on α\alpha. If f:α→βf : \alpha \to \beta is a continuous map, then the pushforward measure f∗μf_* \mu is a regular measure on β\beta.

theorem

Inner regularity is preserved on measurable subsets

Let μ\mu be an inner regular measure on a topological space α\alpha. For any measurable subset s⊆αs \subseteq \alpha, the measure obtained by the comap of μ\mu along the inclusion map ι:s→α\iota : s \to \alpha is also inner regular.