src/HOL/Probability/Embed_Measure.thy
author wenzelm
Mon, 19 Jan 2015 20:39:01 +0100
changeset 59409 b7cfe12acf2e
parent 59092 d469103c0737
child 60065 390de6d3a7b8
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     1
(*  Title:      HOL/Probability/Embed_Measure.thy
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     2
    Author:     Manuel Eberl, TU München
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     3
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     4
    Defines measure embeddings with injective functions, i.e. lifting a measure on some values 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     5
    to a measure on "tagged" values (e.g. embed_measure M Inl lifts a measure on values 'a to a 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     6
    measure on the left part of the sum type 'a + 'b)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     7
*)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     8
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
     9
section {* Embed Measure Spaces with a Function *}
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    10
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    11
theory Embed_Measure
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    12
imports Binary_Product_Measure
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    13
begin
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    14
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    15
definition embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    16
  "embed_measure M f = measure_of (f ` space M) {f ` A |A. A \<in> sets M} 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    17
                           (\<lambda>A. emeasure M (f -` A \<inter> space M))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    18
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    19
lemma space_embed_measure: "space (embed_measure M f) = f ` space M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    20
  unfolding embed_measure_def 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    21
  by (subst space_measure_of) (auto dest: sets.sets_into_space)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    22
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    23
lemma sets_embed_measure':
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    24
  assumes inj: "inj_on f (space M)" 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    25
  shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    26
  unfolding embed_measure_def
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    27
proof (intro sigma_algebra.sets_measure_of_eq sigma_algebra_iff2[THEN iffD2] conjI allI ballI impI)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    28
  fix s assume "s \<in> {f ` A |A. A \<in> sets M}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    29
  then obtain s' where s'_props: "s = f ` s'" "s' \<in> sets M" by auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    30
  hence "f ` space M - s = f ` (space M - s')" using inj
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    31
    by (auto dest: inj_onD sets.sets_into_space)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    32
  also have "... \<in> {f ` A |A. A \<in> sets M}" using s'_props by auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    33
  finally show "f ` space M - s \<in> {f ` A |A. A \<in> sets M}" .
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    34
next
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    35
  fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> {f ` A |A. A \<in> sets M}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    36
  then obtain A' where "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    37
    by (auto simp: subset_eq choice_iff)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    38
  moreover from this have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    39
  ultimately show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}" by blast
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    40
qed (auto dest: sets.sets_into_space)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    41
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    42
lemma the_inv_into_vimage:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    43
  "inj_on f X \<Longrightarrow> A \<subseteq> X \<Longrightarrow> the_inv_into X f -` A \<inter> (f`X) = f ` A"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    44
  by (auto simp: the_inv_into_f_f)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    45
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    46
lemma sets_embed_eq_vimage_algebra:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    47
  assumes "inj_on f (space M)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    48
  shows "sets (embed_measure M f) = sets (vimage_algebra (f`space M) (the_inv_into (space M) f) M)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    49
  by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 simple_image
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    50
           dest: sets.sets_into_space
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    51
           intro!: image_cong the_inv_into_vimage[symmetric])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    52
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    53
lemma sets_embed_measure:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    54
  assumes inj: "inj f" 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    55
  shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    56
  using assms by (subst sets_embed_measure') (auto intro!: inj_onI dest: injD)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    57
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    58
lemma in_sets_embed_measure: "A \<in> sets M \<Longrightarrow> f ` A \<in> sets (embed_measure M f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    59
  unfolding embed_measure_def
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    60
  by (intro in_measure_of) (auto dest: sets.sets_into_space)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    61
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    62
lemma measurable_embed_measure1:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    63
  assumes g: "(\<lambda>x. g (f x)) \<in> measurable M N" 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    64
  shows "g \<in> measurable (embed_measure M f) N"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    65
  unfolding measurable_def
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    66
proof safe
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    67
  fix A assume "A \<in> sets N"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    68
  with g have "(\<lambda>x. g (f x)) -` A \<inter> space M \<in> sets M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    69
    by (rule measurable_sets)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    70
  then have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) \<in> sets (embed_measure M f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    71
    by (rule in_sets_embed_measure)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    72
  also have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) = g -` A \<inter> space (embed_measure M f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    73
    by (auto simp: space_embed_measure)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    74
  finally show "g -` A \<inter> space (embed_measure M f) \<in> sets (embed_measure M f)" .
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    75
qed (insert measurable_space[OF assms], auto simp: space_embed_measure)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    76
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    77
lemma measurable_embed_measure2':
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    78
  assumes "inj_on f (space M)" 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    79
  shows "f \<in> measurable M (embed_measure M f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    80
proof-
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    81
  {
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    82
    fix A assume A: "A \<in> sets M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    83
    also from this have "A = A \<inter> space M" by auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    84
    also have "... = f -` f ` A \<inter> space M" using A assms
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    85
      by (auto dest: inj_onD sets.sets_into_space)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    86
    finally have "f -` f ` A \<inter> space M \<in> sets M" .
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    87
  }
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    88
  thus ?thesis using assms unfolding embed_measure_def
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    89
    by (intro measurable_measure_of) (auto dest: sets.sets_into_space)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    90
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    91
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    92
lemma measurable_embed_measure2:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    93
  assumes [simp]: "inj f" shows "f \<in> measurable M (embed_measure M f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    94
  by (auto simp: inj_vimage_image_eq embed_measure_def
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    95
           intro!: measurable_measure_of dest: sets.sets_into_space)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    96
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    97
lemma embed_measure_eq_distr':
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    98
  assumes "inj_on f (space M)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
    99
  shows "embed_measure M f = distr M (embed_measure M f) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   100
proof-
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   101
  have "distr M (embed_measure M f) f = 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   102
            measure_of (f ` space M) {f ` A |A. A \<in> sets M}
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   103
                       (\<lambda>A. emeasure M (f -` A \<inter> space M))" unfolding distr_def
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   104
      by (simp add: space_embed_measure sets_embed_measure'[OF assms])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   105
  also have "... = embed_measure M f" unfolding embed_measure_def ..
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   106
  finally show ?thesis ..
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   107
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   108
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   109
lemma embed_measure_eq_distr:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   110
    "inj f \<Longrightarrow> embed_measure M f = distr M (embed_measure M f) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   111
  by (rule embed_measure_eq_distr') (auto intro!: inj_onI dest: injD)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   112
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   113
lemma nn_integral_embed_measure:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   114
  "inj f \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   115
  nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   116
  apply (subst embed_measure_eq_distr, simp)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   117
  apply (subst nn_integral_distr)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   118
  apply (simp_all add: measurable_embed_measure2)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   119
  done
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   120
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   121
lemma emeasure_embed_measure':
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   122
    assumes "inj_on f (space M)" "A \<in> sets (embed_measure M f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   123
    shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   124
  by (subst embed_measure_eq_distr'[OF assms(1)])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   125
     (simp add: emeasure_distr[OF measurable_embed_measure2'[OF assms(1)] assms(2)])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   126
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   127
lemma emeasure_embed_measure:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   128
    assumes "inj f" "A \<in> sets (embed_measure M f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   129
    shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   130
 using assms by (intro emeasure_embed_measure') (auto intro!: inj_onI dest: injD)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   131
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   132
lemma embed_measure_comp: 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   133
  assumes [simp]: "inj f" "inj g"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   134
  shows "embed_measure (embed_measure M f) g = embed_measure M (g \<circ> f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   135
proof-
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   136
  have [simp]: "inj (\<lambda>x. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_comp)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   137
  note measurable_embed_measure2[measurable]
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   138
  have "embed_measure (embed_measure M f) g = 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   139
            distr M (embed_measure (embed_measure M f) g) (g \<circ> f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   140
      by (subst (1 2) embed_measure_eq_distr) 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   141
         (simp_all add: distr_distr sets_embed_measure cong: distr_cong)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   142
  also have "... = embed_measure M (g \<circ> f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   143
      by (subst (3) embed_measure_eq_distr, simp add: o_def, rule distr_cong)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   144
         (auto simp: sets_embed_measure o_def image_image[symmetric] 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   145
               intro: inj_comp cong: distr_cong)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   146
  finally show ?thesis .
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   147
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   148
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   149
lemma sigma_finite_embed_measure:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   150
  assumes "sigma_finite_measure M" and inj: "inj f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   151
  shows "sigma_finite_measure (embed_measure M f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   152
proof
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   153
  case goal1
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   154
  from assms(1) interpret sigma_finite_measure M .
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   155
  from sigma_finite_countable obtain A where
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   156
      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
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   157
  show ?case
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   158
  proof (intro exI[of _ "op ` f`A"] conjI allI)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   159
    from A_props show "countable (op ` f`A)" by auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   160
    from inj and A_props show "op ` f`A \<subseteq> sets (embed_measure M f)" 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   161
      by (auto simp: sets_embed_measure)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   162
    from A_props and inj show "\<Union>(op ` f`A) = space (embed_measure M f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   163
      by (auto simp: space_embed_measure intro!: imageI)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   164
    from A_props and inj show "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   165
      by (intro ballI, subst emeasure_embed_measure)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   166
         (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   167
  qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   168
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   169
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   170
lemma embed_measure_count_space: 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   171
    "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   172
  apply (subst distr_bij_count_space[of f A "f`A", symmetric])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   173
  apply (simp add: inj_on_def bij_betw_def)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   174
  apply (subst embed_measure_eq_distr)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   175
  apply simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   176
  apply (auto intro!: measure_eqI imageI simp: sets_embed_measure subset_image_iff)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   177
  apply blast
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   178
  apply (subst (1 2) emeasure_distr)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   179
  apply (auto simp: space_embed_measure sets_embed_measure)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   180
  done
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   181
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   182
lemma sets_embed_measure_alt:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   183
    "inj f \<Longrightarrow> sets (embed_measure M f) = (op`f) ` sets M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   184
  by (auto simp: sets_embed_measure)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   185
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   186
lemma emeasure_embed_measure_image':
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   187
  assumes "inj_on f (space M)" "X \<in> sets M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   188
  shows "emeasure (embed_measure M f) (f`X) = emeasure M X"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   189
proof-
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   190
  from assms have "emeasure (embed_measure M f) (f`X) = emeasure M (f -` f ` X \<inter> space M)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   191
    by (subst emeasure_embed_measure') (auto simp: sets_embed_measure')
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   192
  also from assms have "f -` f ` X \<inter> space M = X" by (auto dest: inj_onD sets.sets_into_space)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   193
  finally show ?thesis .
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   194
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   195
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   196
lemma emeasure_embed_measure_image:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   197
    "inj f \<Longrightarrow> X \<in> sets M \<Longrightarrow> emeasure (embed_measure M f) (f`X) = emeasure M X"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   198
  by (simp_all add: emeasure_embed_measure in_sets_embed_measure inj_vimage_image_eq)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   199
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   200
lemma embed_measure_eq_iff:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   201
  assumes "inj f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   202
  shows "embed_measure A f = embed_measure B f \<longleftrightarrow> A = B" (is "?M = ?N \<longleftrightarrow> _")
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   203
proof
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   204
  from assms have I: "inj (op` f)" by (auto intro: injI dest: injD)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   205
  assume asm: "?M = ?N"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   206
  hence "sets (embed_measure A f) = sets (embed_measure B f)" by simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   207
  with assms have "sets A = sets B" by (simp only: I inj_image_eq_iff sets_embed_measure_alt)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   208
  moreover {
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   209
    fix X assume "X \<in> sets A"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   210
    from asm have "emeasure ?M (f`X) = emeasure ?N (f`X)" by simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   211
    with `X \<in> sets A` and `sets A = sets B` and assms 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   212
        have "emeasure A X = emeasure B X" by (simp add: emeasure_embed_measure_image)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   213
  }
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   214
  ultimately show "A = B" by (rule measure_eqI)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   215
qed simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   216
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   217
lemma the_inv_into_in_Pi: "inj_on f A \<Longrightarrow> the_inv_into A f \<in> f ` A \<rightarrow> A"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   218
  by (auto simp: the_inv_into_f_f)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   219
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   220
lemma map_prod_image: "map_prod f g ` (A \<times> B) = (f`A) \<times> (g`B)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   221
  using map_prod_surj_on[OF refl refl] .
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   222
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   223
lemma map_prod_vimage: "map_prod f g -` (A \<times> B) = (f-`A) \<times> (g-`B)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   224
  by auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   225
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   226
lemma embed_measure_prod:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   227
  assumes f: "inj f" and g: "inj g" and [simp]: "sigma_finite_measure M" "sigma_finite_measure N"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   228
  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))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   229
    (is "?L = _")
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   230
  unfolding map_prod_def[symmetric]
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   231
proof (rule pair_measure_eqI)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   232
  have fg[simp]: "\<And>A. inj_on (map_prod f g) A" "\<And>A. inj_on f A" "\<And>A. inj_on g A"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   233
    using f g by (auto simp: inj_on_def)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   234
  
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   235
  show sets: "sets ?L = sets (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   236
    unfolding map_prod_def[symmetric]
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   237
    apply (simp add: sets_pair_eq_sets_fst_snd sets_embed_eq_vimage_algebra
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   238
      cong: vimage_algebra_cong)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   239
    apply (subst vimage_algebra_Sup_sigma)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   240
    apply (simp_all add: space_pair_measure[symmetric])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   241
    apply (auto simp add: the_inv_into_f_f
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   242
                simp del: map_prod_simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   243
                del: prod_fun_imageE) []
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   244
    apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   245
    apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   246
    apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   247
       space_pair_measure[symmetric] map_prod_image[symmetric])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   248
    apply (intro arg_cong[where f=sets] arg_cong[where f=Sup_sigma] arg_cong2[where f=insert] vimage_algebra_cong)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   249
    apply (auto simp: map_prod_image the_inv_into_f_f
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   250
                simp del: map_prod_simp del: prod_fun_imageE)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   251
    apply (simp_all add: the_inv_into_f_f space_pair_measure)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   252
    done
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   253
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   254
  note measurable_embed_measure2[measurable]
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   255
  fix A B assume AB: "A \<in> sets (embed_measure M f)" "B \<in> sets (embed_measure N g)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   256
  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)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   257
    by (auto simp: space_pair_measure)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   258
  ultimately show "emeasure (embed_measure M f) A * emeasure (embed_measure N g) B =
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   259
                     emeasure (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g)) (A \<times> B)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   260
    by (simp add: map_prod_vimage sets[symmetric] emeasure_embed_measure
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   261
                  sigma_finite_measure.emeasure_pair_measure_Times)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   262
qed (insert assms, simp_all add: sigma_finite_embed_measure)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   263
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   264
lemma density_embed_measure:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   265
  assumes inj: "inj f" and Mg[measurable]: "g \<in> borel_measurable (embed_measure M f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   266
  shows "density (embed_measure M f) g = embed_measure (density M (g \<circ> f)) f" (is "?M1 = ?M2")
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   267
proof (rule measure_eqI)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   268
  fix X assume X: "X \<in> sets ?M1"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   269
  from inj have Mf[measurable]: "f \<in> measurable M (embed_measure M f)" 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   270
    by (rule measurable_embed_measure2)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   271
  from Mg and X have "emeasure ?M1 X = \<integral>\<^sup>+ x. g x * indicator X x \<partial>embed_measure M f" 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   272
    by (subst emeasure_density) simp_all
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   273
  also from X have "... = \<integral>\<^sup>+ x. g (f x) * indicator X (f x) \<partial>M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   274
    by (subst embed_measure_eq_distr[OF inj], subst nn_integral_distr)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   275
       (auto intro!: borel_measurable_ereal_times borel_measurable_indicator)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   276
  also have "... = \<integral>\<^sup>+ x. g (f x) * indicator (f -` X \<inter> space M) x \<partial>M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   277
    by (intro nn_integral_cong) (auto split: split_indicator)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   278
  also from X have "... = emeasure (density M (g \<circ> f)) (f -` X \<inter> space M)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   279
    by (subst emeasure_density) (simp_all add: measurable_comp[OF Mf Mg] measurable_sets[OF Mf])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   280
  also from X and inj have "... = emeasure ?M2 X" 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   281
    by (subst emeasure_embed_measure) (simp_all add: sets_embed_measure)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   282
  finally show "emeasure ?M1 X = emeasure ?M2 X" .
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   283
qed (simp_all add: sets_embed_measure inj)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   284
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   285
lemma density_embed_measure':
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   286
  assumes inj: "inj f" and inv: "\<And>x. f' (f x) = x" and Mg[measurable]: "g \<in> borel_measurable M"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   287
  shows "density (embed_measure M f) (g \<circ> f') = embed_measure (density M g) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   288
proof-
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   289
  have "density (embed_measure M f) (g \<circ> f') = embed_measure (density M (g \<circ> f' \<circ> f)) f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   290
    by (rule density_embed_measure[OF inj])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   291
       (rule measurable_comp, rule measurable_embed_measure1, subst measurable_cong, 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   292
        rule inv, rule measurable_ident_sets, simp, rule Mg)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   293
  also have "density M (g \<circ> f' \<circ> f) = density M g"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   294
    by (intro density_cong) (subst measurable_cong, simp add: o_def inv, simp_all add: Mg inv)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   295
  finally show ?thesis .
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   296
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   297
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   298
lemma inj_on_image_subset_iff:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   299
  assumes "inj_on f C" "A \<subseteq> C"  "B \<subseteq> C"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   300
  shows "f ` A \<subseteq> f ` B \<longleftrightarrow> A \<subseteq> B"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   301
proof (intro iffI subsetI)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   302
  fix x assume A: "f ` A \<subseteq> f ` B" and B: "x \<in> A"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   303
  from B have "f x \<in> f ` A" by blast
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   304
  with A have "f x \<in> f ` B" by blast
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   305
  then obtain y where "f x = f y" and "y \<in> B" by blast
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   306
  with assms and B have "x = y" by (auto dest: inj_onD)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   307
  with `y \<in> B` show "x \<in> B" by simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   308
qed auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   309
  
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   310
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   311
lemma AE_embed_measure':
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   312
  assumes inj: "inj_on f (space M)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   313
  shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   314
proof
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   315
  let ?M = "embed_measure M f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   316
  assume "AE x in ?M. P x"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   317
  then obtain A where A_props: "A \<in> sets ?M" "emeasure ?M A = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> A"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   318
    by (force elim: AE_E)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   319
  then obtain A' where A'_props: "A = f ` A'" "A' \<in> sets M" by (auto simp: sets_embed_measure' inj)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   320
  moreover have B: "{x\<in>space ?M. \<not>P x} = f ` {x\<in>space M. \<not>P (f x)}" 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   321
    by (auto simp: inj space_embed_measure)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   322
  from A_props(3) have "{x\<in>space M. \<not>P (f x)} \<subseteq> A'"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   323
    by (subst (asm) B, subst (asm) A'_props, subst (asm) inj_on_image_subset_iff[OF inj])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   324
       (insert A'_props, auto dest: sets.sets_into_space)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   325
  moreover from A_props A'_props have "emeasure M A' = 0"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   326
    by (simp add: emeasure_embed_measure_image' inj)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   327
  ultimately show "AE x in M. P (f x)" by (intro AE_I)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   328
next
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   329
  let ?M = "embed_measure M f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   330
  assume "AE x in M. P (f x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   331
  then obtain A where A_props: "A \<in> sets M" "emeasure M A = 0" "{x\<in>space M. \<not>P (f x)} \<subseteq> A"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   332
    by (force elim: AE_E)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   333
  hence "f`A \<in> sets ?M" "emeasure ?M (f`A) = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> f`A"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   334
    by (auto simp: space_embed_measure emeasure_embed_measure_image' sets_embed_measure' inj)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   335
  thus "AE x in ?M. P x" by (intro AE_I)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   336
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   337
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   338
lemma AE_embed_measure:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   339
  assumes inj: "inj f"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   340
  shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   341
  using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   342
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
diff changeset
   343
end