# HG changeset patch
# User hoelzl
# Date 1301500436 -7200
# Node ID f88c7315d72d4f7eb2e95d135367311c34da7949
# Parent  392fd6c4669c8a5c389e2c79bf9498fe41e2f1aa
add lebesgue_real_affine

diff -r 392fd6c4669c -r f88c7315d72d src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Mar 30 11:32:52 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Mar 30 17:53:56 2011 +0200
@@ -980,4 +980,97 @@
   shows "integral\<^isup>L lborel f = \<integral>x. f (p2e x) \<partial>(lborel_space.P DIM('a))"
   using f by (simp add: borel_fubini_positiv_integral lebesgue_integral_def)
 
+
+lemma Int_stable_atLeastAtMost:
+  "Int_stable \<lparr>space = UNIV, sets = range (\<lambda>(a,b). {a::'a::ordered_euclidean_space .. b}) \<rparr>"
+proof (simp add: Int_stable_def image_iff, intro allI)
+  fix a1 b1 a2 b2 :: 'a
+  have "\<forall>i<DIM('a). \<exists>a b. {a1$$i..b1$$i} \<inter> {a2$$i..b2$$i} = {a..b}" by auto
+  then have "\<exists>a b. \<forall>i<DIM('a). {a1$$i..b1$$i} \<inter> {a2$$i..b2$$i} = {a i..b i}"
+    unfolding choice_iff' .
+  then guess a b by safe
+  then have "{a1..b1} \<inter> {a2..b2} = {(\<chi>\<chi> i. a i) .. (\<chi>\<chi> i. b i)}"
+    by (simp add: set_eq_iff eucl_le[where 'a='a] all_conj_distrib[symmetric]) blast
+  then show "\<exists>a' b'. {a1..b1} \<inter> {a2..b2} = {a'..b'}" by blast
+qed
+
+lemma (in sigma_algebra) borel_measurable_sets:
+  assumes "f \<in> measurable borel M" "A \<in> sets M"
+  shows "f -` A \<in> sets borel"
+  using measurable_sets[OF assms] by simp
+
+lemma (in sigma_algebra) measurable_identity[intro,simp]:
+  "(\<lambda>x. x) \<in> measurable M M"
+  unfolding measurable_def by auto
+
+lemma lebesgue_real_affine:
+  fixes X :: "real set"
+  assumes "X \<in> sets borel" and "c \<noteq> 0"
+  shows "measure lebesgue X = extreal \<bar>c\<bar> * measure lebesgue ((\<lambda>x. t + c * x) -` X)"
+    (is "_ = ?\<nu> X")
+proof -
+  let ?E = "\<lparr>space = UNIV, sets = range (\<lambda>(a,b). {a::real .. b})\<rparr> :: real algebra"
+  let "?M \<nu>" = "\<lparr>space = space ?E, sets = sets (sigma ?E), measure = \<nu>\<rparr> :: real measure_space"
+  have *: "?M (measure lebesgue) = lborel"
+    unfolding borel_eq_atLeastAtMost[symmetric]
+    by (simp add: lborel_def lebesgue_def)
+  have **: "?M ?\<nu> = lborel \<lparr> measure := ?\<nu> \<rparr>"
+    unfolding borel_eq_atLeastAtMost[symmetric]
+    by (simp add: lborel_def lebesgue_def)
+  show ?thesis
+  proof (rule measure_unique_Int_stable[where X=X, OF Int_stable_atLeastAtMost], unfold * **)
+    show "X \<in> sets (sigma ?E)"
+      unfolding borel_eq_atLeastAtMost[symmetric] by fact
+    have "\<And>x. \<exists>xa. x \<in> cube xa" apply(rule_tac x=x in mem_big_cube) by fastsimp
+    then show "(\<Union>i. cube i) = space ?E" by auto
+    show "incseq cube" by (intro incseq_SucI cube_subset_Suc)
+    show "range cube \<subseteq> sets ?E"
+      unfolding cube_def_raw by auto
+    show "\<And>i. measure lebesgue (cube i) \<noteq> \<infinity>"
+      by (simp add: cube_def)
+    show "measure_space lborel" by default
+    then interpret sigma_algebra "lborel\<lparr>measure := ?\<nu>\<rparr>"
+      by (auto simp add: measure_space_def)
+    show "measure_space (lborel\<lparr>measure := ?\<nu>\<rparr>)"
+    proof
+      show "positive (lborel\<lparr>measure := ?\<nu>\<rparr>) (measure (lborel\<lparr>measure := ?\<nu>\<rparr>))"
+        by (auto simp: positive_def intro!: extreal_0_le_mult borel.borel_measurable_sets)
+      show "countably_additive (lborel\<lparr>measure := ?\<nu>\<rparr>) (measure (lborel\<lparr>measure := ?\<nu>\<rparr>))"
+      proof (simp add: countably_additive_def, safe)
+        fix A :: "nat \<Rightarrow> real set" assume A: "range A \<subseteq> sets borel" "disjoint_family A"
+        then have Ai: "\<And>i. A i \<in> sets borel" by auto
+        have "(\<Sum>n. measure lebesgue ((\<lambda>x. t + c * x) -` A n)) = measure lebesgue (\<Union>n. (\<lambda>x. t + c * x) -` A n)"
+        proof (intro lborel.measure_countably_additive)
+          { fix n have "(\<lambda>x. t + c * x) -` A n \<inter> space borel \<in> sets borel"
+              using A borel.measurable_ident unfolding id_def
+              by (intro measurable_sets[where A=borel] borel.borel_measurable_add[OF _ borel.borel_measurable_times]) auto }
+          then show "range (\<lambda>i. (\<lambda>x. t + c * x) -` A i) \<subseteq> sets borel" by auto
+          from `disjoint_family A`
+          show "disjoint_family (\<lambda>i. (\<lambda>x. t + c * x) -` A i)"
+            by (rule disjoint_family_on_bisimulation) auto
+        qed
+        with Ai show "(\<Sum>n. ?\<nu> (A n)) = ?\<nu> (UNION UNIV A)"
+          by (subst suminf_cmult_extreal)
+             (auto simp: vimage_UN borel.borel_measurable_sets)
+      qed
+    qed
+    fix X assume "X \<in> sets ?E"
+    then obtain a b where [simp]: "X = {a .. b}" by auto
+    show "measure lebesgue X = ?\<nu> X"
+    proof cases
+      assume "0 < c"
+      then have "(\<lambda>x. t + c * x) -` {a..b} = {(a - t) / c .. (b - t) / c}"
+        by (auto simp: field_simps)
+      with `0 < c` show ?thesis
+        by (cases "a \<le> b") (auto simp: field_simps)
+    next
+      assume "\<not> 0 < c" with `c \<noteq> 0` have "c < 0" by auto
+      then have *: "(\<lambda>x. t + c * x) -` {a..b} = {(b - t) / c .. (a - t) / c}"
+        by (auto simp: field_simps)
+      with `c < 0` show ?thesis
+        by (cases "a \<le> b") (auto simp: field_simps)
+    qed
+  qed
+qed
+
 end