src/HOL/Probability/Measurable.thy
changeset 59000 6eb0725503fc
parent 58965 a62cdcc5344b
child 59047 8d7cec9b861d
     1.1 --- a/src/HOL/Probability/Measurable.thy	Thu Nov 13 14:40:06 2014 +0100
     1.2 +++ b/src/HOL/Probability/Measurable.thy	Thu Nov 13 17:19:52 2014 +0100
     1.3 @@ -198,6 +198,14 @@
     1.4      by (simp add: eq_commute)
     1.5  qed
     1.6  
     1.7 +lemma pred_count_space_const1[measurable (raw)]:
     1.8 +  "f \<in> measurable M (count_space UNIV) \<Longrightarrow> Measurable.pred M (\<lambda>x. f x = c)"
     1.9 +  by (intro pred_eq_const1[where N="count_space UNIV"]) (auto )
    1.10 +
    1.11 +lemma pred_count_space_const2[measurable (raw)]:
    1.12 +  "f \<in> measurable M (count_space UNIV) \<Longrightarrow> Measurable.pred M (\<lambda>x. c = f x)"
    1.13 +  by (intro pred_eq_const2[where N="count_space UNIV"]) (auto )
    1.14 +
    1.15  lemma pred_le_const[measurable (raw generic)]:
    1.16    assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
    1.17    using measurable_sets[OF f c]
    1.18 @@ -335,6 +343,9 @@
    1.19    "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
    1.20    by simp
    1.21  
    1.22 +lemma sets_UNIV [measurable (raw)]: "A \<in> sets (count_space UNIV)"
    1.23 +  by simp
    1.24 +
    1.25  lemma measurable_card[measurable]:
    1.26    fixes S :: "'a \<Rightarrow> nat set"
    1.27    assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
    1.28 @@ -394,6 +405,187 @@
    1.29    finally show ?thesis .
    1.30  qed
    1.31  
    1.32 +lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]:
    1.33 +  assumes "P M"
    1.34 +  assumes "Order_Continuity.continuous F"
    1.35 +  assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
    1.36 +  shows "Measurable.pred M (lfp F)"
    1.37 +proof -
    1.38 +  { fix i from `P M` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
    1.39 +      by (induct i arbitrary: M) (auto intro!: *) }
    1.40 +  then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x)"
    1.41 +    by measurable
    1.42 +  also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
    1.43 +    by (auto simp add: bot_fun_def)
    1.44 +  also have "\<dots> = lfp F"
    1.45 +    by (rule continuous_lfp[symmetric]) fact
    1.46 +  finally show ?thesis .
    1.47 +qed
    1.48 +
    1.49 +lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]:
    1.50 +  assumes "P M"
    1.51 +  assumes "Order_Continuity.down_continuous F"
    1.52 +  assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
    1.53 +  shows "Measurable.pred M (gfp F)"
    1.54 +proof -
    1.55 +  { fix i from `P M` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
    1.56 +      by (induct i arbitrary: M) (auto intro!: *) }
    1.57 +  then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x)"
    1.58 +    by measurable
    1.59 +  also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
    1.60 +    by (auto simp add: top_fun_def)
    1.61 +  also have "\<dots> = gfp F"
    1.62 +    by (rule down_continuous_gfp[symmetric]) fact
    1.63 +  finally show ?thesis .
    1.64 +qed
    1.65 +
    1.66 +lemma measurable_lfp2_coinduct[consumes 1, case_names continuity step]:
    1.67 +  assumes "P M s"
    1.68 +  assumes "Order_Continuity.continuous F"
    1.69 +  assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> Measurable.pred N (A t)) \<Longrightarrow> Measurable.pred M (F A s)"
    1.70 +  shows "Measurable.pred M (lfp F s)"
    1.71 +proof -
    1.72 +  { fix i from `P M s` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>t x. False) s x)"
    1.73 +      by (induct i arbitrary: M s) (auto intro!: *) }
    1.74 +  then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>t x. False) s x)"
    1.75 +    by measurable
    1.76 +  also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>t x. False) s x) = (SUP i. (F ^^ i) bot) s"
    1.77 +    by (auto simp add: bot_fun_def)
    1.78 +  also have "(SUP i. (F ^^ i) bot) = lfp F"
    1.79 +    by (rule continuous_lfp[symmetric]) fact
    1.80 +  finally show ?thesis .
    1.81 +qed
    1.82 +
    1.83 +lemma measurable_gfp2_coinduct[consumes 1, case_names continuity step]:
    1.84 +  assumes "P M s"
    1.85 +  assumes "Order_Continuity.down_continuous F"
    1.86 +  assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> Measurable.pred N (A t)) \<Longrightarrow> Measurable.pred M (F A s)"
    1.87 +  shows "Measurable.pred M (gfp F s)"
    1.88 +proof -
    1.89 +  { fix i from `P M s` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>t x. True) s x)"
    1.90 +      by (induct i arbitrary: M s) (auto intro!: *) }
    1.91 +  then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>t x. True) s x)"
    1.92 +    by measurable
    1.93 +  also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>t x. True) s x) = (INF i. (F ^^ i) top) s"
    1.94 +    by (auto simp add: top_fun_def)
    1.95 +  also have "(INF i. (F ^^ i) top) = gfp F"
    1.96 +    by (rule down_continuous_gfp[symmetric]) fact
    1.97 +  finally show ?thesis .
    1.98 +qed
    1.99 +
   1.100 +lemma measurable_enat_coinduct:
   1.101 +  fixes f :: "'a \<Rightarrow> enat"
   1.102 +  assumes "R f"
   1.103 +  assumes *: "\<And>f. R f \<Longrightarrow> \<exists>g h i P. R g \<and> f = (\<lambda>x. if P x then h x else eSuc (g (i x))) \<and> 
   1.104 +    Measurable.pred M P \<and>
   1.105 +    i \<in> measurable M M \<and>
   1.106 +    h \<in> measurable M (count_space UNIV)"
   1.107 +  shows "f \<in> measurable M (count_space UNIV)"
   1.108 +proof (simp add: measurable_count_space_eq2_countable, rule )
   1.109 +  fix a :: enat
   1.110 +  have "f -` {a} \<inter> space M = {x\<in>space M. f x = a}"
   1.111 +    by auto
   1.112 +  { fix i :: nat
   1.113 +    from `R f` have "Measurable.pred M (\<lambda>x. f x = enat i)"
   1.114 +    proof (induction i arbitrary: f)
   1.115 +      case 0
   1.116 +      from *[OF this] obtain g h i P
   1.117 +        where f: "f = (\<lambda>x. if P x then h x else eSuc (g (i x)))" and
   1.118 +          [measurable]: "Measurable.pred M P" "i \<in> measurable M M" "h \<in> measurable M (count_space UNIV)"
   1.119 +        by auto
   1.120 +      have "Measurable.pred M (\<lambda>x. P x \<and> h x = 0)"
   1.121 +        by measurable
   1.122 +      also have "(\<lambda>x. P x \<and> h x = 0) = (\<lambda>x. f x = enat 0)"
   1.123 +        by (auto simp: f zero_enat_def[symmetric])
   1.124 +      finally show ?case .
   1.125 +    next
   1.126 +      case (Suc n)
   1.127 +      from *[OF Suc.prems] obtain g h i P
   1.128 +        where f: "f = (\<lambda>x. if P x then h x else eSuc (g (i x)))" and "R g" and
   1.129 +          M[measurable]: "Measurable.pred M P" "i \<in> measurable M M" "h \<in> measurable M (count_space UNIV)"
   1.130 +        by auto
   1.131 +      have "(\<lambda>x. f x = enat (Suc n)) =
   1.132 +        (\<lambda>x. (P x \<longrightarrow> h x = enat (Suc n)) \<and> (\<not> P x \<longrightarrow> g (i x) = enat n))"
   1.133 +        by (auto simp: f zero_enat_def[symmetric] eSuc_enat[symmetric])
   1.134 +      also have "Measurable.pred M \<dots>"
   1.135 +        by (intro pred_intros_logic measurable_compose[OF M(2)] Suc `R g`) measurable
   1.136 +      finally show ?case .
   1.137 +    qed
   1.138 +    then have "f -` {enat i} \<inter> space M \<in> sets M"
   1.139 +      by (simp add: pred_def Int_def conj_commute) }
   1.140 +  note fin = this
   1.141 +  show "f -` {a} \<inter> space M \<in> sets M"
   1.142 +  proof (cases a)
   1.143 +    case infinity
   1.144 +    then have "f -` {a} \<inter> space M = space M - (\<Union>n. f -` {enat n} \<inter> space M)"
   1.145 +      by auto
   1.146 +    also have "\<dots> \<in> sets M"
   1.147 +      by (intro sets.Diff sets.top sets.Un sets.countable_UN) (auto intro!: fin)
   1.148 +    finally show ?thesis .
   1.149 +  qed (simp add: fin)
   1.150 +qed
   1.151 +
   1.152 +lemma measurable_pred_countable[measurable (raw)]:
   1.153 +  assumes "countable X"
   1.154 +  shows 
   1.155 +    "(\<And>i. i \<in> X \<Longrightarrow> Measurable.pred M (\<lambda>x. P x i)) \<Longrightarrow> Measurable.pred M (\<lambda>x. \<forall>i\<in>X. P x i)"
   1.156 +    "(\<And>i. i \<in> X \<Longrightarrow> Measurable.pred M (\<lambda>x. P x i)) \<Longrightarrow> Measurable.pred M (\<lambda>x. \<exists>i\<in>X. P x i)"
   1.157 +  unfolding pred_def
   1.158 +  by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms)
   1.159 +
   1.160 +lemma measurable_THE:
   1.161 +  fixes P :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   1.162 +  assumes [measurable]: "\<And>i. Measurable.pred M (P i)"
   1.163 +  assumes I[simp]: "countable I" "\<And>i x. x \<in> space M \<Longrightarrow> P i x \<Longrightarrow> i \<in> I"
   1.164 +  assumes unique: "\<And>x i j. x \<in> space M \<Longrightarrow> P i x \<Longrightarrow> P j x \<Longrightarrow> i = j"
   1.165 +  shows "(\<lambda>x. THE i. P i x) \<in> measurable M (count_space UNIV)"
   1.166 +  unfolding measurable_def
   1.167 +proof safe
   1.168 +  fix X
   1.169 +  def f \<equiv> "\<lambda>x. THE i. P i x" def undef \<equiv> "THE i::'a. False"
   1.170 +  { fix i x assume "x \<in> space M" "P i x" then have "f x = i"
   1.171 +      unfolding f_def using unique by auto }
   1.172 +  note f_eq = this
   1.173 +  { fix x assume "x \<in> space M" "\<forall>i\<in>I. \<not> P i x"
   1.174 +    then have "\<And>i. \<not> P i x"
   1.175 +      using I(2)[of x] by auto
   1.176 +    then have "f x = undef"
   1.177 +      by (auto simp: undef_def f_def) }
   1.178 +  then have "f -` X \<inter> space M = (\<Union>i\<in>I \<inter> X. {x\<in>space M. P i x}) \<union>
   1.179 +     (if undef \<in> X then space M - (\<Union>i\<in>I. {x\<in>space M. P i x}) else {})"
   1.180 +    by (auto dest: f_eq)
   1.181 +  also have "\<dots> \<in> sets M"
   1.182 +    by (auto intro!: sets.Diff sets.countable_UN')
   1.183 +  finally show "f -` X \<inter> space M \<in> sets M" .
   1.184 +qed simp
   1.185 +
   1.186 +lemma measurable_bot[measurable]: "Measurable.pred M bot"
   1.187 +  by (simp add: bot_fun_def)
   1.188 +
   1.189 +lemma measurable_top[measurable]: "Measurable.pred M top"
   1.190 +  by (simp add: top_fun_def)
   1.191 +
   1.192 +lemma measurable_Ex1[measurable (raw)]:
   1.193 +  assumes [simp]: "countable I" and [measurable]: "\<And>i. i \<in> I \<Longrightarrow> Measurable.pred M (P i)"
   1.194 +  shows "Measurable.pred M (\<lambda>x. \<exists>!i\<in>I. P i x)"
   1.195 +  unfolding bex1_def by measurable
   1.196 +
   1.197 +lemma measurable_split_if[measurable (raw)]:
   1.198 +  "(c \<Longrightarrow> Measurable.pred M f) \<Longrightarrow> (\<not> c \<Longrightarrow> Measurable.pred M g) \<Longrightarrow>
   1.199 +   Measurable.pred M (if c then f else g)"
   1.200 +  by simp
   1.201 +
   1.202 +lemma pred_restrict_space:
   1.203 +  assumes "S \<in> sets M"
   1.204 +  shows "Measurable.pred (restrict_space M S) P \<longleftrightarrow> Measurable.pred M (\<lambda>x. x \<in> S \<and> P x)"
   1.205 +  unfolding pred_def sets_Collect_restrict_space_iff[OF assms] ..
   1.206 +
   1.207 +lemma measurable_predpow[measurable]:
   1.208 +  assumes "Measurable.pred M T"
   1.209 +  assumes "\<And>Q. Measurable.pred M Q \<Longrightarrow> Measurable.pred M (R Q)"
   1.210 +  shows "Measurable.pred M ((R ^^ n) T)"
   1.211 +  by (induct n) (auto intro: assms)
   1.212 +
   1.213  hide_const (open) pred
   1.214  
   1.215  end