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 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)" (*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) ∧ 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(*>*) (*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" 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