# HG changeset patch
# User hoelzl
# Date 1450367016 -3600
# Node ID ff4d33058566de5dbb933ca24f22a245e37d39af
# Parent  e4f9d8f094fe9248147481d063cc07dc04e5905a
moved some theorems from the CLT proof; reordered some theorems / notation

diff -r e4f9d8f094fe -r ff4d33058566 src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/HOL/Library/ContNotDenum.thy	Thu Dec 17 16:43:36 2015 +0100
@@ -143,4 +143,20 @@
   using uncountable_open_interval [of a b]
   by (metis countable_Un_iff ivl_disj_un_singleton(4))
 
+lemma real_interval_avoid_countable_set:
+  fixes a b :: real and A :: "real set"
+  assumes "a < b" and "countable A"
+  shows "\<exists>x\<in>{a<..<b}. x \<notin> A"
+proof -
+  from `countable A` have "countable (A \<inter> {a<..<b})" by auto
+  moreover with `a < b` have "\<not> countable {a<..<b}" 
+    by (simp add: uncountable_open_interval)
+  ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}" by auto
+  hence "A \<inter> {a<..<b} \<subset> {a<..<b}" 
+    by (intro psubsetI, auto)
+  hence "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}"
+    by (rule psubset_imp_ex_mem)
+  thus ?thesis by auto
+qed
+
 end
diff -r e4f9d8f094fe -r ff4d33058566 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Dec 17 16:43:36 2015 +0100
@@ -2450,6 +2450,16 @@
 lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
   by (auto dest!: lim_real_of_ereal)
 
+lemma convergent_real_imp_convergent_ereal:
+  assumes "convergent a"
+  shows "convergent (\<lambda>n. ereal (a n))" and "lim (\<lambda>n. ereal (a n)) = ereal (lim a)"
+proof -
+  from assms obtain L where L: "a ----> L" unfolding convergent_def ..
+  hence lim: "(\<lambda>n. ereal (a n)) ----> ereal L" using lim_ereal by auto
+  thus "convergent (\<lambda>n. ereal (a n))" unfolding convergent_def ..
+  thus "lim (\<lambda>n. ereal (a n)) = ereal (lim a)" using lim L limI by metis
+qed
+
 lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
 proof -
   {
@@ -3223,7 +3233,6 @@
   thus "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>" by simp_all
 qed
 
-
 lemma SUP_ereal_add_directed:
   fixes f g :: "'a \<Rightarrow> ereal"
   assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
@@ -3293,50 +3302,6 @@
     done
 qed
 
-subsection \<open>More Limits\<close>
-
-lemma convergent_limsup_cl:
-  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
-  shows "convergent X \<Longrightarrow> limsup X = lim X"
-  by (auto simp: convergent_def limI lim_imp_Limsup)
-
-lemma lim_increasing_cl:
-  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
-  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
-proof
-  show "f ----> (SUP n. f n)"
-    using assms
-    by (intro increasing_tendsto)
-       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
-qed
-
-lemma lim_decreasing_cl:
-  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
-  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
-proof
-  show "f ----> (INF n. f n)"
-    using assms
-    by (intro decreasing_tendsto)
-       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
-qed
-
-lemma compact_complete_linorder:
-  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
-  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
-proof -
-  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
-    using seq_monosub[of X]
-    unfolding comp_def
-    by auto
-  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)"
-    by (auto simp add: monoseq_def)
-  then obtain l where "(X \<circ> r) ----> l"
-     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
-     by auto
-  then show ?thesis
-    using \<open>subseq r\<close> by auto
-qed
-
 lemma ereal_dense3:
   fixes x y :: ereal
   shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
diff -r e4f9d8f094fe -r ff4d33058566 src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Thu Dec 17 16:43:36 2015 +0100
@@ -351,5 +351,53 @@
   finally show ?thesis
     by (auto simp: Liminf_def)
 qed
+subsection \<open>More Limits\<close>
+
+lemma convergent_limsup_cl:
+  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+  shows "convergent X \<Longrightarrow> limsup X = lim X"
+  by (auto simp: convergent_def limI lim_imp_Limsup)
+
+lemma convergent_liminf_cl:
+  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+  shows "convergent X \<Longrightarrow> liminf X = lim X"
+  by (auto simp: convergent_def limI lim_imp_Liminf)
+
+lemma lim_increasing_cl:
+  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
+  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
+proof
+  show "f ----> (SUP n. f n)"
+    using assms
+    by (intro increasing_tendsto)
+       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
+qed
+
+lemma lim_decreasing_cl:
+  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
+  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
+proof
+  show "f ----> (INF n. f n)"
+    using assms
+    by (intro decreasing_tendsto)
+       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
+qed
+
+lemma compact_complete_linorder:
+  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
+proof -
+  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
+    using seq_monosub[of X]
+    unfolding comp_def
+    by auto
+  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)"
+    by (auto simp add: monoseq_def)
+  then obtain l where "(X \<circ> r) ----> l"
+     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
+     by auto
+  then show ?thesis
+    using \<open>subseq r\<close> by auto
+qed
 
 end
diff -r e4f9d8f094fe -r ff4d33058566 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Dec 17 16:43:36 2015 +0100
@@ -3391,6 +3391,60 @@
   ultimately show ?thesis by auto
 qed
 
+lemma continuous_ge_on_Ioo:
+  assumes "continuous_on {c..d} g" "\<And>x. x \<in> {c<..<d} \<Longrightarrow> g x \<ge> a" "c < d" "x \<in> {c..d}"
+  shows "g (x::real) \<ge> (a::real)"
+proof-
+  from assms(3) have "{c..d} = closure {c<..<d}" by (rule closure_greaterThanLessThan[symmetric])
+  also from assms(2) have "{c<..<d} \<subseteq> (g -` {a..} \<inter> {c..d})" by auto
+  hence "closure {c<..<d} \<subseteq> closure (g -` {a..} \<inter> {c..d})" by (rule closure_mono)
+  also from assms(1) have "closed (g -` {a..} \<inter> {c..d})"
+    by (auto simp: continuous_on_closed_vimage)
+  hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp
+  finally show ?thesis using \<open>x \<in> {c..d}\<close> by auto 
+qed 
+
+lemma interior_real_semiline':
+  fixes a :: real
+  shows "interior {..a} = {..<a}"
+proof -
+  {
+    fix y
+    assume "a > y"
+    then have "y \<in> interior {..a}"
+      apply (simp add: mem_interior)
+      apply (rule_tac x="(a-y)" in exI)
+      apply (auto simp add: dist_norm)
+      done
+  }
+  moreover
+  {
+    fix y
+    assume "y \<in> interior {..a}"
+    then obtain e where e: "e > 0" "cball y e \<subseteq> {..a}"
+      using mem_interior_cball[of y "{..a}"] by auto
+    moreover from e have "y + e \<in> cball y e"
+      by (auto simp add: cball_def dist_norm)
+    ultimately have "a \<ge> y + e" by auto
+    then have "a > y" using e by auto
+  }
+  ultimately show ?thesis by auto
+qed
+
+lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
+proof-
+  have "{a..b} = {a..} \<inter> {..b}" by auto
+  also have "interior ... = {a<..} \<inter> {..<b}" 
+    by (simp add: interior_real_semiline interior_real_semiline')
+  also have "... = {a<..<b}" by auto
+  finally show ?thesis .
+qed
+
+lemma frontier_real_Iic:
+  fixes a :: real
+  shows "frontier {..a} = {a}"
+  unfolding frontier_def by (auto simp add: interior_real_semiline')
+
 lemma rel_interior_real_box:
   fixes a b :: real
   assumes "a < b"
diff -r e4f9d8f094fe -r ff4d33058566 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Dec 17 16:43:36 2015 +0100
@@ -2451,6 +2451,20 @@
   unfolding has_vector_derivative_def
   by (rule has_derivative_at_within)
 
+lemma has_vector_derivative_weaken:
+  fixes x D and f g s t
+  assumes f: "(f has_vector_derivative D) (at x within t)"
+    and "x \<in> s" "s \<subseteq> t" 
+    and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
+  shows "(g has_vector_derivative D) (at x within s)"
+proof -
+  have "(f has_vector_derivative D) (at x within s) \<longleftrightarrow> (g has_vector_derivative D) (at x within s)"
+    unfolding has_vector_derivative_def has_derivative_iff_norm
+    using assms by (intro conj_cong Lim_cong_within refl) auto
+  then show ?thesis
+    using has_vector_derivative_within_subset[OF f `s \<subseteq> t`] by simp
+qed
+
 lemma has_vector_derivative_transform_within:
   assumes "0 < d"
     and "x \<in> s"
diff -r e4f9d8f094fe -r ff4d33058566 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Dec 17 16:43:36 2015 +0100
@@ -8,11 +8,12 @@
 
 theory Topology_Euclidean_Space
 imports
-  Complex_Main
+  "~~/src/HOL/Library/Indicator_Function"
   "~~/src/HOL/Library/Countable_Set"
   "~~/src/HOL/Library/FuncSet"
   Linear_Algebra
   Norm_Arith
+  
 begin
 
 lemma image_affinity_interval:
@@ -5736,6 +5737,60 @@
     done
 qed
 
+lemma isCont_indicator: 
+  fixes x :: "'a::t2_space"
+  shows "isCont (indicator A :: 'a \<Rightarrow> real) x = (x \<notin> frontier A)"
+proof auto
+  fix x
+  assume cts_at: "isCont (indicator A :: 'a \<Rightarrow> real) x" and fr: "x \<in> frontier A"
+  with continuous_at_open have 1: "\<forall>V::real set. open V \<and> indicator A x \<in> V \<longrightarrow>
+    (\<exists>U::'a set. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> V))" by auto
+  show False
+  proof (cases "x \<in> A")
+    assume x: "x \<in> A"
+    hence "indicator A x \<in> ({0<..<2} :: real set)" by simp
+    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set))"
+      using 1 open_greaterThanLessThan by blast
+    then guess U .. note U = this
+    hence "\<forall>y\<in>U. indicator A y > (0::real)"
+      unfolding greaterThanLessThan_def by auto
+    hence "U \<subseteq> A" using indicator_eq_0_iff by force
+    hence "x \<in> interior A" using U interiorI by auto
+    thus ?thesis using fr unfolding frontier_def by simp
+  next
+    assume x: "x \<notin> A"
+    hence "indicator A x \<in> ({-1<..<1} :: real set)" by simp
+    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set))"
+      using 1 open_greaterThanLessThan by blast
+    then guess U .. note U = this
+    hence "\<forall>y\<in>U. indicator A y < (1::real)"
+      unfolding greaterThanLessThan_def by auto
+    hence "U \<subseteq> -A" by auto
+    hence "x \<in> interior (-A)" using U interiorI by auto
+    thus ?thesis using fr interior_complement unfolding frontier_def by auto
+  qed
+next
+  assume nfr: "x \<notin> frontier A"
+  hence "x \<in> interior A \<or> x \<in> interior (-A)"
+    by (auto simp: frontier_def closure_interior)
+  thus "isCont ((indicator A)::'a \<Rightarrow> real) x"
+  proof
+    assume int: "x \<in> interior A"
+    hence "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> A" unfolding interior_def by auto
+    then guess U .. note U = this
+    hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto
+    hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff)
+    thus ?thesis using U continuous_on_eq_continuous_at by auto
+  next
+    assume ext: "x \<in> interior (-A)"
+    hence "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> -A" unfolding interior_def by auto
+    then guess U .. note U = this
+    hence "\<forall>y\<in>U. indicator A y = (0::real)" unfolding indicator_def by auto
+    hence "continuous_on U (indicator A)" by (smt U continuous_on_topological indicator_def)
+    thus ?thesis using U continuous_on_eq_continuous_at by auto
+  qed
+qed
+
 text \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
 
 lemma continuous_within_avoid:
diff -r e4f9d8f094fe -r ff4d33058566 src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy	Thu Dec 17 16:43:36 2015 +0100
@@ -904,6 +904,12 @@
 translations
   "\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
 
+syntax
+  "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" ("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
+
+translations
+  "LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
+
 lemma has_bochner_integral_integral_eq: "has_bochner_integral M f x \<Longrightarrow> integral\<^sup>L M f = x"
   by (metis the_equality has_bochner_integral_eq lebesgue_integral_def)
 
@@ -2581,6 +2587,33 @@
     by (simp add: integral_distr[symmetric, OF measurable_pair_swap' f] distr_pair_swap[symmetric])
 qed
 
+lemma (in pair_sigma_finite) Fubini_integrable:
+  fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
+  assumes f[measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
+    and integ1: "integrable M1 (\<lambda>x. \<integral> y. norm (f (x, y)) \<partial>M2)"
+    and integ2: "AE x in M1. integrable M2 (\<lambda>y. f (x, y))"
+  shows "integrable (M1 \<Otimes>\<^sub>M M2) f"
+proof (rule integrableI_bounded)
+  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)"
+    by (simp add: M2.nn_integral_fst [symmetric])
+  also have "\<dots> = (\<integral>\<^sup>+ x. \<bar>\<integral>y. norm (f (x, y)) \<partial>M2\<bar> \<partial>M1)"
+    apply (intro nn_integral_cong_AE)
+    using integ2
+  proof eventually_elim
+    fix x assume "integrable M2 (\<lambda>y. f (x, y))"
+    then have f: "integrable M2 (\<lambda>y. norm (f (x, y)))"
+      by simp
+    then have "(\<integral>\<^sup>+y. ereal (norm (f (x, y))) \<partial>M2) = ereal (LINT y|M2. norm (f (x, y)))"
+      by (rule nn_integral_eq_integral) simp
+    also have "\<dots> = ereal \<bar>LINT y|M2. norm (f (x, y))\<bar>"
+      using f by (auto intro!: abs_of_nonneg[symmetric] integral_nonneg_AE)
+    finally show "(\<integral>\<^sup>+y. ereal (norm (f (x, y))) \<partial>M2) = ereal \<bar>LINT y|M2. norm (f (x, y))\<bar>" .
+  qed
+  also have "\<dots> < \<infinity>"
+    using integ1 by (simp add: integrable_iff_bounded integral_nonneg_AE)
+  finally show "(\<integral>\<^sup>+ p. norm (f p) \<partial>(M1 \<Otimes>\<^sub>M M2)) < \<infinity>" .
+qed fact
+
 lemma (in pair_sigma_finite) emeasure_pair_measure_finite:
   assumes A: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" and finite: "emeasure (M1 \<Otimes>\<^sub>M M2) A < \<infinity>"
   shows "AE x in M1. emeasure M2 {y\<in>space M2. (x, y) \<in> A} < \<infinity>"
diff -r e4f9d8f094fe -r ff4d33058566 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Thu Dec 17 16:43:36 2015 +0100
@@ -1467,6 +1467,35 @@
     by simp
 qed
 
+lemma is_real_interval:
+  assumes S: "is_interval S"
+  shows "\<exists>a b::real. S = {} \<or> S = UNIV \<or> S = {..<b} \<or> S = {..b} \<or> S = {a<..} \<or> S = {a..} \<or>
+    S = {a<..<b} \<or> S = {a<..b} \<or> S = {a..<b} \<or> S = {a..b}"
+  using S unfolding is_interval_1 by (blast intro: interval_cases)
+
+lemma real_interval_borel_measurable:
+  assumes "is_interval (S::real set)"
+  shows "S \<in> sets borel"
+proof -
+  from assms is_real_interval have "\<exists>a b::real. S = {} \<or> S = UNIV \<or> S = {..<b} \<or> S = {..b} \<or>
+    S = {a<..} \<or> S = {a..} \<or> S = {a<..<b} \<or> S = {a<..b} \<or> S = {a..<b} \<or> S = {a..b}" by auto
+  then guess a ..
+  then guess b ..
+  thus ?thesis
+    by auto
+qed
+
+lemma borel_measurable_mono:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "mono f"
+  shows "f \<in> borel_measurable borel"
+proof (subst borel_measurable_iff_ge, auto simp add:)
+  fix a :: real
+  have "is_interval {w. a \<le> f w}"
+    unfolding is_interval_1 using assms by (auto dest: monoD intro: order.trans)
+  thus "{w. a \<le> f w} \<in> sets borel" using real_interval_borel_measurable by auto  
+qed
+
 no_notation
   eucl_less (infix "<e" 50)
 
diff -r e4f9d8f094fe -r ff4d33058566 src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Thu Dec 17 16:43:36 2015 +0100
@@ -91,9 +91,9 @@
   from mono have inj: "inj_on g {a..b}" by (rule strict_mono_on_imp_inj_on)
   from mono have mono': "mono_on g {a..b}" by (rule strict_mono_on_imp_mono_on)
   from mono' derivg have "\<And>x. x \<in> {a<..<b} \<Longrightarrow> g' x \<ge> 0"
-    by (rule mono_on_imp_deriv_nonneg) (auto simp: interior_atLeastAtMost_real)
+    by (rule mono_on_imp_deriv_nonneg) auto
   from contg' this have derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
-    by (rule continuous_ge_on_Iii) (simp_all add: \<open>a < b\<close>)
+    by (rule continuous_ge_on_Ioo) (simp_all add: \<open>a < b\<close>)
 
   from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
   have A: "h -` {a..b} = {g a..g b}"
diff -r e4f9d8f094fe -r ff4d33058566 src/HOL/Probability/Lebesgue_Integral_Substitution.thy
--- a/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Thu Dec 17 16:43:36 2015 +0100
@@ -16,65 +16,6 @@
     "\<lbrakk>f \<in> measurable borel M; A \<in> sets M\<rbrakk> \<Longrightarrow> f -` A \<in> sets borel"
   by (drule (1) measurable_sets) simp
 
-lemma closure_Iii: 
-  assumes "a < b"
-  shows "closure {a<..<b::real} = {a..b}"
-proof-
-  have "{a<..<b} = ball ((a+b)/2) ((b-a)/2)" by (auto simp: dist_real_def field_simps not_less)
-  also from assms have "closure ... = cball ((a+b)/2) ((b-a)/2)" by (intro closure_ball) simp
-  also have "... = {a..b}" by (auto simp: dist_real_def field_simps not_less)
-  finally show ?thesis .
-qed
-
-lemma continuous_ge_on_Iii:
-  assumes "continuous_on {c..d} g" "\<And>x. x \<in> {c<..<d} \<Longrightarrow> g x \<ge> a" "c < d" "x \<in> {c..d}"
-  shows "g (x::real) \<ge> (a::real)"
-proof-
-  from assms(3) have "{c..d} = closure {c<..<d}" by (rule closure_Iii[symmetric])
-  also from assms(2) have "{c<..<d} \<subseteq> (g -` {a..} \<inter> {c..d})" by auto
-  hence "closure {c<..<d} \<subseteq> closure (g -` {a..} \<inter> {c..d})" by (rule closure_mono)
-  also from assms(1) have "closed (g -` {a..} \<inter> {c..d})"
-    by (auto simp: continuous_on_closed_vimage)
-  hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp
-  finally show ?thesis using \<open>x \<in> {c..d}\<close> by auto 
-qed 
-
-lemma interior_real_semiline':
-  fixes a :: real
-  shows "interior {..a} = {..<a}"
-proof -
-  {
-    fix y
-    assume "a > y"
-    then have "y \<in> interior {..a}"
-      apply (simp add: mem_interior)
-      apply (rule_tac x="(a-y)" in exI)
-      apply (auto simp add: dist_norm)
-      done
-  }
-  moreover
-  {
-    fix y
-    assume "y \<in> interior {..a}"
-    then obtain e where e: "e > 0" "cball y e \<subseteq> {..a}"
-      using mem_interior_cball[of y "{..a}"] by auto
-    moreover from e have "y + e \<in> cball y e"
-      by (auto simp add: cball_def dist_norm)
-    ultimately have "a \<ge> y + e" by auto
-    then have "a > y" using e by auto
-  }
-  ultimately show ?thesis by auto
-qed
-
-lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
-proof-
-  have "{a..b} = {a..} \<inter> {..b}" by auto
-  also have "interior ... = {a<..} \<inter> {..<b}" 
-    by (simp add: interior_real_semiline interior_real_semiline')
-  also have "... = {a<..<b}" by auto
-  finally show ?thesis .
-qed
-
 lemma nn_integral_indicator_singleton[simp]:
   assumes [measurable]: "{y} \<in> sets M"
   shows "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = max 0 (f y) * emeasure M {y}"
diff -r e4f9d8f094fe -r ff4d33058566 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Thu Dec 17 16:43:36 2015 +0100
@@ -1410,6 +1410,9 @@
 lemma measure_nonneg: "0 \<le> measure M A"
   using emeasure_nonneg[of M A] unfolding measure_def by (auto intro: real_of_ereal_pos)
 
+lemma zero_less_measure_iff: "0 < measure M A \<longleftrightarrow> measure M A \<noteq> 0"
+  using measure_nonneg[of M A] by (auto simp add: le_less)
+
 lemma measure_le_0_iff: "measure M X \<le> 0 \<longleftrightarrow> measure M X = 0"
   using measure_nonneg[of M X] by auto
 
diff -r e4f9d8f094fe -r ff4d33058566 src/HOL/Probability/Set_Integral.thy
--- a/src/HOL/Probability/Set_Integral.thy	Sun Dec 20 13:56:02 2015 +0100
+++ b/src/HOL/Probability/Set_Integral.thy	Thu Dec 17 16:43:36 2015 +0100
@@ -14,13 +14,6 @@
     Notation
 *)
 
-syntax
-"_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
-
-translations
-"LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
-
 abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
 
 abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"