src/HOL/Probability/Probability_Measure.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 62343 24106dc44def
child 62390 842917225d56
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
hoelzl@42148
     1
(*  Title:      HOL/Probability/Probability_Measure.thy
hoelzl@42067
     2
    Author:     Johannes Hölzl, TU München
hoelzl@42067
     3
    Author:     Armin Heller, TU München
hoelzl@42067
     4
*)
hoelzl@42067
     5
wenzelm@61808
     6
section \<open>Probability measure\<close>
hoelzl@42067
     7
hoelzl@42148
     8
theory Probability_Measure
hoelzl@47694
     9
  imports Lebesgue_Measure Radon_Nikodym
hoelzl@35582
    10
begin
hoelzl@35582
    11
hoelzl@62083
    12
lemma (in finite_measure) countable_support:
hoelzl@62083
    13
  "countable {x. measure M {x} \<noteq> 0}"
hoelzl@62083
    14
proof cases
hoelzl@62083
    15
  assume "measure M (space M) = 0"
hoelzl@62083
    16
  with bounded_measure measure_le_0_iff have "{x. measure M {x} \<noteq> 0} = {}"
hoelzl@62083
    17
    by auto
hoelzl@62083
    18
  then show ?thesis
hoelzl@62083
    19
    by simp
hoelzl@62083
    20
next
hoelzl@62083
    21
  let ?M = "measure M (space M)" and ?m = "\<lambda>x. measure M {x}"
hoelzl@62083
    22
  assume "?M \<noteq> 0"
hoelzl@62083
    23
  then have *: "{x. ?m x \<noteq> 0} = (\<Union>n. {x. ?M / Suc n < ?m x})"
hoelzl@62083
    24
    using reals_Archimedean[of "?m x / ?M" for x]
hoelzl@62083
    25
    by (auto simp: field_simps not_le[symmetric] measure_nonneg divide_le_0_iff measure_le_0_iff)
hoelzl@62083
    26
  have **: "\<And>n. finite {x. ?M / Suc n < ?m x}"
hoelzl@62083
    27
  proof (rule ccontr)
hoelzl@62083
    28
    fix n assume "infinite {x. ?M / Suc n < ?m x}" (is "infinite ?X")
hoelzl@62083
    29
    then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X"
hoelzl@62083
    30
      by (metis infinite_arbitrarily_large)
hoelzl@62083
    31
    from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x"
hoelzl@62083
    32
      by auto
hoelzl@62083
    33
    { fix x assume "x \<in> X"
hoelzl@62083
    34
      from \<open>?M \<noteq> 0\<close> *[OF this] have "?m x \<noteq> 0" by (auto simp: field_simps measure_le_0_iff)
hoelzl@62083
    35
      then have "{x} \<in> sets M" by (auto dest: measure_notin_sets) }
hoelzl@62083
    36
    note singleton_sets = this
hoelzl@62083
    37
    have "?M < (\<Sum>x\<in>X. ?M / Suc n)"
hoelzl@62083
    38
      using \<open>?M \<noteq> 0\<close>
hoelzl@62083
    39
      by (simp add: \<open>card X = Suc (Suc n)\<close> of_nat_Suc field_simps less_le measure_nonneg)
hoelzl@62083
    40
    also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)"
hoelzl@62083
    41
      by (rule setsum_mono) fact
hoelzl@62083
    42
    also have "\<dots> = measure M (\<Union>x\<in>X. {x})"
hoelzl@62083
    43
      using singleton_sets \<open>finite X\<close>
hoelzl@62083
    44
      by (intro finite_measure_finite_Union[symmetric]) (auto simp: disjoint_family_on_def)
hoelzl@62083
    45
    finally have "?M < measure M (\<Union>x\<in>X. {x})" .
hoelzl@62083
    46
    moreover have "measure M (\<Union>x\<in>X. {x}) \<le> ?M"
hoelzl@62083
    47
      using singleton_sets[THEN sets.sets_into_space] by (intro finite_measure_mono) auto
hoelzl@62083
    48
    ultimately show False by simp
hoelzl@62083
    49
  qed
hoelzl@62083
    50
  show ?thesis
hoelzl@62083
    51
    unfolding * by (intro countable_UN countableI_type countable_finite[OF **])
hoelzl@62083
    52
qed
hoelzl@62083
    53
hoelzl@45777
    54
locale prob_space = finite_measure +
hoelzl@47694
    55
  assumes emeasure_space_1: "emeasure M (space M) = 1"
hoelzl@38656
    56
hoelzl@45777
    57
lemma prob_spaceI[Pure.intro!]:
hoelzl@47694
    58
  assumes *: "emeasure M (space M) = 1"
hoelzl@45777
    59
  shows "prob_space M"
hoelzl@45777
    60
proof -
hoelzl@45777
    61
  interpret finite_measure M
hoelzl@45777
    62
  proof
hoelzl@47694
    63
    show "emeasure M (space M) \<noteq> \<infinity>" using * by simp 
hoelzl@45777
    64
  qed
wenzelm@61169
    65
  show "prob_space M" by standard fact
hoelzl@38656
    66
qed
hoelzl@38656
    67
hoelzl@59425
    68
lemma prob_space_imp_sigma_finite: "prob_space M \<Longrightarrow> sigma_finite_measure M"
hoelzl@59425
    69
  unfolding prob_space_def finite_measure_def by simp
hoelzl@59425
    70
hoelzl@40859
    71
abbreviation (in prob_space) "events \<equiv> sets M"
hoelzl@47694
    72
abbreviation (in prob_space) "prob \<equiv> measure M"
hoelzl@47694
    73
abbreviation (in prob_space) "random_variable M' X \<equiv> X \<in> measurable M M'"
wenzelm@53015
    74
abbreviation (in prob_space) "expectation \<equiv> integral\<^sup>L M"
hoelzl@57235
    75
abbreviation (in prob_space) "variance X \<equiv> integral\<^sup>L M (\<lambda>x. (X x - expectation X)\<^sup>2)"
hoelzl@35582
    76
hoelzl@57447
    77
lemma (in prob_space) finite_measure [simp]: "finite_measure M"
hoelzl@57447
    78
  by unfold_locales
hoelzl@57447
    79
hoelzl@47694
    80
lemma (in prob_space) prob_space_distr:
hoelzl@47694
    81
  assumes f: "f \<in> measurable M M'" shows "prob_space (distr M M' f)"
hoelzl@47694
    82
proof (rule prob_spaceI)
hoelzl@47694
    83
  have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space)
hoelzl@47694
    84
  with f show "emeasure (distr M M' f) (space (distr M M' f)) = 1"
hoelzl@47694
    85
    by (auto simp: emeasure_distr emeasure_space_1)
hoelzl@43339
    86
qed
hoelzl@43339
    87
hoelzl@61359
    88
lemma prob_space_distrD:
hoelzl@61359
    89
  assumes f: "f \<in> measurable M N" and M: "prob_space (distr M N f)" shows "prob_space M"
hoelzl@61359
    90
proof
wenzelm@61605
    91
  interpret M: prob_space "distr M N f" by fact
hoelzl@61359
    92
  have "f -` space N \<inter> space M = space M"
hoelzl@61359
    93
    using f[THEN measurable_space] by auto
hoelzl@61359
    94
  then show "emeasure M (space M) = 1"
hoelzl@61359
    95
    using M.emeasure_space_1 by (simp add: emeasure_distr[OF f])
hoelzl@61359
    96
qed
hoelzl@61359
    97
hoelzl@40859
    98
lemma (in prob_space) prob_space: "prob (space M) = 1"
hoelzl@47694
    99
  using emeasure_space_1 unfolding measure_def by (simp add: one_ereal_def)
hoelzl@41981
   100
hoelzl@41981
   101
lemma (in prob_space) prob_le_1[simp, intro]: "prob A \<le> 1"
hoelzl@41981
   102
  using bounded_measure[of A] by (simp add: prob_space)
hoelzl@41981
   103
hoelzl@47694
   104
lemma (in prob_space) not_empty: "space M \<noteq> {}"
hoelzl@47694
   105
  using prob_space by auto
hoelzl@41981
   106
hoelzl@47694
   107
lemma (in prob_space) measure_le_1: "emeasure M X \<le> 1"
hoelzl@47694
   108
  using emeasure_space[of M X] by (simp add: emeasure_space_1)
hoelzl@42950
   109
hoelzl@43339
   110
lemma (in prob_space) AE_I_eq_1:
hoelzl@47694
   111
  assumes "emeasure M {x\<in>space M. P x} = 1" "{x\<in>space M. P x} \<in> sets M"
hoelzl@47694
   112
  shows "AE x in M. P x"
hoelzl@43339
   113
proof (rule AE_I)
hoelzl@47694
   114
  show "emeasure M (space M - {x \<in> space M. P x}) = 0"
hoelzl@47694
   115
    using assms emeasure_space_1 by (simp add: emeasure_compl)
hoelzl@43339
   116
qed (insert assms, auto)
hoelzl@43339
   117
hoelzl@59000
   118
lemma prob_space_restrict_space:
hoelzl@59000
   119
  "S \<in> sets M \<Longrightarrow> emeasure M S = 1 \<Longrightarrow> prob_space (restrict_space M S)"
hoelzl@59000
   120
  by (intro prob_spaceI)
hoelzl@59000
   121
     (simp add: emeasure_restrict_space space_restrict_space)
hoelzl@59000
   122
hoelzl@40859
   123
lemma (in prob_space) prob_compl:
hoelzl@41981
   124
  assumes A: "A \<in> events"
hoelzl@38656
   125
  shows "prob (space M - A) = 1 - prob A"
hoelzl@41981
   126
  using finite_measure_compl[OF A] by (simp add: prob_space)
hoelzl@35582
   127
hoelzl@47694
   128
lemma (in prob_space) AE_in_set_eq_1:
hoelzl@47694
   129
  assumes "A \<in> events" shows "(AE x in M. x \<in> A) \<longleftrightarrow> prob A = 1"
hoelzl@47694
   130
proof
hoelzl@47694
   131
  assume ae: "AE x in M. x \<in> A"
hoelzl@47694
   132
  have "{x \<in> space M. x \<in> A} = A" "{x \<in> space M. x \<notin> A} = space M - A"
wenzelm@61808
   133
    using \<open>A \<in> events\<close>[THEN sets.sets_into_space] by auto
wenzelm@61808
   134
  with AE_E2[OF ae] \<open>A \<in> events\<close> have "1 - emeasure M A = 0"
hoelzl@47694
   135
    by (simp add: emeasure_compl emeasure_space_1)
hoelzl@47694
   136
  then show "prob A = 1"
wenzelm@61808
   137
    using \<open>A \<in> events\<close> by (simp add: emeasure_eq_measure one_ereal_def)
hoelzl@47694
   138
next
hoelzl@47694
   139
  assume prob: "prob A = 1"
hoelzl@47694
   140
  show "AE x in M. x \<in> A"
hoelzl@47694
   141
  proof (rule AE_I)
hoelzl@47694
   142
    show "{x \<in> space M. x \<notin> A} \<subseteq> space M - A" by auto
hoelzl@47694
   143
    show "emeasure M (space M - A) = 0"
wenzelm@61808
   144
      using \<open>A \<in> events\<close> prob
hoelzl@47694
   145
      by (simp add: prob_compl emeasure_space_1 emeasure_eq_measure one_ereal_def)
hoelzl@47694
   146
    show "space M - A \<in> events"
wenzelm@61808
   147
      using \<open>A \<in> events\<close> by auto
hoelzl@47694
   148
  qed
hoelzl@47694
   149
qed
hoelzl@47694
   150
hoelzl@47694
   151
lemma (in prob_space) AE_False: "(AE x in M. False) \<longleftrightarrow> False"
hoelzl@47694
   152
proof
hoelzl@47694
   153
  assume "AE x in M. False"
hoelzl@47694
   154
  then have "AE x in M. x \<in> {}" by simp
hoelzl@47694
   155
  then show False
hoelzl@47694
   156
    by (subst (asm) AE_in_set_eq_1) auto
hoelzl@47694
   157
qed simp
hoelzl@47694
   158
hoelzl@47694
   159
lemma (in prob_space) AE_prob_1:
hoelzl@47694
   160
  assumes "prob A = 1" shows "AE x in M. x \<in> A"
hoelzl@47694
   161
proof -
wenzelm@61808
   162
  from \<open>prob A = 1\<close> have "A \<in> events"
hoelzl@47694
   163
    by (metis measure_notin_sets zero_neq_one)
hoelzl@47694
   164
  with AE_in_set_eq_1 assms show ?thesis by simp
hoelzl@47694
   165
qed
hoelzl@47694
   166
hoelzl@50098
   167
lemma (in prob_space) AE_const[simp]: "(AE x in M. P) \<longleftrightarrow> P"
hoelzl@50098
   168
  by (cases P) (auto simp: AE_False)
hoelzl@50098
   169
hoelzl@59000
   170
lemma (in prob_space) ae_filter_bot: "ae_filter M \<noteq> bot"
hoelzl@59000
   171
  by (simp add: trivial_limit_def)
hoelzl@59000
   172
hoelzl@50098
   173
lemma (in prob_space) AE_contr:
hoelzl@50098
   174
  assumes ae: "AE \<omega> in M. P \<omega>" "AE \<omega> in M. \<not> P \<omega>"
hoelzl@50098
   175
  shows False
hoelzl@50098
   176
proof -
hoelzl@50098
   177
  from ae have "AE \<omega> in M. False" by eventually_elim auto
hoelzl@50098
   178
  then show False by auto
hoelzl@50098
   179
qed
hoelzl@50098
   180
hoelzl@59000
   181
lemma (in prob_space) emeasure_eq_1_AE:
hoelzl@59000
   182
  "S \<in> sets M \<Longrightarrow> AE x in M. x \<in> S \<Longrightarrow> emeasure M S = 1"
hoelzl@59000
   183
  by (subst emeasure_eq_AE[where B="space M"]) (auto simp: emeasure_space_1)
hoelzl@59000
   184
hoelzl@57025
   185
lemma (in prob_space) integral_ge_const:
hoelzl@57025
   186
  fixes c :: real
hoelzl@57025
   187
  shows "integrable M f \<Longrightarrow> (AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>x. f x \<partial>M)"
hoelzl@57025
   188
  using integral_mono_AE[of M "\<lambda>x. c" f] prob_space by simp
hoelzl@57025
   189
hoelzl@57025
   190
lemma (in prob_space) integral_le_const:
hoelzl@57025
   191
  fixes c :: real
hoelzl@57025
   192
  shows "integrable M f \<Longrightarrow> (AE x in M. f x \<le> c) \<Longrightarrow> (\<integral>x. f x \<partial>M) \<le> c"
hoelzl@57025
   193
  using integral_mono_AE[of M f "\<lambda>x. c"] prob_space by simp
hoelzl@57025
   194
hoelzl@57025
   195
lemma (in prob_space) nn_integral_ge_const:
hoelzl@57025
   196
  "(AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>\<^sup>+x. f x \<partial>M)"
hoelzl@57025
   197
  using nn_integral_mono_AE[of "\<lambda>x. c" f M] emeasure_space_1
hoelzl@57025
   198
  by (simp add: nn_integral_const_If split: split_if_asm)
hoelzl@57025
   199
hoelzl@43339
   200
lemma (in prob_space) expectation_less:
hoelzl@56993
   201
  fixes X :: "_ \<Rightarrow> real"
hoelzl@43339
   202
  assumes [simp]: "integrable M X"
hoelzl@49786
   203
  assumes gt: "AE x in M. X x < b"
hoelzl@43339
   204
  shows "expectation X < b"
hoelzl@43339
   205
proof -
hoelzl@43339
   206
  have "expectation X < expectation (\<lambda>x. b)"
hoelzl@47694
   207
    using gt emeasure_space_1
hoelzl@43340
   208
    by (intro integral_less_AE_space) auto
hoelzl@43339
   209
  then show ?thesis using prob_space by simp
hoelzl@43339
   210
qed
hoelzl@43339
   211
hoelzl@43339
   212
lemma (in prob_space) expectation_greater:
hoelzl@56993
   213
  fixes X :: "_ \<Rightarrow> real"
hoelzl@43339
   214
  assumes [simp]: "integrable M X"
hoelzl@49786
   215
  assumes gt: "AE x in M. a < X x"
hoelzl@43339
   216
  shows "a < expectation X"
hoelzl@43339
   217
proof -
hoelzl@43339
   218
  have "expectation (\<lambda>x. a) < expectation X"
hoelzl@47694
   219
    using gt emeasure_space_1
hoelzl@43340
   220
    by (intro integral_less_AE_space) auto
hoelzl@43339
   221
  then show ?thesis using prob_space by simp
hoelzl@43339
   222
qed
hoelzl@43339
   223
hoelzl@43339
   224
lemma (in prob_space) jensens_inequality:
hoelzl@56993
   225
  fixes q :: "real \<Rightarrow> real"
hoelzl@49786
   226
  assumes X: "integrable M X" "AE x in M. X x \<in> I"
hoelzl@43339
   227
  assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV"
hoelzl@43339
   228
  assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q"
hoelzl@43339
   229
  shows "q (expectation X) \<le> expectation (\<lambda>x. q (X x))"
hoelzl@43339
   230
proof -
wenzelm@46731
   231
  let ?F = "\<lambda>x. Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I))"
hoelzl@49786
   232
  from X(2) AE_False have "I \<noteq> {}" by auto
hoelzl@43339
   233
hoelzl@43339
   234
  from I have "open I" by auto
hoelzl@43339
   235
hoelzl@43339
   236
  note I
hoelzl@43339
   237
  moreover
hoelzl@43339
   238
  { assume "I \<subseteq> {a <..}"
hoelzl@43339
   239
    with X have "a < expectation X"
hoelzl@43339
   240
      by (intro expectation_greater) auto }
hoelzl@43339
   241
  moreover
hoelzl@43339
   242
  { assume "I \<subseteq> {..< b}"
hoelzl@43339
   243
    with X have "expectation X < b"
hoelzl@43339
   244
      by (intro expectation_less) auto }
hoelzl@43339
   245
  ultimately have "expectation X \<in> I"
hoelzl@43339
   246
    by (elim disjE)  (auto simp: subset_eq)
hoelzl@43339
   247
  moreover
hoelzl@43339
   248
  { fix y assume y: "y \<in> I"
wenzelm@61808
   249
    with q(2) \<open>open I\<close> have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
haftmann@62343
   250
      by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open) }
hoelzl@43339
   251
  ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
hoelzl@43339
   252
    by simp
hoelzl@43339
   253
  also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
hoelzl@51475
   254
  proof (rule cSup_least)
hoelzl@43339
   255
    show "(\<lambda>x. q x + ?F x * (expectation X - x)) ` I \<noteq> {}"
wenzelm@61808
   256
      using \<open>I \<noteq> {}\<close> by auto
hoelzl@43339
   257
  next
hoelzl@43339
   258
    fix k assume "k \<in> (\<lambda>x. q x + ?F x * (expectation X - x)) ` I"
hoelzl@43339
   259
    then guess x .. note x = this
hoelzl@43339
   260
    have "q x + ?F x * (expectation X  - x) = expectation (\<lambda>w. q x + ?F x * (X w - x))"
hoelzl@47694
   261
      using prob_space by (simp add: X)
hoelzl@43339
   262
    also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
wenzelm@61808
   263
      using \<open>x \<in> I\<close> \<open>open I\<close> X(2)
hoelzl@56993
   264
      apply (intro integral_mono_AE integrable_add integrable_mult_right integrable_diff
hoelzl@56993
   265
                integrable_const X q)
lp15@61810
   266
      apply (elim eventually_mono)
hoelzl@49786
   267
      apply (intro convex_le_Inf_differential)
hoelzl@49786
   268
      apply (auto simp: interior_open q)
hoelzl@49786
   269
      done
hoelzl@43339
   270
    finally show "k \<le> expectation (\<lambda>w. q (X w))" using x by auto
hoelzl@43339
   271
  qed
hoelzl@43339
   272
  finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" .
hoelzl@43339
   273
qed
hoelzl@43339
   274
wenzelm@61808
   275
subsection  \<open>Introduce binder for probability\<close>
hoelzl@50001
   276
hoelzl@50001
   277
syntax
Andreas@59356
   278
  "_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("('\<P>'((/_ in _./ _)'))")
hoelzl@50001
   279
hoelzl@50001
   280
translations
hoelzl@50001
   281
  "\<P>(x in M. P)" => "CONST measure M {x \<in> CONST space M. P}"
hoelzl@50001
   282
wenzelm@61808
   283
print_translation \<open>
Andreas@58764
   284
  let
Andreas@58764
   285
    fun to_pattern (Const (@{const_syntax Pair}, _) $ l $ r) =
Andreas@58764
   286
      Syntax.const @{const_syntax Pair} :: to_pattern l @ to_pattern r
Andreas@58764
   287
    | to_pattern (t as (Const (@{syntax_const "_bound"}, _)) $ _) = [t]
Andreas@58764
   288
Andreas@58764
   289
    fun mk_pattern ((t, n) :: xs) = mk_patterns n xs |>> curry list_comb t
Andreas@58764
   290
    and mk_patterns 0 xs = ([], xs)
Andreas@58764
   291
    | mk_patterns n xs =
Andreas@58764
   292
      let
Andreas@58764
   293
        val (t, xs') = mk_pattern xs
Andreas@58764
   294
        val (ts, xs'') = mk_patterns (n - 1) xs'
Andreas@58764
   295
      in
Andreas@58764
   296
        (t :: ts, xs'')
Andreas@58764
   297
      end
Andreas@58764
   298
Andreas@58764
   299
    fun unnest_tuples
Andreas@58764
   300
      (Const (@{syntax_const "_pattern"}, _) $ 
Andreas@58764
   301
        t1 $
Andreas@58764
   302
        (t as (Const (@{syntax_const "_pattern"}, _) $ _ $ _)))
Andreas@58764
   303
      = let
Andreas@58764
   304
        val (_ $ t2 $ t3) = unnest_tuples t
Andreas@58764
   305
      in
Andreas@58764
   306
        Syntax.const @{syntax_const "_pattern"} $ 
Andreas@58764
   307
          unnest_tuples t1 $
Andreas@58764
   308
          (Syntax.const @{syntax_const "_patterns"} $ t2 $ t3)
Andreas@58764
   309
      end
Andreas@58764
   310
    | unnest_tuples pat = pat
Andreas@58764
   311
Andreas@58764
   312
    fun tr' [sig_alg, Const (@{const_syntax Collect}, _) $ t] = 
Andreas@58764
   313
      let
Andreas@58764
   314
        val bound_dummyT = Const (@{syntax_const "_bound"}, dummyT)
Andreas@58764
   315
Andreas@58764
   316
        fun go pattern elem
Andreas@58764
   317
          (Const (@{const_syntax "conj"}, _) $ 
Andreas@58764
   318
            (Const (@{const_syntax Set.member}, _) $ elem' $ (Const (@{const_syntax space}, _) $ sig_alg')) $
Andreas@58764
   319
            u)
Andreas@58764
   320
          = let
Andreas@58764
   321
              val _ = if sig_alg aconv sig_alg' andalso to_pattern elem' = rev elem then () else raise Match;
Andreas@58764
   322
              val (pat, rest) = mk_pattern (rev pattern);
Andreas@58764
   323
              val _ = case rest of [] => () | _ => raise Match
Andreas@58764
   324
            in
Andreas@58764
   325
              Syntax.const @{syntax_const "_prob"} $ unnest_tuples pat $ sig_alg $ u
Andreas@58764
   326
            end
Andreas@58764
   327
        | go pattern elem (Abs abs) =
Andreas@58764
   328
            let
Andreas@58764
   329
              val (x as (_ $ tx), t) = Syntax_Trans.atomic_abs_tr' abs
Andreas@58764
   330
            in
Andreas@58764
   331
              go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t
Andreas@58764
   332
            end
haftmann@61424
   333
        | go pattern elem (Const (@{const_syntax case_prod}, _) $ t) =
Andreas@58764
   334
            go 
Andreas@58764
   335
              ((Syntax.const @{syntax_const "_pattern"}, 2) :: pattern)
Andreas@58764
   336
              (Syntax.const @{const_syntax Pair} :: elem)
Andreas@58764
   337
              t
Andreas@58764
   338
      in
Andreas@58764
   339
        go [] [] t
Andreas@58764
   340
      end
Andreas@58764
   341
  in
Andreas@58764
   342
    [(@{const_syntax Sigma_Algebra.measure}, K tr')]
Andreas@58764
   343
  end
wenzelm@61808
   344
\<close>
Andreas@58764
   345
hoelzl@50001
   346
definition
hoelzl@50001
   347
  "cond_prob M P Q = \<P>(\<omega> in M. P \<omega> \<and> Q \<omega>) / \<P>(\<omega> in M. Q \<omega>)"
hoelzl@50001
   348
hoelzl@50001
   349
syntax
hoelzl@50001
   350
  "_conditional_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("('\<P>'(_ in _. _ \<bar>/ _'))")
hoelzl@50001
   351
hoelzl@50001
   352
translations
hoelzl@50001
   353
  "\<P>(x in M. P \<bar> Q)" => "CONST cond_prob M (\<lambda>x. P) (\<lambda>x. Q)"
hoelzl@50001
   354
hoelzl@50001
   355
lemma (in prob_space) AE_E_prob:
hoelzl@50001
   356
  assumes ae: "AE x in M. P x"
hoelzl@50001
   357
  obtains S where "S \<subseteq> {x \<in> space M. P x}" "S \<in> events" "prob S = 1"
hoelzl@50001
   358
proof -
hoelzl@50001
   359
  from ae[THEN AE_E] guess N .
hoelzl@50001
   360
  then show thesis
hoelzl@50001
   361
    by (intro that[of "space M - N"])
hoelzl@50001
   362
       (auto simp: prob_compl prob_space emeasure_eq_measure)
hoelzl@50001
   363
qed
hoelzl@50001
   364
hoelzl@50001
   365
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)"
hoelzl@50001
   366
  by (auto intro!: arg_cong[where f=prob] simp add: prob_compl[symmetric])
hoelzl@50001
   367
hoelzl@50001
   368
lemma (in prob_space) prob_eq_AE:
hoelzl@50001
   369
  "(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)"
hoelzl@50001
   370
  by (rule finite_measure_eq_AE) auto
hoelzl@50001
   371
hoelzl@50001
   372
lemma (in prob_space) prob_eq_0_AE:
hoelzl@50001
   373
  assumes not: "AE x in M. \<not> P x" shows "\<P>(x in M. P x) = 0"
hoelzl@50001
   374
proof cases
hoelzl@50001
   375
  assume "{x\<in>space M. P x} \<in> events"
hoelzl@50001
   376
  with not have "\<P>(x in M. P x) = \<P>(x in M. False)"
hoelzl@50001
   377
    by (intro prob_eq_AE) auto
hoelzl@50001
   378
  then show ?thesis by simp
hoelzl@50001
   379
qed (simp add: measure_notin_sets)
hoelzl@50001
   380
hoelzl@50098
   381
lemma (in prob_space) prob_Collect_eq_0:
hoelzl@50098
   382
  "{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)"
hoelzl@50098
   383
  using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"] by (simp add: emeasure_eq_measure)
hoelzl@50098
   384
hoelzl@50098
   385
lemma (in prob_space) prob_Collect_eq_1:
hoelzl@50098
   386
  "{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 1 \<longleftrightarrow> (AE x in M. P x)"
hoelzl@50098
   387
  using AE_in_set_eq_1[of "{x\<in>space M. P x}"] by simp
hoelzl@50098
   388
hoelzl@50098
   389
lemma (in prob_space) prob_eq_0:
hoelzl@50098
   390
  "A \<in> sets M \<Longrightarrow> prob A = 0 \<longleftrightarrow> (AE x in M. x \<notin> A)"
hoelzl@50098
   391
  using AE_iff_measurable[OF _ refl, of M "\<lambda>x. x \<notin> A"]
hoelzl@50098
   392
  by (auto simp add: emeasure_eq_measure Int_def[symmetric])
hoelzl@50098
   393
hoelzl@50098
   394
lemma (in prob_space) prob_eq_1:
hoelzl@50098
   395
  "A \<in> sets M \<Longrightarrow> prob A = 1 \<longleftrightarrow> (AE x in M. x \<in> A)"
hoelzl@50098
   396
  using AE_in_set_eq_1[of A] by simp
hoelzl@50098
   397
hoelzl@50001
   398
lemma (in prob_space) prob_sums:
hoelzl@50001
   399
  assumes P: "\<And>n. {x\<in>space M. P n x} \<in> events"
hoelzl@50001
   400
  assumes Q: "{x\<in>space M. Q x} \<in> events"
hoelzl@50001
   401
  assumes ae: "AE x in M. (\<forall>n. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n. P n x))"
hoelzl@50001
   402
  shows "(\<lambda>n. \<P>(x in M. P n x)) sums \<P>(x in M. Q x)"
hoelzl@50001
   403
proof -
hoelzl@50001
   404
  from ae[THEN AE_E_prob] guess S . note S = this
hoelzl@50001
   405
  then have disj: "disjoint_family (\<lambda>n. {x\<in>space M. P n x} \<inter> S)"
hoelzl@50001
   406
    by (auto simp: disjoint_family_on_def)
hoelzl@50001
   407
  from S have ae_S:
hoelzl@50001
   408
    "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)"
hoelzl@50001
   409
    "\<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"
hoelzl@50001
   410
    using ae by (auto dest!: AE_prob_1)
hoelzl@50001
   411
  from ae_S have *:
hoelzl@50001
   412
    "\<P>(x in M. Q x) = prob (\<Union>n. {x\<in>space M. P n x} \<inter> S)"
hoelzl@50001
   413
    using P Q S by (intro finite_measure_eq_AE) auto
hoelzl@50001
   414
  from ae_S have **:
hoelzl@50001
   415
    "\<And>n. \<P>(x in M. P n x) = prob ({x\<in>space M. P n x} \<inter> S)"
hoelzl@50001
   416
    using P Q S by (intro finite_measure_eq_AE) auto
hoelzl@50001
   417
  show ?thesis
hoelzl@50001
   418
    unfolding * ** using S P disj
hoelzl@50001
   419
    by (intro finite_measure_UNION) auto
hoelzl@50001
   420
qed
hoelzl@50001
   421
hoelzl@59000
   422
lemma (in prob_space) prob_setsum:
hoelzl@59000
   423
  assumes [simp, intro]: "finite I"
hoelzl@59000
   424
  assumes P: "\<And>n. n \<in> I \<Longrightarrow> {x\<in>space M. P n x} \<in> events"
hoelzl@59000
   425
  assumes Q: "{x\<in>space M. Q x} \<in> events"
hoelzl@59000
   426
  assumes ae: "AE x in M. (\<forall>n\<in>I. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n\<in>I. P n x))"
hoelzl@59000
   427
  shows "\<P>(x in M. Q x) = (\<Sum>n\<in>I. \<P>(x in M. P n x))"
hoelzl@59000
   428
proof -
hoelzl@59000
   429
  from ae[THEN AE_E_prob] guess S . note S = this
hoelzl@59000
   430
  then have disj: "disjoint_family_on (\<lambda>n. {x\<in>space M. P n x} \<inter> S) I"
hoelzl@59000
   431
    by (auto simp: disjoint_family_on_def)
hoelzl@59000
   432
  from S have ae_S:
hoelzl@59000
   433
    "AE x in M. x \<in> {x\<in>space M. Q x} \<longleftrightarrow> x \<in> (\<Union>n\<in>I. {x\<in>space M. P n x} \<inter> S)"
hoelzl@59000
   434
    "\<And>n. n \<in> I \<Longrightarrow> 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"
hoelzl@59000
   435
    using ae by (auto dest!: AE_prob_1)
hoelzl@59000
   436
  from ae_S have *:
hoelzl@59000
   437
    "\<P>(x in M. Q x) = prob (\<Union>n\<in>I. {x\<in>space M. P n x} \<inter> S)"
hoelzl@59000
   438
    using P Q S by (intro finite_measure_eq_AE) (auto intro!: sets.Int)
hoelzl@59000
   439
  from ae_S have **:
hoelzl@59000
   440
    "\<And>n. n \<in> I \<Longrightarrow> \<P>(x in M. P n x) = prob ({x\<in>space M. P n x} \<inter> S)"
hoelzl@59000
   441
    using P Q S by (intro finite_measure_eq_AE) auto
hoelzl@59000
   442
  show ?thesis
hoelzl@59000
   443
    using S P disj
hoelzl@59000
   444
    by (auto simp add: * ** simp del: UN_simps intro!: finite_measure_finite_Union)
hoelzl@59000
   445
qed
hoelzl@59000
   446
hoelzl@54418
   447
lemma (in prob_space) prob_EX_countable:
hoelzl@54418
   448
  assumes sets: "\<And>i. i \<in> I \<Longrightarrow> {x\<in>space M. P i x} \<in> sets M" and I: "countable I" 
hoelzl@54418
   449
  assumes disj: "AE x in M. \<forall>i\<in>I. \<forall>j\<in>I. P i x \<longrightarrow> P j x \<longrightarrow> i = j"
hoelzl@54418
   450
  shows "\<P>(x in M. \<exists>i\<in>I. P i x) = (\<integral>\<^sup>+i. \<P>(x in M. P i x) \<partial>count_space I)"
hoelzl@54418
   451
proof -
hoelzl@54418
   452
  let ?N= "\<lambda>x. \<exists>!i\<in>I. P i x"
hoelzl@54418
   453
  have "ereal (\<P>(x in M. \<exists>i\<in>I. P i x)) = \<P>(x in M. (\<exists>i\<in>I. P i x \<and> ?N x))"
hoelzl@54418
   454
    unfolding ereal.inject
hoelzl@54418
   455
  proof (rule prob_eq_AE)
hoelzl@54418
   456
    show "AE x in M. (\<exists>i\<in>I. P i x) = (\<exists>i\<in>I. P i x \<and> ?N x)"
hoelzl@54418
   457
      using disj by eventually_elim blast
hoelzl@54418
   458
  qed (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets)+
hoelzl@54418
   459
  also have "\<P>(x in M. (\<exists>i\<in>I. P i x \<and> ?N x)) = emeasure M (\<Union>i\<in>I. {x\<in>space M. P i x \<and> ?N x})"
hoelzl@54418
   460
    unfolding emeasure_eq_measure by (auto intro!: arg_cong[where f=prob])
hoelzl@54418
   461
  also have "\<dots> = (\<integral>\<^sup>+i. emeasure M {x\<in>space M. P i x \<and> ?N x} \<partial>count_space I)"
hoelzl@54418
   462
    by (rule emeasure_UN_countable)
hoelzl@54418
   463
       (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets
hoelzl@54418
   464
             simp: disjoint_family_on_def)
hoelzl@54418
   465
  also have "\<dots> = (\<integral>\<^sup>+i. \<P>(x in M. P i x) \<partial>count_space I)"
hoelzl@54418
   466
    unfolding emeasure_eq_measure using disj
hoelzl@56996
   467
    by (intro nn_integral_cong ereal.inject[THEN iffD2] prob_eq_AE)
hoelzl@54418
   468
       (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets)+
hoelzl@54418
   469
  finally show ?thesis .
hoelzl@54418
   470
qed
hoelzl@54418
   471
hoelzl@50001
   472
lemma (in prob_space) cond_prob_eq_AE:
hoelzl@50001
   473
  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"
hoelzl@50001
   474
  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"
hoelzl@50001
   475
  shows "cond_prob M P Q = cond_prob M P' Q'"
hoelzl@50001
   476
  using P Q
immler@50244
   477
  by (auto simp: cond_prob_def intro!: arg_cong2[where f="op /"] prob_eq_AE sets.sets_Collect_conj)
hoelzl@50001
   478
hoelzl@50001
   479
hoelzl@40859
   480
lemma (in prob_space) joint_distribution_Times_le_fst:
hoelzl@47694
   481
  "random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY
wenzelm@53015
   482
    \<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^sub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MX X) A"
hoelzl@47694
   483
  by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets)
hoelzl@40859
   484
hoelzl@40859
   485
lemma (in prob_space) joint_distribution_Times_le_snd:
hoelzl@47694
   486
  "random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY
wenzelm@53015
   487
    \<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^sub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MY Y) B"
hoelzl@47694
   488
  by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets)
hoelzl@40859
   489
hoelzl@57235
   490
lemma (in prob_space) variance_eq:
hoelzl@57235
   491
  fixes X :: "'a \<Rightarrow> real"
hoelzl@57235
   492
  assumes [simp]: "integrable M X"
hoelzl@57235
   493
  assumes [simp]: "integrable M (\<lambda>x. (X x)\<^sup>2)"
hoelzl@57235
   494
  shows "variance X = expectation (\<lambda>x. (X x)\<^sup>2) - (expectation X)\<^sup>2"
hoelzl@57235
   495
  by (simp add: field_simps prob_space power2_diff power2_eq_square[symmetric])
hoelzl@57235
   496
hoelzl@57235
   497
lemma (in prob_space) variance_positive: "0 \<le> variance (X::'a \<Rightarrow> real)"
hoelzl@57235
   498
  by (intro integral_nonneg_AE) (auto intro!: integral_nonneg_AE)
hoelzl@57235
   499
hoelzl@57447
   500
lemma (in prob_space) variance_mean_zero:
hoelzl@57447
   501
  "expectation X = 0 \<Longrightarrow> variance X = expectation (\<lambda>x. (X x)^2)"
hoelzl@57447
   502
  by simp
hoelzl@57447
   503
hoelzl@45777
   504
locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2
hoelzl@41689
   505
ballarin@61565
   506
sublocale pair_prob_space \<subseteq> P?: prob_space "M1 \<Otimes>\<^sub>M M2"
hoelzl@45777
   507
proof
wenzelm@53015
   508
  show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) = 1"
hoelzl@49776
   509
    by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
hoelzl@45777
   510
qed
hoelzl@40859
   511
hoelzl@47694
   512
locale product_prob_space = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +
hoelzl@45777
   513
  fixes I :: "'i set"
hoelzl@45777
   514
  assumes prob_space: "\<And>i. prob_space (M i)"
hoelzl@42988
   515
ballarin@61565
   516
sublocale product_prob_space \<subseteq> M?: prob_space "M i" for i
hoelzl@42988
   517
  by (rule prob_space)
hoelzl@42988
   518
hoelzl@45777
   519
locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I
hoelzl@42988
   520
wenzelm@53015
   521
sublocale finite_product_prob_space \<subseteq> prob_space "\<Pi>\<^sub>M i\<in>I. M i"
hoelzl@45777
   522
proof
wenzelm@53015
   523
  show "emeasure (\<Pi>\<^sub>M i\<in>I. M i) (space (\<Pi>\<^sub>M i\<in>I. M i)) = 1"
haftmann@57418
   524
    by (simp add: measure_times M.emeasure_space_1 setprod.neutral_const space_PiM)
hoelzl@45777
   525
qed
hoelzl@42988
   526
hoelzl@42988
   527
lemma (in finite_product_prob_space) prob_times:
hoelzl@42988
   528
  assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets (M i)"
wenzelm@53015
   529
  shows "prob (\<Pi>\<^sub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))"
hoelzl@42988
   530
proof -
wenzelm@53015
   531
  have "ereal (measure (\<Pi>\<^sub>M i\<in>I. M i) (\<Pi>\<^sub>E i\<in>I. X i)) = emeasure (\<Pi>\<^sub>M i\<in>I. M i) (\<Pi>\<^sub>E i\<in>I. X i)"
hoelzl@47694
   532
    using X by (simp add: emeasure_eq_measure)
hoelzl@47694
   533
  also have "\<dots> = (\<Prod>i\<in>I. emeasure (M i) (X i))"
hoelzl@42988
   534
    using measure_times X by simp
hoelzl@47694
   535
  also have "\<dots> = ereal (\<Prod>i\<in>I. measure (M i) (X i))"
hoelzl@47694
   536
    using X by (simp add: M.emeasure_eq_measure setprod_ereal)
hoelzl@42859
   537
  finally show ?thesis by simp
hoelzl@42859
   538
qed
hoelzl@42859
   539
wenzelm@61808
   540
subsection \<open>Distributions\<close>
hoelzl@42892
   541
hoelzl@47694
   542
definition "distributed M N X f \<longleftrightarrow> distr M N X = density N f \<and> 
hoelzl@47694
   543
  f \<in> borel_measurable N \<and> (AE x in N. 0 \<le> f x) \<and> X \<in> measurable M N"
hoelzl@36624
   544
hoelzl@47694
   545
lemma
hoelzl@50003
   546
  assumes "distributed M N X f"
hoelzl@50003
   547
  shows distributed_distr_eq_density: "distr M N X = density N f"
hoelzl@50003
   548
    and distributed_measurable: "X \<in> measurable M N"
hoelzl@50003
   549
    and distributed_borel_measurable: "f \<in> borel_measurable N"
hoelzl@50003
   550
    and distributed_AE: "(AE x in N. 0 \<le> f x)"
hoelzl@50003
   551
  using assms by (simp_all add: distributed_def)
hoelzl@50003
   552
hoelzl@50003
   553
lemma
hoelzl@50003
   554
  assumes D: "distributed M N X f"
hoelzl@50003
   555
  shows distributed_measurable'[measurable_dest]:
hoelzl@50003
   556
      "g \<in> measurable L M \<Longrightarrow> (\<lambda>x. X (g x)) \<in> measurable L N"
hoelzl@50003
   557
    and distributed_borel_measurable'[measurable_dest]:
hoelzl@50003
   558
      "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
hoelzl@50003
   559
  using distributed_measurable[OF D] distributed_borel_measurable[OF D]
hoelzl@50003
   560
  by simp_all
hoelzl@39097
   561
hoelzl@47694
   562
lemma
hoelzl@47694
   563
  shows distributed_real_measurable: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> f \<in> borel_measurable N"
hoelzl@47694
   564
    and distributed_real_AE: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> (AE x in N. 0 \<le> f x)"
hoelzl@47694
   565
  by (simp_all add: distributed_def borel_measurable_ereal_iff)
hoelzl@35977
   566
hoelzl@59353
   567
lemma distributed_real_measurable':
hoelzl@59353
   568
  "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
hoelzl@59353
   569
  by simp
hoelzl@50003
   570
hoelzl@59353
   571
lemma joint_distributed_measurable1:
hoelzl@59353
   572
  "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f \<Longrightarrow> h1 \<in> measurable N M \<Longrightarrow> (\<lambda>x. X (h1 x)) \<in> measurable N S"
hoelzl@59353
   573
  by simp
hoelzl@59353
   574
hoelzl@59353
   575
lemma joint_distributed_measurable2:
hoelzl@59353
   576
  "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f \<Longrightarrow> h2 \<in> measurable N M \<Longrightarrow> (\<lambda>x. Y (h2 x)) \<in> measurable N T"
hoelzl@59353
   577
  by simp
hoelzl@50003
   578
hoelzl@47694
   579
lemma distributed_count_space:
hoelzl@47694
   580
  assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A"
hoelzl@47694
   581
  shows "P a = emeasure M (X -` {a} \<inter> space M)"
hoelzl@39097
   582
proof -
hoelzl@47694
   583
  have "emeasure M (X -` {a} \<inter> space M) = emeasure (distr M (count_space A) X) {a}"
hoelzl@50003
   584
    using X a A by (simp add: emeasure_distr)
hoelzl@47694
   585
  also have "\<dots> = emeasure (density (count_space A) P) {a}"
hoelzl@47694
   586
    using X by (simp add: distributed_distr_eq_density)
wenzelm@53015
   587
  also have "\<dots> = (\<integral>\<^sup>+x. P a * indicator {a} x \<partial>count_space A)"
hoelzl@56996
   588
    using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: nn_integral_cong)
hoelzl@47694
   589
  also have "\<dots> = P a"
hoelzl@56996
   590
    using X a by (subst nn_integral_cmult_indicator) (auto simp: distributed_def one_ereal_def[symmetric] AE_count_space)
hoelzl@47694
   591
  finally show ?thesis ..
hoelzl@39092
   592
qed
hoelzl@35977
   593
hoelzl@47694
   594
lemma distributed_cong_density:
hoelzl@47694
   595
  "(AE x in N. f x = g x) \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> f \<in> borel_measurable N \<Longrightarrow>
hoelzl@47694
   596
    distributed M N X f \<longleftrightarrow> distributed M N X g"
hoelzl@47694
   597
  by (auto simp: distributed_def intro!: density_cong)
hoelzl@47694
   598
hoelzl@47694
   599
lemma subdensity:
hoelzl@47694
   600
  assumes T: "T \<in> measurable P Q"
hoelzl@47694
   601
  assumes f: "distributed M P X f"
hoelzl@47694
   602
  assumes g: "distributed M Q Y g"
hoelzl@47694
   603
  assumes Y: "Y = T \<circ> X"
hoelzl@47694
   604
  shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0"
hoelzl@47694
   605
proof -
hoelzl@47694
   606
  have "{x\<in>space Q. g x = 0} \<in> null_sets (distr M Q (T \<circ> X))"
hoelzl@47694
   607
    using g Y by (auto simp: null_sets_density_iff distributed_def)
hoelzl@47694
   608
  also have "distr M Q (T \<circ> X) = distr (distr M P X) Q T"
hoelzl@47694
   609
    using T f[THEN distributed_measurable] by (rule distr_distr[symmetric])
hoelzl@47694
   610
  finally have "T -` {x\<in>space Q. g x = 0} \<inter> space P \<in> null_sets (distr M P X)"
hoelzl@47694
   611
    using T by (subst (asm) null_sets_distr_iff) auto
hoelzl@47694
   612
  also have "T -` {x\<in>space Q. g x = 0} \<inter> space P = {x\<in>space P. g (T x) = 0}"
hoelzl@47694
   613
    using T by (auto dest: measurable_space)
hoelzl@47694
   614
  finally show ?thesis
hoelzl@47694
   615
    using f g by (auto simp add: null_sets_density_iff distributed_def)
hoelzl@35977
   616
qed
hoelzl@35977
   617
hoelzl@47694
   618
lemma subdensity_real:
hoelzl@47694
   619
  fixes g :: "'a \<Rightarrow> real" and f :: "'b \<Rightarrow> real"
hoelzl@47694
   620
  assumes T: "T \<in> measurable P Q"
hoelzl@47694
   621
  assumes f: "distributed M P X f"
hoelzl@47694
   622
  assumes g: "distributed M Q Y g"
hoelzl@47694
   623
  assumes Y: "Y = T \<circ> X"
hoelzl@47694
   624
  shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0"
hoelzl@47694
   625
  using subdensity[OF T, of M X "\<lambda>x. ereal (f x)" Y "\<lambda>x. ereal (g x)"] assms by auto
hoelzl@47694
   626
hoelzl@49788
   627
lemma distributed_emeasure:
wenzelm@53015
   628
  "distributed M N X f \<Longrightarrow> A \<in> sets N \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^sup>+x. f x * indicator A x \<partial>N)"
hoelzl@50003
   629
  by (auto simp: distributed_AE
hoelzl@49788
   630
                 distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr)
hoelzl@49788
   631
hoelzl@56996
   632
lemma distributed_nn_integral:
wenzelm@53015
   633
  "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^sup>+x. f x * g x \<partial>N) = (\<integral>\<^sup>+x. g (X x) \<partial>M)"
hoelzl@50003
   634
  by (auto simp: distributed_AE
hoelzl@56996
   635
                 distributed_distr_eq_density[symmetric] nn_integral_density[symmetric] nn_integral_distr)
hoelzl@49788
   636
hoelzl@47694
   637
lemma distributed_integral:
hoelzl@47694
   638
  "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)"
hoelzl@50003
   639
  by (auto simp: distributed_real_AE
hoelzl@56993
   640
                 distributed_distr_eq_density[symmetric] integral_real_density[symmetric] integral_distr)
hoelzl@47694
   641
  
hoelzl@47694
   642
lemma distributed_transform_integral:
hoelzl@47694
   643
  assumes Px: "distributed M N X Px"
hoelzl@47694
   644
  assumes "distributed M P Y Py"
hoelzl@47694
   645
  assumes Y: "Y = T \<circ> X" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P"
hoelzl@47694
   646
  shows "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. Px x * f (T x) \<partial>N)"
hoelzl@41689
   647
proof -
hoelzl@47694
   648
  have "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. f (Y x) \<partial>M)"
hoelzl@47694
   649
    by (rule distributed_integral) fact+
hoelzl@47694
   650
  also have "\<dots> = (\<integral>x. f (T (X x)) \<partial>M)"
hoelzl@47694
   651
    using Y by simp
hoelzl@47694
   652
  also have "\<dots> = (\<integral>x. Px x * f (T x) \<partial>N)"
hoelzl@47694
   653
    using measurable_comp[OF T f] Px by (intro distributed_integral[symmetric]) (auto simp: comp_def)
hoelzl@45777
   654
  finally show ?thesis .
hoelzl@39092
   655
qed
hoelzl@36624
   656
hoelzl@49788
   657
lemma (in prob_space) distributed_unique:
hoelzl@47694
   658
  assumes Px: "distributed M S X Px"
hoelzl@49788
   659
  assumes Py: "distributed M S X Py"
hoelzl@49788
   660
  shows "AE x in S. Px x = Py x"
hoelzl@49788
   661
proof -
hoelzl@49788
   662
  interpret X: prob_space "distr M S X"
hoelzl@50003
   663
    using Px by (intro prob_space_distr) simp
hoelzl@49788
   664
  have "sigma_finite_measure (distr M S X)" ..
hoelzl@49788
   665
  with sigma_finite_density_unique[of Px S Py ] Px Py
hoelzl@49788
   666
  show ?thesis
hoelzl@49788
   667
    by (auto simp: distributed_def)
hoelzl@49788
   668
qed
hoelzl@49788
   669
hoelzl@49788
   670
lemma (in prob_space) distributed_jointI:
hoelzl@49788
   671
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
hoelzl@50003
   672
  assumes X[measurable]: "X \<in> measurable M S" and Y[measurable]: "Y \<in> measurable M T"
wenzelm@53015
   673
  assumes [measurable]: "f \<in> borel_measurable (S \<Otimes>\<^sub>M T)" and f: "AE x in S \<Otimes>\<^sub>M T. 0 \<le> f x"
hoelzl@49788
   674
  assumes eq: "\<And>A B. A \<in> sets S \<Longrightarrow> B \<in> sets T \<Longrightarrow> 
wenzelm@53015
   675
    emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B} = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. f (x, y) * indicator B y \<partial>T) * indicator A x \<partial>S)"
wenzelm@53015
   676
  shows "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f"
hoelzl@49788
   677
  unfolding distributed_def
hoelzl@49788
   678
proof safe
hoelzl@49788
   679
  interpret S: sigma_finite_measure S by fact
hoelzl@49788
   680
  interpret T: sigma_finite_measure T by fact
wenzelm@61169
   681
  interpret ST: pair_sigma_finite S T ..
hoelzl@47694
   682
hoelzl@49788
   683
  from ST.sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('b \<times> 'c) set" .. note F = this
hoelzl@49788
   684
  let ?E = "{a \<times> b |a b. a \<in> sets S \<and> b \<in> sets T}"
wenzelm@53015
   685
  let ?P = "S \<Otimes>\<^sub>M T"
hoelzl@49788
   686
  show "distr M ?P (\<lambda>x. (X x, Y x)) = density ?P f" (is "?L = ?R")
hoelzl@49788
   687
  proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of S T]])
hoelzl@49788
   688
    show "?E \<subseteq> Pow (space ?P)"
immler@50244
   689
      using sets.space_closed[of S] sets.space_closed[of T] by (auto simp: space_pair_measure)
hoelzl@49788
   690
    show "sets ?L = sigma_sets (space ?P) ?E"
hoelzl@49788
   691
      by (simp add: sets_pair_measure space_pair_measure)
hoelzl@49788
   692
    then show "sets ?R = sigma_sets (space ?P) ?E"
hoelzl@49788
   693
      by simp
hoelzl@49788
   694
  next
hoelzl@49788
   695
    interpret L: prob_space ?L
hoelzl@49788
   696
      by (rule prob_space_distr) (auto intro!: measurable_Pair)
hoelzl@49788
   697
    show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?L (F i) \<noteq> \<infinity>"
hoelzl@49788
   698
      using F by (auto simp: space_pair_measure)
hoelzl@49788
   699
  next
hoelzl@49788
   700
    fix E assume "E \<in> ?E"
hoelzl@50003
   701
    then obtain A B where E[simp]: "E = A \<times> B"
hoelzl@50003
   702
      and A[measurable]: "A \<in> sets S" and B[measurable]: "B \<in> sets T" by auto
hoelzl@49788
   703
    have "emeasure ?L E = emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B}"
hoelzl@49788
   704
      by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair)
wenzelm@53015
   705
    also have "\<dots> = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)"
hoelzl@56996
   706
      using f by (auto simp add: eq nn_integral_multc intro!: nn_integral_cong)
hoelzl@49788
   707
    also have "\<dots> = emeasure ?R E"
hoelzl@56996
   708
      by (auto simp add: emeasure_density T.nn_integral_fst[symmetric]
hoelzl@56996
   709
               intro!: nn_integral_cong split: split_indicator)
hoelzl@49788
   710
    finally show "emeasure ?L E = emeasure ?R E" .
hoelzl@49788
   711
  qed
hoelzl@50003
   712
qed (auto simp: f)
hoelzl@49788
   713
hoelzl@49788
   714
lemma (in prob_space) distributed_swap:
hoelzl@49788
   715
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
wenzelm@53015
   716
  assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
wenzelm@53015
   717
  shows "distributed M (T \<Otimes>\<^sub>M S) (\<lambda>x. (Y x, X x)) (\<lambda>(x, y). Pxy (y, x))"
hoelzl@49788
   718
proof -
hoelzl@49788
   719
  interpret S: sigma_finite_measure S by fact
hoelzl@49788
   720
  interpret T: sigma_finite_measure T by fact
wenzelm@61169
   721
  interpret ST: pair_sigma_finite S T ..
wenzelm@61169
   722
  interpret TS: pair_sigma_finite T S ..
hoelzl@49788
   723
hoelzl@50003
   724
  note Pxy[measurable]
hoelzl@49788
   725
  show ?thesis 
hoelzl@49788
   726
    apply (subst TS.distr_pair_swap)
hoelzl@49788
   727
    unfolding distributed_def
hoelzl@49788
   728
  proof safe
wenzelm@53015
   729
    let ?D = "distr (S \<Otimes>\<^sub>M T) (T \<Otimes>\<^sub>M S) (\<lambda>(x, y). (y, x))"
hoelzl@49788
   730
    show 1: "(\<lambda>(x, y). Pxy (y, x)) \<in> borel_measurable ?D"
hoelzl@50003
   731
      by auto
hoelzl@49788
   732
    with Pxy
wenzelm@53015
   733
    show "AE x in distr (S \<Otimes>\<^sub>M T) (T \<Otimes>\<^sub>M S) (\<lambda>(x, y). (y, x)). 0 \<le> (case x of (x, y) \<Rightarrow> Pxy (y, x))"
hoelzl@49788
   734
      by (subst AE_distr_iff)
hoelzl@49788
   735
         (auto dest!: distributed_AE
hoelzl@49788
   736
               simp: measurable_split_conv split_beta
hoelzl@51683
   737
               intro!: measurable_Pair)
wenzelm@53015
   738
    show 2: "random_variable (distr (S \<Otimes>\<^sub>M T) (T \<Otimes>\<^sub>M S) (\<lambda>(x, y). (y, x))) (\<lambda>x. (Y x, X x))"
hoelzl@50003
   739
      using Pxy by auto
wenzelm@53015
   740
    { fix A assume A: "A \<in> sets (T \<Otimes>\<^sub>M S)"
wenzelm@53015
   741
      let ?B = "(\<lambda>(x, y). (y, x)) -` A \<inter> space (S \<Otimes>\<^sub>M T)"
immler@50244
   742
      from sets.sets_into_space[OF A]
hoelzl@49788
   743
      have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
hoelzl@49788
   744
        emeasure M ((\<lambda>x. (X x, Y x)) -` ?B \<inter> space M)"
hoelzl@49788
   745
        by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure)
wenzelm@53015
   746
      also have "\<dots> = (\<integral>\<^sup>+ x. Pxy x * indicator ?B x \<partial>(S \<Otimes>\<^sub>M T))"
hoelzl@50003
   747
        using Pxy A by (intro distributed_emeasure) auto
hoelzl@49788
   748
      finally have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
wenzelm@53015
   749
        (\<integral>\<^sup>+ x. Pxy x * indicator A (snd x, fst x) \<partial>(S \<Otimes>\<^sub>M T))"
hoelzl@56996
   750
        by (auto intro!: nn_integral_cong split: split_indicator) }
hoelzl@49788
   751
    note * = this
hoelzl@49788
   752
    show "distr M ?D (\<lambda>x. (Y x, X x)) = density ?D (\<lambda>(x, y). Pxy (y, x))"
hoelzl@49788
   753
      apply (intro measure_eqI)
hoelzl@49788
   754
      apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1])
hoelzl@56996
   755
      apply (subst nn_integral_distr)
hoelzl@50003
   756
      apply (auto intro!: * simp: comp_def split_beta)
hoelzl@49788
   757
      done
hoelzl@49788
   758
  qed
hoelzl@36624
   759
qed
hoelzl@36624
   760
hoelzl@47694
   761
lemma (in prob_space) distr_marginal1:
hoelzl@47694
   762
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
wenzelm@53015
   763
  assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
wenzelm@53015
   764
  defines "Px \<equiv> \<lambda>x. (\<integral>\<^sup>+z. Pxy (x, z) \<partial>T)"
hoelzl@47694
   765
  shows "distributed M S X Px"
hoelzl@47694
   766
  unfolding distributed_def
hoelzl@47694
   767
proof safe
hoelzl@47694
   768
  interpret S: sigma_finite_measure S by fact
hoelzl@47694
   769
  interpret T: sigma_finite_measure T by fact
wenzelm@61169
   770
  interpret ST: pair_sigma_finite S T ..
hoelzl@47694
   771
hoelzl@50003
   772
  note Pxy[measurable]
hoelzl@50003
   773
  show X: "X \<in> measurable M S" by simp
hoelzl@47694
   774
hoelzl@50003
   775
  show borel: "Px \<in> borel_measurable S"
hoelzl@56996
   776
    by (auto intro!: T.nn_integral_fst simp: Px_def)
hoelzl@39097
   777
wenzelm@53015
   778
  interpret Pxy: prob_space "distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))"
hoelzl@50003
   779
    by (intro prob_space_distr) simp
wenzelm@53015
   780
  have "(\<integral>\<^sup>+ x. max 0 (- Pxy x) \<partial>(S \<Otimes>\<^sub>M T)) = (\<integral>\<^sup>+ x. 0 \<partial>(S \<Otimes>\<^sub>M T))"
hoelzl@47694
   781
    using Pxy
hoelzl@56996
   782
    by (intro nn_integral_cong_AE) (auto simp: max_def dest: distributed_AE)
hoelzl@49788
   783
hoelzl@47694
   784
  show "distr M S X = density S Px"
hoelzl@47694
   785
  proof (rule measure_eqI)
hoelzl@47694
   786
    fix A assume A: "A \<in> sets (distr M S X)"
hoelzl@50003
   787
    with X measurable_space[of Y M T]
wenzelm@53015
   788
    have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)"
hoelzl@50003
   789
      by (auto simp add: emeasure_distr intro!: arg_cong[where f="emeasure M"])
wenzelm@53015
   790
    also have "\<dots> = emeasure (density (S \<Otimes>\<^sub>M T) Pxy) (A \<times> space T)"
hoelzl@47694
   791
      using Pxy by (simp add: distributed_def)
wenzelm@53015
   792
    also have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"
hoelzl@47694
   793
      using A borel Pxy
hoelzl@56996
   794
      by (simp add: emeasure_density T.nn_integral_fst[symmetric])
wenzelm@53015
   795
    also have "\<dots> = \<integral>\<^sup>+ x. Px x * indicator A x \<partial>S"
hoelzl@56996
   796
      apply (rule nn_integral_cong_AE)
hoelzl@49788
   797
      using Pxy[THEN distributed_AE, THEN ST.AE_pair] AE_space
hoelzl@47694
   798
    proof eventually_elim
hoelzl@49788
   799
      fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)"
hoelzl@47694
   800
      moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x"
hoelzl@47694
   801
        by (auto simp: indicator_def)
wenzelm@53015
   802
      ultimately have "(\<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = (\<integral>\<^sup>+ y. Pxy (x, y) \<partial>T) * indicator A x"
hoelzl@56996
   803
        by (simp add: eq nn_integral_multc cong: nn_integral_cong)
wenzelm@53015
   804
      also have "(\<integral>\<^sup>+ y. Pxy (x, y) \<partial>T) = Px x"
hoelzl@56996
   805
        by (simp add: Px_def ereal_real nn_integral_nonneg)
wenzelm@53015
   806
      finally show "(\<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = Px x * indicator A x" .
hoelzl@47694
   807
    qed
hoelzl@47694
   808
    finally show "emeasure (distr M S X) A = emeasure (density S Px) A"
hoelzl@47694
   809
      using A borel Pxy by (simp add: emeasure_density)
hoelzl@47694
   810
  qed simp
hoelzl@47694
   811
  
hoelzl@49788
   812
  show "AE x in S. 0 \<le> Px x"
hoelzl@56996
   813
    by (simp add: Px_def nn_integral_nonneg real_of_ereal_pos)
hoelzl@40859
   814
qed
hoelzl@40859
   815
hoelzl@49788
   816
lemma (in prob_space) distr_marginal2:
hoelzl@49788
   817
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
wenzelm@53015
   818
  assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
wenzelm@53015
   819
  shows "distributed M T Y (\<lambda>y. (\<integral>\<^sup>+x. Pxy (x, y) \<partial>S))"
hoelzl@49788
   820
  using distr_marginal1[OF T S distributed_swap[OF S T]] Pxy by simp
hoelzl@49788
   821
hoelzl@49788
   822
lemma (in prob_space) distributed_marginal_eq_joint1:
hoelzl@49788
   823
  assumes T: "sigma_finite_measure T"
hoelzl@49788
   824
  assumes S: "sigma_finite_measure S"
hoelzl@49788
   825
  assumes Px: "distributed M S X Px"
wenzelm@53015
   826
  assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
wenzelm@53015
   827
  shows "AE x in S. Px x = (\<integral>\<^sup>+y. Pxy (x, y) \<partial>T)"
hoelzl@49788
   828
  using Px distr_marginal1[OF S T Pxy] by (rule distributed_unique)
hoelzl@49788
   829
hoelzl@49788
   830
lemma (in prob_space) distributed_marginal_eq_joint2:
hoelzl@49788
   831
  assumes T: "sigma_finite_measure T"
hoelzl@49788
   832
  assumes S: "sigma_finite_measure S"
hoelzl@49788
   833
  assumes Py: "distributed M T Y Py"
wenzelm@53015
   834
  assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
wenzelm@53015
   835
  shows "AE y in T. Py y = (\<integral>\<^sup>+x. Pxy (x, y) \<partial>S)"
hoelzl@49788
   836
  using Py distr_marginal2[OF S T Pxy] by (rule distributed_unique)
hoelzl@49788
   837
hoelzl@49795
   838
lemma (in prob_space) distributed_joint_indep':
hoelzl@49795
   839
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
hoelzl@50003
   840
  assumes X[measurable]: "distributed M S X Px" and Y[measurable]: "distributed M T Y Py"
wenzelm@53015
   841
  assumes indep: "distr M S X \<Otimes>\<^sub>M distr M T Y = distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))"
wenzelm@53015
   842
  shows "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
hoelzl@49795
   843
  unfolding distributed_def
hoelzl@49795
   844
proof safe
hoelzl@49795
   845
  interpret S: sigma_finite_measure S by fact
hoelzl@49795
   846
  interpret T: sigma_finite_measure T by fact
wenzelm@61169
   847
  interpret ST: pair_sigma_finite S T ..
hoelzl@49795
   848
hoelzl@49795
   849
  interpret X: prob_space "density S Px"
hoelzl@49795
   850
    unfolding distributed_distr_eq_density[OF X, symmetric]
hoelzl@50003
   851
    by (rule prob_space_distr) simp
hoelzl@49795
   852
  have sf_X: "sigma_finite_measure (density S Px)" ..
hoelzl@49795
   853
hoelzl@49795
   854
  interpret Y: prob_space "density T Py"
hoelzl@49795
   855
    unfolding distributed_distr_eq_density[OF Y, symmetric]
hoelzl@50003
   856
    by (rule prob_space_distr) simp
hoelzl@49795
   857
  have sf_Y: "sigma_finite_measure (density T Py)" ..
hoelzl@49795
   858
wenzelm@53015
   859
  show "distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) = density (S \<Otimes>\<^sub>M T) (\<lambda>(x, y). Px x * Py y)"
hoelzl@49795
   860
    unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
hoelzl@49795
   861
    using distributed_borel_measurable[OF X] distributed_AE[OF X]
hoelzl@49795
   862
    using distributed_borel_measurable[OF Y] distributed_AE[OF Y]
hoelzl@50003
   863
    by (rule pair_measure_density[OF _ _ _ _ T sf_Y])
hoelzl@49795
   864
wenzelm@53015
   865
  show "random_variable (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))" by auto
hoelzl@49795
   866
wenzelm@53015
   867
  show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^sub>M T)" by auto
hoelzl@49795
   868
wenzelm@53015
   869
  show "AE x in S \<Otimes>\<^sub>M T. 0 \<le> (case x of (x, y) \<Rightarrow> Px x * Py y)"
hoelzl@51683
   870
    apply (intro ST.AE_pair_measure borel_measurable_le Pxy borel_measurable_const)
hoelzl@49795
   871
    using distributed_AE[OF X]
hoelzl@49795
   872
    apply eventually_elim
hoelzl@49795
   873
    using distributed_AE[OF Y]
hoelzl@49795
   874
    apply eventually_elim
hoelzl@49795
   875
    apply auto
hoelzl@49795
   876
    done
hoelzl@49795
   877
qed
hoelzl@49795
   878
hoelzl@57235
   879
lemma distributed_integrable:
hoelzl@57235
   880
  "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow>
hoelzl@57235
   881
    integrable N (\<lambda>x. f x * g x) \<longleftrightarrow> integrable M (\<lambda>x. g (X x))"
hoelzl@57235
   882
  by (auto simp: distributed_real_AE
hoelzl@57235
   883
                    distributed_distr_eq_density[symmetric] integrable_real_density[symmetric] integrable_distr_eq)
hoelzl@57235
   884
  
hoelzl@57235
   885
lemma distributed_transform_integrable:
hoelzl@57235
   886
  assumes Px: "distributed M N X Px"
hoelzl@57235
   887
  assumes "distributed M P Y Py"
hoelzl@57235
   888
  assumes Y: "Y = (\<lambda>x. T (X x))" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P"
hoelzl@57235
   889
  shows "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
hoelzl@57235
   890
proof -
hoelzl@57235
   891
  have "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable M (\<lambda>x. f (Y x))"
hoelzl@57235
   892
    by (rule distributed_integrable) fact+
hoelzl@57235
   893
  also have "\<dots> \<longleftrightarrow> integrable M (\<lambda>x. f (T (X x)))"
hoelzl@57235
   894
    using Y by simp
hoelzl@57235
   895
  also have "\<dots> \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
hoelzl@57235
   896
    using measurable_comp[OF T f] Px by (intro distributed_integrable[symmetric]) (auto simp: comp_def)
hoelzl@57235
   897
  finally show ?thesis .
hoelzl@57235
   898
qed
hoelzl@57235
   899
hoelzl@57275
   900
lemma distributed_integrable_var:
hoelzl@57275
   901
  fixes X :: "'a \<Rightarrow> real"
hoelzl@57275
   902
  shows "distributed M lborel X (\<lambda>x. ereal (f x)) \<Longrightarrow> integrable lborel (\<lambda>x. f x * x) \<Longrightarrow> integrable M X"
hoelzl@57275
   903
  using distributed_integrable[of M lborel X f "\<lambda>x. x"] by simp
hoelzl@57275
   904
hoelzl@57235
   905
lemma (in prob_space) distributed_variance:
hoelzl@57235
   906
  fixes f::"real \<Rightarrow> real"
hoelzl@57235
   907
  assumes D: "distributed M lborel X f"
hoelzl@57235
   908
  shows "variance X = (\<integral>x. x\<^sup>2 * f (x + expectation X) \<partial>lborel)"
hoelzl@57235
   909
proof (subst distributed_integral[OF D, symmetric])
hoelzl@57235
   910
  show "(\<integral> x. f x * (x - expectation X)\<^sup>2 \<partial>lborel) = (\<integral> x. x\<^sup>2 * f (x + expectation X) \<partial>lborel)"
hoelzl@57235
   911
    by (subst lborel_integral_real_affine[where c=1 and t="expectation X"])  (auto simp: ac_simps)
hoelzl@57235
   912
qed simp
hoelzl@57235
   913
hoelzl@57235
   914
lemma (in prob_space) variance_affine:
hoelzl@57235
   915
  fixes f::"real \<Rightarrow> real"
hoelzl@57235
   916
  assumes [arith]: "b \<noteq> 0"
hoelzl@57235
   917
  assumes D[intro]: "distributed M lborel X f"
hoelzl@57235
   918
  assumes [simp]: "prob_space (density lborel f)"
hoelzl@57235
   919
  assumes I[simp]: "integrable M X"
hoelzl@57235
   920
  assumes I2[simp]: "integrable M (\<lambda>x. (X x)\<^sup>2)" 
hoelzl@57235
   921
  shows "variance (\<lambda>x. a + b * X x) = b\<^sup>2 * variance X"
hoelzl@57235
   922
  by (subst variance_eq)
hoelzl@57235
   923
     (auto simp: power2_sum power_mult_distrib prob_space variance_eq right_diff_distrib)
hoelzl@57235
   924
hoelzl@47694
   925
definition
hoelzl@47694
   926
  "simple_distributed M X f \<longleftrightarrow> distributed M (count_space (X`space M)) X (\<lambda>x. ereal (f x)) \<and>
hoelzl@47694
   927
    finite (X`space M)"
hoelzl@42902
   928
hoelzl@47694
   929
lemma simple_distributed:
hoelzl@47694
   930
  "simple_distributed M X Px \<Longrightarrow> distributed M (count_space (X`space M)) X Px"
hoelzl@47694
   931
  unfolding simple_distributed_def by auto
hoelzl@42902
   932
hoelzl@47694
   933
lemma simple_distributed_finite[dest]: "simple_distributed M X P \<Longrightarrow> finite (X`space M)"
hoelzl@47694
   934
  by (simp add: simple_distributed_def)
hoelzl@42902
   935
hoelzl@47694
   936
lemma (in prob_space) distributed_simple_function_superset:
hoelzl@47694
   937
  assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X -` {x} \<inter> space M)"
hoelzl@47694
   938
  assumes A: "X`space M \<subseteq> A" "finite A"
hoelzl@47694
   939
  defines "S \<equiv> count_space A" and "P' \<equiv> (\<lambda>x. if x \<in> X`space M then P x else 0)"
hoelzl@47694
   940
  shows "distributed M S X P'"
hoelzl@47694
   941
  unfolding distributed_def
hoelzl@47694
   942
proof safe
hoelzl@47694
   943
  show "(\<lambda>x. ereal (P' x)) \<in> borel_measurable S" unfolding S_def by simp
hoelzl@47694
   944
  show "AE x in S. 0 \<le> ereal (P' x)"
hoelzl@47694
   945
    using X by (auto simp: S_def P'_def simple_distributed_def intro!: measure_nonneg)
hoelzl@47694
   946
  show "distr M S X = density S P'"
hoelzl@47694
   947
  proof (rule measure_eqI_finite)
hoelzl@47694
   948
    show "sets (distr M S X) = Pow A" "sets (density S P') = Pow A"
hoelzl@47694
   949
      using A unfolding S_def by auto
hoelzl@47694
   950
    show "finite A" by fact
hoelzl@47694
   951
    fix a assume a: "a \<in> A"
hoelzl@47694
   952
    then have "a \<notin> X`space M \<Longrightarrow> X -` {a} \<inter> space M = {}" by auto
hoelzl@47694
   953
    with A a X have "emeasure (distr M S X) {a} = P' a"
hoelzl@47694
   954
      by (subst emeasure_distr)
hoelzl@50002
   955
         (auto simp add: S_def P'_def simple_functionD emeasure_eq_measure measurable_count_space_eq2
hoelzl@47694
   956
               intro!: arg_cong[where f=prob])
wenzelm@53015
   957
    also have "\<dots> = (\<integral>\<^sup>+x. ereal (P' a) * indicator {a} x \<partial>S)"
hoelzl@47694
   958
      using A X a
hoelzl@56996
   959
      by (subst nn_integral_cmult_indicator)
hoelzl@47694
   960
         (auto simp: S_def P'_def simple_distributed_def simple_functionD measure_nonneg)
wenzelm@53015
   961
    also have "\<dots> = (\<integral>\<^sup>+x. ereal (P' x) * indicator {a} x \<partial>S)"
hoelzl@56996
   962
      by (auto simp: indicator_def intro!: nn_integral_cong)
hoelzl@47694
   963
    also have "\<dots> = emeasure (density S P') {a}"
hoelzl@47694
   964
      using a A by (intro emeasure_density[symmetric]) (auto simp: S_def)
hoelzl@47694
   965
    finally show "emeasure (distr M S X) {a} = emeasure (density S P') {a}" .
hoelzl@47694
   966
  qed
hoelzl@47694
   967
  show "random_variable S X"
hoelzl@47694
   968
    using X(1) A by (auto simp: measurable_def simple_functionD S_def)
hoelzl@47694
   969
qed
hoelzl@42902
   970
hoelzl@47694
   971
lemma (in prob_space) simple_distributedI:
hoelzl@47694
   972
  assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X -` {x} \<inter> space M)"
hoelzl@47694
   973
  shows "simple_distributed M X P"
hoelzl@47694
   974
  unfolding simple_distributed_def
hoelzl@47694
   975
proof
hoelzl@47694
   976
  have "distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (if x \<in> X`space M then P x else 0))"
hoelzl@47694
   977
    (is "?A")
hoelzl@47694
   978
    using simple_functionD[OF X(1)] by (intro distributed_simple_function_superset[OF X]) auto
hoelzl@47694
   979
  also have "?A \<longleftrightarrow> distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (P x))"
hoelzl@47694
   980
    by (rule distributed_cong_density) auto
hoelzl@47694
   981
  finally show "\<dots>" .
hoelzl@47694
   982
qed (rule simple_functionD[OF X(1)])
hoelzl@47694
   983
hoelzl@47694
   984
lemma simple_distributed_joint_finite:
hoelzl@47694
   985
  assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px"
hoelzl@47694
   986
  shows "finite (X ` space M)" "finite (Y ` space M)"
hoelzl@42902
   987
proof -
hoelzl@47694
   988
  have "finite ((\<lambda>x. (X x, Y x)) ` space M)"
hoelzl@47694
   989
    using X by (auto simp: simple_distributed_def simple_functionD)
hoelzl@47694
   990
  then have "finite (fst ` (\<lambda>x. (X x, Y x)) ` space M)" "finite (snd ` (\<lambda>x. (X x, Y x)) ` space M)"
hoelzl@47694
   991
    by auto
hoelzl@47694
   992
  then show fin: "finite (X ` space M)" "finite (Y ` space M)"
hoelzl@47694
   993
    by (auto simp: image_image)
hoelzl@47694
   994
qed
hoelzl@47694
   995
hoelzl@47694
   996
lemma simple_distributed_joint2_finite:
hoelzl@47694
   997
  assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px"
hoelzl@47694
   998
  shows "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)"
hoelzl@47694
   999
proof -
hoelzl@47694
  1000
  have "finite ((\<lambda>x. (X x, Y x, Z x)) ` space M)"
hoelzl@47694
  1001
    using X by (auto simp: simple_distributed_def simple_functionD)
hoelzl@47694
  1002
  then have "finite (fst ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"
hoelzl@47694
  1003
    "finite ((fst \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"
hoelzl@47694
  1004
    "finite ((snd \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)"
hoelzl@47694
  1005
    by auto
hoelzl@47694
  1006
  then show fin: "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)"
hoelzl@47694
  1007
    by (auto simp: image_image)
hoelzl@42902
  1008
qed
hoelzl@42902
  1009
hoelzl@47694
  1010
lemma simple_distributed_simple_function:
hoelzl@47694
  1011
  "simple_distributed M X Px \<Longrightarrow> simple_function M X"
hoelzl@47694
  1012
  unfolding simple_distributed_def distributed_def
hoelzl@50002
  1013
  by (auto simp: simple_function_def measurable_count_space_eq2)
hoelzl@47694
  1014
hoelzl@47694
  1015
lemma simple_distributed_measure:
hoelzl@47694
  1016
  "simple_distributed M X P \<Longrightarrow> a \<in> X`space M \<Longrightarrow> P a = measure M (X -` {a} \<inter> space M)"
hoelzl@47694
  1017
  using distributed_count_space[of M "X`space M" X P a, symmetric]
hoelzl@47694
  1018
  by (auto simp: simple_distributed_def measure_def)
hoelzl@47694
  1019
hoelzl@47694
  1020
lemma simple_distributed_nonneg: "simple_distributed M X f \<Longrightarrow> x \<in> space M \<Longrightarrow> 0 \<le> f (X x)"
hoelzl@47694
  1021
  by (auto simp: simple_distributed_measure measure_nonneg)
hoelzl@42860
  1022
hoelzl@47694
  1023
lemma (in prob_space) simple_distributed_joint:
hoelzl@47694
  1024
  assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px"
wenzelm@53015
  1025
  defines "S \<equiv> count_space (X`space M) \<Otimes>\<^sub>M count_space (Y`space M)"
hoelzl@47694
  1026
  defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x))`space M then Px x else 0)"
hoelzl@47694
  1027
  shows "distributed M S (\<lambda>x. (X x, Y x)) P"
hoelzl@47694
  1028
proof -
hoelzl@47694
  1029
  from simple_distributed_joint_finite[OF X, simp]
hoelzl@47694
  1030
  have S_eq: "S = count_space (X`space M \<times> Y`space M)"
hoelzl@47694
  1031
    by (simp add: S_def pair_measure_count_space)
hoelzl@47694
  1032
  show ?thesis
hoelzl@47694
  1033
    unfolding S_eq P_def
hoelzl@47694
  1034
  proof (rule distributed_simple_function_superset)
hoelzl@47694
  1035
    show "simple_function M (\<lambda>x. (X x, Y x))"
hoelzl@47694
  1036
      using X by (rule simple_distributed_simple_function)
hoelzl@47694
  1037
    fix x assume "x \<in> (\<lambda>x. (X x, Y x)) ` space M"
hoelzl@47694
  1038
    from simple_distributed_measure[OF X this]
hoelzl@47694
  1039
    show "Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)" .
hoelzl@47694
  1040
  qed auto
hoelzl@47694
  1041
qed
hoelzl@42860
  1042
hoelzl@47694
  1043
lemma (in prob_space) simple_distributed_joint2:
hoelzl@47694
  1044
  assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px"
wenzelm@53015
  1045
  defines "S \<equiv> count_space (X`space M) \<Otimes>\<^sub>M count_space (Y`space M) \<Otimes>\<^sub>M count_space (Z`space M)"
hoelzl@47694
  1046
  defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x))`space M then Px x else 0)"
hoelzl@47694
  1047
  shows "distributed M S (\<lambda>x. (X x, Y x, Z x)) P"
hoelzl@47694
  1048
proof -
hoelzl@47694
  1049
  from simple_distributed_joint2_finite[OF X, simp]
hoelzl@47694
  1050
  have S_eq: "S = count_space (X`space M \<times> Y`space M \<times> Z`space M)"
hoelzl@47694
  1051
    by (simp add: S_def pair_measure_count_space)
hoelzl@47694
  1052
  show ?thesis
hoelzl@47694
  1053
    unfolding S_eq P_def
hoelzl@47694
  1054
  proof (rule distributed_simple_function_superset)
hoelzl@47694
  1055
    show "simple_function M (\<lambda>x. (X x, Y x, Z x))"
hoelzl@47694
  1056
      using X by (rule simple_distributed_simple_function)
hoelzl@47694
  1057
    fix x assume "x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M"
hoelzl@47694
  1058
    from simple_distributed_measure[OF X this]
hoelzl@47694
  1059
    show "Px x = prob ((\<lambda>x. (X x, Y x, Z x)) -` {x} \<inter> space M)" .
hoelzl@47694
  1060
  qed auto
hoelzl@47694
  1061
qed
hoelzl@47694
  1062
hoelzl@47694
  1063
lemma (in prob_space) simple_distributed_setsum_space:
hoelzl@47694
  1064
  assumes X: "simple_distributed M X f"
hoelzl@47694
  1065
  shows "setsum f (X`space M) = 1"
hoelzl@47694
  1066
proof -
hoelzl@47694
  1067
  from X have "setsum f (X`space M) = prob (\<Union>i\<in>X`space M. X -` {i} \<inter> space M)"
hoelzl@47694
  1068
    by (subst finite_measure_finite_Union)
hoelzl@47694
  1069
       (auto simp add: disjoint_family_on_def simple_distributed_measure simple_distributed_simple_function simple_functionD
haftmann@57418
  1070
             intro!: setsum.cong arg_cong[where f="prob"])
hoelzl@47694
  1071
  also have "\<dots> = prob (space M)"
hoelzl@47694
  1072
    by (auto intro!: arg_cong[where f=prob])
hoelzl@47694
  1073
  finally show ?thesis
hoelzl@47694
  1074
    using emeasure_space_1 by (simp add: emeasure_eq_measure one_ereal_def)
hoelzl@47694
  1075
qed
hoelzl@42860
  1076
hoelzl@47694
  1077
lemma (in prob_space) distributed_marginal_eq_joint_simple:
hoelzl@47694
  1078
  assumes Px: "simple_function M X"
hoelzl@47694
  1079
  assumes Py: "simple_distributed M Y Py"
hoelzl@47694
  1080
  assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
  1081
  assumes y: "y \<in> Y`space M"
hoelzl@47694
  1082
  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)"
hoelzl@47694
  1083
proof -
hoelzl@47694
  1084
  note Px = simple_distributedI[OF Px refl]
hoelzl@47694
  1085
  have *: "\<And>f A. setsum (\<lambda>x. max 0 (ereal (f x))) A = ereal (setsum (\<lambda>x. max 0 (f x)) A)"
hoelzl@47694
  1086
    by (simp add: setsum_ereal[symmetric] zero_ereal_def)
hoelzl@49788
  1087
  from distributed_marginal_eq_joint2[OF
hoelzl@49788
  1088
    sigma_finite_measure_count_space_finite
hoelzl@49788
  1089
    sigma_finite_measure_count_space_finite
hoelzl@49788
  1090
    simple_distributed[OF Py] simple_distributed_joint[OF Pxy],
hoelzl@47694
  1091
    OF Py[THEN simple_distributed_finite] Px[THEN simple_distributed_finite]]
hoelzl@49788
  1092
    y
hoelzl@49788
  1093
    Px[THEN simple_distributed_finite]
hoelzl@49788
  1094
    Py[THEN simple_distributed_finite]
hoelzl@47694
  1095
    Pxy[THEN simple_distributed, THEN distributed_real_AE]
hoelzl@47694
  1096
  show ?thesis
hoelzl@47694
  1097
    unfolding AE_count_space
haftmann@57418
  1098
    apply (auto simp add: nn_integral_count_space_finite * intro!: setsum.cong split: split_max)
hoelzl@47694
  1099
    done
hoelzl@47694
  1100
qed
hoelzl@42860
  1101
hoelzl@50419
  1102
lemma distributedI_real:
hoelzl@50419
  1103
  fixes f :: "'a \<Rightarrow> real"
hoelzl@50419
  1104
  assumes gen: "sets M1 = sigma_sets (space M1) E" and "Int_stable E"
hoelzl@50419
  1105
    and A: "range A \<subseteq> E" "(\<Union>i::nat. A i) = space M1" "\<And>i. emeasure (distr M M1 X) (A i) \<noteq> \<infinity>"
hoelzl@50419
  1106
    and X: "X \<in> measurable M M1"
hoelzl@50419
  1107
    and f: "f \<in> borel_measurable M1" "AE x in M1. 0 \<le> f x"
wenzelm@53015
  1108
    and eq: "\<And>A. A \<in> E \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^sup>+ x. f x * indicator A x \<partial>M1)"
hoelzl@50419
  1109
  shows "distributed M M1 X f"
hoelzl@50419
  1110
  unfolding distributed_def
hoelzl@50419
  1111
proof (intro conjI)
hoelzl@50419
  1112
  show "distr M M1 X = density M1 f"
hoelzl@50419
  1113
  proof (rule measure_eqI_generator_eq[where A=A])
hoelzl@50419
  1114
    { fix A assume A: "A \<in> E"
hoelzl@50419
  1115
      then have "A \<in> sigma_sets (space M1) E" by auto
hoelzl@50419
  1116
      then have "A \<in> sets M1"
hoelzl@50419
  1117
        using gen by simp
hoelzl@50419
  1118
      with f A eq[of A] X show "emeasure (distr M M1 X) A = emeasure (density M1 f) A"
hoelzl@50419
  1119
        by (simp add: emeasure_distr emeasure_density borel_measurable_ereal
hoelzl@50419
  1120
                      times_ereal.simps[symmetric] ereal_indicator
hoelzl@50419
  1121
                 del: times_ereal.simps) }
hoelzl@50419
  1122
    note eq_E = this
hoelzl@50419
  1123
    show "Int_stable E" by fact
hoelzl@50419
  1124
    { fix e assume "e \<in> E"
hoelzl@50419
  1125
      then have "e \<in> sigma_sets (space M1) E" by auto
hoelzl@50419
  1126
      then have "e \<in> sets M1" unfolding gen .
hoelzl@50419
  1127
      then have "e \<subseteq> space M1" by (rule sets.sets_into_space) }
hoelzl@50419
  1128
    then show "E \<subseteq> Pow (space M1)" by auto
hoelzl@50419
  1129
    show "sets (distr M M1 X) = sigma_sets (space M1) E"
hoelzl@50419
  1130
      "sets (density M1 (\<lambda>x. ereal (f x))) = sigma_sets (space M1) E"
hoelzl@50419
  1131
      unfolding gen[symmetric] by auto
hoelzl@50419
  1132
  qed fact+
hoelzl@50419
  1133
qed (insert X f, auto)
hoelzl@50419
  1134
hoelzl@50419
  1135
lemma distributedI_borel_atMost:
hoelzl@50419
  1136
  fixes f :: "real \<Rightarrow> real"
hoelzl@50419
  1137
  assumes [measurable]: "X \<in> borel_measurable M"
hoelzl@50419
  1138
    and [measurable]: "f \<in> borel_measurable borel" and f[simp]: "AE x in lborel. 0 \<le> f x"
wenzelm@53015
  1139
    and g_eq: "\<And>a. (\<integral>\<^sup>+x. f x * indicator {..a} x \<partial>lborel)  = ereal (g a)"
hoelzl@50419
  1140
    and M_eq: "\<And>a. emeasure M {x\<in>space M. X x \<le> a} = ereal (g a)"
hoelzl@50419
  1141
  shows "distributed M lborel X f"
hoelzl@50419
  1142
proof (rule distributedI_real)
hoelzl@57447
  1143
  show "sets (lborel::real measure) = sigma_sets (space lborel) (range atMost)"
hoelzl@50419
  1144
    by (simp add: borel_eq_atMost)
hoelzl@50419
  1145
  show "Int_stable (range atMost :: real set set)"
hoelzl@50419
  1146
    by (auto simp: Int_stable_def)
hoelzl@50419
  1147
  have vimage_eq: "\<And>a. (X -` {..a} \<inter> space M) = {x\<in>space M. X x \<le> a}" by auto
hoelzl@50419
  1148
  def A \<equiv> "\<lambda>i::nat. {.. real i}"
hoelzl@50419
  1149
  then show "range A \<subseteq> range atMost" "(\<Union>i. A i) = space lborel"
hoelzl@50419
  1150
    "\<And>i. emeasure (distr M lborel X) (A i) \<noteq> \<infinity>"
hoelzl@50419
  1151
    by (auto simp: real_arch_simple emeasure_distr vimage_eq M_eq)
hoelzl@50419
  1152
hoelzl@50419
  1153
  fix A :: "real set" assume "A \<in> range atMost"
hoelzl@50419
  1154
  then obtain a where A: "A = {..a}" by auto
wenzelm@53015
  1155
  show "emeasure M (X -` A \<inter> space M) = (\<integral>\<^sup>+x. f x * indicator A x \<partial>lborel)"
hoelzl@50419
  1156
    unfolding vimage_eq A M_eq g_eq ..
hoelzl@50419
  1157
qed auto
hoelzl@50419
  1158
hoelzl@50419
  1159
lemma (in prob_space) uniform_distributed_params:
hoelzl@50419
  1160
  assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)"
hoelzl@50419
  1161
  shows "A \<in> sets MX" "measure MX A \<noteq> 0"
hoelzl@50419
  1162
proof -
hoelzl@50419
  1163
  interpret X: prob_space "distr M MX X"
hoelzl@50419
  1164
    using distributed_measurable[OF X] by (rule prob_space_distr)
hoelzl@50419
  1165
hoelzl@50419
  1166
  show "measure MX A \<noteq> 0"
hoelzl@50419
  1167
  proof
hoelzl@50419
  1168
    assume "measure MX A = 0"
hoelzl@50419
  1169
    with X.emeasure_space_1 X.prob_space distributed_distr_eq_density[OF X]
hoelzl@50419
  1170
    show False
hoelzl@50419
  1171
      by (simp add: emeasure_density zero_ereal_def[symmetric])
hoelzl@50419
  1172
  qed
hoelzl@50419
  1173
  with measure_notin_sets[of A MX] show "A \<in> sets MX"
hoelzl@50419
  1174
    by blast
hoelzl@50419
  1175
qed
hoelzl@50419
  1176
hoelzl@47694
  1177
lemma prob_space_uniform_measure:
hoelzl@47694
  1178
  assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>"
hoelzl@47694
  1179
  shows "prob_space (uniform_measure M A)"
hoelzl@47694
  1180
proof
hoelzl@47694
  1181
  show "emeasure (uniform_measure M A) (space (uniform_measure M A)) = 1"
hoelzl@47694
  1182
    using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)], of "space M"]
immler@50244
  1183
    using sets.sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A
hoelzl@47694
  1184
    by (simp add: Int_absorb2 emeasure_nonneg)
hoelzl@47694
  1185
qed
hoelzl@47694
  1186
hoelzl@47694
  1187
lemma prob_space_uniform_count_measure: "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> prob_space (uniform_count_measure A)"
wenzelm@61169
  1188
  by standard (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def)
hoelzl@42860
  1189
hoelzl@59000
  1190
lemma (in prob_space) measure_uniform_measure_eq_cond_prob:
hoelzl@59000
  1191
  assumes [measurable]: "Measurable.pred M P" "Measurable.pred M Q"
hoelzl@59000
  1192
  shows "\<P>(x in uniform_measure M {x\<in>space M. Q x}. P x) = \<P>(x in M. P x \<bar> Q x)"
hoelzl@59000
  1193
proof cases
hoelzl@59000
  1194
  assume Q: "measure M {x\<in>space M. Q x} = 0"
hoelzl@59000
  1195
  then have "AE x in M. \<not> Q x"
hoelzl@59000
  1196
    by (simp add: prob_eq_0)
hoelzl@59000
  1197
  then have "AE x in M. indicator {x\<in>space M. Q x} x / ereal 0 = 0"
hoelzl@59000
  1198
    by (auto split: split_indicator)
hoelzl@59000
  1199
  from density_cong[OF _ _ this] show ?thesis
hoelzl@59000
  1200
    by (simp add: uniform_measure_def emeasure_eq_measure cond_prob_def Q measure_density_const)
hoelzl@59000
  1201
qed (auto simp add: emeasure_eq_measure cond_prob_def intro!: arg_cong[where f=prob])
hoelzl@59000
  1202
hoelzl@59000
  1203
lemma prob_space_point_measure:
hoelzl@59000
  1204
  "finite S \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> 0 \<le> p s) \<Longrightarrow> (\<Sum>s\<in>S. p s) = 1 \<Longrightarrow> prob_space (point_measure S p)"
hoelzl@59000
  1205
  by (rule prob_spaceI) (simp add: space_point_measure emeasure_point_measure_finite)
hoelzl@59000
  1206
hoelzl@61359
  1207
lemma (in prob_space) distr_pair_fst: "distr (N \<Otimes>\<^sub>M M) N fst = N"
hoelzl@61359
  1208
proof (intro measure_eqI)
hoelzl@61359
  1209
  fix A assume A: "A \<in> sets (distr (N \<Otimes>\<^sub>M M) N fst)"
hoelzl@61359
  1210
  from A have "emeasure (distr (N \<Otimes>\<^sub>M M) N fst) A = emeasure (N \<Otimes>\<^sub>M M) (A \<times> space M)"
hoelzl@61359
  1211
    by (auto simp add: emeasure_distr space_pair_measure dest: sets.sets_into_space intro!: arg_cong2[where f=emeasure])
hoelzl@61359
  1212
  with A show "emeasure (distr (N \<Otimes>\<^sub>M M) N fst) A = emeasure N A"
hoelzl@61359
  1213
    by (simp add: emeasure_pair_measure_Times emeasure_space_1)
hoelzl@61359
  1214
qed simp
hoelzl@61359
  1215
hoelzl@61359
  1216
lemma (in product_prob_space) distr_reorder:
hoelzl@61359
  1217
  assumes "inj_on t J" "t \<in> J \<rightarrow> K" "finite K"
hoelzl@61359
  1218
  shows "distr (PiM K M) (Pi\<^sub>M J (\<lambda>x. M (t x))) (\<lambda>\<omega>. \<lambda>n\<in>J. \<omega> (t n)) = PiM J (\<lambda>x. M (t x))"
hoelzl@61359
  1219
proof (rule product_sigma_finite.PiM_eqI)
hoelzl@61359
  1220
  show "product_sigma_finite (\<lambda>x. M (t x))" ..
hoelzl@61359
  1221
  have "t`J \<subseteq> K" using assms by auto
hoelzl@61359
  1222
  then show [simp]: "finite J"
hoelzl@61359
  1223
    by (rule finite_imageD[OF finite_subset]) fact+
hoelzl@61359
  1224
  fix A assume A: "\<And>i. i \<in> J \<Longrightarrow> A i \<in> sets (M (t i))"
hoelzl@61359
  1225
  moreover have "((\<lambda>\<omega>. \<lambda>n\<in>J. \<omega> (t n)) -` Pi\<^sub>E J A \<inter> space (Pi\<^sub>M K M)) =
hoelzl@61359
  1226
    (\<Pi>\<^sub>E i\<in>K. if i \<in> t`J then A (the_inv_into J t i) else space (M i))"
hoelzl@61359
  1227
    using A A[THEN sets.sets_into_space] \<open>t \<in> J \<rightarrow> K\<close> \<open>inj_on t J\<close>
hoelzl@61359
  1228
    by (subst prod_emb_Pi[symmetric]) (auto simp: space_PiM PiE_iff the_inv_into_f_f prod_emb_def)
hoelzl@61359
  1229
  ultimately show "distr (Pi\<^sub>M K M) (Pi\<^sub>M J (\<lambda>x. M (t x))) (\<lambda>\<omega>. \<lambda>n\<in>J. \<omega> (t n)) (Pi\<^sub>E J A) = (\<Prod>i\<in>J. M (t i) (A i))"
hoelzl@61359
  1230
    using assms
hoelzl@61359
  1231
    apply (subst emeasure_distr)
hoelzl@61359
  1232
    apply (auto intro!: sets_PiM_I_finite simp: Pi_iff)
hoelzl@61359
  1233
    apply (subst emeasure_PiM)
hoelzl@61359
  1234
    apply (auto simp: the_inv_into_f_f \<open>inj_on t J\<close> setprod.reindex[OF \<open>inj_on t J\<close>]
hoelzl@61359
  1235
      if_distrib[where f="emeasure (M _)"] setprod.If_cases emeasure_space_1 Int_absorb1 \<open>t`J \<subseteq> K\<close>)
hoelzl@61359
  1236
    done
hoelzl@61359
  1237
qed simp
hoelzl@61359
  1238
hoelzl@61359
  1239
lemma (in product_prob_space) distr_restrict:
hoelzl@61359
  1240
  "J \<subseteq> K \<Longrightarrow> finite K \<Longrightarrow> (\<Pi>\<^sub>M i\<in>J. M i) = distr (\<Pi>\<^sub>M i\<in>K. M i) (\<Pi>\<^sub>M i\<in>J. M i) (\<lambda>f. restrict f J)"
hoelzl@61359
  1241
  using distr_reorder[of "\<lambda>x. x" J K] by (simp add: Pi_iff subset_eq)
hoelzl@61359
  1242
hoelzl@61359
  1243
lemma (in product_prob_space) emeasure_prod_emb[simp]:
hoelzl@61359
  1244
  assumes L: "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^sub>M J M)"
hoelzl@61359
  1245
  shows "emeasure (Pi\<^sub>M L M) (prod_emb L M J X) = emeasure (Pi\<^sub>M J M) X"
hoelzl@61359
  1246
  by (subst distr_restrict[OF L])
hoelzl@61359
  1247
     (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
hoelzl@61359
  1248
hoelzl@61359
  1249
lemma emeasure_distr_restrict:
hoelzl@61359
  1250
  assumes "I \<subseteq> K" and Q[measurable_cong]: "sets Q = sets (PiM K M)" and A[measurable]: "A \<in> sets (PiM I M)"
hoelzl@61359
  1251
  shows "emeasure (distr Q (PiM I M) (\<lambda>\<omega>. restrict \<omega> I)) A = emeasure Q (prod_emb K M I A)"
hoelzl@61359
  1252
  using \<open>I\<subseteq>K\<close> sets_eq_imp_space_eq[OF Q]
hoelzl@61359
  1253
  by (subst emeasure_distr)
hoelzl@61359
  1254
     (auto simp: measurable_cong_sets[OF Q] prod_emb_def space_PiM[symmetric] intro!: measurable_restrict)
hoelzl@61359
  1255
hoelzl@35582
  1256
end