add syntax and a.e.-rules for (conditional) probability on predicates
authorhoelzl
Fri Nov 02 14:00:39 2012 +0100 (2012-11-02)
changeset 50001382bd3173584
parent 50000 cfe8ee8a1371
child 50002 ce0d316b5b44
add syntax and a.e.-rules for (conditional) probability on predicates
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Probability_Measure.thy
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:00:39 2012 +0100
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:00:39 2012 +0100
     1.3 @@ -91,6 +91,11 @@
     1.4    unfolding indicator_def [abs_def] using A
     1.5    by (auto intro!: measurable_If_set)
     1.6  
     1.7 +lemma borel_measurable_indicator': 
     1.8 +  "{x\<in>space M. x \<in> A} \<in> sets M \<Longrightarrow> indicator A \<in> borel_measurable M"
     1.9 +  unfolding indicator_def[abs_def]
    1.10 +  by (auto intro!: measurable_If)
    1.11 +
    1.12  lemma borel_measurable_indicator_iff:
    1.13    "(indicator A :: 'a \<Rightarrow> 'x::{t1_space, zero_neq_one}) \<in> borel_measurable M \<longleftrightarrow> A \<inter> space M \<in> sets M"
    1.14      (is "?I \<in> borel_measurable M \<longleftrightarrow> _")
     2.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 02 14:00:39 2012 +0100
     2.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 02 14:00:39 2012 +0100
     2.3 @@ -1403,6 +1403,11 @@
     2.4    finally show ?thesis .
     2.5  qed
     2.6  
     2.7 +lemma AE_iff_positive_integral: 
     2.8 +  "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> integral\<^isup>P M (indicator {x. \<not> P x}) = 0"
     2.9 +  by (subst positive_integral_0_iff_AE)
    2.10 +     (auto simp: one_ereal_def zero_ereal_def sets_Collect_neg indicator_def[abs_def] measurable_If)
    2.11 +
    2.12  lemma positive_integral_const_If:
    2.13    "(\<integral>\<^isup>+x. a \<partial>M) = (if 0 \<le> a then a * (emeasure M) (space M) else 0)"
    2.14    by (auto intro!: positive_integral_0_iff_AE[THEN iffD2])
     3.1 --- a/src/HOL/Probability/Measure_Space.thy	Fri Nov 02 14:00:39 2012 +0100
     3.2 +++ b/src/HOL/Probability/Measure_Space.thy	Fri Nov 02 14:00:39 2012 +0100
     3.3 @@ -1095,6 +1095,10 @@
     3.4    show "sigma_algebra (space N) (sets N)" ..
     3.5  qed fact
     3.6  
     3.7 +lemma measure_distr:
     3.8 +  "f \<in> measurable M N \<Longrightarrow> S \<in> sets N \<Longrightarrow> measure (distr M N f) S = measure M (f -` S \<inter> space M)"
     3.9 +  by (simp add: emeasure_distr measure_def)
    3.10 +
    3.11  lemma AE_distrD:
    3.12    assumes f: "f \<in> measurable M M'"
    3.13      and AE: "AE x in distr M M' f. P x"
     4.1 --- a/src/HOL/Probability/Probability_Measure.thy	Fri Nov 02 14:00:39 2012 +0100
     4.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Fri Nov 02 14:00:39 2012 +0100
     4.3 @@ -395,6 +395,81 @@
     4.4    shows "prob {y} = 0"
     4.5    using prob_one_inter[of "{y}" "{x}"] assms by auto
     4.6  
     4.7 +subsection  {* Introduce binder for probability *}
     4.8 +
     4.9 +syntax
    4.10 +  "_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("('\<P>'(_ in _. _'))")
    4.11 +
    4.12 +translations
    4.13 +  "\<P>(x in M. P)" => "CONST measure M {x \<in> CONST space M. P}"
    4.14 +
    4.15 +definition
    4.16 +  "cond_prob M P Q = \<P>(\<omega> in M. P \<omega> \<and> Q \<omega>) / \<P>(\<omega> in M. Q \<omega>)"
    4.17 +
    4.18 +syntax
    4.19 +  "_conditional_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("('\<P>'(_ in _. _ \<bar>/ _'))")
    4.20 +
    4.21 +translations
    4.22 +  "\<P>(x in M. P \<bar> Q)" => "CONST cond_prob M (\<lambda>x. P) (\<lambda>x. Q)"
    4.23 +
    4.24 +lemma (in prob_space) AE_E_prob:
    4.25 +  assumes ae: "AE x in M. P x"
    4.26 +  obtains S where "S \<subseteq> {x \<in> space M. P x}" "S \<in> events" "prob S = 1"
    4.27 +proof -
    4.28 +  from ae[THEN AE_E] guess N .
    4.29 +  then show thesis
    4.30 +    by (intro that[of "space M - N"])
    4.31 +       (auto simp: prob_compl prob_space emeasure_eq_measure)
    4.32 +qed
    4.33 +
    4.34 +lemma (in prob_space) prob_neg: "{x\<in>space M. P x} \<in> events \<Longrightarrow> \<P>(x in M. \<not> P x) = 1 - \<P>(x in M. P x)"
    4.35 +  by (auto intro!: arg_cong[where f=prob] simp add: prob_compl[symmetric])
    4.36 +
    4.37 +lemma (in prob_space) prob_eq_AE:
    4.38 +  "(AE x in M. P x \<longleftrightarrow> Q x) \<Longrightarrow> {x\<in>space M. P x} \<in> events \<Longrightarrow> {x\<in>space M. Q x} \<in> events \<Longrightarrow> \<P>(x in M. P x) = \<P>(x in M. Q x)"
    4.39 +  by (rule finite_measure_eq_AE) auto
    4.40 +
    4.41 +lemma (in prob_space) prob_eq_0_AE:
    4.42 +  assumes not: "AE x in M. \<not> P x" shows "\<P>(x in M. P x) = 0"
    4.43 +proof cases
    4.44 +  assume "{x\<in>space M. P x} \<in> events"
    4.45 +  with not have "\<P>(x in M. P x) = \<P>(x in M. False)"
    4.46 +    by (intro prob_eq_AE) auto
    4.47 +  then show ?thesis by simp
    4.48 +qed (simp add: measure_notin_sets)
    4.49 +
    4.50 +lemma (in prob_space) prob_sums:
    4.51 +  assumes P: "\<And>n. {x\<in>space M. P n x} \<in> events"
    4.52 +  assumes Q: "{x\<in>space M. Q x} \<in> events"
    4.53 +  assumes ae: "AE x in M. (\<forall>n. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n. P n x))"
    4.54 +  shows "(\<lambda>n. \<P>(x in M. P n x)) sums \<P>(x in M. Q x)"
    4.55 +proof -
    4.56 +  from ae[THEN AE_E_prob] guess S . note S = this
    4.57 +  then have disj: "disjoint_family (\<lambda>n. {x\<in>space M. P n x} \<inter> S)"
    4.58 +    by (auto simp: disjoint_family_on_def)
    4.59 +  from S have ae_S:
    4.60 +    "AE x in M. x \<in> {x\<in>space M. Q x} \<longleftrightarrow> x \<in> (\<Union>n. {x\<in>space M. P n x} \<inter> S)"
    4.61 +    "\<And>n. AE x in M. x \<in> {x\<in>space M. P n x} \<longleftrightarrow> x \<in> {x\<in>space M. P n x} \<inter> S"
    4.62 +    using ae by (auto dest!: AE_prob_1)
    4.63 +  from ae_S have *:
    4.64 +    "\<P>(x in M. Q x) = prob (\<Union>n. {x\<in>space M. P n x} \<inter> S)"
    4.65 +    using P Q S by (intro finite_measure_eq_AE) auto
    4.66 +  from ae_S have **:
    4.67 +    "\<And>n. \<P>(x in M. P n x) = prob ({x\<in>space M. P n x} \<inter> S)"
    4.68 +    using P Q S by (intro finite_measure_eq_AE) auto
    4.69 +  show ?thesis
    4.70 +    unfolding * ** using S P disj
    4.71 +    by (intro finite_measure_UNION) auto
    4.72 +qed
    4.73 +
    4.74 +lemma (in prob_space) cond_prob_eq_AE:
    4.75 +  assumes P: "AE x in M. Q x \<longrightarrow> P x \<longleftrightarrow> P' x" "{x\<in>space M. P x} \<in> events" "{x\<in>space M. P' x} \<in> events"
    4.76 +  assumes Q: "AE x in M. Q x \<longleftrightarrow> Q' x" "{x\<in>space M. Q x} \<in> events" "{x\<in>space M. Q' x} \<in> events"
    4.77 +  shows "cond_prob M P Q = cond_prob M P' Q'"
    4.78 +  using P Q
    4.79 +  by (auto simp: cond_prob_def intro!: arg_cong2[where f="op /"] prob_eq_AE sets_Collect_conj)
    4.80 +
    4.81 +
    4.82  lemma (in prob_space) joint_distribution_Times_le_fst:
    4.83    "random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY
    4.84      \<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^isub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MX X) A"
    4.85 @@ -587,7 +662,7 @@
    4.86        by (auto simp add: eq measurable_Pair measurable_compose[OF _ f(1)] positive_integral_multc
    4.87                 intro!: positive_integral_cong)
    4.88      also have "\<dots> = emeasure ?R E"
    4.89 -      by (auto simp add: emeasure_density ST.positive_integral_fst_measurable(2)[symmetric]
    4.90 +      by (auto simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric]
    4.91                 intro!: positive_integral_cong split: split_indicator)
    4.92      finally show "emeasure ?L E = emeasure ?R E" .
    4.93    qed
    4.94 @@ -661,7 +736,7 @@
    4.95      unfolding measurable_pair_iff by (simp add: comp_def)
    4.96  
    4.97    from Pxy show borel: "Px \<in> borel_measurable S"
    4.98 -    by (auto intro!: ST.positive_integral_fst_measurable dest!: distributed_borel_measurable simp: Px_def)
    4.99 +    by (auto intro!: T.positive_integral_fst_measurable dest!: distributed_borel_measurable simp: Px_def)
   4.100  
   4.101    interpret Pxy: prob_space "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
   4.102      using XY by (rule prob_space_distr)
   4.103 @@ -679,7 +754,7 @@
   4.104        using Pxy by (simp add: distributed_def)
   4.105      also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"
   4.106        using A borel Pxy
   4.107 -      by (simp add: emeasure_density ST.positive_integral_fst_measurable(2)[symmetric] distributed_def)
   4.108 +      by (simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric] distributed_def)
   4.109      also have "\<dots> = \<integral>\<^isup>+ x. Px x * indicator A x \<partial>S"
   4.110        apply (rule positive_integral_cong_AE)
   4.111        using Pxy[THEN distributed_AE, THEN ST.AE_pair] AE_space