Uniform laws on expanding finite grids converge to uniform zero one

The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$): The Axiom of Countable Choice, written ${\mathrm{A}\mathrm{C}}_{\omega }$, is the following statement.

For every family $(X_n{)}_{n\in \mathbb{N}}$ of nonempty sets indexed by $\mathbb{N}$ there is a function $f$ with domain $\mathbb{N}$ such that $f(n)\in X_n$ for every $n\in \mathbb{N}$.

Equivalently, in the vocabulary of def-choice-function: every at most countable family of nonempty sets (def-countable) has a choice function.

A box in ${\mathbb{R}}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure ${\prod }_{i<n}(b_i-a_i)$, whichever of its faces are included: Let $n\ge 1$, assume the Axiom of Countable Choice (def-countable-choice), and let $a_i\le b_i$ be reals for $i<n$. Write

$R^{\circ }:=\{x\in {\mathbb{R}}^n:a_i<x_i<b_i\text{ for every }i<n\},\bar{R}:=[a,b]=\{x\in {\mathbb{R}}^n:a_i\le x_i\le b_i\text{ for every }i<n\}$

(def-multidimensional-rectangle-and-volume). Then $R^{\circ }$ is open and $\bar{R}$ is closed, so both are Borel and Lebesgue measurable, and every set $R$ with $R^{\circ }\subseteq R\subseteq \bar{R}$ is Lebesgue measurable with

${\lambda }_n(R)={\prod }_{i<n}(b_i-a_i)\mathrm{.}$

In particular this covers the four one-dimensional face conventions in each coordinate — the open box, the closed box $[a,b]$, the half-open box $B(a,b)={\prod }_{i<n}(a_i,b_i]$ of def-half-open-box, and every mixture of them, in any combination of coordinates — and it gives measure $0$ to all of them whenever $a_i=b_i$ for some $i<n$. For a half-open box with infinite parameters the value is already ${\lambda }_n(B)=\mathrm{vol}(B)$ (thm-lebesgue-measure-is-a-complete-measure).

The nonnegative integral agrees with the simple integral on simple functions: If $s$ is a nonnegative simple measurable function, then its nonnegative Lebesgue integral equals its simple integral: $\int sd\mu ={\int }_{\mathrm{s}\mathrm{i}\mathrm{m}\mathrm{p}\mathrm{l}\mathrm{e}}sd\mu \mathrm{.}$

Heine-Cantor in $\mathbb{R}$: a continuous real function on a compact subset of $\mathbb{R}$ is uniformly continuous, proved $\mathbb{R}$-natively from sequential compactness: Let $K\subseteq \mathbb{R}$ be compact (def-open-cover-r) and let $f:K\to \mathbb{R}$ be continuous on $K$ (def-continuity-real). Then $f$ is uniformly continuous on $K$ (def-uniform-continuity-real).

This theorem is stated twice in this library, on purpose. Its metric-space twin is thm-heine-cantor-metric, proved there from the cover machinery of metric spaces; the proof below is $\mathbb{R}$-native and runs through thm-compact-iff-sequentially-compact-r, which is order-based. That the two statements are the same statement in two vocabularies is lem-real-and-metric-notions-agree, clauses 1, 2 and 5, immediately above.

The choice cost, named. The proof invokes the axiom of countable choice (def-countable-choice) exactly once, at step 3.1, to select one bad pair of points from each of countably many nonempty sets. The backward implication of thm-compact-iff-sequentially-compact-r also spends countable choice, and that item names its own uses; the forward implication used here, from compact to sequentially compact, does not. No claim is made that the axiom is necessary for either.

The Lebesgue integral is linear on $L^1(\mu )$: The class $L^1(\mu )$ is a complex vector space, and the Lebesgue integral is complex-linear on it: $\int (\alpha f+\beta g)d\mu =\alpha \int fd\mu +\beta \int gd\mu (\alpha ,\beta \in \mathbb{C},f,g\in L^1(\mu ))\mathrm{.}$

The modulus of an integral is bounded by the integral of the modulus: If $f\in L^1(\mu )$, then $\mid \int fd\mu \mid \le \int \mathrm{\mid }f\mathrm{\mid }d\mu \mathrm{.}$

Weak convergence of borel probability measures: For Borel probability measures ${\mu }_n,\mu$ on a metric space S, write ${\mu }_n\Rightarrow \mu$ if $\int fd{\mu }_n\to \int fd\mu$ for every bounded continuous real function f on S. Continuity is def-metric-continuity. Such f is Borel measurable (inverse images of open sets are open) and $\int \mathrm{\mid }f\mathrm{\mid }d\mu \le \mathrm{\parallel }f{\mathrm{\parallel }}_{\mathrm{\infty }}\mu (S)<\mathrm{\infty }$, so the integrals are finite in def-integrable-real-and-complex-functions-and-their-integrals. No completeness or coupling is required.