leroy

1.4 Caratheodory Extnesion on Locales

Definition 30 Measure on Locales
✓
#

Uses

Lean declarations

A measure on a local \(X\) is a map \(\mu : O(X) \to [0,\infty )\) such that:

  1. \(\mu (\emptyset ) = 0\)

  2. \(U \subset V \implies \mu (U) \le \mu (V)\)

  3. \(\mu (U \cup V) = \mu (U) + \mu (V) - \mu (V \cap V)\)

  4. For any increasingly filtered family \(V_i\) of open sublocals of \(X\), we have:

    \[ \mu (\bigcup V_i) = \sup _i \mu (V_i) \]

    this means: For all \(i\) and \(j\) there exists a \(k\) such that \(V_i \cup V_j \subset V_k\) bzw. \(V_i \subset V_k\) and \(V_j \subset V_k\).

(Leroy III.1.)

Definition 31 Caratheodory
✓
#

Uses

Lean declarations

For any measure \(\mu \) on a local \(X\), the caratheodory extension is:

\[ \mu (A) = \inf \{ \mu (U) | A \subset U \in O(X)\} ,~ A\in X \]
Lemma 32 Proptery 0 (Commutes with sup)
✓
#

Uses

(Leroy lemme 3.1) The caratheodory extension of a measure on a local commutes with unions of increasing families.

Proof ▶
Lemma 33 Caratheodory Extensions are monotonic
✓
#

Uses

Lean declarations

The caratheodory extension is monotonic i.e.

\[ A \le B \implies \mu (A) \le \mu (B) \]
Proof ▶

This is a direct consequence of the definition of the caratheodory extension.

Lemma 34 Subadditivity
✓
#

Uses

Lean declarations

The Caratheodory extension is subaddtive:

\[ \mu (A \cup B) \le \mu (A) + \mu (B) \]
Proof ▶
Definition 35 Regular Local
✓
#

Uses

Lean declarations

A local is regular, if for all open sublocals \(U\) of \(E\), the open sublocals \(V\) such that \(V\bar\subset U\) recover \(U\).

Definition 36 Neighborhood
✓
#

Uses

Lean declarations

A neighborhood of a sublocal \(A\) of \(X\) is an open sublocal \(V\) of \(X\) such that \(A \le V\).

Lemma 37 Regularity of Sublocals
✓
#

Uses

Lean declarations

(Leroy lemme 3.2) In a regular local, any sublocal is regular, meaning that it is the intersection of all open neighborhoods.

Proof ▶
Lemma 38 Measure add compl eq top
✓
#

Uses

Lean declarations

(Leroy Lemme 3.3) For any open sublocal \(U\) of a local \(X\), the caratheodory extension of a measure on \(X\) satisfies

\[ \mu (U) + \mu (X \setminus U) = \mu (X) \]
Proof ▶

Siehe Leroy

Lemma 39 Restriction
✓
#

Uses

Lean declarations

The Restriction of a Measure to any open Sublocal is a Measure.

Proof ▶
Lemma 40 Property 2
✓
#

Uses

Lean declarations

(Leroy Lemm 3.4) For any open sublocal \(U\) and any sublocal \(A\) of a local \(E\), the caratheodory extension of a measure on \(X\) satisfies

\[ \mu (A) = \mu (A \cap U) + \mu (A \cap (E\setminus U)) \]
Proof ▶

Siehe Leroy

Lemma 41 Property 3
✓
#

Uses

Lean declarations

(Leroy Lemm 3.5) For a increasing family \(V_{\alpha }\) of open sublocals of \(E\) and any sublocal \(A\), we have:

\[ \mu (A \cap (\bigcup V_{\alpha })) = \sup _\alpha \mu (A\cap V_\alpha ) \]
Proof ▶
Lemma 42 Restriction to a Sublocale
✓
#

Uses

Lean declarations

Let \(A\) be a sublocale of \(E\) with the embedding \(i : A \rightarrow E\). The restriction of a measure \(\mu \) on \(E\) to \(A\) is a measure on \(A\):

\[ V \mapsto \mu (i(V)) : Open(A) \to \mathbb {R} \]
Proof ▶
Proposition 43 strictly additve
✓
#

Uses

Lean declarations

(Leroy theorem 3.3.1) For any measure on a local \(X\), the caratheodory extension is strictly additive, i.e. \(\mu (A \cup B) = \mu (A) + \mu (B) - \mu (A \cap B)\).

Proof ▶
Proposition 44 reductive
✓
#

Uses

(Proposition 3.3.1) For any measure on a local \(X\), the caratheodory extension is reductive, i.e. for all \(A \le X\) the set \(\{ A' \subset A, \mu (A') = \mu (A)\} \) has a minimal element.

Proof ▶
Lemma 45 Commutes with inf opens
✓
#

Uses

Lean declarations

(Leroy Lemme 3.6) For any measure on a local \(X\) and a decreasing family \((V_i)_{i\in I}\) of open sublocals, the caratheodory extension fulfills: \(\mu (\inf _{i\in I} V_i) = \inf _{i\in I} \mu (V_i)\).

Proof ▶
Proposition 46 Commutes with inf
✓
#

Uses

(Leroy lemme 3.7 et principal) For any measure on a local \(X\), the caratheodory extension is regular \(\mu (\inf _{i\in I} A_i) = \inf {i\in I} \mu (A_i)\). For decreasing families \((A_i)_{i\in I}\)

Proof ▶
Theorem 47 Main Theorem (very important)
✓
#

Uses

For any measure on a local \(X\), the caratheodory extension is

  1. strictly additiv, i.e. \(\mu (A \cup B) = \mu (A) + \mu (B) - \mu (A \cap B)\) for all \(A,B\in X\),

  2. commutes with inf \(\mu (\inf _{i\in \mathbb {N}} A_i) = \inf _{i\in \mathbb {N}} \mu (A_i)\) for a familiy \((A_i)_{i\in \mathbb {N}}\) of elements \(A_i\in X\),

  3. reductive, i.e. for all \(A \le X\) the set \(\{ A' \subset A, \mu (A') = \mu (A)\} \) has a minimal element.

Proof ▶