--- 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
--- 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"
--- 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
--- 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"
--- 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"
--- 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:
--- 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>"
--- 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)
--- 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}"
--- 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}"
--- 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
--- 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)"