13 begin |
13 begin |
14 |
14 |
15 lemma measurable_sets_borel: |
15 lemma measurable_sets_borel: |
16 "\<lbrakk>f \<in> measurable borel M; A \<in> sets M\<rbrakk> \<Longrightarrow> f -` A \<in> sets borel" |
16 "\<lbrakk>f \<in> measurable borel M; A \<in> sets M\<rbrakk> \<Longrightarrow> f -` A \<in> sets borel" |
17 by (drule (1) measurable_sets) simp |
17 by (drule (1) measurable_sets) simp |
18 |
|
19 lemma closure_Iii: |
|
20 assumes "a < b" |
|
21 shows "closure {a<..<b::real} = {a..b}" |
|
22 proof- |
|
23 have "{a<..<b} = ball ((a+b)/2) ((b-a)/2)" by (auto simp: dist_real_def field_simps not_less) |
|
24 also from assms have "closure ... = cball ((a+b)/2) ((b-a)/2)" by (intro closure_ball) simp |
|
25 also have "... = {a..b}" by (auto simp: dist_real_def field_simps not_less) |
|
26 finally show ?thesis . |
|
27 qed |
|
28 |
|
29 lemma continuous_ge_on_Iii: |
|
30 assumes "continuous_on {c..d} g" "\<And>x. x \<in> {c<..<d} \<Longrightarrow> g x \<ge> a" "c < d" "x \<in> {c..d}" |
|
31 shows "g (x::real) \<ge> (a::real)" |
|
32 proof- |
|
33 from assms(3) have "{c..d} = closure {c<..<d}" by (rule closure_Iii[symmetric]) |
|
34 also from assms(2) have "{c<..<d} \<subseteq> (g -` {a..} \<inter> {c..d})" by auto |
|
35 hence "closure {c<..<d} \<subseteq> closure (g -` {a..} \<inter> {c..d})" by (rule closure_mono) |
|
36 also from assms(1) have "closed (g -` {a..} \<inter> {c..d})" |
|
37 by (auto simp: continuous_on_closed_vimage) |
|
38 hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp |
|
39 finally show ?thesis using \<open>x \<in> {c..d}\<close> by auto |
|
40 qed |
|
41 |
|
42 lemma interior_real_semiline': |
|
43 fixes a :: real |
|
44 shows "interior {..a} = {..<a}" |
|
45 proof - |
|
46 { |
|
47 fix y |
|
48 assume "a > y" |
|
49 then have "y \<in> interior {..a}" |
|
50 apply (simp add: mem_interior) |
|
51 apply (rule_tac x="(a-y)" in exI) |
|
52 apply (auto simp add: dist_norm) |
|
53 done |
|
54 } |
|
55 moreover |
|
56 { |
|
57 fix y |
|
58 assume "y \<in> interior {..a}" |
|
59 then obtain e where e: "e > 0" "cball y e \<subseteq> {..a}" |
|
60 using mem_interior_cball[of y "{..a}"] by auto |
|
61 moreover from e have "y + e \<in> cball y e" |
|
62 by (auto simp add: cball_def dist_norm) |
|
63 ultimately have "a \<ge> y + e" by auto |
|
64 then have "a > y" using e by auto |
|
65 } |
|
66 ultimately show ?thesis by auto |
|
67 qed |
|
68 |
|
69 lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}" |
|
70 proof- |
|
71 have "{a..b} = {a..} \<inter> {..b}" by auto |
|
72 also have "interior ... = {a<..} \<inter> {..<b}" |
|
73 by (simp add: interior_real_semiline interior_real_semiline') |
|
74 also have "... = {a<..<b}" by auto |
|
75 finally show ?thesis . |
|
76 qed |
|
77 |
18 |
78 lemma nn_integral_indicator_singleton[simp]: |
19 lemma nn_integral_indicator_singleton[simp]: |
79 assumes [measurable]: "{y} \<in> sets M" |
20 assumes [measurable]: "{y} \<in> sets M" |
80 shows "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = max 0 (f y) * emeasure M {y}" |
21 shows "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = max 0 (f y) * emeasure M {y}" |
81 proof- |
22 proof- |