src/HOL/Probability/Probability_Measure.thy
author hoelzl
Mon, 23 Apr 2012 12:14:35 +0200
changeset 47694 05663f75964c
parent 46905 6b1c0a80a57a
child 49776 199d1d5bb17e
permissions -rw-r--r--
reworked Probability theory
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42148
d596e7bb251f rename Probability_Space to Probability_Measure
hoelzl
parents: 42146
diff changeset
     1
(*  Title:      HOL/Probability/Probability_Measure.thy
42067
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     2
    Author:     Johannes Hölzl, TU München
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     3
    Author:     Armin Heller, TU München
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     4
*)
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     5
42148
d596e7bb251f rename Probability_Space to Probability_Measure
hoelzl
parents: 42146
diff changeset
     6
header {*Probability measure*}
42067
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     7
42148
d596e7bb251f rename Probability_Space to Probability_Measure
hoelzl
parents: 42146
diff changeset
     8
theory Probability_Measure
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
     9
  imports Lebesgue_Measure Radon_Nikodym
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    10
begin
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    11
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    12
lemma funset_eq_UN_fun_upd_I:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    13
  assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    14
  and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    15
  and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    16
  shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    17
proof safe
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    18
  fix f assume f: "f \<in> F (insert a A)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    19
  show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    20
  proof (rule UN_I[of "f(a := d)"])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    21
    show "f(a := d) \<in> F A" using *[OF f] .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    22
    show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    23
    proof (rule image_eqI[of _ _ "f a"])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    24
      show "f a \<in> G (f(a := d))" using **[OF f] .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    25
    qed simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    26
  qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    27
next
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    28
  fix f x assume "f \<in> F A" "x \<in> G f"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    29
  from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    30
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    31
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    32
lemma extensional_funcset_insert_eq[simp]:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    33
  assumes "a \<notin> A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    34
  shows "extensional (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    35
  apply (rule funset_eq_UN_fun_upd_I)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    36
  using assms
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    37
  by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    38
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    39
lemma finite_extensional_funcset[simp, intro]:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    40
  assumes "finite A" "finite B"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    41
  shows "finite (extensional A \<inter> (A \<rightarrow> B))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    42
  using assms by induct auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    43
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    44
lemma finite_PiE[simp, intro]:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    45
  assumes fin: "finite A" "\<And>i. i \<in> A \<Longrightarrow> finite (B i)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    46
  shows "finite (Pi\<^isub>E A B)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    47
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    48
  have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    49
  show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    50
    using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    51
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    52
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    53
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    54
lemma countably_additiveI[case_names countably]:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    55
  assumes "\<And>A. \<lbrakk> range A \<subseteq> M ; disjoint_family A ; (\<Union>i. A i) \<in> M\<rbrakk> \<Longrightarrow> (\<Sum>n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    56
  shows "countably_additive M \<mu>"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    57
  using assms unfolding countably_additive_def by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    58
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    59
lemma convex_le_Inf_differential:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    60
  fixes f :: "real \<Rightarrow> real"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    61
  assumes "convex_on I f"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    62
  assumes "x \<in> interior I" "y \<in> I"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    63
  shows "f y \<ge> f x + Inf ((\<lambda>t. (f x - f t) / (x - t)) ` ({x<..} \<inter> I)) * (y - x)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    64
    (is "_ \<ge> _ + Inf (?F x) * (y - x)")
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    65
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    66
  show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    67
  proof (cases rule: linorder_cases)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    68
    assume "x < y"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    69
    moreover
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    70
    have "open (interior I)" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    71
    from openE[OF this `x \<in> interior I`] guess e . note e = this
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    72
    moreover def t \<equiv> "min (x + e / 2) ((x + y) / 2)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    73
    ultimately have "x < t" "t < y" "t \<in> ball x e"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    74
      by (auto simp: dist_real_def field_simps split: split_min)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    75
    with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    76
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    77
    have "open (interior I)" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    78
    from openE[OF this `x \<in> interior I`] guess e .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    79
    moreover def K \<equiv> "x - e / 2"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    80
    with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: dist_real_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    81
    ultimately have "K \<in> I" "K < x" "x \<in> I"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    82
      using interior_subset[of I] `x \<in> interior I` by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    83
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    84
    have "Inf (?F x) \<le> (f x - f y) / (x - y)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    85
    proof (rule Inf_lower2)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    86
      show "(f x - f t) / (x - t) \<in> ?F x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    87
        using `t \<in> I` `x < t` by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    88
      show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    89
        using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` by (rule convex_on_diff)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    90
    next
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    91
      fix y assume "y \<in> ?F x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    92
      with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    93
      show "(f K - f x) / (K - x) \<le> y" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    94
    qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    95
    then show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    96
      using `x < y` by (simp add: field_simps)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    97
  next
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    98
    assume "y < x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    99
    moreover
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   100
    have "open (interior I)" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   101
    from openE[OF this `x \<in> interior I`] guess e . note e = this
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   102
    moreover def t \<equiv> "x + e / 2"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   103
    ultimately have "x < t" "t \<in> ball x e"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   104
      by (auto simp: dist_real_def field_simps)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   105
    with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   106
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   107
    have "(f x - f y) / (x - y) \<le> Inf (?F x)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   108
    proof (rule Inf_greatest)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   109
      have "(f x - f y) / (x - y) = (f y - f x) / (y - x)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   110
        using `y < x` by (auto simp: field_simps)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   111
      also
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   112
      fix z  assume "z \<in> ?F x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   113
      with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   114
      have "(f y - f x) / (y - x) \<le> z" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   115
      finally show "(f x - f y) / (x - y) \<le> z" .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   116
    next
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   117
      have "open (interior I)" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   118
      from openE[OF this `x \<in> interior I`] guess e . note e = this
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   119
      then have "x + e / 2 \<in> ball x e" by (auto simp: dist_real_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   120
      with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   121
      then show "?F x \<noteq> {}" by blast
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   122
    qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   123
    then show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   124
      using `y < x` by (simp add: field_simps)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   125
  qed simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   126
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   127
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   128
lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   129
  by (rule measure_eqI) (auto simp: emeasure_distr)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   130
45777
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   131
locale prob_space = finite_measure +
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   132
  assumes emeasure_space_1: "emeasure M (space M) = 1"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   133
45777
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   134
lemma prob_spaceI[Pure.intro!]:
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   135
  assumes *: "emeasure M (space M) = 1"
45777
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   136
  shows "prob_space M"
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   137
proof -
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   138
  interpret finite_measure M
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   139
  proof
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   140
    show "emeasure M (space M) \<noteq> \<infinity>" using * by simp 
45777
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   141
  qed
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   142
  show "prob_space M" by default fact
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   143
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   144
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   145
abbreviation (in prob_space) "events \<equiv> sets M"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   146
abbreviation (in prob_space) "prob \<equiv> measure M"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   147
abbreviation (in prob_space) "random_variable M' X \<equiv> X \<in> measurable M M'"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   148
abbreviation (in prob_space) "expectation \<equiv> integral\<^isup>L M"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   149
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   150
lemma (in prob_space) prob_space_distr:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   151
  assumes f: "f \<in> measurable M M'" shows "prob_space (distr M M' f)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   152
proof (rule prob_spaceI)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   153
  have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   154
  with f show "emeasure (distr M M' f) (space (distr M M' f)) = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   155
    by (auto simp: emeasure_distr emeasure_space_1)
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   156
qed
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   157
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   158
lemma (in prob_space) prob_space: "prob (space M) = 1"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   159
  using emeasure_space_1 unfolding measure_def by (simp add: one_ereal_def)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   160
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   161
lemma (in prob_space) prob_le_1[simp, intro]: "prob A \<le> 1"
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   162
  using bounded_measure[of A] by (simp add: prob_space)
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   163
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   164
lemma (in prob_space) not_empty: "space M \<noteq> {}"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   165
  using prob_space by auto
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   166
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   167
lemma (in prob_space) measure_le_1: "emeasure M X \<le> 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   168
  using emeasure_space[of M X] by (simp add: emeasure_space_1)
42950
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 42902
diff changeset
   169
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   170
lemma (in prob_space) AE_I_eq_1:
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   171
  assumes "emeasure M {x\<in>space M. P x} = 1" "{x\<in>space M. P x} \<in> sets M"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   172
  shows "AE x in M. P x"
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   173
proof (rule AE_I)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   174
  show "emeasure M (space M - {x \<in> space M. P x}) = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   175
    using assms emeasure_space_1 by (simp add: emeasure_compl)
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   176
qed (insert assms, auto)
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   177
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   178
lemma (in prob_space) prob_compl:
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   179
  assumes A: "A \<in> events"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   180
  shows "prob (space M - A) = 1 - prob A"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   181
  using finite_measure_compl[OF A] by (simp add: prob_space)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   182
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   183
lemma (in prob_space) AE_in_set_eq_1:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   184
  assumes "A \<in> events" shows "(AE x in M. x \<in> A) \<longleftrightarrow> prob A = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   185
proof
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   186
  assume ae: "AE x in M. x \<in> A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   187
  have "{x \<in> space M. x \<in> A} = A" "{x \<in> space M. x \<notin> A} = space M - A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   188
    using `A \<in> events`[THEN sets_into_space] by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   189
  with AE_E2[OF ae] `A \<in> events` have "1 - emeasure M A = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   190
    by (simp add: emeasure_compl emeasure_space_1)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   191
  then show "prob A = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   192
    using `A \<in> events` by (simp add: emeasure_eq_measure one_ereal_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   193
next
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   194
  assume prob: "prob A = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   195
  show "AE x in M. x \<in> A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   196
  proof (rule AE_I)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   197
    show "{x \<in> space M. x \<notin> A} \<subseteq> space M - A" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   198
    show "emeasure M (space M - A) = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   199
      using `A \<in> events` prob
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   200
      by (simp add: prob_compl emeasure_space_1 emeasure_eq_measure one_ereal_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   201
    show "space M - A \<in> events"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   202
      using `A \<in> events` by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   203
  qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   204
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   205
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   206
lemma (in prob_space) AE_False: "(AE x in M. False) \<longleftrightarrow> False"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   207
proof
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   208
  assume "AE x in M. False"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   209
  then have "AE x in M. x \<in> {}" by simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   210
  then show False
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   211
    by (subst (asm) AE_in_set_eq_1) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   212
qed simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   213
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   214
lemma (in prob_space) AE_prob_1:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   215
  assumes "prob A = 1" shows "AE x in M. x \<in> A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   216
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   217
  from `prob A = 1` have "A \<in> events"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   218
    by (metis measure_notin_sets zero_neq_one)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   219
  with AE_in_set_eq_1 assms show ?thesis by simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   220
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   221
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   222
lemma (in prob_space) prob_space_increasing: "increasing M prob"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   223
  by (auto intro!: finite_measure_mono simp: increasing_def)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   224
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   225
lemma (in prob_space) prob_zero_union:
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   226
  assumes "s \<in> events" "t \<in> events" "prob t = 0"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   227
  shows "prob (s \<union> t) = prob s"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   228
using assms
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   229
proof -
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   230
  have "prob (s \<union> t) \<le> prob s"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   231
    using finite_measure_subadditive[of s t] assms by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   232
  moreover have "prob (s \<union> t) \<ge> prob s"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   233
    using assms by (blast intro: finite_measure_mono)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   234
  ultimately show ?thesis by simp
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   235
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   236
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   237
lemma (in prob_space) prob_eq_compl:
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   238
  assumes "s \<in> events" "t \<in> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   239
  assumes "prob (space M - s) = prob (space M - t)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   240
  shows "prob s = prob t"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   241
  using assms prob_compl by auto
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   242
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   243
lemma (in prob_space) prob_one_inter:
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   244
  assumes events:"s \<in> events" "t \<in> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   245
  assumes "prob t = 1"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   246
  shows "prob (s \<inter> t) = prob s"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   247
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   248
  have "prob ((space M - s) \<union> (space M - t)) = prob (space M - s)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   249
    using events assms  prob_compl[of "t"] by (auto intro!: prob_zero_union)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   250
  also have "(space M - s) \<union> (space M - t) = space M - (s \<inter> t)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   251
    by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   252
  finally show "prob (s \<inter> t) = prob s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   253
    using events by (auto intro!: prob_eq_compl[of "s \<inter> t" s])
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   254
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   255
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   256
lemma (in prob_space) prob_eq_bigunion_image:
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   257
  assumes "range f \<subseteq> events" "range g \<subseteq> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   258
  assumes "disjoint_family f" "disjoint_family g"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   259
  assumes "\<And> n :: nat. prob (f n) = prob (g n)"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   260
  shows "(prob (\<Union> i. f i) = prob (\<Union> i. g i))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   261
using assms
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   262
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   263
  have a: "(\<lambda> i. prob (f i)) sums (prob (\<Union> i. f i))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   264
    by (rule finite_measure_UNION[OF assms(1,3)])
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   265
  have b: "(\<lambda> i. prob (g i)) sums (prob (\<Union> i. g i))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   266
    by (rule finite_measure_UNION[OF assms(2,4)])
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   267
  show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   268
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   269
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   270
lemma (in prob_space) prob_countably_zero:
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   271
  assumes "range c \<subseteq> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   272
  assumes "\<And> i. prob (c i) = 0"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   273
  shows "prob (\<Union> i :: nat. c i) = 0"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   274
proof (rule antisym)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   275
  show "prob (\<Union> i :: nat. c i) \<le> 0"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   276
    using finite_measure_subadditive_countably[OF assms(1)] by (simp add: assms(2))
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   277
qed (simp add: measure_nonneg)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   278
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   279
lemma (in prob_space) prob_equiprobable_finite_unions:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   280
  assumes "s \<in> events"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   281
  assumes s_finite: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   282
  assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   283
  shows "prob s = real (card s) * prob {SOME x. x \<in> s}"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   284
proof (cases "s = {}")
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   285
  case False hence "\<exists> x. x \<in> s" by blast
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   286
  from someI_ex[OF this] assms
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   287
  have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   288
  have "prob s = (\<Sum> x \<in> s. prob {x})"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   289
    using finite_measure_eq_setsum_singleton[OF s_finite] by simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   290
  also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   291
  also have "\<dots> = real (card s) * prob {(SOME x. x \<in> s)}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   292
    using setsum_constant assms by (simp add: real_eq_of_nat)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   293
  finally show ?thesis by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   294
qed simp
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   295
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   296
lemma (in prob_space) prob_real_sum_image_fn:
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   297
  assumes "e \<in> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   298
  assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   299
  assumes "finite s"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   300
  assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   301
  assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   302
  shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   303
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   304
  have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   305
    using `e \<in> events` sets_into_space upper by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   306
  hence "prob e = prob (\<Union> i \<in> s. e \<inter> f i)" by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   307
  also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
   308
  proof (rule finite_measure_finite_Union)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   309
    show "finite s" by fact
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   310
    show "(\<lambda>i. e \<inter> f i)`s \<subseteq> events" using assms(2) by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   311
    show "disjoint_family_on (\<lambda>i. e \<inter> f i) s"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   312
      using disjoint by (auto simp: disjoint_family_on_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   313
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   314
  finally show ?thesis .
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   315
qed
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   316
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   317
lemma (in prob_space) expectation_less:
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   318
  assumes [simp]: "integrable M X"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   319
  assumes gt: "\<forall>x\<in>space M. X x < b"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   320
  shows "expectation X < b"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   321
proof -
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   322
  have "expectation X < expectation (\<lambda>x. b)"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   323
    using gt emeasure_space_1
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 43339
diff changeset
   324
    by (intro integral_less_AE_space) auto
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   325
  then show ?thesis using prob_space by simp
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   326
qed
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   327
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   328
lemma (in prob_space) expectation_greater:
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   329
  assumes [simp]: "integrable M X"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   330
  assumes gt: "\<forall>x\<in>space M. a < X x"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   331
  shows "a < expectation X"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   332
proof -
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   333
  have "expectation (\<lambda>x. a) < expectation X"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   334
    using gt emeasure_space_1
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 43339
diff changeset
   335
    by (intro integral_less_AE_space) auto
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   336
  then show ?thesis using prob_space by simp
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   337
qed
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   338
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   339
lemma (in prob_space) jensens_inequality:
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   340
  fixes a b :: real
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   341
  assumes X: "integrable M X" "X ` space M \<subseteq> I"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   342
  assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   343
  assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   344
  shows "q (expectation X) \<le> expectation (\<lambda>x. q (X x))"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   345
proof -
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 45934
diff changeset
   346
  let ?F = "\<lambda>x. Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))"
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   347
  from not_empty X(2) have "I \<noteq> {}" by auto
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   348
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   349
  from I have "open I" by auto
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   350
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   351
  note I
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   352
  moreover
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   353
  { assume "I \<subseteq> {a <..}"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   354
    with X have "a < expectation X"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   355
      by (intro expectation_greater) auto }
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   356
  moreover
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   357
  { assume "I \<subseteq> {..< b}"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   358
    with X have "expectation X < b"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   359
      by (intro expectation_less) auto }
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   360
  ultimately have "expectation X \<in> I"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   361
    by (elim disjE)  (auto simp: subset_eq)
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   362
  moreover
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   363
  { fix y assume y: "y \<in> I"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   364
    with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   365
      by (auto intro!: Sup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) }
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   366
  ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   367
    by simp
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   368
  also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   369
  proof (rule Sup_least)
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   370
    show "(\<lambda>x. q x + ?F x * (expectation X - x)) ` I \<noteq> {}"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   371
      using `I \<noteq> {}` by auto
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   372
  next
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   373
    fix k assume "k \<in> (\<lambda>x. q x + ?F x * (expectation X - x)) ` I"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   374
    then guess x .. note x = this
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   375
    have "q x + ?F x * (expectation X  - x) = expectation (\<lambda>w. q x + ?F x * (X w - x))"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   376
      using prob_space by (simp add: X)
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   377
    also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   378
      using `x \<in> I` `open I` X(2)
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   379
      by (intro integral_mono integral_add integral_cmult integral_diff
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   380
                lebesgue_integral_const X q convex_le_Inf_differential)
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   381
         (auto simp: interior_open)
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   382
    finally show "k \<le> expectation (\<lambda>w. q (X w))" using x by auto
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   383
  qed
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   384
  finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" .
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   385
qed
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   386
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   387
lemma (in prob_space) prob_x_eq_1_imp_prob_y_eq_0:
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   388
  assumes "{x} \<in> events"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   389
  assumes "prob {x} = 1"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   390
  assumes "{y} \<in> events"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   391
  assumes "y \<noteq> x"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   392
  shows "prob {y} = 0"
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   393
  using prob_one_inter[of "{y}" "{x}"] assms by auto
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   394
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   395
lemma (in prob_space) joint_distribution_Times_le_fst:
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   396
  "random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   397
    \<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"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   398
  by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   399
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   400
lemma (in prob_space) joint_distribution_Times_le_snd:
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   401
  "random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   402
    \<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^isub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MY Y) B"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   403
  by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   404
45777
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   405
locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   406
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   407
sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^isub>M M2"
45777
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   408
proof
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   409
  show "emeasure (M1 \<Otimes>\<^isub>M M2) (space (M1 \<Otimes>\<^isub>M M2)) = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   410
    by (simp add: emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
45777
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   411
qed
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   412
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   413
locale product_prob_space = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +
45777
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   414
  fixes I :: "'i set"
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   415
  assumes prob_space: "\<And>i. prob_space (M i)"
42988
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   416
45777
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   417
sublocale product_prob_space \<subseteq> M: prob_space "M i" for i
42988
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   418
  by (rule prob_space)
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   419
45777
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   420
locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I
42988
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   421
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   422
sublocale finite_product_prob_space \<subseteq> prob_space "\<Pi>\<^isub>M i\<in>I. M i"
45777
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   423
proof
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   424
  show "emeasure (\<Pi>\<^isub>M i\<in>I. M i) (space (\<Pi>\<^isub>M i\<in>I. M i)) = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   425
    by (simp add: measure_times M.emeasure_space_1 setprod_1 space_PiM)
45777
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   426
qed
42988
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   427
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   428
lemma (in finite_product_prob_space) prob_times:
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   429
  assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets (M i)"
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   430
  shows "prob (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))"
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   431
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   432
  have "ereal (measure (\<Pi>\<^isub>M i\<in>I. M i) (\<Pi>\<^isub>E i\<in>I. X i)) = emeasure (\<Pi>\<^isub>M i\<in>I. M i) (\<Pi>\<^isub>E i\<in>I. X i)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   433
    using X by (simp add: emeasure_eq_measure)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   434
  also have "\<dots> = (\<Prod>i\<in>I. emeasure (M i) (X i))"
42988
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   435
    using measure_times X by simp
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   436
  also have "\<dots> = ereal (\<Prod>i\<in>I. measure (M i) (X i))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   437
    using X by (simp add: M.emeasure_eq_measure setprod_ereal)
42859
d9dfc733f25c add product of probability spaces with finite cardinality
hoelzl
parents: 42858
diff changeset
   438
  finally show ?thesis by simp
d9dfc733f25c add product of probability spaces with finite cardinality
hoelzl
parents: 42858
diff changeset
   439
qed
d9dfc733f25c add product of probability spaces with finite cardinality
hoelzl
parents: 42858
diff changeset
   440
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   441
section {* Distributions *}
42892
a61e30bfd0bc add lemma prob_finite_product
hoelzl
parents: 42860
diff changeset
   442
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   443
definition "distributed M N X f \<longleftrightarrow> distr M N X = density N f \<and> 
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   444
  f \<in> borel_measurable N \<and> (AE x in N. 0 \<le> f x) \<and> X \<in> measurable M N"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   445
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   446
lemma
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   447
  shows distributed_distr_eq_density: "distributed M N X f \<Longrightarrow> distr M N X = density N f"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   448
    and distributed_measurable: "distributed M N X f \<Longrightarrow> X \<in> measurable M N"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   449
    and distributed_borel_measurable: "distributed M N X f \<Longrightarrow> f \<in> borel_measurable N"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   450
    and distributed_AE: "distributed M N X f \<Longrightarrow> (AE x in N. 0 \<le> f x)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   451
  by (simp_all add: distributed_def)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39096
diff changeset
   452
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   453
lemma
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   454
  shows distributed_real_measurable: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> f \<in> borel_measurable N"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   455
    and distributed_real_AE: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> (AE x in N. 0 \<le> f x)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   456
  by (simp_all add: distributed_def borel_measurable_ereal_iff)
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   457
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   458
lemma distributed_count_space:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   459
  assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   460
  shows "P a = emeasure M (X -` {a} \<inter> space M)"
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39096
diff changeset
   461
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   462
  have "emeasure M (X -` {a} \<inter> space M) = emeasure (distr M (count_space A) X) {a}"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   463
    using X a A by (simp add: distributed_measurable emeasure_distr)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   464
  also have "\<dots> = emeasure (density (count_space A) P) {a}"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   465
    using X by (simp add: distributed_distr_eq_density)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   466
  also have "\<dots> = (\<integral>\<^isup>+x. P a * indicator {a} x \<partial>count_space A)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   467
    using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: positive_integral_cong)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   468
  also have "\<dots> = P a"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   469
    using X a by (subst positive_integral_cmult_indicator) (auto simp: distributed_def one_ereal_def[symmetric] AE_count_space)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   470
  finally show ?thesis ..
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39091
diff changeset
   471
qed
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   472
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   473
lemma distributed_cong_density:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   474
  "(AE x in N. f x = g x) \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> f \<in> borel_measurable N \<Longrightarrow>
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   475
    distributed M N X f \<longleftrightarrow> distributed M N X g"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   476
  by (auto simp: distributed_def intro!: density_cong)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   477
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   478
lemma subdensity:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   479
  assumes T: "T \<in> measurable P Q"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   480
  assumes f: "distributed M P X f"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   481
  assumes g: "distributed M Q Y g"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   482
  assumes Y: "Y = T \<circ> X"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   483
  shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   484
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   485
  have "{x\<in>space Q. g x = 0} \<in> null_sets (distr M Q (T \<circ> X))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   486
    using g Y by (auto simp: null_sets_density_iff distributed_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   487
  also have "distr M Q (T \<circ> X) = distr (distr M P X) Q T"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   488
    using T f[THEN distributed_measurable] by (rule distr_distr[symmetric])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   489
  finally have "T -` {x\<in>space Q. g x = 0} \<inter> space P \<in> null_sets (distr M P X)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   490
    using T by (subst (asm) null_sets_distr_iff) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   491
  also have "T -` {x\<in>space Q. g x = 0} \<inter> space P = {x\<in>space P. g (T x) = 0}"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   492
    using T by (auto dest: measurable_space)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   493
  finally show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   494
    using f g by (auto simp add: null_sets_density_iff distributed_def)
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   495
qed
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   496
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   497
lemma subdensity_real:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   498
  fixes g :: "'a \<Rightarrow> real" and f :: "'b \<Rightarrow> real"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   499
  assumes T: "T \<in> measurable P Q"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   500
  assumes f: "distributed M P X f"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   501
  assumes g: "distributed M Q Y g"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   502
  assumes Y: "Y = T \<circ> X"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   503
  shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   504
  using subdensity[OF T, of M X "\<lambda>x. ereal (f x)" Y "\<lambda>x. ereal (g x)"] assms by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   505
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   506
lemma distributed_integral:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   507
  "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>x. f x * g x \<partial>N) = (\<integral>x. g (X x) \<partial>M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   508
  by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   509
                 distributed_distr_eq_density[symmetric] integral_density[symmetric] integral_distr)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   510
  
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   511
lemma distributed_transform_integral:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   512
  assumes Px: "distributed M N X Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   513
  assumes "distributed M P Y Py"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   514
  assumes Y: "Y = T \<circ> X" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   515
  shows "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. Px x * f (T x) \<partial>N)"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   516
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   517
  have "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. f (Y x) \<partial>M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   518
    by (rule distributed_integral) fact+
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   519
  also have "\<dots> = (\<integral>x. f (T (X x)) \<partial>M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   520
    using Y by simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   521
  also have "\<dots> = (\<integral>x. Px x * f (T x) \<partial>N)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   522
    using measurable_comp[OF T f] Px by (intro distributed_integral[symmetric]) (auto simp: comp_def)
45777
c36637603821 remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents: 45712
diff changeset
   523
  finally show ?thesis .
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39091
diff changeset
   524
qed
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   525
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   526
lemma distributed_marginal_eq_joint:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   527
  assumes T: "sigma_finite_measure T"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   528
  assumes S: "sigma_finite_measure S"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   529
  assumes Px: "distributed M S X Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   530
  assumes Py: "distributed M T Y Py"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   531
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   532
  shows "AE y in T. Py y = (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   533
proof (rule sigma_finite_measure.density_unique[OF T])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   534
  interpret ST: pair_sigma_finite S T using S T unfolding pair_sigma_finite_def by simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   535
  show "Py \<in> borel_measurable T" "AE y in T. 0 \<le> Py y"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   536
    "(\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S) \<in> borel_measurable T" "AE y in T. 0 \<le> \<integral>\<^isup>+ x. Pxy (x, y) \<partial>S"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   537
    using Pxy[THEN distributed_borel_measurable]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   538
    by (auto intro!: Py[THEN distributed_borel_measurable] Py[THEN distributed_AE]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   539
                     ST.positive_integral_snd_measurable' positive_integral_positive)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   540
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   541
  show "density T Py = density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   542
  proof (rule measure_eqI)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   543
    fix A assume A: "A \<in> sets (density T Py)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   544
    have *: "\<And>x y. x \<in> space S \<Longrightarrow> indicator (space S \<times> A) (x, y) = indicator A y"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   545
      by (auto simp: indicator_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   546
    have "emeasure (density T Py) A = emeasure (distr M T Y) A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   547
      unfolding Py[THEN distributed_distr_eq_density] ..
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   548
    also have "\<dots> = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (space S \<times> A)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   549
      using A Px Py Pxy
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   550
      by (subst (1 2) emeasure_distr)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   551
         (auto dest: measurable_space distributed_measurable intro!: arg_cong[where f="emeasure M"])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   552
    also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (space S \<times> A)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   553
      unfolding Pxy[THEN distributed_distr_eq_density] ..
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   554
    also have "\<dots> = (\<integral>\<^isup>+ x. Pxy x * indicator (space S \<times> A) x \<partial>(S \<Otimes>\<^isub>M T))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   555
      using A Pxy by (simp add: emeasure_density distributed_borel_measurable)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   556
    also have "\<dots> = (\<integral>\<^isup>+y. \<integral>\<^isup>+x. Pxy (x, y) * indicator (space S \<times> A) (x, y) \<partial>S \<partial>T)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   557
      using A Pxy
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   558
      by (subst ST.positive_integral_snd_measurable) (simp_all add: emeasure_density distributed_borel_measurable)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   559
    also have "\<dots> = (\<integral>\<^isup>+y. (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S) * indicator A y \<partial>T)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   560
      using measurable_comp[OF measurable_Pair1[OF measurable_identity] distributed_borel_measurable[OF Pxy]]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   561
      using distributed_borel_measurable[OF Pxy] distributed_AE[OF Pxy, THEN ST.AE_pair]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   562
      by (subst (asm) ST.AE_commute) (auto intro!: positive_integral_cong_AE positive_integral_multc cong: positive_integral_cong simp: * comp_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   563
    also have "\<dots> = emeasure (density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)) A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   564
      using A by (intro emeasure_density[symmetric])  (auto intro!: ST.positive_integral_snd_measurable' Pxy[THEN distributed_borel_measurable])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   565
    finally show "emeasure (density T Py) A = emeasure (density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)) A" .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   566
  qed simp
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   567
qed
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   568
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   569
lemma (in prob_space) distr_marginal1:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   570
  fixes Pxy :: "('b \<times> 'c) \<Rightarrow> real"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   571
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   572
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   573
  defines "Px \<equiv> \<lambda>x. real (\<integral>\<^isup>+z. Pxy (x, z) \<partial>T)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   574
  shows "distributed M S X Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   575
  unfolding distributed_def
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   576
proof safe
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   577
  interpret S: sigma_finite_measure S by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   578
  interpret T: sigma_finite_measure T by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   579
  interpret ST: pair_sigma_finite S T by default
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   580
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   581
  have XY: "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   582
    using Pxy by (rule distributed_measurable)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   583
  then show X: "X \<in> measurable M S"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   584
    unfolding measurable_pair_iff by (simp add: comp_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   585
  from XY have Y: "Y \<in> measurable M T"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   586
    unfolding measurable_pair_iff by (simp add: comp_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   587
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   588
  from Pxy show borel: "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   589
    by (auto intro!: ST.positive_integral_fst_measurable borel_measurable_real_of_ereal dest!: distributed_real_measurable simp: Px_def)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39096
diff changeset
   590
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   591
  interpret Pxy: prob_space "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   592
    using XY by (rule prob_space_distr)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   593
  have "(\<integral>\<^isup>+ x. max 0 (ereal (- Pxy x)) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>\<^isup>+ x. 0 \<partial>(S \<Otimes>\<^isub>M T))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   594
    using Pxy
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   595
    by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_real_measurable distributed_real_AE)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   596
  then have Pxy_integrable: "integrable (S \<Otimes>\<^isub>M T) Pxy"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   597
    using Pxy Pxy.emeasure_space_1
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   598
    by (simp add: integrable_def emeasure_density positive_integral_max_0 distributed_def borel_measurable_ereal_iff cong: positive_integral_cong)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   599
    
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   600
  show "distr M S X = density S Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   601
  proof (rule measure_eqI)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   602
    fix A assume A: "A \<in> sets (distr M S X)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   603
    with X Y XY have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   604
      by (auto simp add: emeasure_distr
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   605
               intro!: arg_cong[where f="emeasure M"] dest: measurable_space)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   606
    also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (A \<times> space T)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   607
      using Pxy by (simp add: distributed_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   608
    also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   609
      using A borel Pxy
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   610
      by (simp add: emeasure_density ST.positive_integral_fst_measurable(2)[symmetric] distributed_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   611
    also have "\<dots> = \<integral>\<^isup>+ x. ereal (Px x) * indicator A x \<partial>S"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   612
      apply (rule positive_integral_cong_AE)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   613
      using Pxy[THEN distributed_real_AE, THEN ST.AE_pair] ST.integrable_fst_measurable(1)[OF Pxy_integrable] AE_space
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   614
    proof eventually_elim
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   615
      fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)" and i: "integrable T (\<lambda>y. Pxy (x, y))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   616
      moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   617
        by (auto simp: indicator_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   618
      ultimately have "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T) =
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   619
          (\<integral>\<^isup>+ y. ereal (Pxy (x, y)) \<partial>T) * indicator A x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   620
        using Pxy[THEN distributed_real_measurable] by (simp add: eq positive_integral_multc measurable_Pair2 cong: positive_integral_cong)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   621
      also have "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) \<partial>T) = Px x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   622
        using i by (simp add: Px_def ereal_real integrable_def positive_integral_positive)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   623
      finally show "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T) = ereal (Px x) * indicator A x" .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   624
    qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   625
    finally show "emeasure (distr M S X) A = emeasure (density S Px) A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   626
      using A borel Pxy by (simp add: emeasure_density)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   627
  qed simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   628
  
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   629
  show "AE x in S. 0 \<le> ereal (Px x)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   630
    by (simp add: Px_def positive_integral_positive real_of_ereal_pos)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   631
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   632
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   633
definition
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   634
  "simple_distributed M X f \<longleftrightarrow> distributed M (count_space (X`space M)) X (\<lambda>x. ereal (f x)) \<and>
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   635
    finite (X`space M)"
42902
e8dbf90a2f3b Add restricted borel measure to {0 .. 1}
hoelzl
parents: 42892
diff changeset
   636
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   637
lemma simple_distributed:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   638
  "simple_distributed M X Px \<Longrightarrow> distributed M (count_space (X`space M)) X Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   639
  unfolding simple_distributed_def by auto
42902
e8dbf90a2f3b Add restricted borel measure to {0 .. 1}
hoelzl
parents: 42892
diff changeset
   640
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   641
lemma simple_distributed_finite[dest]: "simple_distributed M X P \<Longrightarrow> finite (X`space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   642
  by (simp add: simple_distributed_def)
42902
e8dbf90a2f3b Add restricted borel measure to {0 .. 1}
hoelzl
parents: 42892
diff changeset
   643
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   644
lemma (in prob_space) distributed_simple_function_superset:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   645
  assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X -` {x} \<inter> space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   646
  assumes A: "X`space M \<subseteq> A" "finite A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   647
  defines "S \<equiv> count_space A" and "P' \<equiv> (\<lambda>x. if x \<in> X`space M then P x else 0)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   648
  shows "distributed M S X P'"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   649
  unfolding distributed_def
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   650
proof safe
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   651
  show "(\<lambda>x. ereal (P' x)) \<in> borel_measurable S" unfolding S_def by simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   652
  show "AE x in S. 0 \<le> ereal (P' x)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   653
    using X by (auto simp: S_def P'_def simple_distributed_def intro!: measure_nonneg)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   654
  show "distr M S X = density S P'"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   655
  proof (rule measure_eqI_finite)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   656
    show "sets (distr M S X) = Pow A" "sets (density S P') = Pow A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   657
      using A unfolding S_def by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   658
    show "finite A" by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   659
    fix a assume a: "a \<in> A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   660
    then have "a \<notin> X`space M \<Longrightarrow> X -` {a} \<inter> space M = {}" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   661
    with A a X have "emeasure (distr M S X) {a} = P' a"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   662
      by (subst emeasure_distr)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   663
         (auto simp add: S_def P'_def simple_functionD emeasure_eq_measure
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   664
               intro!: arg_cong[where f=prob])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   665
    also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' a) * indicator {a} x \<partial>S)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   666
      using A X a
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   667
      by (subst positive_integral_cmult_indicator)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   668
         (auto simp: S_def P'_def simple_distributed_def simple_functionD measure_nonneg)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   669
    also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' x) * indicator {a} x \<partial>S)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   670
      by (auto simp: indicator_def intro!: positive_integral_cong)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   671
    also have "\<dots> = emeasure (density S P') {a}"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   672
      using a A by (intro emeasure_density[symmetric]) (auto simp: S_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   673
    finally show "emeasure (distr M S X) {a} = emeasure (density S P') {a}" .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   674
  qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   675
  show "random_variable S X"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   676
    using X(1) A by (auto simp: measurable_def simple_functionD S_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   677
qed
42902
e8dbf90a2f3b Add restricted borel measure to {0 .. 1}
hoelzl
parents: 42892
diff changeset
   678
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   679
lemma (in prob_space) simple_distributedI:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   680
  assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X -` {x} \<inter> space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   681
  shows "simple_distributed M X P"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   682
  unfolding simple_distributed_def
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   683
proof
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   684
  have "distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (if x \<in> X`space M then P x else 0))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   685
    (is "?A")
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   686
    using simple_functionD[OF X(1)] by (intro distributed_simple_function_superset[OF X]) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   687
  also have "?A \<longleftrightarrow> distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (P x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   688
    by (rule distributed_cong_density) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   689
  finally show "\<dots>" .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   690
qed (rule simple_functionD[OF X(1)])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   691
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   692
lemma simple_distributed_joint_finite:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   693
  assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   694
  shows "finite (X ` space M)" "finite (Y ` space M)"
42902
e8dbf90a2f3b Add restricted borel measure to {0 .. 1}
hoelzl
parents: 42892
diff changeset
   695
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   696
  have "finite ((\<lambda>x. (X x, Y x)) ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   697
    using X by (auto simp: simple_distributed_def simple_functionD)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   698
  then have "finite (fst ` (\<lambda>x. (X x, Y x)) ` space M)" "finite (snd ` (\<lambda>x. (X x, Y x)) ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   699
    by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   700
  then show fin: "finite (X ` space M)" "finite (Y ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   701
    by (auto simp: image_image)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   702
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   703
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   704
lemma simple_distributed_joint2_finite:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   705
  assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   706
  shows "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   707
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   708
  have "finite ((\<lambda>x. (X x, Y x, Z x)) ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   709
    using X by (auto simp: simple_distributed_def simple_functionD)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   710
  then have "finite (fst ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   711
    "finite ((fst \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   712
    "finite ((snd \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   713
    by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   714
  then show fin: "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   715
    by (auto simp: image_image)
42902
e8dbf90a2f3b Add restricted borel measure to {0 .. 1}
hoelzl
parents: 42892
diff changeset
   716
qed
e8dbf90a2f3b Add restricted borel measure to {0 .. 1}
hoelzl
parents: 42892
diff changeset
   717
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   718
lemma simple_distributed_simple_function:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   719
  "simple_distributed M X Px \<Longrightarrow> simple_function M X"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   720
  unfolding simple_distributed_def distributed_def
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   721
  by (auto simp: simple_function_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   722
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   723
lemma simple_distributed_measure:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   724
  "simple_distributed M X P \<Longrightarrow> a \<in> X`space M \<Longrightarrow> P a = measure M (X -` {a} \<inter> space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   725
  using distributed_count_space[of M "X`space M" X P a, symmetric]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   726
  by (auto simp: simple_distributed_def measure_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   727
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   728
lemma simple_distributed_nonneg: "simple_distributed M X f \<Longrightarrow> x \<in> space M \<Longrightarrow> 0 \<le> f (X x)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   729
  by (auto simp: simple_distributed_measure measure_nonneg)
42860
b02349e70d5a add Bernoulli space
hoelzl
parents: 42859
diff changeset
   730
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   731
lemma (in prob_space) simple_distributed_joint:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   732
  assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   733
  defines "S \<equiv> count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   734
  defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x))`space M then Px x else 0)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   735
  shows "distributed M S (\<lambda>x. (X x, Y x)) P"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   736
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   737
  from simple_distributed_joint_finite[OF X, simp]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   738
  have S_eq: "S = count_space (X`space M \<times> Y`space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   739
    by (simp add: S_def pair_measure_count_space)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   740
  show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   741
    unfolding S_eq P_def
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   742
  proof (rule distributed_simple_function_superset)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   743
    show "simple_function M (\<lambda>x. (X x, Y x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   744
      using X by (rule simple_distributed_simple_function)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   745
    fix x assume "x \<in> (\<lambda>x. (X x, Y x)) ` space M"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   746
    from simple_distributed_measure[OF X this]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   747
    show "Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)" .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   748
  qed auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   749
qed
42860
b02349e70d5a add Bernoulli space
hoelzl
parents: 42859
diff changeset
   750
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   751
lemma (in prob_space) simple_distributed_joint2:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   752
  assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   753
  defines "S \<equiv> count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M) \<Otimes>\<^isub>M count_space (Z`space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   754
  defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x))`space M then Px x else 0)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   755
  shows "distributed M S (\<lambda>x. (X x, Y x, Z x)) P"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   756
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   757
  from simple_distributed_joint2_finite[OF X, simp]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   758
  have S_eq: "S = count_space (X`space M \<times> Y`space M \<times> Z`space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   759
    by (simp add: S_def pair_measure_count_space)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   760
  show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   761
    unfolding S_eq P_def
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   762
  proof (rule distributed_simple_function_superset)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   763
    show "simple_function M (\<lambda>x. (X x, Y x, Z x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   764
      using X by (rule simple_distributed_simple_function)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   765
    fix x assume "x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   766
    from simple_distributed_measure[OF X this]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   767
    show "Px x = prob ((\<lambda>x. (X x, Y x, Z x)) -` {x} \<inter> space M)" .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   768
  qed auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   769
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   770
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   771
lemma (in prob_space) simple_distributed_setsum_space:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   772
  assumes X: "simple_distributed M X f"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   773
  shows "setsum f (X`space M) = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   774
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   775
  from X have "setsum f (X`space M) = prob (\<Union>i\<in>X`space M. X -` {i} \<inter> space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   776
    by (subst finite_measure_finite_Union)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   777
       (auto simp add: disjoint_family_on_def simple_distributed_measure simple_distributed_simple_function simple_functionD
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   778
             intro!: setsum_cong arg_cong[where f="prob"])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   779
  also have "\<dots> = prob (space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   780
    by (auto intro!: arg_cong[where f=prob])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   781
  finally show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   782
    using emeasure_space_1 by (simp add: emeasure_eq_measure one_ereal_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   783
qed
42860
b02349e70d5a add Bernoulli space
hoelzl
parents: 42859
diff changeset
   784
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   785
lemma (in prob_space) distributed_marginal_eq_joint_simple:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   786
  assumes Px: "simple_function M X"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   787
  assumes Py: "simple_distributed M Y Py"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   788
  assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   789
  assumes y: "y \<in> Y`space M"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   790
  shows "Py y = (\<Sum>x\<in>X`space M. if (x, y) \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy (x, y) else 0)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   791
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   792
  note Px = simple_distributedI[OF Px refl]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   793
  have *: "\<And>f A. setsum (\<lambda>x. max 0 (ereal (f x))) A = ereal (setsum (\<lambda>x. max 0 (f x)) A)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   794
    by (simp add: setsum_ereal[symmetric] zero_ereal_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   795
  from distributed_marginal_eq_joint[OF sigma_finite_measure_count_space_finite sigma_finite_measure_count_space_finite
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   796
    simple_distributed[OF Px] simple_distributed[OF Py] simple_distributed_joint[OF Pxy],
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   797
    OF Py[THEN simple_distributed_finite] Px[THEN simple_distributed_finite]]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   798
    y Px[THEN simple_distributed_finite] Py[THEN simple_distributed_finite]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   799
    Pxy[THEN simple_distributed, THEN distributed_real_AE]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   800
  show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   801
    unfolding AE_count_space
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   802
    apply (elim ballE[where x=y])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   803
    apply (auto simp add: positive_integral_count_space_finite * intro!: setsum_cong split: split_max)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   804
    done
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   805
qed
42860
b02349e70d5a add Bernoulli space
hoelzl
parents: 42859
diff changeset
   806
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   807
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   808
lemma prob_space_uniform_measure:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   809
  assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   810
  shows "prob_space (uniform_measure M A)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   811
proof
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   812
  show "emeasure (uniform_measure M A) (space (uniform_measure M A)) = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   813
    using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)], of "space M"]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   814
    using sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   815
    by (simp add: Int_absorb2 emeasure_nonneg)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   816
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   817
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   818
lemma prob_space_uniform_count_measure: "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> prob_space (uniform_count_measure A)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   819
  by default (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def)
42860
b02349e70d5a add Bernoulli space
hoelzl
parents: 42859
diff changeset
   820
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   821
end