(* Title: Sigma_Algebra.thy Author: Stefan Richter, Markus Wenzel, TU Muenchen License: LGPL Changes for Accordance to Joe Hurd's conventions and additions by Stefan Richter 2002 *) 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" ― ‹Named premises are introduced like this.› 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" ― ‹The $\isacommand {show}$ command starts the proof of a subgoal.› 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 ― ‹A new named variable is introduced.› 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 - ― ‹This form of $\isacommand {proof}$ foregoes the application of a rule.› 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 ― ‹This is just an abbreviation for $\isacommand {"from this have"}$.› } 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