src/HOL/Probability/Lebesgue_Measure.thy
changeset 41704 8c539202f854
parent 41689 3e39b0e730d6
child 41706 a207a858d1f6
     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"