src/HOL/Probability/Product_Measure.thy
 author hoelzl Wed, 01 Dec 2010 19:20:30 +0100 changeset 40859 de0b30e6c2d2 parent 39098 21e9bd6cf0a8 child 40871 688f6ff859e1 permissions -rw-r--r--
Support product spaces on sigma finite measures. Introduce the almost everywhere quantifier. Introduce 'morphism' theorems for most constants. Prove uniqueness of measures on cut stable generators. Prove uniqueness of the Radon-Nikodym derivative. Removed misleading suffix from borel_space and lebesgue_space. Use product spaces to introduce Fubini on the Lebesgue integral. Combine Euclidean_Lebesgue and Lebesgue_Measure. Generalize theorems about mutual information and entropy to arbitrary probability spaces. Remove simproc mult_log as it does not work with interpretations. Introduce completion of measure spaces. Change type of sigma. Introduce dynkin systems.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 35833 7b7ae5aa396d Added product measure space hoelzl parents: diff changeset  1 theory Product_Measure  38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36649 diff changeset  2 imports Lebesgue_Integration  35833 7b7ae5aa396d Added product measure space hoelzl parents: diff changeset  3 begin  7b7ae5aa396d Added product measure space hoelzl parents: diff changeset  4 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  5 lemma in_sigma[intro, simp]: "A \ sets M \ A \ sets (sigma M)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  6  unfolding sigma_def by (auto intro!: sigma_sets.Basic)  39080 cae59dc0a094 dynkin system hellerar parents: 38705 diff changeset  7 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  8 lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  9  unfolding sigma_def sigma_sets_eq by simp  39082 54dbe0368dc6 changed definition of dynkin; replaces proofs by metis calles hoelzl parents: 39080 diff changeset  10 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  11 lemma vimage_algebra_sigma:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  12  assumes E: "sets E \ Pow (space E)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  13  and f: "f \ space F \ space E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  14  and "\A. A \ sets F \ A \ (\X. f - X \ space F)  sets E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  15  and "\A. A \ sets E \ f - A \ space F \ sets F"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  16  shows "sigma_algebra.vimage_algebra (sigma E) (space F) f = sigma F"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  17 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  18  interpret sigma_algebra "sigma E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  19  using assms by (intro sigma_algebra_sigma) auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  20  have eq: "sets F = (\X. f - X \ space F)  sets E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  21  using assms by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  22  show "vimage_algebra (space F) f = sigma F"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  23  unfolding vimage_algebra_def using assms  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  24  by (simp add: sigma_def eq sigma_sets_vimage)  39094 67da17aced5a measure unique hellerar parents: 39080 diff changeset  25 qed  67da17aced5a measure unique hellerar parents: 39080 diff changeset  26 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  27 lemma times_Int_times: "A \ B \ C \ D = (A \ C) \ (B \ D)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  28  by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  29 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  30 lemma Pair_vimage_times[simp]: "\A B x. Pair x - (A \ B) = (if x \ A then B else {})"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  31  by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  32 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  33 lemma rev_Pair_vimage_times[simp]: "\A B y. (\x. (x, y)) - (A \ B) = (if y \ B then A else {})"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  34  by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  35 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  36 lemma case_prod_distrib: "f (case x of (x, y) \ g x y) = (case x of (x, y) \ f (g x y))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  37  by (cases x) simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  38 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  39 abbreviation  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  40  "Pi\<^isub>E A B \ Pi A B \ extensional A"  39094 67da17aced5a measure unique hellerar parents: 39080 diff changeset  41 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  42 abbreviation  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  43  funcset_extensional :: "['a set, 'b set] => ('a => 'b) set"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  44  (infixr "->\<^isub>E" 60) where  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  45  "A ->\<^isub>E B \ Pi\<^isub>E A (%_. B)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  46 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  47 notation (xsymbols)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  48  funcset_extensional (infixr "\\<^isub>E" 60)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  49 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  50 lemma extensional_empty[simp]: "extensional {} = {\x. undefined}"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  51  by safe (auto simp add: extensional_def fun_eq_iff)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  52 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  53 lemma extensional_insert[intro, simp]:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  54  assumes "a \ extensional (insert i I)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  55  shows "a(i := b) \ extensional (insert i I)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  56  using assms unfolding extensional_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  57 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  58 lemma extensional_Int[simp]:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  59  "extensional I \ extensional I' = extensional (I \ I')"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  60  unfolding extensional_def by auto  38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36649 diff changeset  61 35833 7b7ae5aa396d Added product measure space hoelzl parents: diff changeset  62 definition  40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  63  "merge I x J y = (\i. if i \ I then x i else if i \ J then y i else undefined)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  64 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  65 lemma merge_apply[simp]:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  66  "I \ J = {} \ i \ I \ merge I x J y i = x i"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  67  "I \ J = {} \ i \ J \ merge I x J y i = y i"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  68  "J \ I = {} \ i \ I \ merge I x J y i = x i"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  69  "J \ I = {} \ i \ J \ merge I x J y i = y i"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  70  "i \ I \ i \ J \ merge I x J y i = undefined"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  71  unfolding merge_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  72 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  73 lemma merge_commute:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  74  "I \ J = {} \ merge I x J y = merge J y I x"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  75  by (auto simp: merge_def intro!: ext)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  76 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  77 lemma Pi_cancel_merge_range[simp]:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  78  "I \ J = {} \ x \ Pi I (merge I A J B) \ x \ Pi I A"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  79  "I \ J = {} \ x \ Pi I (merge J B I A) \ x \ Pi I A"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  80  "J \ I = {} \ x \ Pi I (merge I A J B) \ x \ Pi I A"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  81  "J \ I = {} \ x \ Pi I (merge J B I A) \ x \ Pi I A"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  82  by (auto simp: Pi_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  83 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  84 lemma Pi_cancel_merge[simp]:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  85  "I \ J = {} \ merge I x J y \ Pi I B \ x \ Pi I B"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  86  "J \ I = {} \ merge I x J y \ Pi I B \ x \ Pi I B"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  87  "I \ J = {} \ merge I x J y \ Pi J B \ y \ Pi J B"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  88  "J \ I = {} \ merge I x J y \ Pi J B \ y \ Pi J B"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  89  by (auto simp: Pi_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  90 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  91 lemma extensional_merge[simp]: "merge I x J y \ extensional (I \ J)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  92  by (auto simp: extensional_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  93 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  94 lemma restrict_Pi_cancel: "restrict x I \ Pi I A \ x \ Pi I A"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  95  by (auto simp: restrict_def Pi_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  96 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  97 lemma restrict_merge[simp]:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  98  "I \ J = {} \ restrict (merge I x J y) I = restrict x I"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  99  "I \ J = {} \ restrict (merge I x J y) J = restrict y J"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  100  "J \ I = {} \ restrict (merge I x J y) I = restrict x I"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  101  "J \ I = {} \ restrict (merge I x J y) J = restrict y J"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  102  by (auto simp: restrict_def intro!: ext)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  103 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  104 lemma extensional_insert_undefined[intro, simp]:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  105  assumes "a \ extensional (insert i I)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  106  shows "a(i := undefined) \ extensional I"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  107  using assms unfolding extensional_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  108 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  109 lemma extensional_insert_cancel[intro, simp]:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  110  assumes "a \ extensional I"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  111  shows "a \ extensional (insert i I)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  112  using assms unfolding extensional_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  113 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  114 lemma PiE_Int: "(Pi\<^isub>E I A) \ (Pi\<^isub>E I B) = Pi\<^isub>E I (\x. A x \ B x)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  115  by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  116 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  117 lemma Pi_cancel_fupd_range[simp]: "i \ I \ x \ Pi I (B(i := b)) \ x \ Pi I B"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  118  by (auto simp: Pi_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  119 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  120 lemma Pi_split_insert_domain[simp]: "x \ Pi (insert i I) X \ x \ Pi I X \ x i \ X i"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  121  by (auto simp: Pi_def)  39088 ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  122 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  123 lemma Pi_split_domain[simp]: "x \ Pi (I \ J) X \ x \ Pi I X \ x \ Pi J X"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  124  by (auto simp: Pi_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  125 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  126 lemma Pi_cancel_fupd[simp]: "i \ I \ x(i := a) \ Pi I B \ x \ Pi I B"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  127  by (auto simp: Pi_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  128 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  129 section "Binary products"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  130 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  131 definition  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  132  "pair_algebra A B = \ space = space A \ space B,  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  133  sets = {a \ b | a b. a \ sets A \ b \ sets B} \"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  134 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  135 locale pair_sigma_algebra = M1: sigma_algebra M1 + M2: sigma_algebra M2  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  136  for M1 M2  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  137 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  138 abbreviation (in pair_sigma_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  139  "E \ pair_algebra M1 M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  140 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  141 abbreviation (in pair_sigma_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  142  "P \ sigma E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  143 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  144 sublocale pair_sigma_algebra \ sigma_algebra P  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  145  using M1.sets_into_space M2.sets_into_space  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  146  by (force simp: pair_algebra_def intro!: sigma_algebra_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  147 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  148 lemma pair_algebraI[intro, simp]:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  149  "x \ sets A \ y \ sets B \ x \ y \ sets (pair_algebra A B)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  150  by (auto simp add: pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  151 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  152 lemma space_pair_algebra:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  153  "space (pair_algebra A B) = space A \ space B"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  154  by (simp add: pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  155 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  156 lemma pair_algebra_Int_snd:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  157  assumes "sets S1 \ Pow (space S1)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  158  shows "pair_algebra S1 (algebra.restricted_space S2 A) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  159  algebra.restricted_space (pair_algebra S1 S2) (space S1 \ A)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  160  (is "?L = ?R")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  161 proof (intro algebra.equality set_eqI iffI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  162  fix X assume "X \ sets ?L"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  163  then obtain A1 A2 where X: "X = A1 \ (A \ A2)" and "A1 \ sets S1" "A2 \ sets S2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  164  by (auto simp: pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  165  then show "X \ sets ?R" unfolding pair_algebra_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  166  using assms apply simp by (intro image_eqI[of _ _ "A1 \ A2"]) auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  167 next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  168  fix X assume "X \ sets ?R"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  169  then obtain A1 A2 where "X = space S1 \ A \ A1 \ A2" "A1 \ sets S1" "A2 \ sets S2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  170  by (auto simp: pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  171  moreover then have "X = A1 \ (A \ A2)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  172  using assms by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  173  ultimately show "X \ sets ?L"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  174  unfolding pair_algebra_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  175 qed (auto simp add: pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  176 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  177 lemma (in pair_sigma_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  178  shows measurable_fst[intro!, simp]:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  179  "fst \ measurable P M1" (is ?fst)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  180  and measurable_snd[intro!, simp]:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  181  "snd \ measurable P M2" (is ?snd)  39088 ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  182 proof -  ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  183  { fix X assume "X \ sets M1"  ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  184  then have "\X1\sets M1. \X2\sets M2. fst - X \ space M1 \ space M2 = X1 \ X2"  ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  185  apply - apply (rule bexI[of _ X]) apply (rule bexI[of _ "space M2"])  ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  186  using M1.sets_into_space by force+ }  ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  187  moreover  ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  188  { fix X assume "X \ sets M2"  ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  189  then have "\X1\sets M1. \X2\sets M2. snd - X \ space M1 \ space M2 = X1 \ X2"  ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  190  apply - apply (rule bexI[of _ "space M1"]) apply (rule bexI[of _ X])  ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  191  using M2.sets_into_space by force+ }  40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  192  ultimately have "?fst \ ?snd"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  193  by (fastsimp simp: measurable_def sets_sigma space_pair_algebra  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  194  intro!: sigma_sets.Basic)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  195  then show ?fst ?snd by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  196 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  197 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  198 lemma (in pair_sigma_algebra) measurable_pair:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  199  assumes "sigma_algebra M"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  200  shows "f \ measurable M P \  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  201  (fst \ f) \ measurable M M1 \ (snd \ f) \ measurable M M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  202 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  203  interpret M: sigma_algebra M by fact  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  204  from assms show ?thesis  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  205  proof (safe intro!: measurable_comp[where b=P])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  206  assume f: "(fst \ f) \ measurable M M1" and s: "(snd \ f) \ measurable M M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  207  show "f \ measurable M P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  208  proof (rule M.measurable_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  209  show "sets (pair_algebra M1 M2) \ Pow (space E)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  210  unfolding pair_algebra_def using M1.sets_into_space M2.sets_into_space by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  211  show "f \ space M \ space E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  212  using f s by (auto simp: mem_Times_iff measurable_def comp_def space_sigma space_pair_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  213  fix A assume "A \ sets E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  214  then obtain B C where "B \ sets M1" "C \ sets M2" "A = B \ C"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  215  unfolding pair_algebra_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  216  moreover have "(fst \ f) - B \ space M \ sets M"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  217  using f B \ sets M1 unfolding measurable_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  218  moreover have "(snd \ f) - C \ space M \ sets M"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  219  using s C \ sets M2 unfolding measurable_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  220  moreover have "f - A \ space M = ((fst \ f) - B \ space M) \ ((snd \ f) - C \ space M)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  221  unfolding A = B \ C by (auto simp: vimage_Times)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  222  ultimately show "f - A \ space M \ sets M" by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  223  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  224  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  225 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  226 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  227 lemma (in pair_sigma_algebra) measurable_prod_sigma:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  228  assumes "sigma_algebra M"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  229  assumes 1: "(fst \ f) \ measurable M M1" and 2: "(snd \ f) \ measurable M M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  230  shows "f \ measurable M P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  231 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  232  interpret M: sigma_algebra M by fact  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  233  from 1 have fn1: "fst \ f \ space M \ space M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  234  and q1: "\y\sets M1. (fst \ f) - y \ space M \ sets M"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  235  by (auto simp add: measurable_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  236  from 2 have fn2: "snd \ f \ space M \ space M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  237  and q2: "\y\sets M2. (snd \ f) - y \ space M \ sets M"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  238  by (auto simp add: measurable_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  239  show ?thesis  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  240  proof (rule M.measurable_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  241  show "sets E \ Pow (space E)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  242  using M1.space_closed M2.space_closed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  243  by (auto simp add: sigma_algebra_iff pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  244  next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  245  show "f \ space M \ space E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  246  by (simp add: space_pair_algebra) (rule prod_final [OF fn1 fn2])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  247  next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  248  fix z  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  249  assume z: "z \ sets E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  250  thus "f - z \ space M \ sets M"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  251  proof (auto simp add: pair_algebra_def vimage_Times)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  252  fix x y  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  253  assume x: "x \ sets M1" and y: "y \ sets M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  254  have "(fst \ f) - x \ (snd \ f) - y \ space M =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  255  ((fst \ f) - x \ space M) \ ((snd \ f) - y \ space M)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  256  by blast  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  257  also have "... \ sets M" using x y q1 q2  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  258  by blast  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  259  finally show "(fst \ f) - x \ (snd \ f) - y \ space M \ sets M" .  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  260  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  261  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  262 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  263 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  264 lemma pair_algebraE:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  265  assumes "X \ sets (pair_algebra M1 M2)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  266  obtains A B where "X = A \ B" "A \ sets M1" "B \ sets M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  267  using assms unfolding pair_algebra_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  268 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  269 lemma (in pair_sigma_algebra) pair_algebra_swap:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  270  "(\X. ($$x,y). (y,x)) - X \ space M2 \ space M1)  sets E = sets (pair_algebra M2 M1)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  271 proof (safe elim!: pair_algebraE)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  272  fix A B assume "A \ sets M1" "B \ sets M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  273  moreover then have "(\(x, y). (y, x)) - (A \ B) \ space M2 \ space M1 = B \ A"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  274  using M1.sets_into_space M2.sets_into_space by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  275  ultimately show "(\(x, y). (y, x)) - (A \ B) \ space M2 \ space M1 \ sets (pair_algebra M2 M1)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  276  by (auto intro: pair_algebraI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  277 next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  278  fix A B assume "A \ sets M1" "B \ sets M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  279  then show "B \ A \ (\X. (\(x, y). (y, x)) - X \ space M2 \ space M1)  sets E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  280  using M1.sets_into_space M2.sets_into_space  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  281  by (auto intro!: image_eqI[where x="A \ B"] pair_algebraI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  282 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  283 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  284 lemma (in pair_sigma_algebra) sets_pair_sigma_algebra_swap:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  285  assumes Q: "Q \ sets P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  286  shows "(\(x,y). (y, x))  Q \ sets (sigma (pair_algebra M2 M1))" (is "_ \ sets ?Q")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  287 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  288  have *: "(\(x,y). (y, x)) \ space M2 \ space M1 \ (space M1 \ space M2)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  289  "sets (pair_algebra M1 M2) \ Pow (space M1 \ space M2)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  290  using M1.sets_into_space M2.sets_into_space by (auto elim!: pair_algebraE)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  291  from Q sets_into_space show ?thesis  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  292  by (auto intro!: image_eqI[where x=Q]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  293  simp: pair_algebra_swap[symmetric] sets_sigma  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  294  sigma_sets_vimage[OF *] space_pair_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  295 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  296 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  297 lemma (in pair_sigma_algebra) pair_sigma_algebra_swap_measurable:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  298  shows "(\(x,y). (y, x)) \ measurable P (sigma (pair_algebra M2 M1))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  299  (is "?f \ measurable ?P ?Q")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  300  unfolding measurable_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  301 proof (intro CollectI conjI Pi_I ballI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  302  fix x assume "x \ space ?P" then show "(case x of (x, y) \ (y, x)) \ space ?Q"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  303  unfolding pair_algebra_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  304 next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  305  fix A assume "A \ sets ?Q"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  306  interpret Q: pair_sigma_algebra M2 M1 by default  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  307  have "?f - A \ space ?P = (\(x,y). (y, x))  A"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  308  using Q.sets_into_space A \ sets ?Q by (auto simp: pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  309  with Q.sets_pair_sigma_algebra_swap[OF A \ sets ?Q]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  310  show "?f - A \ space ?P \ sets ?P" by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  311 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  312 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  313 lemma (in pair_sigma_algebra) measurable_cut_fst:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  314  assumes "Q \ sets P" shows "Pair x - Q \ sets M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  315 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  316  let ?Q' = "{Q. Q \ space P \ Pair x - Q \ sets M2}"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  317  let ?Q = "\ space = space P, sets = ?Q' \"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  318  interpret Q: sigma_algebra ?Q  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  319  proof qed (auto simp: vimage_UN vimage_Diff space_pair_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  320  have "sets E \ sets ?Q"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  321  using M1.sets_into_space M2.sets_into_space  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  322  by (auto simp: pair_algebra_def space_pair_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  323  then have "sets P \ sets ?Q"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  324  by (subst pair_algebra_def, intro Q.sets_sigma_subset)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  325  (simp_all add: pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  326  with assms show ?thesis by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  327 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  328 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  329 lemma (in pair_sigma_algebra) measurable_cut_snd:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  330  assumes Q: "Q \ sets P" shows "(\x. (x, y)) - Q \ sets M1" (is "?cut Q \ sets M1")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  331 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  332  interpret Q: pair_sigma_algebra M2 M1 by default  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  333  have "Pair y - (\(x, y). (y, x))  Q = (\x. (x, y)) - Q" by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  334  with Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  335  show ?thesis by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  336 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  337 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  338 lemma (in pair_sigma_algebra) measurable_pair_image_snd:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  339  assumes m: "f \ measurable P M" and "x \ space M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  340  shows "(\y. f (x, y)) \ measurable M2 M"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  341  unfolding measurable_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  342 proof (intro CollectI conjI Pi_I ballI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  343  fix y assume "y \ space M2" with f \ measurable P M x \ space M1  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  344  show "f (x, y) \ space M" unfolding measurable_def pair_algebra_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  345 next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  346  fix A assume "A \ sets M"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  347  then have "Pair x - (f - A \ space P) \ sets M2" (is "?C \ _")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  348  using f \ measurable P M  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  349  by (intro measurable_cut_fst) (auto simp: measurable_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  350  also have "?C = (\y. f (x, y)) - A \ space M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  351  using x \ space M1 by (auto simp: pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  352  finally show "(\y. f (x, y)) - A \ space M2 \ sets M2" .  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  353 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  354 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  355 lemma (in pair_sigma_algebra) measurable_pair_image_fst:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  356  assumes m: "f \ measurable P M" and "y \ space M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  357  shows "(\x. f (x, y)) \ measurable M1 M"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  358 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  359  interpret Q: pair_sigma_algebra M2 M1 by default  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  360  from Q.measurable_pair_image_snd[OF measurable_comp y \ space M2,  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  361  OF Q.pair_sigma_algebra_swap_measurable m]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  362  show ?thesis by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  363 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  364 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  365 lemma (in pair_sigma_algebra) Int_stable_pair_algebra: "Int_stable E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  366  unfolding Int_stable_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  367 proof (intro ballI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  368  fix A B assume "A \ sets E" "B \ sets E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  369  then obtain A1 A2 B1 B2 where "A = A1 \ A2" "B = B1 \ B2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  370  "A1 \ sets M1" "A2 \ sets M2" "B1 \ sets M1" "B2 \ sets M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  371  unfolding pair_algebra_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  372  then show "A \ B \ sets E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  373  by (auto simp add: times_Int_times pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  374 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  375 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  376 lemma finite_measure_cut_measurable:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  377  fixes M1 :: "'a algebra" and M2 :: "'b algebra"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  378  assumes "sigma_finite_measure M1 \1" "finite_measure M2 \2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  379  assumes "Q \ sets (sigma (pair_algebra M1 M2))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  380  shows "(\x. \2 (Pair x - Q)) \ borel_measurable M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  381  (is "?s Q \ _")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  382 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  383  interpret M1: sigma_finite_measure M1 \1 by fact  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  384  interpret M2: finite_measure M2 \2 by fact  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  385  interpret pair_sigma_algebra M1 M2 by default  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  386  have [intro]: "sigma_algebra M1" by fact  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  387  have [intro]: "sigma_algebra M2" by fact  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  388  let ?D = "\ space = space P, sets = {A\sets P. ?s A \ borel_measurable M1} \"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  389  note space_pair_algebra[simp]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  390  interpret dynkin_system ?D  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  391  proof (intro dynkin_systemI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  392  fix A assume "A \ sets ?D" then show "A \ space ?D"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  393  using sets_into_space by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  394  next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  395  from top show "space ?D \ sets ?D"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  396  by (auto simp add: if_distrib intro!: M1.measurable_If)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  397  next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  398  fix A assume "A \ sets ?D"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  399  with sets_into_space have "\x. \2 (Pair x - (space M1 \ space M2 - A)) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  400  (if x \ space M1 then \2 (space M2) - ?s A x else 0)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  401  by (auto intro!: M2.finite_measure_compl measurable_cut_fst  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  402  simp: vimage_Diff)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  403  with A \ sets ?D top show "space ?D - A \ sets ?D"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  404  by (auto intro!: Diff M1.measurable_If M1.borel_measurable_pinfreal_diff)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  405  next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  406  fix F :: "nat \ ('a\'b) set" assume "disjoint_family F" "range F \ sets ?D"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  407  moreover then have "\x. \2 (\i. Pair x - F i) = (\\<^isub>\ i. ?s (F i) x)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  408  by (intro M2.measure_countably_additive[symmetric])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  409  (auto intro!: measurable_cut_fst simp: disjoint_family_on_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  410  ultimately show "(\i. F i) \ sets ?D"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  411  by (auto simp: vimage_UN intro!: M1.borel_measurable_psuminf)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  412  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  413  have "P = ?D"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  414  proof (intro dynkin_lemma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  415  show "Int_stable E" by (rule Int_stable_pair_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  416  from M1.sets_into_space have "\A. A \ sets M1 \ {x \ space M1. x \ A} = A"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  417  by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  418  then show "sets E \ sets ?D"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  419  by (auto simp: pair_algebra_def sets_sigma if_distrib  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  420  intro: sigma_sets.Basic intro!: M1.measurable_If)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  421  qed auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  422  with Q \ sets P have "Q \ sets ?D" by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  423  then show "?s Q \ borel_measurable M1" by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  424 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  425 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  426 subsection {* Binary products of \sigma-finite measure spaces *}  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  427 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  428 locale pair_sigma_finite = M1: sigma_finite_measure M1 \1 + M2: sigma_finite_measure M2 \2  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  429  for M1 \1 M2 \2  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  430 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  431 sublocale pair_sigma_finite \ pair_sigma_algebra M1 M2  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  432  by default  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  433 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  434 lemma (in pair_sigma_finite) measure_cut_measurable_fst:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  435  assumes "Q \ sets P" shows "(\x. \2 (Pair x - Q)) \ borel_measurable M1" (is "?s Q \ _")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  436 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  437  have [intro]: "sigma_algebra M1" and [intro]: "sigma_algebra M2" by default+  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  438  have M1: "sigma_finite_measure M1 \1" by default  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  439 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  440  from M2.disjoint_sigma_finite guess F .. note F = this  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  441  let "?C x i" = "F i \ Pair x - Q"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  442  { fix i  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  443  let ?R = "M2.restricted_space (F i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  444  have [simp]: "space M1 \ F i \ space M1 \ space M2 = space M1 \ F i"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  445  using F M2.sets_into_space by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  446  have "(\x. \2 (Pair x - (space M1 \ F i \ Q))) \ borel_measurable M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  447  proof (intro finite_measure_cut_measurable[OF M1])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  448  show "finite_measure (M2.restricted_space (F i)) \2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  449  using F by (intro M2.restricted_to_finite_measure) auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  450  have "space M1 \ F i \ sets P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  451  using M1.top F by blast  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  452  from sigma_sets_Int[symmetric,  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  453  OF this[unfolded pair_sigma_algebra_def sets_sigma]]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  454  show "(space M1 \ F i) \ Q \ sets (sigma (pair_algebra M1 ?R))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  455  using Q \ sets P  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  456  using pair_algebra_Int_snd[OF M1.space_closed, of "F i" M2]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  457  by (auto simp: pair_algebra_def sets_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  458  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  459  moreover have "\x. Pair x - (space M1 \ F i \ Q) = ?C x i"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  460  using Q \ sets P sets_into_space by (auto simp: space_pair_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  461  ultimately have "(\x. \2 (?C x i)) \ borel_measurable M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  462  by simp }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  463  moreover  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  464  { fix x  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  465  have "(\\<^isub>\i. \2 (?C x i)) = \2 (\i. ?C x i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  466  proof (intro M2.measure_countably_additive)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  467  show "range (?C x) \ sets M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  468  using F Q \ sets P by (auto intro!: M2.Int measurable_cut_fst)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  469  have "disjoint_family F" using F by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  470  show "disjoint_family (?C x)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  471  by (rule disjoint_family_on_bisimulation[OF disjoint_family F]) auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  472  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  473  also have "(\i. ?C x i) = Pair x - Q"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  474  using F sets_into_space Q \ sets P  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  475  by (auto simp: space_pair_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  476  finally have "\2 (Pair x - Q) = (\\<^isub>\i. \2 (?C x i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  477  by simp }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  478  ultimately show ?thesis  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  479  by (auto intro!: M1.borel_measurable_psuminf)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  480 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  481 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  482 lemma (in pair_sigma_finite) measure_cut_measurable_snd:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  483  assumes "Q \ sets P" shows "(\y. \1 ((\x. (x, y)) - Q)) \ borel_measurable M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  484 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  485  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  486  have [simp]: "\y. (Pair y - (\(x, y). (y, x))  Q) = (\x. (x, y)) - Q"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  487  by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  488  note sets_pair_sigma_algebra_swap[OF assms]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  489  from Q.measure_cut_measurable_fst[OF this]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  490  show ?thesis by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  491 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  492 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  493 lemma (in pair_sigma_algebra) pair_sigma_algebra_measurable:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  494  assumes "f \ measurable P M"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  495  shows "(\(x,y). f (y, x)) \ measurable (sigma (pair_algebra M2 M1)) M"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  496 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  497  interpret Q: pair_sigma_algebra M2 M1 by default  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  498  have *: "(\(x,y). f (y, x)) = f \ (\(x,y). (y, x))" by (simp add: fun_eq_iff)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  499  show ?thesis  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  500  using Q.pair_sigma_algebra_swap_measurable assms  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  501  unfolding * by (rule measurable_comp)  39088 ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  502 qed  ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  503 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  504 lemma (in pair_sigma_algebra) pair_sigma_algebra_swap:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  505  "sigma (pair_algebra M2 M1) = (vimage_algebra (space M2 \ space M1) (\(x, y). (y, x)))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  506  unfolding vimage_algebra_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  507  apply (simp add: sets_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  508  apply (subst sigma_sets_vimage[symmetric])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  509  apply (fastsimp simp: pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  510  using M1.sets_into_space M2.sets_into_space apply (fastsimp simp: pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  511 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  512  have "(\X. (\(x, y). (y, x)) - X \ space M2 \ space M1)  sets E  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  513  = sets (pair_algebra M2 M1)" (is "?S = _")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  514  by (rule pair_algebra_swap)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  515  then show "sigma (pair_algebra M2 M1) = \space = space M2 \ space M1,  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  516  sets = sigma_sets (space M2 \ space M1) ?S\"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  517  by (simp add: pair_algebra_def sigma_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  518 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  519 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  520 definition (in pair_sigma_finite)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  521  "pair_measure A = M1.positive_integral (\x.  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  522  M2.positive_integral (\y. indicator A (x, y)))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  523 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  524 lemma (in pair_sigma_finite) pair_measure_alt:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  525  assumes "A \ sets P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  526  shows "pair_measure A = M1.positive_integral (\x. \2 (Pair x - A))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  527  unfolding pair_measure_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  528 proof (rule M1.positive_integral_cong)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  529  fix x assume "x \ space M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  530  have *: "\y. indicator A (x, y) = (indicator (Pair x - A) y :: pinfreal)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  531  unfolding indicator_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  532  show "M2.positive_integral (\y. indicator A (x, y)) = \2 (Pair x - A)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  533  unfolding *  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  534  apply (subst M2.positive_integral_indicator)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  535  apply (rule measurable_cut_fst[OF assms])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  536  by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  537 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  538 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  539 lemma (in pair_sigma_finite) pair_measure_times:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  540  assumes A: "A \ sets M1" and "B \ sets M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  541  shows "pair_measure (A \ B) = \1 A * \2 B"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  542 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  543  from assms have "pair_measure (A \ B) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  544  M1.positive_integral (\x. \2 B * indicator A x)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  545  by (auto intro!: M1.positive_integral_cong simp: pair_measure_alt)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  546  with assms show ?thesis  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  547  by (simp add: M1.positive_integral_cmult_indicator ac_simps)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  548 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  549 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  550 lemma (in pair_sigma_finite) sigma_finite_up_in_pair_algebra:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  551  "\F::nat \ ('a \ 'b) set. range F \ sets E \ F \ space E \  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  552  (\i. pair_measure (F i) \$$"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  553 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  554  obtain F1 :: "nat \ 'a set" and F2 :: "nat \ 'b set" where  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  555  F1: "range F1 \ sets M1" "F1 \ space M1" "\i. \1 (F1 i) \ \" and  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  556  F2: "range F2 \ sets M2" "F2 \ space M2" "\i. \2 (F2 i) \ \"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  557  using M1.sigma_finite_up M2.sigma_finite_up by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  558  then have space: "space M1 = (\i. F1 i)" "space M2 = (\i. F2 i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  559  unfolding isoton_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  560  let ?F = "\i. F1 i \ F2 i"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  561  show ?thesis unfolding isoton_def space_pair_algebra  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  562  proof (intro exI[of _ ?F] conjI allI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  563  show "range ?F \ sets E" using F1 F2  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  564  by (fastsimp intro!: pair_algebraI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  565  next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  566  have "space M1 \ space M2 \ (\i. ?F i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  567  proof (intro subsetI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  568  fix x assume "x \ space M1 \ space M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  569  then obtain i j where "fst x \ F1 i" "snd x \ F2 j"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  570  by (auto simp: space)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  571  then have "fst x \ F1 (max i j)" "snd x \ F2 (max j i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  572  using F1 \ space M1 F2 \ space M2  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  573  by (auto simp: max_def dest: isoton_mono_le)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  574  then have "(fst x, snd x) \ F1 (max i j) \ F2 (max i j)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  575  by (intro SigmaI) (auto simp add: min_max.sup_commute)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  576  then show "x \ (\i. ?F i)" by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  577  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  578  then show "(\i. ?F i) = space M1 \ space M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  579  using space by (auto simp: space)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  580  next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  581  fix i show "F1 i \ F2 i \ F1 (Suc i) \ F2 (Suc i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  582  using F1 \ space M1 F2 \ space M2 unfolding isoton_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  583  by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  584  next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  585  fix i  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  586  from F1 F2 have "F1 i \ sets M1" "F2 i \ sets M2" by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  587  with F1 F2 show "pair_measure (F1 i \ F2 i) \ \"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  588  by (simp add: pair_measure_times)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  589  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  590 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  591 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  592 sublocale pair_sigma_finite \ sigma_finite_measure P pair_measure  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  593 proof  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  594  show "pair_measure {} = 0"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  595  unfolding pair_measure_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  596 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  597  show "countably_additive P pair_measure"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  598  unfolding countably_additive_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  599  proof (intro allI impI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  600  fix F :: "nat \ ('a \ 'b) set"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  601  assume F: "range F \ sets P" "disjoint_family F"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  602  from F have *: "\i. F i \ sets P" "(\i. F i) \ sets P" by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  603  moreover from F have "\i. (\x. \2 (Pair x - F i)) \ borel_measurable M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  604  by (intro measure_cut_measurable_fst) auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  605  moreover have "\x. disjoint_family (\i. Pair x - F i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  606  by (intro disjoint_family_on_bisimulation[OF F(2)]) auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  607  moreover have "\x. x \ space M1 \ range (\i. Pair x - F i) \ sets M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  608  using F by (auto intro!: measurable_cut_fst)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  609  ultimately show "(\\<^isub>\n. pair_measure (F n)) = pair_measure (\i. F i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  610  by (simp add: pair_measure_alt vimage_UN M1.positive_integral_psuminf[symmetric]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  611  M2.measure_countably_additive  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  612  cong: M1.positive_integral_cong)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  613  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  614 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  615  from sigma_finite_up_in_pair_algebra guess F :: "nat \ ('a \ 'c) set" .. note F = this  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  616  show "\F::nat \ ('a \ 'b) set. range F \ sets P \ (\i. F i) = space P \ (\i. pair_measure (F i) \ \)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  617  proof (rule exI[of _ F], intro conjI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  618  show "range F \ sets P" using F by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  619  show "(\i. F i) = space P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  620  using F by (auto simp: space_pair_algebra isoton_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  621  show "\i. pair_measure (F i) \ \" using F by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  622  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  623 qed  39088 ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  624 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  625 lemma (in pair_sigma_finite) pair_measure_alt2:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  626  assumes "A \ sets P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  627  shows "pair_measure A = M2.positive_integral (\y. \1 ((\x. (x, y)) - A))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  628  (is "_ = ?\ A")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  629 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  630  from sigma_finite_up_in_pair_algebra guess F :: "nat \ ('a \ 'c) set" .. note F = this  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  631  show ?thesis  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  632  proof (rule measure_unique_Int_stable[where \="?\", OF Int_stable_pair_algebra],  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  633  simp_all add: pair_sigma_algebra_def[symmetric])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  634  show "range F \ sets E" "F \ space E" "\i. pair_measure (F i) \ \"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  635  using F by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  636  show "measure_space P pair_measure" by default  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  637  next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  638  show "measure_space P ?\"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  639  proof  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  640  show "?\ {} = 0" by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  641  show "countably_additive P ?\"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  642  unfolding countably_additive_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  643  proof (intro allI impI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  644  fix F :: "nat \ ('a \ 'b) set"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  645  assume F: "range F \ sets P" "disjoint_family F"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  646  from F have *: "\i. F i \ sets P" "(\i. F i) \ sets P" by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  647  moreover from F have "\i. (\y. \1 ((\x. (x, y)) - F i)) \ borel_measurable M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  648  by (intro measure_cut_measurable_snd) auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  649  moreover have "\y. disjoint_family (\i. (\x. (x, y)) - F i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  650  by (intro disjoint_family_on_bisimulation[OF F(2)]) auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  651  moreover have "\y. y \ space M2 \ range (\i. (\x. (x, y)) - F i) \ sets M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  652  using F by (auto intro!: measurable_cut_snd)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  653  ultimately show "(\\<^isub>\n. ?\ (F n)) = ?\ (\i. F i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  654  by (simp add: vimage_UN M2.positive_integral_psuminf[symmetric]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  655  M1.measure_countably_additive  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  656  cong: M2.positive_integral_cong)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  657  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  658  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  659  next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  660  fix X assume "X \ sets E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  661  then obtain A B where X: "X = A \ B" and AB: "A \ sets M1" "B \ sets M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  662  unfolding pair_algebra_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  663  show "pair_measure X = ?\ X"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  664  proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  665  from AB have "?\ (A \ B) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  666  M2.positive_integral (\y. \1 A * indicator B y)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  667  by (auto intro!: M2.positive_integral_cong)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  668  with AB show ?thesis  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  669  unfolding pair_measure_times[OF AB] X  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  670  by (simp add: M2.positive_integral_cmult_indicator ac_simps)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  671  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  672  qed fact  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  673 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  674 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  675 section "Fubinis theorem"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  676 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  677 lemma (in pair_sigma_finite) simple_function_cut:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  678  assumes f: "simple_function f"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  679  shows "(\x. M2.positive_integral (\ y. f (x, y))) \ borel_measurable M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  680  and "M1.positive_integral (\x. M2.positive_integral (\y. f (x, y)))  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  681  = positive_integral f"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  682 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  683  have f_borel: "f \ borel_measurable P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  684  using f by (rule borel_measurable_simple_function)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  685  let "?F z" = "f - {z} \ space P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  686  let "?F' x z" = "Pair x - ?F z"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  687  { fix x assume "x \ space M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  688  have [simp]: "\z y. indicator (?F z) (x, y) = indicator (?F' x z) y"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  689  by (auto simp: indicator_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  690  have "\y. y \ space M2 \ (x, y) \ space P" using x \ space M1  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  691  by (simp add: space_pair_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  692  moreover have "\x z. ?F' x z \ sets M2" using f_borel  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  693  by (intro borel_measurable_vimage measurable_cut_fst)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  694  ultimately have "M2.simple_function (\ y. f (x, y))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  695  apply (rule_tac M2.simple_function_cong[THEN iffD2, OF _])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  696  apply (rule simple_function_indicator_representation[OF f])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  697  using x \ space M1 by (auto simp del: space_sigma) }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  698  note M2_sf = this  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  699  { fix x assume x: "x \ space M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  700  then have "M2.positive_integral (\ y. f (x, y)) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  701  (\z\f  space P. z * \2 (?F' x z))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  702  unfolding M2.positive_integral_eq_simple_integral[OF M2_sf[OF x]]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  703  unfolding M2.simple_integral_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  704  proof (safe intro!: setsum_mono_zero_cong_left)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  705  from f show "finite (f  space P)" by (rule simple_functionD)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  706  next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  707  fix y assume "y \ space M2" then show "f (x, y) \ f  space P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  708  using x \ space M1 by (auto simp: space_pair_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  709  next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  710  fix x' y assume "(x', y) \ space P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  711  "f (x', y) \ (\y. f (x, y))  space M2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  712  then have *: "?F' x (f (x', y)) = {}"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  713  by (force simp: space_pair_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  714  show "f (x', y) * \2 (?F' x (f (x', y))) = 0"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  715  unfolding * by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  716  qed (simp add: vimage_compose[symmetric] comp_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  717  space_pair_algebra) }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  718  note eq = this  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  719  moreover have "\z. ?F z \ sets P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  720  by (auto intro!: f_borel borel_measurable_vimage simp del: space_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  721  moreover then have "\z. (\x. \2 (?F' x z)) \ borel_measurable M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  722  by (auto intro!: measure_cut_measurable_fst simp del: vimage_Int)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  723  ultimately  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  724  show "(\ x. M2.positive_integral (\ y. f (x, y))) \ borel_measurable M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  725  and "M1.positive_integral (\x. M2.positive_integral (\y. f (x, y)))  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  726  = positive_integral f"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  727  by (auto simp del: vimage_Int cong: measurable_cong  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  728  intro!: M1.borel_measurable_pinfreal_setsum  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  729  simp add: M1.positive_integral_setsum simple_integral_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  730  M1.positive_integral_cmult  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  731  M1.positive_integral_cong[OF eq]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  732  positive_integral_eq_simple_integral[OF f]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  733  pair_measure_alt[symmetric])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  734 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  735 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  736 lemma (in pair_sigma_finite) positive_integral_fst_measurable:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  737  assumes f: "f \ borel_measurable P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  738  shows "(\ x. M2.positive_integral (\ y. f (x, y))) \ borel_measurable M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  739  (is "?C f \ borel_measurable M1")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  740  and "M1.positive_integral (\ x. M2.positive_integral (\ y. f (x, y))) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  741  positive_integral f"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  742 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  743  from borel_measurable_implies_simple_function_sequence[OF f]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  744  obtain F where F: "\i. simple_function (F i)" "F \ f" by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  745  then have F_borel: "\i. F i \ borel_measurable P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  746  and F_mono: "\i x. F i x \ F (Suc i) x"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  747  and F_SUPR: "\x. (SUP i. F i x) = f x"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  748  unfolding isoton_def le_fun_def SUPR_fun_expand  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  749  by (auto intro: borel_measurable_simple_function)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  750  note sf = simple_function_cut[OF F(1)]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  751  then have "(SUP i. ?C (F i)) \ borel_measurable M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  752  using F(1) by (auto intro!: M1.borel_measurable_SUP)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  753  moreover  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  754  { fix x assume "x \ space M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  755  have isotone: "(\ i y. F i (x, y)) \ (\y. f (x, y))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  756  using F \ f unfolding isoton_fun_expand  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  757  by (auto simp: isoton_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  758  note measurable_pair_image_snd[OF F_borelx \ space M1]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  759  from M2.positive_integral_isoton[OF isotone this]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  760  have "(SUP i. ?C (F i) x) = ?C f x"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  761  by (simp add: isoton_def) }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  762  note SUPR_C = this  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  763  ultimately show "?C f \ borel_measurable M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  764  unfolding SUPR_fun_expand by (simp cong: measurable_cong)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  765  have "positive_integral (\x. SUP i. F i x) = (SUP i. positive_integral (F i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  766  using F_borel F_mono  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  767  by (auto intro!: positive_integral_monotone_convergence_SUP[symmetric])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  768  also have "(SUP i. positive_integral (F i)) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  769  (SUP i. M1.positive_integral (\x. M2.positive_integral (\y. F i (x, y))))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  770  unfolding sf(2) by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  771  also have "\ = M1.positive_integral (\x. SUP i. M2.positive_integral (\y. F i (x, y)))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  772  by (auto intro!: M1.positive_integral_monotone_convergence_SUP[OF _ sf(1)]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  773  M2.positive_integral_mono F_mono)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  774  also have "\ = M1.positive_integral (\x. M2.positive_integral (\y. SUP i. F i (x, y)))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  775  using F_borel F_mono  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  776  by (auto intro!: M2.positive_integral_monotone_convergence_SUP  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  777  M1.positive_integral_cong measurable_pair_image_snd)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  778  finally show "M1.positive_integral (\ x. M2.positive_integral (\ y. f (x, y))) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  779  positive_integral f"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  780  unfolding F_SUPR by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  781 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  782 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  783 lemma (in pair_sigma_finite) positive_integral_snd_measurable:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  784  assumes f: "f \ borel_measurable P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  785  shows "M2.positive_integral (\y. M1.positive_integral (\x. f (x, y))) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  786  positive_integral f"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  787 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  788  interpret Q: pair_sigma_finite M2 \2 M1 \1 by default  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  789 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  790  have s: "\x y. (case (x, y) of (x, y) \ f (y, x)) = f (y, x)" by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  791  have t: "(\x. f (case x of (x, y) \ (y, x))) = (\(x, y). f (y, x))" by (auto simp: fun_eq_iff)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  792 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  793  have bij: "bij_betw (\(x, y). (y, x)) (space M2 \ space M1) (space P)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  794  by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  795 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  796  note pair_sigma_algebra_measurable[OF f]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  797  from Q.positive_integral_fst_measurable[OF this]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  798  have "M2.positive_integral (\y. M1.positive_integral (\x. f (x, y))) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  799  Q.positive_integral (\(x, y). f (y, x))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  800  by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  801  also have "\ = positive_integral f"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  802  unfolding positive_integral_vimage[OF bij, of f] t  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  803  unfolding pair_sigma_algebra_swap[symmetric]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  804  proof (rule Q.positive_integral_cong_measure[symmetric])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  805  fix A assume "A \ sets Q.P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  806  from this Q.sets_pair_sigma_algebra_swap[OF this]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  807  show "pair_measure ((\(x, y). (y, x))  A) = Q.pair_measure A"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  808  by (auto intro!: M1.positive_integral_cong arg_cong[where f=\2]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  809  simp: pair_measure_alt Q.pair_measure_alt2)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  810  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  811  finally show ?thesis .  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  812 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  813 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  814 lemma (in pair_sigma_finite) Fubini:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  815  assumes f: "f \ borel_measurable P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  816  shows "M2.positive_integral (\y. M1.positive_integral (\x. f (x, y))) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  817  M1.positive_integral (\x. M2.positive_integral (\y. f (x, y)))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  818  unfolding positive_integral_snd_measurable[OF assms]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  819  unfolding positive_integral_fst_measurable[OF assms] ..  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  820 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  821 lemma (in pair_sigma_finite) AE_pair:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  822  assumes "almost_everywhere (\x. Q x)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  823  shows "M1.almost_everywhere (\x. M2.almost_everywhere (\y. Q (x, y)))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  824 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  825  obtain N where N: "N \ sets P" "pair_measure N = 0" "{x\space P. \ Q x} \ N"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  826  using assms unfolding almost_everywhere_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  827  show ?thesis  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  828  proof (rule M1.AE_I)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  829  from N measure_cut_measurable_fst[OF N \ sets P]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  830  show "\1 {x\space M1. \2 (Pair x - N) \ 0} = 0"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  831  by (simp add: M1.positive_integral_0_iff pair_measure_alt vimage_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  832  show "{x \ space M1. \2 (Pair x - N) \ 0} \ sets M1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  833  by (intro M1.borel_measurable_pinfreal_neq_const measure_cut_measurable_fst N)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  834  { fix x assume "x \ space M1" "\2 (Pair x - N) = 0"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  835  have "M2.almost_everywhere (\y. Q (x, y))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  836  proof (rule M2.AE_I)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  837  show "\2 (Pair x - N) = 0" by fact  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  838  show "Pair x - N \ sets M2" by (intro measurable_cut_fst N)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  839  show "{y \ space M2. \ Q (x, y)} \ Pair x - N"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  840  using N x \ space M1 unfolding space_sigma space_pair_algebra by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  841  qed }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  842  then show "{x \ space M1. \ M2.almost_everywhere (\y. Q (x, y))} \ {x \ space M1. \2 (Pair x - N) \ 0}"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  843  by auto  39088 ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  844  qed  ca17017c10e6 Measurable on product space is equiv. to measurable components hoelzl parents: 39082 diff changeset  845 qed  35833 7b7ae5aa396d Added product measure space hoelzl parents: diff changeset  846 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  847 section "Finite product spaces"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  848 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  849 section "Products"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  850 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  851 locale product_sigma_algebra =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  852  fixes M :: "'i \ 'a algebra"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  853  assumes sigma_algebras: "\i. sigma_algebra (M i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  854 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  855 locale finite_product_sigma_algebra = product_sigma_algebra M for M :: "'i \ 'a algebra" +  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  856  fixes I :: "'i set"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  857  assumes finite_index: "finite I"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  858 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  859 syntax  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  860  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PIE _:_./ _)" 10)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  861 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  862 syntax (xsymbols)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  863  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<^isub>E _\_./ _)" 10)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  864 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  865 syntax (HTML output)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  866  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<^isub>E _\_./ _)" 10)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  867 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  868 translations  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  869  "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  870 35833 7b7ae5aa396d Added product measure space hoelzl parents: diff changeset  871 definition  40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  872  "product_algebra M I = \ space = (\\<^isub>E i\I. space (M i)), sets = Pi\<^isub>E I  (\ i \ I. sets (M i)) \"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  873 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  874 abbreviation (in finite_product_sigma_algebra) "G \ product_algebra M I"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  875 abbreviation (in finite_product_sigma_algebra) "P \ sigma G"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  876 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  877 sublocale product_sigma_algebra \ M: sigma_algebra "M i" for i by (rule sigma_algebras)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  878 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  879 lemma (in finite_product_sigma_algebra) product_algebra_into_space:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  880  "sets G \ Pow (space G)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  881  using M.sets_into_space unfolding product_algebra_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  882  by auto blast  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  883 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  884 sublocale finite_product_sigma_algebra \ sigma_algebra P  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  885  using product_algebra_into_space by (rule sigma_algebra_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  886 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  887 lemma space_product_algebra[simp]:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  888  "space (product_algebra M I) = Pi\<^isub>E I (\i. space (M i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  889  unfolding product_algebra_def by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  890 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  891 lemma (in finite_product_sigma_algebra) P_empty:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  892  "I = {} \ P = \ space = {\k. undefined}, sets = { {}, {\k. undefined} }\"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  893  unfolding product_algebra_def by (simp add: sigma_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  894 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  895 lemma (in finite_product_sigma_algebra) in_P[simp, intro]:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  896  "\ \i. i \ I \ A i \ sets (M i) \ \ Pi\<^isub>E I A \ sets P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  897  by (auto simp: product_algebra_def sets_sigma intro!: sigma_sets.Basic)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  898 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  899 lemma bij_betw_prod_fold:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  900  assumes "i \ I"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  901  shows "bij_betw (\x. (x(i:=undefined), x i)) (\\<^isub>E j\insert i I. space (M j)) ((\\<^isub>E j\I. space (M j)) \ space (M i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  902  (is "bij_betw ?f ?P ?F")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  903  using i \ I  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  904 proof (unfold bij_betw_def, intro conjI set_eqI iffI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  905  show "inj_on ?f ?P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  906  proof (safe intro!: inj_onI ext)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  907  fix a b x assume "a(i:=undefined) = b(i:=undefined)" "a i = b i"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  908  then show "a x = b x"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  909  by (cases "x = i") (auto simp: fun_eq_iff split: split_if_asm)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  910  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  911 next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  912  fix X assume *: "X \ ?F" show "X \ ?f  ?P"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  913  proof (cases X)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  914  case (Pair a b) with * i \ I show ?thesis  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  915  by (auto intro!: image_eqI[where x="a (i := b)"] ext simp: extensional_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  916  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  917 qed auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  918 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  919 section "Generating set generates also product algebra"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  920 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  921 lemma pair_sigma_algebra_sigma:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  922  assumes 1: "S1 \ (space E1)" "range S1 \ sets E1" and E1: "sets E1 \ Pow (space E1)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  923  assumes 2: "S2 \ (space E2)" "range S2 \ sets E2" and E2: "sets E2 \ Pow (space E2)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  924  shows "sigma (pair_algebra (sigma E1) (sigma E2)) = sigma (pair_algebra E1 E2)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  925  (is "?S = ?E")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  926 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  927  interpret M1: sigma_algebra "sigma E1" using E1 by (rule sigma_algebra_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  928  interpret M2: sigma_algebra "sigma E2" using E2 by (rule sigma_algebra_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  929  have P: "sets (pair_algebra E1 E2) \ Pow (space E1 \ space E2)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  930  using E1 E2 by (auto simp add: pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  931  interpret E: sigma_algebra ?E unfolding pair_algebra_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  932  using E1 E2 by (intro sigma_algebra_sigma) auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  933 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  934  { fix A assume "A \ sets E1"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  935  then have "fst - A \ space ?E = A \ (\i. S2 i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  936  using E1 2 unfolding isoton_def pair_algebra_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  937  also have "\ = (\i. A \ S2 i)" by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  938  also have "\ \ sets ?E" unfolding pair_algebra_def sets_sigma  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  939  using 2 A \ sets E1  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  940  by (intro sigma_sets.Union)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  941  (auto simp: image_subset_iff intro!: sigma_sets.Basic)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  942  finally have "fst - A \ space ?E \ sets ?E" . }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  943  moreover  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  944  { fix B assume "B \ sets E2"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  945  then have "snd - B \ space ?E = (\i. S1 i) \ B"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  946  using E2 1 unfolding isoton_def pair_algebra_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  947  also have "\ = (\i. S1 i \ B)" by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  948  also have "\ \ sets ?E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  949  using 1 B \ sets E2 unfolding pair_algebra_def sets_sigma  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  950  by (intro sigma_sets.Union)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  951  (auto simp: image_subset_iff intro!: sigma_sets.Basic)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  952  finally have "snd - B \ space ?E \ sets ?E" . }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  953  ultimately have proj:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  954  "fst \ measurable ?E (sigma E1) \ snd \ measurable ?E (sigma E2)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  955  using E1 E2 by (subst (1 2) E.measurable_iff_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  956  (auto simp: pair_algebra_def sets_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  957 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  958  { fix A B assume A: "A \ sets (sigma E1)" and B: "B \ sets (sigma E2)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  959  with proj have "fst - A \ space ?E \ sets ?E" "snd - B \ space ?E \ sets ?E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  960  unfolding measurable_def by simp_all  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  961  moreover have "A \ B = (fst - A \ space ?E) \ (snd - B \ space ?E)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  962  using A B M1.sets_into_space M2.sets_into_space  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  963  by (auto simp: pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  964  ultimately have "A \ B \ sets ?E" by auto }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  965  then have "sigma_sets (space ?E) (sets (pair_algebra (sigma E1) (sigma E2))) \ sets ?E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  966  by (intro E.sigma_sets_subset) (auto simp add: pair_algebra_def sets_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  967  then have subset: "sets ?S \ sets ?E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  968  by (simp add: sets_sigma pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  969 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  970  have "sets ?S = sets ?E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  971  proof (intro set_eqI iffI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  972  fix A assume "A \ sets ?E" then show "A \ sets ?S"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  973  unfolding sets_sigma  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  974  proof induct  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  975  case (Basic A) then show ?case  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  976  by (auto simp: pair_algebra_def sets_sigma intro: sigma_sets.Basic)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  977  qed (auto intro: sigma_sets.intros simp: pair_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  978  next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  979  fix A assume "A \ sets ?S" then show "A \ sets ?E" using subset by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  980  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  981  then show ?thesis  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  982  by (simp add: pair_algebra_def sigma_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  983 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  984 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  985 lemma Pi_fupd_iff: "i \ I \ f \ Pi I (B(i := A)) \ f \ Pi (I - {i}) B \ f i \ A"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  986  apply auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  987  apply (drule_tac x=x in Pi_mem)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  988  apply (simp_all split: split_if_asm)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  989  apply (drule_tac x=i in Pi_mem)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  990  apply (auto dest!: Pi_mem)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  991  done  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  992 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  993 lemma Pi_UN:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  994  fixes A :: "nat \ 'i \ 'a set"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  995  assumes "finite I" and mono: "\i n m. i \ I \ n \ m \ A n i \ A m i"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  996  shows "(\n. Pi I (A n)) = (\ i\I. \n. A n i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  997 proof (intro set_eqI iffI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  998  fix f assume "f \ (\ i\I. \n. A n i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  999  then have "\i\I. \n. f i \ A n i" by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1000  from bchoice[OF this] obtain n where n: "\i. i \ I \ f i \ (A (n i) i)" by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1001  obtain k where k: "\i. i \ I \ n i \ k"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1002  using finite I finite_nat_set_iff_bounded_le[of "nI"] by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1003  have "f \ Pi I (A k)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1004  proof (intro Pi_I)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1005  fix i assume "i \ I"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1006  from mono[OF this, of "n i" k] k[OF this] n[OF this]  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1007  show "f i \ A k i" by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1008  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1009  then show "f \ (\n. Pi I (A n))" by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1010 qed auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1011 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1012 lemma PiE_cong:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1013  assumes "\i. i\I \ A i = B i"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1014  shows "Pi\<^isub>E I A = Pi\<^isub>E I B"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1015  using assms by (auto intro!: Pi_cong)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1016 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1017 lemma sigma_product_algebra_sigma_eq:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1018  assumes "finite I"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1019  assumes isotone: "\i. i \ I \ (S i) \ (space (E i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1020  assumes sets_into: "\i. i \ I \ range (S i) \ sets (E i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1021  and E: "\i. sets (E i) \ Pow (space (E i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1022  shows "sigma (product_algebra (\i. sigma (E i)) I) = sigma (product_algebra E I)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1023  (is "?S = ?E")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1024 proof cases  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1025  assume "I = {}" then show ?thesis by (simp add: product_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1026 next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1027  assume "I \ {}"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1028  interpret E: sigma_algebra "sigma (E i)" for i  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1029  using E by (rule sigma_algebra_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1030 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1031  have into_space[intro]: "\i x A. A \ sets (E i) \ x i \ A \ x i \ space (E i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1032  using E by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1033 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1034  interpret G: sigma_algebra ?E  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1035  unfolding product_algebra_def using E  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1036  by (intro sigma_algebra_sigma) (auto dest: Pi_mem)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1037 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1038  { fix A i assume "i \ I" and A: "A \ sets (E i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1039  then have "(\x. x i) - A \ space ?E = (\\<^isub>E j\I. if j = i then A else \n. S j n) \ space ?E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1040  using isotone unfolding isoton_def product_algebra_def by (auto dest: Pi_mem)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1041  also have "\ = (\n. (\\<^isub>E j\I. if j = i then A else S j n))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1042  unfolding product_algebra_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1043  apply simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1044  apply (subst Pi_UN[OF finite I])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1045  using isotone[THEN isoton_mono_le] apply simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1046  apply (simp add: PiE_Int)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1047  apply (intro PiE_cong)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1048  using A sets_into by (auto intro!: into_space)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1049  also have "\ \ sets ?E" unfolding product_algebra_def sets_sigma  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1050  using sets_into A \ sets (E i)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1051  by (intro sigma_sets.Union)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1052  (auto simp: image_subset_iff intro!: sigma_sets.Basic)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1053  finally have "(\x. x i) - A \ space ?E \ sets ?E" . }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1054  then have proj:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1055  "\i. i\I \ (\x. x i) \ measurable ?E (sigma (E i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1056  using E by (subst G.measurable_iff_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1057  (auto simp: product_algebra_def sets_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1058 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1059  { fix A assume A: "\i. i \ I \ A i \ sets (sigma (E i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1060  with proj have basic: "\i. i \ I \ (\x. x i) - (A i) \ space ?E \ sets ?E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1061  unfolding measurable_def by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1062  have "Pi\<^isub>E I A = (\i\I. (\x. x i) - (A i) \ space ?E)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1063  using A E.sets_into_space I \ {} unfolding product_algebra_def by auto blast  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1064  then have "Pi\<^isub>E I A \ sets ?E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1065  using G.finite_INT[OF finite I I \ {} basic, of "\i. i"] by simp }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1066  then have "sigma_sets (space ?E) (sets (product_algebra (\i. sigma (E i)) I)) \ sets ?E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1067  by (intro G.sigma_sets_subset) (auto simp add: sets_sigma product_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1068  then have subset: "sets ?S \ sets ?E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1069  by (simp add: sets_sigma product_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1070 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1071  have "sets ?S = sets ?E"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1072  proof (intro set_eqI iffI)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1073  fix A assume "A \ sets ?E" then show "A \ sets ?S"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1074  unfolding sets_sigma  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1075  proof induct  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1076  case (Basic A) then show ?case  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1077  by (auto simp: sets_sigma product_algebra_def intro: sigma_sets.Basic)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1078  qed (auto intro: sigma_sets.intros simp: product_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1079  next  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1080  fix A assume "A \ sets ?S" then show "A \ sets ?E" using subset by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1081  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1082  then show ?thesis  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1083  by (simp add: product_algebra_def sigma_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1084 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1085 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1086 lemma (in finite_product_sigma_algebra) pair_sigma_algebra_finite_product_space:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1087  "sigma (pair_algebra P (M i)) = sigma (pair_algebra G (M i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1088 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1089  have "sigma (pair_algebra P (M i)) = sigma (pair_algebra P (sigma (M i)))" by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1090  also have "\ = sigma (pair_algebra G (M i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1091  proof (rule pair_sigma_algebra_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1092  show "(\_. \\<^isub>E i\I. space (M i)) \ space G"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1093  "(\_. space (M i)) \ space (M i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1094  by (simp_all add: isoton_const)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1095  show "range (\_. \\<^isub>E i\I. space (M i)) \ sets G" "range (\_. space (M i)) \ sets (M i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1096  by (auto intro!: image_eqI[where x="\i\I. space (M i)"] dest: Pi_mem  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1097  simp: product_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1098  show "sets G \ Pow (space G)" "sets (M i) \ Pow (space (M i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1099  using product_algebra_into_space M.sets_into_space by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1100  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1101  finally show ?thesis .  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1102 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1103 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1104 lemma sets_pair_algebra: "sets (pair_algebra N M) = (\(x, y). x \ y)  (sets N \ sets M)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1105  unfolding pair_algebra_def by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1106 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1107 lemma (in finite_product_sigma_algebra) sigma_pair_algebra_sigma_eq:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1108  "sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1109  sigma (pair_algebra (product_algebra M I) (product_algebra M J))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1110  using M.sets_into_space  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1111  by (intro pair_sigma_algebra_sigma[of "\_. \\<^isub>E i\I. space (M i)", of _ "\_. \\<^isub>E i\J. space (M i)"])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1112  (auto simp: isoton_const product_algebra_def, blast+)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1113 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1114 lemma (in product_sigma_algebra) product_product_vimage_algebra:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1115  assumes [simp]: "I \ J = {}" and "finite I" "finite J"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1116  shows "sigma_algebra.vimage_algebra  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1117  (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1118  (space (product_algebra M (I \ J))) (\x. ((\i\I. x i), (\i\J. x i))) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1119  sigma (product_algebra M (I \ J))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1120  (is "sigma_algebra.vimage_algebra _ (space ?IJ) ?f = sigma ?IJ")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1121 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1122  have "finite (I \ J)" using assms by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1123  interpret I: finite_product_sigma_algebra M I by default fact  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1124  interpret J: finite_product_sigma_algebra M J by default fact  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1125  interpret IJ: finite_product_sigma_algebra M "I \ J" by default fact  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1126  interpret pair_sigma_algebra I.P J.P by default  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1127 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1128  show "vimage_algebra (space ?IJ) ?f = sigma ?IJ"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1129  unfolding I.sigma_pair_algebra_sigma_eq  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1130  proof (rule vimage_algebra_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1131  from M.sets_into_space  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1132  show "sets (pair_algebra I.G J.G) \ Pow (space (pair_algebra I.G J.G))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1133  by (auto simp: sets_pair_algebra space_pair_algebra product_algebra_def) blast+  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1134  show "?f \ space IJ.G \ space (pair_algebra I.G J.G)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1135  by (auto simp: space_pair_algebra product_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1136  let ?F = "\A. ?f - A \ (space IJ.G)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1137  let ?s = "\I. Pi\<^isub>E I  (\ i\I. sets (M i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1138  { fix A assume "A \ sets IJ.G"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1139  then obtain F where A: "A = Pi\<^isub>E (I \ J) F" "F \ (\ i\I. sets (M i))" "F \ (\ i\J. sets (M i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1140  by (auto simp: product_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1141  show "A \ ?F  sets (pair_algebra I.G J.G)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1142  using A M.sets_into_space  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1143  by (auto simp: restrict_Pi_cancel product_algebra_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1144  intro!: image_eqI[where x="Pi\<^isub>E I F \ Pi\<^isub>E J F"]) blast+ }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1145  { fix A assume "A \ sets (pair_algebra I.G J.G)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1146  then obtain E F where A: "A = Pi\<^isub>E I E \ Pi\<^isub>E J F" "E \ (\ i\I. sets (M i))" "F \ (\ i\J. sets (M i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1147  by (auto simp: product_algebra_def sets_pair_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1148  then show "?F A \ sets IJ.G"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1149  using A M.sets_into_space  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1150  by (auto simp: restrict_Pi_cancel product_algebra_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1151  intro!: image_eqI[where x="merge I E J F"]) blast+ }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1152  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1153 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1154 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1155 lemma (in finite_product_sigma_algebra) sigma_pair_algebra_sigma_M_eq:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1156  "sigma (pair_algebra P (M i)) = sigma (pair_algebra G (M i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1157 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1158  have "sigma (pair_algebra P (sigma (M i))) = sigma (pair_algebra G (M i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1159  using M.sets_into_space  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1160  by (intro pair_sigma_algebra_sigma[of "\_. \\<^isub>E i\I. space (M i)", of _ "\_. space (M i)"])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1161  (auto simp: isoton_const product_algebra_def, blast+)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1162  then show ?thesis by simp  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1163 qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1164 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1165 lemma (in product_sigma_algebra) product_singleton_vimage_algebra_eq:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1166  assumes [simp]: "i \ I" "finite I"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1167  shows "sigma_algebra.vimage_algebra  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1168  (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1169  (space (product_algebra M (insert i I))) (\x. ((\i\I. x i), x i)) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1170  sigma (product_algebra M (insert i I))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1171  (is "sigma_algebra.vimage_algebra _ (space ?I') ?f = sigma ?I'")  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1172 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1173  have "finite (insert i I)" using assms by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1174  interpret I: finite_product_sigma_algebra M I by default fact  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1175  interpret I': finite_product_sigma_algebra M "insert i I" by default fact  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1176  interpret pair_sigma_algebra I.P "M i" by default  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1177  show "vimage_algebra (space ?I') ?f = sigma ?I'"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1178  unfolding I.sigma_pair_algebra_sigma_M_eq  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1179  proof (rule vimage_algebra_sigma)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1180  from M.sets_into_space  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1181  show "sets (pair_algebra I.G (M i)) \ Pow (space (pair_algebra I.G (M i)))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1182  by (auto simp: sets_pair_algebra space_pair_algebra product_algebra_def) blast  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1183  show "?f \ space I'.G \ space (pair_algebra I.G (M i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1184  by (auto simp: space_pair_algebra product_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1185  let ?F = "\A. ?f - A \ (space I'.G)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1186  { fix A assume "A \ sets I'.G"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1187  then obtain F where A: "A = Pi\<^isub>E (insert i I) F" "F \ (\ i\I. sets (M i))" "F i \ sets (M i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1188  by (auto simp: product_algebra_def)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1189  show "A \ ?F  sets (pair_algebra I.G (M i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1190  using A M.sets_into_space  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1191  by (auto simp: restrict_Pi_cancel product_algebra_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1192  intro!: image_eqI[where x="Pi\<^isub>E I F \ F i"]) blast+ }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1193  { fix A assume "A \ sets (pair_algebra I.G (M i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1194  then obtain E F where A: "A = Pi\<^isub>E I E \ F" "E \ (\ i\I. sets (M i))" "F \ sets (M i)"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1195  by (auto simp: product_algebra_def sets_pair_algebra)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1196  then show "?F A \ sets I'.G"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1197  using A M.sets_into_space  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1198  by (auto simp: restrict_Pi_cancel product_algebra_def  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1199  intro!: image_eqI[where x="E(i:= F)"]) blast+ }  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1200  qed  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1201 qed  38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36649 diff changeset  1202 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1203 lemma restrict_fupd[simp]: "i \ I \ restrict (f (i := x)) I = restrict f I"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1204  by (auto simp: restrict_def intro!: ext)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1205 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1206 lemma bij_betw_restrict_I_i:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1207  "i \ I \ bij_betw (\x. (restrict x I, x i))  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1208  (space (product_algebra M (insert i I)))  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1209  (space (pair_algebra (sigma (product_algebra M I)) (M i)))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1210  by (intro bij_betwI[where g="(\(x,y). x(i:=y))"])  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1211  (auto simp: space_pair_algebra extensional_def intro!: ext)  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1212 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1213 lemma (in product_sigma_algebra) product_singleton_vimage_algebra_inv_eq:  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1214  assumes [simp]: "i \ I" "finite I"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1215  shows "sigma_algebra.vimage_algebra  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1216  (sigma (product_algebra M (insert i I)))  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1217  (space (pair_algebra (sigma (product_algebra M I)) (M i))) (\(x,y). x(i:=y)) =  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1218  sigma (pair_algebra (sigma (product_algebra M I)) (M i))"  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1219 proof -  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1220  have "finite (insert i I)" using finite I by auto  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098 diff changeset  1221  interpret I: finite_product_sigma_algebra M I by default fact  de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39098