src/HOL/Probability/Probability_Measure.thy
author wenzelm
Thu, 18 Apr 2013 17:07:01 +0200
changeset 51717 9e7d1c139569
parent 51683 baefa3b461c2
child 53015 a1119cf551e8
permissions -rw-r--r--
simplifier uses proper Proof.context instead of historic type simpset;
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
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
    12
locale prob_space = finite_measure +
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    13
  assumes emeasure_space_1: "emeasure M (space M) = 1"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    14
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
    15
lemma prob_spaceI[Pure.intro!]:
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    16
  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
    17
  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
    18
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
    19
  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
    20
  proof
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    21
    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
    22
  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
    23
  show "prob_space M" by default fact
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    24
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    25
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    26
abbreviation (in prob_space) "events \<equiv> sets M"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    27
abbreviation (in prob_space) "prob \<equiv> measure M"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    28
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
    29
abbreviation (in prob_space) "expectation \<equiv> integral\<^isup>L M"
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    30
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    31
lemma (in prob_space) prob_space_distr:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    32
  assumes f: "f \<in> measurable M M'" shows "prob_space (distr M M' f)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    33
proof (rule prob_spaceI)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    34
  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
    35
  with f show "emeasure (distr M M' f) (space (distr M M' f)) = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    36
    by (auto simp: emeasure_distr emeasure_space_1)
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
    37
qed
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
    38
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    39
lemma (in prob_space) prob_space: "prob (space M) = 1"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    40
  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
    41
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    42
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
    43
  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
    44
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    45
lemma (in prob_space) not_empty: "space M \<noteq> {}"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    46
  using prob_space by auto
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41831
diff changeset
    47
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    48
lemma (in prob_space) measure_le_1: "emeasure M X \<le> 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    49
  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
    50
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
    51
lemma (in prob_space) AE_I_eq_1:
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    52
  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
    53
  shows "AE x in M. P x"
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
    54
proof (rule AE_I)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    55
  show "emeasure M (space M - {x \<in> space M. P x}) = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    56
    using assms emeasure_space_1 by (simp add: emeasure_compl)
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
    57
qed (insert assms, auto)
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
    58
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    59
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
    60
  assumes A: "A \<in> events"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    61
  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
    62
  using finite_measure_compl[OF A] by (simp add: prob_space)
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
    63
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    64
lemma (in prob_space) AE_in_set_eq_1:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    65
  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
    66
proof
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    67
  assume ae: "AE x in M. x \<in> A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    68
  have "{x \<in> space M. x \<in> A} = A" "{x \<in> space M. x \<notin> A} = space M - A"
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
    69
    using `A \<in> events`[THEN sets.sets_into_space] by auto
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    70
  with AE_E2[OF ae] `A \<in> events` have "1 - emeasure M A = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    71
    by (simp add: emeasure_compl emeasure_space_1)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    72
  then show "prob A = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    73
    using `A \<in> events` by (simp add: emeasure_eq_measure one_ereal_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    74
next
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    75
  assume prob: "prob A = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    76
  show "AE x in M. x \<in> A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    77
  proof (rule AE_I)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    78
    show "{x \<in> space M. x \<notin> A} \<subseteq> space M - A" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    79
    show "emeasure M (space M - A) = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    80
      using `A \<in> events` prob
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    81
      by (simp add: prob_compl emeasure_space_1 emeasure_eq_measure one_ereal_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    82
    show "space M - A \<in> events"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    83
      using `A \<in> events` by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    84
  qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    85
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    86
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    87
lemma (in prob_space) AE_False: "(AE x in M. False) \<longleftrightarrow> False"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    88
proof
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    89
  assume "AE x in M. False"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    90
  then have "AE x in M. x \<in> {}" by simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    91
  then show False
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    92
    by (subst (asm) AE_in_set_eq_1) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    93
qed simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    94
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    95
lemma (in prob_space) AE_prob_1:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    96
  assumes "prob A = 1" shows "AE x in M. x \<in> A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    97
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    98
  from `prob A = 1` have "A \<in> events"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    99
    by (metis measure_notin_sets zero_neq_one)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   100
  with AE_in_set_eq_1 assms show ?thesis by simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   101
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   102
50098
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   103
lemma (in prob_space) AE_const[simp]: "(AE x in M. P) \<longleftrightarrow> P"
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   104
  by (cases P) (auto simp: AE_False)
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   105
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   106
lemma (in prob_space) AE_contr:
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   107
  assumes ae: "AE \<omega> in M. P \<omega>" "AE \<omega> in M. \<not> P \<omega>"
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   108
  shows False
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   109
proof -
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   110
  from ae have "AE \<omega> in M. False" by eventually_elim auto
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   111
  then show False by auto
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   112
qed
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   113
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   114
lemma (in prob_space) expectation_less:
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   115
  assumes [simp]: "integrable M X"
49786
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49783
diff changeset
   116
  assumes gt: "AE x in M. X x < b"
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   117
  shows "expectation X < b"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   118
proof -
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   119
  have "expectation X < expectation (\<lambda>x. b)"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   120
    using gt emeasure_space_1
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 43339
diff changeset
   121
    by (intro integral_less_AE_space) auto
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   122
  then show ?thesis using prob_space by simp
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   123
qed
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   124
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   125
lemma (in prob_space) expectation_greater:
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   126
  assumes [simp]: "integrable M X"
49786
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49783
diff changeset
   127
  assumes gt: "AE x in M. a < X x"
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   128
  shows "a < expectation X"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   129
proof -
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   130
  have "expectation (\<lambda>x. a) < expectation X"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   131
    using gt emeasure_space_1
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 43339
diff changeset
   132
    by (intro integral_less_AE_space) auto
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   133
  then show ?thesis using prob_space by simp
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   134
qed
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   135
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   136
lemma (in prob_space) jensens_inequality:
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   137
  fixes a b :: real
49786
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49783
diff changeset
   138
  assumes X: "integrable M X" "AE x in M. X x \<in> I"
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   139
  assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   140
  assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   141
  shows "q (expectation X) \<le> expectation (\<lambda>x. q (X x))"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   142
proof -
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 45934
diff changeset
   143
  let ?F = "\<lambda>x. Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))"
49786
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49783
diff changeset
   144
  from X(2) AE_False have "I \<noteq> {}" by auto
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   145
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   146
  from I have "open I" by auto
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   147
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   148
  note I
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   149
  moreover
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   150
  { assume "I \<subseteq> {a <..}"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   151
    with X have "a < expectation X"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   152
      by (intro expectation_greater) auto }
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   153
  moreover
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   154
  { assume "I \<subseteq> {..< b}"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   155
    with X have "expectation X < b"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   156
      by (intro expectation_less) auto }
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   157
  ultimately have "expectation X \<in> I"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   158
    by (elim disjE)  (auto simp: subset_eq)
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   159
  moreover
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   160
  { fix y assume y: "y \<in> I"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   161
    with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
51475
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 50419
diff changeset
   162
      by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) }
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   163
  ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   164
    by simp
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   165
  also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
51475
ebf9d4fd00ba introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents: 50419
diff changeset
   166
  proof (rule cSup_least)
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   167
    show "(\<lambda>x. q x + ?F x * (expectation X - x)) ` I \<noteq> {}"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   168
      using `I \<noteq> {}` by auto
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   169
  next
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   170
    fix k assume "k \<in> (\<lambda>x. q x + ?F x * (expectation X - x)) ` I"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   171
    then guess x .. note x = this
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   172
    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
   173
      using prob_space by (simp add: X)
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   174
    also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   175
      using `x \<in> I` `open I` X(2)
49786
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49783
diff changeset
   176
      apply (intro integral_mono_AE integral_add integral_cmult integral_diff
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49783
diff changeset
   177
                lebesgue_integral_const X q)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49783
diff changeset
   178
      apply (elim eventually_elim1)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49783
diff changeset
   179
      apply (intro convex_le_Inf_differential)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49783
diff changeset
   180
      apply (auto simp: interior_open q)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49783
diff changeset
   181
      done
43339
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   182
    finally show "k \<le> expectation (\<lambda>w. q (X w))" using x by auto
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   183
  qed
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   184
  finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" .
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   185
qed
9ba256ad6781 jensens inequality
hoelzl
parents: 42991
diff changeset
   186
50001
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   187
subsection  {* Introduce binder for probability *}
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   188
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   189
syntax
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   190
  "_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("('\<P>'(_ in _. _'))")
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   191
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   192
translations
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   193
  "\<P>(x in M. P)" => "CONST measure M {x \<in> CONST space M. P}"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   194
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   195
definition
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   196
  "cond_prob M P Q = \<P>(\<omega> in M. P \<omega> \<and> Q \<omega>) / \<P>(\<omega> in M. Q \<omega>)"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   197
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   198
syntax
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   199
  "_conditional_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("('\<P>'(_ in _. _ \<bar>/ _'))")
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   200
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   201
translations
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   202
  "\<P>(x in M. P \<bar> Q)" => "CONST cond_prob M (\<lambda>x. P) (\<lambda>x. Q)"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   203
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   204
lemma (in prob_space) AE_E_prob:
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   205
  assumes ae: "AE x in M. P x"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   206
  obtains S where "S \<subseteq> {x \<in> space M. P x}" "S \<in> events" "prob S = 1"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   207
proof -
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   208
  from ae[THEN AE_E] guess N .
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   209
  then show thesis
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   210
    by (intro that[of "space M - N"])
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   211
       (auto simp: prob_compl prob_space emeasure_eq_measure)
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   212
qed
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   213
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   214
lemma (in prob_space) prob_neg: "{x\<in>space M. P x} \<in> events \<Longrightarrow> \<P>(x in M. \<not> P x) = 1 - \<P>(x in M. P x)"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   215
  by (auto intro!: arg_cong[where f=prob] simp add: prob_compl[symmetric])
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   216
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   217
lemma (in prob_space) prob_eq_AE:
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   218
  "(AE x in M. P x \<longleftrightarrow> Q x) \<Longrightarrow> {x\<in>space M. P x} \<in> events \<Longrightarrow> {x\<in>space M. Q x} \<in> events \<Longrightarrow> \<P>(x in M. P x) = \<P>(x in M. Q x)"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   219
  by (rule finite_measure_eq_AE) auto
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   220
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   221
lemma (in prob_space) prob_eq_0_AE:
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   222
  assumes not: "AE x in M. \<not> P x" shows "\<P>(x in M. P x) = 0"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   223
proof cases
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   224
  assume "{x\<in>space M. P x} \<in> events"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   225
  with not have "\<P>(x in M. P x) = \<P>(x in M. False)"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   226
    by (intro prob_eq_AE) auto
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   227
  then show ?thesis by simp
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   228
qed (simp add: measure_notin_sets)
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   229
50098
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   230
lemma (in prob_space) prob_Collect_eq_0:
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   231
  "{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 0 \<longleftrightarrow> (AE x in M. \<not> P x)"
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   232
  using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"] by (simp add: emeasure_eq_measure)
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   233
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   234
lemma (in prob_space) prob_Collect_eq_1:
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   235
  "{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 1 \<longleftrightarrow> (AE x in M. P x)"
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   236
  using AE_in_set_eq_1[of "{x\<in>space M. P x}"] by simp
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   237
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   238
lemma (in prob_space) prob_eq_0:
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   239
  "A \<in> sets M \<Longrightarrow> prob A = 0 \<longleftrightarrow> (AE x in M. x \<notin> A)"
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   240
  using AE_iff_measurable[OF _ refl, of M "\<lambda>x. x \<notin> A"]
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   241
  by (auto simp add: emeasure_eq_measure Int_def[symmetric])
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   242
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   243
lemma (in prob_space) prob_eq_1:
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   244
  "A \<in> sets M \<Longrightarrow> prob A = 1 \<longleftrightarrow> (AE x in M. x \<in> A)"
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   245
  using AE_in_set_eq_1[of A] by simp
98abff4a775b rules for AE and prob
hoelzl
parents: 50003
diff changeset
   246
50001
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   247
lemma (in prob_space) prob_sums:
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   248
  assumes P: "\<And>n. {x\<in>space M. P n x} \<in> events"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   249
  assumes Q: "{x\<in>space M. Q x} \<in> events"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   250
  assumes ae: "AE x in M. (\<forall>n. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n. P n x))"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   251
  shows "(\<lambda>n. \<P>(x in M. P n x)) sums \<P>(x in M. Q x)"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   252
proof -
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   253
  from ae[THEN AE_E_prob] guess S . note S = this
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   254
  then have disj: "disjoint_family (\<lambda>n. {x\<in>space M. P n x} \<inter> S)"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   255
    by (auto simp: disjoint_family_on_def)
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   256
  from S have ae_S:
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   257
    "AE x in M. x \<in> {x\<in>space M. Q x} \<longleftrightarrow> x \<in> (\<Union>n. {x\<in>space M. P n x} \<inter> S)"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   258
    "\<And>n. AE x in M. x \<in> {x\<in>space M. P n x} \<longleftrightarrow> x \<in> {x\<in>space M. P n x} \<inter> S"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   259
    using ae by (auto dest!: AE_prob_1)
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   260
  from ae_S have *:
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   261
    "\<P>(x in M. Q x) = prob (\<Union>n. {x\<in>space M. P n x} \<inter> S)"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   262
    using P Q S by (intro finite_measure_eq_AE) auto
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   263
  from ae_S have **:
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   264
    "\<And>n. \<P>(x in M. P n x) = prob ({x\<in>space M. P n x} \<inter> S)"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   265
    using P Q S by (intro finite_measure_eq_AE) auto
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   266
  show ?thesis
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   267
    unfolding * ** using S P disj
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   268
    by (intro finite_measure_UNION) auto
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   269
qed
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   270
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   271
lemma (in prob_space) cond_prob_eq_AE:
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   272
  assumes P: "AE x in M. Q x \<longrightarrow> P x \<longleftrightarrow> P' x" "{x\<in>space M. P x} \<in> events" "{x\<in>space M. P' x} \<in> events"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   273
  assumes Q: "AE x in M. Q x \<longleftrightarrow> Q' x" "{x\<in>space M. Q x} \<in> events" "{x\<in>space M. Q' x} \<in> events"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   274
  shows "cond_prob M P Q = cond_prob M P' Q'"
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   275
  using P Q
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
   276
  by (auto simp: cond_prob_def intro!: arg_cong2[where f="op /"] prob_eq_AE sets.sets_Collect_conj)
50001
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   277
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   278
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   279
lemma (in prob_space) joint_distribution_Times_le_fst:
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   280
  "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
   281
    \<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
   282
  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
   283
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   284
lemma (in prob_space) joint_distribution_Times_le_snd:
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   285
  "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
   286
    \<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
   287
  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
   288
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
   289
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
   290
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   291
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
   292
proof
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   293
  show "emeasure (M1 \<Otimes>\<^isub>M M2) (space (M1 \<Otimes>\<^isub>M M2)) = 1"
49776
199d1d5bb17e tuned product measurability
hoelzl
parents: 47694
diff changeset
   294
    by (simp add: M2.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
   295
qed
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   296
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   297
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
   298
  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
   299
  assumes prob_space: "\<And>i. prob_space (M i)"
42988
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   300
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
   301
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
   302
  by (rule prob_space)
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   303
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
   304
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
   305
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   306
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
   307
proof
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   308
  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
   309
    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
   310
qed
42988
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   311
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   312
lemma (in finite_product_prob_space) prob_times:
d8f3fc934ff6 add lemma indep_distribution_eq_measure
hoelzl
parents: 42981
diff changeset
   313
  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
   314
  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
   315
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   316
  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
   317
    using X by (simp add: emeasure_eq_measure)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   318
  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
   319
    using measure_times X by simp
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   320
  also have "\<dots> = ereal (\<Prod>i\<in>I. measure (M i) (X i))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   321
    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
   322
  finally show ?thesis by simp
d9dfc733f25c add product of probability spaces with finite cardinality
hoelzl
parents: 42858
diff changeset
   323
qed
d9dfc733f25c add product of probability spaces with finite cardinality
hoelzl
parents: 42858
diff changeset
   324
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   325
section {* Distributions *}
42892
a61e30bfd0bc add lemma prob_finite_product
hoelzl
parents: 42860
diff changeset
   326
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   327
definition "distributed M N X f \<longleftrightarrow> distr M N X = density N f \<and> 
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   328
  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
   329
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   330
lemma
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   331
  assumes "distributed M N X f"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   332
  shows distributed_distr_eq_density: "distr M N X = density N f"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   333
    and distributed_measurable: "X \<in> measurable M N"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   334
    and distributed_borel_measurable: "f \<in> borel_measurable N"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   335
    and distributed_AE: "(AE x in N. 0 \<le> f x)"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   336
  using assms by (simp_all add: distributed_def)
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   337
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   338
lemma
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   339
  assumes D: "distributed M N X f"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   340
  shows distributed_measurable'[measurable_dest]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   341
      "g \<in> measurable L M \<Longrightarrow> (\<lambda>x. X (g x)) \<in> measurable L N"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   342
    and distributed_borel_measurable'[measurable_dest]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   343
      "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   344
  using distributed_measurable[OF D] distributed_borel_measurable[OF D]
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   345
  by simp_all
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39096
diff changeset
   346
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   347
lemma
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   348
  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
   349
    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
   350
  by (simp_all add: distributed_def borel_measurable_ereal_iff)
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   351
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   352
lemma
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   353
  assumes D: "distributed M N X (\<lambda>x. ereal (f x))"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   354
  shows distributed_real_measurable'[measurable_dest]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   355
      "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   356
  using distributed_real_measurable[OF D]
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   357
  by simp_all
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   358
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   359
lemma
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   360
  assumes D: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) f"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   361
  shows joint_distributed_measurable1[measurable_dest]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   362
      "h1 \<in> measurable N M \<Longrightarrow> (\<lambda>x. X (h1 x)) \<in> measurable N S"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   363
    and joint_distributed_measurable2[measurable_dest]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   364
      "h2 \<in> measurable N M \<Longrightarrow> (\<lambda>x. Y (h2 x)) \<in> measurable N T"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   365
  using measurable_compose[OF distributed_measurable[OF D] measurable_fst]
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   366
  using measurable_compose[OF distributed_measurable[OF D] measurable_snd]
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   367
  by auto
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   368
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   369
lemma distributed_count_space:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   370
  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
   371
  shows "P a = emeasure M (X -` {a} \<inter> space M)"
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39096
diff changeset
   372
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   373
  have "emeasure M (X -` {a} \<inter> space M) = emeasure (distr M (count_space A) X) {a}"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   374
    using X a A by (simp add: emeasure_distr)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   375
  also have "\<dots> = emeasure (density (count_space A) P) {a}"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   376
    using X by (simp add: distributed_distr_eq_density)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   377
  also have "\<dots> = (\<integral>\<^isup>+x. P a * indicator {a} x \<partial>count_space A)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   378
    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
   379
  also have "\<dots> = P a"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   380
    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
   381
  finally show ?thesis ..
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39091
diff changeset
   382
qed
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   383
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   384
lemma distributed_cong_density:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   385
  "(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
   386
    distributed M N X f \<longleftrightarrow> distributed M N X g"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   387
  by (auto simp: distributed_def intro!: density_cong)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   388
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   389
lemma subdensity:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   390
  assumes T: "T \<in> measurable P Q"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   391
  assumes f: "distributed M P X f"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   392
  assumes g: "distributed M Q Y g"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   393
  assumes Y: "Y = T \<circ> X"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   394
  shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   395
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   396
  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
   397
    using g Y by (auto simp: null_sets_density_iff distributed_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   398
  also have "distr M Q (T \<circ> X) = distr (distr M P X) Q T"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   399
    using T f[THEN distributed_measurable] by (rule distr_distr[symmetric])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   400
  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
   401
    using T by (subst (asm) null_sets_distr_iff) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   402
  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
   403
    using T by (auto dest: measurable_space)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   404
  finally show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   405
    using f g by (auto simp add: null_sets_density_iff distributed_def)
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   406
qed
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35929
diff changeset
   407
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   408
lemma subdensity_real:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   409
  fixes g :: "'a \<Rightarrow> real" and f :: "'b \<Rightarrow> real"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   410
  assumes T: "T \<in> measurable P Q"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   411
  assumes f: "distributed M P X f"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   412
  assumes g: "distributed M Q Y g"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   413
  assumes Y: "Y = T \<circ> X"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   414
  shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   415
  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
   416
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   417
lemma distributed_emeasure:
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   418
  "distributed M N X f \<Longrightarrow> A \<in> sets N \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^isup>+x. f x * indicator A x \<partial>N)"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   419
  by (auto simp: distributed_AE
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   420
                 distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   421
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   422
lemma distributed_positive_integral:
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   423
  "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^isup>+x. f x * g x \<partial>N) = (\<integral>\<^isup>+x. g (X x) \<partial>M)"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   424
  by (auto simp: distributed_AE
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   425
                 distributed_distr_eq_density[symmetric] positive_integral_density[symmetric] positive_integral_distr)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   426
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   427
lemma distributed_integral:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   428
  "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)"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   429
  by (auto simp: distributed_real_AE
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   430
                 distributed_distr_eq_density[symmetric] integral_density[symmetric] integral_distr)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   431
  
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   432
lemma distributed_transform_integral:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   433
  assumes Px: "distributed M N X Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   434
  assumes "distributed M P Y Py"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   435
  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
   436
  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
   437
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   438
  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
   439
    by (rule distributed_integral) fact+
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   440
  also have "\<dots> = (\<integral>x. f (T (X x)) \<partial>M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   441
    using Y by simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   442
  also have "\<dots> = (\<integral>x. Px x * f (T x) \<partial>N)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   443
    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
   444
  finally show ?thesis .
39092
98de40859858 move lemmas to correct theory files
hoelzl
parents: 39091
diff changeset
   445
qed
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   446
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   447
lemma (in prob_space) distributed_unique:
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   448
  assumes Px: "distributed M S X Px"
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   449
  assumes Py: "distributed M S X Py"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   450
  shows "AE x in S. Px x = Py x"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   451
proof -
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   452
  interpret X: prob_space "distr M S X"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   453
    using Px by (intro prob_space_distr) simp
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   454
  have "sigma_finite_measure (distr M S X)" ..
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   455
  with sigma_finite_density_unique[of Px S Py ] Px Py
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   456
  show ?thesis
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   457
    by (auto simp: distributed_def)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   458
qed
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   459
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   460
lemma (in prob_space) distributed_jointI:
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   461
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   462
  assumes X[measurable]: "X \<in> measurable M S" and Y[measurable]: "Y \<in> measurable M T"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   463
  assumes [measurable]: "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)" and f: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> f x"
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   464
  assumes eq: "\<And>A B. A \<in> sets S \<Longrightarrow> B \<in> sets T \<Longrightarrow> 
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   465
    emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B} = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. f (x, y) * indicator B y \<partial>T) * indicator A x \<partial>S)"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   466
  shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) f"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   467
  unfolding distributed_def
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   468
proof safe
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   469
  interpret S: sigma_finite_measure S by fact
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   470
  interpret T: sigma_finite_measure T by fact
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   471
  interpret ST: pair_sigma_finite S T by default
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   472
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   473
  from ST.sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('b \<times> 'c) set" .. note F = this
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   474
  let ?E = "{a \<times> b |a b. a \<in> sets S \<and> b \<in> sets T}"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   475
  let ?P = "S \<Otimes>\<^isub>M T"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   476
  show "distr M ?P (\<lambda>x. (X x, Y x)) = density ?P f" (is "?L = ?R")
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   477
  proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of S T]])
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   478
    show "?E \<subseteq> Pow (space ?P)"
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
   479
      using sets.space_closed[of S] sets.space_closed[of T] by (auto simp: space_pair_measure)
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   480
    show "sets ?L = sigma_sets (space ?P) ?E"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   481
      by (simp add: sets_pair_measure space_pair_measure)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   482
    then show "sets ?R = sigma_sets (space ?P) ?E"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   483
      by simp
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   484
  next
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   485
    interpret L: prob_space ?L
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   486
      by (rule prob_space_distr) (auto intro!: measurable_Pair)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   487
    show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?L (F i) \<noteq> \<infinity>"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   488
      using F by (auto simp: space_pair_measure)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   489
  next
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   490
    fix E assume "E \<in> ?E"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   491
    then obtain A B where E[simp]: "E = A \<times> B"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   492
      and A[measurable]: "A \<in> sets S" and B[measurable]: "B \<in> sets T" by auto
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   493
    have "emeasure ?L E = emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B}"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   494
      by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   495
    also have "\<dots> = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   496
      using f by (auto simp add: eq positive_integral_multc intro!: positive_integral_cong)
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   497
    also have "\<dots> = emeasure ?R E"
50001
382bd3173584 add syntax and a.e.-rules for (conditional) probability on predicates
hoelzl
parents: 49795
diff changeset
   498
      by (auto simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric]
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   499
               intro!: positive_integral_cong split: split_indicator)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   500
    finally show "emeasure ?L E = emeasure ?R E" .
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   501
  qed
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   502
qed (auto simp: f)
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   503
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   504
lemma (in prob_space) distributed_swap:
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   505
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   506
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   507
  shows "distributed M (T \<Otimes>\<^isub>M S) (\<lambda>x. (Y x, X x)) (\<lambda>(x, y). Pxy (y, x))"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   508
proof -
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   509
  interpret S: sigma_finite_measure S by fact
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   510
  interpret T: sigma_finite_measure T by fact
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   511
  interpret ST: pair_sigma_finite S T by default
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   512
  interpret TS: pair_sigma_finite T S by default
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   513
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   514
  note Pxy[measurable]
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   515
  show ?thesis 
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   516
    apply (subst TS.distr_pair_swap)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   517
    unfolding distributed_def
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   518
  proof safe
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   519
    let ?D = "distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   520
    show 1: "(\<lambda>(x, y). Pxy (y, x)) \<in> borel_measurable ?D"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   521
      by auto
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   522
    with Pxy
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   523
    show "AE x in distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x)). 0 \<le> (case x of (x, y) \<Rightarrow> Pxy (y, x))"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   524
      by (subst AE_distr_iff)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   525
         (auto dest!: distributed_AE
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   526
               simp: measurable_split_conv split_beta
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51475
diff changeset
   527
               intro!: measurable_Pair)
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   528
    show 2: "random_variable (distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))) (\<lambda>x. (Y x, X x))"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   529
      using Pxy by auto
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   530
    { fix A assume A: "A \<in> sets (T \<Otimes>\<^isub>M S)"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   531
      let ?B = "(\<lambda>(x, y). (y, x)) -` A \<inter> space (S \<Otimes>\<^isub>M T)"
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
   532
      from sets.sets_into_space[OF A]
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   533
      have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   534
        emeasure M ((\<lambda>x. (X x, Y x)) -` ?B \<inter> space M)"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   535
        by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   536
      also have "\<dots> = (\<integral>\<^isup>+ x. Pxy x * indicator ?B x \<partial>(S \<Otimes>\<^isub>M T))"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   537
        using Pxy A by (intro distributed_emeasure) auto
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   538
      finally have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   539
        (\<integral>\<^isup>+ x. Pxy x * indicator A (snd x, fst x) \<partial>(S \<Otimes>\<^isub>M T))"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   540
        by (auto intro!: positive_integral_cong split: split_indicator) }
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   541
    note * = this
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   542
    show "distr M ?D (\<lambda>x. (Y x, X x)) = density ?D (\<lambda>(x, y). Pxy (y, x))"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   543
      apply (intro measure_eqI)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   544
      apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1])
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   545
      apply (subst positive_integral_distr)
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   546
      apply (auto intro!: * simp: comp_def split_beta)
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   547
      done
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   548
  qed
36624
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   549
qed
25153c08655e Cleanup information theory
hoelzl
parents: 35977
diff changeset
   550
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   551
lemma (in prob_space) distr_marginal1:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   552
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   553
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   554
  defines "Px \<equiv> \<lambda>x. (\<integral>\<^isup>+z. Pxy (x, z) \<partial>T)"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   555
  shows "distributed M S X Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   556
  unfolding distributed_def
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   557
proof safe
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   558
  interpret S: sigma_finite_measure S by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   559
  interpret T: sigma_finite_measure T by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   560
  interpret ST: pair_sigma_finite S T by default
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   561
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   562
  note Pxy[measurable]
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   563
  show X: "X \<in> measurable M S" by simp
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   564
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   565
  show borel: "Px \<in> borel_measurable S"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   566
    by (auto intro!: T.positive_integral_fst_measurable simp: Px_def)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39096
diff changeset
   567
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   568
  interpret Pxy: prob_space "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   569
    by (intro prob_space_distr) simp
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   570
  have "(\<integral>\<^isup>+ x. max 0 (- Pxy x) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>\<^isup>+ x. 0 \<partial>(S \<Otimes>\<^isub>M T))"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   571
    using Pxy
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   572
    by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_AE)
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   573
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   574
  show "distr M S X = density S Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   575
  proof (rule measure_eqI)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   576
    fix A assume A: "A \<in> sets (distr M S X)"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   577
    with X measurable_space[of Y M T]
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   578
    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)"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   579
      by (auto simp add: emeasure_distr intro!: arg_cong[where f="emeasure M"])
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   580
    also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (A \<times> space T)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   581
      using Pxy by (simp add: distributed_def)
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   582
    also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   583
      using A borel Pxy
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   584
      by (simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric])
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   585
    also have "\<dots> = \<integral>\<^isup>+ x. Px x * indicator A x \<partial>S"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   586
      apply (rule positive_integral_cong_AE)
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   587
      using Pxy[THEN distributed_AE, THEN ST.AE_pair] AE_space
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   588
    proof eventually_elim
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   589
      fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   590
      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
   591
        by (auto simp: indicator_def)
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   592
      ultimately have "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = (\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) * indicator A x"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   593
        by (simp add: eq positive_integral_multc cong: positive_integral_cong)
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   594
      also have "(\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) = Px x"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   595
        by (simp add: Px_def ereal_real positive_integral_positive)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   596
      finally show "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = Px x * indicator A x" .
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   597
    qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   598
    finally show "emeasure (distr M S X) A = emeasure (density S Px) A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   599
      using A borel Pxy by (simp add: emeasure_density)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   600
  qed simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   601
  
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   602
  show "AE x in S. 0 \<le> Px x"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   603
    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
   604
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   605
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   606
lemma (in prob_space) distr_marginal2:
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   607
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   608
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   609
  shows "distributed M T Y (\<lambda>y. (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S))"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   610
  using distr_marginal1[OF T S distributed_swap[OF S T]] Pxy by simp
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   611
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   612
lemma (in prob_space) distributed_marginal_eq_joint1:
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   613
  assumes T: "sigma_finite_measure T"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   614
  assumes S: "sigma_finite_measure S"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   615
  assumes Px: "distributed M S X Px"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   616
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   617
  shows "AE x in S. Px x = (\<integral>\<^isup>+y. Pxy (x, y) \<partial>T)"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   618
  using Px distr_marginal1[OF S T Pxy] by (rule distributed_unique)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   619
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   620
lemma (in prob_space) distributed_marginal_eq_joint2:
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   621
  assumes T: "sigma_finite_measure T"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   622
  assumes S: "sigma_finite_measure S"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   623
  assumes Py: "distributed M T Y Py"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   624
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   625
  shows "AE y in T. Py y = (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S)"
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   626
  using Py distr_marginal2[OF S T Pxy] by (rule distributed_unique)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   627
49795
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   628
lemma (in prob_space) distributed_joint_indep':
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   629
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   630
  assumes X[measurable]: "distributed M S X Px" and Y[measurable]: "distributed M T Y Py"
49795
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   631
  assumes indep: "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   632
  shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   633
  unfolding distributed_def
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   634
proof safe
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   635
  interpret S: sigma_finite_measure S by fact
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   636
  interpret T: sigma_finite_measure T by fact
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   637
  interpret ST: pair_sigma_finite S T by default
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   638
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   639
  interpret X: prob_space "density S Px"
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   640
    unfolding distributed_distr_eq_density[OF X, symmetric]
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   641
    by (rule prob_space_distr) simp
49795
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   642
  have sf_X: "sigma_finite_measure (density S Px)" ..
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   643
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   644
  interpret Y: prob_space "density T Py"
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   645
    unfolding distributed_distr_eq_density[OF Y, symmetric]
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   646
    by (rule prob_space_distr) simp
49795
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   647
  have sf_Y: "sigma_finite_measure (density T Py)" ..
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   648
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   649
  show "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) = density (S \<Otimes>\<^isub>M T) (\<lambda>(x, y). Px x * Py y)"
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   650
    unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   651
    using distributed_borel_measurable[OF X] distributed_AE[OF X]
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   652
    using distributed_borel_measurable[OF Y] distributed_AE[OF Y]
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   653
    by (rule pair_measure_density[OF _ _ _ _ T sf_Y])
49795
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   654
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   655
  show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" by auto
49795
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   656
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   657
  show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)" by auto
49795
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   658
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   659
  show "AE x in S \<Otimes>\<^isub>M T. 0 \<le> (case x of (x, y) \<Rightarrow> Px x * Py y)"
51683
baefa3b461c2 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents: 51475
diff changeset
   660
    apply (intro ST.AE_pair_measure borel_measurable_le Pxy borel_measurable_const)
49795
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   661
    using distributed_AE[OF X]
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   662
    apply eventually_elim
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   663
    using distributed_AE[OF Y]
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   664
    apply eventually_elim
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   665
    apply auto
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   666
    done
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   667
qed
9f2fb9b25a77 joint distribution of independent variables
hoelzl
parents: 49788
diff changeset
   668
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   669
definition
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   670
  "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
   671
    finite (X`space M)"
42902
e8dbf90a2f3b Add restricted borel measure to {0 .. 1}
hoelzl
parents: 42892
diff changeset
   672
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   673
lemma simple_distributed:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   674
  "simple_distributed M X Px \<Longrightarrow> distributed M (count_space (X`space M)) X Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   675
  unfolding simple_distributed_def by auto
42902
e8dbf90a2f3b Add restricted borel measure to {0 .. 1}
hoelzl
parents: 42892
diff changeset
   676
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   677
lemma simple_distributed_finite[dest]: "simple_distributed M X P \<Longrightarrow> finite (X`space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   678
  by (simp add: simple_distributed_def)
42902
e8dbf90a2f3b Add restricted borel measure to {0 .. 1}
hoelzl
parents: 42892
diff changeset
   679
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   680
lemma (in prob_space) distributed_simple_function_superset:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   681
  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
   682
  assumes A: "X`space M \<subseteq> A" "finite A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   683
  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
   684
  shows "distributed M S X P'"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   685
  unfolding distributed_def
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   686
proof safe
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   687
  show "(\<lambda>x. ereal (P' x)) \<in> borel_measurable S" unfolding S_def by simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   688
  show "AE x in S. 0 \<le> ereal (P' x)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   689
    using X by (auto simp: S_def P'_def simple_distributed_def intro!: measure_nonneg)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   690
  show "distr M S X = density S P'"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   691
  proof (rule measure_eqI_finite)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   692
    show "sets (distr M S X) = Pow A" "sets (density S P') = Pow A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   693
      using A unfolding S_def by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   694
    show "finite A" by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   695
    fix a assume a: "a \<in> A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   696
    then have "a \<notin> X`space M \<Longrightarrow> X -` {a} \<inter> space M = {}" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   697
    with A a X have "emeasure (distr M S X) {a} = P' a"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   698
      by (subst emeasure_distr)
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   699
         (auto simp add: S_def P'_def simple_functionD emeasure_eq_measure measurable_count_space_eq2
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   700
               intro!: arg_cong[where f=prob])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   701
    also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' a) * indicator {a} x \<partial>S)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   702
      using A X a
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   703
      by (subst positive_integral_cmult_indicator)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   704
         (auto simp: S_def P'_def simple_distributed_def simple_functionD measure_nonneg)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   705
    also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' x) * indicator {a} x \<partial>S)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   706
      by (auto simp: indicator_def intro!: positive_integral_cong)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   707
    also have "\<dots> = emeasure (density S P') {a}"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   708
      using a A by (intro emeasure_density[symmetric]) (auto simp: S_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   709
    finally show "emeasure (distr M S X) {a} = emeasure (density S P') {a}" .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   710
  qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   711
  show "random_variable S X"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   712
    using X(1) A by (auto simp: measurable_def simple_functionD S_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   713
qed
42902
e8dbf90a2f3b Add restricted borel measure to {0 .. 1}
hoelzl
parents: 42892
diff changeset
   714
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   715
lemma (in prob_space) simple_distributedI:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   716
  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
   717
  shows "simple_distributed M X P"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   718
  unfolding simple_distributed_def
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   719
proof
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   720
  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
   721
    (is "?A")
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   722
    using simple_functionD[OF X(1)] by (intro distributed_simple_function_superset[OF X]) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   723
  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
   724
    by (rule distributed_cong_density) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   725
  finally show "\<dots>" .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   726
qed (rule simple_functionD[OF X(1)])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   727
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   728
lemma simple_distributed_joint_finite:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   729
  assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   730
  shows "finite (X ` space M)" "finite (Y ` space M)"
42902
e8dbf90a2f3b Add restricted borel measure to {0 .. 1}
hoelzl
parents: 42892
diff changeset
   731
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   732
  have "finite ((\<lambda>x. (X x, Y x)) ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   733
    using X by (auto simp: simple_distributed_def simple_functionD)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   734
  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
   735
    by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   736
  then show fin: "finite (X ` space M)" "finite (Y ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   737
    by (auto simp: image_image)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   738
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   739
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   740
lemma simple_distributed_joint2_finite:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   741
  assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   742
  shows "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   743
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   744
  have "finite ((\<lambda>x. (X x, Y x, Z x)) ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   745
    using X by (auto simp: simple_distributed_def simple_functionD)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   746
  then have "finite (fst ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   747
    "finite ((fst \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   748
    "finite ((snd \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   749
    by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   750
  then show fin: "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   751
    by (auto simp: image_image)
42902
e8dbf90a2f3b Add restricted borel measure to {0 .. 1}
hoelzl
parents: 42892
diff changeset
   752
qed
e8dbf90a2f3b Add restricted borel measure to {0 .. 1}
hoelzl
parents: 42892
diff changeset
   753
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   754
lemma simple_distributed_simple_function:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   755
  "simple_distributed M X Px \<Longrightarrow> simple_function M X"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   756
  unfolding simple_distributed_def distributed_def
50002
ce0d316b5b44 add measurability prover; add support for Borel sets
hoelzl
parents: 50001
diff changeset
   757
  by (auto simp: simple_function_def measurable_count_space_eq2)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   758
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   759
lemma simple_distributed_measure:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   760
  "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
   761
  using distributed_count_space[of M "X`space M" X P a, symmetric]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   762
  by (auto simp: simple_distributed_def measure_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   763
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   764
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
   765
  by (auto simp: simple_distributed_measure measure_nonneg)
42860
b02349e70d5a add Bernoulli space
hoelzl
parents: 42859
diff changeset
   766
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   767
lemma (in prob_space) simple_distributed_joint:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   768
  assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   769
  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
   770
  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
   771
  shows "distributed M S (\<lambda>x. (X x, Y x)) P"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   772
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   773
  from simple_distributed_joint_finite[OF X, simp]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   774
  have S_eq: "S = count_space (X`space M \<times> Y`space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   775
    by (simp add: S_def pair_measure_count_space)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   776
  show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   777
    unfolding S_eq P_def
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   778
  proof (rule distributed_simple_function_superset)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   779
    show "simple_function M (\<lambda>x. (X x, Y x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   780
      using X by (rule simple_distributed_simple_function)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   781
    fix x assume "x \<in> (\<lambda>x. (X x, Y x)) ` space M"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   782
    from simple_distributed_measure[OF X this]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   783
    show "Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)" .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   784
  qed auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   785
qed
42860
b02349e70d5a add Bernoulli space
hoelzl
parents: 42859
diff changeset
   786
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   787
lemma (in prob_space) simple_distributed_joint2:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   788
  assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   789
  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
   790
  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
   791
  shows "distributed M S (\<lambda>x. (X x, Y x, Z x)) P"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   792
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   793
  from simple_distributed_joint2_finite[OF X, simp]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   794
  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
   795
    by (simp add: S_def pair_measure_count_space)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   796
  show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   797
    unfolding S_eq P_def
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   798
  proof (rule distributed_simple_function_superset)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   799
    show "simple_function M (\<lambda>x. (X x, Y x, Z x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   800
      using X by (rule simple_distributed_simple_function)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   801
    fix x assume "x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   802
    from simple_distributed_measure[OF X this]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   803
    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
   804
  qed auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   805
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   806
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   807
lemma (in prob_space) simple_distributed_setsum_space:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   808
  assumes X: "simple_distributed M X f"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   809
  shows "setsum f (X`space M) = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   810
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   811
  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
   812
    by (subst finite_measure_finite_Union)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   813
       (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
   814
             intro!: setsum_cong arg_cong[where f="prob"])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   815
  also have "\<dots> = prob (space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   816
    by (auto intro!: arg_cong[where f=prob])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   817
  finally show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   818
    using emeasure_space_1 by (simp add: emeasure_eq_measure one_ereal_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   819
qed
42860
b02349e70d5a add Bernoulli space
hoelzl
parents: 42859
diff changeset
   820
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   821
lemma (in prob_space) distributed_marginal_eq_joint_simple:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   822
  assumes Px: "simple_function M X"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   823
  assumes Py: "simple_distributed M Y Py"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   824
  assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   825
  assumes y: "y \<in> Y`space M"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   826
  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
   827
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   828
  note Px = simple_distributedI[OF Px refl]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   829
  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
   830
    by (simp add: setsum_ereal[symmetric] zero_ereal_def)
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   831
  from distributed_marginal_eq_joint2[OF
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   832
    sigma_finite_measure_count_space_finite
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   833
    sigma_finite_measure_count_space_finite
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   834
    simple_distributed[OF Py] simple_distributed_joint[OF Pxy],
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   835
    OF Py[THEN simple_distributed_finite] Px[THEN simple_distributed_finite]]
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   836
    y
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   837
    Px[THEN simple_distributed_finite]
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49786
diff changeset
   838
    Py[THEN simple_distributed_finite]
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   839
    Pxy[THEN simple_distributed, THEN distributed_real_AE]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   840
  show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   841
    unfolding AE_count_space
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   842
    apply (auto simp add: positive_integral_count_space_finite * intro!: setsum_cong split: split_max)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   843
    done
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   844
qed
42860
b02349e70d5a add Bernoulli space
hoelzl
parents: 42859
diff changeset
   845
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   846
lemma distributedI_real:
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   847
  fixes f :: "'a \<Rightarrow> real"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   848
  assumes gen: "sets M1 = sigma_sets (space M1) E" and "Int_stable E"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   849
    and A: "range A \<subseteq> E" "(\<Union>i::nat. A i) = space M1" "\<And>i. emeasure (distr M M1 X) (A i) \<noteq> \<infinity>"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   850
    and X: "X \<in> measurable M M1"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   851
    and f: "f \<in> borel_measurable M1" "AE x in M1. 0 \<le> f x"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   852
    and eq: "\<And>A. A \<in> E \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M1)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   853
  shows "distributed M M1 X f"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   854
  unfolding distributed_def
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   855
proof (intro conjI)
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   856
  show "distr M M1 X = density M1 f"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   857
  proof (rule measure_eqI_generator_eq[where A=A])
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   858
    { fix A assume A: "A \<in> E"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   859
      then have "A \<in> sigma_sets (space M1) E" by auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   860
      then have "A \<in> sets M1"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   861
        using gen by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   862
      with f A eq[of A] X show "emeasure (distr M M1 X) A = emeasure (density M1 f) A"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   863
        by (simp add: emeasure_distr emeasure_density borel_measurable_ereal
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   864
                      times_ereal.simps[symmetric] ereal_indicator
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   865
                 del: times_ereal.simps) }
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   866
    note eq_E = this
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   867
    show "Int_stable E" by fact
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   868
    { fix e assume "e \<in> E"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   869
      then have "e \<in> sigma_sets (space M1) E" by auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   870
      then have "e \<in> sets M1" unfolding gen .
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   871
      then have "e \<subseteq> space M1" by (rule sets.sets_into_space) }
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   872
    then show "E \<subseteq> Pow (space M1)" by auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   873
    show "sets (distr M M1 X) = sigma_sets (space M1) E"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   874
      "sets (density M1 (\<lambda>x. ereal (f x))) = sigma_sets (space M1) E"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   875
      unfolding gen[symmetric] by auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   876
  qed fact+
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   877
qed (insert X f, auto)
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   878
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   879
lemma distributedI_borel_atMost:
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   880
  fixes f :: "real \<Rightarrow> real"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   881
  assumes [measurable]: "X \<in> borel_measurable M"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   882
    and [measurable]: "f \<in> borel_measurable borel" and f[simp]: "AE x in lborel. 0 \<le> f x"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   883
    and g_eq: "\<And>a. (\<integral>\<^isup>+x. f x * indicator {..a} x \<partial>lborel)  = ereal (g a)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   884
    and M_eq: "\<And>a. emeasure M {x\<in>space M. X x \<le> a} = ereal (g a)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   885
  shows "distributed M lborel X f"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   886
proof (rule distributedI_real)
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   887
  show "sets lborel = sigma_sets (space lborel) (range atMost)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   888
    by (simp add: borel_eq_atMost)
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   889
  show "Int_stable (range atMost :: real set set)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   890
    by (auto simp: Int_stable_def)
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   891
  have vimage_eq: "\<And>a. (X -` {..a} \<inter> space M) = {x\<in>space M. X x \<le> a}" by auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   892
  def A \<equiv> "\<lambda>i::nat. {.. real i}"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   893
  then show "range A \<subseteq> range atMost" "(\<Union>i. A i) = space lborel"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   894
    "\<And>i. emeasure (distr M lborel X) (A i) \<noteq> \<infinity>"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   895
    by (auto simp: real_arch_simple emeasure_distr vimage_eq M_eq)
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   896
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   897
  fix A :: "real set" assume "A \<in> range atMost"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   898
  then obtain a where A: "A = {..a}" by auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   899
  show "emeasure M (X -` A \<inter> space M) = (\<integral>\<^isup>+x. f x * indicator A x \<partial>lborel)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   900
    unfolding vimage_eq A M_eq g_eq ..
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   901
qed auto
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   902
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   903
lemma (in prob_space) uniform_distributed_params:
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   904
  assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   905
  shows "A \<in> sets MX" "measure MX A \<noteq> 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   906
proof -
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   907
  interpret X: prob_space "distr M MX X"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   908
    using distributed_measurable[OF X] by (rule prob_space_distr)
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   909
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   910
  show "measure MX A \<noteq> 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   911
  proof
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   912
    assume "measure MX A = 0"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   913
    with X.emeasure_space_1 X.prob_space distributed_distr_eq_density[OF X]
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   914
    show False
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   915
      by (simp add: emeasure_density zero_ereal_def[symmetric])
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   916
  qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   917
  with measure_notin_sets[of A MX] show "A \<in> sets MX"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   918
    by blast
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   919
qed
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50244
diff changeset
   920
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   921
lemma prob_space_uniform_measure:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   922
  assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   923
  shows "prob_space (uniform_measure M A)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   924
proof
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   925
  show "emeasure (uniform_measure M A) (space (uniform_measure M A)) = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   926
    using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)], of "space M"]
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 50104
diff changeset
   927
    using sets.sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   928
    by (simp add: Int_absorb2 emeasure_nonneg)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   929
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   930
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   931
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
   932
  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
   933
35582
b16d99a72dc9 Add Lebesgue integral and probability space.
hoelzl
parents:
diff changeset
   934
end