author hoelzl Fri Feb 04 14:16:48 2011 +0100 (2011-02-04) changeset 41704 8c539202f854 parent 41696 f69bb9077b02 child 41705 1100512e16d8
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
```     1.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Feb 02 22:48:24 2011 +0100
1.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Feb 04 14:16:48 2011 +0100
1.3 @@ -756,13 +756,6 @@
1.4    "p2e (e2p x) = (x::'a::ordered_euclidean_space)"
1.5    by (auto simp: euclidean_eq[where 'a='a] p2e_def e2p_def)
1.6
1.7 -lemma bij_inv_p2e_e2p:
1.8 -  shows "bij_inv ({..<DIM('a)} \<rightarrow>\<^isub>E UNIV) (UNIV :: 'a::ordered_euclidean_space set)
1.9 -     p2e e2p" (is "bij_inv ?P ?U _ _")
1.10 -proof (rule bij_invI)
1.11 -  show "p2e \<in> ?P \<rightarrow> ?U" "e2p \<in> ?U \<rightarrow> ?P" by (auto simp: e2p_def)
1.12 -qed auto
1.13 -
1.14  declare restrict_extensional[intro]
1.15
1.16  lemma e2p_extensional[intro]:"e2p (y::'a::ordered_euclidean_space) \<in> extensional {..<DIM('a)}"
1.17 @@ -850,10 +843,15 @@
1.18    then show "p2e -` A \<inter> space ?P \<in> sets ?P" by auto
1.19  qed simp
1.20
1.21 +lemma inj_e2p[intro, simp]: "inj e2p"
1.22 +proof (intro inj_onI conjI allI impI euclidean_eq[where 'a='a, THEN iffD2])
1.23 +  fix x y ::'a and i assume "e2p x = e2p y" "i < DIM('a)"
1.24 +  then show "x \$\$ i= y \$\$ i"
1.25 +    by (auto simp: e2p_def restrict_def fun_eq_iff elim!: allE[where x=i])
1.26 +qed
1.27 +
1.28  lemma e2p_Int:"e2p ` A \<inter> e2p ` B = e2p ` (A \<inter> B)" (is "?L = ?R")
1.29 -  apply(rule image_Int[THEN sym])
1.30 -  using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)]
1.31 -  unfolding bij_betw_def by auto
1.32 +  by (auto simp: image_Int[THEN sym])
1.33
1.34  lemma Int_stable_cuboids: fixes x::"'a::ordered_euclidean_space"
1.35    shows "Int_stable \<lparr>space = UNIV, sets = range (\<lambda>(a, b::'a). e2p ` {a..b})\<rparr>"
1.36 @@ -947,6 +945,31 @@
1.37      using lmeasure_measure_eq_borel_prod[OF A] by (simp add: range_e2p)
1.38  qed
1.39
1.40 +lemma borel_fubini_integrable:
1.41 +  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
1.42 +  shows "integrable lborel f \<longleftrightarrow>
1.43 +    integrable (lborel_space.P TYPE('a)) (\<lambda>x. f (p2e x))"
1.44 +    (is "_ \<longleftrightarrow> integrable ?B ?f")
1.45 +proof
1.46 +  assume "integrable lborel f"
1.47 +  moreover then have f: "f \<in> borel_measurable borel"
1.48 +    by auto
1.49 +  moreover with measurable_p2e
1.50 +  have "f \<circ> p2e \<in> borel_measurable ?B"
1.51 +    by (rule measurable_comp)
1.52 +  ultimately show "integrable ?B ?f"
1.53 +    by (simp add: comp_def borel_fubini_positiv_integral integrable_def)
1.54 +next
1.55 +  assume "integrable ?B ?f"
1.56 +  moreover then
1.57 +  have "?f \<circ> e2p \<in> borel_measurable (borel::'a algebra)"
1.58 +    by (auto intro!: measurable_e2p measurable_comp)
1.59 +  then have "f \<in> borel_measurable borel"
1.60 +    by (simp cong: measurable_cong)
1.61 +  ultimately show "integrable lborel f"
1.62 +    by (simp add: comp_def borel_fubini_positiv_integral integrable_def)
1.63 +qed
1.64 +
1.65  lemma borel_fubini:
1.66    fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
1.67    assumes f: "f \<in> borel_measurable borel"
```
```     2.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Feb 02 22:48:24 2011 +0100
2.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Feb 04 14:16:48 2011 +0100
2.3 @@ -769,48 +769,6 @@
2.4    show ?thesis by (simp add: comp_def)
2.5  qed
2.6
2.7 -lemma (in sigma_algebra) vimage_vimage_inv:
2.8 -  assumes f: "bij_betw f S (space M)"
2.9 -  assumes [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f (g x) = x" and g: "g \<in> space M \<rightarrow> S"
2.10 -  shows "sigma_algebra.vimage_algebra (vimage_algebra S f) (space M) g = M"
2.11 -proof -
2.12 -  interpret T: sigma_algebra "vimage_algebra S f"
2.13 -    using f by (safe intro!: sigma_algebra_vimage bij_betw_imp_funcset)
2.14 -
2.15 -  have inj: "inj_on f S" and [simp]: "f`S = space M"
2.16 -    using f unfolding bij_betw_def by auto
2.17 -
2.18 -  { fix A assume A: "A \<in> sets M"
2.19 -    have "g -` f -` A \<inter> g -` S \<inter> space M = (f \<circ> g) -` A \<inter> space M"
2.20 -      using g by auto
2.21 -    also have "\<dots> = A"
2.22 -      using `A \<in> sets M`[THEN sets_into_space] by auto
2.23 -    finally have "g -` f -` A \<inter> g -` S \<inter> space M = A" . }
2.24 -  note X = this
2.25 -  show ?thesis
2.26 -    unfolding T.vimage_algebra_def unfolding vimage_algebra_def
2.27 -    by (simp add: image_compose[symmetric] comp_def X cong: image_cong)
2.28 -qed
2.29 -
2.30 -lemma (in sigma_algebra) measurable_vimage_iff:
2.31 -  fixes f :: "'b \<Rightarrow> 'a" assumes f: "bij_betw f S (space M)"
2.32 -  shows "g \<in> measurable M M' \<longleftrightarrow> (g \<circ> f) \<in> measurable (vimage_algebra S f) M'"
2.33 -proof
2.34 -  assume "g \<in> measurable M M'"
2.35 -  from measurable_vimage[OF this f[THEN bij_betw_imp_funcset]]
2.36 -  show "(g \<circ> f) \<in> measurable (vimage_algebra S f) M'" unfolding comp_def .
2.37 -next
2.38 -  interpret v: sigma_algebra "vimage_algebra S f"
2.39 -    using f[THEN bij_betw_imp_funcset] by (rule sigma_algebra_vimage)
2.40 -  note f' = f[THEN bij_betw_the_inv_into]
2.41 -  assume "g \<circ> f \<in> measurable (vimage_algebra S f) M'"
2.42 -  from v.measurable_vimage[OF this, unfolded space_vimage_algebra, OF f'[THEN bij_betw_imp_funcset]]
2.43 -  show "g \<in> measurable M M'"
2.44 -    using f f'[THEN bij_betw_imp_funcset] f[unfolded bij_betw_def]
2.45 -    by (subst (asm) vimage_vimage_inv)
2.46 -       (simp_all add: f_the_inv_into_f cong: measurable_cong)
2.47 -qed
2.48 -
2.49  lemma sigma_sets_vimage:
2.50    assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S"
2.51    shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A"
2.52 @@ -1417,93 +1375,10 @@
2.53      by (auto simp: image_space_def)
2.54  qed
2.55
2.56 -subsection "Bijective functions with inverse"
2.57 -
2.58 -definition "bij_inv A B f g \<longleftrightarrow>
2.59 -  f \<in> A \<rightarrow> B \<and> g \<in> B \<rightarrow> A \<and> (\<forall>x\<in>A. g (f x) = x) \<and> (\<forall>x\<in>B. f (g x) = x)"
2.60 -
2.61 -lemma bij_inv_symmetric[sym]: "bij_inv A B f g \<Longrightarrow> bij_inv B A g f"
2.62 -  unfolding bij_inv_def by auto
2.63 -
2.64 -lemma bij_invI:
2.65 -  assumes "f \<in> A \<rightarrow> B" "g \<in> B \<rightarrow> A"
2.66 -  and "\<And>x. x \<in> A \<Longrightarrow> g (f x) = x"
2.67 -  and "\<And>x. x \<in> B \<Longrightarrow> f (g x) = x"
2.68 -  shows "bij_inv A B f g"
2.69 -  using assms unfolding bij_inv_def by auto
2.70 -
2.71 -lemma bij_invE:
2.72 -  assumes "bij_inv A B f g"
2.73 -    "\<lbrakk> f \<in> A \<rightarrow> B ; g \<in> B \<rightarrow> A ;
2.74 -        (\<And>x. x \<in> A \<Longrightarrow> g (f x) = x) ;
2.75 -        (\<And>x. x \<in> B \<Longrightarrow> f (g x) = x) \<rbrakk> \<Longrightarrow> P"
2.76 -  shows P
2.77 -  using assms unfolding bij_inv_def by auto
2.78 -
2.79 -lemma bij_inv_bij_betw:
2.80 -  assumes "bij_inv A B f g"
2.81 -  shows "bij_betw f A B" "bij_betw g B A"
2.82 -  using assms by (auto intro: bij_betwI elim!: bij_invE)
2.83 -
2.84 -lemma bij_inv_vimage_vimage:
2.85 -  assumes "bij_inv A B f e"
2.86 -  shows "f -` (e -` X \<inter> B) \<inter> A = X \<inter> A"
2.87 -  using assms by (auto elim!: bij_invE)
2.88 -
2.89 -lemma (in sigma_algebra) measurable_vimage_iff_inv:
2.90 -  fixes f :: "'b \<Rightarrow> 'a" assumes "bij_inv S (space M) f g"
2.91 -  shows "h \<in> measurable (vimage_algebra S f) M' \<longleftrightarrow> (\<lambda>x. h (g x)) \<in> measurable M M'"
2.92 -  unfolding measurable_vimage_iff[OF bij_inv_bij_betw(1), OF assms]
2.93 -proof (rule measurable_cong)
2.94 -  fix w assume "w \<in> space (vimage_algebra S f)"
2.95 -  then have "w \<in> S" by auto
2.96 -  then show "h w = ((\<lambda>x. h (g x)) \<circ> f) w"
2.97 -    using assms by (auto elim: bij_invE)
2.98 -qed
2.99 -
2.100 -lemma vimage_algebra_sigma:
2.101 -  assumes bi: "bij_inv (space (sigma F)) (space (sigma E)) f e"
2.102 -    and "sets E \<subseteq> Pow (space E)" and F: "sets F \<subseteq> Pow (space F)"
2.103 -    and "more E = more F"
2.104 -    and "f \<in> measurable F E" "e \<in> measurable E F"
2.105 -  shows "sigma_algebra.vimage_algebra (sigma E) (space (sigma F)) f = sigma F"
2.106 -proof -
2.107 -  interpret sigma_algebra "sigma E"
2.108 -    using assms by (intro sigma_algebra_sigma) auto
2.109 -  have eq: "sets F = (\<lambda>X. f -` X \<inter> space F) ` sets E"
2.110 -  proof safe
2.111 -    fix X assume "X \<in> sets F"
2.112 -    then have "e -` X \<inter> space E \<in> sets E"
2.113 -      using `e \<in> measurable E F` unfolding measurable_def by auto
2.114 -    then show "X \<in>(\<lambda>Y. f -` Y \<inter> space F) ` sets E"
2.115 -      apply (rule rev_image_eqI)
2.116 -      unfolding bij_inv_vimage_vimage[OF bi[simplified]]
2.117 -      using F `X \<in> sets F` by auto
2.118 -  next
2.119 -    fix X assume "X \<in> sets E" then show "f -` X \<inter> space F \<in> sets F"
2.120 -      using `f \<in> measurable F E` unfolding measurable_def by auto
2.121 -  qed
2.122 -  show "vimage_algebra (space (sigma F)) f = sigma F"
2.123 -    unfolding vimage_algebra_def using assms
2.124 -    by (auto simp: bij_inv_def eq sigma_sets_vimage[symmetric] sigma_def)
2.125 -qed
2.126 -
2.127  lemma measurable_sigma_sigma:
2.128    assumes M: "sets M \<subseteq> Pow (space M)" and N: "sets N \<subseteq> Pow (space N)"
2.129    shows "f \<in> measurable M N \<Longrightarrow> f \<in> measurable (sigma M) (sigma N)"
2.130    using sigma_algebra.measurable_subset[OF sigma_algebra_sigma[OF M], of N]
2.131    using measurable_up_sigma[of M N] N by auto
2.132
2.133 -lemma bij_inv_the_inv_into:
2.134 -  assumes "bij_betw f A B" shows "bij_inv A B f (the_inv_into A f)"
2.135 -proof (rule bij_invI)
2.136 -  show "the_inv_into A f \<in> B \<rightarrow> A"
2.137 -    using bij_betw_the_inv_into[OF assms] by (rule bij_betw_imp_funcset)
2.138 -  show "f \<in> A \<rightarrow> B" using assms by (rule bij_betw_imp_funcset)
2.139 -  show "\<And>x. x \<in> A \<Longrightarrow> the_inv_into A f (f x) = x"
2.140 -    "\<And>x. x \<in> B \<Longrightarrow> f (the_inv_into A f x) = x"
2.141 -    using the_inv_into_f_f[of f A] f_the_inv_into_f[of f A]
2.142 -    using assms by (auto simp: bij_betw_def)
2.143 -qed
2.144 -
2.145  end
```