Documentation

Atlas.IntroductionToFunctionalAnalysis.code.MeasureTheory

The collection of measurable sets in a measurable space forms a set algebra: it contains the empty set, is closed under complements, and closed under finite unions. This is the algebra-of-sets part of the σ-algebra structure.

theorem MeasureTheory.sigmaAlgebra_finite_union_mem {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} {f : ιSet α} (S : Finset ι) (hf : iS, MeasurableSet (f i)) :
MeasurableSet (⋃ iS, f i)

If sets $E_1, \dots, E_n$ are measurable, then $\bigcup_{k=1}^n E_k$ is measurable. Stated for an arbitrary finite indexing Finset.

theorem MeasureTheory.exists_disjoint_seq_with_same_union {α : Type u_1} [MeasurableSpace α] (E : Set α) (hE : ∀ (n : ), MeasurableSet (E n)) :
∃ (F : Set α), (∀ (n : ), MeasurableSet (F n)) Pairwise (Function.onFun Disjoint F) ⋃ (n : ), F n = ⋃ (n : ), E n

Let $\mathcal{A}$ be an algebra (here, a σ-algebra), and let $\{E_n\}$ be a countable collection of measurable sets. Then there exists a pairwise disjoint countable collection $\{F_n\}$ of measurable sets such that $\bigcup_n E_n = \bigcup_n F_n$.

The Lebesgue (null-)measurable subsets of $\mathbb{R}$ form a σ-algebra: the empty set is measurable, complements of measurable sets are measurable, and countable unions of measurable sets are measurable.

theorem MeasureTheory.continuity_measure_increasing {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {E : Set α} (hE : Monotone E) :
Filter.Tendsto (fun (n : ) => μ (E n)) Filter.atTop (nhds (μ (⋃ (n : ), E n)))

Continuity of measure for increasing sequences: if $E_1 \subset E_2 \subset \cdots$ is an increasing sequence of measurable sets, then $\mu\left(\bigcup_{k=1}^{\infty} E_k\right) = \lim_{n \to \infty} \mu(E_n)$.

theorem MeasureTheory.measurable_of_pointwise_limit {α : Type u_1} [MeasurableSpace α] {f : αEReal} {g : αEReal} (hf : ∀ (n : ), Measurable (f n)) (hlim : ∀ (x : α), Filter.Tendsto (fun (n : ) => f n x) Filter.atTop (nhds (g x))) :

The pointwise limit of measurable functions is measurable: if $f_n : \alpha \to \overline{\mathbb{R}}$ are measurable and $f_n(x) \to g(x)$ for all $x$, then $g$ is measurable.

theorem MeasureTheory.simpleFunc_closed_scalar_add_mul {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [AddCommMonoid β] [Mul β] {K : Type u_3} [SMul K β] :
(∀ (c : K) (f : SimpleFunc α β), ∃ (g : SimpleFunc α β), g = c f) (∀ (f g : SimpleFunc α β), ∃ (h : SimpleFunc α β), h = f + g) ∀ (f g : SimpleFunc α β), ∃ (h : SimpleFunc α β), h = f * g

Simple functions are closed under scalar multiplication, addition, and multiplication: for any simple functions $f, g$ and scalar $c$, the functions $c \cdot f$, $f + g$, and $f \cdot g$ are again simple functions.

theorem MeasureTheory.SimpleFunc.exists_monotone_tendsto {α : Type u_1} [MeasurableSpace α] {f : αENNReal} (hf : Measurable f) :
∃ (φ : SimpleFunc α ENNReal), ((∀ (n : ) (a : α), (φ n) a f a) Monotone fun (n : ) => (φ n)) (∀ (a : α), Filter.Tendsto (fun (n : ) => (φ n) a) Filter.atTop (nhds (f a))) ∀ (B : ENNReal), B ∀ (ε : ENNReal), ε 0∃ (N : ), nN, ∀ (a : α), f a Bf a - (φ n) a < ε

For any nonnegative measurable function $f : \alpha \to [0, \infty]$, there exists a sequence of simple functions $\{\varphi_n\}$ such that: (a) $0 \le \varphi_0(a) \le \varphi_1(a) \le \cdots \le f(a)$ for all $a$ (pointwise increasing and dominated by $f$); (b) $\varphi_n(a) \to f(a)$ pointwise; and (c) for every bound $B < \infty$ and every $\varepsilon > 0$, there is an $N$ such that $f(a) - \varphi_n(a) < \varepsilon$ for all $n \ge N$ and all $a$ with $f(a) \le B$ (uniform convergence on sets where $f$ is bounded).

For all $a \in \mathbb{R}$, the open interval $(a, \infty)$ is measurable.