src/HOL/Probability/Sigma_Algebra.thy
 author hoelzl Wed, 01 Dec 2010 19:20:30 +0100 changeset 40859 de0b30e6c2d2 parent 40702 cf26dd7395e4 child 40869 251df82c0088 permissions -rw-r--r--
Support product spaces on sigma finite measures. Introduce the almost everywhere quantifier. Introduce 'morphism' theorems for most constants. Prove uniqueness of measures on cut stable generators. Prove uniqueness of the Radon-Nikodym derivative. Removed misleading suffix from borel_space and lebesgue_space. Use product spaces to introduce Fubini on the Lebesgue integral. Combine Euclidean_Lebesgue and Lebesgue_Measure. Generalize theorems about mutual information and entropy to arbitrary probability spaces. Remove simproc mult_log as it does not work with interpretations. Introduce completion of measure spaces. Change type of sigma. Introduce dynkin systems.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 1` ```(* Title: Sigma_Algebra.thy ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 2` ``` Author: Stefan Richter, Markus Wenzel, TU Muenchen ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 3` ``` Plus material from the Hurd/Coble measure theory development, ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 4` ``` translated by Lawrence Paulson. ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 5` ```*) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 6` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 7` ```header {* Sigma Algebras *} ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 8` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 9` ```theory Sigma_Algebra imports Main Countable FuncSet Indicator_Function begin ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 10` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 11` ```text {* Sigma algebras are an elementary concept in measure ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 12` ``` theory. To measure --- that is to integrate --- functions, we first have ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 13` ``` to measure sets. Unfortunately, when dealing with a large universe, ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 14` ``` it is often not possible to consistently assign a measure to every ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 15` ``` subset. Therefore it is necessary to define the set of measurable ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 16` ``` subsets of the universe. A sigma algebra is such a set that has ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 17` ``` three very natural and desirable properties. *} ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 18` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 19` ```subsection {* Algebras *} ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 20` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 21` ```record 'a algebra = ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 22` ``` space :: "'a set" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 23` ``` sets :: "'a set set" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 24` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 25` ```locale algebra = ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 26` ``` fixes M :: "'a algebra" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 27` ``` assumes space_closed: "sets M \ Pow (space M)" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 28` ``` and empty_sets [iff]: "{} \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 29` ``` and compl_sets [intro]: "!!a. a \ sets M \ space M - a \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 30` ``` and Un [intro]: "!!a b. a \ sets M \ b \ sets M \ a \ b \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 31` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 32` ```lemma (in algebra) top [iff]: "space M \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 33` ``` by (metis Diff_empty compl_sets empty_sets) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 34` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 35` ```lemma (in algebra) sets_into_space: "x \ sets M \ x \ space M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 36` ``` by (metis PowD contra_subsetD space_closed) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 37` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 38` ```lemma (in algebra) Int [intro]: ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 39` ``` assumes a: "a \ sets M" and b: "b \ sets M" shows "a \ b \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 40` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 41` ``` have "((space M - a) \ (space M - b)) \ sets M" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 42` ``` by (metis a b compl_sets Un) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 43` ``` moreover ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 44` ``` have "a \ b = space M - ((space M - a) \ (space M - b))" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 45` ``` using space_closed a b ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 46` ``` by blast ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 47` ``` ultimately show ?thesis ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 48` ``` by (metis compl_sets) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 49` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 50` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 51` ```lemma (in algebra) Diff [intro]: ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 52` ``` assumes a: "a \ sets M" and b: "b \ sets M" shows "a - b \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 53` ```proof - ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 54` ``` have "(a \ (space M - b)) \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 55` ``` by (metis a b compl_sets Int) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 56` ``` moreover ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 57` ``` have "a - b = (a \ (space M - b))" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 58` ``` by (metis Int_Diff Int_absorb1 Int_commute a sets_into_space) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 59` ``` ultimately show ?thesis ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 60` ``` by metis ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 61` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 62` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 63` ```lemma (in algebra) finite_union [intro]: ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 64` ``` "finite X \ X \ sets M \ Union X \ sets M" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 65` ``` by (induct set: finite) (auto simp add: Un) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 66` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 67` ```lemma algebra_iff_Int: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 68` ``` "algebra M \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 69` ``` sets M \ Pow (space M) & {} \ sets M & ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 70` ``` (\a \ sets M. space M - a \ sets M) & ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 71` ``` (\a \ sets M. \ b \ sets M. a \ b \ sets M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 72` ```proof (auto simp add: algebra.Int, auto simp add: algebra_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 73` ``` fix a b ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 74` ``` assume ab: "sets M \ Pow (space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 75` ``` "\a\sets M. space M - a \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 76` ``` "\a\sets M. \b\sets M. a \ b \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 77` ``` "a \ sets M" "b \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 78` ``` hence "a \ b = space M - ((space M - a) \ (space M - b))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 79` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 80` ``` also have "... \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 81` ``` by (metis ab) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 82` ``` finally show "a \ b \ sets M" . ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 83` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 84` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 85` ```lemma (in algebra) insert_in_sets: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 86` ``` assumes "{x} \ sets M" "A \ sets M" shows "insert x A \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 87` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 88` ``` have "{x} \ A \ sets M" using assms by (rule Un) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 89` ``` thus ?thesis by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 90` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 91` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 92` ```lemma (in algebra) Int_space_eq1 [simp]: "x \ sets M \ space M \ x = x" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 93` ``` by (metis Int_absorb1 sets_into_space) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 94` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 95` ```lemma (in algebra) Int_space_eq2 [simp]: "x \ sets M \ x \ space M = x" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 96` ``` by (metis Int_absorb2 sets_into_space) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 97` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 98` ```section {* Restricted algebras *} ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 99` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 100` ```abbreviation (in algebra) ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 101` ``` "restricted_space A \ \ space = A, sets = (\S. (A \ S)) ` sets M \" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 102` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 103` ```lemma (in algebra) restricted_algebra: ``` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 104` ``` assumes "A \ sets M" shows "algebra (restricted_space A)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 105` ``` using assms by unfold_locales auto ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 106` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 107` ```subsection {* Sigma Algebras *} ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 108` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 109` ```locale sigma_algebra = algebra + ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 110` ``` assumes countable_nat_UN [intro]: ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 111` ``` "!!A. range A \ sets M \ (\i::nat. A i) \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 112` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 113` ```lemma countable_UN_eq: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 114` ``` fixes A :: "'i::countable \ 'a set" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 115` ``` shows "(range A \ sets M \ (\i. A i) \ sets M) \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 116` ``` (range (A \ from_nat) \ sets M \ (\i. (A \ from_nat) i) \ sets M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 117` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 118` ``` let ?A' = "A \ from_nat" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 119` ``` have *: "(\i. ?A' i) = (\i. A i)" (is "?l = ?r") ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 120` ``` proof safe ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 121` ``` fix x i assume "x \ A i" thus "x \ ?l" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 122` ``` by (auto intro!: exI[of _ "to_nat i"]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 123` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 124` ``` fix x i assume "x \ ?A' i" thus "x \ ?r" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 125` ``` by (auto intro!: exI[of _ "from_nat i"]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 126` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 127` ``` have **: "range ?A' = range A" ``` 40702 cf26dd7395e4 Replace surj by abbreviation; remove surj_on. hoelzl parents: 39960 diff changeset ` 128` ``` using surj_from_nat ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 129` ``` by (auto simp: image_compose intro!: imageI) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 130` ``` show ?thesis unfolding * ** .. ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 131` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 132` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 133` ```lemma (in sigma_algebra) countable_UN[intro]: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 134` ``` fixes A :: "'i::countable \ 'a set" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 135` ``` assumes "A`X \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 136` ``` shows "(\x\X. A x) \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 137` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 138` ``` let "?A i" = "if i \ X then A i else {}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 139` ``` from assms have "range ?A \ sets M" by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 140` ``` with countable_nat_UN[of "?A \ from_nat"] countable_UN_eq[of ?A M] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 141` ``` have "(\x. ?A x) \ sets M" by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 142` ``` moreover have "(\x. ?A x) = (\x\X. A x)" by (auto split: split_if_asm) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 143` ``` ultimately show ?thesis by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 144` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 145` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 146` ```lemma (in sigma_algebra) finite_UN: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 147` ``` assumes "finite I" and "\i. i \ I \ A i \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 148` ``` shows "(\i\I. A i) \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 149` ``` using assms by induct auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 150` 33533 40b44cb20c8c New theory Probability/Borel.thy, and some associated lemmas paulson parents: 33271 diff changeset ` 151` ```lemma (in sigma_algebra) countable_INT [intro]: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 152` ``` fixes A :: "'i::countable \ 'a set" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 153` ``` assumes A: "A`X \ sets M" "X \ {}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 154` ``` shows "(\i\X. A i) \ sets M" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 155` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 156` ``` from A have "\i\X. A i \ sets M" by fast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 157` ``` hence "space M - (\i\X. space M - A i) \ sets M" by blast ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 158` ``` moreover ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 159` ``` have "(\i\X. A i) = space M - (\i\X. space M - A i)" using space_closed A ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 160` ``` by blast ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 161` ``` ultimately show ?thesis by metis ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 162` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 163` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 164` ```lemma (in sigma_algebra) finite_INT: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 165` ``` assumes "finite I" "I \ {}" "\i. i \ I \ A i \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 166` ``` shows "(\i\I. A i) \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 167` ``` using assms by (induct rule: finite_ne_induct) auto ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 168` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 169` ```lemma algebra_Pow: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 170` ``` "algebra \ space = sp, sets = Pow sp, \ = X \" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 171` ``` by (auto simp add: algebra_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 172` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 173` ```lemma sigma_algebra_Pow: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 174` ``` "sigma_algebra \ space = sp, sets = Pow sp, \ = X \" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 175` ``` by (auto simp add: sigma_algebra_def sigma_algebra_axioms_def algebra_Pow) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 176` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 177` ```lemma sigma_algebra_iff: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 178` ``` "sigma_algebra M \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 179` ``` algebra M \ (\A. range A \ sets M \ (\i::nat. A i) \ sets M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 180` ``` by (simp add: sigma_algebra_def sigma_algebra_axioms_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 181` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 182` ```subsection {* Binary Unions *} ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 183` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 184` ```definition binary :: "'a \ 'a \ nat \ 'a" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 185` ``` where "binary a b = (\\<^isup>x. b)(0 := a)" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 186` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 187` ```lemma range_binary_eq: "range(binary a b) = {a,b}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 188` ``` by (auto simp add: binary_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 189` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 190` ```lemma Un_range_binary: "a \ b = (\i::nat. binary a b i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 191` ``` by (simp add: UNION_eq_Union_image range_binary_eq) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 192` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 193` ```lemma Int_range_binary: "a \ b = (\i::nat. binary a b i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 194` ``` by (simp add: INTER_eq_Inter_image range_binary_eq) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 195` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 196` ```lemma sigma_algebra_iff2: ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 197` ``` "sigma_algebra M \ ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 198` ``` sets M \ Pow (space M) \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 199` ``` {} \ sets M \ (\s \ sets M. space M - s \ sets M) \ ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 200` ``` (\A. range A \ sets M \ (\i::nat. A i) \ sets M)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 201` ``` by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 202` ``` algebra_def Un_range_binary) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 203` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 204` ```subsection {* Initial Sigma Algebra *} ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 205` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 206` ```text {*Sigma algebras can naturally be created as the closure of any set of ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 207` ``` sets with regard to the properties just postulated. *} ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 208` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 209` ```inductive_set ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 210` ``` sigma_sets :: "'a set \ 'a set set \ 'a set set" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 211` ``` for sp :: "'a set" and A :: "'a set set" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 212` ``` where ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 213` ``` Basic: "a \ A \ a \ sigma_sets sp A" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 214` ``` | Empty: "{} \ sigma_sets sp A" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 215` ``` | Compl: "a \ sigma_sets sp A \ sp - a \ sigma_sets sp A" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 216` ``` | Union: "(\i::nat. a i \ sigma_sets sp A) \ (\i. a i) \ sigma_sets sp A" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 217` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 218` ```definition ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 219` ``` "sigma M = (| space = space M, sets = sigma_sets (space M) (sets M) |)" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 220` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 221` ```lemma sets_sigma: "sets (sigma M) = sigma_sets (space M) (sets M)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 222` ``` unfolding sigma_def by simp ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 223` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 224` ```lemma space_sigma [simp]: "space (sigma M) = space M" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 225` ``` by (simp add: sigma_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 226` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 227` ```lemma sigma_sets_top: "sp \ sigma_sets sp A" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 228` ``` by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 229` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 230` ```lemma sigma_sets_into_sp: "A \ Pow sp \ x \ sigma_sets sp A \ x \ sp" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 231` ``` by (erule sigma_sets.induct, auto) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 232` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 233` ```lemma sigma_sets_Un: ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 234` ``` "a \ sigma_sets sp A \ b \ sigma_sets sp A \ a \ b \ sigma_sets sp A" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 235` ```apply (simp add: Un_range_binary range_binary_eq) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 236` ```apply (rule Union, simp add: binary_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 237` ```done ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 238` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 239` ```lemma sigma_sets_Inter: ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 240` ``` assumes Asb: "A \ Pow sp" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 241` ``` shows "(\i::nat. a i \ sigma_sets sp A) \ (\i. a i) \ sigma_sets sp A" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 242` ```proof - ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 243` ``` assume ai: "\i::nat. a i \ sigma_sets sp A" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 244` ``` hence "\i::nat. sp-(a i) \ sigma_sets sp A" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 245` ``` by (rule sigma_sets.Compl) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 246` ``` hence "(\i. sp-(a i)) \ sigma_sets sp A" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 247` ``` by (rule sigma_sets.Union) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 248` ``` hence "sp-(\i. sp-(a i)) \ sigma_sets sp A" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 249` ``` by (rule sigma_sets.Compl) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 250` ``` also have "sp-(\i. sp-(a i)) = sp Int (\i. a i)" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 251` ``` by auto ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 252` ``` also have "... = (\i. a i)" using ai ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 253` ``` by (blast dest: sigma_sets_into_sp [OF Asb]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 254` ``` finally show ?thesis . ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 255` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 256` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 257` ```lemma sigma_sets_INTER: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 258` ``` assumes Asb: "A \ Pow sp" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 259` ``` and ai: "\i::nat. i \ S \ a i \ sigma_sets sp A" and non: "S \ {}" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 260` ``` shows "(\i\S. a i) \ sigma_sets sp A" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 261` ```proof - ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 262` ``` from ai have "\i. (if i\S then a i else sp) \ sigma_sets sp A" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 263` ``` by (simp add: sigma_sets.intros sigma_sets_top) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 264` ``` hence "(\i. (if i\S then a i else sp)) \ sigma_sets sp A" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 265` ``` by (rule sigma_sets_Inter [OF Asb]) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 266` ``` also have "(\i. (if i\S then a i else sp)) = (\i\S. a i)" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 267` ``` by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+ ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 268` ``` finally show ?thesis . ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 269` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 270` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 271` ```lemma (in sigma_algebra) sigma_sets_subset: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 272` ``` assumes a: "a \ sets M" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 273` ``` shows "sigma_sets (space M) a \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 274` ```proof ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 275` ``` fix x ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 276` ``` assume "x \ sigma_sets (space M) a" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 277` ``` from this show "x \ sets M" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 278` ``` by (induct rule: sigma_sets.induct, auto) (metis a subsetD) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 279` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 280` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 281` ```lemma (in sigma_algebra) sigma_sets_eq: ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 282` ``` "sigma_sets (space M) (sets M) = sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 283` ```proof ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 284` ``` show "sets M \ sigma_sets (space M) (sets M)" ``` 37032 58a0757031dd speed up some proofs and fix some warnings huffman parents: 33536 diff changeset ` 285` ``` by (metis Set.subsetI sigma_sets.Basic) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 286` ``` next ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 287` ``` show "sigma_sets (space M) (sets M) \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 288` ``` by (metis sigma_sets_subset subset_refl) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 289` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 290` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 291` ```lemma sigma_algebra_sigma_sets: ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 292` ``` "a \ Pow (space M) \ sets M = sigma_sets (space M) a \ sigma_algebra M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 293` ``` apply (auto simp add: sigma_algebra_def sigma_algebra_axioms_def ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 294` ``` algebra_def sigma_sets.Empty sigma_sets.Compl sigma_sets_Un) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 295` ``` apply (blast dest: sigma_sets_into_sp) ``` 37032 58a0757031dd speed up some proofs and fix some warnings huffman parents: 33536 diff changeset ` 296` ``` apply (rule sigma_sets.Union, fast) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 297` ``` done ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 298` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 299` ```lemma sigma_algebra_sigma: ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 300` ``` "sets M \ Pow (space M) \ sigma_algebra (sigma M)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 301` ``` apply (rule sigma_algebra_sigma_sets) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 302` ``` apply (auto simp add: sigma_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 303` ``` done ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 304` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 305` ```lemma (in sigma_algebra) sigma_subset: ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 306` ``` "sets N \ sets M \ space N = space M \ sets (sigma N) \ (sets M)" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 307` ``` by (simp add: sigma_def sigma_sets_subset) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 308` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 309` ```lemma sigma_sets_least_sigma_algebra: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 310` ``` assumes "A \ Pow S" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 311` ``` shows "sigma_sets S A = \{B. A \ B \ sigma_algebra \space = S, sets = B\}" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 312` ```proof safe ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 313` ``` fix B X assume "A \ B" and sa: "sigma_algebra \ space = S, sets = B \" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 314` ``` and X: "X \ sigma_sets S A" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 315` ``` from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF `A \ B`] X ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 316` ``` show "X \ B" by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 317` ```next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 318` ``` fix X assume "X \ \{B. A \ B \ sigma_algebra \space = S, sets = B\}" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 319` ``` then have [intro!]: "\B. A \ B \ sigma_algebra \space = S, sets = B\ \ X \ B" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 320` ``` by simp ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 321` ``` have "A \ sigma_sets S A" using assms ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 322` ``` by (auto intro!: sigma_sets.Basic) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 323` ``` moreover have "sigma_algebra \space = S, sets = sigma_sets S A\" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 324` ``` using assms by (intro sigma_algebra_sigma_sets[of A]) auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 325` ``` ultimately show "X \ sigma_sets S A" by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 326` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 327` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 328` ```lemma (in sigma_algebra) restriction_in_sets: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 329` ``` fixes A :: "nat \ 'a set" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 330` ``` assumes "S \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 331` ``` and *: "range A \ (\A. S \ A) ` sets M" (is "_ \ ?r") ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 332` ``` shows "range A \ sets M" "(\i. A i) \ (\A. S \ A) ` sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 333` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 334` ``` { fix i have "A i \ ?r" using * by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 335` ``` hence "\B. A i = B \ S \ B \ sets M" by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 336` ``` hence "A i \ S" "A i \ sets M" using `S \ sets M` by auto } ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 337` ``` thus "range A \ sets M" "(\i. A i) \ (\A. S \ A) ` sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 338` ``` by (auto intro!: image_eqI[of _ _ "(\i. A i)"]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 339` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 340` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 341` ```lemma (in sigma_algebra) restricted_sigma_algebra: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 342` ``` assumes "S \ sets M" ``` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 343` ``` shows "sigma_algebra (restricted_space S)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 344` ``` unfolding sigma_algebra_def sigma_algebra_axioms_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 345` ```proof safe ``` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 346` ``` show "algebra (restricted_space S)" using restricted_algebra[OF assms] . ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 347` ```next ``` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 348` ``` fix A :: "nat \ 'a set" assume "range A \ sets (restricted_space S)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 349` ``` from restriction_in_sets[OF assms this[simplified]] ``` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 350` ``` show "(\i. A i) \ sets (restricted_space S)" by simp ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 351` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 352` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 353` ```lemma sigma_sets_Int: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 354` ``` assumes "A \ sigma_sets sp st" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 355` ``` shows "op \ A ` sigma_sets sp st = sigma_sets (A \ sp) (op \ A ` st)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 356` ```proof (intro equalityI subsetI) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 357` ``` fix x assume "x \ op \ A ` sigma_sets sp st" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 358` ``` then obtain y where "y \ sigma_sets sp st" "x = y \ A" by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 359` ``` then show "x \ sigma_sets (A \ sp) (op \ A ` st)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 360` ``` proof (induct arbitrary: x) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 361` ``` case (Compl a) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 362` ``` then show ?case ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 363` ``` by (force intro!: sigma_sets.Compl simp: Diff_Int_distrib ac_simps) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 364` ``` next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 365` ``` case (Union a) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 366` ``` then show ?case ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 367` ``` by (auto intro!: sigma_sets.Union ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 368` ``` simp add: UN_extend_simps simp del: UN_simps) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 369` ``` qed (auto intro!: sigma_sets.intros) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 370` ```next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 371` ``` fix x assume "x \ sigma_sets (A \ sp) (op \ A ` st)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 372` ``` then show "x \ op \ A ` sigma_sets sp st" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 373` ``` proof induct ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 374` ``` case (Compl a) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 375` ``` then obtain x where "a = A \ x" "x \ sigma_sets sp st" by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 376` ``` then show ?case ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 377` ``` by (force simp add: image_iff intro!: bexI[of _ "sp - x"] sigma_sets.Compl) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 378` ``` next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 379` ``` case (Union a) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 380` ``` then have "\i. \x. x \ sigma_sets sp st \ a i = A \ x" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 381` ``` by (auto simp: image_iff Bex_def) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 382` ``` from choice[OF this] guess f .. ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 383` ``` then show ?case ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 384` ``` by (auto intro!: bexI[of _ "(\x. f x)"] sigma_sets.Union ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 385` ``` simp add: image_iff) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 386` ``` qed (auto intro!: sigma_sets.intros) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 387` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 388` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 389` ```lemma sigma_sets_single[simp]: "sigma_sets {X} {{X}} = {{}, {X}}" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 390` ```proof (intro set_eqI iffI) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 391` ``` fix x assume "x \ sigma_sets {X} {{X}}" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 392` ``` from sigma_sets_into_sp[OF _ this] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 393` ``` show "x \ {{}, {X}}" by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 394` ```next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 395` ``` fix x assume "x \ {{}, {X}}" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 396` ``` then show "x \ sigma_sets {X} {{X}}" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 397` ``` by (auto intro: sigma_sets.Empty sigma_sets_top) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 398` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 399` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 400` ```section {* Measurable functions *} ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 401` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 402` ```definition ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 403` ``` "measurable A B = {f \ space A -> space B. \y \ sets B. f -` y \ space A \ sets A}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 404` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 405` ```lemma (in sigma_algebra) measurable_sigma: ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 406` ``` assumes B: "sets N \ Pow (space N)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 407` ``` and f: "f \ space M -> space N" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 408` ``` and ba: "\y. y \ sets N \ (f -` y) \ space M \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 409` ``` shows "f \ measurable M (sigma N)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 410` ```proof - ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 411` ``` have "sigma_sets (space N) (sets N) \ {y . (f -` y) \ space M \ sets M & y \ space N}" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 412` ``` proof clarify ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 413` ``` fix x ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 414` ``` assume "x \ sigma_sets (space N) (sets N)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 415` ``` thus "f -` x \ space M \ sets M \ x \ space N" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 416` ``` proof induct ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 417` ``` case (Basic a) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 418` ``` thus ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 419` ``` by (auto simp add: ba) (metis B subsetD PowD) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 420` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 421` ``` case Empty ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 422` ``` thus ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 423` ``` by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 424` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 425` ``` case (Compl a) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 426` ``` have [simp]: "f -` space N \ space M = space M" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 427` ``` by (auto simp add: funcset_mem [OF f]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 428` ``` thus ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 429` ``` by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 430` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 431` ``` case (Union a) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 432` ``` thus ?case ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 433` ``` by (simp add: vimage_UN, simp only: UN_extend_simps(4)) blast ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 434` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 435` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 436` ``` thus ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 437` ``` by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 438` ``` (auto simp add: sigma_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 439` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 440` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 441` ```lemma measurable_cong: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 442` ``` assumes "\ w. w \ space M \ f w = g w" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 443` ``` shows "f \ measurable M M' \ g \ measurable M M'" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 444` ``` unfolding measurable_def using assms ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 445` ``` by (simp cong: vimage_inter_cong Pi_cong) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 446` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 447` ```lemma measurable_space: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 448` ``` "f \ measurable M A \ x \ space M \ f x \ space A" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 449` ``` unfolding measurable_def by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 450` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 451` ```lemma measurable_sets: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 452` ``` "f \ measurable M A \ S \ sets A \ f -` S \ space M \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 453` ``` unfolding measurable_def by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 454` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 455` ```lemma (in sigma_algebra) measurable_subset: ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 456` ``` "(\S. S \ sets A \ S \ space A) \ measurable M A \ measurable M (sigma A)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 457` ``` by (auto intro: measurable_sigma measurable_sets measurable_space) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 458` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 459` ```lemma measurable_eqI: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 460` ``` "\ space m1 = space m1' ; space m2 = space m2' ; ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 461` ``` sets m1 = sets m1' ; sets m2 = sets m2' \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 462` ``` \ measurable m1 m2 = measurable m1' m2'" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 463` ``` by (simp add: measurable_def sigma_algebra_iff2) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 464` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 465` ```lemma (in sigma_algebra) measurable_const[intro, simp]: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 466` ``` assumes "c \ space M'" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 467` ``` shows "(\x. c) \ measurable M M'" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 468` ``` using assms by (auto simp add: measurable_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 469` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 470` ```lemma (in sigma_algebra) measurable_If: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 471` ``` assumes measure: "f \ measurable M M'" "g \ measurable M M'" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 472` ``` assumes P: "{x\space M. P x} \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 473` ``` shows "(\x. if P x then f x else g x) \ measurable M M'" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 474` ``` unfolding measurable_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 475` ```proof safe ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 476` ``` fix x assume "x \ space M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 477` ``` thus "(if P x then f x else g x) \ space M'" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 478` ``` using measure unfolding measurable_def by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 479` ```next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 480` ``` fix A assume "A \ sets M'" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 481` ``` hence *: "(\x. if P x then f x else g x) -` A \ space M = ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 482` ``` ((f -` A \ space M) \ {x\space M. P x}) \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 483` ``` ((g -` A \ space M) \ (space M - {x\space M. P x}))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 484` ``` using measure unfolding measurable_def by (auto split: split_if_asm) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 485` ``` show "(\x. if P x then f x else g x) -` A \ space M \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 486` ``` using `A \ sets M'` measure P unfolding * measurable_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 487` ``` by (auto intro!: Un) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 488` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 489` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 490` ```lemma (in sigma_algebra) measurable_If_set: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 491` ``` assumes measure: "f \ measurable M M'" "g \ measurable M M'" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 492` ``` assumes P: "A \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 493` ``` shows "(\x. if x \ A then f x else g x) \ measurable M M'" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 494` ```proof (rule measurable_If[OF measure]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 495` ``` have "{x \ space M. x \ A} = A" using `A \ sets M` sets_into_space by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 496` ``` thus "{x \ space M. x \ A} \ sets M" using `A \ sets M` by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 497` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 498` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 499` ```lemma (in algebra) measurable_ident[intro, simp]: "id \ measurable M M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 500` ``` by (auto simp add: measurable_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 501` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 502` ```lemma measurable_comp[intro]: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 503` ``` fixes f :: "'a \ 'b" and g :: "'b \ 'c" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 504` ``` shows "f \ measurable a b \ g \ measurable b c \ (g o f) \ measurable a c" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 505` ``` apply (auto simp add: measurable_def vimage_compose) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 506` ``` apply (subgoal_tac "f -` g -` y \ space a = f -` (g -` y \ space b) \ space a") ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 507` ``` apply force+ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 508` ``` done ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 509` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 510` ```lemma measurable_strong: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 511` ``` fixes f :: "'a \ 'b" and g :: "'b \ 'c" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 512` ``` assumes f: "f \ measurable a b" and g: "g \ (space b -> space c)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 513` ``` and a: "sigma_algebra a" and b: "sigma_algebra b" and c: "sigma_algebra c" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 514` ``` and t: "f ` (space a) \ t" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 515` ``` and cb: "\s. s \ sets c \ (g -` s) \ t \ sets b" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 516` ``` shows "(g o f) \ measurable a c" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 517` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 518` ``` have fab: "f \ (space a -> space b)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 519` ``` and ba: "\y. y \ sets b \ (f -` y) \ (space a) \ sets a" using f ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 520` ``` by (auto simp add: measurable_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 521` ``` have eq: "f -` g -` y \ space a = f -` (g -` y \ t) \ space a" using t ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 522` ``` by force ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 523` ``` show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 524` ``` apply (auto simp add: measurable_def vimage_compose a c) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 525` ``` apply (metis funcset_mem fab g) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 526` ``` apply (subst eq, metis ba cb) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 527` ``` done ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 528` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 529` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 530` ```lemma measurable_mono1: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 531` ``` "a \ b \ sigma_algebra \space = X, sets = b\ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 532` ``` \ measurable \space = X, sets = a\ c \ measurable \space = X, sets = b\ c" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 533` ``` by (auto simp add: measurable_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 534` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 535` ```lemma measurable_up_sigma: ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 536` ``` "measurable A M \ measurable (sigma A) M" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 537` ``` unfolding measurable_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 538` ``` by (auto simp: sigma_def intro: sigma_sets.Basic) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 539` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 540` ```lemma (in sigma_algebra) measurable_range_reduce: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 541` ``` "\ f \ measurable M \space = s, sets = Pow s\ ; s \ {} \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 542` ``` \ f \ measurable M \space = s \ (f ` space M), sets = Pow (s \ (f ` space M))\" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 543` ``` by (simp add: measurable_def sigma_algebra_Pow del: Pow_Int_eq) blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 544` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 545` ```lemma (in sigma_algebra) measurable_Pow_to_Pow: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 546` ``` "(sets M = Pow (space M)) \ f \ measurable M \space = UNIV, sets = Pow UNIV\" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 547` ``` by (auto simp add: measurable_def sigma_algebra_def sigma_algebra_axioms_def algebra_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 548` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 549` ```lemma (in sigma_algebra) measurable_Pow_to_Pow_image: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 550` ``` "sets M = Pow (space M) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 551` ``` \ f \ measurable M \space = f ` space M, sets = Pow (f ` space M)\" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 552` ``` by (simp add: measurable_def sigma_algebra_Pow) intro_locales ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 553` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 554` ```lemma (in sigma_algebra) measurable_iff_sigma: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 555` ``` assumes "sets E \ Pow (space E)" and "f \ space M \ space E" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 556` ``` shows "f \ measurable M (sigma E) \ (\A\sets E. f -` A \ space M \ sets M)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 557` ``` using measurable_sigma[OF assms] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 558` ``` by (fastsimp simp: measurable_def sets_sigma intro: sigma_sets.intros) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 559` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 560` ```section "Disjoint families" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 561` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 562` ```definition ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 563` ``` disjoint_family_on where ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 564` ``` "disjoint_family_on A S \ (\m\S. \n\S. m \ n \ A m \ A n = {})" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 565` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 566` ```abbreviation ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 567` ``` "disjoint_family A \ disjoint_family_on A UNIV" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 568` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 569` ```lemma range_subsetD: "range f \ B \ f i \ B" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 570` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 571` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 572` ```lemma Int_Diff_disjoint: "A \ B \ (A - B) = {}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 573` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 574` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 575` ```lemma Int_Diff_Un: "A \ B \ (A - B) = A" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 576` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 577` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 578` ```lemma disjoint_family_subset: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 579` ``` "disjoint_family A \ (!!x. B x \ A x) \ disjoint_family B" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 580` ``` by (force simp add: disjoint_family_on_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 581` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 582` ```lemma disjoint_family_on_bisimulation: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 583` ``` assumes "disjoint_family_on f S" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 584` ``` and "\n m. n \ S \ m \ S \ n \ m \ f n \ f m = {} \ g n \ g m = {}" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 585` ``` shows "disjoint_family_on g S" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 586` ``` using assms unfolding disjoint_family_on_def by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 587` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 588` ```lemma disjoint_family_on_mono: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 589` ``` "A \ B \ disjoint_family_on f B \ disjoint_family_on f A" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 590` ``` unfolding disjoint_family_on_def by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 591` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 592` ```lemma disjoint_family_Suc: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 593` ``` assumes Suc: "!!n. A n \ A (Suc n)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 594` ``` shows "disjoint_family (\i. A (Suc i) - A i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 595` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 596` ``` { ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 597` ``` fix m ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 598` ``` have "!!n. A n \ A (m+n)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 599` ``` proof (induct m) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 600` ``` case 0 show ?case by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 601` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 602` ``` case (Suc m) thus ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 603` ``` by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 604` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 605` ``` } ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 606` ``` hence "!!m n. m < n \ A m \ A n" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 607` ``` by (metis add_commute le_add_diff_inverse nat_less_le) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 608` ``` thus ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 609` ``` by (auto simp add: disjoint_family_on_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 610` ``` (metis insert_absorb insert_subset le_SucE le_antisym not_leE) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 611` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 612` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 613` ```lemma setsum_indicator_disjoint_family: ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 614` ``` fixes f :: "'d \ 'e::semiring_1" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 615` ``` assumes d: "disjoint_family_on A P" and "x \ A j" and "finite P" and "j \ P" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 616` ``` shows "(\i\P. f i * indicator (A i) x) = f j" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 617` ```proof - ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 618` ``` have "P \ {i. x \ A i} = {j}" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 619` ``` using d `x \ A j` `j \ P` unfolding disjoint_family_on_def ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 620` ``` by auto ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 621` ``` thus ?thesis ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 622` ``` unfolding indicator_def ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 623` ``` by (simp add: if_distrib setsum_cases[OF `finite P`]) ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 624` ```qed ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 625` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 626` ```definition disjointed :: "(nat \ 'a set) \ nat \ 'a set " ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 627` ``` where "disjointed A n = A n - (\i\{0..i\{0..i\{0..i. disjointed A i) = (\i. A i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 638` ``` apply (rule UN_finite2_eq [where k=0]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 639` ``` apply (simp add: finite_UN_disjointed_eq) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 640` ``` done ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 641` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 642` ```lemma less_disjoint_disjointed: "m disjointed A m \ disjointed A n = {}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 643` ``` by (auto simp add: disjointed_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 644` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 645` ```lemma disjoint_family_disjointed: "disjoint_family (disjointed A)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 646` ``` by (simp add: disjoint_family_on_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 647` ``` (metis neq_iff Int_commute less_disjoint_disjointed) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 648` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 649` ```lemma disjointed_subset: "disjointed A n \ A n" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 650` ``` by (auto simp add: disjointed_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 651` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 652` ```lemma (in algebra) UNION_in_sets: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 653` ``` fixes A:: "nat \ 'a set" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 654` ``` assumes A: "range A \ sets M " ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 655` ``` shows "(\i\{0.. sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 656` ```proof (induct n) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 657` ``` case 0 show ?case by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 658` ```next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 659` ``` case (Suc n) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 660` ``` thus ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 661` ``` by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 662` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 663` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 664` ```lemma (in algebra) range_disjointed_sets: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 665` ``` assumes A: "range A \ sets M " ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 666` ``` shows "range (disjointed A) \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 667` ```proof (auto simp add: disjointed_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 668` ``` fix n ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 669` ``` show "A n - (\i\{0.. sets M" using UNION_in_sets ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 670` ``` by (metis A Diff UNIV_I image_subset_iff) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 671` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 672` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 673` ```lemma sigma_algebra_disjoint_iff: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 674` ``` "sigma_algebra M \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 675` ``` algebra M & ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 676` ``` (\A. range A \ sets M \ disjoint_family A \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 677` ``` (\i::nat. A i) \ sets M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 678` ```proof (auto simp add: sigma_algebra_iff) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 679` ``` fix A :: "nat \ 'a set" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 680` ``` assume M: "algebra M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 681` ``` and A: "range A \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 682` ``` and UnA: "\A. range A \ sets M \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 683` ``` disjoint_family A \ (\i::nat. A i) \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 684` ``` hence "range (disjointed A) \ sets M \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 685` ``` disjoint_family (disjointed A) \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 686` ``` (\i. disjointed A i) \ sets M" by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 687` ``` hence "(\i. disjointed A i) \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 688` ``` by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 689` ``` thus "(\i::nat. A i) \ sets M" by (simp add: UN_disjointed_eq) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 690` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 691` 39090 a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 692` ```subsection {* Sigma algebra generated by function preimages *} ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 693` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 694` ```definition (in sigma_algebra) ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 695` ``` "vimage_algebra S f = \ space = S, sets = (\A. f -` A \ S) ` sets M \" ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 696` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 697` ```lemma (in sigma_algebra) in_vimage_algebra[simp]: ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 698` ``` "A \ sets (vimage_algebra S f) \ (\B\sets M. A = f -` B \ S)" ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 699` ``` by (simp add: vimage_algebra_def image_iff) ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 700` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 701` ```lemma (in sigma_algebra) space_vimage_algebra[simp]: ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 702` ``` "space (vimage_algebra S f) = S" ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 703` ``` by (simp add: vimage_algebra_def) ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 704` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 705` ```lemma (in sigma_algebra) sigma_algebra_preimages: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 706` ``` fixes f :: "'x \ 'a" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 707` ``` assumes "f \ A \ space M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 708` ``` shows "sigma_algebra \ space = A, sets = (\M. f -` M \ A) ` sets M \" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 709` ``` (is "sigma_algebra \ space = _, sets = ?F ` sets M \") ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 710` ```proof (simp add: sigma_algebra_iff2, safe) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 711` ``` show "{} \ ?F ` sets M" by blast ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 712` ```next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 713` ``` fix S assume "S \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 714` ``` moreover have "A - ?F S = ?F (space M - S)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 715` ``` using assms by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 716` ``` ultimately show "A - ?F S \ ?F ` sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 717` ``` by blast ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 718` ```next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 719` ``` fix S :: "nat \ 'x set" assume *: "range S \ ?F ` sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 720` ``` have "\i. \b. b \ sets M \ S i = ?F b" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 721` ``` proof safe ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 722` ``` fix i ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 723` ``` have "S i \ ?F ` sets M" using * by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 724` ``` then show "\b. b \ sets M \ S i = ?F b" by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 725` ``` qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 726` ``` from choice[OF this] obtain b where b: "range b \ sets M" "\i. S i = ?F (b i)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 727` ``` by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 728` ``` then have "(\i. S i) = ?F (\i. b i)" by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 729` ``` then show "(\i. S i) \ ?F ` sets M" using b(1) by blast ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 730` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 731` 39090 a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 732` ```lemma (in sigma_algebra) sigma_algebra_vimage: ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 733` ``` fixes S :: "'c set" assumes "f \ S \ space M" ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 734` ``` shows "sigma_algebra (vimage_algebra S f)" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 735` ```proof - ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 736` ``` from sigma_algebra_preimages[OF assms] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 737` ``` show ?thesis unfolding vimage_algebra_def by (auto simp: sigma_algebra_iff2) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 738` ```qed ``` 39090 a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 739` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 740` ```lemma (in sigma_algebra) measurable_vimage_algebra: ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 741` ``` fixes S :: "'c set" assumes "f \ S \ space M" ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 742` ``` shows "f \ measurable (vimage_algebra S f) M" ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 743` ``` unfolding measurable_def using assms by force ``` a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 38656 diff changeset ` 744` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 745` ```lemma (in sigma_algebra) measurable_vimage: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 746` ``` fixes g :: "'a \ 'c" and f :: "'d \ 'a" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 747` ``` assumes "g \ measurable M M2" "f \ S \ space M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 748` ``` shows "(\x. g (f x)) \ measurable (vimage_algebra S f) M2" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 749` ```proof - ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 750` ``` note measurable_vimage_algebra[OF assms(2)] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 751` ``` from measurable_comp[OF this assms(1)] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 752` ``` show ?thesis by (simp add: comp_def) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 753` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 754` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 755` ```lemma (in sigma_algebra) vimage_vimage_inv: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 756` ``` assumes f: "bij_betw f S (space M)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 757` ``` assumes [simp]: "\x. x \ space M \ f (g x) = x" and g: "g \ space M \ S" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 758` ``` shows "sigma_algebra.vimage_algebra (vimage_algebra S f) (space M) g = M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 759` ```proof - ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 760` ``` interpret T: sigma_algebra "vimage_algebra S f" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 761` ``` using f by (safe intro!: sigma_algebra_vimage bij_betw_imp_funcset) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 762` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 763` ``` have inj: "inj_on f S" and [simp]: "f`S = space M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 764` ``` using f unfolding bij_betw_def by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 765` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 766` ``` { fix A assume A: "A \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 767` ``` have "g -` f -` A \ g -` S \ space M = (f \ g) -` A \ space M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 768` ``` using g by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 769` ``` also have "\ = A" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 770` ``` using `A \ sets M`[THEN sets_into_space] by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 771` ``` finally have "g -` f -` A \ g -` S \ space M = A" . } ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 772` ``` note X = this ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 773` ``` show ?thesis ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 774` ``` unfolding T.vimage_algebra_def unfolding vimage_algebra_def ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 775` ``` by (simp add: image_compose[symmetric] comp_def X cong: image_cong) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 776` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 777` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 778` ```lemma (in sigma_algebra) measurable_vimage_iff: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 779` ``` fixes f :: "'b \ 'a" assumes f: "bij_betw f S (space M)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 780` ``` shows "g \ measurable M M' \ (g \ f) \ measurable (vimage_algebra S f) M'" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 781` ```proof ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 782` ``` assume "g \ measurable M M'" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 783` ``` from measurable_vimage[OF this f[THEN bij_betw_imp_funcset]] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 784` ``` show "(g \ f) \ measurable (vimage_algebra S f) M'" unfolding comp_def . ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 785` ```next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 786` ``` interpret v: sigma_algebra "vimage_algebra S f" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 787` ``` using f[THEN bij_betw_imp_funcset] by (rule sigma_algebra_vimage) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 788` ``` note f' = f[THEN bij_betw_the_inv_into] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 789` ``` assume "g \ f \ measurable (vimage_algebra S f) M'" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 790` ``` from v.measurable_vimage[OF this, unfolded space_vimage_algebra, OF f'[THEN bij_betw_imp_funcset]] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 791` ``` show "g \ measurable M M'" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 792` ``` using f f'[THEN bij_betw_imp_funcset] f[unfolded bij_betw_def] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 793` ``` by (subst (asm) vimage_vimage_inv) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 794` ``` (simp_all add: f_the_inv_into_f cong: measurable_cong) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 795` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 796` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 797` ```lemma (in sigma_algebra) measurable_vimage_iff_inv: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 798` ``` fixes f :: "'b \ 'a" assumes f: "bij_betw f S (space M)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 799` ``` shows "g \ measurable (vimage_algebra S f) M' \ (g \ the_inv_into S f) \ measurable M M'" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 800` ``` unfolding measurable_vimage_iff[OF f] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 801` ``` using f[unfolded bij_betw_def] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 802` ``` by (auto intro!: measurable_cong simp add: the_inv_into_f_f) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 803` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 804` ```lemma sigma_sets_vimage: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 805` ``` assumes "f \ S' \ S" and "A \ Pow S" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 806` ``` shows "sigma_sets S' ((\X. f -` X \ S') ` A) = (\X. f -` X \ S') ` sigma_sets S A" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 807` ```proof (intro set_eqI iffI) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 808` ``` let ?F = "\X. f -` X \ S'" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 809` ``` fix X assume "X \ sigma_sets S' (?F ` A)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 810` ``` then show "X \ ?F ` sigma_sets S A" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 811` ``` proof induct ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 812` ``` case (Basic X) then obtain X' where "X = ?F X'" "X' \ A" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 813` ``` by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 814` ``` then show ?case by (auto intro!: sigma_sets.Basic) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 815` ``` next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 816` ``` case Empty then show ?case ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 817` ``` by (auto intro!: image_eqI[of _ _ "{}"] sigma_sets.Empty) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 818` ``` next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 819` ``` case (Compl X) then obtain X' where X: "X = ?F X'" and "X' \ sigma_sets S A" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 820` ``` by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 821` ``` then have "S - X' \ sigma_sets S A" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 822` ``` by (auto intro!: sigma_sets.Compl) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 823` ``` then show ?case ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 824` ``` using X assms by (auto intro!: image_eqI[where x="S - X'"]) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 825` ``` next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 826` ``` case (Union F) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 827` ``` then have "\i. \F'. F' \ sigma_sets S A \ F i = f -` F' \ S'" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 828` ``` by (auto simp: image_iff Bex_def) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 829` ``` from choice[OF this] obtain F' where ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 830` ``` "\i. F' i \ sigma_sets S A" and "\i. F i = f -` F' i \ S'" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 831` ``` by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 832` ``` then show ?case ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 833` ``` by (auto intro!: sigma_sets.Union image_eqI[where x="\i. F' i"]) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 834` ``` qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 835` ```next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 836` ``` let ?F = "\X. f -` X \ S'" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 837` ``` fix X assume "X \ ?F ` sigma_sets S A" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 838` ``` then obtain X' where "X' \ sigma_sets S A" "X = ?F X'" by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 839` ``` then show "X \ sigma_sets S' (?F ` A)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 840` ``` proof (induct arbitrary: X) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 841` ``` case (Basic X') then show ?case by (auto intro: sigma_sets.Basic) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 842` ``` next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 843` ``` case Empty then show ?case by (auto intro: sigma_sets.Empty) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 844` ``` next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 845` ``` case (Compl X') ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 846` ``` have "S' - (S' - X) \ sigma_sets S' (?F ` A)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 847` ``` apply (rule sigma_sets.Compl) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 848` ``` using assms by (auto intro!: Compl.hyps simp: Compl.prems) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 849` ``` also have "S' - (S' - X) = X" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 850` ``` using assms Compl by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 851` ``` finally show ?case . ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 852` ``` next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 853` ``` case (Union F) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 854` ``` have "(\i. f -` F i \ S') \ sigma_sets S' (?F ` A)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 855` ``` by (intro sigma_sets.Union Union.hyps) simp ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 856` ``` also have "(\i. f -` F i \ S') = X" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 857` ``` using assms Union by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 858` ``` finally show ?case . ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 859` ``` qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 860` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 861` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 862` ```section {* Conditional space *} ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 863` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 864` ```definition (in algebra) ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 865` ``` "image_space X = \ space = X`space M, sets = (\S. X`S) ` sets M \" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 866` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 867` ```definition (in algebra) ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 868` ``` "conditional_space X A = algebra.image_space (restricted_space A) X" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 869` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 870` ```lemma (in algebra) space_conditional_space: ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 871` ``` assumes "A \ sets M" shows "space (conditional_space X A) = X`A" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 872` ```proof - ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 873` ``` interpret r: algebra "restricted_space A" using assms by (rule restricted_algebra) ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 874` ``` show ?thesis unfolding conditional_space_def r.image_space_def ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 875` ``` by simp ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 876` ```qed ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39090 diff changeset ` 877` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 878` ```subsection {* A Two-Element Series *} ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 879` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 880` ```definition binaryset :: "'a set \ 'a set \ nat \ 'a set " ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 881` ``` where "binaryset A B = (\\<^isup>x. {})(0 := A, Suc 0 := B)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 882` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 883` ```lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 884` ``` apply (simp add: binaryset_def) ``` 39302 d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI nipkow parents: 39092 diff changeset ` 885` ``` apply (rule set_eqI) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 886` ``` apply (auto simp add: image_iff) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 887` ``` done ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 888` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 889` ```lemma UN_binaryset_eq: "(\i. binaryset A B i) = A \ B" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 890` ``` by (simp add: UNION_eq_Union_image range_binaryset_eq) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 891` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 892` ```section {* Closed CDI *} ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 893` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 894` ```definition ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 895` ``` closed_cdi where ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 896` ``` "closed_cdi M \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 897` ``` sets M \ Pow (space M) & ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 898` ``` (\s \ sets M. space M - s \ sets M) & ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 899` ``` (\A. (range A \ sets M) & (A 0 = {}) & (\n. A n \ A (Suc n)) \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 900` ``` (\i. A i) \ sets M) & ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 901` ``` (\A. (range A \ sets M) & disjoint_family A \ (\i::nat. A i) \ sets M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 902` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 903` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 904` ```inductive_set ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 905` ``` smallest_ccdi_sets :: "('a, 'b) algebra_scheme \ 'a set set" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 906` ``` for M ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 907` ``` where ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 908` ``` Basic [intro]: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 909` ``` "a \ sets M \ a \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 910` ``` | Compl [intro]: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 911` ``` "a \ smallest_ccdi_sets M \ space M - a \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 912` ``` | Inc: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 913` ``` "range A \ Pow(smallest_ccdi_sets M) \ A 0 = {} \ (\n. A n \ A (Suc n)) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 914` ``` \ (\i. A i) \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 915` ``` | Disj: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 916` ``` "range A \ Pow(smallest_ccdi_sets M) \ disjoint_family A ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 917` ``` \ (\i::nat. A i) \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 918` ``` monos Pow_mono ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 919` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 920` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 921` ```definition ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 922` ``` smallest_closed_cdi where ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 923` ``` "smallest_closed_cdi M = (|space = space M, sets = smallest_ccdi_sets M|)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 924` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 925` ```lemma space_smallest_closed_cdi [simp]: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 926` ``` "space (smallest_closed_cdi M) = space M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 927` ``` by (simp add: smallest_closed_cdi_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 928` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 929` ```lemma (in algebra) smallest_closed_cdi1: "sets M \ sets (smallest_closed_cdi M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 930` ``` by (auto simp add: smallest_closed_cdi_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 931` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 932` ```lemma (in algebra) smallest_ccdi_sets: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 933` ``` "smallest_ccdi_sets M \ Pow (space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 934` ``` apply (rule subsetI) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 935` ``` apply (erule smallest_ccdi_sets.induct) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 936` ``` apply (auto intro: range_subsetD dest: sets_into_space) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 937` ``` done ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 938` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 939` ```lemma (in algebra) smallest_closed_cdi2: "closed_cdi (smallest_closed_cdi M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 940` ``` apply (auto simp add: closed_cdi_def smallest_closed_cdi_def smallest_ccdi_sets) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 941` ``` apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) + ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 942` ``` done ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 943` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 944` ```lemma (in algebra) smallest_closed_cdi3: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 945` ``` "sets (smallest_closed_cdi M) \ Pow (space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 946` ``` by (simp add: smallest_closed_cdi_def smallest_ccdi_sets) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 947` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 948` ```lemma closed_cdi_subset: "closed_cdi M \ sets M \ Pow (space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 949` ``` by (simp add: closed_cdi_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 950` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 951` ```lemma closed_cdi_Compl: "closed_cdi M \ s \ sets M \ space M - s \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 952` ``` by (simp add: closed_cdi_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 953` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 954` ```lemma closed_cdi_Inc: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 955` ``` "closed_cdi M \ range A \ sets M \ A 0 = {} \ (!!n. A n \ A (Suc n)) \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 956` ``` (\i. A i) \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 957` ``` by (simp add: closed_cdi_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 958` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 959` ```lemma closed_cdi_Disj: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 960` ``` "closed_cdi M \ range A \ sets M \ disjoint_family A \ (\i::nat. A i) \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 961` ``` by (simp add: closed_cdi_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 962` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 963` ```lemma closed_cdi_Un: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 964` ``` assumes cdi: "closed_cdi M" and empty: "{} \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 965` ``` and A: "A \ sets M" and B: "B \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 966` ``` and disj: "A \ B = {}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 967` ``` shows "A \ B \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 968` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 969` ``` have ra: "range (binaryset A B) \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 970` ``` by (simp add: range_binaryset_eq empty A B) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 971` ``` have di: "disjoint_family (binaryset A B)" using disj ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 972` ``` by (simp add: disjoint_family_on_def binaryset_def Int_commute) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 973` ``` from closed_cdi_Disj [OF cdi ra di] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 974` ``` show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 975` ``` by (simp add: UN_binaryset_eq) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 976` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 977` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 978` ```lemma (in algebra) smallest_ccdi_sets_Un: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 979` ``` assumes A: "A \ smallest_ccdi_sets M" and B: "B \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 980` ``` and disj: "A \ B = {}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 981` ``` shows "A \ B \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 982` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 983` ``` have ra: "range (binaryset A B) \ Pow (smallest_ccdi_sets M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 984` ``` by (simp add: range_binaryset_eq A B smallest_ccdi_sets.Basic) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 985` ``` have di: "disjoint_family (binaryset A B)" using disj ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 986` ``` by (simp add: disjoint_family_on_def binaryset_def Int_commute) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 987` ``` from Disj [OF ra di] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 988` ``` show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 989` ``` by (simp add: UN_binaryset_eq) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 990` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 991` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 992` ```lemma (in algebra) smallest_ccdi_sets_Int1: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 993` ``` assumes a: "a \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 994` ``` shows "b \ smallest_ccdi_sets M \ a \ b \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 995` ```proof (induct rule: smallest_ccdi_sets.induct) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 996` ``` case (Basic x) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 997` ``` thus ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 998` ``` by (metis a Int smallest_ccdi_sets.Basic) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 999` ```next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1000` ``` case (Compl x) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1001` ``` have "a \ (space M - x) = space M - ((space M - a) \ (a \ x))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1002` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1003` ``` also have "... \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1004` ``` by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2 ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1005` ``` Diff_disjoint Int_Diff Int_empty_right Un_commute ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1006` ``` smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1007` ``` smallest_ccdi_sets_Un) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1008` ``` finally show ?case . ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1009` ```next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1010` ``` case (Inc A) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1011` ``` have 1: "(\i. (\i. a \ A i) i) = a \ (\i. A i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1012` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1013` ``` have "range (\i. a \ A i) \ Pow(smallest_ccdi_sets M)" using Inc ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1014` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1015` ``` moreover have "(\i. a \ A i) 0 = {}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1016` ``` by (simp add: Inc) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1017` ``` moreover have "!!n. (\i. a \ A i) n \ (\i. a \ A i) (Suc n)" using Inc ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1018` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1019` ``` ultimately have 2: "(\i. (\i. a \ A i) i) \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1020` ``` by (rule smallest_ccdi_sets.Inc) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1021` ``` show ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1022` ``` by (metis 1 2) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1023` ```next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1024` ``` case (Disj A) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1025` ``` have 1: "(\i. (\i. a \ A i) i) = a \ (\i. A i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1026` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1027` ``` have "range (\i. a \ A i) \ Pow(smallest_ccdi_sets M)" using Disj ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1028` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1029` ``` moreover have "disjoint_family (\i. a \ A i)" using Disj ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1030` ``` by (auto simp add: disjoint_family_on_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1031` ``` ultimately have 2: "(\i. (\i. a \ A i) i) \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1032` ``` by (rule smallest_ccdi_sets.Disj) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1033` ``` show ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1034` ``` by (metis 1 2) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1035` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1036` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1037` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1038` ```lemma (in algebra) smallest_ccdi_sets_Int: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1039` ``` assumes b: "b \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1040` ``` shows "a \ smallest_ccdi_sets M \ a \ b \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1041` ```proof (induct rule: smallest_ccdi_sets.induct) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1042` ``` case (Basic x) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1043` ``` thus ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1044` ``` by (metis b smallest_ccdi_sets_Int1) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1045` ```next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1046` ``` case (Compl x) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1047` ``` have "(space M - x) \ b = space M - (x \ b \ (space M - b))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1048` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1049` ``` also have "... \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1050` ``` by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1051` ``` smallest_ccdi_sets.Compl smallest_ccdi_sets_Un) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1052` ``` finally show ?case . ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1053` ```next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1054` ``` case (Inc A) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1055` ``` have 1: "(\i. (\i. A i \ b) i) = (\i. A i) \ b" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1056` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1057` ``` have "range (\i. A i \ b) \ Pow(smallest_ccdi_sets M)" using Inc ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1058` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1059` ``` moreover have "(\i. A i \ b) 0 = {}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1060` ``` by (simp add: Inc) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1061` ``` moreover have "!!n. (\i. A i \ b) n \ (\i. A i \ b) (Suc n)" using Inc ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1062` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1063` ``` ultimately have 2: "(\i. (\i. A i \ b) i) \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1064` ``` by (rule smallest_ccdi_sets.Inc) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1065` ``` show ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1066` ``` by (metis 1 2) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1067` ```next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1068` ``` case (Disj A) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1069` ``` have 1: "(\i. (\i. A i \ b) i) = (\i. A i) \ b" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1070` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1071` ``` have "range (\i. A i \ b) \ Pow(smallest_ccdi_sets M)" using Disj ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1072` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1073` ``` moreover have "disjoint_family (\i. A i \ b)" using Disj ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1074` ``` by (auto simp add: disjoint_family_on_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1075` ``` ultimately have 2: "(\i. (\i. A i \ b) i) \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1076` ``` by (rule smallest_ccdi_sets.Disj) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1077` ``` show ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1078` ``` by (metis 1 2) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1079` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1080` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1081` ```lemma (in algebra) sets_smallest_closed_cdi_Int: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1082` ``` "a \ sets (smallest_closed_cdi M) \ b \ sets (smallest_closed_cdi M) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1083` ``` \ a \ b \ sets (smallest_closed_cdi M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1084` ``` by (simp add: smallest_ccdi_sets_Int smallest_closed_cdi_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1085` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1086` ```lemma (in algebra) sigma_property_disjoint_lemma: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1087` ``` assumes sbC: "sets M \ C" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1088` ``` and ccdi: "closed_cdi (|space = space M, sets = C|)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1089` ``` shows "sigma_sets (space M) (sets M) \ C" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1090` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1091` ``` have "smallest_ccdi_sets M \ {B . sets M \ B \ sigma_algebra (|space = space M, sets = B|)}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1092` ``` apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1093` ``` smallest_ccdi_sets_Int) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1094` ``` apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1095` ``` apply (blast intro: smallest_ccdi_sets.Disj) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1096` ``` done ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1097` ``` hence "sigma_sets (space M) (sets M) \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1098` ``` by clarsimp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1099` ``` (drule sigma_algebra.sigma_sets_subset [where a="sets M"], auto) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1100` ``` also have "... \ C" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1101` ``` proof ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1102` ``` fix x ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1103` ``` assume x: "x \ smallest_ccdi_sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1104` ``` thus "x \ C" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1105` ``` proof (induct rule: smallest_ccdi_sets.induct) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1106` ``` case (Basic x) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1107` ``` thus ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1108` ``` by (metis Basic subsetD sbC) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1109` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1110` ``` case (Compl x) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1111` ``` thus ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1112` ``` by (blast intro: closed_cdi_Compl [OF ccdi, simplified]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1113` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1114` ``` case (Inc A) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1115` ``` thus ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1116` ``` by (auto intro: closed_cdi_Inc [OF ccdi, simplified]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1117` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1118` ``` case (Disj A) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1119` ``` thus ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1120` ``` by (auto intro: closed_cdi_Disj [OF ccdi, simplified]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1121` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1122` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1123` ``` finally show ?thesis . ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1124` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1125` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1126` ```lemma (in algebra) sigma_property_disjoint: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1127` ``` assumes sbC: "sets M \ C" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1128` ``` and compl: "!!s. s \ C \ sigma_sets (space M) (sets M) \ space M - s \ C" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1129` ``` and inc: "!!A. range A \ C \ sigma_sets (space M) (sets M) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1130` ``` \ A 0 = {} \ (!!n. A n \ A (Suc n)) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1131` ``` \ (\i. A i) \ C" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1132` ``` and disj: "!!A. range A \ C \ sigma_sets (space M) (sets M) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1133` ``` \ disjoint_family A \ (\i::nat. A i) \ C" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1134` ``` shows "sigma_sets (space M) (sets M) \ C" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1135` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1136` ``` have "sigma_sets (space M) (sets M) \ C \ sigma_sets (space M) (sets M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1137` ``` proof (rule sigma_property_disjoint_lemma) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1138` ``` show "sets M \ C \ sigma_sets (space M) (sets M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1139` ``` by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1140` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1141` ``` show "closed_cdi \space = space M, sets = C \ sigma_sets (space M) (sets M)\" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1142` ``` by (simp add: closed_cdi_def compl inc disj) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1143` ``` (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1144` ``` IntE sigma_sets.Compl range_subsetD sigma_sets.Union) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1145` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1146` ``` thus ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1147` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1148` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37032 diff changeset ` 1149` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1150` ```section {* Dynkin systems *} ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1151` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1152` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1153` ```locale dynkin_system = ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1154` ``` fixes M :: "'a algebra" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1155` ``` assumes space_closed: "sets M \ Pow (space M)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1156` ``` and space: "space M \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1157` ``` and compl[intro!]: "\A. A \ sets M \ space M - A \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1158` ``` and UN[intro!]: "\A. disjoint_family A \ range A \ sets M ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1159` ``` \ (\i::nat. A i) \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1160` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1161` ```lemma (in dynkin_system) sets_into_space: "\ A. A \ sets M \ A \ space M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1162` ``` using space_closed by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1163` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1164` ```lemma (in dynkin_system) empty[intro, simp]: "{} \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1165` ``` using space compl[of "space M"] by simp ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1166` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1167` ```lemma (in dynkin_system) diff: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1168` ``` assumes sets: "D \ sets M" "E \ sets M" and "D \ E" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1169` ``` shows "E - D \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1170` ```proof - ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1171` ``` let ?f = "\x. if x = 0 then D else if x = Suc 0 then space M - E else {}" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1172` ``` have "range ?f = {D, space M - E, {}}" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1173` ``` by (auto simp: image_iff) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1174` ``` moreover have "D \ (space M - E) = (\i. ?f i)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1175` ``` by (auto simp: image_iff split: split_if_asm) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1176` ``` moreover ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1177` ``` then have "disjoint_family ?f" unfolding disjoint_family_on_def ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1178` ``` using `D \ sets M`[THEN sets_into_space] `D \ E` by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1179` ``` ultimately have "space M - (D \ (space M - E)) \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1180` ``` using sets by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1181` ``` also have "space M - (D \ (space M - E)) = E - D" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1182` ``` using assms sets_into_space by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1183` ``` finally show ?thesis . ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1184` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1185` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1186` ```lemma dynkin_systemI: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1187` ``` assumes "\ A. A \ sets M \ A \ space M" "space M \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1188` ``` assumes "\ A. A \ sets M \ space M - A \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1189` ``` assumes "\ A. disjoint_family A \ range A \ sets M ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1190` ``` \ (\i::nat. A i) \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1191` ``` shows "dynkin_system M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1192` ``` using assms by (auto simp: dynkin_system_def) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1193` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1194` ```lemma dynkin_system_trivial: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1195` ``` shows "dynkin_system \ space = A, sets = Pow A \" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1196` ``` by (rule dynkin_systemI) auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1197` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1198` ```lemma sigma_algebra_imp_dynkin_system: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1199` ``` assumes "sigma_algebra M" shows "dynkin_system M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1200` ```proof - ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1201` ``` interpret sigma_algebra M by fact ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1202` ``` show ?thesis using sets_into_space by (fastsimp intro!: dynkin_systemI) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1203` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1204` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1205` ```subsection "Intersection stable algebras" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1206` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1207` ```definition "Int_stable M \ (\ a \ sets M. \ b \ sets M. a \ b \ sets M)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1208` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1209` ```lemma (in algebra) Int_stable: "Int_stable M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1210` ``` unfolding Int_stable_def by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1211` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1212` ```lemma (in dynkin_system) sigma_algebra_eq_Int_stable: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1213` ``` "sigma_algebra M \ Int_stable M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1214` ```proof ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1215` ``` assume "sigma_algebra M" then show "Int_stable M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1216` ``` unfolding sigma_algebra_def using algebra.Int_stable by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1217` ```next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1218` ``` assume "Int_stable M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1219` ``` show "sigma_algebra M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1220` ``` unfolding sigma_algebra_disjoint_iff algebra_def ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1221` ``` proof (intro conjI ballI allI impI) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1222` ``` show "sets M \ Pow (space M)" using sets_into_space by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1223` ``` next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1224` ``` fix A B assume "A \ sets M" "B \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1225` ``` then have "A \ B = space M - ((space M - A) \ (space M - B))" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1226` ``` "space M - A \ sets M" "space M - B \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1227` ``` using sets_into_space by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1228` ``` then show "A \ B \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1229` ``` using `Int_stable M` unfolding Int_stable_def by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1230` ``` qed auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1231` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1232` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1233` ```subsection "Smallest Dynkin systems" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1234` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1235` ```definition dynkin :: "'a algebra \ 'a algebra" where ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1236` ``` "dynkin M = \ space = space M, ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1237` ``` sets = \{D. dynkin_system \ space = space M, sets = D\ \ sets M \ D}\" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1238` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1239` ```lemma dynkin_system_dynkin: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1240` ``` fixes M :: "'a algebra" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1241` ``` assumes "sets M \ Pow (space M)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1242` ``` shows "dynkin_system (dynkin M)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1243` ```proof (rule dynkin_systemI) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1244` ``` fix A assume "A \ sets (dynkin M)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1245` ``` moreover ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1246` ``` { fix D assume "A \ D" and d: "dynkin_system \ space = space M, sets = D \" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1247` ``` from dynkin_system.sets_into_space[OF d] `A \ D` ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1248` ``` have "A \ space M" by auto } ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1249` ``` moreover have "{D. dynkin_system \ space = space M, sets = D\ \ sets M \ D} \ {}" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1250` ``` using assms dynkin_system_trivial by fastsimp ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1251` ``` ultimately show "A \ space (dynkin M)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1252` ``` unfolding dynkin_def using assms ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1253` ``` by simp (metis dynkin_system.sets_into_space in_mono mem_def) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1254` ```next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1255` ``` show "space (dynkin M) \ sets (dynkin M)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1256` ``` unfolding dynkin_def using dynkin_system.space by fastsimp ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1257` ```next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1258` ``` fix A assume "A \ sets (dynkin M)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1259` ``` then show "space (dynkin M) - A \ sets (dynkin M)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1260` ``` unfolding dynkin_def using dynkin_system.compl by force ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1261` ```next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1262` ``` fix A :: "nat \ 'a set" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1263` ``` assume A: "disjoint_family A" "range A \ sets (dynkin M)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1264` ``` show "(\i. A i) \ sets (dynkin M)" unfolding dynkin_def ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 40702 diff changeset ` 1265` ``` proof (simp, safe) ```