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