generalizd measurability on restricted space; rule for integrability on compact sets

--- a/src/HOL/Probability/Borel_Space.thy	Fri May 30 15:56:30 2014 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Fri May 30 18:48:05 2014 +0200
@@ -124,53 +124,68 @@
   assumes \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M"
   shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
     (\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M"
-proof -
-  { fix X :: "ereal set" assume "X \<in> sets borel"
-    have 1: "(\<lambda>x. f x * indicator \<Omega> x) -` X \<inter> space M = 
-      (if 0 \<in> X then (f -` X \<inter> (\<Omega> \<inter> space M)) \<union> (space M - (\<Omega> \<inter> space M)) else f -` X \<inter> (\<Omega> \<inter> space M))" 
-      by (auto split: split_if_asm simp: indicator_def)
-    have *: "f -` X \<inter> (\<Omega> \<inter> space M) = 
-      (f -` X \<inter> (\<Omega> \<inter> space M) \<union> (space M - \<Omega> \<inter> space M)) - (space M - \<Omega> \<inter> space M)"
-      by auto
-    have "f -` X \<inter> (\<Omega> \<inter> space M) \<union> (space M - \<Omega> \<inter> space M) \<in> sets M
-      \<Longrightarrow> f -` X \<inter> (\<Omega> \<inter> space M) \<in> sets M"
-      by (subst *) auto
-    note this 1 }
-  note 1 = this(1) and 2 = this(2)
-
-  from 2 show ?thesis
-    by (auto simp add: measurable_def space_restrict_space sets_restrict_space_iff intro: 1 \<Omega>)
-qed
+  by (subst measurable_restrict_space_iff)
+     (auto simp: indicator_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_cong)
 
 lemma borel_measurable_restrict_space_iff:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M"
   shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
     (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M"
-proof -
-  { fix X :: "'b set" assume "X \<in> sets borel"
-    have 1: "(\<lambda>x. indicator \<Omega> x *\<^sub>R f x) -` X \<inter> space M = 
-      (if 0 \<in> X then (f -` X \<inter> (\<Omega> \<inter> space M)) \<union> (space M - (\<Omega> \<inter> space M)) else f -` X \<inter> (\<Omega> \<inter> space M))" 
-      by (auto split: split_if_asm simp: indicator_def)
-    have *: "f -` X \<inter> (\<Omega> \<inter> space M) = 
-      (f -` X \<inter> (\<Omega> \<inter> space M) \<union> (space M - \<Omega> \<inter> space M)) - (space M - \<Omega> \<inter> space M)"
-      by auto
-    have "f -` X \<inter> (\<Omega> \<inter> space M) \<union> (space M - \<Omega> \<inter> space M) \<in> sets M
-      \<Longrightarrow> f -` X \<inter> (\<Omega> \<inter> space M) \<in> sets M"
-      by (subst *) auto
-    note this 1 }
-  note 1 = this(1) and 2 = this(2)
+  by (subst measurable_restrict_space_iff)
+     (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] mult_ac cong del: if_cong)
+
+lemma cbox_borel[measurable]: "cbox a b \<in> sets borel"
+  by (auto intro: borel_closed)
+
+lemma borel_compact: "compact (A::'a::t2_space set) \<Longrightarrow> A \<in> sets borel"
+  by (auto intro: borel_closed dest!: compact_imp_closed)
 
-  from 2 show ?thesis
-    by (auto simp add: measurable_def space_restrict_space sets_restrict_space_iff intro: 1 \<Omega>)
+lemma borel_measurable_continuous_on_if:
+  assumes A: "A \<in> sets borel" and f: "continuous_on A f" and g: "continuous_on (- A) g"
+  shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> borel_measurable borel"
+proof (rule borel_measurableI)
+  fix S :: "'b set" assume "open S"
+  have "(\<lambda>x. if x \<in> A then f x else g x) -` S \<inter> space borel = (f -` S \<inter> A) \<union> (g -` S \<inter> -A)"
+    by (auto split: split_if_asm)
+  moreover obtain A' where "f -` S \<inter> A = A' \<inter> A" "open A'"
+    using continuous_on_open_invariant[THEN iffD1, rule_format, OF f `open S`] by metis
+  moreover obtain B' where "g -` S \<inter> -A = B' \<inter> -A" "open B'"
+    using continuous_on_open_invariant[THEN iffD1, rule_format, OF g `open S`] by metis
+  ultimately show "(\<lambda>x. if x \<in> A then f x else g x) -` S \<inter> space borel \<in> sets borel"
+    using A by auto
 qed
 
 lemma borel_measurable_continuous_on1:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
-  assumes "continuous_on UNIV f"
-  shows "f \<in> borel_measurable borel"
-  apply(rule borel_measurableI)
-  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
+  "continuous_on UNIV f \<Longrightarrow> f \<in> borel_measurable borel"
+  using borel_measurable_continuous_on_if[of UNIV f "\<lambda>_. undefined"]
+  by (auto intro: continuous_on_const)
+
+lemma borel_measurable_continuous_on:
+  assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. f (g x)) \<in> borel_measurable M"
+  using measurable_comp[OF g borel_measurable_continuous_on1[OF f]] by (simp add: comp_def)
+
+lemma borel_measurable_continuous_on_open':
+  "continuous_on A f \<Longrightarrow> open A \<Longrightarrow>
+    (\<lambda>x. if x \<in> A then f x else c) \<in> borel_measurable borel"
+  using borel_measurable_continuous_on_if[of A f "\<lambda>_. c"] by (auto intro: continuous_on_const)
+
+lemma borel_measurable_continuous_on_open:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
+  assumes cont: "continuous_on A f" "open A"
+  assumes g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. if g x \<in> A then f (g x) else c) \<in> borel_measurable M"
+  using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
+  by (simp add: comp_def)
+
+lemma borel_measurable_continuous_on_indicator:
+  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+  assumes A: "A \<in> sets borel" and f: "continuous_on A f"
+  shows "(\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable borel"
+  using borel_measurable_continuous_on_if[OF assms, of "\<lambda>_. 0"]
+  by (simp add: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] continuous_on_const
+           cong del: if_cong)
 
 lemma borel_eq_countable_basis:
   fixes B::"'a::topological_space set set"
@@ -216,37 +231,6 @@
   qed auto
 qed
 
-lemma borel_measurable_continuous_on:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
-  assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M"
-  shows "(\<lambda>x. f (g x)) \<in> borel_measurable M"
-  using measurable_comp[OF g borel_measurable_continuous_on1[OF f]] by (simp add: comp_def)
-
-lemma borel_measurable_continuous_on_open':
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
-  assumes cont: "continuous_on A f" "open A"
-  shows "(\<lambda>x. if x \<in> A then f x else c) \<in> borel_measurable borel" (is "?f \<in> _")
-proof (rule borel_measurableI)
-  fix S :: "'b set" assume "open S"
-  then have "open {x\<in>A. f x \<in> S}"
-    by (intro continuous_open_preimage[OF cont]) auto
-  then have *: "{x\<in>A. f x \<in> S} \<in> sets borel" by auto
-  have "?f -` S \<inter> space borel = 
-    {x\<in>A. f x \<in> S} \<union> (if c \<in> S then space borel - A else {})"
-    by (auto split: split_if_asm)
-  also have "\<dots> \<in> sets borel"
-    using * `open A` by auto
-  finally show "?f -` S \<inter> space borel \<in> sets borel" .
-qed
-
-lemma borel_measurable_continuous_on_open:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::t1_space"
-  assumes cont: "continuous_on A f" "open A"
-  assumes g: "g \<in> borel_measurable M"
-  shows "(\<lambda>x. if g x \<in> A then f (g x) else c) \<in> borel_measurable M"
-  using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
-  by (simp add: comp_def)
-
 lemma borel_measurable_continuous_Pair:
   fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
   assumes [measurable]: "f \<in> borel_measurable M"
@@ -852,11 +836,8 @@
       by (auto simp: ln_def) }
   note ln_imp = this
   have "(\<lambda>x. if f x \<in> {0<..} then ln (f x) else ln 0) \<in> borel_measurable M"
-  proof (rule borel_measurable_continuous_on_open[OF _ _ f])
-    show "continuous_on {0<..} ln"
-      by (auto intro!: continuous_at_imp_continuous_on DERIV_ln DERIV_isCont)
-    show "open ({0<..}::real set)" by auto
-  qed
+    by (rule borel_measurable_continuous_on_open[OF _ _ f])
+       (auto intro!: continuous_intros)
   also have "(\<lambda>x. if x \<in> {0<..} then ln x else ln 0) = ln"
     by (simp add: fun_eq_iff not_less ln_imp)
   finally show ?thesis .

--- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri May 30 15:56:30 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri May 30 18:48:05 2014 +0200
@@ -428,6 +428,16 @@
     by (simp add: indicator_def [abs_def] cbox_interval[symmetric])
 qed
 
+lemma
+  fixes a b ::"'a::ordered_euclidean_space"
+  shows lmeasure_cbox[simp]: "emeasure lebesgue (cbox a b) = ereal (content (cbox a b))"
+proof -
+  have "(indicator (UNIV \<inter> {a..b})::_\<Rightarrow>real) integrable_on UNIV"
+    unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def [abs_def] cbox_interval[symmetric])
+  from lmeasure_eq_integral[OF this] show ?thesis unfolding integral_indicator_UNIV
+    by (simp add: indicator_def [abs_def] cbox_interval[symmetric])
+qed
+
 lemma lmeasure_singleton[simp]:
   fixes a :: "'a::ordered_euclidean_space" shows "emeasure lebesgue {a} = 0"
   using lmeasure_atLeastAtMost[of a a] by simp
@@ -1035,40 +1045,56 @@
 
 subsection {* Fundamental Theorem of Calculus for the Lebesgue integral *}
 
+lemma emeasure_bounded_finite:
+  assumes "bounded A" shows "emeasure lborel A < \<infinity>"
+proof -
+  from bounded_subset_cbox[OF `bounded A`] obtain a b where "A \<subseteq> cbox a b"
+    by auto
+  then have "emeasure lborel A \<le> emeasure lborel (cbox a b)"
+    by (intro emeasure_mono) auto
+  then show ?thesis
+    by auto
+qed
+
+lemma emeasure_compact_finite: "compact A \<Longrightarrow> emeasure lborel A < \<infinity>"
+  using emeasure_bounded_finite[of A] by (auto intro: compact_imp_bounded)
+
+lemma borel_integrable_compact:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes "compact S" "continuous_on S f"
+  shows "integrable lborel (\<lambda>x. indicator S x *\<^sub>R f x)"
+proof cases
+  assume "S \<noteq> {}"
+  have "continuous_on S (\<lambda>x. norm (f x))"
+    using assms by (intro continuous_intros)
+  from continuous_attains_sup[OF `compact S` `S \<noteq> {}` this]
+  obtain M where M: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> M"
+    by auto
+
+  show ?thesis
+  proof (rule integrable_bound)
+    show "integrable lborel (\<lambda>x. indicator S x * M)"
+      using assms by (auto intro!: emeasure_compact_finite borel_compact integrable_mult_left)
+    show "(\<lambda>x. indicator S x *\<^sub>R f x) \<in> borel_measurable lborel"
+      using assms by (auto intro!: borel_measurable_continuous_on_indicator borel_compact)
+    show "AE x in lborel. norm (indicator S x *\<^sub>R f x) \<le> norm (indicator S x * M)"
+      by (auto split: split_indicator simp: abs_real_def dest!: M)
+  qed
+qed simp
+
 lemma borel_integrable_atLeastAtMost:
   fixes f :: "real \<Rightarrow> real"
   assumes f: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
   shows "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)" (is "integrable _ ?f")
-proof cases
-  assume "a \<le> b"
-
-  from isCont_Lb_Ub[OF `a \<le> b`, of f] f
-  obtain M L where
-    bounds: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> f x \<le> M" "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> L \<le> f x"
-    by metis
-
-  show ?thesis
-  proof (rule integrable_bound)
-    show "integrable lborel (\<lambda>x. max \<bar>M\<bar> \<bar>L\<bar> * indicator {a..b} x)"
-      by (intro integrable_mult_right integrable_real_indicator) simp_all
-    show "AE x in lborel. norm (?f x) \<le> norm (max \<bar>M\<bar> \<bar>L\<bar> * indicator {a..b} x)"
-    proof (rule AE_I2)
-      fix x show "norm (?f x) \<le> norm (max \<bar>M\<bar> \<bar>L\<bar> * indicator {a..b} x)"
-        using bounds[of x] by (auto split: split_indicator)
-    qed
-
-    let ?g = "\<lambda>x. if x = a then f a else if x = b then f b else if x \<in> {a <..< b} then f x else 0"
-    from f have "continuous_on {a <..< b} f"
-      by (subst continuous_on_eq_continuous_at) auto
-    then have "?g \<in> borel_measurable borel"
-      using borel_measurable_continuous_on_open[of "{a <..< b }" f "\<lambda>x. x" borel 0]
-      by (auto intro!: measurable_If[where P="\<lambda>x. x = a"] measurable_If[where P="\<lambda>x. x = b"])
-    also have "?g = ?f"
-      using `a \<le> b` by (intro ext) (auto split: split_indicator)
-    finally show "?f \<in> borel_measurable lborel"
-      by simp
-  qed
-qed simp
+proof -
+  have "integrable lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x)"
+  proof (rule borel_integrable_compact)
+    from f show "continuous_on {a..b} f"
+      by (auto intro: continuous_at_imp_continuous_on)
+  qed simp
+  then show ?thesis
+    by (auto simp: mult_commute)
+qed
 
 lemma has_field_derivative_subset:
   "(f has_field_derivative y) (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_field_derivative y) (at x within t)"

--- a/src/HOL/Probability/Sigma_Algebra.thy	Fri May 30 15:56:30 2014 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri May 30 18:48:05 2014 +0200
@@ -2355,5 +2355,35 @@
     f \<in> measurable M (restrict_space N \<Omega>)"
   by (simp add: measurable_def space_restrict_space sets_restrict_space_iff Pi_Int[symmetric])
 
+lemma measurable_restrict_space_iff:
+  assumes \<Omega>[simp, intro]: "\<Omega> \<inter> space M \<in> sets M" "c \<in> space N"
+  shows "f \<in> measurable (restrict_space M \<Omega>) N \<longleftrightarrow>
+    (\<lambda>x. if x \<in> \<Omega> then f x else c) \<in> measurable M N" (is "f \<in> measurable ?R N \<longleftrightarrow> ?f \<in> measurable M N")
+  unfolding measurable_def
+proof safe
+  fix x assume "f \<in> space ?R \<rightarrow> space N" "x \<in> space M" then show "?f x \<in> space N"
+    using `c\<in>space N` by (auto simp: space_restrict_space)
+next
+  fix x assume "?f \<in> space M \<rightarrow> space N" "x \<in> space ?R" then show "f x \<in> space N"
+    using `c\<in>space N` by (auto simp: space_restrict_space Pi_iff)
+next
+  fix X assume X: "X \<in> sets N"
+  assume *[THEN bspec]: "\<forall>y\<in>sets N. f -` y \<inter> space ?R \<in> sets ?R"
+  have "?f -` X \<inter> space M = (f -` X \<inter> (\<Omega> \<inter> space M)) \<union> (if c \<in> X then (space M - (\<Omega> \<inter> space M)) else {})"
+    by (auto split: split_if_asm)
+  also have "\<dots> \<in> sets M"
+    using *[OF X] by (auto simp add: space_restrict_space sets_restrict_space_iff)
+  finally show "?f -` X \<inter> space M \<in> sets M" .
+next
+  assume *[THEN bspec]: "\<forall>y\<in>sets N. ?f -` y \<inter> space M \<in> sets M"
+  fix X :: "'b set" assume X: "X \<in> sets N"
+  have "f -` X \<inter> (\<Omega> \<inter> space M) = (?f -` X \<inter> space M) \<inter> (\<Omega> \<inter> space M)"
+    by (auto simp: space_restrict_space)
+  also have "\<dots> \<in> sets M"
+    using *[OF X] by auto
+  finally show "f -` X \<inter> space ?R \<in> sets ?R"
+    by (auto simp add: sets_restrict_space_iff space_restrict_space)
+qed
+
 end