# HG changeset patch
# User hoelzl
# Date 1401805321 -7200
# Node ID 5cfcc616d485ffe8a920b6eab64be7bfea09cefb
# Parent  7b1bf424ec5fca5f73418893cf4997645c584b6f
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules

diff -r 7b1bf424ec5f -r 5cfcc616d485 src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Tue Jun 03 11:43:07 2014 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy	Tue Jun 03 16:22:01 2014 +0200
@@ -886,7 +886,7 @@
   "has_bochner_integral M f x \<Longrightarrow> integrable M f"
 
 definition lebesgue_integral ("integral\<^sup>L") where
-  "integral\<^sup>L M f = (THE x. has_bochner_integral M f x)"
+  "integral\<^sup>L M f = (if \<exists>x. has_bochner_integral M f x then THE x. has_bochner_integral M f x else 0)"
 
 syntax
   "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real" ("\<integral> _. _ \<partial>_" [60,61] 110)
@@ -910,7 +910,7 @@
   using has_bochner_integral_simple_bochner_integrable[of M f]
   by (simp add: has_bochner_integral_integral_eq)
 
-lemma not_integrable_integral_eq: "\<not> integrable M f \<Longrightarrow> integral\<^sup>L M f = (THE x. False)"
+lemma not_integrable_integral_eq: "\<not> integrable M f \<Longrightarrow> integral\<^sup>L M f = 0"
   unfolding integrable.simps lebesgue_integral_def by (auto intro!: arg_cong[where f=The])
 
 lemma integral_eq_cases:
@@ -934,13 +934,13 @@
 
 lemma integral_cong:
   "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L N g"
-  using assms by (simp cong: has_bochner_integral_cong add: lebesgue_integral_def)
+  using assms by (simp cong: has_bochner_integral_cong cong del: if_cong add: lebesgue_integral_def)
 
 lemma integral_cong_AE:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
     integral\<^sup>L M f = integral\<^sup>L M g"
   unfolding lebesgue_integral_def
-  by (intro has_bochner_integral_cong_AE arg_cong[where f=The] ext)
+  by (rule arg_cong[where x="has_bochner_integral M f"]) (intro has_bochner_integral_cong_AE ext)
 
 lemma integrable_add[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x + g x)"
   by (auto simp: integrable.simps)
@@ -1030,19 +1030,38 @@
     integral\<^sup>L M (\<lambda>x. T (f x)) = T (integral\<^sup>L M f)"
   by (metis has_bochner_integral_bounded_linear has_bochner_integral_integrable has_bochner_integral_integral_eq)
 
-lemma integral_indicator[simp]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
-  integral\<^sup>L M (\<lambda>x. indicator A x *\<^sub>R c) = measure M A *\<^sub>R c"
-  by (intro has_bochner_integral_integral_eq has_bochner_integral_indicator has_bochner_integral_integrable)
-
-lemma integral_real_indicator[simp]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
-  integral\<^sup>L M (indicator A :: 'a \<Rightarrow> real) = measure M A"
-  by (intro has_bochner_integral_integral_eq has_bochner_integral_real_indicator has_bochner_integral_integrable)
+lemma integral_bounded_linear':
+  assumes T: "bounded_linear T" and T': "bounded_linear T'"
+  assumes *: "\<not> (\<forall>x. T x = 0) \<Longrightarrow> (\<forall>x. T' (T x) = x)"
+  shows "integral\<^sup>L M (\<lambda>x. T (f x)) = T (integral\<^sup>L M f)"
+proof cases
+  assume "(\<forall>x. T x = 0)" then show ?thesis
+    by simp
+next
+  assume **: "\<not> (\<forall>x. T x = 0)"
+  show ?thesis
+  proof cases
+    assume "integrable M f" with T show ?thesis
+      by (rule integral_bounded_linear)
+  next
+    assume not: "\<not> integrable M f"
+    moreover have "\<not> integrable M (\<lambda>x. T (f x))"
+    proof
+      assume "integrable M (\<lambda>x. T (f x))"
+      from integrable_bounded_linear[OF T' this] not *[OF **]
+      show False
+        by auto
+    qed
+    ultimately show ?thesis
+      using T by (simp add: not_integrable_integral_eq linear_simps)
+  qed
+qed
 
 lemma integral_scaleR_left[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x *\<^sub>R c \<partial>M) = integral\<^sup>L M f *\<^sub>R c"
   by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_scaleR_left)
 
-lemma integral_scaleR_right[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c *\<^sub>R f x \<partial>M) = c *\<^sub>R integral\<^sup>L M f"
-  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_scaleR_right)
+lemma integral_scaleR_right[simp]: "(\<integral> x. c *\<^sub>R f x \<partial>M) = c *\<^sub>R integral\<^sup>L M f"
+  by (rule integral_bounded_linear'[OF bounded_linear_scaleR_right bounded_linear_scaleR_right[of "1 / c"]]) simp
 
 lemma integral_mult_left[simp]:
   fixes c :: "_::{real_normed_algebra,second_countable_topology}"
@@ -1054,6 +1073,16 @@
   shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c * f x \<partial>M) = c * integral\<^sup>L M f"
   by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_right)
 
+lemma integral_mult_left_zero[simp]:
+  fixes c :: "_::{real_normed_field,second_countable_topology}"
+  shows "(\<integral> x. f x * c \<partial>M) = integral\<^sup>L M f * c"
+  by (rule integral_bounded_linear'[OF bounded_linear_mult_left bounded_linear_mult_left[of "1 / c"]]) simp
+
+lemma integral_mult_right_zero[simp]:
+  fixes c :: "_::{real_normed_field,second_countable_topology}"
+  shows "(\<integral> x. c * f x \<partial>M) = c * integral\<^sup>L M f"
+  by (rule integral_bounded_linear'[OF bounded_linear_mult_right bounded_linear_mult_right[of "1 / c"]]) simp
+
 lemma integral_inner_left[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x \<bullet> c \<partial>M) = integral\<^sup>L M f \<bullet> c"
   by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_left)
 
@@ -1062,19 +1091,24 @@
 
 lemma integral_divide_zero[simp]:
   fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}"
-  shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integral\<^sup>L M (\<lambda>x. f x / c) = integral\<^sup>L M f / c"
-  by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_divide_zero)
+  shows "integral\<^sup>L M (\<lambda>x. f x / c) = integral\<^sup>L M f / c"
+  by (rule integral_bounded_linear'[OF bounded_linear_divide bounded_linear_mult_left[of c]]) simp
+
+lemma integral_minus[simp]: "integral\<^sup>L M (\<lambda>x. - f x) = - integral\<^sup>L M f"
+  by (rule integral_bounded_linear'[OF bounded_linear_minus[OF bounded_linear_ident] bounded_linear_minus[OF bounded_linear_ident]]) simp
 
-lemmas integral_minus[simp] =
-  integral_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
+lemma integral_complex_of_real[simp]: "integral\<^sup>L M (\<lambda>x. complex_of_real (f x)) = of_real (integral\<^sup>L M f)"
+  by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_Re]) simp
+
+lemma integral_cnj[simp]: "integral\<^sup>L M (\<lambda>x. cnj (f x)) = cnj (integral\<^sup>L M f)"
+  by (rule integral_bounded_linear'[OF bounded_linear_cnj bounded_linear_cnj]) simp
+
 lemmas integral_divide[simp] =
   integral_bounded_linear[OF bounded_linear_divide]
 lemmas integral_Re[simp] =
   integral_bounded_linear[OF bounded_linear_Re]
 lemmas integral_Im[simp] =
   integral_bounded_linear[OF bounded_linear_Im]
-lemmas integral_cnj[simp] =
-  integral_bounded_linear[OF bounded_linear_cnj]
 lemmas integral_of_real[simp] =
   integral_bounded_linear[OF bounded_linear_of_real]
 lemmas integral_fst[simp] =
@@ -1277,6 +1311,25 @@
   by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ereal_indicator nn_integral_indicator'
            cong: conj_cong)
 
+lemma integral_indicator[simp]: "integral\<^sup>L M (indicator A) = measure M (A \<inter> space M)"
+proof cases
+  assume *: "A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>"
+  have "integral\<^sup>L M (indicator A) = integral\<^sup>L M (indicator (A \<inter> space M))"
+    by (intro integral_cong) (auto split: split_indicator)
+  also have "\<dots> = measure M (A \<inter> space M)"
+    using * by (intro has_bochner_integral_integral_eq has_bochner_integral_real_indicator) auto
+  finally show ?thesis .
+next
+  assume *: "\<not> (A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>)"
+  have "integral\<^sup>L M (indicator A) = integral\<^sup>L M (indicator (A \<inter> space M) :: _ \<Rightarrow> real)"
+    by (intro integral_cong) (auto split: split_indicator)
+  also have "\<dots> = 0"
+    using * by (subst not_integrable_integral_eq) (auto simp: integrable_indicator_iff)
+  also have "\<dots> = measure M (A \<inter> space M)"
+    using * by (auto simp: measure_def emeasure_notin_sets)
+  finally show ?thesis .
+qed
+
 lemma
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
   assumes "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M" "integrable M w"
@@ -1547,20 +1600,22 @@
 
 lemma integral_nonneg_AE:
   fixes f :: "'a \<Rightarrow> real"
-  assumes [measurable]: "integrable M f" "AE x in M. 0 \<le> f x"
+  assumes [measurable]: "AE x in M. 0 \<le> f x"
   shows "0 \<le> integral\<^sup>L M f"
-proof -
-  have "0 \<le> ereal (integral\<^sup>L M (\<lambda>x. max 0 (f x)))"
+proof cases
+  assume [measurable]: "integrable M f"
+  then have "0 \<le> ereal (integral\<^sup>L M (\<lambda>x. max 0 (f x)))"
     by (subst integral_eq_nn_integral) (auto intro: real_of_ereal_pos nn_integral_nonneg assms)
   also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = integral\<^sup>L M f"
-    using assms(2) by (intro integral_cong_AE assms integrable_max) auto
+    using assms by (intro integral_cong_AE assms integrable_max) auto
   finally show ?thesis
     by simp
-qed
+qed (simp add: not_integrable_integral_eq)
 
 lemma integral_eq_zero_AE:
-  "f \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = 0) \<Longrightarrow> integral\<^sup>L M f = 0"
-  using integral_cong_AE[of f M "\<lambda>_. 0"] by simp
+  "(AE x in M. f x = 0) \<Longrightarrow> integral\<^sup>L M f = 0"
+  using integral_cong_AE[of f M "\<lambda>_. 0"]
+  by (cases "integrable M f") (simp_all add: not_integrable_integral_eq)
 
 lemma integral_nonneg_eq_0_iff_AE:
   fixes f :: "_ \<Rightarrow> real"
@@ -1618,13 +1673,17 @@
 qed fact
 
 lemma integral_real_bounded:
-  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "integral\<^sup>N M f \<le> ereal r"
+  assumes "AE x in M. 0 \<le> f x" "integral\<^sup>N M f \<le> ereal r"
   shows "integral\<^sup>L M f \<le> r"
-proof -
-  have "integrable M f"
-    using assms by (intro integrableI_real_bounded) auto
-  from nn_integral_eq_integral[OF this] assms show ?thesis
+proof cases
+  assume "integrable M f" from nn_integral_eq_integral[OF this] assms show ?thesis
     by simp
+next
+  assume "\<not> integrable M f"
+  moreover have "0 \<le> ereal r"
+    using nn_integral_nonneg assms(2) by (rule order_trans)
+  ultimately show ?thesis
+    by (simp add: not_integrable_integral_eq)
 qed
 
 subsection {* Restricted measure spaces *}
@@ -1780,11 +1839,11 @@
       by (intro integrable_indicator)
   
     have "integral\<^sup>L (distr M N g) (\<lambda>a. indicator A a *\<^sub>R c) = measure (distr M N g) A *\<^sub>R c"
-      using base by (subst integral_indicator) auto
+      using base by auto
     also have "\<dots> = measure M (g -` A \<inter> space M) *\<^sub>R c"
       by (subst measure_distr) auto
     also have "\<dots> = integral\<^sup>L M (\<lambda>a. indicator (g -` A \<inter> space M) a *\<^sub>R c)"
-      using base by (subst integral_indicator) (auto simp: emeasure_distr)
+      using base by (auto simp: emeasure_distr)
     also have "\<dots> = integral\<^sup>L M (\<lambda>a. indicator A (g a) *\<^sub>R c)"
       using int base by (intro integral_cong_AE) (auto simp: emeasure_distr split: split_indicator)
     finally show ?case .
@@ -2030,14 +2089,30 @@
   shows "integrable M f \<Longrightarrow> (\<integral>x. abs (f x) \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"
   using integral_norm_eq_0_iff[of M f] by simp
 
-lemma (in finite_measure) lebesgue_integral_const[simp]:
-  "(\<integral>x. a \<partial>M) = measure M (space M) *\<^sub>R a"
-  using integral_indicator[of "space M" M a]
-  by (simp del: integral_indicator integral_scaleR_left cong: integral_cong)
-
 lemma (in finite_measure) integrable_const[intro!, simp]: "integrable M (\<lambda>x. a)"
   using integrable_indicator[of "space M" M a] by (simp cong: integrable_cong)
 
+lemma lebesgue_integral_const[simp]: 
+  fixes a :: "'a :: {banach, second_countable_topology}"
+  shows "(\<integral>x. a \<partial>M) = measure M (space M) *\<^sub>R a"
+proof -
+  { assume "emeasure M (space M) = \<infinity>" "a \<noteq> 0"
+    then have ?thesis
+      by (simp add: not_integrable_integral_eq measure_def integrable_iff_bounded) }
+  moreover
+  { assume "a = 0" then have ?thesis by simp }
+  moreover
+  { assume "emeasure M (space M) \<noteq> \<infinity>"
+    interpret finite_measure M
+      proof qed fact
+    have "(\<integral>x. a \<partial>M) = (\<integral>x. indicator (space M) x *\<^sub>R a \<partial>M)"
+      by (intro integral_cong) auto
+    also have "\<dots> = measure M (space M) *\<^sub>R a"
+      by simp
+    finally have ?thesis . }
+  ultimately show ?thesis by blast
+qed
+
 lemma (in finite_measure) integrable_const_bound:
   fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
   shows "AE x in M. norm (f x) \<le> B \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> integrable M f"
@@ -2204,9 +2279,7 @@
   have "\<And>i. s i \<in> measurable (N \<Otimes>\<^sub>M M) (count_space UNIV)"
     by (rule measurable_simple_function) fact
 
-  def f' \<equiv> "\<lambda>i x. if integrable M (f x)
-    then simple_bochner_integral M (\<lambda>y. s i (x, y))
-    else (THE x. False)"
+  def f' \<equiv> "\<lambda>i x. if integrable M (f x) then simple_bochner_integral M (\<lambda>y. s i (x, y)) else 0"
 
   { fix i x assume "x \<in> space N"
     then have "simple_bochner_integral M (\<lambda>y. s i (x, y)) =
diff -r 7b1bf424ec5f -r 5cfcc616d485 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Tue Jun 03 11:43:07 2014 +0200
+++ b/src/HOL/Probability/Information.thy	Tue Jun 03 16:22:01 2014 +0200
@@ -863,11 +863,11 @@
   have " - log b (measure MX {x \<in> space MX. Px x \<noteq> 0}) = 
     - log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX)"
     using Px fin
-    by (subst integral_real_indicator) (auto simp: measure_def borel_measurable_ereal_iff)
+    by (auto simp: measure_def borel_measurable_ereal_iff)
   also have "- log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX) = - log b (\<integral> x. 1 / Px x \<partial>distr M MX X)"
     unfolding distributed_distr_eq_density[OF X] using Px
     apply (intro arg_cong[where f="log b"] arg_cong[where f=uminus])
-    by (subst integral_density) (auto simp: borel_measurable_ereal_iff intro!: integral_cong)
+    by (subst integral_density) (auto simp: borel_measurable_ereal_iff simp del: integral_indicator intro!: integral_cong)
   also have "\<dots> \<le> (\<integral> x. - log b (1 / Px x) \<partial>distr M MX X)"
   proof (rule X.jensens_inequality[of "\<lambda>x. 1 / Px x" "{0<..}" 0 1 "\<lambda>x. - log b x"])
     show "AE x in distr M MX X. 1 / Px x \<in> {0<..}"
diff -r 7b1bf424ec5f -r 5cfcc616d485 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Jun 03 11:43:07 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Jun 03 16:22:01 2014 +0200
@@ -590,10 +590,15 @@
 
 lemma lborel_integral_real_affine:
   fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" and c :: real
-  assumes c: "c \<noteq> 0" and f[measurable]: "integrable lborel f"
-  shows "(\<integral>x. f x \<partial> lborel) = \<bar>c\<bar> *\<^sub>R (\<integral>x. f (t + c * x) \<partial>lborel)"
-  using c f f[THEN borel_measurable_integrable] f[THEN lborel_integrable_real_affine, of c t]
-  by (subst lborel_real_affine[OF c, of t]) (simp add: integral_density integral_distr)
+  assumes c: "c \<noteq> 0" shows "(\<integral>x. f x \<partial> lborel) = \<bar>c\<bar> *\<^sub>R (\<integral>x. f (t + c * x) \<partial>lborel)"
+proof cases
+  assume f[measurable]: "integrable lborel f" then show ?thesis
+    using c f f[THEN borel_measurable_integrable] f[THEN lborel_integrable_real_affine, of c t]
+    by (subst lborel_real_affine[OF c, of t]) (simp add: integral_density integral_distr)
+next
+  assume "\<not> integrable lborel f" with c show ?thesis
+    by (simp add: lborel_integrable_real_affine_iff not_integrable_integral_eq)
+qed
 
 lemma divideR_right: 
   fixes x y :: "'a::real_normed_vector"