src/HOL/Probability/Complete_Measure.thy
author hoelzl
Thu, 14 Apr 2016 15:48:11 +0200
changeset 62975 1d066f6ab25d
parent 62390 842917225d56
permissions -rw-r--r--
Probability: move emeasure and nn_integral from ereal to ennreal
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41983
2dc6e382a58b standardized headers;
wenzelm
parents: 41981
diff changeset
     1
(*  Title:      HOL/Probability/Complete_Measure.thy
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
     2
    Author:     Robert Himmelmann, Johannes Hoelzl, TU Muenchen
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
     3
*)
41983
2dc6e382a58b standardized headers;
wenzelm
parents: 41981
diff changeset
     4
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
     5
theory Complete_Measure
58587
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
     6
  imports Bochner_Integration Probability_Measure
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
     7
begin
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
     8
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
     9
definition
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    10
  "split_completion M A p = (if A \<in> sets M then p = (A, {}) else
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    11
   \<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and> fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets M)"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41097
diff changeset
    12
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    13
definition
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    14
  "main_part M A = fst (Eps (split_completion M A))"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41097
diff changeset
    15
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    16
definition
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    17
  "null_part M A = snd (Eps (split_completion M A))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
    18
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    19
definition completion :: "'a measure \<Rightarrow> 'a measure" where
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    20
  "completion M = measure_of (space M) { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    21
    (emeasure M \<circ> main_part M)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
    22
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    23
lemma completion_into_space:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    24
  "{ S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' } \<subseteq> Pow (space M)"
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 47694
diff changeset
    25
  using sets.sets_into_space by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
    26
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    27
lemma space_completion[simp]: "space (completion M) = space M"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    28
  unfolding completion_def using space_measure_of[OF completion_into_space] by simp
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
    29
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    30
lemma completionI:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    31
  assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    32
  shows "A \<in> { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
    33
  using assms by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
    34
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    35
lemma completionE:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    36
  assumes "A \<in> { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    37
  obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    38
  using assms by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    39
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    40
lemma sigma_algebra_completion:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    41
  "sigma_algebra (space M) { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    42
    (is "sigma_algebra _ ?A")
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    43
  unfolding sigma_algebra_iff2
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    44
proof (intro conjI ballI allI impI)
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    45
  show "?A \<subseteq> Pow (space M)"
50244
de72bbe42190 qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents: 47694
diff changeset
    46
    using sets.sets_into_space by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
    47
next
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    48
  show "{} \<in> ?A" by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
    49
next
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    50
  let ?C = "space M"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    51
  fix A assume "A \<in> ?A" from completionE[OF this] guess S N N' .
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    52
  then show "space M - A \<in> ?A"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    53
    by (intro completionI[of _ "(?C - S) \<inter> (?C - N')" "(?C - S) \<inter> N' \<inter> (?C - N)"]) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    54
next
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    55
  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> ?A"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    56
  then have "\<forall>n. \<exists>S N N'. A n = S \<union> N \<and> S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N'"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    57
    by (auto simp: image_subset_iff)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
    58
  from choice[OF this] guess S ..
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
    59
  from choice[OF this] guess N ..
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
    60
  from choice[OF this] guess N' ..
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    61
  then show "UNION UNIV A \<in> ?A"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
    62
    using null_sets_UN[of N']
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    63
    by (intro completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"]) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    64
qed
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    65
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    66
lemma sets_completion:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    67
  "sets (completion M) = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    68
  using sigma_algebra.sets_measure_of_eq[OF sigma_algebra_completion] by (simp add: completion_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    69
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    70
lemma sets_completionE:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    71
  assumes "A \<in> sets (completion M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    72
  obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    73
  using assms unfolding sets_completion by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    74
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    75
lemma sets_completionI:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    76
  assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    77
  shows "A \<in> sets (completion M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    78
  using assms unfolding sets_completion by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    79
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    80
lemma sets_completionI_sets[intro, simp]:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    81
  "A \<in> sets M \<Longrightarrow> A \<in> sets (completion M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    82
  unfolding sets_completion by force
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
    83
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    84
lemma null_sets_completion:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    85
  assumes "N' \<in> null_sets M" "N \<subseteq> N'" shows "N \<in> sets (completion M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    86
  using assms by (intro sets_completionI[of N "{}" N N']) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    87
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    88
lemma split_completion:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    89
  assumes "A \<in> sets (completion M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    90
  shows "split_completion M A (main_part M A, null_part M A)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    91
proof cases
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    92
  assume "A \<in> sets M" then show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    93
    by (simp add: split_completion_def[abs_def] main_part_def null_part_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    94
next
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    95
  assume nA: "A \<notin> sets M"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    96
  show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    97
    unfolding main_part_def null_part_def if_not_P[OF nA]
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    98
  proof (rule someI2_ex)
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
    99
    from assms[THEN sets_completionE] guess S N N' . note A = this
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   100
    let ?P = "(S, N - S)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   101
    show "\<exists>p. split_completion M A p"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   102
      unfolding split_completion_def if_not_P[OF nA] using A
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   103
    proof (intro exI conjI)
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   104
      show "A = fst ?P \<union> snd ?P" using A by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   105
      show "snd ?P \<subseteq> N'" using A by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   106
   qed auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   107
  qed auto
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   108
qed
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   109
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   110
lemma
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   111
  assumes "S \<in> sets (completion M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   112
  shows main_part_sets[intro, simp]: "main_part M S \<in> sets M"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   113
    and main_part_null_part_Un[simp]: "main_part M S \<union> null_part M S = S"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   114
    and main_part_null_part_Int[simp]: "main_part M S \<inter> null_part M S = {}"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   115
  using split_completion[OF assms]
62390
842917225d56 more canonical names
nipkow
parents: 62343
diff changeset
   116
  by (auto simp: split_completion_def split: if_split_asm)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   117
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   118
lemma main_part[simp]: "S \<in> sets M \<Longrightarrow> main_part M S = S"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   119
  using split_completion[of S M]
62390
842917225d56 more canonical names
nipkow
parents: 62343
diff changeset
   120
  by (auto simp: split_completion_def split: if_split_asm)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   121
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   122
lemma null_part:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   123
  assumes "S \<in> sets (completion M)" shows "\<exists>N. N\<in>null_sets M \<and> null_part M S \<subseteq> N"
62390
842917225d56 more canonical names
nipkow
parents: 62343
diff changeset
   124
  using split_completion[OF assms] by (auto simp: split_completion_def split: if_split_asm)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   125
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   126
lemma null_part_sets[intro, simp]:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   127
  assumes "S \<in> sets M" shows "null_part M S \<in> sets M" "emeasure M (null_part M S) = 0"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   128
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   129
  have S: "S \<in> sets (completion M)" using assms by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   130
  have "S - main_part M S \<in> sets M" using assms by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   131
  moreover
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   132
  from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S]
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   133
  have "S - main_part M S = null_part M S" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   134
  ultimately show sets: "null_part M S \<in> sets M" by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   135
  from null_part[OF S] guess N ..
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   136
  with emeasure_eq_0[of N _ "null_part M S"] sets
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   137
  show "emeasure M (null_part M S) = 0" by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   138
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   139
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   140
lemma emeasure_main_part_UN:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   141
  fixes S :: "nat \<Rightarrow> 'a set"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   142
  assumes "range S \<subseteq> sets (completion M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   143
  shows "emeasure M (main_part M (\<Union>i. (S i))) = emeasure M (\<Union>i. main_part M (S i))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   144
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   145
  have S: "\<And>i. S i \<in> sets (completion M)" using assms by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   146
  then have UN: "(\<Union>i. S i) \<in> sets (completion M)" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   147
  have "\<forall>i. \<exists>N. N \<in> null_sets M \<and> null_part M (S i) \<subseteq> N"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   148
    using null_part[OF S] by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   149
  from choice[OF this] guess N .. note N = this
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   150
  then have UN_N: "(\<Union>i. N i) \<in> null_sets M" by (intro null_sets_UN) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   151
  have "(\<Union>i. S i) \<in> sets (completion M)" using S by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   152
  from null_part[OF this] guess N' .. note N' = this
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   153
  let ?N = "(\<Union>i. N i) \<union> N'"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   154
  have null_set: "?N \<in> null_sets M" using N' UN_N by (intro null_sets.Un) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   155
  have "main_part M (\<Union>i. S i) \<union> ?N = (main_part M (\<Union>i. S i) \<union> null_part M (\<Union>i. S i)) \<union> ?N"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   156
    using N' by auto
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   157
  also have "\<dots> = (\<Union>i. main_part M (S i) \<union> null_part M (S i)) \<union> ?N"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   158
    unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   159
  also have "\<dots> = (\<Union>i. main_part M (S i)) \<union> ?N"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   160
    using N by auto
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   161
  finally have *: "main_part M (\<Union>i. S i) \<union> ?N = (\<Union>i. main_part M (S i)) \<union> ?N" .
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   162
  have "emeasure M (main_part M (\<Union>i. S i)) = emeasure M (main_part M (\<Union>i. S i) \<union> ?N)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   163
    using null_set UN by (intro emeasure_Un_null_set[symmetric]) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   164
  also have "\<dots> = emeasure M ((\<Union>i. main_part M (S i)) \<union> ?N)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   165
    unfolding * ..
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   166
  also have "\<dots> = emeasure M (\<Union>i. main_part M (S i))"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   167
    using null_set S by (intro emeasure_Un_null_set) auto
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41097
diff changeset
   168
  finally show ?thesis .
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   169
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   170
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   171
lemma emeasure_completion[simp]:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   172
  assumes S: "S \<in> sets (completion M)" shows "emeasure (completion M) S = emeasure M (main_part M S)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   173
proof (subst emeasure_measure_of[OF completion_def completion_into_space])
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   174
  let ?\<mu> = "emeasure M \<circ> main_part M"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   175
  show "S \<in> sets (completion M)" "?\<mu> S = emeasure M (main_part M S) " using S by simp_all
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   176
  show "positive (sets (completion M)) ?\<mu>"
62975
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62390
diff changeset
   177
    by (simp add: positive_def)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   178
  show "countably_additive (sets (completion M)) ?\<mu>"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   179
  proof (intro countably_additiveI)
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   180
    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (completion M)" "disjoint_family A"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   181
    have "disjoint_family (\<lambda>i. main_part M (A i))"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   182
    proof (intro disjoint_family_on_bisimulation[OF A(2)])
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   183
      fix n m assume "A n \<inter> A m = {}"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   184
      then have "(main_part M (A n) \<union> null_part M (A n)) \<inter> (main_part M (A m) \<union> null_part M (A m)) = {}"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   185
        using A by (subst (1 2) main_part_null_part_Un) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   186
      then show "main_part M (A n) \<inter> main_part M (A m) = {}" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   187
    qed
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   188
    then have "(\<Sum>n. emeasure M (main_part M (A n))) = emeasure M (\<Union>i. main_part M (A i))"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   189
      using A by (auto intro!: suminf_emeasure)
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   190
    then show "(\<Sum>n. ?\<mu> (A n)) = ?\<mu> (UNION UNIV A)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   191
      by (simp add: completion_def emeasure_main_part_UN[OF A(1)])
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   192
  qed
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   193
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   194
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   195
lemma emeasure_completion_UN:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   196
  "range S \<subseteq> sets (completion M) \<Longrightarrow>
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   197
    emeasure (completion M) (\<Union>i::nat. (S i)) = emeasure M (\<Union>i. main_part M (S i))"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   198
  by (subst emeasure_completion) (auto simp add: emeasure_main_part_UN)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   199
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   200
lemma emeasure_completion_Un:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   201
  assumes S: "S \<in> sets (completion M)" and T: "T \<in> sets (completion M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   202
  shows "emeasure (completion M) (S \<union> T) = emeasure M (main_part M S \<union> main_part M T)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   203
proof (subst emeasure_completion)
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   204
  have UN: "(\<Union>i. binary (main_part M S) (main_part M T) i) = (\<Union>i. main_part M (binary S T i))"
62390
842917225d56 more canonical names
nipkow
parents: 62343
diff changeset
   205
    unfolding binary_def by (auto split: if_split_asm)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   206
  show "emeasure M (main_part M (S \<union> T)) = emeasure M (main_part M S \<union> main_part M T)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   207
    using emeasure_main_part_UN[of "binary S T" M] assms
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 61808
diff changeset
   208
    by (simp add: range_binary_eq, simp add: Un_range_binary UN)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   209
qed (auto intro: S T)
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   210
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   211
lemma sets_completionI_sub:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   212
  assumes N: "N' \<in> null_sets M" "N \<subseteq> N'"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   213
  shows "N \<in> sets (completion M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   214
  using assms by (intro sets_completionI[of _ "{}" N N']) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   215
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   216
lemma completion_ex_simple_function:
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   217
  assumes f: "simple_function (completion M) f"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   218
  shows "\<exists>f'. simple_function M f' \<and> (AE x in M. f x = f' x)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   219
proof -
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 43920
diff changeset
   220
  let ?F = "\<lambda>x. f -` {x} \<inter> space M"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   221
  have F: "\<And>x. ?F x \<in> sets (completion M)" and fin: "finite (f`space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   222
    using simple_functionD[OF f] simple_functionD[OF f] by simp_all
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   223
  have "\<forall>x. \<exists>N. N \<in> null_sets M \<and> null_part M (?F x) \<subseteq> N"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   224
    using F null_part by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   225
  from choice[OF this] obtain N where
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   226
    N: "\<And>x. null_part M (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets M" by auto
46731
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 43920
diff changeset
   227
  let ?N = "\<Union>x\<in>f`space M. N x"
5302e932d1e5 avoid undeclared variables in let bindings;
wenzelm
parents: 43920
diff changeset
   228
  let ?f' = "\<lambda>x. if x \<in> ?N then undefined else f x"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   229
  have sets: "?N \<in> null_sets M" using N fin by (intro null_sets.finite_UN) auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   230
  show ?thesis unfolding simple_function_def
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   231
  proof (safe intro!: exI[of _ ?f'])
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   232
    have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   233
    from finite_subset[OF this] simple_functionD(1)[OF f]
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   234
    show "finite (?f' ` space M)" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   235
  next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   236
    fix x assume "x \<in> space M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   237
    have "?f' -` {?f' x} \<inter> space M =
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   238
      (if x \<in> ?N then ?F undefined \<union> ?N
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   239
       else if f x = undefined then ?F (f x) \<union> ?N
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   240
       else ?F (f x) - ?N)"
62390
842917225d56 more canonical names
nipkow
parents: 62343
diff changeset
   241
      using N(2) sets.sets_into_space by (auto split: if_split_asm simp: null_sets_def)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   242
    moreover { fix y have "?F y \<union> ?N \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   243
      proof cases
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   244
        assume y: "y \<in> f`space M"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   245
        have "?F y \<union> ?N = (main_part M (?F y) \<union> null_part M (?F y)) \<union> ?N"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   246
          using main_part_null_part_Un[OF F] by auto
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   247
        also have "\<dots> = main_part M (?F y) \<union> ?N"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   248
          using y N by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   249
        finally show ?thesis
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   250
          using F sets by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   251
      next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   252
        assume "y \<notin> f`space M" then have "?F y = {}" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   253
        then show ?thesis using sets by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   254
      qed }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   255
    moreover {
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   256
      have "?F (f x) - ?N = main_part M (?F (f x)) \<union> null_part M (?F (f x)) - ?N"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   257
        using main_part_null_part_Un[OF F] by auto
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   258
      also have "\<dots> = main_part M (?F (f x)) - ?N"
61808
fc1556774cfe isabelle update_cartouches -c -t;
wenzelm
parents: 58587
diff changeset
   259
        using N \<open>x \<in> space M\<close> by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   260
      finally have "?F (f x) - ?N \<in> sets M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   261
        using F sets by auto }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   262
    ultimately show "?f' -` {?f' x} \<inter> space M \<in> sets M" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   263
  next
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   264
    show "AE x in M. f x = ?f' x"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   265
      by (rule AE_I', rule sets) auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   266
  qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   267
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   268
62975
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62390
diff changeset
   269
lemma completion_ex_borel_measurable:
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62390
diff changeset
   270
  fixes g :: "'a \<Rightarrow> ennreal"
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62390
diff changeset
   271
  assumes g: "g \<in> borel_measurable (completion M)"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   272
  shows "\<exists>g'\<in>borel_measurable M. (AE x in M. g x = g' x)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   273
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   274
  from g[THEN borel_measurable_implies_simple_function_sequence'] guess f . note f = this
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41959
diff changeset
   275
  from this(1)[THEN completion_ex_simple_function]
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   276
  have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x in M. f i x = f' x)" ..
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   277
  from this[THEN choice] obtain f' where
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41097
diff changeset
   278
    sf: "\<And>i. simple_function M (f' i)" and
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   279
    AE: "\<forall>i. AE x in M. f i x = f' i x" by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   280
  show ?thesis
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   281
  proof (intro bexI)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41959
diff changeset
   282
    from AE[unfolded AE_all_countable[symmetric]]
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46731
diff changeset
   283
    show "AE x in M. g x = (SUP i. f' i x)" (is "AE x in M. g x = ?f x")
41705
1100512e16d8 add auto support for AE_mp
hoelzl
parents: 41689
diff changeset
   284
    proof (elim AE_mp, safe intro!: AE_I2)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   285
      fix x assume eq: "\<forall>i. f i x = f' i x"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41959
diff changeset
   286
      moreover have "g x = (SUP i. f i x)"
62975
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62390
diff changeset
   287
        unfolding f by (auto split: split_max)
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41959
diff changeset
   288
      ultimately show "g x = ?f x" by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   289
    qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   290
    show "?f \<in> borel_measurable M"
56949
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 50244
diff changeset
   291
      using sf[THEN borel_measurable_simple_function] by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   292
  qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   293
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   294
58587
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   295
lemma (in prob_space) prob_space_completion: "prob_space (completion M)"
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   296
  by (rule prob_spaceI) (simp add: emeasure_space_1)
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   297
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   298
lemma null_sets_completionI: "N \<in> null_sets M \<Longrightarrow> N \<in> null_sets (completion M)"
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   299
  by (auto simp: null_sets_def)
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   300
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   301
lemma AE_completion: "(AE x in M. P x) \<Longrightarrow> (AE x in completion M. P x)"
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   302
  unfolding eventually_ae_filter by (auto intro: null_sets_completionI)
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   303
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   304
lemma null_sets_completion_iff: "N \<in> sets M \<Longrightarrow> N \<in> null_sets (completion M) \<longleftrightarrow> N \<in> null_sets M"
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   305
  by (auto simp: null_sets_def)
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   306
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   307
lemma AE_completion_iff: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in completion M. P x)"
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   308
  by (simp add: AE_iff_null null_sets_completion_iff)
5484f6079bcd add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents: 56993
diff changeset
   309
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents:
diff changeset
   310
end