src/HOL/Probability/Caratheodory.thy
 author hoelzl Mon, 23 Aug 2010 19:35:57 +0200 changeset 38656 d5d342611edb parent 37591 d3daea901123 child 39096 111756225292 permissions -rw-r--r--
Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.
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` ```header {*Caratheodory Extension Theorem*} ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 2` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 3` ```theory Caratheodory ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 4` ``` imports Sigma_Algebra Positive_Infinite_Real ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 5` ```begin ``` 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` ```text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*} ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 8` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 9` ```subsection {* Measure Spaces *} ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 10` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 11` ```definition "positive f \ f {} = (0::pinfreal)" -- "Positive is enforced by the type" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 12` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 13` ```definition ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 14` ``` additive where ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 15` ``` "additive M f \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 16` ``` (\x \ sets M. \y \ sets M. x \ y = {} ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 17` ``` \ f (x \ y) = f x + f y)" ``` 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` ```definition ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 20` ``` countably_additive where ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 21` ``` "countably_additive M f \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 22` ``` (\A. range A \ sets M \ ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 23` ``` disjoint_family A \ ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 24` ``` (\i. A i) \ sets M \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 25` ``` (\\<^isub>\ n. f (A n)) = f (\i. A i))" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 26` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 27` ```definition ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 28` ``` increasing where ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 29` ``` "increasing M f \ (\x \ sets M. \y \ sets M. x \ y \ f x \ f y)" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 30` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 31` ```definition ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 32` ``` subadditive where ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 33` ``` "subadditive M f \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 34` ``` (\x \ sets M. \y \ sets M. x \ y = {} ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 35` ``` \ f (x \ y) \ f x + f y)" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 36` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 37` ```definition ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 38` ``` countably_subadditive where ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 39` ``` "countably_subadditive M f \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 40` ``` (\A. range A \ sets M \ ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 41` ``` disjoint_family A \ ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 42` ``` (\i. A i) \ sets M \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 43` ``` f (\i. A i) \ psuminf (\n. f (A n)))" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 44` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 45` ```definition ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 46` ``` lambda_system where ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 47` ``` "lambda_system M f = ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 48` ``` {l. l \ sets M & (\x \ sets M. f (l \ x) + f ((space M - l) \ x) = f x)}" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 49` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 50` ```definition ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 51` ``` outer_measure_space where ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 52` ``` "outer_measure_space M f \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 53` ``` positive f \ increasing M f \ countably_subadditive M f" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 54` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 55` ```definition ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 56` ``` measure_set where ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 57` ``` "measure_set M f X = ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 58` ``` {r . \A. range A \ sets M \ disjoint_family A \ X \ (\i. A i) \ (\\<^isub>\ i. f (A i)) = r}" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 59` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 60` ```locale measure_space = sigma_algebra + ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 61` ``` fixes \ :: "'a set \ pinfreal" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 62` ``` assumes empty_measure [simp]: "\ {} = 0" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 63` ``` and ca: "countably_additive M \" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 64` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 65` ```lemma increasingD: ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 66` ``` "increasing M f \ x \ y \ x\sets M \ y\sets M \ f x \ f y" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 67` ``` by (auto simp add: increasing_def) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 68` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 69` ```lemma subadditiveD: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 70` ``` "subadditive M f \ x \ y = {} \ x\sets M \ y\sets M ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 71` ``` \ f (x \ y) \ f x + f y" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 72` ``` by (auto simp add: subadditive_def) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 73` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 74` ```lemma additiveD: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 75` ``` "additive M f \ x \ y = {} \ x\sets M \ y\sets M ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 76` ``` \ f (x \ y) = f x + f y" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 77` ``` by (auto simp add: additive_def) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 78` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 79` ```lemma countably_additiveD: ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: 33536 diff changeset ` 80` ``` "countably_additive M f \ range A \ sets M \ disjoint_family A ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 81` ``` \ (\i. A i) \ sets M \ (\\<^isub>\ n. f (A n)) = f (\i. A i)" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: 33536 diff changeset ` 82` ``` by (simp add: countably_additive_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 83` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 84` ```section "Extend binary sets" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 85` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: 33536 diff changeset ` 86` ```lemma LIMSEQ_binaryset: ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 87` ``` assumes f: "f {} = 0" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 88` ``` shows "(\n. \i = 0.. f A + f B" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 89` ```proof - ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 90` ``` have "(\n. \i = 0..< Suc (Suc n). f (binaryset A B i)) = (\n. f A + f B)" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: 33536 diff changeset ` 91` ``` proof ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 92` ``` fix n ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 93` ``` show "(\i\nat = 0\nat.. f A + f B" by (rule LIMSEQ_const) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 98` ``` ultimately ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: 33536 diff changeset ` 99` ``` have "(\n. \i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 100` ``` by metis ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 101` ``` hence "(\n. \i = 0..< n+2. f (binaryset A B i)) ----> f A + f B" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 102` ``` by simp ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 103` ``` thus ?thesis by (rule LIMSEQ_offset [where k=2]) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 104` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 105` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 106` ```lemma binaryset_sums: ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 107` ``` assumes f: "f {} = 0" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 108` ``` shows "(\n. f (binaryset A B n)) sums (f A + f B)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 109` ``` by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f]) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 110` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 111` ```lemma suminf_binaryset_eq: ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 112` ``` "f {} = 0 \ suminf (\n. f (binaryset A B n)) = f A + f B" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 113` ``` by (metis binaryset_sums sums_unique) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 114` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 115` ```lemma binaryset_psuminf: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 116` ``` assumes "f {} = 0" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 117` ``` shows "(\\<^isub>\ n. f (binaryset A B n)) = f A + f B" (is "?suminf = ?sum") ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 118` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 119` ``` have *: "{..<2} = {0, 1::nat}" by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 120` ``` have "\n\2. f (binaryset A B n) = 0" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 121` ``` unfolding binaryset_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 122` ``` using assms by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 123` ``` hence "?suminf = (\N<2. f (binaryset A B N))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 124` ``` by (rule psuminf_finite) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 125` ``` also have "... = ?sum" unfolding * binaryset_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 126` ``` by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 127` ``` finally show ?thesis . ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 128` ```qed ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 129` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 130` ```subsection {* Lambda Systems *} ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 131` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 132` ```lemma (in algebra) lambda_system_eq: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 133` ``` "lambda_system M f = ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 134` ``` {l. l \ sets M & (\x \ sets M. f (x \ l) + f (x - l) = f x)}" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 135` ```proof - ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 136` ``` have [simp]: "!!l x. l \ sets M \ x \ sets M \ (space M - l) \ x = x - l" ``` 37032 58a0757031dd speed up some proofs and fix some warnings huffman parents: 36649 diff changeset ` 137` ``` by (metis Int_Diff Int_absorb1 Int_commute sets_into_space) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 138` ``` show ?thesis ``` 37032 58a0757031dd speed up some proofs and fix some warnings huffman parents: 36649 diff changeset ` 139` ``` by (auto simp add: lambda_system_def) (metis Int_commute)+ ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 140` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 141` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 142` ```lemma (in algebra) lambda_system_empty: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 143` ``` "positive f \ {} \ lambda_system M f" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 144` ``` by (auto simp add: positive_def lambda_system_eq) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 145` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 146` ```lemma lambda_system_sets: ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 147` ``` "x \ lambda_system M f \ x \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 148` ``` by (simp add: lambda_system_def) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 149` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 150` ```lemma (in algebra) lambda_system_Compl: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 151` ``` fixes f:: "'a set \ pinfreal" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 152` ``` assumes x: "x \ lambda_system M f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 153` ``` shows "space M - x \ lambda_system M f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 154` ``` proof - ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 155` ``` have "x \ space M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 156` ``` by (metis sets_into_space lambda_system_sets x) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 157` ``` hence "space M - (space M - x) = x" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 158` ``` by (metis double_diff equalityE) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 159` ``` with x show ?thesis ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 160` ``` by (force simp add: lambda_system_def ac_simps) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 161` ``` qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 162` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 163` ```lemma (in algebra) lambda_system_Int: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 164` ``` fixes f:: "'a set \ pinfreal" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 165` ``` assumes xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 166` ``` shows "x \ y \ lambda_system M f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 167` ``` proof - ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 168` ``` from xl yl show ?thesis ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 169` ``` proof (auto simp add: positive_def lambda_system_eq Int) ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 170` ``` fix u ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 171` ``` assume x: "x \ sets M" and y: "y \ sets M" and u: "u \ sets M" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 172` ``` and fx: "\z\sets M. f (z \ x) + f (z - x) = f z" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 173` ``` and fy: "\z\sets M. f (z \ y) + f (z - y) = f z" ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 174` ``` have "u - x \ y \ sets M" ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 175` ``` by (metis Diff Diff_Int Un u x y) ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 176` ``` moreover ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 177` ``` have "(u - (x \ y)) \ y = u \ y - x" by blast ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 178` ``` moreover ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 179` ``` have "u - x \ y - y = u - y" by blast ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 180` ``` ultimately ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 181` ``` have ey: "f (u - x \ y) = f (u \ y - x) + f (u - y)" using fy ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 182` ``` by force ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 183` ``` have "f (u \ (x \ y)) + f (u - x \ y) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 184` ``` = (f (u \ (x \ y)) + f (u \ y - x)) + f (u - y)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 185` ``` by (simp add: ey ac_simps) ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 186` ``` also have "... = (f ((u \ y) \ x) + f (u \ y - x)) + f (u - y)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 187` ``` by (simp add: Int_ac) ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 188` ``` also have "... = f (u \ y) + f (u - y)" ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 189` ``` using fx [THEN bspec, of "u \ y"] Int y u ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 190` ``` by force ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 191` ``` also have "... = f u" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 192` ``` by (metis fy u) ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 193` ``` finally show "f (u \ (x \ y)) + f (u - x \ y) = f u" . ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 194` ``` qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 195` ``` qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 196` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 197` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 198` ```lemma (in algebra) lambda_system_Un: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 199` ``` fixes f:: "'a set \ pinfreal" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 200` ``` assumes xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 201` ``` shows "x \ y \ lambda_system M f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 202` ```proof - ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 203` ``` have "(space M - x) \ (space M - y) \ sets M" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 204` ``` by (metis Diff_Un Un compl_sets lambda_system_sets xl yl) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 205` ``` moreover ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 206` ``` have "x \ y = space M - ((space M - x) \ (space M - y))" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 207` ``` by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+ ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 208` ``` ultimately show ?thesis ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 209` ``` by (metis lambda_system_Compl lambda_system_Int xl yl) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 210` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 211` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 212` ```lemma (in algebra) lambda_system_algebra: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 213` ``` "positive f \ algebra (M (|sets := lambda_system M f|))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 214` ``` apply (auto simp add: algebra_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 215` ``` apply (metis lambda_system_sets set_mp sets_into_space) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 216` ``` apply (metis lambda_system_empty) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 217` ``` apply (metis lambda_system_Compl) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 218` ``` apply (metis lambda_system_Un) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 219` ``` done ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 220` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 221` ```lemma (in algebra) lambda_system_strong_additive: ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 222` ``` assumes z: "z \ sets M" and disj: "x \ y = {}" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 223` ``` and xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 224` ``` shows "f (z \ (x \ y)) = f (z \ x) + f (z \ y)" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 225` ``` proof - ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 226` ``` have "z \ x = (z \ (x \ y)) \ x" using disj by blast ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 227` ``` moreover ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 228` ``` have "z \ y = (z \ (x \ y)) - x" using disj by blast ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 229` ``` moreover ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 230` ``` have "(z \ (x \ y)) \ sets M" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 231` ``` by (metis Int Un lambda_system_sets xl yl z) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 232` ``` ultimately show ?thesis using xl yl ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 233` ``` by (simp add: lambda_system_eq) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 234` ``` qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 235` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 236` ```lemma (in algebra) lambda_system_additive: ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 237` ``` "additive (M (|sets := lambda_system M f|)) f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 238` ``` proof (auto simp add: additive_def) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 239` ``` fix x and y ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 240` ``` assume disj: "x \ y = {}" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 241` ``` and xl: "x \ lambda_system M f" and yl: "y \ lambda_system M f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 242` ``` hence "x \ sets M" "y \ sets M" by (blast intro: lambda_system_sets)+ ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 243` ``` thus "f (x \ y) = f x + f y" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 244` ``` using lambda_system_strong_additive [OF top disj xl yl] ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 245` ``` by (simp add: Un) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 246` ``` qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 247` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 248` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 249` ```lemma (in algebra) countably_subadditive_subadditive: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 250` ``` assumes f: "positive f" and cs: "countably_subadditive M f" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 251` ``` shows "subadditive M f" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: 33536 diff changeset ` 252` ```proof (auto simp add: subadditive_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 253` ``` fix x y ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 254` ``` assume x: "x \ sets M" and y: "y \ sets M" and "x \ y = {}" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 255` ``` hence "disjoint_family (binaryset x y)" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: 33536 diff changeset ` 256` ``` by (auto simp add: disjoint_family_on_def binaryset_def) ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: 33536 diff changeset ` 257` ``` hence "range (binaryset x y) \ sets M \ ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: 33536 diff changeset ` 258` ``` (\i. binaryset x y i) \ sets M \ ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 259` ``` f (\i. binaryset x y i) \ (\\<^isub>\ n. f (binaryset x y n))" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: 33536 diff changeset ` 260` ``` using cs by (simp add: countably_subadditive_def) ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: 33536 diff changeset ` 261` ``` hence "{x,y,{}} \ sets M \ x \ y \ sets M \ ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 262` ``` f (x \ y) \ (\\<^isub>\ n. f (binaryset x y n))" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 263` ``` by (simp add: range_binaryset_eq UN_binaryset_eq) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 264` ``` thus "f (x \ y) \ f x + f y" using f x y ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 265` ``` by (auto simp add: Un o_def binaryset_psuminf positive_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 266` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 267` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 268` ```lemma (in algebra) additive_sum: ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 269` ``` fixes A:: "nat \ 'a set" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 270` ``` assumes f: "positive f" and ad: "additive M f" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 271` ``` and A: "range A \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 272` ``` and disj: "disjoint_family A" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 273` ``` shows "setsum (f \ A) {0..i\{0.. (\i\{0.. sets M" using A by blast ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 282` ``` moreover have "(\i\{0.. sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 283` ``` by (metis A UNION_in_sets atLeast0LessThan) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 284` ``` moreover ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 285` ``` ultimately have "f (A n \ (\i\{0..i\{0.. range A \ sets M \ disjoint_family A \ ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 294` ``` (\i. A i) \ sets M \ f (\i. A i) \ psuminf (f o A)" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 295` ``` by (auto simp add: countably_subadditive_def o_def) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 296` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 297` ```lemma (in algebra) increasing_additive_bound: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 298` ``` fixes A:: "nat \ 'a set" and f :: "'a set \ pinfreal" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 299` ``` assumes f: "positive f" and ad: "additive M f" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 300` ``` and inc: "increasing M f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 301` ``` and A: "range A \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 302` ``` and disj: "disjoint_family A" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 303` ``` shows "psuminf (f \ A) \ f (space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 304` ```proof (safe intro!: psuminf_bound) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 305` ``` fix N ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 306` ``` have "setsum (f \ A) {0..i\{0.. f (space M)" using space_closed A ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 309` ``` by (blast intro: increasingD [OF inc] UNION_in_sets top) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 310` ``` finally show "setsum (f \ A) {.. f (space M)" by (simp add: atLeast0LessThan) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 311` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 312` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 313` ```lemma lambda_system_increasing: ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 314` ``` "increasing M f \ increasing (M (|sets := lambda_system M f|)) f" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 315` ``` by (simp add: increasing_def lambda_system_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 316` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 317` ```lemma (in algebra) lambda_system_strong_sum: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 318` ``` fixes A:: "nat \ 'a set" and f :: "'a set \ pinfreal" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 319` ``` assumes f: "positive f" and a: "a \ sets M" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 320` ``` and A: "range A \ lambda_system M f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 321` ``` and disj: "disjoint_family A" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 322` ``` shows "(\i = 0..A i)) = f (a \ (\i\{0.. UNION {0.. lambda_system M f" using A ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 330` ``` by blast ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 331` ``` have 4: "UNION {0.. lambda_system M f" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 332` ``` using A algebra.UNION_in_sets [OF local.lambda_system_algebra, of f, OF f] ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 333` ``` by simp ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 334` ``` from Suc.hyps show ?case ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 335` ``` by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4]) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 336` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 337` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 338` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 339` ```lemma (in sigma_algebra) lambda_system_caratheodory: ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 340` ``` assumes oms: "outer_measure_space M f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 341` ``` and A: "range A \ lambda_system M f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 342` ``` and disj: "disjoint_family A" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 343` ``` shows "(\i. A i) \ lambda_system M f \ psuminf (f \ A) = f (\i. A i)" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 344` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 345` ``` have pos: "positive f" and inc: "increasing M f" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 346` ``` and csa: "countably_subadditive M f" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 347` ``` by (metis oms outer_measure_space_def)+ ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 348` ``` have sa: "subadditive M f" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 349` ``` by (metis countably_subadditive_subadditive csa pos) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 350` ``` have A': "range A \ sets (M(|sets := lambda_system M f|))" using A ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 351` ``` by simp ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 352` ``` have alg_ls: "algebra (M(|sets := lambda_system M f|))" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 353` ``` by (rule lambda_system_algebra) (rule pos) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 354` ``` have A'': "range A \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 355` ``` by (metis A image_subset_iff lambda_system_sets) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 356` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 357` ``` have U_in: "(\i. A i) \ sets M" ``` 37032 58a0757031dd speed up some proofs and fix some warnings huffman parents: 36649 diff changeset ` 358` ``` by (metis A'' countable_UN) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 359` ``` have U_eq: "f (\i. A i) = psuminf (f o A)" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 360` ``` proof (rule antisym) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 361` ``` show "f (\i. A i) \ psuminf (f \ A)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 362` ``` by (rule countably_subadditiveD [OF csa A'' disj U_in]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 363` ``` show "psuminf (f \ A) \ f (\i. A i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 364` ``` by (rule psuminf_bound, unfold atLeast0LessThan[symmetric]) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 365` ``` (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 366` ``` lambda_system_additive subset_Un_eq increasingD [OF inc] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 367` ``` A' A'' UNION_in_sets U_in) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 368` ``` qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 369` ``` { ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 370` ``` fix a ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 371` ``` assume a [iff]: "a \ sets M" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 372` ``` have "f (a \ (\i. A i)) + f (a - (\i. A i)) = f a" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 373` ``` proof - ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 374` ``` show ?thesis ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 375` ``` proof (rule antisym) ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 376` ``` have "range (\i. a \ A i) \ sets M" using A'' ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 377` ``` by blast ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 378` ``` moreover ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 379` ``` have "disjoint_family (\i. a \ A i)" using disj ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 380` ``` by (auto simp add: disjoint_family_on_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 381` ``` moreover ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 382` ``` have "a \ (\i. A i) \ sets M" ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 383` ``` by (metis Int U_in a) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 384` ``` ultimately ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 385` ``` have "f (a \ (\i. A i)) \ psuminf (f \ (\i. a \ i) \ A)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 386` ``` using countably_subadditiveD [OF csa, of "(\i. a \ A i)"] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 387` ``` by (simp add: o_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 388` ``` hence "f (a \ (\i. A i)) + f (a - (\i. A i)) \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 389` ``` psuminf (f \ (\i. a \ i) \ A) + f (a - (\i. A i))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 390` ``` by (rule add_right_mono) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 391` ``` moreover ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 392` ``` have "psuminf (f \ (\i. a \ i) \ A) + f (a - (\i. A i)) \ f a" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 393` ``` proof (safe intro!: psuminf_bound_add) ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 394` ``` fix n ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 395` ``` have UNION_in: "(\i\{0.. sets M" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 396` ``` by (metis A'' UNION_in_sets) ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 397` ``` have le_fa: "f (UNION {0.. a) \ f a" using A'' ``` 37032 58a0757031dd speed up some proofs and fix some warnings huffman parents: 36649 diff changeset ` 398` ``` by (blast intro: increasingD [OF inc] A'' UNION_in_sets) ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 399` ``` have ls: "(\i\{0.. lambda_system M f" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 400` ``` using algebra.UNION_in_sets [OF lambda_system_algebra [of f, OF pos]] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 401` ``` by (simp add: A) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 402` ``` hence eq_fa: "f a = f (a \ (\i\{0..i\{0..i. A i)) \ f (a - (\i\{0.. (\i. a \ i) \ A) {..i. A i)) \ f a" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 408` ``` by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric]) ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 409` ``` qed ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 410` ``` ultimately show "f (a \ (\i. A i)) + f (a - (\i. A i)) \ f a" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 411` ``` by (rule order_trans) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 412` ``` next ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 413` ``` have "f a \ f (a \ (\i. A i) \ (a - (\i. A i)))" ``` 37032 58a0757031dd speed up some proofs and fix some warnings huffman parents: 36649 diff changeset ` 414` ``` by (blast intro: increasingD [OF inc] U_in) ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 415` ``` also have "... \ f (a \ (\i. A i)) + f (a - (\i. A i))" ``` 37032 58a0757031dd speed up some proofs and fix some warnings huffman parents: 36649 diff changeset ` 416` ``` by (blast intro: subadditiveD [OF sa] U_in) ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 417` ``` finally show "f a \ f (a \ (\i. A i)) + f (a - (\i. A i))" . ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 418` ``` qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 419` ``` qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 420` ``` } ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 421` ``` thus ?thesis ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 422` ``` by (simp add: lambda_system_eq sums_iff U_eq U_in) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 423` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 424` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 425` ```lemma (in sigma_algebra) caratheodory_lemma: ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 426` ``` assumes oms: "outer_measure_space M f" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 427` ``` shows "measure_space (|space = space M, sets = lambda_system M f|) f" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 428` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 429` ``` have pos: "positive f" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 430` ``` by (metis oms outer_measure_space_def) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 431` ``` have alg: "algebra (|space = space M, sets = lambda_system M f|)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 432` ``` using lambda_system_algebra [of f, OF pos] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 433` ``` by (simp add: algebra_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 434` ``` then moreover ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 435` ``` have "sigma_algebra (|space = space M, sets = lambda_system M f|)" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 436` ``` using lambda_system_caratheodory [OF oms] ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 437` ``` by (simp add: sigma_algebra_disjoint_iff) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 438` ``` moreover ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 439` ``` have "measure_space_axioms (|space = space M, sets = lambda_system M f|) f" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 440` ``` using pos lambda_system_caratheodory [OF oms] ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 441` ``` by (simp add: measure_space_axioms_def positive_def lambda_system_sets ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 442` ``` countably_additive_def o_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 443` ``` ultimately ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 444` ``` show ?thesis ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 445` ``` by intro_locales (auto simp add: sigma_algebra_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 446` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 447` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 448` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 449` ```lemma (in algebra) inf_measure_nonempty: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 450` ``` assumes f: "positive f" and b: "b \ sets M" and a: "a \ b" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 451` ``` shows "f b \ measure_set M f a" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 452` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 453` ``` have "psuminf (f \ (\i. {})(0 := b)) = setsum (f \ (\i. {})(0 := b)) {..<1::nat}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 454` ``` by (rule psuminf_finite) (simp add: f[unfolded positive_def]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 455` ``` also have "... = f b" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 456` ``` by simp ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 457` ``` finally have "psuminf (f \ (\i. {})(0 := b)) = f b" . ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 458` ``` thus ?thesis using a b ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 459` ``` by (auto intro!: exI [of _ "(\i. {})(0 := b)"] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 460` ``` simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 461` ```qed ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 462` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 463` ```lemma (in algebra) additive_increasing: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 464` ``` assumes posf: "positive f" and addf: "additive M f" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 465` ``` shows "increasing M f" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 466` ```proof (auto simp add: increasing_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 467` ``` fix x y ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 468` ``` assume xy: "x \ sets M" "y \ sets M" "x \ y" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 469` ``` have "f x \ f x + f (y-x)" .. ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 470` ``` also have "... = f (x \ (y-x))" using addf ``` 37032 58a0757031dd speed up some proofs and fix some warnings huffman parents: 36649 diff changeset ` 471` ``` by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2)) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 472` ``` also have "... = f y" ``` 37032 58a0757031dd speed up some proofs and fix some warnings huffman parents: 36649 diff changeset ` 473` ``` by (metis Un_Diff_cancel Un_absorb1 xy(3)) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 474` ``` finally show "f x \ f y" . ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 475` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 476` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 477` ```lemma (in algebra) countably_additive_additive: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 478` ``` assumes posf: "positive f" and ca: "countably_additive M f" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 479` ``` shows "additive M f" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 480` ```proof (auto simp add: additive_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 481` ``` fix x y ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 482` ``` assume x: "x \ sets M" and y: "y \ sets M" and "x \ y = {}" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 483` ``` hence "disjoint_family (binaryset x y)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 484` ``` by (auto simp add: disjoint_family_on_def binaryset_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 485` ``` hence "range (binaryset x y) \ sets M \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 486` ``` (\i. binaryset x y i) \ sets M \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 487` ``` f (\i. binaryset x y i) = (\\<^isub>\ n. f (binaryset x y n))" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 488` ``` using ca ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 489` ``` by (simp add: countably_additive_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 490` ``` hence "{x,y,{}} \ sets M \ x \ y \ sets M \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 491` ``` f (x \ y) = (\\<^isub>\ n. f (binaryset x y n))" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 492` ``` by (simp add: range_binaryset_eq UN_binaryset_eq) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 493` ``` thus "f (x \ y) = f x + f y" using posf x y ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 494` ``` by (auto simp add: Un binaryset_psuminf positive_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 495` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 496` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 497` ```lemma (in algebra) inf_measure_agrees: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 498` ``` assumes posf: "positive f" and ca: "countably_additive M f" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 499` ``` and s: "s \ sets M" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 500` ``` shows "Inf (measure_set M f s) = f s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 501` ``` unfolding Inf_pinfreal_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 502` ```proof (safe intro!: Greatest_equality) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 503` ``` fix z ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 504` ``` assume z: "z \ measure_set M f s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 505` ``` from this obtain A where ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 506` ``` A: "range A \ sets M" and disj: "disjoint_family A" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 507` ``` and "s \ (\x. A x)" and si: "psuminf (f \ A) = z" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 508` ``` by (auto simp add: measure_set_def comp_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 509` ``` hence seq: "s = (\i. A i \ s)" by blast ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 510` ``` have inc: "increasing M f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 511` ``` by (metis additive_increasing ca countably_additive_additive posf) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 512` ``` have sums: "psuminf (\i. f (A i \ s)) = f (\i. A i \ s)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 513` ``` proof (rule countably_additiveD [OF ca]) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 514` ``` show "range (\n. A n \ s) \ sets M" using A s ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 515` ``` by blast ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 516` ``` show "disjoint_family (\n. A n \ s)" using disj ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: 33536 diff changeset ` 517` ``` by (auto simp add: disjoint_family_on_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 518` ``` show "(\i. A i \ s) \ sets M" using A s ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 519` ``` by (metis UN_extend_simps(4) s seq) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 520` ``` qed ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 521` ``` hence "f s = psuminf (\i. f (A i \ s))" ``` 37032 58a0757031dd speed up some proofs and fix some warnings huffman parents: 36649 diff changeset ` 522` ``` using seq [symmetric] by (simp add: sums_iff) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 523` ``` also have "... \ psuminf (f \ A)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 524` ``` proof (rule psuminf_le) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 525` ``` fix n show "f (A n \ s) \ (f \ A) n" using A s ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 526` ``` by (force intro: increasingD [OF inc]) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 527` ``` qed ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 528` ``` also have "... = z" by (rule si) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 529` ``` finally show "f s \ z" . ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 530` ```next ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 531` ``` fix y ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 532` ``` assume y: "\u \ measure_set M f s. y \ u" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 533` ``` thus "y \ f s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 534` ``` by (blast intro: inf_measure_nonempty [of f, OF posf s subset_refl]) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 535` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 536` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 537` ```lemma (in algebra) inf_measure_empty: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 538` ``` assumes posf: "positive f" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 539` ``` shows "Inf (measure_set M f {}) = 0" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 540` ```proof (rule antisym) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 541` ``` show "Inf (measure_set M f {}) \ 0" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 542` ``` by (metis complete_lattice_class.Inf_lower empty_sets inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 543` ```qed simp ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 544` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 545` ```lemma (in algebra) inf_measure_positive: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 546` ``` "positive f \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 547` ``` positive (\x. Inf (measure_set M f x))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 548` ``` by (simp add: positive_def inf_measure_empty) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 549` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 550` ```lemma (in algebra) inf_measure_increasing: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 551` ``` assumes posf: "positive f" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 552` ``` shows "increasing (| space = space M, sets = Pow (space M) |) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 553` ``` (\x. Inf (measure_set M f x))" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 554` ```apply (auto simp add: increasing_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 555` ```apply (rule complete_lattice_class.Inf_greatest) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 556` ```apply (rule complete_lattice_class.Inf_lower) ``` 37032 58a0757031dd speed up some proofs and fix some warnings huffman parents: 36649 diff changeset ` 557` ```apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 558` ```done ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 559` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 560` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 561` ```lemma (in algebra) inf_measure_le: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 562` ``` assumes posf: "positive f" and inc: "increasing M f" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 563` ``` and x: "x \ {r . \A. range A \ sets M \ s \ (\i. A i) \ psuminf (f \ A) = r}" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 564` ``` shows "Inf (measure_set M f s) \ x" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 565` ```proof - ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 566` ``` from x ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 567` ``` obtain A where A: "range A \ sets M" and ss: "s \ (\i. A i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 568` ``` and xeq: "psuminf (f \ A) = x" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 569` ``` by auto ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 570` ``` have dA: "range (disjointed A) \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 571` ``` by (metis A range_disjointed_sets) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 572` ``` have "\n.(f o disjointed A) n \ (f \ A) n" unfolding comp_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 573` ``` by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A comp_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 574` ``` hence sda: "psuminf (f o disjointed A) \ psuminf (f \ A)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 575` ``` by (blast intro: psuminf_le) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 576` ``` hence ley: "psuminf (f o disjointed A) \ x" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 577` ``` by (metis xeq) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 578` ``` hence y: "psuminf (f o disjointed A) \ measure_set M f s" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 579` ``` apply (auto simp add: measure_set_def) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 580` ``` apply (rule_tac x="disjointed A" in exI) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 581` ``` apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA comp_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 582` ``` done ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 583` ``` show ?thesis ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 584` ``` by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 585` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 586` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 587` ```lemma (in algebra) inf_measure_close: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 588` ``` assumes posf: "positive f" and e: "0 < e" and ss: "s \ (space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 589` ``` shows "\A. range A \ sets M \ disjoint_family A \ s \ (\i. A i) \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 590` ``` psuminf (f \ A) \ Inf (measure_set M f s) + e" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 591` ```proof (cases "Inf (measure_set M f s) = \") ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 592` ``` case False ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 593` ``` obtain l where "l \ measure_set M f s" "l \ Inf (measure_set M f s) + e" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 594` ``` using Inf_close[OF False e] by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 595` ``` thus ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 596` ``` by (auto intro!: exI[of _ l] simp: measure_set_def comp_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 597` ```next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 598` ``` case True ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 599` ``` have "measure_set M f s \ {}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 600` ``` by (metis emptyE ss inf_measure_nonempty [of f, OF posf top]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 601` ``` then obtain l where "l \ measure_set M f s" by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 602` ``` moreover from True have "l \ Inf (measure_set M f s) + e" by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 603` ``` ultimately show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 604` ``` by (auto intro!: exI[of _ l] simp: measure_set_def comp_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 605` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 606` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 607` ```lemma (in algebra) inf_measure_countably_subadditive: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 608` ``` assumes posf: "positive f" and inc: "increasing M f" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 609` ``` shows "countably_subadditive (| space = space M, sets = Pow (space M) |) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 610` ``` (\x. Inf (measure_set M f x))" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 611` ``` unfolding countably_subadditive_def o_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 612` ```proof (safe, simp, rule pinfreal_le_epsilon) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 613` ``` fix A :: "nat \ 'a set" and e :: pinfreal ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 614` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 615` ``` let "?outer n" = "Inf (measure_set M f (A n))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 616` ``` assume A: "range A \ Pow (space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 617` ``` and disj: "disjoint_family A" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 618` ``` and sb: "(\i. A i) \ space M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 619` ``` and e: "0 < e" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 620` ``` hence "\BB. \n. range (BB n) \ sets M \ disjoint_family (BB n) \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 621` ``` A n \ (\i. BB n i) \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 622` ``` psuminf (f o BB n) \ ?outer n + e * (1/2)^(Suc n)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 623` ``` apply (safe intro!: choice inf_measure_close [of f, OF posf _]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 624` ``` using e sb by (cases e, auto simp add: not_le mult_pos_pos) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 625` ``` then obtain BB ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 626` ``` where BB: "\n. (range (BB n) \ sets M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 627` ``` and disjBB: "\n. disjoint_family (BB n)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 628` ``` and sbBB: "\n. A n \ (\i. BB n i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 629` ``` and BBle: "\n. psuminf (f o BB n) \ ?outer n + e * (1/2)^(Suc n)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 630` ``` by auto blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 631` ``` have sll: "(\\<^isub>\ n. psuminf (f o BB n)) \ psuminf ?outer + e" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 632` ``` proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 633` ``` have "(\\<^isub>\ n. psuminf (f o BB n)) \ (\\<^isub>\ n. ?outer n + e*(1/2) ^ Suc n)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 634` ``` by (rule psuminf_le[OF BBle]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 635` ``` also have "... = psuminf ?outer + e" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 636` ``` using psuminf_half_series by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 637` ``` finally show ?thesis . ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 638` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 639` ``` def C \ "(split BB) o prod_decode" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 640` ``` have C: "!!n. C n \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 641` ``` apply (rule_tac p="prod_decode n" in PairE) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 642` ``` apply (simp add: C_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 643` ``` apply (metis BB subsetD rangeI) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 644` ``` done ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 645` ``` have sbC: "(\i. A i) \ (\i. C i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 646` ``` proof (auto simp add: C_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 647` ``` fix x i ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 648` ``` assume x: "x \ A i" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 649` ``` with sbBB [of i] obtain j where "x \ BB i j" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 650` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 651` ``` thus "\i. x \ split BB (prod_decode i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 652` ``` by (metis prod_encode_inverse prod.cases) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 653` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 654` ``` have "(f \ C) = (f \ (\(x, y). BB x y)) \ prod_decode" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 655` ``` by (rule ext) (auto simp add: C_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 656` ``` moreover have "psuminf ... = (\\<^isub>\ n. psuminf (f o BB n))" using BBle ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 657` ``` by (force intro!: psuminf_2dimen simp: o_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 658` ``` ultimately have Csums: "psuminf (f \ C) = (\\<^isub>\ n. psuminf (f o BB n))" by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 659` ``` have "Inf (measure_set M f (\i. A i)) \ (\\<^isub>\ n. psuminf (f o BB n))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 660` ``` apply (rule inf_measure_le [OF posf(1) inc], auto) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 661` ``` apply (rule_tac x="C" in exI) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 662` ``` apply (auto simp add: C sbC Csums) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 663` ``` done ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 664` ``` also have "... \ (\\<^isub>\n. Inf (measure_set M f (A n))) + e" using sll ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 665` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 666` ``` finally show "Inf (measure_set M f (\i. A i)) \ psuminf ?outer + e" . ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 667` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 668` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 669` ```lemma (in algebra) inf_measure_outer: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 670` ``` "\ positive f ; increasing M f \ ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 671` ``` \ outer_measure_space (| space = space M, sets = Pow (space M) |) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 672` ``` (\x. Inf (measure_set M f x))" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 673` ``` by (simp add: outer_measure_space_def inf_measure_empty ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 674` ``` inf_measure_increasing inf_measure_countably_subadditive positive_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 675` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 676` ```(*MOVE UP*) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 677` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 678` ```lemma (in algebra) algebra_subset_lambda_system: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 679` ``` assumes posf: "positive f" and inc: "increasing M f" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 680` ``` and add: "additive M f" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 681` ``` shows "sets M \ lambda_system (| space = space M, sets = Pow (space M) |) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 682` ``` (\x. Inf (measure_set M f x))" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 683` ```proof (auto dest: sets_into_space ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 684` ``` simp add: algebra.lambda_system_eq [OF algebra_Pow]) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 685` ``` fix x s ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 686` ``` assume x: "x \ sets M" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 687` ``` and s: "s \ space M" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 688` ``` have [simp]: "!!x. x \ sets M \ s \ (space M - x) = s-x" using s ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 689` ``` by blast ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 690` ``` have "Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x)) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 691` ``` \ Inf (measure_set M f s)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 692` ``` proof (rule pinfreal_le_epsilon) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 693` ``` fix e :: pinfreal ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 694` ``` assume e: "0 < e" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 695` ``` from inf_measure_close [of f, OF posf e s] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 696` ``` obtain A where A: "range A \ sets M" and disj: "disjoint_family A" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 697` ``` and sUN: "s \ (\i. A i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 698` ``` and l: "psuminf (f \ A) \ Inf (measure_set M f s) + e" ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 699` ``` by auto ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 700` ``` have [simp]: "!!x. x \ sets M \ ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 701` ``` (f o (\z. z \ (space M - x)) o A) = (f o (\z. z - x) o A)" ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 702` ``` by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 703` ``` have [simp]: "!!n. f (A n \ x) + f (A n - x) = f (A n)" ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 704` ``` by (subst additiveD [OF add, symmetric]) ``` fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 705` ``` (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 706` ``` { fix u ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 707` ``` assume u: "u \ sets M" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 708` ``` have [simp]: "\n. f (A n \ u) \ f (A n)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 709` ``` by (simp add: increasingD [OF inc] u Int range_subsetD [OF A]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 710` ``` have 2: "Inf (measure_set M f (s \ u)) \ psuminf (f \ (\z. z \ u) \ A)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 711` ``` proof (rule complete_lattice_class.Inf_lower) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 712` ``` show "psuminf (f \ (\z. z \ u) \ A) \ measure_set M f (s \ u)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 713` ``` apply (simp add: measure_set_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 714` ``` apply (rule_tac x="(\z. z \ u) o A" in exI) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 715` ``` apply (auto simp add: disjoint_family_subset [OF disj] o_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 716` ``` apply (blast intro: u range_subsetD [OF A]) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 717` ``` apply (blast dest: subsetD [OF sUN]) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 718` ``` done ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 719` ``` qed ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 720` ``` } note lesum = this ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 721` ``` have inf1: "Inf (measure_set M f (s\x)) \ psuminf (f o (\z. z\x) o A)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 722` ``` and inf2: "Inf (measure_set M f (s \ (space M - x))) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 723` ``` \ psuminf (f o (\z. z \ (space M - x)) o A)" ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 724` ``` by (metis Diff lesum top x)+ ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 725` ``` hence "Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x)) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 726` ``` \ psuminf (f o (\s. s\x) o A) + psuminf (f o (\s. s-x) o A)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 727` ``` by (simp add: x add_mono) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 728` ``` also have "... \ psuminf (f o A)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 729` ``` by (simp add: x psuminf_add[symmetric] o_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 730` ``` also have "... \ Inf (measure_set M f s) + e" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 731` ``` by (rule l) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 732` ``` finally show "Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x)) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 733` ``` \ Inf (measure_set M f s) + e" . ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 734` ``` qed ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 735` ``` moreover ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 736` ``` have "Inf (measure_set M f s) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 737` ``` \ Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x))" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 738` ``` proof - ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 739` ``` have "Inf (measure_set M f s) = Inf (measure_set M f ((s\x) \ (s-x)))" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 740` ``` by (metis Un_Diff_Int Un_commute) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 741` ``` also have "... \ Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 742` ``` apply (rule subadditiveD) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 743` ``` apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow ``` 33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset ` 744` ``` inf_measure_positive inf_measure_countably_subadditive posf inc) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 745` ``` apply (auto simp add: subsetD [OF s]) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 746` ``` done ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 747` ``` finally show ?thesis . ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 748` ``` qed ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 749` ``` ultimately ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 750` ``` show "Inf (measure_set M f (s\x)) + Inf (measure_set M f (s-x)) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 751` ``` = Inf (measure_set M f s)" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 752` ``` by (rule order_antisym) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 753` ```qed ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 754` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 755` ```lemma measure_down: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 756` ``` "measure_space N \ \ sigma_algebra M \ sets M \ sets N \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 757` ``` (\ = \) \ measure_space M \" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 758` ``` by (simp add: measure_space_def measure_space_axioms_def positive_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 759` ``` countably_additive_def) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 760` ``` blast ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 761` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 762` ```theorem (in algebra) caratheodory: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 763` ``` assumes posf: "positive f" and ca: "countably_additive M f" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 764` ``` shows "\\ :: 'a set \ pinfreal. (\s \ sets M. \ s = f s) \ measure_space (sigma (space M) (sets M)) \" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 765` ``` proof - ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 766` ``` have inc: "increasing M f" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 767` ``` by (metis additive_increasing ca countably_additive_additive posf) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 768` ``` let ?infm = "(\x. Inf (measure_set M f x))" ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 769` ``` def ls \ "lambda_system (|space = space M, sets = Pow (space M)|) ?infm" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 770` ``` have mls: "measure_space \space = space M, sets = ls\ ?infm" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 771` ``` using sigma_algebra.caratheodory_lemma ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 772` ``` [OF sigma_algebra_Pow inf_measure_outer [OF posf inc]] ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 773` ``` by (simp add: ls_def) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 774` ``` hence sls: "sigma_algebra (|space = space M, sets = ls|)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 775` ``` by (simp add: measure_space_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 776` ``` have "sets M \ ls" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 777` ``` by (simp add: ls_def) ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 778` ``` (metis ca posf inc countably_additive_additive algebra_subset_lambda_system) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 779` ``` hence sgs_sb: "sigma_sets (space M) (sets M) \ ls" ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 780` ``` using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"] ``` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 781` ``` by simp ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 782` ``` have "measure_space (sigma (space M) (sets M)) ?infm" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 783` ``` unfolding sigma_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 784` ``` by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 785` ``` (simp_all add: sgs_sb space_closed) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 786` ``` thus ?thesis using inf_measure_agrees [OF posf ca] by (auto intro!: exI[of _ ?infm]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 37591 diff changeset ` 787` ``` qed ``` 33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 788` 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset ` 789` ```end ```