add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
authorhoelzl
Fri Feb 04 14:16:48 2011 +0100 (2011-02-04)
changeset 417048c539202f854
parent 41696 f69bb9077b02
child 41705 1100512e16d8
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Sigma_Algebra.thy
     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