src/HOL/Probability/Projective_Family.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 62026 ea3b1b0413b4
child 62975 1d066f6ab25d
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
immler@50042
     1
(*  Title:      HOL/Probability/Projective_Family.thy
immler@50042
     2
    Author:     Fabian Immler, TU München
immler@50042
     3
    Author:     Johannes Hölzl, TU München
immler@50042
     4
*)
immler@50042
     5
wenzelm@61808
     6
section \<open>Projective Family\<close>
immler@50042
     7
immler@50039
     8
theory Projective_Family
hoelzl@61359
     9
imports Finite_Product_Measure Giry_Monad
immler@50039
    10
begin
immler@50039
    11
hoelzl@61359
    12
lemma vimage_restrict_preseve_mono:
hoelzl@61359
    13
  assumes J: "J \<subseteq> I"
hoelzl@61359
    14
  and sets: "A \<subseteq> (\<Pi>\<^sub>E i\<in>J. S i)" "B \<subseteq> (\<Pi>\<^sub>E i\<in>J. S i)" and ne: "(\<Pi>\<^sub>E i\<in>I. S i) \<noteq> {}"
hoelzl@61359
    15
  and eq: "(\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^sub>E i\<in>I. S i) \<subseteq> (\<lambda>x. restrict x J) -` B \<inter> (\<Pi>\<^sub>E i\<in>I. S i)"
hoelzl@61359
    16
  shows "A \<subseteq> B"
hoelzl@61359
    17
proof  (intro subsetI)
hoelzl@61359
    18
  fix x assume "x \<in> A"
hoelzl@61359
    19
  from ne obtain y where y: "\<And>i. i \<in> I \<Longrightarrow> y i \<in> S i" by auto
hoelzl@61359
    20
  have "J \<inter> (I - J) = {}" by auto
hoelzl@61359
    21
  show "x \<in> B"
hoelzl@61359
    22
  proof cases
hoelzl@61359
    23
    assume x: "x \<in> (\<Pi>\<^sub>E i\<in>J. S i)"
hoelzl@61359
    24
    have "merge J (I - J) (x,y) \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^sub>E i\<in>I. S i)"
wenzelm@61808
    25
      using y x \<open>J \<subseteq> I\<close> PiE_cancel_merge[of "J" "I - J" x y S] \<open>x\<in>A\<close>
hoelzl@61359
    26
      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
hoelzl@61359
    27
    also have "\<dots> \<subseteq> (\<lambda>x. restrict x J) -` B \<inter> (\<Pi>\<^sub>E i\<in>I. S i)" by fact
hoelzl@61359
    28
    finally show "x \<in> B"
wenzelm@61808
    29
      using y x \<open>J \<subseteq> I\<close> PiE_cancel_merge[of "J" "I - J" x y S] \<open>x\<in>A\<close> eq
hoelzl@61359
    30
      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
hoelzl@61359
    31
  qed (insert \<open>x\<in>A\<close> sets, auto)
immler@50087
    32
qed
immler@50087
    33
immler@50039
    34
locale projective_family =
hoelzl@61359
    35
  fixes I :: "'i set" and P :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M :: "'i \<Rightarrow> 'a measure"
hoelzl@61359
    36
  assumes P: "\<And>J H. J \<subseteq> H \<Longrightarrow> finite H \<Longrightarrow> H \<subseteq> I \<Longrightarrow> P J = distr (P H) (PiM J M) (\<lambda>f. restrict f J)"
hoelzl@61359
    37
  assumes prob_space_P: "\<And>J. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> prob_space (P J)"
immler@50039
    38
begin
immler@50039
    39
hoelzl@61359
    40
lemma sets_P: "finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> sets (P J) = sets (PiM J M)"
hoelzl@61359
    41
  by (subst P[of J J]) simp_all
hoelzl@61359
    42
hoelzl@61359
    43
lemma space_P: "finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> space (P J) = space (PiM J M)"
hoelzl@61359
    44
  using sets_P by (rule sets_eq_imp_space_eq)
immler@50039
    45
hoelzl@61359
    46
lemma not_empty_M: "i \<in> I \<Longrightarrow> space (M i) \<noteq> {}"
hoelzl@61359
    47
  using prob_space_P[THEN prob_space.not_empty] by (auto simp: space_PiM space_P)
immler@50039
    48
hoelzl@61359
    49
lemma not_empty: "space (PiM I M) \<noteq> {}"
hoelzl@61359
    50
  by (simp add: not_empty_M)
immler@50039
    51
hoelzl@50124
    52
abbreviation
hoelzl@61359
    53
  "emb L K \<equiv> prod_emb L M K"
hoelzl@50124
    54
hoelzl@61359
    55
lemma emb_preserve_mono:
hoelzl@61359
    56
  assumes "J \<subseteq> L" "L \<subseteq> I" and sets: "X \<in> sets (Pi\<^sub>M J M)" "Y \<in> sets (Pi\<^sub>M J M)"
hoelzl@61359
    57
  assumes "emb L J X \<subseteq> emb L J Y"
hoelzl@61359
    58
  shows "X \<subseteq> Y"
hoelzl@61359
    59
proof (rule vimage_restrict_preseve_mono)
wenzelm@53015
    60
  show "X \<subseteq> (\<Pi>\<^sub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^sub>E i\<in>J. space (M i))"
immler@50244
    61
    using sets[THEN sets.sets_into_space] by (auto simp: space_PiM)
hoelzl@61359
    62
  show "(\<Pi>\<^sub>E i\<in>L. space (M i)) \<noteq> {}"
hoelzl@61359
    63
    using \<open>L \<subseteq> I\<close> by (auto simp add: not_empty_M space_PiM[symmetric])
hoelzl@61359
    64
  show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^sub>E i\<in>L. space (M i)) \<subseteq> (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^sub>E i\<in>L. space (M i))"
wenzelm@61808
    65
    using \<open>prod_emb L M J X \<subseteq> prod_emb L M J Y\<close> by (simp add: prod_emb_def)
immler@50042
    66
qed fact
immler@50042
    67
hoelzl@61359
    68
lemma emb_injective:
hoelzl@61359
    69
  assumes L: "J \<subseteq> L" "L \<subseteq> I" and X: "X \<in> sets (Pi\<^sub>M J M)" and Y: "Y \<in> sets (Pi\<^sub>M J M)"
hoelzl@61359
    70
  shows "emb L J X = emb L J Y \<Longrightarrow> X = Y"
hoelzl@61359
    71
  by (intro antisym emb_preserve_mono[OF L X Y] emb_preserve_mono[OF L Y X]) auto
hoelzl@61359
    72
hoelzl@61359
    73
lemma emeasure_P: "J \<subseteq> K \<Longrightarrow> finite K \<Longrightarrow> K \<subseteq> I \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow> P K (emb K J X) = P J X"
hoelzl@61359
    74
  by (auto intro!: emeasure_distr_restrict[symmetric] simp: P sets_P)
immler@50042
    75
hoelzl@61359
    76
inductive_set generator :: "('i \<Rightarrow> 'a) set set" where
hoelzl@61359
    77
  "finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> emb I J X \<in> generator"
hoelzl@61359
    78
hoelzl@61359
    79
lemma algebra_generator: "algebra (space (PiM I M)) generator"
hoelzl@61359
    80
  unfolding algebra_iff_Int
hoelzl@61359
    81
proof (safe elim!: generator.cases)
hoelzl@61359
    82
  fix J X assume J: "finite J" "J \<subseteq> I" and X: "X \<in> sets (PiM J M)"
hoelzl@61359
    83
hoelzl@61359
    84
  from X[THEN sets.sets_into_space] J show "x \<in> emb I J X \<Longrightarrow> x \<in> space (PiM I M)" for x
hoelzl@61359
    85
    by (auto simp: prod_emb_def space_PiM)
immler@50042
    86
hoelzl@61359
    87
  have "emb I J (space (PiM J M) - X) \<in> generator"
hoelzl@61359
    88
    by (intro generator.intros J sets.Diff sets.top X)
hoelzl@61359
    89
  with J show "space (Pi\<^sub>M I M) - emb I J X \<in> generator"
hoelzl@61359
    90
    by (simp add: space_PiM prod_emb_PiE)
hoelzl@61359
    91
  
hoelzl@61359
    92
  fix K Y assume K: "finite K" "K \<subseteq> I" and Y: "Y \<in> sets (PiM K M)"
hoelzl@61359
    93
  have "emb I (J \<union> K) (emb (J \<union> K) J X) \<inter> emb I (J \<union> K) (emb (J \<union> K) K Y) \<in> generator"
hoelzl@61359
    94
    unfolding prod_emb_Int[symmetric]
hoelzl@61359
    95
    by (intro generator.intros sets.Int measurable_prod_emb) (auto intro!: J K X Y)
hoelzl@61359
    96
  with J K X Y show "emb I J X \<inter> emb I K Y \<in> generator"
hoelzl@61359
    97
    by simp
hoelzl@61359
    98
qed (force simp: generator.simps prod_emb_empty[symmetric])
immler@50042
    99
wenzelm@61605
   100
interpretation generator: algebra "space (PiM I M)" generator
hoelzl@61359
   101
  by (rule algebra_generator)
immler@50042
   102
hoelzl@61359
   103
lemma sets_PiM_generator: "sets (PiM I M) = sigma_sets (space (PiM I M)) generator"
hoelzl@61359
   104
proof (intro antisym sets.sigma_sets_subset)
hoelzl@61359
   105
  show "sets (PiM I M) \<subseteq> sigma_sets (space (PiM I M)) generator"
hoelzl@61359
   106
    unfolding sets_PiM_single space_PiM[symmetric]
hoelzl@61359
   107
  proof (intro sigma_sets_mono', safe)
hoelzl@61359
   108
    fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
hoelzl@61359
   109
    then have "{f \<in> space (Pi\<^sub>M I M). f i \<in> A} = emb I {i} (\<Pi>\<^sub>E j\<in>{i}. A)"
hoelzl@61359
   110
      by (auto simp: prod_emb_def space_PiM restrict_def Pi_iff PiE_iff extensional_def)
hoelzl@61359
   111
    with \<open>i\<in>I\<close> A show "{f \<in> space (Pi\<^sub>M I M). f i \<in> A} \<in> generator"
hoelzl@61359
   112
      by (auto intro!: generator.intros sets_PiM_I_finite)
hoelzl@61359
   113
  qed
hoelzl@61359
   114
qed (auto elim!: generator.cases)
immler@50042
   115
wenzelm@50252
   116
definition mu_G ("\<mu>G") where
hoelzl@61359
   117
  "\<mu>G A = (THE x. \<forall>J\<subseteq>I. finite J \<longrightarrow> (\<forall>X\<in>sets (Pi\<^sub>M J M). A = emb I J X \<longrightarrow> x = emeasure (P J) X))"
hoelzl@61359
   118
hoelzl@61359
   119
definition lim :: "('i \<Rightarrow> 'a) measure" where
hoelzl@61359
   120
  "lim = extend_measure (space (PiM I M)) generator (\<lambda>x. x) \<mu>G"
hoelzl@61359
   121
hoelzl@61359
   122
lemma space_lim[simp]: "space lim = space (PiM I M)"
hoelzl@61359
   123
  using generator.space_closed
hoelzl@61359
   124
  unfolding lim_def by (intro space_extend_measure) simp
hoelzl@61359
   125
hoelzl@61359
   126
lemma sets_lim[simp, measurable]: "sets lim = sets (PiM I M)"
hoelzl@61359
   127
  using generator.space_closed by (simp add: lim_def sets_PiM_generator sets_extend_measure)
immler@50042
   128
wenzelm@50252
   129
lemma mu_G_spec:
hoelzl@61359
   130
  assumes J: "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^sub>M J M)"
hoelzl@61359
   131
  shows "\<mu>G (emb I J X) = emeasure (P J) X"
wenzelm@50252
   132
  unfolding mu_G_def
immler@50042
   133
proof (intro the_equality allI impI ballI)
hoelzl@61359
   134
  fix K Y assume K: "finite K" "K \<subseteq> I" "Y \<in> sets (Pi\<^sub>M K M)"
hoelzl@61359
   135
    and [simp]: "emb I J X = emb I K Y"
hoelzl@61359
   136
  have "emeasure (P K) Y = emeasure (P (K \<union> J)) (emb (K \<union> J) K Y)"
hoelzl@61359
   137
    using K J by (simp add: emeasure_P)
immler@50042
   138
  also have "emb (K \<union> J) K Y = emb (K \<union> J) J X"
hoelzl@61359
   139
    using K J by (simp add: emb_injective[of "K \<union> J" I])
hoelzl@61359
   140
  also have "emeasure (P (K \<union> J)) (emb (K \<union> J) J X) = emeasure (P J) X"
hoelzl@61359
   141
    using K J by (subst emeasure_P) simp_all
hoelzl@61359
   142
  finally show "emeasure (P J) X = emeasure (P K) Y" ..
immler@50042
   143
qed (insert J, force)
immler@50042
   144
hoelzl@61359
   145
lemma positive_mu_G: "positive generator \<mu>G"
hoelzl@61359
   146
proof -
hoelzl@61359
   147
  show ?thesis
hoelzl@61359
   148
  proof (safe intro!: positive_def[THEN iffD2])
hoelzl@61359
   149
    obtain J where "finite J" "J \<subseteq> I" by auto
hoelzl@61359
   150
    then have "\<mu>G (emb I J {}) = 0"
hoelzl@61359
   151
      by (subst mu_G_spec) auto
hoelzl@61359
   152
    then show "\<mu>G {} = 0" by simp
hoelzl@61359
   153
  qed (auto simp: mu_G_spec elim!: generator.cases)
hoelzl@61359
   154
qed
immler@50042
   155
hoelzl@61359
   156
lemma additive_mu_G: "additive generator \<mu>G"
hoelzl@61359
   157
proof (safe intro!: additive_def[THEN iffD2] elim!: generator.cases)
hoelzl@61359
   158
  fix J X K Y assume J: "finite J" "J \<subseteq> I" "X \<in> sets (PiM J M)"
hoelzl@61359
   159
    and K: "finite K" "K \<subseteq> I" "Y \<in> sets (PiM K M)"
hoelzl@61359
   160
    and "emb I J X \<inter> emb I K Y = {}"
hoelzl@61359
   161
  then have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
hoelzl@61359
   162
    by (intro emb_injective[of "J \<union> K" I _ "{}"]) (auto simp: sets.Int prod_emb_Int)
hoelzl@61359
   163
  have "\<mu>G (emb I J X \<union> emb I K Y) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
hoelzl@61359
   164
    using J K by simp
hoelzl@61359
   165
  also have "\<dots> = emeasure (P (J \<union> K)) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
hoelzl@61359
   166
    using J K by (simp add: mu_G_spec sets.Un del: prod_emb_Un)
hoelzl@61359
   167
  also have "\<dots> = \<mu>G (emb I J X) + \<mu>G (emb I K Y)"
hoelzl@61359
   168
    using J K JK_disj by (simp add: plus_emeasure[symmetric] mu_G_spec emeasure_P sets_P)
hoelzl@61359
   169
  finally show "\<mu>G (emb I J X \<union> emb I K Y) = \<mu>G (emb I J X) + \<mu>G (emb I K Y)" .
immler@50042
   170
qed
immler@50042
   171
hoelzl@61359
   172
lemma emeasure_lim:
hoelzl@61359
   173
  assumes JX: "finite J" "J \<subseteq> I" "X \<in> sets (PiM J M)"
hoelzl@61359
   174
  assumes cont: "\<And>J X. (\<And>i. J i \<subseteq> I) \<Longrightarrow> incseq J \<Longrightarrow> (\<And>i. finite (J i)) \<Longrightarrow> (\<And>i. X i \<in> sets (PiM (J i) M)) \<Longrightarrow>
hoelzl@61359
   175
    decseq (\<lambda>i. emb I (J i) (X i)) \<Longrightarrow> 0 < (INF i. P (J i) (X i)) \<Longrightarrow> (\<Inter>i. emb I (J i) (X i)) \<noteq> {}"
hoelzl@61359
   176
  shows "emeasure lim (emb I J X) = P J X"
immler@50042
   177
proof -
hoelzl@61359
   178
  have "\<exists>\<mu>. (\<forall>s\<in>generator. \<mu> s = \<mu>G s) \<and>
hoelzl@61359
   179
    measure_space (space (PiM I M)) (sigma_sets (space (PiM I M)) generator) \<mu>"
hoelzl@61359
   180
  proof (rule generator.caratheodory_empty_continuous[OF positive_mu_G additive_mu_G])
hoelzl@61359
   181
    show "\<And>A. A \<in> generator \<Longrightarrow> \<mu>G A \<noteq> \<infinity>"
hoelzl@61359
   182
    proof (clarsimp elim!: generator.cases simp: mu_G_spec del: notI)
hoelzl@61359
   183
      fix J assume "finite J" "J \<subseteq> I"
hoelzl@61359
   184
      then interpret prob_space "P J" by (rule prob_space_P)
hoelzl@61359
   185
      show "\<And>X. X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> emeasure (P J) X \<noteq> \<infinity>"
hoelzl@61359
   186
        by simp
hoelzl@61359
   187
    qed
hoelzl@61359
   188
  next
hoelzl@61359
   189
    fix A assume "range A \<subseteq> generator" and "decseq A" "(\<Inter>i. A i) = {}"
hoelzl@61359
   190
    then have "\<forall>i. \<exists>J X. A i = emb I J X \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (PiM J M)"
hoelzl@61359
   191
      unfolding image_subset_iff generator.simps by blast
hoelzl@61359
   192
    then obtain J X where A: "\<And>i. A i = emb I (J i) (X i)"
hoelzl@61359
   193
      and *: "\<And>i. finite (J i)" "\<And>i. J i \<subseteq> I" "\<And>i. X i \<in> sets (PiM (J i) M)"
hoelzl@61359
   194
      by metis
hoelzl@61359
   195
    have "(INF i. P (J i) (X i)) = 0"
hoelzl@61359
   196
    proof (rule ccontr)
hoelzl@61359
   197
      assume INF_P: "(INF i. P (J i) (X i)) \<noteq> 0"
hoelzl@61359
   198
      have "(\<Inter>i. emb I (\<Union>n\<le>i. J n) (emb (\<Union>n\<le>i. J n) (J i) (X i))) \<noteq> {}"
hoelzl@61359
   199
      proof (rule cont)
hoelzl@61359
   200
        show "decseq (\<lambda>i. emb I (\<Union>n\<le>i. J n) (emb (\<Union>n\<le>i. J n) (J i) (X i)))"
hoelzl@61359
   201
          using * \<open>decseq A\<close> by (subst prod_emb_trans) (auto simp: A[abs_def])
hoelzl@61359
   202
        show "0 < (INF i. P (\<Union>n\<le>i. J n) (emb (\<Union>n\<le>i. J n) (J i) (X i)))"
hoelzl@61359
   203
           using * INF_P by (subst emeasure_P) (auto simp: less_le intro!: INF_greatest)
hoelzl@61359
   204
        show "incseq (\<lambda>i. \<Union>n\<le>i. J n)"
hoelzl@61359
   205
          by (force simp: incseq_def)
hoelzl@61359
   206
      qed (insert *, auto)
hoelzl@61359
   207
      with \<open>(\<Inter>i. A i) = {}\<close> * show False
hoelzl@61359
   208
        by (subst (asm) prod_emb_trans) (auto simp: A[abs_def])
hoelzl@61359
   209
    qed
wenzelm@61969
   210
    moreover have "(\<lambda>i. P (J i) (X i)) \<longlonglongrightarrow> (INF i. P (J i) (X i))"
hoelzl@61359
   211
    proof (intro LIMSEQ_INF antimonoI)
hoelzl@61359
   212
      fix x y :: nat assume "x \<le> y"
hoelzl@61359
   213
      have "P (J y \<union> J x) (emb (J y \<union> J x) (J y) (X y)) \<le> P (J y \<union> J x) (emb (J y \<union> J x) (J x) (X x))"
hoelzl@61359
   214
        using \<open>decseq A\<close>[THEN decseqD, OF \<open>x\<le>y\<close>] *
hoelzl@61359
   215
        by (auto simp: A sets_P del: subsetI intro!: emeasure_mono  \<open>x \<le> y\<close>
hoelzl@61359
   216
              emb_preserve_mono[of "J y \<union> J x" I, where X="emb (J y \<union> J x) (J y) (X y)"])
hoelzl@61359
   217
      then show "P (J y) (X y) \<le> P (J x) (X x)"
hoelzl@61359
   218
        using * by (simp add: emeasure_P)
hoelzl@61359
   219
    qed
wenzelm@61969
   220
    ultimately show "(\<lambda>i. \<mu>G (A i)) \<longlonglongrightarrow> 0"
hoelzl@61359
   221
      by (auto simp: A[abs_def] mu_G_spec *)
hoelzl@61359
   222
  qed
hoelzl@61359
   223
  then obtain \<mu> where eq: "\<forall>s\<in>generator. \<mu> s = \<mu>G s"
hoelzl@61359
   224
    and ms: "measure_space (space (PiM I M)) (sets (PiM I M)) \<mu>"
hoelzl@61359
   225
    by (metis sets_PiM_generator)
immler@50042
   226
  show ?thesis
hoelzl@61359
   227
  proof (subst emeasure_extend_measure[OF lim_def])
hoelzl@61359
   228
    show "A \<in> generator \<Longrightarrow> \<mu> A = \<mu>G A" for A
hoelzl@61359
   229
      using eq by simp
hoelzl@61359
   230
    show "positive (sets lim) \<mu>" "countably_additive (sets lim) \<mu>"
hoelzl@61359
   231
      using ms by (auto simp add: measure_space_def)
hoelzl@61359
   232
    show "(\<lambda>x. x) ` generator \<subseteq> Pow (space (Pi\<^sub>M I M))"
hoelzl@61359
   233
      using generator.space_closed by simp
hoelzl@61359
   234
    show "emb I J X \<in> generator" "\<mu>G (emb I J X) = emeasure (P J) X"
hoelzl@61359
   235
      using JX by (auto intro: generator.intros simp: mu_G_spec)
immler@50042
   236
  qed
immler@50042
   237
qed
immler@50042
   238
immler@50039
   239
end
immler@50039
   240
immler@50087
   241
sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M
hoelzl@61359
   242
  unfolding projective_family_def
hoelzl@61359
   243
proof (intro conjI allI impI distr_restrict)
hoelzl@61359
   244
  show "\<And>J. finite J \<Longrightarrow> prob_space (Pi\<^sub>M J M)"
hoelzl@61359
   245
    by (intro prob_spaceI) (simp add: space_PiM emeasure_PiM emeasure_space_1)
hoelzl@61359
   246
qed auto
hoelzl@61359
   247
hoelzl@61359
   248
hoelzl@61359
   249
txt \<open> Proof due to Ionescu Tulcea. \<close>
hoelzl@61359
   250
hoelzl@61359
   251
locale Ionescu_Tulcea =
hoelzl@61359
   252
  fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a measure" and M :: "nat \<Rightarrow> 'a measure"
hoelzl@61359
   253
  assumes P[measurable]: "\<And>i. P i \<in> measurable (PiM {0..<i} M) (subprob_algebra (M i))"
hoelzl@61359
   254
  assumes prob_space_P: "\<And>i x. x \<in> space (PiM {0..<i} M) \<Longrightarrow> prob_space (P i x)"
hoelzl@61359
   255
begin
hoelzl@61359
   256
hoelzl@61359
   257
lemma non_empty[simp]: "space (M i) \<noteq> {}"
hoelzl@61359
   258
proof (induction i rule: less_induct)
hoelzl@61359
   259
  case (less i)
hoelzl@61359
   260
  then obtain x where "\<And>j. j < i \<Longrightarrow> x j \<in> space (M j)"
hoelzl@61359
   261
    unfolding ex_in_conv[symmetric] by metis
hoelzl@61359
   262
  then have *: "restrict x {0..<i} \<in> space (PiM {0..<i} M)"
hoelzl@61359
   263
    by (auto simp: space_PiM PiE_iff)
hoelzl@61359
   264
  then interpret prob_space "P i (restrict x {0..<i})"
hoelzl@61359
   265
    by (rule prob_space_P)
hoelzl@61359
   266
  show ?case
hoelzl@61359
   267
    using not_empty subprob_measurableD(1)[OF P, OF *] by simp
hoelzl@61359
   268
qed
hoelzl@61359
   269
hoelzl@61359
   270
lemma space_PiM_not_empty[simp]: "space (PiM UNIV M) \<noteq> {}"
hoelzl@61359
   271
  unfolding space_PiM_empty_iff by auto
hoelzl@61359
   272
hoelzl@61359
   273
lemma space_P: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> space (P n x) = space (M n)"
hoelzl@61359
   274
  by (simp add: P[THEN subprob_measurableD(1)])
hoelzl@61359
   275
hoelzl@61359
   276
lemma sets_P[measurable_cong]: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> sets (P n x) = sets (M n)"
hoelzl@61359
   277
  by (simp add: P[THEN subprob_measurableD(2)])
hoelzl@61359
   278
hoelzl@61359
   279
definition eP :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
hoelzl@61359
   280
  "eP n \<omega> = distr (P n \<omega>) (PiM {0..<Suc n} M) (fun_upd \<omega> n)"
hoelzl@61359
   281
hoelzl@61359
   282
lemma measurable_eP[measurable]:
hoelzl@61359
   283
  "eP n \<in> measurable (PiM {0..< n} M) (subprob_algebra (PiM {0..<Suc n} M))"
hoelzl@61359
   284
  by (auto simp: eP_def[abs_def] measurable_split_conv
hoelzl@61359
   285
           intro!: measurable_fun_upd[where J="{0..<n}"] measurable_distr2[OF _ P])
hoelzl@61359
   286
hoelzl@61359
   287
lemma space_eP:
hoelzl@61359
   288
  "x \<in> space (PiM {0..<n} M) \<Longrightarrow> space (eP n x) = space (PiM {0..<Suc n} M)"
hoelzl@61359
   289
  by (simp add: measurable_eP[THEN subprob_measurableD(1)])
hoelzl@61359
   290
hoelzl@61359
   291
lemma sets_eP[measurable]:
hoelzl@61359
   292
  "x \<in> space (PiM {0..<n} M) \<Longrightarrow> sets (eP n x) = sets (PiM {0..<Suc n} M)"
hoelzl@61359
   293
  by (simp add: measurable_eP[THEN subprob_measurableD(2)])
hoelzl@61359
   294
hoelzl@61359
   295
lemma prob_space_eP: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> prob_space (eP n x)"
hoelzl@61359
   296
  unfolding eP_def
hoelzl@61359
   297
  by (intro prob_space.prob_space_distr prob_space_P measurable_fun_upd[where J="{0..<n}"]) auto
hoelzl@61359
   298
hoelzl@61359
   299
lemma nn_integral_eP:
hoelzl@61359
   300
  "\<omega> \<in> space (PiM {0..<n} M) \<Longrightarrow> f \<in> borel_measurable (PiM {0..<Suc n} M) \<Longrightarrow>
hoelzl@61359
   301
    (\<integral>\<^sup>+x. f x \<partial>eP n \<omega>) = (\<integral>\<^sup>+x. f (\<omega>(n := x)) \<partial>P n \<omega>)"
hoelzl@61359
   302
  unfolding eP_def
hoelzl@61359
   303
  by (subst nn_integral_distr) (auto intro!: measurable_fun_upd[where J="{0..<n}"] simp: space_PiM PiE_iff)
hoelzl@61359
   304
hoelzl@61359
   305
lemma emeasure_eP:
hoelzl@61359
   306
  assumes \<omega>[simp]: "\<omega> \<in> space (PiM {0..<n} M)" and A[measurable]: "A \<in> sets (PiM {0..<Suc n} M)"
hoelzl@61359
   307
  shows "eP n \<omega> A = P n \<omega> ((\<lambda>x. \<omega>(n := x)) -` A \<inter> space (M n))"
hoelzl@61359
   308
  using nn_integral_eP[of \<omega> n "indicator A"]
hoelzl@61359
   309
  apply (simp add: sets_eP nn_integral_indicator[symmetric] sets_P del: nn_integral_indicator)
hoelzl@61359
   310
  apply (subst nn_integral_indicator[symmetric])
hoelzl@61359
   311
  using measurable_sets[OF measurable_fun_upd[OF _ measurable_const[OF \<omega>] measurable_id] A, of n]
hoelzl@61359
   312
  apply (auto simp add: sets_P atLeastLessThanSuc space_P simp del: nn_integral_indicator
hoelzl@61359
   313
     intro!: nn_integral_cong split: split_indicator)
hoelzl@61359
   314
  done
hoelzl@61359
   315
  
hoelzl@61359
   316
hoelzl@61359
   317
primrec C :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
hoelzl@61359
   318
  "C n 0 \<omega> = return (PiM {0..<n} M) \<omega>"
wenzelm@62026
   319
| "C n (Suc m) \<omega> = C n m \<omega> \<bind> eP (n + m)"
hoelzl@61359
   320
hoelzl@61359
   321
lemma measurable_C[measurable]:
hoelzl@61359
   322
  "C n m \<in> measurable (PiM {0..<n} M) (subprob_algebra (PiM {0..<n + m} M))"
hoelzl@61359
   323
  by (induction m) auto
hoelzl@61359
   324
hoelzl@61359
   325
lemma space_C:
hoelzl@61359
   326
  "x \<in> space (PiM {0..<n} M) \<Longrightarrow> space (C n m x) = space (PiM {0..<n + m} M)"
hoelzl@61359
   327
  by (simp add: measurable_C[THEN subprob_measurableD(1)])
hoelzl@61359
   328
hoelzl@61359
   329
lemma sets_C[measurable_cong]:
hoelzl@61359
   330
  "x \<in> space (PiM {0..<n} M) \<Longrightarrow> sets (C n m x) = sets (PiM {0..<n + m} M)"
hoelzl@61359
   331
  by (simp add: measurable_C[THEN subprob_measurableD(2)])
hoelzl@61359
   332
hoelzl@61359
   333
lemma prob_space_C: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> prob_space (C n m x)"
hoelzl@61359
   334
proof (induction m)
hoelzl@61359
   335
  case (Suc m) then show ?case
hoelzl@61359
   336
    by (auto intro!: prob_space.prob_space_bind[where S="PiM {0..<Suc (n + m)} M"]
hoelzl@61359
   337
             simp: space_C prob_space_eP)
hoelzl@61359
   338
qed (auto intro!: prob_space_return simp: space_PiM)
hoelzl@61359
   339
hoelzl@61359
   340
lemma split_C:
wenzelm@62026
   341
  assumes \<omega>: "\<omega> \<in> space (PiM {0..<n} M)" shows "(C n m \<omega> \<bind> C (n + m) l) = C n (m + l) \<omega>"
hoelzl@61359
   342
proof (induction l)
hoelzl@61359
   343
  case 0
hoelzl@61359
   344
  with \<omega> show ?case
hoelzl@61359
   345
    by (simp add: bind_return_distr' prob_space_C[THEN prob_space.not_empty]
hoelzl@61359
   346
                  distr_cong[OF refl sets_C[symmetric, OF \<omega>]])
hoelzl@61359
   347
next
hoelzl@61359
   348
  case (Suc l) with \<omega> show ?case
hoelzl@61359
   349
    by (simp add: bind_assoc[symmetric, OF _ measurable_eP]) (simp add: ac_simps)
hoelzl@61359
   350
qed
hoelzl@61359
   351
hoelzl@61359
   352
lemma nn_integral_C:
hoelzl@61359
   353
  assumes "m \<le> m'" and f[measurable]: "f \<in> borel_measurable (PiM {0..<n+m} M)"
hoelzl@61359
   354
    and nonneg: "\<And>x. x \<in> space (PiM {0..<n+m} M) \<Longrightarrow> 0 \<le> f x"
hoelzl@61359
   355
    and x: "x \<in> space (PiM {0..<n} M)"
hoelzl@61359
   356
  shows "(\<integral>\<^sup>+x. f x \<partial>C n m x) = (\<integral>\<^sup>+x. f (restrict x {0..<n+m}) \<partial>C n m' x)"
hoelzl@61359
   357
  using \<open>m \<le> m'\<close>
hoelzl@61359
   358
proof (induction rule: dec_induct)
hoelzl@61359
   359
  case (step i)
hoelzl@61359
   360
  let ?E = "\<lambda>x. f (restrict x {0..<n + m})" and ?C = "\<lambda>i f. \<integral>\<^sup>+x. f x \<partial>C n i x"
hoelzl@61359
   361
  from \<open>m\<le>i\<close> x have "?C i ?E = ?C (Suc i) ?E"
hoelzl@61359
   362
    by (auto simp: nn_integral_bind[where B="PiM {0 ..< Suc (n + i)} M"] space_C nn_integral_eP
hoelzl@61359
   363
             intro!: nn_integral_cong)
hoelzl@61359
   364
       (simp add: space_PiM PiE_iff  nonneg prob_space.emeasure_space_1[OF prob_space_P])
hoelzl@61359
   365
  with step show ?case by (simp del: restrict_apply)
hoelzl@61359
   366
qed (auto simp: space_PiM space_C[OF x] simp del: restrict_apply intro!: nn_integral_cong)
hoelzl@61359
   367
hoelzl@61359
   368
lemma emeasure_C:
hoelzl@61359
   369
  assumes "m \<le> m'" and A[measurable]: "A \<in> sets (PiM {0..<n+m} M)" and [simp]: "x \<in> space (PiM {0..<n} M)"
hoelzl@61359
   370
  shows "emeasure (C n m' x) (prod_emb {0..<n + m'} M {0..<n+m} A) = emeasure (C n m x) A"
hoelzl@61359
   371
  using assms
hoelzl@61359
   372
  by (subst (1 2) nn_integral_indicator[symmetric])
hoelzl@61359
   373
     (auto intro!: nn_integral_cong split: split_indicator simp del: nn_integral_indicator
hoelzl@61359
   374
           simp: nn_integral_C[of m m' _ n] prod_emb_iff space_PiM PiE_iff sets_C space_C)
hoelzl@61359
   375
hoelzl@61359
   376
lemma distr_C:
hoelzl@61359
   377
  assumes "m \<le> m'" and [simp]: "x \<in> space (PiM {0..<n} M)"
hoelzl@61359
   378
  shows "C n m x = distr (C n m' x) (PiM {0..<n+m} M) (\<lambda>x. restrict x {0..<n+m})"
hoelzl@61359
   379
proof (rule measure_eqI)
hoelzl@61359
   380
  fix A assume "A \<in> sets (C n m x)"
hoelzl@61359
   381
  with \<open>m \<le> m'\<close> show "emeasure (C n m x) A = emeasure (distr (C n m' x) (Pi\<^sub>M {0..<n + m} M) (\<lambda>x. restrict x {0..<n + m})) A"
hoelzl@61359
   382
    by (subst emeasure_C[symmetric, OF \<open>m \<le> m'\<close>]) (auto intro!: emeasure_distr_restrict[symmetric] simp: sets_C)
hoelzl@61359
   383
qed (simp add: sets_C)
hoelzl@61359
   384
hoelzl@61359
   385
definition up_to :: "nat set \<Rightarrow> nat" where
hoelzl@61359
   386
  "up_to J = (LEAST n. \<forall>i\<ge>n. i \<notin> J)"
hoelzl@61359
   387
hoelzl@61359
   388
lemma up_to_less: "finite J \<Longrightarrow> i \<in> J \<Longrightarrow> i < up_to J"
hoelzl@61359
   389
  unfolding up_to_def
hoelzl@61359
   390
  by (rule LeastI2[of _ "Suc (Max J)"]) (auto simp: Suc_le_eq not_le[symmetric])
hoelzl@61359
   391
hoelzl@61359
   392
lemma up_to_iff: "finite J \<Longrightarrow> up_to J \<le> n \<longleftrightarrow> (\<forall>i\<in>J. i < n)"
hoelzl@61359
   393
proof safe
hoelzl@61359
   394
  show "finite J \<Longrightarrow> up_to J \<le> n \<Longrightarrow> i \<in> J \<Longrightarrow> i < n" for i
hoelzl@61359
   395
    using up_to_less[of J i] by auto
hoelzl@61359
   396
qed (auto simp: up_to_def intro!: Least_le)
hoelzl@61359
   397
hoelzl@61359
   398
lemma up_to_iff_Ico: "finite J \<Longrightarrow> up_to J \<le> n \<longleftrightarrow> J \<subseteq> {0..<n}"
hoelzl@61359
   399
  by (auto simp: up_to_iff)
hoelzl@61359
   400
hoelzl@61359
   401
lemma up_to: "finite J \<Longrightarrow> J \<subseteq> {0..< up_to J}"
hoelzl@61359
   402
  by (auto simp: up_to_less)
hoelzl@61359
   403
hoelzl@61359
   404
lemma up_to_mono: "J \<subseteq> H \<Longrightarrow> finite H \<Longrightarrow> up_to J \<le> up_to H"
hoelzl@61359
   405
  by (auto simp add: up_to_iff finite_subset up_to_less)
hoelzl@61359
   406
hoelzl@61359
   407
definition CI :: "nat set \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
hoelzl@61359
   408
  "CI J = distr (C 0 (up_to J) (\<lambda>x. undefined)) (PiM J M) (\<lambda>f. restrict f J)"
hoelzl@61359
   409
wenzelm@61605
   410
sublocale PF: projective_family UNIV CI
hoelzl@61359
   411
  unfolding projective_family_def
hoelzl@61359
   412
proof safe
hoelzl@61359
   413
  show "finite J \<Longrightarrow> prob_space (CI J)" for J
hoelzl@61359
   414
    using up_to[of J] unfolding CI_def
hoelzl@61359
   415
    by (intro prob_space.prob_space_distr prob_space_C measurable_restrict) auto
hoelzl@61359
   416
  note measurable_cong_sets[OF sets_C, simp]
hoelzl@61359
   417
  have [simp]: "J \<subseteq> H \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M H M) (Pi\<^sub>M J M)" for H J
hoelzl@61359
   418
    by (auto intro!: measurable_restrict)
hoelzl@61359
   419
hoelzl@61359
   420
  show "J \<subseteq> H \<Longrightarrow> finite H \<Longrightarrow> CI J = distr (CI H) (Pi\<^sub>M J M) (\<lambda>f. restrict f J)" for J H
hoelzl@61359
   421
    by (simp add: CI_def distr_C[OF up_to_mono[of J H]] up_to up_to_mono distr_distr comp_def
hoelzl@61359
   422
                  inf.absorb2 finite_subset)
hoelzl@61359
   423
qed
hoelzl@61359
   424
hoelzl@61359
   425
lemma emeasure_CI':
hoelzl@61359
   426
  "finite J \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow> CI J X = C 0 (up_to J) (\<lambda>_. undefined) (PF.emb {0..<up_to J} J X)"
hoelzl@61359
   427
  unfolding CI_def using up_to[of J] by (rule emeasure_distr_restrict) (auto simp: sets_C)
hoelzl@61359
   428
hoelzl@61359
   429
lemma emeasure_CI:
hoelzl@61359
   430
  "J \<subseteq> {0..<n} \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow> CI J X = C 0 n (\<lambda>_. undefined) (PF.emb {0..<n} J X)"
hoelzl@61359
   431
  apply (subst emeasure_CI', simp_all add: finite_subset)
hoelzl@61359
   432
  apply (subst emeasure_C[symmetric, of "up_to J" n])
hoelzl@61359
   433
  apply (auto simp: finite_subset up_to_iff_Ico up_to_less)
hoelzl@61359
   434
  apply (subst prod_emb_trans)
hoelzl@61359
   435
  apply (auto simp: up_to_less finite_subset up_to_iff_Ico)
hoelzl@61359
   436
  done
hoelzl@61359
   437
hoelzl@61359
   438
lemma lim:
hoelzl@61359
   439
  assumes J: "finite J" and X: "X \<in> sets (PiM J M)"
hoelzl@61359
   440
  shows "emeasure PF.lim (PF.emb UNIV J X) = emeasure (CI J) X"
hoelzl@61359
   441
proof (rule PF.emeasure_lim[OF J subset_UNIV X])
hoelzl@61359
   442
  fix J X' assume J[simp]: "\<And>i. finite (J i)" and X'[measurable]: "\<And>i. X' i \<in> sets (Pi\<^sub>M (J i) M)"
hoelzl@61359
   443
    and dec: "decseq (\<lambda>i. PF.emb UNIV (J i) (X' i))"
hoelzl@61359
   444
  def X \<equiv> "\<lambda>n. (\<Inter>i\<in>{i. J i \<subseteq> {0..< n}}. PF.emb {0..<n} (J i) (X' i)) \<inter> space (PiM {0..<n} M)"
hoelzl@61359
   445
hoelzl@61359
   446
  have sets_X[measurable]: "X n \<in> sets (PiM {0..<n} M)" for n
hoelzl@61359
   447
    by (cases "{i. J i \<subseteq> {0..< n}} = {}")
hoelzl@61359
   448
       (simp_all add: X_def, auto intro!: sets.countable_INT' sets.Int)
hoelzl@61359
   449
  
hoelzl@61359
   450
  have dec_X: "n \<le> m \<Longrightarrow> X m \<subseteq> PF.emb {0..<m} {0..<n} (X n)" for n m
hoelzl@61359
   451
    unfolding X_def using ivl_subset[of 0 n 0 m]
hoelzl@61359
   452
    by (cases "{i. J i \<subseteq> {0..< n}} = {}")
hoelzl@61359
   453
       (auto simp add: prod_emb_Int prod_emb_PiE space_PiM simp del: ivl_subset)
hoelzl@61359
   454
hoelzl@61359
   455
  have dec_X': "PF.emb {0..<n} (J j) (X' j) \<subseteq> PF.emb {0..<n} (J i) (X' i)"
hoelzl@61359
   456
    if [simp]: "J i \<subseteq> {0..<n}" "J j \<subseteq> {0..<n}" "i \<le> j" for n i j
hoelzl@61359
   457
    by (rule PF.emb_preserve_mono[of "{0..<n}" UNIV]) (auto del: subsetI intro: dec[THEN antimonoD])
hoelzl@61359
   458
hoelzl@61359
   459
  assume "0 < (INF i. CI (J i) (X' i))"
hoelzl@61359
   460
  also have "\<dots> \<le> (INF i. C 0 i (\<lambda>x. undefined) (X i))"
hoelzl@61359
   461
  proof (intro INF_greatest)
hoelzl@61359
   462
    fix n
wenzelm@61605
   463
    interpret C: prob_space "C 0 n (\<lambda>x. undefined)"
hoelzl@61359
   464
      by (rule prob_space_C) simp
hoelzl@61359
   465
    show "(INF i. CI (J i) (X' i)) \<le> C 0 n (\<lambda>x. undefined) (X n)"
hoelzl@61359
   466
    proof cases
hoelzl@61359
   467
      assume "{i. J i \<subseteq> {0..< n}} = {}" with C.emeasure_space_1  show ?thesis
hoelzl@61359
   468
        by (auto simp add: X_def space_C intro!: INF_lower2[of 0] prob_space.measure_le_1 PF.prob_space_P)
hoelzl@61359
   469
    next
hoelzl@61359
   470
      assume *: "{i. J i \<subseteq> {0..< n}} \<noteq> {}"
hoelzl@61359
   471
      have "(INF i. CI (J i) (X' i)) \<le>
hoelzl@61359
   472
          (INF i:{i. J i \<subseteq> {0..<n}}. C 0 n (\<lambda>_. undefined) (PF.emb {0..<n} (J i) (X' i)))"
hoelzl@61359
   473
        by (intro INF_superset_mono) (auto simp: emeasure_CI)
hoelzl@61359
   474
      also have "\<dots> = C 0 n (\<lambda>_. undefined) (\<Inter>i\<in>{i. J i \<subseteq> {0..<n}}. (PF.emb {0..<n} (J i) (X' i)))"
hoelzl@61359
   475
        using * by (intro emeasure_INT_decseq_subset[symmetric]) (auto intro!: dec_X' del: subsetI simp: sets_C)
hoelzl@61359
   476
      also have "\<dots> = C 0 n (\<lambda>_. undefined) (X n)"
hoelzl@61359
   477
        using * by (auto simp add: X_def INT_extend_simps)
hoelzl@61359
   478
      finally show "(INF i. CI (J i) (X' i)) \<le> C 0 n (\<lambda>_. undefined) (X n)" .
hoelzl@61359
   479
    qed
hoelzl@57447
   480
  qed
hoelzl@61359
   481
  finally have pos: "0 < (INF i. C 0 i (\<lambda>x. undefined) (X i))" .
hoelzl@61359
   482
  from less_INF_D[OF this, of 0] have "X 0 \<noteq> {}"
hoelzl@61359
   483
    by auto
hoelzl@61359
   484
hoelzl@61359
   485
  { fix \<omega> n assume \<omega>: "\<omega> \<in> space (PiM {0..<n} M)"
hoelzl@61359
   486
    let ?C = "\<lambda>i. emeasure (C n i \<omega>) (X (n + i))"
hoelzl@61359
   487
    let ?C' = "\<lambda>i x. emeasure (C (Suc n) i (\<omega>(n:=x))) (X (Suc n + i))"
hoelzl@61359
   488
    have M: "\<And>i. ?C' i \<in> borel_measurable (P n \<omega>)"
hoelzl@61359
   489
      using \<omega>[measurable, simp] measurable_fun_upd[where J="{0..<n}"] by measurable auto
hoelzl@61359
   490
hoelzl@61359
   491
    assume "0 < (INF i. ?C i)"
hoelzl@61359
   492
    also have "\<dots> \<le> (INF i. emeasure (C n (1 + i) \<omega>) (X (n + (1 + i))))"
hoelzl@61359
   493
      by (intro INF_greatest INF_lower) auto
hoelzl@61359
   494
    also have "\<dots> = (INF i. \<integral>\<^sup>+x. ?C' i x \<partial>P n \<omega>)"
hoelzl@61359
   495
      using \<omega> measurable_C[of "Suc n"]
hoelzl@61359
   496
      apply (intro INF_cong refl)
hoelzl@61359
   497
      apply (subst split_C[symmetric, OF \<omega>])
hoelzl@61359
   498
      apply (subst emeasure_bind[OF _ _ sets_X])
hoelzl@61359
   499
      apply (simp_all del: C.simps add: space_C)
hoelzl@61359
   500
      apply measurable
hoelzl@61359
   501
      apply simp
hoelzl@61359
   502
      apply (simp add: bind_return[OF measurable_eP] nn_integral_eP)
hoelzl@61359
   503
      done
hoelzl@61359
   504
    also have "\<dots> = (\<integral>\<^sup>+x. (INF i. ?C' i x) \<partial>P n \<omega>)"
hoelzl@61359
   505
    proof (rule nn_integral_monotone_convergence_INF[symmetric])
hoelzl@61359
   506
      have "(\<integral>\<^sup>+x. ?C' 0 x \<partial>P n \<omega>) \<le> (\<integral>\<^sup>+x. 1 \<partial>P n \<omega>)"
hoelzl@61359
   507
        by (intro nn_integral_mono) (auto split: split_indicator)
hoelzl@61359
   508
      also have "\<dots> < \<infinity>"
hoelzl@61359
   509
        using prob_space_P[OF \<omega>, THEN prob_space.emeasure_space_1] by simp
hoelzl@61359
   510
      finally show "(\<integral>\<^sup>+x. ?C' 0 x \<partial>P n \<omega>) < \<infinity>" .
hoelzl@61359
   511
    next
hoelzl@61359
   512
      fix i j :: nat and x assume "i \<le> j" "x \<in> space (P n \<omega>)"
hoelzl@61359
   513
      with \<omega> have \<omega>': "\<omega>(n := x) \<in> space (PiM {0..<Suc n} M)"
hoelzl@61359
   514
        by (auto simp: space_P[OF \<omega>] space_PiM PiE_iff extensional_def)
hoelzl@61359
   515
      show "?C' j x \<le> ?C' i x"
hoelzl@61359
   516
        using \<open>i \<le> j\<close> by (subst emeasure_C[symmetric, of i]) (auto intro!: emeasure_mono dec_X del: subsetI simp: sets_C space_P \<omega> \<omega>')
hoelzl@61359
   517
    qed fact
hoelzl@61359
   518
    finally have "(\<integral>\<^sup>+x. (INF i. ?C' i x) \<partial>P n \<omega>) \<noteq> 0"
hoelzl@61359
   519
      by simp
hoelzl@61359
   520
    then have "\<exists>\<^sub>F x in ae_filter (P n \<omega>). 0 < (INF i. ?C' i x)"
hoelzl@61359
   521
       using M by (subst (asm) nn_integral_0_iff_AE)
hoelzl@61359
   522
         (auto intro!: borel_measurable_INF simp: Filter.not_eventually not_le)
hoelzl@61359
   523
    then have "\<exists>\<^sub>F x in ae_filter (P n \<omega>). x \<in> space (M n) \<and> 0 < (INF i. ?C' i x)"
hoelzl@61359
   524
      by (rule frequently_mp[rotated]) (auto simp: space_P \<omega>)
hoelzl@61359
   525
    then obtain x where "x \<in> space (M n)" "0 < (INF i. ?C' i x)"
hoelzl@61359
   526
      by (auto dest: frequently_ex)
hoelzl@61359
   527
    from this(2)[THEN less_INF_D, of 0] this(2)
hoelzl@61359
   528
    have "\<exists>x. \<omega>(n := x) \<in> X (Suc n) \<and> 0 < (INF i. ?C' i x)"
hoelzl@61359
   529
      by (intro exI[of _ x]) (simp split: split_indicator_asm) }
hoelzl@61359
   530
  note step = this
hoelzl@61359
   531
hoelzl@61359
   532
  let ?\<omega> = "\<lambda>\<omega> n x. (restrict \<omega> {0..<n})(n := x)"
hoelzl@61359
   533
  let ?L = "\<lambda>\<omega> n r. INF i. emeasure (C (Suc n) i (?\<omega> \<omega> n r)) (X (Suc n + i))"
hoelzl@61359
   534
  have *: "(\<And>i. i < n \<Longrightarrow> ?\<omega> \<omega> i (\<omega> i) \<in> X (Suc i)) \<Longrightarrow>
hoelzl@61359
   535
    restrict \<omega> {0..<n} \<in> space (Pi\<^sub>M {0..<n} M)" for \<omega> n
hoelzl@61359
   536
    using sets.sets_into_space[OF sets_X, of n]
hoelzl@61359
   537
    by (cases n) (auto simp: atLeastLessThanSuc restrict_def[of _ "{}"])
hoelzl@61359
   538
  have "\<exists>\<omega>. \<forall>n. ?\<omega> \<omega> n (\<omega> n) \<in> X (Suc n) \<and> 0 < ?L \<omega> n (\<omega> n)"
hoelzl@61359
   539
  proof (rule dependent_wellorder_choice)
hoelzl@61359
   540
    fix n \<omega> assume IH: "\<And>i. i < n \<Longrightarrow> ?\<omega> \<omega> i (\<omega> i) \<in> X (Suc i) \<and> 0 < ?L \<omega> i (\<omega> i)"
hoelzl@61359
   541
    show "\<exists>r. ?\<omega> \<omega> n r \<in> X (Suc n) \<and> 0 < ?L \<omega> n r"
hoelzl@61359
   542
    proof (rule step)
hoelzl@61359
   543
      show "restrict \<omega> {0..<n} \<in> space (Pi\<^sub>M {0..<n} M)"
hoelzl@61359
   544
        using IH[THEN conjunct1] by (rule *)
hoelzl@61359
   545
      show "0 < (INF i. emeasure (C n i (restrict \<omega> {0..<n})) (X (n + i)))"
hoelzl@61359
   546
      proof (cases n)
hoelzl@61359
   547
        case 0 with pos show ?thesis
hoelzl@61359
   548
          by (simp add: CI_def restrict_def)
hoelzl@61359
   549
      next
hoelzl@61359
   550
        case (Suc i) then show ?thesis
hoelzl@61359
   551
          using IH[of i, THEN conjunct2] by (simp add: atLeastLessThanSuc)
hoelzl@61359
   552
      qed
hoelzl@61359
   553
    qed
hoelzl@61359
   554
  qed (simp cong: restrict_cong)
hoelzl@61359
   555
  then obtain \<omega> where \<omega>: "\<And>n. ?\<omega> \<omega> n (\<omega> n) \<in> X (Suc n)"
hoelzl@61359
   556
    by auto
hoelzl@61359
   557
  from this[THEN *] have \<omega>_space: "\<omega> \<in> space (PiM UNIV M)"
hoelzl@61359
   558
    by (auto simp: space_PiM PiE_iff Ball_def)
hoelzl@61359
   559
  have *: "\<omega> \<in> PF.emb UNIV {0..<n} (X n)" for n
hoelzl@61359
   560
  proof (cases n)
hoelzl@61359
   561
    case 0 with \<omega>_space \<open>X 0 \<noteq> {}\<close> sets.sets_into_space[OF sets_X, of 0] show ?thesis
hoelzl@61359
   562
      by (auto simp add: space_PiM prod_emb_def restrict_def PiE_iff)
hoelzl@61359
   563
  next
hoelzl@61359
   564
    case (Suc i) then show ?thesis
hoelzl@61359
   565
      using \<omega>[of i] \<omega>_space by (auto simp: prod_emb_def space_PiM PiE_iff atLeastLessThanSuc)
hoelzl@61359
   566
  qed
hoelzl@61359
   567
  have **: "{i. J i \<subseteq> {0..<up_to (J n)}} \<noteq> {}" for n
hoelzl@61359
   568
    by (auto intro!: exI[of _ n] up_to J)
hoelzl@61359
   569
  have "\<omega> \<in> PF.emb UNIV (J n) (X' n)" for n
hoelzl@61359
   570
    using *[of "up_to (J n)"] up_to[of "J n"] by (simp add: X_def prod_emb_Int prod_emb_INT[OF **])
hoelzl@61359
   571
  then show "(\<Inter>i. PF.emb UNIV (J i) (X' i)) \<noteq> {}"
hoelzl@61359
   572
    by auto
hoelzl@61359
   573
qed
hoelzl@61359
   574
hoelzl@61359
   575
lemma distr_lim: assumes J[simp]: "finite J" shows "distr PF.lim (PiM J M) (\<lambda>x. restrict x J) = CI J"
hoelzl@61359
   576
  apply (rule measure_eqI)
hoelzl@61359
   577
  apply (simp add: CI_def)
hoelzl@61359
   578
  apply (simp add: emeasure_distr measurable_cong_sets[OF PF.sets_lim] lim[symmetric] prod_emb_def space_PiM)
hoelzl@61359
   579
  done
hoelzl@61359
   580
hoelzl@61359
   581
end
hoelzl@61359
   582
hoelzl@61359
   583
lemma (in product_prob_space) emeasure_lim_emb:
hoelzl@61359
   584
  assumes *: "finite J" "J \<subseteq> I" "X \<in> sets (PiM J M)"
hoelzl@61359
   585
  shows "emeasure lim (emb I J X) = emeasure (Pi\<^sub>M J M) X"
hoelzl@61359
   586
proof (rule emeasure_lim[OF *], goal_cases)
hoelzl@61359
   587
  case (1 J X)
hoelzl@61359
   588
  
hoelzl@61359
   589
  have "\<exists>Q. (\<forall>i. sets Q = PiM (\<Union>i. J i) M \<and> distr Q (PiM (J i) M) (\<lambda>x. restrict x (J i)) = Pi\<^sub>M (J i) M)"
hoelzl@61359
   590
  proof cases
hoelzl@61359
   591
    assume "finite (\<Union>i. J i)"
hoelzl@61359
   592
    then have "distr (PiM (\<Union>i. J i) M) (Pi\<^sub>M (J i) M) (\<lambda>x. restrict x (J i)) = Pi\<^sub>M (J i) M" for i
hoelzl@61359
   593
      by (intro distr_restrict[symmetric]) auto
hoelzl@61359
   594
    then show ?thesis
hoelzl@61359
   595
      by auto
hoelzl@61359
   596
  next
hoelzl@61359
   597
    assume inf: "infinite (\<Union>i. J i)"
hoelzl@61359
   598
    moreover have count: "countable (\<Union>i. J i)"
hoelzl@61359
   599
      using 1(3) by (auto intro: countable_finite)
hoelzl@61359
   600
    def f \<equiv> "from_nat_into (\<Union>i. J i)" and t \<equiv> "to_nat_on (\<Union>i. J i)"
hoelzl@61359
   601
    have ft[simp]: "x \<in> J i \<Longrightarrow> f (t x) = x" for x i
hoelzl@61359
   602
      unfolding f_def t_def using inf count by (intro from_nat_into_to_nat_on) auto
hoelzl@61359
   603
    have tf[simp]: "t (f i) = i" for i
hoelzl@61359
   604
      unfolding t_def f_def by (intro to_nat_on_from_nat_into_infinite inf count)
hoelzl@61359
   605
    have inj_t: "inj_on t (\<Union>i. J i)"
hoelzl@61359
   606
      using count by (auto simp: t_def)
hoelzl@61359
   607
    then have inj_t_J: "inj_on t (J i)" for i
hoelzl@61359
   608
      by (rule subset_inj_on) auto
wenzelm@61605
   609
    interpret IT: Ionescu_Tulcea "\<lambda>i \<omega>. M (f i)" "\<lambda>i. M (f i)"
hoelzl@61359
   610
      by standard auto
wenzelm@61605
   611
    interpret Mf: product_prob_space "\<lambda>x. M (f x)" UNIV
hoelzl@61359
   612
      by standard
hoelzl@61359
   613
    have C_eq_PiM: "IT.C 0 n (\<lambda>_. undefined) = PiM {0..<n} (\<lambda>x. M (f x))" for n
hoelzl@61359
   614
    proof (induction n)
hoelzl@61359
   615
      case 0 then show ?case
hoelzl@61359
   616
        by (auto simp: PiM_empty intro!: measure_eqI dest!: subset_singletonD)
hoelzl@61359
   617
    next
hoelzl@61359
   618
      case (Suc n) then show ?case
hoelzl@61359
   619
        apply (auto intro!: measure_eqI simp: sets_bind[OF IT.sets_eP] emeasure_bind[OF _ IT.measurable_eP])
hoelzl@61359
   620
        apply (auto simp: Mf.product_nn_integral_insert nn_integral_indicator[symmetric] atLeastLessThanSuc IT.emeasure_eP space_PiM
hoelzl@61359
   621
                    split: split_indicator simp del: nn_integral_indicator intro!: nn_integral_cong)
hoelzl@61359
   622
        done
hoelzl@61359
   623
    qed
hoelzl@61359
   624
    have CI_eq_PiM: "IT.CI X = PiM X (\<lambda>x. M (f x))" if X: "finite X" for X
hoelzl@61359
   625
      by (auto simp: IT.up_to_less X  IT.CI_def C_eq_PiM intro!: Mf.distr_restrict[symmetric])
hoelzl@61359
   626
hoelzl@61359
   627
    let ?Q = "distr IT.PF.lim (PiM (\<Union>i. J i) M) (\<lambda>\<omega>. \<lambda>x\<in>\<Union>i. J i. \<omega> (t x))"
hoelzl@61359
   628
    { fix i
hoelzl@61359
   629
      have "distr ?Q (Pi\<^sub>M (J i) M) (\<lambda>x. restrict x (J i)) = 
hoelzl@61359
   630
        distr IT.PF.lim (Pi\<^sub>M (J i) M) ((\<lambda>\<omega>. \<lambda>n\<in>J i. \<omega> (t n)) \<circ> (\<lambda>\<omega>. restrict \<omega> (t`J i)))"
hoelzl@61359
   631
      proof (subst distr_distr)
hoelzl@61359
   632
        have "(\<lambda>\<omega>. \<omega> (t x)) \<in> measurable (Pi\<^sub>M UNIV (\<lambda>x. M (f x))) (M x)" if x: "x \<in> J i" for x i
hoelzl@61359
   633
          using measurable_component_singleton[of "t x" "UNIV" "\<lambda>x. M (f x)"] unfolding ft[OF x] by simp
hoelzl@61359
   634
        then show "(\<lambda>\<omega>. \<lambda>x\<in>\<Union>i. J i. \<omega> (t x)) \<in> measurable IT.PF.lim (Pi\<^sub>M (UNION UNIV J) M)"
hoelzl@61359
   635
          by (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl])
hoelzl@61359
   636
      qed (auto intro!: distr_cong measurable_restrict measurable_component_singleton)
hoelzl@61359
   637
      also have "\<dots> = distr (distr IT.PF.lim (PiM (t`J i) (\<lambda>x. M (f x))) (\<lambda>\<omega>. restrict \<omega> (t`J i))) (Pi\<^sub>M (J i) M) (\<lambda>\<omega>. \<lambda>n\<in>J i. \<omega> (t n))"
hoelzl@61359
   638
      proof (intro distr_distr[symmetric])
hoelzl@61359
   639
        have "(\<lambda>\<omega>. \<omega> (t x)) \<in> measurable (Pi\<^sub>M (t`J i) (\<lambda>x. M (f x))) (M x)" if x: "x \<in> J i" for x
hoelzl@61359
   640
          using measurable_component_singleton[of "t x" "t`J i" "\<lambda>x. M (f x)"] x unfolding ft[OF x] by auto
hoelzl@61359
   641
        then show "(\<lambda>\<omega>. \<lambda>n\<in>J i. \<omega> (t n)) \<in> measurable (Pi\<^sub>M (t ` J i) (\<lambda>x. M (f x))) (Pi\<^sub>M (J i) M)"
hoelzl@61359
   642
          by (auto intro!: measurable_restrict)
hoelzl@61359
   643
      qed (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl])
hoelzl@61359
   644
      also have "\<dots> = distr (PiM (t`J i) (\<lambda>x. M (f x))) (Pi\<^sub>M (J i) M) (\<lambda>\<omega>. \<lambda>n\<in>J i. \<omega> (t n))"
hoelzl@61359
   645
        using \<open>finite (J i)\<close> by (subst IT.distr_lim) (auto simp: CI_eq_PiM)
hoelzl@61359
   646
      also have "\<dots> = Pi\<^sub>M (J i) M"
hoelzl@61359
   647
        using Mf.distr_reorder[of t "J i"] by (simp add: 1 inj_t_J cong: PiM_cong)
hoelzl@61359
   648
      finally have "distr ?Q (Pi\<^sub>M (J i) M) (\<lambda>x. restrict x (J i)) = Pi\<^sub>M (J i) M" . }
hoelzl@61359
   649
    then show "\<exists>Q. \<forall>i. sets Q = PiM (\<Union>i. J i) M \<and> distr Q (Pi\<^sub>M (J i) M) (\<lambda>x. restrict x (J i)) = Pi\<^sub>M (J i) M"
hoelzl@61359
   650
      by (intro exI[of _ ?Q]) auto
hoelzl@61359
   651
  qed
hoelzl@61359
   652
  then obtain Q where sets_Q: "sets Q = PiM (\<Union>i. J i) M"
hoelzl@61359
   653
    and Q: "\<And>i. distr Q (PiM (J i) M) (\<lambda>x. restrict x (J i)) = Pi\<^sub>M (J i) M" by blast
hoelzl@61359
   654
hoelzl@61359
   655
  from 1 interpret Q: prob_space Q
hoelzl@61359
   656
    by (intro prob_space_distrD[of "\<lambda>x. restrict x (J 0)" Q "PiM (J 0) M"])
hoelzl@61359
   657
       (auto simp: Q measurable_cong_sets[OF sets_Q]
hoelzl@61359
   658
                intro!: prob_space_P measurable_restrict measurable_component_singleton)
hoelzl@61359
   659
hoelzl@61359
   660
  have "0 < (INF i. emeasure (Pi\<^sub>M (J i) M) (X i))" by fact
hoelzl@61359
   661
  also have "\<dots> = (INF i. emeasure Q (emb (\<Union>i. J i) (J i) (X i)))"
hoelzl@61359
   662
    by (simp add: emeasure_distr_restrict[OF _ sets_Q 1(4), symmetric] SUP_upper Q)
hoelzl@61359
   663
  also have "\<dots> = emeasure Q (\<Inter>i. emb (\<Union>i. J i) (J i) (X i))"
hoelzl@61359
   664
  proof (rule INF_emeasure_decseq)
hoelzl@61359
   665
    from 1 show "decseq (\<lambda>n. emb (\<Union>i. J i) (J n) (X n))"
hoelzl@61359
   666
      by (intro antimonoI emb_preserve_mono[where X="emb (\<Union>i. J i) (J n) (X n)" and L=I and J="\<Union>i. J i" for n]
hoelzl@61359
   667
         measurable_prod_emb)
hoelzl@61359
   668
         (auto simp: SUP_least SUP_upper antimono_def)
hoelzl@61359
   669
  qed (insert 1, auto simp: sets_Q)
hoelzl@61359
   670
  finally have "(\<Inter>i. emb (\<Union>i. J i) (J i) (X i)) \<noteq> {}"
hoelzl@61359
   671
    by auto
hoelzl@61359
   672
  moreover have "(\<Inter>i. emb I (J i) (X i)) = {} \<Longrightarrow> (\<Inter>i. emb (\<Union>i. J i) (J i) (X i)) = {}"
hoelzl@61359
   673
    using 1 by (intro emb_injective[of "\<Union>i. J i" I _ "{}"] sets.countable_INT) (auto simp: SUP_least SUP_upper)
hoelzl@61359
   674
  ultimately show ?case by auto
hoelzl@57447
   675
qed
immler@50087
   676
immler@50039
   677
end