author hoelzl Thu Dec 17 16:43:36 2015 +0100 (2015-12-17) changeset 61880 ff4d33058566 parent 61879 e4f9d8f094fe child 61881 b4bfa62e799d
moved some theorems from the CLT proof; reordered some theorems / notation
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.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.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.24 -
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.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.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.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.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.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.16  lemma image_affinity_interval:
6.17 @@ -5736,6 +5737,60 @@
6.18      done
6.19  qed
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.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.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.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.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.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)
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.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.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.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.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.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.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.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
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.7 -syntax
12.8 -"_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
12.9 -("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
12.11 -translations
12.12 -"LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
12.14  abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
12.16  abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"