Theory Measure
subsection ‹Measure spaces \label{sec:measure-spaces}›
theory Measure
imports Sigma_Algebra MonConv
begin
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
countably additive for disjoint sets.›
definition
positive:: "('a set set * ('a set ⇒ real)) ⇒ bool" where
"positive M ⟷ measure M {} = 0 ∧
(∀A. A∈ measurable_sets M ⟶ 0 ≤ measure M A)"
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) ∧
positive M ∧ countably_additive 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"
by (simp add: Q_def)
next
case complement
fix r assume "r ∈ Q"
then obtain r1 where im: "r1 = f -` r" and a: "r1 ∈ a"
by (simp add: Q_def)
with sig have "-r1 ∈ a"
by (simp only: sigma_algebra_def)
with im Q_def show "-r ∈ Q"
by (simp add: vimage_Compl)
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"
by (simp add: Q_def)
from a sig have "⋃(r1 ` UNIV) ∈ a"
by (auto simp only: sigma_algebra_def)
with im Q_def show "⋃(r ` UNIV) ∈ Q"
by (auto simp add: vimage_UN)
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 = {}"
by (simp add: disjoint_iff_not_equal)
} 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
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"
by (simp add: measure_space_def sigma_algebra_def)
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 = {}"
by (simp add: mkdisjoint_disj)
moreover note ms
ultimately
have sums:
"(λi. measure M (mkdisjoint A i)) sums (measure M (⋃i. mkdisjoint A i))"
by (simp add: measure_space_def countably_additive_def)
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"
by (simp add: measure_space_def sigma_algebra_def cong add: SUP_cong_simp)
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 {}) = {}"
by (simp add: mkdisjoint_disj)
moreover note ms
ultimately have
"measure M (A n) = (∑i. measure M (if i ≤ n then mkdisjoint A i else {}))"
by (simp add: measure_space_def countably_additive_def sums_unique cong add: SUP_cong_simp)
also
from ms have
"∀i. (Suc n)≤i ⟶ measure M (if i ≤ n then mkdisjoint A i else {}) = 0"
by (simp add: measure_space_def positive_def)
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
by (simp add: mkdisjoint_mon_conv)
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
by (simp add: measure_space_def countably_additive_def)
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))"
by (simp_all add: sums_unique)
thus ?thesis by simp
qed
end