src/HOL/Analysis/Embed_Measure.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago)
changeset 69981 3dced198b9ec
parent 69768 7e4966eaf781
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
hoelzl@63627
     1
(*  Title:      HOL/Analysis/Embed_Measure.thy
hoelzl@59092
     2
    Author:     Manuel Eberl, TU M√ľnchen
hoelzl@59092
     3
hoelzl@62975
     4
    Defines measure embeddings with injective functions, i.e. lifting a measure on some values
hoelzl@62975
     5
    to a measure on "tagged" values (e.g. embed_measure M Inl lifts a measure on values 'a to a
hoelzl@59092
     6
    measure on the left part of the sum type 'a + 'b)
hoelzl@59092
     7
*)
hoelzl@59092
     8
eberlm@69180
     9
section \<open>Embedding Measure Spaces with a Function\<close>
hoelzl@59092
    10
hoelzl@59092
    11
theory Embed_Measure
hoelzl@59092
    12
imports Binary_Product_Measure
hoelzl@59092
    13
begin
hoelzl@59092
    14
eberlm@69180
    15
text \<open>
eberlm@69180
    16
  Given a measure space on some carrier set \<open>\<Omega>\<close> and a function \<open>f\<close>, we can define a push-forward
wenzelm@69566
    17
  measure on the carrier set \<open>f(\<Omega>)\<close> whose \<open>\<sigma>\<close>-algebra is the one generated by mapping \<open>f\<close> over
eberlm@69180
    18
  the original sigma algebra.
eberlm@69180
    19
eberlm@69180
    20
  This is useful e.\,g.\ when \<open>f\<close> is injective, i.\,e.\ it is some kind of ``tagging'' function.
eberlm@69180
    21
  For instance, suppose we have some algebraaic datatype of values with various constructors,
eberlm@69180
    22
  including a constructor \<open>RealVal\<close> for real numbers. Then \<open>embed_measure\<close> allows us to lift a 
eberlm@69180
    23
  measure on real numbers to the appropriate subset of that algebraic datatype.
eberlm@69180
    24
\<close>
eberlm@69180
    25
definition%important embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
hoelzl@62975
    26
  "embed_measure M f = measure_of (f ` space M) {f ` A |A. A \<in> sets M}
hoelzl@59092
    27
                           (\<lambda>A. emeasure M (f -` A \<inter> space M))"
hoelzl@59092
    28
hoelzl@59092
    29
lemma space_embed_measure: "space (embed_measure M f) = f ` space M"
hoelzl@62975
    30
  unfolding embed_measure_def
hoelzl@59092
    31
  by (subst space_measure_of) (auto dest: sets.sets_into_space)
hoelzl@59092
    32
hoelzl@59092
    33
lemma sets_embed_measure':
hoelzl@62975
    34
  assumes inj: "inj_on f (space M)"
hoelzl@59092
    35
  shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"
hoelzl@59092
    36
  unfolding embed_measure_def
hoelzl@59092
    37
proof (intro sigma_algebra.sets_measure_of_eq sigma_algebra_iff2[THEN iffD2] conjI allI ballI impI)
hoelzl@59092
    38
  fix s assume "s \<in> {f ` A |A. A \<in> sets M}"
hoelzl@59092
    39
  then obtain s' where s'_props: "s = f ` s'" "s' \<in> sets M" by auto
hoelzl@59092
    40
  hence "f ` space M - s = f ` (space M - s')" using inj
hoelzl@59092
    41
    by (auto dest: inj_onD sets.sets_into_space)
hoelzl@59092
    42
  also have "... \<in> {f ` A |A. A \<in> sets M}" using s'_props by auto
hoelzl@59092
    43
  finally show "f ` space M - s \<in> {f ` A |A. A \<in> sets M}" .
hoelzl@59092
    44
next
hoelzl@59092
    45
  fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> {f ` A |A. A \<in> sets M}"
wenzelm@63539
    46
  then obtain A' where A': "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M"
hoelzl@59092
    47
    by (auto simp: subset_eq choice_iff)
wenzelm@63539
    48
  then have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast
wenzelm@63539
    49
  with A' show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}"
haftmann@62343
    50
    by simp blast
hoelzl@59092
    51
qed (auto dest: sets.sets_into_space)
hoelzl@59092
    52
hoelzl@59092
    53
lemma the_inv_into_vimage:
hoelzl@59092
    54
  "inj_on f X \<Longrightarrow> A \<subseteq> X \<Longrightarrow> the_inv_into X f -` A \<inter> (f`X) = f ` A"
hoelzl@59092
    55
  by (auto simp: the_inv_into_f_f)
hoelzl@59092
    56
hoelzl@59092
    57
lemma sets_embed_eq_vimage_algebra:
hoelzl@59092
    58
  assumes "inj_on f (space M)"
hoelzl@59092
    59
  shows "sets (embed_measure M f) = sets (vimage_algebra (f`space M) (the_inv_into (space M) f) M)"
hoelzl@63886
    60
  by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 Setcompr_eq_image
hoelzl@59092
    61
           dest: sets.sets_into_space
hoelzl@59092
    62
           intro!: image_cong the_inv_into_vimage[symmetric])
hoelzl@59092
    63
hoelzl@59092
    64
lemma sets_embed_measure:
hoelzl@62975
    65
  assumes inj: "inj f"
hoelzl@59092
    66
  shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"
hoelzl@59092
    67
  using assms by (subst sets_embed_measure') (auto intro!: inj_onI dest: injD)
hoelzl@59092
    68
hoelzl@59092
    69
lemma in_sets_embed_measure: "A \<in> sets M \<Longrightarrow> f ` A \<in> sets (embed_measure M f)"
hoelzl@59092
    70
  unfolding embed_measure_def
hoelzl@59092
    71
  by (intro in_measure_of) (auto dest: sets.sets_into_space)
hoelzl@59092
    72
hoelzl@59092
    73
lemma measurable_embed_measure1:
hoelzl@62975
    74
  assumes g: "(\<lambda>x. g (f x)) \<in> measurable M N"
hoelzl@59092
    75
  shows "g \<in> measurable (embed_measure M f) N"
hoelzl@59092
    76
  unfolding measurable_def
hoelzl@59092
    77
proof safe
hoelzl@59092
    78
  fix A assume "A \<in> sets N"
hoelzl@59092
    79
  with g have "(\<lambda>x. g (f x)) -` A \<inter> space M \<in> sets M"
hoelzl@59092
    80
    by (rule measurable_sets)
hoelzl@59092
    81
  then have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) \<in> sets (embed_measure M f)"
hoelzl@59092
    82
    by (rule in_sets_embed_measure)
hoelzl@59092
    83
  also have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) = g -` A \<inter> space (embed_measure M f)"
hoelzl@59092
    84
    by (auto simp: space_embed_measure)
hoelzl@59092
    85
  finally show "g -` A \<inter> space (embed_measure M f) \<in> sets (embed_measure M f)" .
hoelzl@59092
    86
qed (insert measurable_space[OF assms], auto simp: space_embed_measure)
hoelzl@59092
    87
hoelzl@59092
    88
lemma measurable_embed_measure2':
hoelzl@62975
    89
  assumes "inj_on f (space M)"
hoelzl@59092
    90
  shows "f \<in> measurable M (embed_measure M f)"
hoelzl@59092
    91
proof-
hoelzl@59092
    92
  {
hoelzl@59092
    93
    fix A assume A: "A \<in> sets M"
wenzelm@63539
    94
    also from A have "A = A \<inter> space M" by auto
hoelzl@59092
    95
    also have "... = f -` f ` A \<inter> space M" using A assms
hoelzl@59092
    96
      by (auto dest: inj_onD sets.sets_into_space)
hoelzl@59092
    97
    finally have "f -` f ` A \<inter> space M \<in> sets M" .
hoelzl@59092
    98
  }
hoelzl@59092
    99
  thus ?thesis using assms unfolding embed_measure_def
hoelzl@59092
   100
    by (intro measurable_measure_of) (auto dest: sets.sets_into_space)
hoelzl@59092
   101
qed
hoelzl@59092
   102
hoelzl@59092
   103
lemma measurable_embed_measure2:
hoelzl@59092
   104
  assumes [simp]: "inj f" shows "f \<in> measurable M (embed_measure M f)"
hoelzl@59092
   105
  by (auto simp: inj_vimage_image_eq embed_measure_def
hoelzl@59092
   106
           intro!: measurable_measure_of dest: sets.sets_into_space)
hoelzl@59092
   107
hoelzl@59092
   108
lemma embed_measure_eq_distr':
hoelzl@59092
   109
  assumes "inj_on f (space M)"
hoelzl@59092
   110
  shows "embed_measure M f = distr M (embed_measure M f) f"
hoelzl@59092
   111
proof-
hoelzl@62975
   112
  have "distr M (embed_measure M f) f =
hoelzl@59092
   113
            measure_of (f ` space M) {f ` A |A. A \<in> sets M}
hoelzl@59092
   114
                       (\<lambda>A. emeasure M (f -` A \<inter> space M))" unfolding distr_def
hoelzl@59092
   115
      by (simp add: space_embed_measure sets_embed_measure'[OF assms])
hoelzl@59092
   116
  also have "... = embed_measure M f" unfolding embed_measure_def ..
hoelzl@59092
   117
  finally show ?thesis ..
hoelzl@59092
   118
qed
hoelzl@59092
   119
hoelzl@59092
   120
lemma embed_measure_eq_distr:
hoelzl@59092
   121
    "inj f \<Longrightarrow> embed_measure M f = distr M (embed_measure M f) f"
hoelzl@59092
   122
  by (rule embed_measure_eq_distr') (auto intro!: inj_onI dest: injD)
hoelzl@59092
   123
Andreas@60065
   124
lemma nn_integral_embed_measure':
Andreas@60065
   125
  "inj_on f (space M) \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
Andreas@60065
   126
  nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
Andreas@60065
   127
  apply (subst embed_measure_eq_distr', simp)
Andreas@60065
   128
  apply (subst nn_integral_distr)
Andreas@60065
   129
  apply (simp_all add: measurable_embed_measure2')
Andreas@60065
   130
  done
Andreas@60065
   131
hoelzl@59092
   132
lemma nn_integral_embed_measure:
hoelzl@59092
   133
  "inj f \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
hoelzl@59092
   134
  nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
Andreas@60065
   135
  by(erule nn_integral_embed_measure'[OF subset_inj_on]) simp
hoelzl@59092
   136
hoelzl@59092
   137
lemma emeasure_embed_measure':
hoelzl@59092
   138
    assumes "inj_on f (space M)" "A \<in> sets (embed_measure M f)"
hoelzl@59092
   139
    shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"
hoelzl@59092
   140
  by (subst embed_measure_eq_distr'[OF assms(1)])
hoelzl@59092
   141
     (simp add: emeasure_distr[OF measurable_embed_measure2'[OF assms(1)] assms(2)])
hoelzl@59092
   142
hoelzl@59092
   143
lemma emeasure_embed_measure:
hoelzl@59092
   144
    assumes "inj f" "A \<in> sets (embed_measure M f)"
hoelzl@59092
   145
    shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"
hoelzl@59092
   146
 using assms by (intro emeasure_embed_measure') (auto intro!: inj_onI dest: injD)
hoelzl@59092
   147
hoelzl@62975
   148
lemma embed_measure_comp:
hoelzl@59092
   149
  assumes [simp]: "inj f" "inj g"
hoelzl@59092
   150
  shows "embed_measure (embed_measure M f) g = embed_measure M (g \<circ> f)"
hoelzl@59092
   151
proof-
lp15@69700
   152
  have [simp]: "inj (\<lambda>x. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_compose)
hoelzl@59092
   153
  note measurable_embed_measure2[measurable]
hoelzl@62975
   154
  have "embed_measure (embed_measure M f) g =
hoelzl@59092
   155
            distr M (embed_measure (embed_measure M f) g) (g \<circ> f)"
hoelzl@62975
   156
      by (subst (1 2) embed_measure_eq_distr)
hoelzl@59092
   157
         (simp_all add: distr_distr sets_embed_measure cong: distr_cong)
hoelzl@59092
   158
  also have "... = embed_measure M (g \<circ> f)"
hoelzl@59092
   159
      by (subst (3) embed_measure_eq_distr, simp add: o_def, rule distr_cong)
hoelzl@62975
   160
         (auto simp: sets_embed_measure o_def image_image[symmetric]
lp15@69700
   161
               intro: inj_compose cong: distr_cong)
hoelzl@59092
   162
  finally show ?thesis .
hoelzl@59092
   163
qed
hoelzl@59092
   164
hoelzl@59092
   165
lemma sigma_finite_embed_measure:
hoelzl@59092
   166
  assumes "sigma_finite_measure M" and inj: "inj f"
hoelzl@59092
   167
  shows "sigma_finite_measure (embed_measure M f)"
wenzelm@60580
   168
proof -
hoelzl@59092
   169
  from assms(1) interpret sigma_finite_measure M .
hoelzl@59092
   170
  from sigma_finite_countable obtain A where
hoelzl@59092
   171
      A_props: "countable A" "A \<subseteq> sets M" "\<Union>A = space M" "\<And>X. X\<in>A \<Longrightarrow> emeasure M X \<noteq> \<infinity>" by blast
nipkow@67399
   172
  from A_props have "countable ((`) f`A)" by auto
wenzelm@60580
   173
  moreover
nipkow@67399
   174
  from inj and A_props have "(`) f`A \<subseteq> sets (embed_measure M f)"
wenzelm@60580
   175
    by (auto simp: sets_embed_measure)
wenzelm@60580
   176
  moreover
nipkow@67399
   177
  from A_props and inj have "\<Union>((`) f`A) = space (embed_measure M f)"
wenzelm@60580
   178
    by (auto simp: space_embed_measure intro!: imageI)
wenzelm@60580
   179
  moreover
nipkow@67399
   180
  from A_props and inj have "\<forall>a\<in>(`) f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
wenzelm@60580
   181
    by (intro ballI, subst emeasure_embed_measure)
wenzelm@60580
   182
       (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
wenzelm@61169
   183
  ultimately show ?thesis by - (standard, blast)
hoelzl@59092
   184
qed
hoelzl@59092
   185
Andreas@60065
   186
lemma embed_measure_count_space':
Andreas@60065
   187
    "inj_on f A \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
hoelzl@59092
   188
  apply (subst distr_bij_count_space[of f A "f`A", symmetric])
hoelzl@59092
   189
  apply (simp add: inj_on_def bij_betw_def)
Andreas@60065
   190
  apply (subst embed_measure_eq_distr')
hoelzl@59092
   191
  apply simp
Andreas@60065
   192
  apply(auto 4 3 intro!: measure_eqI imageI simp add: sets_embed_measure' subset_image_iff)
hoelzl@59092
   193
  apply (subst (1 2) emeasure_distr)
Andreas@60065
   194
  apply (auto simp: space_embed_measure sets_embed_measure')
hoelzl@59092
   195
  done
hoelzl@59092
   196
hoelzl@62975
   197
lemma embed_measure_count_space:
Andreas@60065
   198
    "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
Andreas@60065
   199
  by(rule embed_measure_count_space')(erule subset_inj_on, simp)
Andreas@60065
   200
hoelzl@59092
   201
lemma sets_embed_measure_alt:
nipkow@67399
   202
    "inj f \<Longrightarrow> sets (embed_measure M f) = ((`) f) ` sets M"
hoelzl@59092
   203
  by (auto simp: sets_embed_measure)
hoelzl@59092
   204
hoelzl@59092
   205
lemma emeasure_embed_measure_image':
hoelzl@59092
   206
  assumes "inj_on f (space M)" "X \<in> sets M"
hoelzl@59092
   207
  shows "emeasure (embed_measure M f) (f`X) = emeasure M X"
hoelzl@59092
   208
proof-
hoelzl@59092
   209
  from assms have "emeasure (embed_measure M f) (f`X) = emeasure M (f -` f ` X \<inter> space M)"
hoelzl@59092
   210
    by (subst emeasure_embed_measure') (auto simp: sets_embed_measure')
hoelzl@59092
   211
  also from assms have "f -` f ` X \<inter> space M = X" by (auto dest: inj_onD sets.sets_into_space)
hoelzl@59092
   212
  finally show ?thesis .
hoelzl@59092
   213
qed
hoelzl@59092
   214
hoelzl@59092
   215
lemma emeasure_embed_measure_image:
hoelzl@59092
   216
    "inj f \<Longrightarrow> X \<in> sets M \<Longrightarrow> emeasure (embed_measure M f) (f`X) = emeasure M X"
hoelzl@59092
   217
  by (simp_all add: emeasure_embed_measure in_sets_embed_measure inj_vimage_image_eq)
hoelzl@59092
   218
hoelzl@59092
   219
lemma embed_measure_eq_iff:
hoelzl@59092
   220
  assumes "inj f"
hoelzl@59092
   221
  shows "embed_measure A f = embed_measure B f \<longleftrightarrow> A = B" (is "?M = ?N \<longleftrightarrow> _")
hoelzl@59092
   222
proof
nipkow@67399
   223
  from assms have I: "inj ((`) f)" by (auto intro: injI dest: injD)
hoelzl@59092
   224
  assume asm: "?M = ?N"
hoelzl@59092
   225
  hence "sets (embed_measure A f) = sets (embed_measure B f)" by simp
hoelzl@59092
   226
  with assms have "sets A = sets B" by (simp only: I inj_image_eq_iff sets_embed_measure_alt)
hoelzl@59092
   227
  moreover {
hoelzl@59092
   228
    fix X assume "X \<in> sets A"
hoelzl@59092
   229
    from asm have "emeasure ?M (f`X) = emeasure ?N (f`X)" by simp
hoelzl@62975
   230
    with \<open>X \<in> sets A\<close> and \<open>sets A = sets B\<close> and assms
hoelzl@59092
   231
        have "emeasure A X = emeasure B X" by (simp add: emeasure_embed_measure_image)
hoelzl@59092
   232
  }
hoelzl@59092
   233
  ultimately show "A = B" by (rule measure_eqI)
hoelzl@59092
   234
qed simp
hoelzl@59092
   235
hoelzl@59092
   236
lemma the_inv_into_in_Pi: "inj_on f A \<Longrightarrow> the_inv_into A f \<in> f ` A \<rightarrow> A"
hoelzl@59092
   237
  by (auto simp: the_inv_into_f_f)
hoelzl@59092
   238
hoelzl@59092
   239
lemma map_prod_image: "map_prod f g ` (A \<times> B) = (f`A) \<times> (g`B)"
hoelzl@59092
   240
  using map_prod_surj_on[OF refl refl] .
hoelzl@59092
   241
hoelzl@59092
   242
lemma map_prod_vimage: "map_prod f g -` (A \<times> B) = (f-`A) \<times> (g-`B)"
hoelzl@59092
   243
  by auto
hoelzl@59092
   244
hoelzl@59092
   245
lemma embed_measure_prod:
hoelzl@59092
   246
  assumes f: "inj f" and g: "inj g" and [simp]: "sigma_finite_measure M" "sigma_finite_measure N"
hoelzl@59092
   247
  shows "embed_measure M f \<Otimes>\<^sub>M embed_measure N g = embed_measure (M \<Otimes>\<^sub>M N) (\<lambda>(x, y). (f x, g y))"
hoelzl@59092
   248
    (is "?L = _")
hoelzl@59092
   249
  unfolding map_prod_def[symmetric]
hoelzl@59092
   250
proof (rule pair_measure_eqI)
hoelzl@59092
   251
  have fg[simp]: "\<And>A. inj_on (map_prod f g) A" "\<And>A. inj_on f A" "\<And>A. inj_on g A"
hoelzl@59092
   252
    using f g by (auto simp: inj_on_def)
hoelzl@62975
   253
hoelzl@63333
   254
  note complete_lattice_class.Sup_insert[simp del] ccSup_insert[simp del] SUP_insert[simp del]
hoelzl@63333
   255
     ccSUP_insert[simp del]
hoelzl@59092
   256
  show sets: "sets ?L = sets (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g))"
hoelzl@59092
   257
    unfolding map_prod_def[symmetric]
hoelzl@59092
   258
    apply (simp add: sets_pair_eq_sets_fst_snd sets_embed_eq_vimage_algebra
hoelzl@59092
   259
      cong: vimage_algebra_cong)
hoelzl@63333
   260
    apply (subst sets_vimage_Sup_eq[where Y="space (M \<Otimes>\<^sub>M N)"])
hoelzl@59092
   261
    apply (simp_all add: space_pair_measure[symmetric])
hoelzl@59092
   262
    apply (auto simp add: the_inv_into_f_f
hoelzl@59092
   263
                simp del: map_prod_simp
hoelzl@59092
   264
                del: prod_fun_imageE) []
hoelzl@63333
   265
    apply auto []
hoelzl@59092
   266
    apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq)
hoelzl@59092
   267
    apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure)
hoelzl@59092
   268
    apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq
hoelzl@59092
   269
       space_pair_measure[symmetric] map_prod_image[symmetric])
hoelzl@63333
   270
    apply (intro arg_cong[where f=sets] arg_cong[where f=Sup] arg_cong2[where f=insert] vimage_algebra_cong)
hoelzl@59092
   271
    apply (auto simp: map_prod_image the_inv_into_f_f
hoelzl@59092
   272
                simp del: map_prod_simp del: prod_fun_imageE)
hoelzl@59092
   273
    apply (simp_all add: the_inv_into_f_f space_pair_measure)
hoelzl@59092
   274
    done
hoelzl@59092
   275
hoelzl@59092
   276
  note measurable_embed_measure2[measurable]
hoelzl@59092
   277
  fix A B assume AB: "A \<in> sets (embed_measure M f)" "B \<in> sets (embed_measure N g)"
hoelzl@59092
   278
  moreover have "f -` A \<times> g -` B \<inter> space (M \<Otimes>\<^sub>M N) = (f -` A \<inter> space M) \<times> (g -` B \<inter> space N)"
hoelzl@59092
   279
    by (auto simp: space_pair_measure)
hoelzl@59092
   280
  ultimately show "emeasure (embed_measure M f) A * emeasure (embed_measure N g) B =
hoelzl@59092
   281
                     emeasure (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g)) (A \<times> B)"
hoelzl@59092
   282
    by (simp add: map_prod_vimage sets[symmetric] emeasure_embed_measure
hoelzl@59092
   283
                  sigma_finite_measure.emeasure_pair_measure_Times)
hoelzl@59092
   284
qed (insert assms, simp_all add: sigma_finite_embed_measure)
hoelzl@59092
   285
hoelzl@63333
   286
lemma mono_embed_measure:
hoelzl@63333
   287
  "space M = space M' \<Longrightarrow> sets M \<subseteq> sets M' \<Longrightarrow> sets (embed_measure M f) \<subseteq> sets (embed_measure M' f)"
hoelzl@63333
   288
  unfolding embed_measure_def
hoelzl@63333
   289
  apply (subst (1 2) sets_measure_of)
hoelzl@63333
   290
  apply (blast dest: sets.sets_into_space)
hoelzl@63333
   291
  apply (blast dest: sets.sets_into_space)
hoelzl@63333
   292
  apply simp
hoelzl@63333
   293
  apply (intro sigma_sets_mono')
hoelzl@63333
   294
  apply safe
hoelzl@63333
   295
  apply (simp add: subset_eq)
hoelzl@63333
   296
  apply metis
hoelzl@63333
   297
  done
hoelzl@63333
   298
hoelzl@59092
   299
lemma density_embed_measure:
hoelzl@59092
   300
  assumes inj: "inj f" and Mg[measurable]: "g \<in> borel_measurable (embed_measure M f)"
hoelzl@59092
   301
  shows "density (embed_measure M f) g = embed_measure (density M (g \<circ> f)) f" (is "?M1 = ?M2")
hoelzl@59092
   302
proof (rule measure_eqI)
hoelzl@59092
   303
  fix X assume X: "X \<in> sets ?M1"
hoelzl@62975
   304
  from inj have Mf[measurable]: "f \<in> measurable M (embed_measure M f)"
hoelzl@59092
   305
    by (rule measurable_embed_measure2)
hoelzl@62975
   306
  from Mg and X have "emeasure ?M1 X = \<integral>\<^sup>+ x. g x * indicator X x \<partial>embed_measure M f"
hoelzl@59092
   307
    by (subst emeasure_density) simp_all
hoelzl@59092
   308
  also from X have "... = \<integral>\<^sup>+ x. g (f x) * indicator X (f x) \<partial>M"
hoelzl@62975
   309
    by (subst embed_measure_eq_distr[OF inj], subst nn_integral_distr) auto
hoelzl@59092
   310
  also have "... = \<integral>\<^sup>+ x. g (f x) * indicator (f -` X \<inter> space M) x \<partial>M"
hoelzl@59092
   311
    by (intro nn_integral_cong) (auto split: split_indicator)
hoelzl@59092
   312
  also from X have "... = emeasure (density M (g \<circ> f)) (f -` X \<inter> space M)"
hoelzl@59092
   313
    by (subst emeasure_density) (simp_all add: measurable_comp[OF Mf Mg] measurable_sets[OF Mf])
hoelzl@62975
   314
  also from X and inj have "... = emeasure ?M2 X"
hoelzl@59092
   315
    by (subst emeasure_embed_measure) (simp_all add: sets_embed_measure)
hoelzl@59092
   316
  finally show "emeasure ?M1 X = emeasure ?M2 X" .
hoelzl@59092
   317
qed (simp_all add: sets_embed_measure inj)
hoelzl@59092
   318
hoelzl@59092
   319
lemma density_embed_measure':
hoelzl@59092
   320
  assumes inj: "inj f" and inv: "\<And>x. f' (f x) = x" and Mg[measurable]: "g \<in> borel_measurable M"
hoelzl@59092
   321
  shows "density (embed_measure M f) (g \<circ> f') = embed_measure (density M g) f"
hoelzl@59092
   322
proof-
hoelzl@59092
   323
  have "density (embed_measure M f) (g \<circ> f') = embed_measure (density M (g \<circ> f' \<circ> f)) f"
hoelzl@59092
   324
    by (rule density_embed_measure[OF inj])
hoelzl@62975
   325
       (rule measurable_comp, rule measurable_embed_measure1, subst measurable_cong,
hoelzl@59092
   326
        rule inv, rule measurable_ident_sets, simp, rule Mg)
hoelzl@59092
   327
  also have "density M (g \<circ> f' \<circ> f) = density M g"
hoelzl@59092
   328
    by (intro density_cong) (subst measurable_cong, simp add: o_def inv, simp_all add: Mg inv)
hoelzl@59092
   329
  finally show ?thesis .
hoelzl@59092
   330
qed
hoelzl@59092
   331
hoelzl@59092
   332
lemma inj_on_image_subset_iff:
hoelzl@59092
   333
  assumes "inj_on f C" "A \<subseteq> C"  "B \<subseteq> C"
hoelzl@59092
   334
  shows "f ` A \<subseteq> f ` B \<longleftrightarrow> A \<subseteq> B"
hoelzl@59092
   335
proof (intro iffI subsetI)
hoelzl@59092
   336
  fix x assume A: "f ` A \<subseteq> f ` B" and B: "x \<in> A"
hoelzl@59092
   337
  from B have "f x \<in> f ` A" by blast
hoelzl@59092
   338
  with A have "f x \<in> f ` B" by blast
hoelzl@59092
   339
  then obtain y where "f x = f y" and "y \<in> B" by blast
hoelzl@59092
   340
  with assms and B have "x = y" by (auto dest: inj_onD)
wenzelm@61808
   341
  with \<open>y \<in> B\<close> show "x \<in> B" by simp
hoelzl@59092
   342
qed auto
hoelzl@62975
   343
hoelzl@59092
   344
hoelzl@59092
   345
lemma AE_embed_measure':
hoelzl@59092
   346
  assumes inj: "inj_on f (space M)"
hoelzl@59092
   347
  shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
hoelzl@59092
   348
proof
hoelzl@59092
   349
  let ?M = "embed_measure M f"
hoelzl@59092
   350
  assume "AE x in ?M. P x"
hoelzl@59092
   351
  then obtain A where A_props: "A \<in> sets ?M" "emeasure ?M A = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> A"
hoelzl@59092
   352
    by (force elim: AE_E)
hoelzl@59092
   353
  then obtain A' where A'_props: "A = f ` A'" "A' \<in> sets M" by (auto simp: sets_embed_measure' inj)
hoelzl@62975
   354
  moreover have B: "{x\<in>space ?M. \<not>P x} = f ` {x\<in>space M. \<not>P (f x)}"
hoelzl@59092
   355
    by (auto simp: inj space_embed_measure)
hoelzl@59092
   356
  from A_props(3) have "{x\<in>space M. \<not>P (f x)} \<subseteq> A'"
hoelzl@59092
   357
    by (subst (asm) B, subst (asm) A'_props, subst (asm) inj_on_image_subset_iff[OF inj])
hoelzl@59092
   358
       (insert A'_props, auto dest: sets.sets_into_space)
hoelzl@59092
   359
  moreover from A_props A'_props have "emeasure M A' = 0"
hoelzl@59092
   360
    by (simp add: emeasure_embed_measure_image' inj)
hoelzl@59092
   361
  ultimately show "AE x in M. P (f x)" by (intro AE_I)
hoelzl@59092
   362
next
hoelzl@59092
   363
  let ?M = "embed_measure M f"
hoelzl@59092
   364
  assume "AE x in M. P (f x)"
hoelzl@59092
   365
  then obtain A where A_props: "A \<in> sets M" "emeasure M A = 0" "{x\<in>space M. \<not>P (f x)} \<subseteq> A"
hoelzl@59092
   366
    by (force elim: AE_E)
hoelzl@59092
   367
  hence "f`A \<in> sets ?M" "emeasure ?M (f`A) = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> f`A"
hoelzl@59092
   368
    by (auto simp: space_embed_measure emeasure_embed_measure_image' sets_embed_measure' inj)
hoelzl@59092
   369
  thus "AE x in ?M. P x" by (intro AE_I)
hoelzl@59092
   370
qed
hoelzl@59092
   371
hoelzl@59092
   372
lemma AE_embed_measure:
hoelzl@59092
   373
  assumes inj: "inj f"
hoelzl@59092
   374
  shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
hoelzl@59092
   375
  using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD)
hoelzl@59092
   376
Andreas@60065
   377
lemma nn_integral_monotone_convergence_SUP_countable:
hoelzl@62975
   378
  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ennreal"
Andreas@60065
   379
  assumes nonempty: "Y \<noteq> {}"
nipkow@67399
   380
  and chain: "Complete_Partial_Order.chain (\<le>) (f ` Y)"
Andreas@60065
   381
  and countable: "countable B"
haftmann@69260
   382
  shows "(\<integral>\<^sup>+ x. (SUP i\<in>Y. f i x) \<partial>count_space B) = (SUP i\<in>Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))"
Andreas@60065
   383
  (is "?lhs = ?rhs")
Andreas@60065
   384
proof -
Andreas@60065
   385
  let ?f = "(\<lambda>i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)"
haftmann@69260
   386
  have "?lhs = \<integral>\<^sup>+ x. (SUP i\<in>Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"
Andreas@60065
   387
    by(rule nn_integral_cong)(simp add: countable)
haftmann@69260
   388
  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i\<in>Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"
Andreas@60065
   389
    by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
haftmann@69260
   390
  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i\<in>Y. ?f i x) \<partial>count_space UNIV"
hoelzl@62975
   391
    by(simp add: nn_integral_count_space_indicator ennreal_indicator[symmetric] SUP_mult_right_ennreal nonempty)
haftmann@69260
   392
  also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)"
Andreas@60065
   393
  proof(rule nn_integral_monotone_convergence_SUP_nat)
nipkow@67399
   394
    show "Complete_Partial_Order.chain (\<le>) (?f ` Y)"
Andreas@60065
   395
      by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD)
hoelzl@62975
   396
  qed fact
haftmann@69260
   397
  also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"
Andreas@60065
   398
    by(simp add: nn_integral_count_space_indicator)
haftmann@69260
   399
  also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"
Andreas@60065
   400
    by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
hoelzl@62975
   401
  also have "\<dots> = ?rhs"
haftmann@69313
   402
    by(intro arg_cong2[where f = "\<lambda>A f. Sup (f ` A)"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)
Andreas@60065
   403
  finally show ?thesis .
Andreas@60065
   404
qed
Andreas@60065
   405
hoelzl@59092
   406
end