Theory Sigma_Algebra
subsection ‹Sigma algebras \label{sec:sigma}›
theory Sigma_Algebra imports Main begin
text ‹The $\isacommand {theory}$ command commences a formal document and enumerates the
theories it depends on. With the ‹Main› theory, a standard
selection of useful HOL theories excluding the real
numbers is loaded. This theory includes and builds upon a tiny theory of the
same name by Markus Wenzel. This theory as well as ‹Measure›
in \ref{sec:measure-spaces} is heavily
influenced by Joe Hurd's thesis \<^cite>‹"hurd2002"› and has been designed to keep the terminology as
consistent as possible with that work.
Sigma algebras are an elementary concept in measure
theory. To measure --- that is to integrate --- functions, we first have
to measure sets. Unfortunately, when dealing with a large universe,
it is often not possible to consistently assign a measure to every
subset. Therefore it is necessary to define the set of measurable
subsets of the universe. A sigma algebra is such a set that has
three very natural and desirable properties.›
definition
sigma_algebra:: "'a set set ⇒ bool" where
"sigma_algebra A ⟷
{} ∈ A ∧ (∀a. a ∈ A ⟶ -a ∈ A) ∧
(∀a. (∀ i::nat. a i ∈ A) ⟶ (⋃i. a i) ∈ A)"
text ‹
The $\isacommand {definition}$ command defines new constants, which
are just named functions in HOL. Mind that the third condition
expresses the fact that the union of countably many sets in $A$ is
again a set in $A$ without explicitly defining the notion of
countability.
Sigma algebras can naturally be created as the closure of any set of
sets with regard to the properties just postulated. Markus Wenzel
wrote the following
inductive definition of the $\isa {sigma}$ operator.›
inductive_set
sigma :: "'a set set ⇒ 'a set set"
for A :: "'a set set"
where
basic: "a ∈ A ⟹ a ∈ sigma A"
| empty: "{} ∈ sigma A"
| complement: "a ∈ sigma A ⟹ -a ∈ sigma A"
| Union: "(⋀i::nat. a i ∈ sigma A) ⟹ (⋃i. a i) ∈ sigma A"
text ‹He also proved the following basic facts. The easy proofs are omitted.
›
theorem sigma_UNIV: "UNIV ∈ sigma A"
proof -
have "{} ∈ sigma A" by (rule sigma.empty)
hence "-{} ∈ sigma A" by (rule sigma.complement)
also have "-{} = UNIV" by simp
finally show ?thesis .
qed
theorem sigma_Inter:
"(⋀i::nat. a i ∈ sigma A) ⟹ (⋂i. a i) ∈ sigma A"
proof -
assume "⋀i::nat. a i ∈ sigma A"
hence "⋀i::nat. -(a i) ∈ sigma A" by (rule sigma.complement)
hence "(⋃i. -(a i)) ∈ sigma A" by (rule sigma.Union)
hence "-(⋃i. -(a i)) ∈ sigma A" by (rule sigma.complement)
also have "-(⋃i. -(a i)) = (⋂i. a i)" by simp
finally show ?thesis .
qed
text ‹It is trivial to show the connection between our first
definitions. We use the opportunity to introduce the proof syntax.›
theorem assumes sa: "sigma_algebra A"
shows sigma_sigma_algebra: "sigma A = A"
proof
txt ‹The $\isacommand {proof}$ command alone invokes a single standard rule to
simplify the goal. Here the following two subgoals emerge.›
show "A ⊆ sigma A"
by (auto simp add: sigma.basic)
txt ‹This is easy enough to be solved by an automatic step,
indicated by the keyword $\isacommand {by}$. The method $\isacommand {auto}$ is stated in parentheses, with attributes to it following. In
this case, the first introduction rule for the $\isacommand {sigma}$
operator is given as an extra simplification rule.›
show "sigma A ⊆ A"
proof
txt ‹Because this goal is not quite as trivial, another proof is
invoked, delimiting a block as in a programming language.›
fix x
assume "x ∈ sigma A"
txt ‹An assumption is made that must be justified by the current proof
context. In this case the corresponding fact had been generated
by a rule automatically invoked by the inner $\isacommand {proof}$
command.›
from this sa show "x ∈ A"
txt ‹Named facts can explicitly be given to the proof methods using
$\isacommand {from}$. A special name is ‹this›, which denotes
current facts generated by the last command. Usually $\isacommand
{from}$ ‹this sa› --- remember that ‹sa› is an assumption from above
--- is abbreviated to $\isacommand {with}$ ‹sa›, but in this case the order of
facts is relevant for the following method and $\isacommand
{with}$
would have put the current facts last.›
by (induct rule: sigma.induct) (auto simp add: sigma_algebra_def)
txt ‹Two methods may be carried out at $\isacommand {by}$. The first
one applies induction here via the canonical rule generated by the
inductive definition above, while the latter solves the
resulting subgoals by an automatic step involving
simplification.›
qed
qed
text "These two steps finish their respective proofs, checking
that all subgoals have been proven."
text ‹To end this theory we prove a special case of the ‹sigma_Inter› theorem above. It seems trivial that
the fact holds for two sets as well as for countably many.
We get a first taste of the cost of formal reasoning here, however. The
idea must be made precise by exhibiting a concrete sequence of
sets.›
primrec trivial_series:: "'a set ⇒ 'a set ⇒ (nat ⇒ 'a set)"
where
"trivial_series a b 0 = a"
| "trivial_series a b (Suc n) = b"
text ‹Using $\isacommand {primrec}$, primitive recursive functions over
inductively defined data types --- the natural numbers in this case ---
may be constructed.›
theorem assumes s: "sigma_algebra A" and a: "a ∈ A" and b: "b ∈ A"
shows sigma_algebra_inter: "a ∩ b ∈ A"
proof -
have "a ∩ b = (⋂i::nat. trivial_series a b i)"
txt ‹Intermediate facts that do not solve any subgoals yet are established this way.›
proof (rule set_eqI)
txt ‹The $\isacommand {proof}$ command may also take one explicit method
as an argument like the single rule application in this instance.›
fix x
{
fix i
assume "x ∈ a ∩ b"
hence "x ∈ trivial_series a b i" by (cases i) auto
}
txt ‹Curly braces can be used to explicitly delimit
blocks. In conjunction with $\isacommand {fix}$, universal
quantification over the fixed variable $i$ is achieved
for the last statement in the block, which is exported to the
enclosing block.›
hence "x ∈ a ∩ b ⟹ ∀i. x ∈ trivial_series a b i"
by fast
also
txt ‹The statement $\isacommand {also}$ introduces calculational
reasoning. This basically amounts to collecting facts. With
$\isacommand {also}$, the current fact is added to a special list of
theorems called the calculation and
an automatically selected transitivity rule
is additionally applied from the second collected fact on.›
{ assume "⋀i. x ∈ trivial_series a b i"
hence "x ∈ trivial_series a b 0" and "x ∈ trivial_series a b 1"
by this+
hence "x ∈ a ∩ b"
by simp
}
hence "∀i. x ∈ trivial_series a b i ⟹ x ∈ a ∩ b"
by blast
ultimately have "x ∈ a ∩ b = (∀i::nat. x ∈ trivial_series a b i)" ..
txt ‹The accumulated calculational facts including the current one
are exposed to the next statement by $\isacommand {ultimately}$ and
the calculation list is then erased. The two dots after the
statement here indicate proof by a single automatically
selected rule.›
also have "… = (x ∈ (⋂i::nat. trivial_series a b i))"
by simp
finally show "x ∈ a ∩ b = (x ∈ (⋂i::nat. trivial_series a b i))" .
txt ‹The $\isacommand {finally}$ directive behaves like $\isacommand {ultimately}$
with the addition of a further transitivity rule application. A
single dot stands for proof by assumption.›
qed
moreover have "(⋂i::nat. trivial_series a b i) ∈ A"
proof -
{ fix i
from a b have "trivial_series a b i ∈ A"
by (cases i) auto
}
hence "⋀i. trivial_series a b i ∈ sigma A"
by (simp only: sigma.basic)
hence "(⋂i::nat. trivial_series a b i) ∈ sigma A"
by (simp only: sigma_Inter)
with s show ?thesis
by (simp only: sigma_sigma_algebra)
qed
ultimately show ?thesis by simp
qed
text ‹Of course, a like theorem holds for union instead of
intersection. But as we will not need it in what follows, the
theory is finished with the following easy properties instead.
Note that the former is a kind of generalization of the last result and
could be used to shorten its proof. Unfortunately, this one was needed ---
and therefore found --- only late in the development.
›
theorem sigma_INTER:
assumes a:"(⋀i::nat. i ∈ S ⟹ a i ∈ sigma A)"
shows "(⋂i∈S. a i) ∈ sigma A"
proof -
from a have "⋀i. (if i∈S then {} else UNIV) ∪ a i ∈ sigma A"
by (simp add: sigma.intros sigma_UNIV)
hence "(⋂i. (if i∈S then {} else UNIV) ∪ a i) ∈ sigma A"
by (rule sigma_Inter)
also have "(⋂i. (if i∈S then {} else UNIV) ∪ a i) = (⋂i∈S. a i)"
by force
finally show ?thesis .
qed
lemma assumes s: "sigma_algebra a" shows sigma_algebra_UNIV: "UNIV ∈ a"
proof -
from s have "{}∈a" by (unfold sigma_algebra_def) blast
with s show ?thesis by (unfold sigma_algebra_def) auto
qed
end