src/HOL/Probability/Infinite_Product_Measure.thy
changeset 50099 a58bb401af80
parent 50095 94d7dfa9f404
child 50123 69b35a75caf3
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 16 14:46:23 2012 +0100
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 16 14:46:23 2012 +0100
     1.3 @@ -449,23 +449,6 @@
     1.4  
     1.5  subsection {* Sequence space *}
     1.6  
     1.7 -lemma measurable_nat_case: "(\<lambda>(x, \<omega>). nat_case x \<omega>) \<in> measurable (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) (\<Pi>\<^isub>M i\<in>UNIV. M)"
     1.8 -proof (rule measurable_PiM_single)
     1.9 -  show "(\<lambda>(x, \<omega>). nat_case x \<omega>) \<in> space (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) \<rightarrow> (UNIV \<rightarrow>\<^isub>E space M)"
    1.10 -    by (auto simp: space_pair_measure space_PiM Pi_iff split: nat.split)
    1.11 -  fix i :: nat and A assume A: "A \<in> sets M"
    1.12 -  then have *: "{\<omega> \<in> space (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case nat_case \<omega> i \<in> A} =
    1.13 -    (case i of 0 \<Rightarrow> A \<times> space (\<Pi>\<^isub>M i\<in>UNIV. M) | Suc n \<Rightarrow> space M \<times> {\<omega>\<in>space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> n \<in> A})"
    1.14 -    by (auto simp: space_PiM space_pair_measure split: nat.split dest: sets_into_space)
    1.15 -  show "{\<omega> \<in> space (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case nat_case \<omega> i \<in> A} \<in> sets (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M))"
    1.16 -    unfolding * by (auto simp: A split: nat.split intro!: sets_Collect_single)
    1.17 -qed
    1.18 -
    1.19 -lemma measurable_nat_case':
    1.20 -  assumes f: "f \<in> measurable N M" and g: "g \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
    1.21 -  shows "(\<lambda>x. nat_case (f x) (g x)) \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
    1.22 -  using measurable_compose[OF measurable_Pair[OF f g] measurable_nat_case] by simp
    1.23 -
    1.24  definition comb_seq :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)" where
    1.25    "comb_seq i \<omega> \<omega>' j = (if j < i then \<omega> j else \<omega>' (j - i))"
    1.26  
    1.27 @@ -475,7 +458,8 @@
    1.28  lemma split_comb_seq_asm: "P (comb_seq i \<omega> \<omega>' j) \<longleftrightarrow> \<not> ((j < i \<and> \<not> P (\<omega> j)) \<or> (\<exists>k. j = i + k \<and> \<not> P (\<omega>' k)))"
    1.29    by (auto simp: comb_seq_def)
    1.30  
    1.31 -lemma measurable_comb_seq: "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> measurable ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) (\<Pi>\<^isub>M i\<in>UNIV. M)"
    1.32 +lemma measurable_comb_seq:
    1.33 +  "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> measurable ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) (\<Pi>\<^isub>M i\<in>UNIV. M)"
    1.34  proof (rule measurable_PiM_single)
    1.35    show "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) \<rightarrow> (UNIV \<rightarrow>\<^isub>E space M)"
    1.36      by (auto simp: space_pair_measure space_PiM Pi_iff split: split_comb_seq)
    1.37 @@ -488,11 +472,33 @@
    1.38      unfolding * by (auto simp: A intro!: sets_Collect_single)
    1.39  qed
    1.40  
    1.41 -lemma measurable_comb_seq':
    1.42 +lemma measurable_comb_seq'[measurable (raw)]:
    1.43    assumes f: "f \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)" and g: "g \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
    1.44    shows "(\<lambda>x. comb_seq i (f x) (g x)) \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
    1.45    using measurable_compose[OF measurable_Pair[OF f g] measurable_comb_seq] by simp
    1.46  
    1.47 +lemma comb_seq_0: "comb_seq 0 \<omega> \<omega>' = \<omega>'"
    1.48 +  by (auto simp add: comb_seq_def)
    1.49 +
    1.50 +lemma comb_seq_Suc: "comb_seq (Suc n) \<omega> \<omega>' = comb_seq n \<omega> (nat_case (\<omega> n) \<omega>')"
    1.51 +  by (auto simp add: comb_seq_def not_less less_Suc_eq le_imp_diff_is_add intro!: ext split: nat.split)
    1.52 +
    1.53 +lemma comb_seq_Suc_0[simp]: "comb_seq (Suc 0) \<omega> = nat_case (\<omega> 0)"
    1.54 +  by (intro ext) (simp add: comb_seq_Suc comb_seq_0)
    1.55 +
    1.56 +lemma comb_seq_less: "i < n \<Longrightarrow> comb_seq n \<omega> \<omega>' i = \<omega> i"
    1.57 +  by (auto split: split_comb_seq)
    1.58 +
    1.59 +lemma comb_seq_add: "comb_seq n \<omega> \<omega>' (i + n) = \<omega>' i"
    1.60 +  by (auto split: nat.split split_comb_seq)
    1.61 +
    1.62 +lemma nat_case_comb_seq: "nat_case s' (comb_seq n \<omega> \<omega>') (i + n) = nat_case (nat_case s' \<omega> n) \<omega>' i"
    1.63 +  by (auto split: nat.split split_comb_seq)
    1.64 +
    1.65 +lemma nat_case_comb_seq':
    1.66 +  "nat_case s (comb_seq i \<omega> \<omega>') = comb_seq (Suc i) (nat_case s \<omega>) \<omega>'"
    1.67 +  by (auto split: split_comb_seq nat.split)
    1.68 +
    1.69  locale sequence_space = product_prob_space "\<lambda>i. M" "UNIV :: nat set" for M
    1.70  begin
    1.71  
    1.72 @@ -578,7 +584,7 @@
    1.73     by (auto simp: space_pair_measure space_PiM Pi_iff prod_emb_def all_conj_distrib
    1.74        split: nat.split nat.split_asm)
    1.75    then have "emeasure ?D ?X = emeasure (M \<Otimes>\<^isub>M S) (?E \<times> ?F)"
    1.76 -    by (subst emeasure_distr[OF measurable_nat_case])
    1.77 +    by (subst emeasure_distr)
    1.78         (auto intro!: sets_PiM_I simp: split_beta' J)
    1.79    also have "\<dots> = emeasure M ?E * emeasure S ?F"
    1.80      using J by (intro P.emeasure_pair_measure_Times) (auto intro!: sets_PiM_I finite_vimageI)