# HG changeset patch # User hoelzl # Date 1496869905 14400 # Node ID 704e4970d7034fb706edea985421c2561ec6a339 # Parent 96f86c613a9fe46ba10c02e6103ff236f25c49fd HOL-Probability: add measurable space for trees diff -r 96f86c613a9f -r 704e4970d703 src/HOL/Probability/Probability.thy --- a/src/HOL/Probability/Probability.thy Tue Jun 06 23:13:53 2017 +0200 +++ b/src/HOL/Probability/Probability.thy Wed Jun 07 17:11:45 2017 -0400 @@ -11,6 +11,7 @@ Random_Permutations SPMF Stream_Space + Tree_Space Conditional_Expectation Essential_Supremum Stopping_Time diff -r 96f86c613a9f -r 704e4970d703 src/HOL/Probability/Tree_Space.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Probability/Tree_Space.thy Wed Jun 07 17:11:45 2017 -0400 @@ -0,0 +1,343 @@ +(* Title: HOL/Probability/Tree_Space.thy + Author: Johannes Hölzl, CMU *) + +theory Tree_Space + imports Analysis +begin + +lemma countable_lfp: + assumes step: "\Y. countable Y \ countable (F Y)" + and cont: "Order_Continuity.sup_continuous F" + shows "countable (lfp F)" +by(subst sup_continuous_lfp[OF cont])(simp add: countable_funpow[OF step]) + +lemma countable_lfp_apply: + assumes step: "\Y x. (\x. countable (Y x)) \ countable (F Y x)" + and cont: "Order_Continuity.sup_continuous F" + shows "countable (lfp F x)" +proof - + { fix n + have "\x. countable ((F ^^ n) bot x)" + by(induct n)(auto intro: step) } + thus ?thesis using cont by(simp add: sup_continuous_lfp) +qed + +datatype 'a tree = Leaf + | Node (left: "'a tree") (val: 'a) (right: "'a tree") + where + "left Leaf = Leaf" + | "right Leaf = Leaf" + | "val Leaf = undefined" + +inductive_set trees :: "'a set \ 'a tree set" for S :: "'a set" where + [intro!]: "Leaf \ trees S" +| "l \ trees S \ r \ trees S \ v \ S \ Node l v r \ trees S" + +lemma Node_in_trees_iff[simp]: "Node l v r \ trees S \ (l \ trees S \ v \ S \ r \ trees S)" + by (subst trees.simps) auto + +lemma trees_sub_lfp: "trees S \ lfp (\T. T \ {Leaf} \ (\l\T. (\v\S. (\r\T. {Node l v r}))))" +proof + have mono: "mono (\T. T \ {Leaf} \ (\l\T. (\v\S. (\r\T. {Node l v r}))))" + by (auto simp: mono_def) + fix t assume "t \ trees S" then show "t \ lfp (\T. T \ {Leaf} \ (\l\T. (\v\S. (\r\T. {Node l v r}))))" + proof induction + case 1 then show ?case + by (subst lfp_unfold[OF mono]) auto + next + case 2 then show ?case + by (subst lfp_unfold[OF mono]) auto + qed +qed + +lemma countable_trees: "countable A \ countable (trees A)" + apply (rule countable_subset[OF trees_sub_lfp]) + apply (rule countable_lfp) + subgoal by auto + apply (intro sup_continuous_sup sup_continuous_const) + subgoal by (simp add: sup_continuous_def) + subgoal apply (auto simp add: sup_continuous_def) + subgoal premises prems for M x c a y d + using prems(3,5) prems(2)[THEN incseqD, of x "max x y"] prems(2)[THEN incseqD, of y "max x y"] + by (intro exI[of _ "max x y"]) auto + done + done + +lemma trees_UNIV[simp]: "trees UNIV = UNIV" +proof - + have "t \ trees UNIV" for t :: "'a tree" + by (induction t) (auto intro: trees.intros(2)) + then show ?thesis by auto +qed + +instance tree :: (countable) countable +proof + have "countable (UNIV :: 'a tree set)" + by (subst trees_UNIV[symmetric]) (intro countable_trees[OF countableI_type]) + then show "\to_nat::'a tree \ nat. inj to_nat" + by (auto simp: countable_def) +qed + +lemma map_in_trees[intro]: "(\x. x \ set_tree t \ f x \ S) \ map_tree f t \ trees S" + by (induction t) (auto intro: trees.intros(2)) + +primrec trees_cyl :: "'a set tree \ 'a tree set" where + "trees_cyl Leaf = {Leaf} " +| "trees_cyl (Node l v r) = (\l'\trees_cyl l. (\v'\v. (\r'\trees_cyl r. {Node l' v' r'})))" + +definition tree_sigma :: "'a measure \ 'a tree measure" +where + "tree_sigma M = sigma (trees (space M)) (trees_cyl ` trees (sets M))" + +lemma Node_in_trees_cyl: "Node l' v' r' \ trees_cyl t \ + (\l v r. t = Node l v r \ l' \ trees_cyl l \ r' \ trees_cyl r \ v' \ v)" + by (cases t) auto + +lemma trees_cyl_sub_trees: + assumes "t \ trees A" "A \ Pow B" shows "trees_cyl t \ trees B" + using assms(1) +proof induction + case (2 l v r) with \A \ Pow B\ show ?case + by (auto intro!: trees.intros(2)) +qed auto + +lemma trees_cyl_sets_in_space: "trees_cyl ` trees (sets M) \ Pow (trees (space M))" + using trees_cyl_sub_trees[OF _ sets.space_closed, of _ M] by auto + +lemma space_tree_sigma: "space (tree_sigma M) = trees (space M)" + unfolding tree_sigma_def by (rule space_measure_of_conv) + +lemma sets_tree_sigma_eq: "sets (tree_sigma M) = sigma_sets (trees (space M)) (trees_cyl ` trees (sets M))" + unfolding tree_sigma_def by (rule sets_measure_of) (rule trees_cyl_sets_in_space) + +lemma Leaf_in_tree_sigma[measurable]: "{Leaf} \ sets (tree_sigma M)" + unfolding sets_tree_sigma_eq + by (rule sigma_sets.Basic) (auto intro: trees.intros(2) image_eqI[where x=Leaf]) + +lemma trees_cyl_map_treeI: "t \ trees_cyl (map_tree (\x. A) t)" if *: "t \ trees A" + using * by induction auto + +lemma trees_cyl_map_in_sets: + "(\x. x \ set_tree t \ f x \ sets M) \ trees_cyl (map_tree f t) \ sets (tree_sigma M)" + by (subst sets_tree_sigma_eq) auto + +lemma Node_in_tree_sigma: + assumes L: "X \ sets (M \\<^sub>M (tree_sigma M \\<^sub>M tree_sigma M))" + shows "{Node l v r | l v r. (v, l, r) \ X} \ sets (tree_sigma M)" +proof - + let ?E = "\s::unit tree. trees_cyl (map_tree (\_. space M) s)" + have 1: "countable (range ?E)" + by (intro countable_image countableI_type) + have 2: "trees_cyl ` trees (sets M) \ Pow (space (tree_sigma M))" + using trees_cyl_sets_in_space[of M] by (simp add: space_tree_sigma) + have 3: "sets (tree_sigma M) = sigma_sets (space (tree_sigma M)) (trees_cyl ` trees (sets M))" + unfolding sets_tree_sigma_eq by (simp add: space_tree_sigma) + have 4: "(\s. ?E s) = space (tree_sigma M)" + proof (safe; clarsimp simp: space_tree_sigma) + fix t s assume "t \ trees_cyl (map_tree (\_::unit. space M) s)" + then show "t \ trees (space M)" + by (induction s arbitrary: t) auto + next + fix t assume "t \ trees (space M)" + then show "\t'. t \ ?E t'" + by (intro exI[of _ "map_tree (\_. ()) t"]) + (auto simp: tree.map_comp comp_def intro: trees_cyl_map_treeI) + qed + have 5: "range ?E \ trees_cyl ` trees (sets M)" by auto + let ?P = "{A \ B | A B. A \ trees_cyl ` trees (sets M) \ B \ trees_cyl ` trees (sets M)}" + have P: "sets (tree_sigma M \\<^sub>M tree_sigma M) = sets (sigma (space (tree_sigma M) \ space (tree_sigma M)) ?P)" + by (rule sets_pair_eq[OF 2 3 1 5 4 2 3 1 5 4]) + + have "sets (M \\<^sub>M (tree_sigma M \\<^sub>M tree_sigma M)) = + sets (sigma (space M \ space (tree_sigma M \\<^sub>M tree_sigma M)) {A \ BC | A BC. A \ sets M \ BC \ ?P})" + proof (rule sets_pair_eq) + show "sets M \ Pow (space M)" "sets M = sigma_sets (space M) (sets M)" + by (auto simp: sets.sigma_sets_eq sets.space_closed) + show "countable {space M}" "{space M} \ sets M" "\{space M} = space M" + by auto + show "?P \ Pow (space (tree_sigma M \\<^sub>M tree_sigma M))" + using trees_cyl_sets_in_space[of M] + by (auto simp: space_pair_measure space_tree_sigma subset_eq) + then show "sets (tree_sigma M \\<^sub>M tree_sigma M) = + sigma_sets (space (tree_sigma M \\<^sub>M tree_sigma M)) ?P" + by (subst P, subst sets_measure_of) (auto simp: space_tree_sigma space_pair_measure) + show "countable ((\(a, b). a \ b) ` (range ?E \ range ?E))" + by (intro countable_image countable_SIGMA countableI_type) + show "(\(a, b). a \ b) ` (range ?E \ range ?E) \ ?P" + by auto + qed (insert 4, auto simp: space_pair_measure space_tree_sigma set_eq_iff) + also have "\ = sigma_sets (space M \ trees (space M) \ trees (space M)) + {A \ trees_cyl B \ trees_cyl C | A B C. A \ sets M \ B \ trees (sets M) \ C \ trees (sets M) }" + apply (subst sets_measure_of) + subgoal + using sets.space_closed[of M] trees_cyl_sets_in_space[of M] + by (clarsimp simp: space_pair_measure space_tree_sigma) blast + apply (rule arg_cong2[where f=sigma_sets]) + apply (auto simp: space_pair_measure space_tree_sigma) + subgoal premises prems for A B C + apply (rule exI conjI refl prems)+ + using trees_cyl_sets_in_space[of M] prems + by auto + done + finally have "X \ sigma_sets (space M \ trees (space M) \ trees (space M)) + {A \ trees_cyl B \ trees_cyl C | A B C. A \ sets M \ B \ trees (sets M) \ C \ trees (sets M) }" + using assms by auto + then show ?thesis + proof induction + case (Basic A') + then obtain A B C where "A' = A \ trees_cyl B \ trees_cyl C" + and *: "A \ sets M" "B \ trees (sets M)" "C \ trees (sets M)" + by auto + then have "{Node l v r |l v r. (v, l, r) \ A'} = trees_cyl (Node B A C)" + by auto + then show ?case + by (auto simp del: trees_cyl.simps simp: sets_tree_sigma_eq intro!: sigma_sets.Basic *) + next + case Empty show ?case by auto + next + case (Compl A) + have "{Node l v r |l v r. (v, l, r) \ space M \ trees (space M) \ trees (space M) - A} = + (space (tree_sigma M) - {Node l v r |l v r. (v, l, r) \ A}) - {Leaf}" + apply (auto simp: space_tree_sigma) + subgoal for t + by (cases t) auto + done + also have "\ \ sets (tree_sigma M)" + by (intro sets.Diff Compl) auto + finally show ?case . + next + case (Union I) + have *: "{Node l v r |l v r. (v, l, r) \ UNION UNIV I} = + (\i. {Node l v r |l v r. (v, l, r) \ I i})" by auto + show ?case unfolding * using Union(2) by (intro sets.countable_UN) auto + qed +qed + +lemma measurable_left[measurable]: "left \ tree_sigma M \\<^sub>M tree_sigma M" +proof (rule measurableI) + show "t \ space (tree_sigma M) \ left t \ space (tree_sigma M)" for t + by (cases t) (auto simp: space_tree_sigma) + fix A assume A: "A \ sets (tree_sigma M)" + from sets.sets_into_space[OF this] + have *: "left -` A \ space (tree_sigma M) = + (if Leaf \ A then {Leaf} else {}) \ + {Node a v r | a v r. (v, a, r) \ space M \ A \ space (tree_sigma M)}" + by (auto simp: space_tree_sigma elim: trees.cases) + show "left -` A \ space (tree_sigma M) \ sets (tree_sigma M)" + unfolding * using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto +qed + +lemma measurable_right[measurable]: "right \ tree_sigma M \\<^sub>M tree_sigma M" +proof (rule measurableI) + show "t \ space (tree_sigma M) \ right t \ space (tree_sigma M)" for t + by (cases t) (auto simp: space_tree_sigma) + fix A assume A: "A \ sets (tree_sigma M)" + from sets.sets_into_space[OF this] + have *: "right -` A \ space (tree_sigma M) = + (if Leaf \ A then {Leaf} else {}) \ + {Node l v a | l v a. (v, l, a) \ space M \ space (tree_sigma M) \ A}" + by (auto simp: space_tree_sigma elim: trees.cases) + show "right -` A \ space (tree_sigma M) \ sets (tree_sigma M)" + unfolding * using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto +qed + +lemma measurable_val': "val \ restrict_space (tree_sigma M) (-{Leaf}) \\<^sub>M M" +proof (rule measurableI) + show "t \ space (restrict_space (tree_sigma M) (- {Leaf})) \ val t \ space M" for t + by (cases t) (auto simp: space_restrict_space space_tree_sigma) + fix A assume A: "A \ sets M" + from sets.sets_into_space[OF this] + have "val -` A \ space (restrict_space (tree_sigma M) (- {Leaf})) = + {Node l a r | l a r. (a, l, r) \ A \ space (tree_sigma M) \ space (tree_sigma M)}" + by (auto simp: space_tree_sigma space_restrict_space elim: trees.cases) + also have "\ \ sets (tree_sigma M)" + using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto + finally show "val -` A \ space (restrict_space (tree_sigma M) (- {Leaf})) \ + sets (restrict_space (tree_sigma M) (- {Leaf}))" + by (auto simp: sets_restrict_space_iff space_restrict_space) +qed + +lemma measurable_restrict_mono: + assumes f: "f \ restrict_space M A \\<^sub>M N" and "B \ A" + shows "f \ restrict_space M B \\<^sub>M N" +by (rule measurable_compose[OF measurable_restrict_space3 f]) + (insert \B \ A\, auto) + +(* +lemma measurable_val[measurable (raw)]: + assumes "f \ X \\<^sub>M tree_sigma M" + and "\x. x \ space X \ f x \ Leaf" + shows "(\\. val (f \)) \ X \\<^sub>M M" + sorry +*) + +lemma measurable_rec_tree[measurable (raw)]: + assumes t: "t \ B \\<^sub>M tree_sigma M" + assumes l: "l \ B \\<^sub>M A" + assumes n: "(\(x, l, v, r, al, ar). n x l v r al ar) \ + (B \\<^sub>M tree_sigma M \\<^sub>M M \\<^sub>M tree_sigma M \\<^sub>M A \\<^sub>M A) \\<^sub>M A" (is "?N \ ?M \\<^sub>M A") + shows "(\x. rec_tree (l x) (n x) (t x)) \ B \\<^sub>M A" +proof (rule measurable_piecewise_restrict) + let ?C = "\t. \s::unit tree. t -` trees_cyl (map_tree (\_. space M) s)" + show "countable (range (?C t))" by (intro countable_image countableI_type) + show "space B \ (\s. ?C t s)" + proof (safe; clarsimp) + fix x assume x: "x \ space B" have "t x \ trees (space M)" + using t[THEN measurable_space, OF x] by (simp add: space_tree_sigma) + then show "\xa::unit tree. t x \ trees_cyl (map_tree (\_. space M) xa)" + by (intro exI[of _ "map_tree (\_. ()) (t x)"]) + (simp add: tree.map_comp comp_def trees_cyl_map_treeI) + qed + fix \ assume "\ \ range (?C t)" + then obtain s :: "unit tree" where \: "\ = ?C t s" by auto + then show "\ \ space B \ sets B" + by (safe intro!: measurable_sets[OF t] trees_cyl_map_in_sets) + show "(\x. rec_tree (l x) (n x) (t x)) \ restrict_space B \ \\<^sub>M A" + unfolding \ using t + proof (induction s arbitrary: t) + case Leaf + show ?case + proof (rule measurable_cong[THEN iffD2]) + fix \ assume "\ \ space (restrict_space B (?C t Leaf))" + then show "rec_tree (l \) (n \) (t \) = l \" + by (auto simp: space_restrict_space) + next + show "l \ restrict_space B (?C t Leaf) \\<^sub>M A" + using l by (rule measurable_restrict_space1) + qed + next + case (Node ls u rs) + let ?F = "\\. ?N (\, left (t \), val (t \), right (t \), + rec_tree (l \) (n \) (left (t \)), rec_tree (l \) (n \) (right (t \)))" + show ?case + proof (rule measurable_cong[THEN iffD2]) + fix \ assume "\ \ space (restrict_space B (?C t (Node ls u rs)))" + then show "rec_tree (l \) (n \) (t \) = ?F \" + by (auto simp: space_restrict_space) + next + show "?F \ (restrict_space B (?C t (Node ls u rs))) \\<^sub>M A" + apply (intro measurable_compose[OF _ n] measurable_Pair[rotated]) + subgoal + apply (rule measurable_restrict_mono[OF Node(2)]) + apply (rule measurable_compose[OF Node(3) measurable_right]) + by auto + subgoal + apply (rule measurable_restrict_mono[OF Node(1)]) + apply (rule measurable_compose[OF Node(3) measurable_left]) + by auto + subgoal + by (rule measurable_restrict_space1) + (rule measurable_compose[OF Node(3) measurable_right]) + subgoal + apply (rule measurable_compose[OF _ measurable_val']) + apply (rule measurable_restrict_space3[OF Node(3)]) + by auto + subgoal + by (rule measurable_restrict_space1) + (rule measurable_compose[OF Node(3) measurable_left]) + by (rule measurable_restrict_space1) auto + qed + qed +qed + +end