moved some theorems from the CLT proof; reordered some theorems / notation
authorhoelzl
Thu Dec 17 16:43:36 2015 +0100 (2015-12-17)
changeset 61880ff4d33058566
parent 61879 e4f9d8f094fe
child 61881 b4bfa62e799d
moved some theorems from the CLT proof; reordered some theorems / notation
src/HOL/Library/ContNotDenum.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Lebesgue_Integral_Substitution.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Set_Integral.thy
     1.1 --- a/src/HOL/Library/ContNotDenum.thy	Sun Dec 20 13:56:02 2015 +0100
     1.2 +++ b/src/HOL/Library/ContNotDenum.thy	Thu Dec 17 16:43:36 2015 +0100
     1.3 @@ -143,4 +143,20 @@
     1.4    using uncountable_open_interval [of a b]
     1.5    by (metis countable_Un_iff ivl_disj_un_singleton(4))
     1.6  
     1.7 +lemma real_interval_avoid_countable_set:
     1.8 +  fixes a b :: real and A :: "real set"
     1.9 +  assumes "a < b" and "countable A"
    1.10 +  shows "\<exists>x\<in>{a<..<b}. x \<notin> A"
    1.11 +proof -
    1.12 +  from `countable A` have "countable (A \<inter> {a<..<b})" by auto
    1.13 +  moreover with `a < b` have "\<not> countable {a<..<b}" 
    1.14 +    by (simp add: uncountable_open_interval)
    1.15 +  ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}" by auto
    1.16 +  hence "A \<inter> {a<..<b} \<subset> {a<..<b}" 
    1.17 +    by (intro psubsetI, auto)
    1.18 +  hence "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}"
    1.19 +    by (rule psubset_imp_ex_mem)
    1.20 +  thus ?thesis by auto
    1.21 +qed
    1.22 +
    1.23  end
     2.1 --- a/src/HOL/Library/Extended_Real.thy	Sun Dec 20 13:56:02 2015 +0100
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Dec 17 16:43:36 2015 +0100
     2.3 @@ -2450,6 +2450,16 @@
     2.4  lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
     2.5    by (auto dest!: lim_real_of_ereal)
     2.6  
     2.7 +lemma convergent_real_imp_convergent_ereal:
     2.8 +  assumes "convergent a"
     2.9 +  shows "convergent (\<lambda>n. ereal (a n))" and "lim (\<lambda>n. ereal (a n)) = ereal (lim a)"
    2.10 +proof -
    2.11 +  from assms obtain L where L: "a ----> L" unfolding convergent_def ..
    2.12 +  hence lim: "(\<lambda>n. ereal (a n)) ----> ereal L" using lim_ereal by auto
    2.13 +  thus "convergent (\<lambda>n. ereal (a n))" unfolding convergent_def ..
    2.14 +  thus "lim (\<lambda>n. ereal (a n)) = ereal (lim a)" using lim L limI by metis
    2.15 +qed
    2.16 +
    2.17  lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
    2.18  proof -
    2.19    {
    2.20 @@ -3223,7 +3233,6 @@
    2.21    thus "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>" by simp_all
    2.22  qed
    2.23  
    2.24 -
    2.25  lemma SUP_ereal_add_directed:
    2.26    fixes f g :: "'a \<Rightarrow> ereal"
    2.27    assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
    2.28 @@ -3293,50 +3302,6 @@
    2.29      done
    2.30  qed
    2.31  
    2.32 -subsection \<open>More Limits\<close>
    2.33 -
    2.34 -lemma convergent_limsup_cl:
    2.35 -  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
    2.36 -  shows "convergent X \<Longrightarrow> limsup X = lim X"
    2.37 -  by (auto simp: convergent_def limI lim_imp_Limsup)
    2.38 -
    2.39 -lemma lim_increasing_cl:
    2.40 -  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
    2.41 -  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
    2.42 -proof
    2.43 -  show "f ----> (SUP n. f n)"
    2.44 -    using assms
    2.45 -    by (intro increasing_tendsto)
    2.46 -       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
    2.47 -qed
    2.48 -
    2.49 -lemma lim_decreasing_cl:
    2.50 -  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
    2.51 -  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
    2.52 -proof
    2.53 -  show "f ----> (INF n. f n)"
    2.54 -    using assms
    2.55 -    by (intro decreasing_tendsto)
    2.56 -       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
    2.57 -qed
    2.58 -
    2.59 -lemma compact_complete_linorder:
    2.60 -  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
    2.61 -  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
    2.62 -proof -
    2.63 -  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
    2.64 -    using seq_monosub[of X]
    2.65 -    unfolding comp_def
    2.66 -    by auto
    2.67 -  then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
    2.68 -    by (auto simp add: monoseq_def)
    2.69 -  then obtain l where "(X \<circ> r) ----> l"
    2.70 -     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
    2.71 -     by auto
    2.72 -  then show ?thesis
    2.73 -    using \<open>subseq r\<close> by auto
    2.74 -qed
    2.75 -
    2.76  lemma ereal_dense3:
    2.77    fixes x y :: ereal
    2.78    shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
     3.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Sun Dec 20 13:56:02 2015 +0100
     3.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Thu Dec 17 16:43:36 2015 +0100
     3.3 @@ -351,5 +351,53 @@
     3.4    finally show ?thesis
     3.5      by (auto simp: Liminf_def)
     3.6  qed
     3.7 +subsection \<open>More Limits\<close>
     3.8 +
     3.9 +lemma convergent_limsup_cl:
    3.10 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
    3.11 +  shows "convergent X \<Longrightarrow> limsup X = lim X"
    3.12 +  by (auto simp: convergent_def limI lim_imp_Limsup)
    3.13 +
    3.14 +lemma convergent_liminf_cl:
    3.15 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
    3.16 +  shows "convergent X \<Longrightarrow> liminf X = lim X"
    3.17 +  by (auto simp: convergent_def limI lim_imp_Liminf)
    3.18 +
    3.19 +lemma lim_increasing_cl:
    3.20 +  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
    3.21 +  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
    3.22 +proof
    3.23 +  show "f ----> (SUP n. f n)"
    3.24 +    using assms
    3.25 +    by (intro increasing_tendsto)
    3.26 +       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
    3.27 +qed
    3.28 +
    3.29 +lemma lim_decreasing_cl:
    3.30 +  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
    3.31 +  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
    3.32 +proof
    3.33 +  show "f ----> (INF n. f n)"
    3.34 +    using assms
    3.35 +    by (intro decreasing_tendsto)
    3.36 +       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
    3.37 +qed
    3.38 +
    3.39 +lemma compact_complete_linorder:
    3.40 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
    3.41 +  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
    3.42 +proof -
    3.43 +  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
    3.44 +    using seq_monosub[of X]
    3.45 +    unfolding comp_def
    3.46 +    by auto
    3.47 +  then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
    3.48 +    by (auto simp add: monoseq_def)
    3.49 +  then obtain l where "(X \<circ> r) ----> l"
    3.50 +     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
    3.51 +     by auto
    3.52 +  then show ?thesis
    3.53 +    using \<open>subseq r\<close> by auto
    3.54 +qed
    3.55  
    3.56  end
     4.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Dec 20 13:56:02 2015 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Dec 17 16:43:36 2015 +0100
     4.3 @@ -3391,6 +3391,60 @@
     4.4    ultimately show ?thesis by auto
     4.5  qed
     4.6  
     4.7 +lemma continuous_ge_on_Ioo:
     4.8 +  assumes "continuous_on {c..d} g" "\<And>x. x \<in> {c<..<d} \<Longrightarrow> g x \<ge> a" "c < d" "x \<in> {c..d}"
     4.9 +  shows "g (x::real) \<ge> (a::real)"
    4.10 +proof-
    4.11 +  from assms(3) have "{c..d} = closure {c<..<d}" by (rule closure_greaterThanLessThan[symmetric])
    4.12 +  also from assms(2) have "{c<..<d} \<subseteq> (g -` {a..} \<inter> {c..d})" by auto
    4.13 +  hence "closure {c<..<d} \<subseteq> closure (g -` {a..} \<inter> {c..d})" by (rule closure_mono)
    4.14 +  also from assms(1) have "closed (g -` {a..} \<inter> {c..d})"
    4.15 +    by (auto simp: continuous_on_closed_vimage)
    4.16 +  hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp
    4.17 +  finally show ?thesis using \<open>x \<in> {c..d}\<close> by auto 
    4.18 +qed 
    4.19 +
    4.20 +lemma interior_real_semiline':
    4.21 +  fixes a :: real
    4.22 +  shows "interior {..a} = {..<a}"
    4.23 +proof -
    4.24 +  {
    4.25 +    fix y
    4.26 +    assume "a > y"
    4.27 +    then have "y \<in> interior {..a}"
    4.28 +      apply (simp add: mem_interior)
    4.29 +      apply (rule_tac x="(a-y)" in exI)
    4.30 +      apply (auto simp add: dist_norm)
    4.31 +      done
    4.32 +  }
    4.33 +  moreover
    4.34 +  {
    4.35 +    fix y
    4.36 +    assume "y \<in> interior {..a}"
    4.37 +    then obtain e where e: "e > 0" "cball y e \<subseteq> {..a}"
    4.38 +      using mem_interior_cball[of y "{..a}"] by auto
    4.39 +    moreover from e have "y + e \<in> cball y e"
    4.40 +      by (auto simp add: cball_def dist_norm)
    4.41 +    ultimately have "a \<ge> y + e" by auto
    4.42 +    then have "a > y" using e by auto
    4.43 +  }
    4.44 +  ultimately show ?thesis by auto
    4.45 +qed
    4.46 +
    4.47 +lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
    4.48 +proof-
    4.49 +  have "{a..b} = {a..} \<inter> {..b}" by auto
    4.50 +  also have "interior ... = {a<..} \<inter> {..<b}" 
    4.51 +    by (simp add: interior_real_semiline interior_real_semiline')
    4.52 +  also have "... = {a<..<b}" by auto
    4.53 +  finally show ?thesis .
    4.54 +qed
    4.55 +
    4.56 +lemma frontier_real_Iic:
    4.57 +  fixes a :: real
    4.58 +  shows "frontier {..a} = {a}"
    4.59 +  unfolding frontier_def by (auto simp add: interior_real_semiline')
    4.60 +
    4.61  lemma rel_interior_real_box:
    4.62    fixes a b :: real
    4.63    assumes "a < b"
     5.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Dec 20 13:56:02 2015 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Dec 17 16:43:36 2015 +0100
     5.3 @@ -2451,6 +2451,20 @@
     5.4    unfolding has_vector_derivative_def
     5.5    by (rule has_derivative_at_within)
     5.6  
     5.7 +lemma has_vector_derivative_weaken:
     5.8 +  fixes x D and f g s t
     5.9 +  assumes f: "(f has_vector_derivative D) (at x within t)"
    5.10 +    and "x \<in> s" "s \<subseteq> t" 
    5.11 +    and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
    5.12 +  shows "(g has_vector_derivative D) (at x within s)"
    5.13 +proof -
    5.14 +  have "(f has_vector_derivative D) (at x within s) \<longleftrightarrow> (g has_vector_derivative D) (at x within s)"
    5.15 +    unfolding has_vector_derivative_def has_derivative_iff_norm
    5.16 +    using assms by (intro conj_cong Lim_cong_within refl) auto
    5.17 +  then show ?thesis
    5.18 +    using has_vector_derivative_within_subset[OF f `s \<subseteq> t`] by simp
    5.19 +qed
    5.20 +
    5.21  lemma has_vector_derivative_transform_within:
    5.22    assumes "0 < d"
    5.23      and "x \<in> s"
     6.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Dec 20 13:56:02 2015 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Dec 17 16:43:36 2015 +0100
     6.3 @@ -8,11 +8,12 @@
     6.4  
     6.5  theory Topology_Euclidean_Space
     6.6  imports
     6.7 -  Complex_Main
     6.8 +  "~~/src/HOL/Library/Indicator_Function"
     6.9    "~~/src/HOL/Library/Countable_Set"
    6.10    "~~/src/HOL/Library/FuncSet"
    6.11    Linear_Algebra
    6.12    Norm_Arith
    6.13 +  
    6.14  begin
    6.15  
    6.16  lemma image_affinity_interval:
    6.17 @@ -5736,6 +5737,60 @@
    6.18      done
    6.19  qed
    6.20  
    6.21 +lemma isCont_indicator: 
    6.22 +  fixes x :: "'a::t2_space"
    6.23 +  shows "isCont (indicator A :: 'a \<Rightarrow> real) x = (x \<notin> frontier A)"
    6.24 +proof auto
    6.25 +  fix x
    6.26 +  assume cts_at: "isCont (indicator A :: 'a \<Rightarrow> real) x" and fr: "x \<in> frontier A"
    6.27 +  with continuous_at_open have 1: "\<forall>V::real set. open V \<and> indicator A x \<in> V \<longrightarrow>
    6.28 +    (\<exists>U::'a set. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> V))" by auto
    6.29 +  show False
    6.30 +  proof (cases "x \<in> A")
    6.31 +    assume x: "x \<in> A"
    6.32 +    hence "indicator A x \<in> ({0<..<2} :: real set)" by simp
    6.33 +    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set))"
    6.34 +      using 1 open_greaterThanLessThan by blast
    6.35 +    then guess U .. note U = this
    6.36 +    hence "\<forall>y\<in>U. indicator A y > (0::real)"
    6.37 +      unfolding greaterThanLessThan_def by auto
    6.38 +    hence "U \<subseteq> A" using indicator_eq_0_iff by force
    6.39 +    hence "x \<in> interior A" using U interiorI by auto
    6.40 +    thus ?thesis using fr unfolding frontier_def by simp
    6.41 +  next
    6.42 +    assume x: "x \<notin> A"
    6.43 +    hence "indicator A x \<in> ({-1<..<1} :: real set)" by simp
    6.44 +    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set))"
    6.45 +      using 1 open_greaterThanLessThan by blast
    6.46 +    then guess U .. note U = this
    6.47 +    hence "\<forall>y\<in>U. indicator A y < (1::real)"
    6.48 +      unfolding greaterThanLessThan_def by auto
    6.49 +    hence "U \<subseteq> -A" by auto
    6.50 +    hence "x \<in> interior (-A)" using U interiorI by auto
    6.51 +    thus ?thesis using fr interior_complement unfolding frontier_def by auto
    6.52 +  qed
    6.53 +next
    6.54 +  assume nfr: "x \<notin> frontier A"
    6.55 +  hence "x \<in> interior A \<or> x \<in> interior (-A)"
    6.56 +    by (auto simp: frontier_def closure_interior)
    6.57 +  thus "isCont ((indicator A)::'a \<Rightarrow> real) x"
    6.58 +  proof
    6.59 +    assume int: "x \<in> interior A"
    6.60 +    hence "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> A" unfolding interior_def by auto
    6.61 +    then guess U .. note U = this
    6.62 +    hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto
    6.63 +    hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff)
    6.64 +    thus ?thesis using U continuous_on_eq_continuous_at by auto
    6.65 +  next
    6.66 +    assume ext: "x \<in> interior (-A)"
    6.67 +    hence "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> -A" unfolding interior_def by auto
    6.68 +    then guess U .. note U = this
    6.69 +    hence "\<forall>y\<in>U. indicator A y = (0::real)" unfolding indicator_def by auto
    6.70 +    hence "continuous_on U (indicator A)" by (smt U continuous_on_topological indicator_def)
    6.71 +    thus ?thesis using U continuous_on_eq_continuous_at by auto
    6.72 +  qed
    6.73 +qed
    6.74 +
    6.75  text \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
    6.76  
    6.77  lemma continuous_within_avoid:
     7.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Sun Dec 20 13:56:02 2015 +0100
     7.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Thu Dec 17 16:43:36 2015 +0100
     7.3 @@ -904,6 +904,12 @@
     7.4  translations
     7.5    "\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
     7.6  
     7.7 +syntax
     7.8 +  "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" ("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
     7.9 +
    7.10 +translations
    7.11 +  "LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
    7.12 +
    7.13  lemma has_bochner_integral_integral_eq: "has_bochner_integral M f x \<Longrightarrow> integral\<^sup>L M f = x"
    7.14    by (metis the_equality has_bochner_integral_eq lebesgue_integral_def)
    7.15  
    7.16 @@ -2581,6 +2587,33 @@
    7.17      by (simp add: integral_distr[symmetric, OF measurable_pair_swap' f] distr_pair_swap[symmetric])
    7.18  qed
    7.19  
    7.20 +lemma (in pair_sigma_finite) Fubini_integrable:
    7.21 +  fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
    7.22 +  assumes f[measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
    7.23 +    and integ1: "integrable M1 (\<lambda>x. \<integral> y. norm (f (x, y)) \<partial>M2)"
    7.24 +    and integ2: "AE x in M1. integrable M2 (\<lambda>y. f (x, y))"
    7.25 +  shows "integrable (M1 \<Otimes>\<^sub>M M2) f"
    7.26 +proof (rule integrableI_bounded)
    7.27 +  have "(\<integral>\<^sup>+ p. norm (f p) \<partial>(M1 \<Otimes>\<^sub>M M2)) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. norm (f (x, y)) \<partial>M2) \<partial>M1)"
    7.28 +    by (simp add: M2.nn_integral_fst [symmetric])
    7.29 +  also have "\<dots> = (\<integral>\<^sup>+ x. \<bar>\<integral>y. norm (f (x, y)) \<partial>M2\<bar> \<partial>M1)"
    7.30 +    apply (intro nn_integral_cong_AE)
    7.31 +    using integ2
    7.32 +  proof eventually_elim
    7.33 +    fix x assume "integrable M2 (\<lambda>y. f (x, y))"
    7.34 +    then have f: "integrable M2 (\<lambda>y. norm (f (x, y)))"
    7.35 +      by simp
    7.36 +    then have "(\<integral>\<^sup>+y. ereal (norm (f (x, y))) \<partial>M2) = ereal (LINT y|M2. norm (f (x, y)))"
    7.37 +      by (rule nn_integral_eq_integral) simp
    7.38 +    also have "\<dots> = ereal \<bar>LINT y|M2. norm (f (x, y))\<bar>"
    7.39 +      using f by (auto intro!: abs_of_nonneg[symmetric] integral_nonneg_AE)
    7.40 +    finally show "(\<integral>\<^sup>+y. ereal (norm (f (x, y))) \<partial>M2) = ereal \<bar>LINT y|M2. norm (f (x, y))\<bar>" .
    7.41 +  qed
    7.42 +  also have "\<dots> < \<infinity>"
    7.43 +    using integ1 by (simp add: integrable_iff_bounded integral_nonneg_AE)
    7.44 +  finally show "(\<integral>\<^sup>+ p. norm (f p) \<partial>(M1 \<Otimes>\<^sub>M M2)) < \<infinity>" .
    7.45 +qed fact
    7.46 +
    7.47  lemma (in pair_sigma_finite) emeasure_pair_measure_finite:
    7.48    assumes A: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" and finite: "emeasure (M1 \<Otimes>\<^sub>M M2) A < \<infinity>"
    7.49    shows "AE x in M1. emeasure M2 {y\<in>space M2. (x, y) \<in> A} < \<infinity>"
     8.1 --- a/src/HOL/Probability/Borel_Space.thy	Sun Dec 20 13:56:02 2015 +0100
     8.2 +++ b/src/HOL/Probability/Borel_Space.thy	Thu Dec 17 16:43:36 2015 +0100
     8.3 @@ -1467,6 +1467,35 @@
     8.4      by simp
     8.5  qed
     8.6  
     8.7 +lemma is_real_interval:
     8.8 +  assumes S: "is_interval S"
     8.9 +  shows "\<exists>a b::real. S = {} \<or> S = UNIV \<or> S = {..<b} \<or> S = {..b} \<or> S = {a<..} \<or> S = {a..} \<or>
    8.10 +    S = {a<..<b} \<or> S = {a<..b} \<or> S = {a..<b} \<or> S = {a..b}"
    8.11 +  using S unfolding is_interval_1 by (blast intro: interval_cases)
    8.12 +
    8.13 +lemma real_interval_borel_measurable:
    8.14 +  assumes "is_interval (S::real set)"
    8.15 +  shows "S \<in> sets borel"
    8.16 +proof -
    8.17 +  from assms is_real_interval have "\<exists>a b::real. S = {} \<or> S = UNIV \<or> S = {..<b} \<or> S = {..b} \<or>
    8.18 +    S = {a<..} \<or> S = {a..} \<or> S = {a<..<b} \<or> S = {a<..b} \<or> S = {a..<b} \<or> S = {a..b}" by auto
    8.19 +  then guess a ..
    8.20 +  then guess b ..
    8.21 +  thus ?thesis
    8.22 +    by auto
    8.23 +qed
    8.24 +
    8.25 +lemma borel_measurable_mono:
    8.26 +  fixes f :: "real \<Rightarrow> real"
    8.27 +  assumes "mono f"
    8.28 +  shows "f \<in> borel_measurable borel"
    8.29 +proof (subst borel_measurable_iff_ge, auto simp add:)
    8.30 +  fix a :: real
    8.31 +  have "is_interval {w. a \<le> f w}"
    8.32 +    unfolding is_interval_1 using assms by (auto dest: monoD intro: order.trans)
    8.33 +  thus "{w. a \<le> f w} \<in> sets borel" using real_interval_borel_measurable by auto  
    8.34 +qed
    8.35 +
    8.36  no_notation
    8.37    eucl_less (infix "<e" 50)
    8.38  
     9.1 --- a/src/HOL/Probability/Giry_Monad.thy	Sun Dec 20 13:56:02 2015 +0100
     9.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Thu Dec 17 16:43:36 2015 +0100
     9.3 @@ -91,9 +91,9 @@
     9.4    from mono have inj: "inj_on g {a..b}" by (rule strict_mono_on_imp_inj_on)
     9.5    from mono have mono': "mono_on g {a..b}" by (rule strict_mono_on_imp_mono_on)
     9.6    from mono' derivg have "\<And>x. x \<in> {a<..<b} \<Longrightarrow> g' x \<ge> 0"
     9.7 -    by (rule mono_on_imp_deriv_nonneg) (auto simp: interior_atLeastAtMost_real)
     9.8 +    by (rule mono_on_imp_deriv_nonneg) auto
     9.9    from contg' this have derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
    9.10 -    by (rule continuous_ge_on_Iii) (simp_all add: \<open>a < b\<close>)
    9.11 +    by (rule continuous_ge_on_Ioo) (simp_all add: \<open>a < b\<close>)
    9.12  
    9.13    from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
    9.14    have A: "h -` {a..b} = {g a..g b}"
    10.1 --- a/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Sun Dec 20 13:56:02 2015 +0100
    10.2 +++ b/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Thu Dec 17 16:43:36 2015 +0100
    10.3 @@ -16,65 +16,6 @@
    10.4      "\<lbrakk>f \<in> measurable borel M; A \<in> sets M\<rbrakk> \<Longrightarrow> f -` A \<in> sets borel"
    10.5    by (drule (1) measurable_sets) simp
    10.6  
    10.7 -lemma closure_Iii: 
    10.8 -  assumes "a < b"
    10.9 -  shows "closure {a<..<b::real} = {a..b}"
   10.10 -proof-
   10.11 -  have "{a<..<b} = ball ((a+b)/2) ((b-a)/2)" by (auto simp: dist_real_def field_simps not_less)
   10.12 -  also from assms have "closure ... = cball ((a+b)/2) ((b-a)/2)" by (intro closure_ball) simp
   10.13 -  also have "... = {a..b}" by (auto simp: dist_real_def field_simps not_less)
   10.14 -  finally show ?thesis .
   10.15 -qed
   10.16 -
   10.17 -lemma continuous_ge_on_Iii:
   10.18 -  assumes "continuous_on {c..d} g" "\<And>x. x \<in> {c<..<d} \<Longrightarrow> g x \<ge> a" "c < d" "x \<in> {c..d}"
   10.19 -  shows "g (x::real) \<ge> (a::real)"
   10.20 -proof-
   10.21 -  from assms(3) have "{c..d} = closure {c<..<d}" by (rule closure_Iii[symmetric])
   10.22 -  also from assms(2) have "{c<..<d} \<subseteq> (g -` {a..} \<inter> {c..d})" by auto
   10.23 -  hence "closure {c<..<d} \<subseteq> closure (g -` {a..} \<inter> {c..d})" by (rule closure_mono)
   10.24 -  also from assms(1) have "closed (g -` {a..} \<inter> {c..d})"
   10.25 -    by (auto simp: continuous_on_closed_vimage)
   10.26 -  hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp
   10.27 -  finally show ?thesis using \<open>x \<in> {c..d}\<close> by auto 
   10.28 -qed 
   10.29 -
   10.30 -lemma interior_real_semiline':
   10.31 -  fixes a :: real
   10.32 -  shows "interior {..a} = {..<a}"
   10.33 -proof -
   10.34 -  {
   10.35 -    fix y
   10.36 -    assume "a > y"
   10.37 -    then have "y \<in> interior {..a}"
   10.38 -      apply (simp add: mem_interior)
   10.39 -      apply (rule_tac x="(a-y)" in exI)
   10.40 -      apply (auto simp add: dist_norm)
   10.41 -      done
   10.42 -  }
   10.43 -  moreover
   10.44 -  {
   10.45 -    fix y
   10.46 -    assume "y \<in> interior {..a}"
   10.47 -    then obtain e where e: "e > 0" "cball y e \<subseteq> {..a}"
   10.48 -      using mem_interior_cball[of y "{..a}"] by auto
   10.49 -    moreover from e have "y + e \<in> cball y e"
   10.50 -      by (auto simp add: cball_def dist_norm)
   10.51 -    ultimately have "a \<ge> y + e" by auto
   10.52 -    then have "a > y" using e by auto
   10.53 -  }
   10.54 -  ultimately show ?thesis by auto
   10.55 -qed
   10.56 -
   10.57 -lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
   10.58 -proof-
   10.59 -  have "{a..b} = {a..} \<inter> {..b}" by auto
   10.60 -  also have "interior ... = {a<..} \<inter> {..<b}" 
   10.61 -    by (simp add: interior_real_semiline interior_real_semiline')
   10.62 -  also have "... = {a<..<b}" by auto
   10.63 -  finally show ?thesis .
   10.64 -qed
   10.65 -
   10.66  lemma nn_integral_indicator_singleton[simp]:
   10.67    assumes [measurable]: "{y} \<in> sets M"
   10.68    shows "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = max 0 (f y) * emeasure M {y}"
    11.1 --- a/src/HOL/Probability/Measure_Space.thy	Sun Dec 20 13:56:02 2015 +0100
    11.2 +++ b/src/HOL/Probability/Measure_Space.thy	Thu Dec 17 16:43:36 2015 +0100
    11.3 @@ -1410,6 +1410,9 @@
    11.4  lemma measure_nonneg: "0 \<le> measure M A"
    11.5    using emeasure_nonneg[of M A] unfolding measure_def by (auto intro: real_of_ereal_pos)
    11.6  
    11.7 +lemma zero_less_measure_iff: "0 < measure M A \<longleftrightarrow> measure M A \<noteq> 0"
    11.8 +  using measure_nonneg[of M A] by (auto simp add: le_less)
    11.9 +
   11.10  lemma measure_le_0_iff: "measure M X \<le> 0 \<longleftrightarrow> measure M X = 0"
   11.11    using measure_nonneg[of M X] by auto
   11.12  
    12.1 --- a/src/HOL/Probability/Set_Integral.thy	Sun Dec 20 13:56:02 2015 +0100
    12.2 +++ b/src/HOL/Probability/Set_Integral.thy	Thu Dec 17 16:43:36 2015 +0100
    12.3 @@ -14,13 +14,6 @@
    12.4      Notation
    12.5  *)
    12.6  
    12.7 -syntax
    12.8 -"_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
    12.9 -("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
   12.10 -
   12.11 -translations
   12.12 -"LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
   12.13 -
   12.14  abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
   12.15  
   12.16  abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"