# Theory Measure

subsection ‹Measure spaces \label{sec:measure-spaces}›

theory Measure
imports Sigma_Algebra MonConv
begin

(*We use a modified version of the simple Sigma_Algebra Theory by
Markus Wenzel here,
which does not need an explicit definition of countable,
changing the names according to Joe Hurd*)
text ‹Now we are already set for the central concept of
measure. The following definitions are translated as faithfully as possible
from those in Joe Hurd's thesis \cite{hurd2002}.›

definition
measurable:: "'a set set ⇒ 'b set set ⇒ ('a ⇒ 'b) set" where
"measurable F G = {f. ∀g∈G. f - g ∈ F}"

text ‹So a function is called $F$-$G$-measurable if and only if the inverse
image of any set in $G$ is in $F$. $F$ and $G$ are usually the sets of
measurable sets, the first component of a measure space\footnote{In
standard mathematical notation, the universe is first in a
measure space triple, but in our definitions, following Joe Hurd, it is always the
whole type universe and therefore omitted.}.›

definition
measurable_sets:: "('a set set * ('a set ⇒ real)) ⇒ 'a set set" where
"measurable_sets = fst"

definition
measure:: "('a set set * ('a set ⇒ real)) ⇒ ('a set ⇒ real)" where
"measure = snd"

text ‹The other component is the measure itself. It is a function that
assigns a nonnegative real number to every measurable set and has
the property of being

definition
positive:: "('a set set * ('a set ⇒ real)) ⇒ bool" where
"positive M ⟷ measure M {} = 0 ∧
(∀A. A∈ measurable_sets M ⟶ 0 ≤ measure M A)"
(*Remark: This definition of measure space is not minimal,
in the sense that the containment of the ⋃(the  in) measurable sets
is implied by the measurable sets being a sigma algebra*)

definition
countably_additive:: "('a set set * ('a set => real)) => bool" where
"countably_additive M ⟷ (∀f::(nat => 'a set). range f ⊆ measurable_sets M
∧ (∀m n. m ≠ n ⟶ f m ∩ f n = {}) ∧  (⋃i. f i) ∈ measurable_sets M
⟶ (λn. measure M (f n)) sums  measure M (⋃i. f i))"

text ‹This last property deserves some comments. The conclusion is
usually --- also in the aforementioned source --- phrased as

‹measure M (⋃i. f i) = (∑n. measure M (f n))›.

In our formal setting this is unsatisfactory, because the
sum operator\footnote{Which is merely syntactic sugar for the
\isa{suminf} functional from the \isa{Series} theory
\cite{Fleuriot:2000:MNR}.}, like any HOL function, is total, although
a series obviously need not converge. It is defined using the ‹ε› operator, and its
behavior is unspecified in the diverging case. Hence, the above assertion
would give no information about the convergence of the series.

Furthermore, the definition contains redundancy. Assuming that the
countable union of sets is measurable is unnecessary when the
measurable sets form a sigma algebra, which is postulated in the
final definition\footnote{Joe Hurd inherited this practice from a very
influential probability textbook \cite{Williams.mart}}.
›

definition
measure_space:: "('a set set * ('a set ⇒ real)) ⇒ bool" where
"measure_space M ⟷ sigma_algebra (measurable_sets M) ∧

text ‹Note that our definition is restricted to finite measure
spaces --- that is, ‹measure M UNIV < ∞› --- since the measure
must be a real number for any measurable set. In probability, this
is naturally the case.

Two important theorems close this section. Both appear in
Hurd's work as well, but are shown anyway, owing to their central
role in measure theory. The first one is a mighty tool for proving measurability. It states
that for a function mapping one sigma algebra into another, it is
sufficient to be measurable regarding only a generator of the target
sigma algebra. Formalizing the interesting proof out of Bauer's
textbook \cite{Bauer} is relatively straightforward using rule
induction.›

theorem assumes sig: "sigma_algebra a" and meas: "f ∈ measurable a b" shows
measurable_lift: "f ∈ measurable a (sigma b)"
proof -
define Q where "Q = {q. f - q ∈ a}"
with meas have 1: "b ⊆ Q" by (auto simp add: measurable_def)

{ fix x assume "x∈sigma b"
hence "x∈Q"
proof (induct rule: sigma.induct)
case basic
from 1 show " ⋀a. a ∈ b ⟹ a ∈ Q" ..
next
case empty
from sig have "{}∈a"
by (simp only: sigma_algebra_def)
thus "{} ∈ Q"
next
case complement
fix r assume "r ∈ Q"
then obtain r1 where im: "r1 = f - r" and a: "r1 ∈ a"
with sig have "-r1 ∈ a"
by (simp only: sigma_algebra_def)
with im Q_def show "-r ∈ Q"
next
case Union
fix r assume "⋀i::nat. r i ∈ Q"
then obtain r1 where im: "⋀i. r1 i =  f - r i" and a: "⋀i. r1 i ∈        a"
from a sig have "⋃(r1  UNIV) ∈ a"
by (auto simp only: sigma_algebra_def)
with im Q_def show "⋃(r  UNIV) ∈ Q"
qed }

hence "(sigma b) ⊆ Q" ..
thus "f ∈ measurable a (sigma b)"
by (auto simp add: measurable_def Q_def)
qed

text ‹The case is different for the second theorem. It is only five
lines in the book (ibid.), but almost 200 in formal text. Precision
still pays here, gaining a detailed view of a technique that
is often employed in measure theory --- making a sequence of sets
disjoint. Moreover, the necessity for the above-mentioned change in the
definition of countably additive was detected only in the
formalization of this proof.

To enable application of the additivity of measures, the following construction
yields disjoint sets. We skip the justification of the lemmata for
brevity.›

primrec mkdisjoint:: "(nat ⇒ 'a set) ⇒ (nat ⇒ 'a set)"
where
"mkdisjoint A 0 = A 0"
| "mkdisjoint A (Suc n) = A (Suc n) - A n"

lemma mkdisjoint_un:
assumes up: "⋀n. A n ⊆ A (Suc n)"
shows "A n = (⋃i∈{..n}. mkdisjoint A i)"
(*<*)proof (induct n)
case 0 show ?case by simp
next
case (Suc n)
hence "A n = (⋃i∈{..n}. mkdisjoint A i)" .
moreover
have "(⋃i∈{..(Suc n)}. mkdisjoint A i) = mkdisjoint A (Suc n) ∪
(⋃i∈{..n}. mkdisjoint A i)" by (simp add: atMost_Suc)
moreover
have "mkdisjoint A (Suc n) ∪ A n = A (Suc n) ∪ A n" by simp
moreover
from up have "… = A (Suc n)" by auto
ultimately
show ?case by simp
qed(*>*)

lemma mkdisjoint_disj:
assumes up: "⋀n. A n ⊆ A (Suc n)" and ne: "m ≠ n"
shows "mkdisjoint A m ∩ mkdisjoint A n = {}"
(*<*)proof -
{ fix m1 m2::nat assume less: "m1 < m2"
hence "0 < m2" by simp
then obtain n where eq: "m2 = Suc n" by (auto simp add: gr0_conv_Suc)
with less have less2: "m1 < Suc n" by simp

{
fix y assume y: "y ∈ mkdisjoint A m1"
fix x assume x: "x ∈ mkdisjoint A m2"
with eq have"x ∉ A n" by simp
also from up have "A n = (⋃i∈{..n}. mkdisjoint A i)"
by (rule mkdisjoint_un)
also
from less2 have "m1 ∈ {..n}" by simp
hence "mkdisjoint A m1 ⊆ (⋃i∈{..n}. mkdisjoint A i)" by auto
ultimately
have "x ∉ mkdisjoint A m1" by auto
with y have "y ≠ x" by fast
}
hence "mkdisjoint A m1 ∩ mkdisjoint A m2 = {}"
} hence 1: "⋀m1 m2. m1 < m2 ⟹  mkdisjoint A m1 ∩ mkdisjoint A m2 = {}" .

show ?thesis
proof (cases "m < n")
case True
thus ?thesis by (rule 1)
next
case False
with ne have "n < m" by arith
hence "mkdisjoint A n ∩ mkdisjoint A m = {}" by (rule 1)
thus ?thesis by fast
qed
qed(*>*)

lemma mkdisjoint_mon_conv:
assumes mc: "A↑B"
shows "(⋃i. mkdisjoint A i) = B"
(*<*)proof
{ fix x assume "x ∈ (⋃i. mkdisjoint A i)"
then obtain i where "x ∈ mkdisjoint A i" by auto
hence "x ∈ A i" by (cases i) simp_all
with mc have "x ∈ B" by (auto simp add: mon_conv_set_def)
}
thus "(⋃i. mkdisjoint A i) ⊆ B" by fast

{ fix x assume "x ∈ B"
with mc obtain i where "x ∈ A i" by (auto simp add: mon_conv_set_def)
also from mc have "⋀n. A n ⊆ A (Suc n)" by (simp only: mon_conv_set_def)
hence "A i = (⋃r∈{..i}. mkdisjoint A r)" by (rule mkdisjoint_un)
also have "… ⊆ (⋃r. mkdisjoint A r)" by auto
finally have "x ∈ (⋃i. mkdisjoint A i)".
}
thus "B ⊆ (⋃i. mkdisjoint A i)" by fast
qed(*>*)

(*This is in Joe Hurd's Thesis (p. 35) as Monotone Convergence theorem. Check the real name … .
Also, it's not as strong as it could be,
but we need no more.*)

text ‹Joe Hurd calls the following the Monotone Convergence Theorem,
though in mathematical literature this name is often reserved for a
similar fact
about integrals that we will prove in \ref{nnfis}, which depends on this
one. The claim made here is that the measures of monotonically convergent sets
approach the measure of their limit. A strengthened version would
imply monotone convergence of the measures, but is not needed in the
development.
›

theorem measure_mon_conv:
assumes ms: "measure_space M" and
Ams: "⋀n. A n ∈ measurable_sets M" and AB: "A↑B"
shows "(λn. measure M (A n)) ⇢ measure M B"
proof -

from AB have up: "⋀n. A n ⊆ A (Suc n)"
by (simp only: mon_conv_set_def)

{ fix i
have "mkdisjoint A i ∈ measurable_sets M"
proof (cases i)
case 0 with Ams show ?thesis by simp
next
case (Suc i)
have "A (Suc i) - A i = A (Suc i) ∩ - A i" by blast
with Suc ms Ams show ?thesis
by (auto simp add: measure_space_def sigma_algebra_def sigma_algebra_inter)
qed
}
hence i: "⋀i. mkdisjoint A i ∈ measurable_sets M" .

with ms have un: "(⋃i. mkdisjoint A i) ∈ measurable_sets M"
moreover
from i have range: "range (mkdisjoint A) ⊆ measurable_sets M"
by fast
moreover
from up have "∀i j. i ≠ j ⟶  mkdisjoint A i ∩ mkdisjoint A j = {}"
moreover note ms
ultimately
have sums:
"(λi. measure M (mkdisjoint A i)) sums (measure M (⋃i. mkdisjoint A i))"
hence "(∑i. measure M (mkdisjoint A i)) = (measure M (⋃i. mkdisjoint A i))"
by (rule sums_unique[THEN sym])

also
from sums have "summable (λi. measure M (mkdisjoint A i))"
by (rule sums_summable)

hence "(λn. ∑i<n. measure M (mkdisjoint A i))
⇢ (∑i. measure M (mkdisjoint A i))"
by (rule summable_LIMSEQ)

hence "(λn. ∑i<Suc n. measure M (mkdisjoint A i)) ⇢ (∑i. measure M (mkdisjoint A i))"
by (rule LIMSEQ_Suc)

ultimately have "(λn. ∑i<Suc n. measure M (mkdisjoint A i))
⇢ (measure M (⋃i. mkdisjoint A i))" by simp

also
{ fix n
from up have "A n = (⋃i∈{..n}. mkdisjoint A i)"
by (rule mkdisjoint_un)
hence "measure M (A n) = measure M (⋃i∈{..n}. mkdisjoint A i)"
by simp

also have
"(⋃i∈{..n}. mkdisjoint A i) = (⋃i. if i≤n then mkdisjoint A i else {})"
proof -
have "UNIV = {..n} ∪ {n<..}" by auto
hence "(⋃i. if i≤n then mkdisjoint A i else {}) =
(⋃i∈{..n}. if i≤n then mkdisjoint A i else {})
∪  (⋃i∈{n<..}. if i≤n then mkdisjoint A i else {})"
by (auto split: if_splits)
moreover
{ have "(⋃i∈{n<..}. if i≤n then mkdisjoint A i else {}) = {}"
by force }
hence "… = (⋃i∈{..n}. mkdisjoint A i)"
by auto
ultimately show
"(⋃i∈{..n}. mkdisjoint A i) = (⋃i. if i≤n then mkdisjoint A i else {})" by simp
qed

ultimately have
"measure M (A n) = measure M (⋃i. if i≤n then mkdisjoint A i else {})"
by simp

also
from i ms have
un: "(⋃i. if i≤n then mkdisjoint A i else {}) ∈ measurable_sets M"
moreover
from i ms have
"range (λi. if i≤n then mkdisjoint A i else {}) ⊆ measurable_sets M"
by (auto simp add: measure_space_def sigma_algebra_def)
moreover
from up have "∀i j. i ≠ j ⟶
(if i≤n then mkdisjoint A i else {}) ∩
(if j≤n then mkdisjoint A j else {}) = {}"
moreover note ms
ultimately have
"measure M (A n) = (∑i. measure M (if i ≤ n then mkdisjoint A i else {}))"

also
from ms have
"∀i. (Suc n)≤i ⟶ measure M (if i ≤ n then mkdisjoint A i else {}) = 0"
hence "(λi. measure M (if i ≤ n then mkdisjoint A i else {})) sums
(∑i<Suc n. measure M (if i ≤ n then mkdisjoint A i else {}))"
by (intro sums_finite) auto
hence "(∑i. measure M (if i ≤ n then mkdisjoint A i else {})) =
(∑i<Suc n. measure M (if i ≤ n then mkdisjoint A i else {}))"
by (rule sums_unique[THEN sym])
also
have "… = (∑i<Suc n. measure M (mkdisjoint A i))"
by simp
finally have
"measure M (A n) = (∑i<Suc n. measure M (mkdisjoint A i))" .
}

ultimately have
"(λn. measure M (A n)) ⇢ (measure M (⋃i. mkdisjoint A i))"
by simp

with AB show ?thesis
qed(*>*)

(*<*)
primrec trivial_series2:: "'a set ⇒ 'a set ⇒ (nat ⇒ 'a set)"
where
"trivial_series2 a b 0 = a"
| "trivial_series2 a b (Suc n) = (if (n=0) then b else {})"

lemma measure_additive: assumes ms: "measure_space M"
and disj: "a ∩ b = {}" and a: "a ∈ measurable_sets M"
and b:"b ∈ measurable_sets M"
shows "measure M (a ∪ b) = measure M a + measure M b"
(*<*)proof -
have "(a ∪ b) = (⋃i. trivial_series2 a b i)"
proof (rule set_eqI)
fix x
{
assume "x ∈ a ∪ b"
hence "∃i. x ∈ trivial_series2 a b i"
proof
assume "x ∈ a"
hence "x ∈ trivial_series2 a b 0"
by simp
thus "∃i. x ∈ trivial_series2 a b i"
by fast
next
assume "x ∈ b"
hence "x ∈ trivial_series2 a b 1"
by simp
thus "∃i. x ∈ trivial_series2 a b i"
by fast
qed
}
hence "(x ∈ a ∪ b) ⟹ (x ∈ (⋃i. trivial_series2 a b i))"
by simp
also
{
assume "x ∈ (⋃i. trivial_series2 a b i)"
then obtain i where x: "x ∈ trivial_series2 a b i"
by auto
hence "x ∈ a ∪ b"
proof (cases i)
case 0
with x show ?thesis by simp
next
case (Suc n)
with x show ?thesis
by (cases n) auto
qed
}
ultimately show "(x ∈ a ∪ b) = (x ∈ (⋃i. trivial_series2 a b i))"
by fast
qed
also
{ fix i
from a b ms have "trivial_series2 a b i ∈ measurable_sets M"
by (cases i) (auto simp add: measure_space_def sigma_algebra_def)
}
hence m1: "range (trivial_series2 a b) ⊆ measurable_sets M"
and m2: "(⋃i. trivial_series2 a b i) ∈ measurable_sets M"
using ms
by (auto simp add: measure_space_def sigma_algebra_def)

{ fix i j::nat
assume "i ≠ j"
hence "trivial_series2 a b i ∩ trivial_series2 a b j = {}"
using disj
by (cases i, cases j, auto)(cases j, auto)
}
with m1 m2 have "(λn. measure M (trivial_series2 a b n)) sums  measure M (⋃i. trivial_series2 a b i)"
using ms
moreover
from ms have "∀m. Suc(Suc 0) ≤ m ⟶ measure M (trivial_series2 a b m) = 0"
proof (clarify)
fix m
assume "Suc (Suc 0) ≤ m"
thus "measure M (trivial_series2 a b m) = 0"
using ms
by (cases m) (auto simp add: measure_space_def positive_def)
qed
hence "(λn. measure M (trivial_series2 a b n)) sums (∑n<Suc(Suc 0). measure M (trivial_series2 a b n))"
by (intro sums_finite) auto
moreover
have "(∑n=0..<Suc(Suc 0). measure M (trivial_series2 a b n)) =
measure M a + measure M b"
by simp
ultimately
have "measure M (a ∪ b) = (∑n. measure M (trivial_series2 a b n))"
and "Measure.measure M a + Measure.measure M b = (∑n. measure M (trivial_series2 a b n))"
`