author | paulson <lp15@cam.ac.uk> |
Sun, 15 Apr 2018 21:41:40 +0100 | |
changeset 67986 | b65c4a6a015e |
parent 67984 | adc1a992c470 |
child 67989 | 706f86afff43 |
permissions | -rw-r--r-- |
63627 | 1 |
(* Title: HOL/Analysis/Lebesgue_Measure.thy |
42067 | 2 |
Author: Johannes Hölzl, TU München |
3 |
Author: Robert Himmelmann, TU München |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
4 |
Author: Jeremy Avigad |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
5 |
Author: Luke Serafin |
42067 | 6 |
*) |
7 |
||
61808 | 8 |
section \<open>Lebesgue measure\<close> |
42067 | 9 |
|
38656 | 10 |
theory Lebesgue_Measure |
63968
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
11 |
imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests Regularity |
38656 | 12 |
begin |
13 |
||
64008
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
14 |
lemma measure_eqI_lessThan: |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
15 |
fixes M N :: "real measure" |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
16 |
assumes sets: "sets M = sets borel" "sets N = sets borel" |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
17 |
assumes fin: "\<And>x. emeasure M {x <..} < \<infinity>" |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
18 |
assumes "\<And>x. emeasure M {x <..} = emeasure N {x <..}" |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
19 |
shows "M = N" |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
20 |
proof (rule measure_eqI_generator_eq_countable) |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
21 |
let ?LT = "\<lambda>a::real. {a <..}" let ?E = "range ?LT" |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
22 |
show "Int_stable ?E" |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
23 |
by (auto simp: Int_stable_def lessThan_Int_lessThan) |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
24 |
|
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
25 |
show "?E \<subseteq> Pow UNIV" "sets M = sigma_sets UNIV ?E" "sets N = sigma_sets UNIV ?E" |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
26 |
unfolding sets borel_Ioi by auto |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
27 |
|
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
28 |
show "?LT`Rats \<subseteq> ?E" "(\<Union>i\<in>Rats. ?LT i) = UNIV" "\<And>a. a \<in> ?LT`Rats \<Longrightarrow> emeasure M a \<noteq> \<infinity>" |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
29 |
using fin by (auto intro: Rats_no_bot_less simp: less_top) |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
30 |
qed (auto intro: assms countable_rat) |
17a20ca86d62
HOL-Probability: more about probability, prepare for Markov processes in the AFP
hoelzl
parents:
63968
diff
changeset
|
31 |
|
61808 | 32 |
subsection \<open>Every right continuous and nondecreasing function gives rise to a measure\<close> |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
33 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
34 |
definition interval_measure :: "(real \<Rightarrow> real) \<Rightarrow> real measure" where |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
35 |
"interval_measure F = extend_measure UNIV {(a, b). a \<le> b} (\<lambda>(a, b). {a <.. b}) (\<lambda>(a, b). ennreal (F b - F a))" |
49777 | 36 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
37 |
lemma emeasure_interval_measure_Ioc: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
38 |
assumes "a \<le> b" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
39 |
assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y" |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
40 |
assumes right_cont_F : "\<And>a. continuous (at_right a) F" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
41 |
shows "emeasure (interval_measure F) {a <.. b} = F b - F a" |
61808 | 42 |
proof (rule extend_measure_caratheodory_pair[OF interval_measure_def \<open>a \<le> b\<close>]) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
43 |
show "semiring_of_sets UNIV {{a<..b} |a b :: real. a \<le> b}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
44 |
proof (unfold_locales, safe) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
45 |
fix a b c d :: real assume *: "a \<le> b" "c \<le> d" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
46 |
then show "\<exists>C\<subseteq>{{a<..b} |a b. a \<le> b}. finite C \<and> disjoint C \<and> {a<..b} - {c<..d} = \<Union>C" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
47 |
proof cases |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
48 |
let ?C = "{{a<..b}}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
49 |
assume "b < c \<or> d \<le> a \<or> d \<le> c" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
50 |
with * have "?C \<subseteq> {{a<..b} |a b. a \<le> b} \<and> finite ?C \<and> disjoint ?C \<and> {a<..b} - {c<..d} = \<Union>?C" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
51 |
by (auto simp add: disjoint_def) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
52 |
thus ?thesis .. |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
53 |
next |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
54 |
let ?C = "{{a<..c}, {d<..b}}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
55 |
assume "\<not> (b < c \<or> d \<le> a \<or> d \<le> c)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
56 |
with * have "?C \<subseteq> {{a<..b} |a b. a \<le> b} \<and> finite ?C \<and> disjoint ?C \<and> {a<..b} - {c<..d} = \<Union>?C" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
57 |
by (auto simp add: disjoint_def Ioc_inj) (metis linear)+ |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
58 |
thus ?thesis .. |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
59 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
60 |
qed (auto simp: Ioc_inj, metis linear) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
61 |
next |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
62 |
fix l r :: "nat \<Rightarrow> real" and a b :: real |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
63 |
assume l_r[simp]: "\<And>n. l n \<le> r n" and "a \<le> b" and disj: "disjoint_family (\<lambda>n. {l n<..r n})" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
64 |
assume lr_eq_ab: "(\<Union>i. {l i<..r i}) = {a<..b}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
65 |
|
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61610
diff
changeset
|
66 |
have [intro, simp]: "\<And>a b. a \<le> b \<Longrightarrow> F a \<le> F b" |
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61610
diff
changeset
|
67 |
by (auto intro!: l_r mono_F) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
68 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
69 |
{ fix S :: "nat set" assume "finite S" |
61808 | 70 |
moreover note \<open>a \<le> b\<close> |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
71 |
moreover have "\<And>i. i \<in> S \<Longrightarrow> {l i <.. r i} \<subseteq> {a <.. b}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
72 |
unfolding lr_eq_ab[symmetric] by auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
73 |
ultimately have "(\<Sum>i\<in>S. F (r i) - F (l i)) \<le> F b - F a" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
74 |
proof (induction S arbitrary: a rule: finite_psubset_induct) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
75 |
case (psubset S) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
76 |
show ?case |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
77 |
proof cases |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
78 |
assume "\<exists>i\<in>S. l i < r i" |
61808 | 79 |
with \<open>finite S\<close> have "Min (l ` {i\<in>S. l i < r i}) \<in> l ` {i\<in>S. l i < r i}" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
80 |
by (intro Min_in) auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
81 |
then obtain m where m: "m \<in> S" "l m < r m" "l m = Min (l ` {i\<in>S. l i < r i})" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
82 |
by fastforce |
50104 | 83 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
84 |
have "(\<Sum>i\<in>S. F (r i) - F (l i)) = (F (r m) - F (l m)) + (\<Sum>i\<in>S - {m}. F (r i) - F (l i))" |
64267 | 85 |
using m psubset by (intro sum.remove) auto |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
86 |
also have "(\<Sum>i\<in>S - {m}. F (r i) - F (l i)) \<le> F b - F (r m)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
87 |
proof (intro psubset.IH) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
88 |
show "S - {m} \<subset> S" |
61808 | 89 |
using \<open>m\<in>S\<close> by auto |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
90 |
show "r m \<le> b" |
61808 | 91 |
using psubset.prems(2)[OF \<open>m\<in>S\<close>] \<open>l m < r m\<close> by auto |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
92 |
next |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
93 |
fix i assume "i \<in> S - {m}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
94 |
then have i: "i \<in> S" "i \<noteq> m" by auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
95 |
{ assume i': "l i < r i" "l i < r m" |
63540 | 96 |
with \<open>finite S\<close> i m have "l m \<le> l i" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
97 |
by auto |
63540 | 98 |
with i' have "{l i <.. r i} \<inter> {l m <.. r m} \<noteq> {}" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
99 |
by auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
100 |
then have False |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
101 |
using disjoint_family_onD[OF disj, of i m] i by auto } |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
102 |
then have "l i \<noteq> r i \<Longrightarrow> r m \<le> l i" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
103 |
unfolding not_less[symmetric] using l_r[of i] by auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
104 |
then show "{l i <.. r i} \<subseteq> {r m <.. b}" |
61808 | 105 |
using psubset.prems(2)[OF \<open>i\<in>S\<close>] by auto |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
106 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
107 |
also have "F (r m) - F (l m) \<le> F (r m) - F a" |
61808 | 108 |
using psubset.prems(2)[OF \<open>m \<in> S\<close>] \<open>l m < r m\<close> |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
109 |
by (auto simp add: Ioc_subset_iff intro!: mono_F) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
110 |
finally show ?case |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
111 |
by (auto intro: add_mono) |
61808 | 112 |
qed (auto simp add: \<open>a \<le> b\<close> less_le) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
113 |
qed } |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
114 |
note claim1 = this |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
115 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
116 |
(* second key induction: a lower bound on the measures of any finite collection of Ai's |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
117 |
that cover an interval {u..v} *) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
118 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
119 |
{ fix S u v and l r :: "nat \<Rightarrow> real" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
120 |
assume "finite S" "\<And>i. i\<in>S \<Longrightarrow> l i < r i" "{u..v} \<subseteq> (\<Union>i\<in>S. {l i<..< r i})" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
121 |
then have "F v - F u \<le> (\<Sum>i\<in>S. F (r i) - F (l i))" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
122 |
proof (induction arbitrary: v u rule: finite_psubset_induct) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
123 |
case (psubset S) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
124 |
show ?case |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
125 |
proof cases |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
126 |
assume "S = {}" then show ?case |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
127 |
using psubset by (simp add: mono_F) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
128 |
next |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
129 |
assume "S \<noteq> {}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
130 |
then obtain j where "j \<in> S" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
131 |
by auto |
47694 | 132 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
133 |
let ?R = "r j < u \<or> l j > v \<or> (\<exists>i\<in>S-{j}. l i \<le> l j \<and> r j \<le> r i)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
134 |
show ?case |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
135 |
proof cases |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
136 |
assume "?R" |
61808 | 137 |
with \<open>j \<in> S\<close> psubset.prems have "{u..v} \<subseteq> (\<Union>i\<in>S-{j}. {l i<..< r i})" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
138 |
apply (auto simp: subset_eq Ball_def) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
139 |
apply (metis Diff_iff less_le_trans leD linear singletonD) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
140 |
apply (metis Diff_iff less_le_trans leD linear singletonD) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
141 |
apply (metis order_trans less_le_not_le linear) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
142 |
done |
61808 | 143 |
with \<open>j \<in> S\<close> have "F v - F u \<le> (\<Sum>i\<in>S - {j}. F (r i) - F (l i))" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
144 |
by (intro psubset) auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
145 |
also have "\<dots> \<le> (\<Sum>i\<in>S. F (r i) - F (l i))" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
146 |
using psubset.prems |
64267 | 147 |
by (intro sum_mono2 psubset) (auto intro: less_imp_le) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
148 |
finally show ?thesis . |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
149 |
next |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
150 |
assume "\<not> ?R" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
151 |
then have j: "u \<le> r j" "l j \<le> v" "\<And>i. i \<in> S - {j} \<Longrightarrow> r i < r j \<or> l i > l j" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
152 |
by (auto simp: not_less) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
153 |
let ?S1 = "{i \<in> S. l i < l j}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
154 |
let ?S2 = "{i \<in> S. r i > r j}" |
40859 | 155 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
156 |
have "(\<Sum>i\<in>S. F (r i) - F (l i)) \<ge> (\<Sum>i\<in>?S1 \<union> ?S2 \<union> {j}. F (r i) - F (l i))" |
61808 | 157 |
using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j |
64267 | 158 |
by (intro sum_mono2) (auto intro: less_imp_le) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
159 |
also have "(\<Sum>i\<in>?S1 \<union> ?S2 \<union> {j}. F (r i) - F (l i)) = |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
160 |
(\<Sum>i\<in>?S1. F (r i) - F (l i)) + (\<Sum>i\<in>?S2 . F (r i) - F (l i)) + (F (r j) - F (l j))" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
161 |
using psubset(1) psubset.prems(1) j |
64267 | 162 |
apply (subst sum.union_disjoint) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
163 |
apply simp_all |
64267 | 164 |
apply (subst sum.union_disjoint) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
165 |
apply auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
166 |
apply (metis less_le_not_le) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
167 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
168 |
also (xtrans) have "(\<Sum>i\<in>?S1. F (r i) - F (l i)) \<ge> F (l j) - F u" |
61808 | 169 |
using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
170 |
apply (intro psubset.IH psubset) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
171 |
apply (auto simp: subset_eq Ball_def) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
172 |
apply (metis less_le_trans not_le) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
173 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
174 |
also (xtrans) have "(\<Sum>i\<in>?S2. F (r i) - F (l i)) \<ge> F v - F (r j)" |
61808 | 175 |
using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
176 |
apply (intro psubset.IH psubset) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
177 |
apply (auto simp: subset_eq Ball_def) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
178 |
apply (metis le_less_trans not_le) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
179 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
180 |
finally (xtrans) show ?case |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
181 |
by (auto simp: add_mono) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
182 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
183 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
184 |
qed } |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
185 |
note claim2 = this |
49777 | 186 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
187 |
(* now prove the inequality going the other way *) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
188 |
have "ennreal (F b - F a) \<le> (\<Sum>i. ennreal (F (r i) - F (l i)))" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
189 |
proof (rule ennreal_le_epsilon) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
190 |
fix epsilon :: real assume egt0: "epsilon > 0" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
191 |
have "\<forall>i. \<exists>d>0. F (r i + d) < F (r i) + epsilon / 2^(i+2)" |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
192 |
proof |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
193 |
fix i |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
194 |
note right_cont_F [of "r i"] |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
195 |
thus "\<exists>d>0. F (r i + d) < F (r i) + epsilon / 2^(i+2)" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
196 |
apply - |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
197 |
apply (subst (asm) continuous_at_right_real_increasing) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
198 |
apply (rule mono_F, assumption) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
199 |
apply (drule_tac x = "epsilon / 2 ^ (i + 2)" in spec) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
200 |
apply (erule impE) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
201 |
using egt0 by (auto simp add: field_simps) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
202 |
qed |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
203 |
then obtain delta where |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
204 |
deltai_gt0: "\<And>i. delta i > 0" and |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
205 |
deltai_prop: "\<And>i. F (r i + delta i) < F (r i) + epsilon / 2^(i+2)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
206 |
by metis |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
207 |
have "\<exists>a' > a. F a' - F a < epsilon / 2" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
208 |
apply (insert right_cont_F [of a]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
209 |
apply (subst (asm) continuous_at_right_real_increasing) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
210 |
using mono_F apply force |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
211 |
apply (drule_tac x = "epsilon / 2" in spec) |
59554
4044f53326c9
inlined rules to free user-space from technical names
haftmann
parents:
59425
diff
changeset
|
212 |
using egt0 unfolding mult.commute [of 2] by force |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
213 |
then obtain a' where a'lea [arith]: "a' > a" and |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
214 |
a_prop: "F a' - F a < epsilon / 2" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
215 |
by auto |
63040 | 216 |
define S' where "S' = {i. l i < r i}" |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
217 |
obtain S :: "nat set" where |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
218 |
"S \<subseteq> S'" and finS: "finite S" and |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
219 |
Sprop: "{a'..b} \<subseteq> (\<Union>i \<in> S. {l i<..<r i + delta i})" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
220 |
proof (rule compactE_image) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
221 |
show "compact {a'..b}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
222 |
by (rule compact_Icc) |
65585
a043de9ad41e
Some fixes related to compactE_image
paulson <lp15@cam.ac.uk>
parents:
65204
diff
changeset
|
223 |
show "\<And>i. i \<in> S' \<Longrightarrow> open ({l i<..<r i + delta i})" by auto |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
224 |
have "{a'..b} \<subseteq> {a <.. b}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
225 |
by auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
226 |
also have "{a <.. b} = (\<Union>i\<in>S'. {l i<..r i})" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
227 |
unfolding lr_eq_ab[symmetric] by (fastforce simp add: S'_def intro: less_le_trans) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
228 |
also have "\<dots> \<subseteq> (\<Union>i \<in> S'. {l i<..<r i + delta i})" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
229 |
apply (intro UN_mono) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
230 |
apply (auto simp: S'_def) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
231 |
apply (cut_tac i=i in deltai_gt0) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
232 |
apply simp |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
233 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
234 |
finally show "{a'..b} \<subseteq> (\<Union>i \<in> S'. {l i<..<r i + delta i})" . |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
235 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
236 |
with S'_def have Sprop2: "\<And>i. i \<in> S \<Longrightarrow> l i < r i" by auto |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
237 |
from finS have "\<exists>n. \<forall>i \<in> S. i \<le> n" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
238 |
by (subst finite_nat_set_iff_bounded_le [symmetric]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
239 |
then obtain n where Sbound [rule_format]: "\<forall>i \<in> S. i \<le> n" .. |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
240 |
have "F b - F a' \<le> (\<Sum>i\<in>S. F (r i + delta i) - F (l i))" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
241 |
apply (rule claim2 [rule_format]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
242 |
using finS Sprop apply auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
243 |
apply (frule Sprop2) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
244 |
apply (subgoal_tac "delta i > 0") |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
245 |
apply arith |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
246 |
by (rule deltai_gt0) |
61954 | 247 |
also have "... \<le> (\<Sum>i \<in> S. F(r i) - F(l i) + epsilon / 2^(i+2))" |
64267 | 248 |
apply (rule sum_mono) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
249 |
apply simp |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
250 |
apply (rule order_trans) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
251 |
apply (rule less_imp_le) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
252 |
apply (rule deltai_prop) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
253 |
by auto |
61954 | 254 |
also have "... = (\<Sum>i \<in> S. F(r i) - F(l i)) + |
255 |
(epsilon / 4) * (\<Sum>i \<in> S. (1 / 2)^i)" (is "_ = ?t + _") |
|
64267 | 256 |
by (subst sum.distrib) (simp add: field_simps sum_distrib_left) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
257 |
also have "... \<le> ?t + (epsilon / 4) * (\<Sum> i < Suc n. (1 / 2)^i)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
258 |
apply (rule add_left_mono) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
259 |
apply (rule mult_left_mono) |
64267 | 260 |
apply (rule sum_mono2) |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
261 |
using egt0 apply auto |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
262 |
by (frule Sbound, auto) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
263 |
also have "... \<le> ?t + (epsilon / 2)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
264 |
apply (rule add_left_mono) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
265 |
apply (subst geometric_sum) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
266 |
apply auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
267 |
apply (rule mult_left_mono) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
268 |
using egt0 apply auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
269 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
270 |
finally have aux2: "F b - F a' \<le> (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon / 2" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
271 |
by simp |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
272 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
273 |
have "F b - F a = (F b - F a') + (F a' - F a)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
274 |
by auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
275 |
also have "... \<le> (F b - F a') + epsilon / 2" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
276 |
using a_prop by (intro add_left_mono) simp |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
277 |
also have "... \<le> (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon / 2 + epsilon / 2" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
278 |
apply (intro add_right_mono) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
279 |
apply (rule aux2) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
280 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
281 |
also have "... = (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
282 |
by auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
283 |
also have "... \<le> (\<Sum>i\<le>n. F (r i) - F (l i)) + epsilon" |
65680
378a2f11bec9
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
paulson <lp15@cam.ac.uk>
parents:
65585
diff
changeset
|
284 |
using finS Sbound Sprop by (auto intro!: add_right_mono sum_mono2) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
285 |
finally have "ennreal (F b - F a) \<le> (\<Sum>i\<le>n. ennreal (F (r i) - F (l i))) + epsilon" |
64267 | 286 |
using egt0 by (simp add: ennreal_plus[symmetric] sum_nonneg del: ennreal_plus) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
287 |
then show "ennreal (F b - F a) \<le> (\<Sum>i. ennreal (F (r i) - F (l i))) + (epsilon :: real)" |
64267 | 288 |
by (rule order_trans) (auto intro!: add_mono sum_le_suminf simp del: sum_ennreal) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
289 |
qed |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
290 |
moreover have "(\<Sum>i. ennreal (F (r i) - F (l i))) \<le> ennreal (F b - F a)" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
291 |
using \<open>a \<le> b\<close> by (auto intro!: suminf_le_const ennreal_le_iff[THEN iffD2] claim1) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
292 |
ultimately show "(\<Sum>n. ennreal (F (r n) - F (l n))) = ennreal (F b - F a)" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
293 |
by (rule antisym[rotated]) |
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61610
diff
changeset
|
294 |
qed (auto simp: Ioc_inj mono_F) |
38656 | 295 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
296 |
lemma measure_interval_measure_Ioc: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
297 |
assumes "a \<le> b" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
298 |
assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y" |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
299 |
assumes right_cont_F : "\<And>a. continuous (at_right a) F" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
300 |
shows "measure (interval_measure F) {a <.. b} = F b - F a" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
301 |
unfolding measure_def |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
302 |
apply (subst emeasure_interval_measure_Ioc) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
303 |
apply fact+ |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
304 |
apply (simp add: assms) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
305 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
306 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
307 |
lemma emeasure_interval_measure_Ioc_eq: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
308 |
"(\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y) \<Longrightarrow> (\<And>a. continuous (at_right a) F) \<Longrightarrow> |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
309 |
emeasure (interval_measure F) {a <.. b} = (if a \<le> b then F b - F a else 0)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
310 |
using emeasure_interval_measure_Ioc[of a b F] by auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
311 |
|
59048 | 312 |
lemma sets_interval_measure [simp, measurable_cong]: "sets (interval_measure F) = sets borel" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
313 |
apply (simp add: sets_extend_measure interval_measure_def borel_sigma_sets_Ioc) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
314 |
apply (rule sigma_sets_eqI) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
315 |
apply auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
316 |
apply (case_tac "a \<le> ba") |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
317 |
apply (auto intro: sigma_sets.Empty) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
318 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
319 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
320 |
lemma space_interval_measure [simp]: "space (interval_measure F) = UNIV" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
321 |
by (simp add: interval_measure_def space_extend_measure) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
322 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
323 |
lemma emeasure_interval_measure_Icc: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
324 |
assumes "a \<le> b" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
325 |
assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y" |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
326 |
assumes cont_F : "continuous_on UNIV F" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
327 |
shows "emeasure (interval_measure F) {a .. b} = F b - F a" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
328 |
proof (rule tendsto_unique) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
329 |
{ fix a b :: real assume "a \<le> b" then have "emeasure (interval_measure F) {a <.. b} = F b - F a" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
330 |
using cont_F |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
331 |
by (subst emeasure_interval_measure_Ioc) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
332 |
(auto intro: mono_F continuous_within_subset simp: continuous_on_eq_continuous_within) } |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
333 |
note * = this |
38656 | 334 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
335 |
let ?F = "interval_measure F" |
61973 | 336 |
show "((\<lambda>a. F b - F a) \<longlongrightarrow> emeasure ?F {a..b}) (at_left a)" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
337 |
proof (rule tendsto_at_left_sequentially) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
338 |
show "a - 1 < a" by simp |
61969 | 339 |
fix X assume "\<And>n. X n < a" "incseq X" "X \<longlonglongrightarrow> a" |
340 |
with \<open>a \<le> b\<close> have "(\<lambda>n. emeasure ?F {X n<..b}) \<longlonglongrightarrow> emeasure ?F (\<Inter>n. {X n <..b})" |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
341 |
apply (intro Lim_emeasure_decseq) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
342 |
apply (auto simp: decseq_def incseq_def emeasure_interval_measure_Ioc *) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
343 |
apply force |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
344 |
apply (subst (asm ) *) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
345 |
apply (auto intro: less_le_trans less_imp_le) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
346 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
347 |
also have "(\<Inter>n. {X n <..b}) = {a..b}" |
61808 | 348 |
using \<open>\<And>n. X n < a\<close> |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
349 |
apply auto |
61969 | 350 |
apply (rule LIMSEQ_le_const2[OF \<open>X \<longlonglongrightarrow> a\<close>]) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
351 |
apply (auto intro: less_imp_le) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
352 |
apply (auto intro: less_le_trans) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
353 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
354 |
also have "(\<lambda>n. emeasure ?F {X n<..b}) = (\<lambda>n. F b - F (X n))" |
61808 | 355 |
using \<open>\<And>n. X n < a\<close> \<open>a \<le> b\<close> by (subst *) (auto intro: less_imp_le less_le_trans) |
61969 | 356 |
finally show "(\<lambda>n. F b - F (X n)) \<longlonglongrightarrow> emeasure ?F {a..b}" . |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
357 |
qed |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
358 |
show "((\<lambda>a. ennreal (F b - F a)) \<longlongrightarrow> F b - F a) (at_left a)" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
359 |
by (rule continuous_on_tendsto_compose[where g="\<lambda>x. x" and s=UNIV]) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
360 |
(auto simp: continuous_on_ennreal continuous_on_diff cont_F continuous_on_const) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
361 |
qed (rule trivial_limit_at_left_real) |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
362 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
363 |
lemma sigma_finite_interval_measure: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
364 |
assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y" |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
365 |
assumes right_cont_F : "\<And>a. continuous (at_right a) F" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
366 |
shows "sigma_finite_measure (interval_measure F)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
367 |
apply unfold_locales |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
368 |
apply (intro exI[of _ "(\<lambda>(a, b). {a <.. b}) ` (\<rat> \<times> \<rat>)"]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
369 |
apply (auto intro!: Rats_no_top_le Rats_no_bot_less countable_rat simp: emeasure_interval_measure_Ioc_eq[OF assms]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
370 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
371 |
|
61808 | 372 |
subsection \<open>Lebesgue-Borel measure\<close> |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
373 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
374 |
definition lborel :: "('a :: euclidean_space) measure" where |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
375 |
"lborel = distr (\<Pi>\<^sub>M b\<in>Basis. interval_measure (\<lambda>x. x)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
376 |
|
63958
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
377 |
abbreviation lebesgue :: "'a::euclidean_space measure" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
378 |
where "lebesgue \<equiv> completion lborel" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
379 |
|
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
380 |
abbreviation lebesgue_on :: "'a set \<Rightarrow> 'a::euclidean_space measure" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
381 |
where "lebesgue_on \<Omega> \<equiv> restrict_space (completion lborel) \<Omega>" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
382 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
383 |
lemma |
59048 | 384 |
shows sets_lborel[simp, measurable_cong]: "sets lborel = sets borel" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
385 |
and space_lborel[simp]: "space lborel = space borel" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
386 |
and measurable_lborel1[simp]: "measurable M lborel = measurable M borel" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
387 |
and measurable_lborel2[simp]: "measurable lborel M = measurable borel M" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
388 |
by (simp_all add: lborel_def) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
389 |
|
66164
2d79288b042c
New theorems and much tidying up of the old ones
paulson <lp15@cam.ac.uk>
parents:
65680
diff
changeset
|
390 |
lemma sets_lebesgue_on_refl [iff]: "S \<in> sets (lebesgue_on S)" |
2d79288b042c
New theorems and much tidying up of the old ones
paulson <lp15@cam.ac.uk>
parents:
65680
diff
changeset
|
391 |
by (metis inf_top.right_neutral sets.top space_borel space_completion space_lborel space_restrict_space) |
2d79288b042c
New theorems and much tidying up of the old ones
paulson <lp15@cam.ac.uk>
parents:
65680
diff
changeset
|
392 |
|
2d79288b042c
New theorems and much tidying up of the old ones
paulson <lp15@cam.ac.uk>
parents:
65680
diff
changeset
|
393 |
lemma Compl_in_sets_lebesgue: "-A \<in> sets lebesgue \<longleftrightarrow> A \<in> sets lebesgue" |
2d79288b042c
New theorems and much tidying up of the old ones
paulson <lp15@cam.ac.uk>
parents:
65680
diff
changeset
|
394 |
by (metis Compl_eq_Diff_UNIV double_compl space_borel space_completion space_lborel Sigma_Algebra.sets.compl_sets) |
2d79288b042c
New theorems and much tidying up of the old ones
paulson <lp15@cam.ac.uk>
parents:
65680
diff
changeset
|
395 |
|
67982
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
396 |
lemma measurable_lebesgue_cong: |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
397 |
assumes "\<And>x. x \<in> S \<Longrightarrow> f x = g x" |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
398 |
shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M" |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
399 |
by (metis (mono_tags, lifting) IntD1 assms measurable_cong_strong space_restrict_space) |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
400 |
|
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
401 |
text\<open>Measurability of continuous functions\<close> |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
402 |
lemma continuous_imp_measurable_on_sets_lebesgue: |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
403 |
assumes f: "continuous_on S f" and S: "S \<in> sets lebesgue" |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
404 |
shows "f \<in> borel_measurable (lebesgue_on S)" |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
405 |
proof - |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
406 |
have "sets (restrict_space borel S) \<subseteq> sets (lebesgue_on S)" |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
407 |
by (simp add: mono_restrict_space subsetI) |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
408 |
then show ?thesis |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
409 |
by (simp add: borel_measurable_continuous_on_restrict [OF f] borel_measurable_subalgebra |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
410 |
space_restrict_space) |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
411 |
qed |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
412 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
413 |
context |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
414 |
begin |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
415 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
416 |
interpretation sigma_finite_measure "interval_measure (\<lambda>x. x)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
417 |
by (rule sigma_finite_interval_measure) auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
418 |
interpretation finite_product_sigma_finite "\<lambda>_. interval_measure (\<lambda>x. x)" Basis |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
419 |
proof qed simp |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
420 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
421 |
lemma lborel_eq_real: "lborel = interval_measure (\<lambda>x. x)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
422 |
unfolding lborel_def Basis_real_def |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
423 |
using distr_id[of "interval_measure (\<lambda>x. x)"] |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
424 |
by (subst distr_component[symmetric]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
425 |
(simp_all add: distr_distr comp_def del: distr_id cong: distr_cong) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
426 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
427 |
lemma lborel_eq: "lborel = distr (\<Pi>\<^sub>M b\<in>Basis. lborel) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
428 |
by (subst lborel_def) (simp add: lborel_eq_real) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
429 |
|
64272 | 430 |
lemma nn_integral_lborel_prod: |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
431 |
assumes [measurable]: "\<And>b. b \<in> Basis \<Longrightarrow> f b \<in> borel_measurable borel" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
432 |
assumes nn[simp]: "\<And>b x. b \<in> Basis \<Longrightarrow> 0 \<le> f b x" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
433 |
shows "(\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. f b (x \<bullet> b)) \<partial>lborel) = (\<Prod>b\<in>Basis. (\<integral>\<^sup>+x. f b x \<partial>lborel))" |
64272 | 434 |
by (simp add: lborel_def nn_integral_distr product_nn_integral_prod |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
435 |
product_nn_integral_singleton) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
436 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
437 |
lemma emeasure_lborel_Icc[simp]: |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
438 |
fixes l u :: real |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
439 |
assumes [simp]: "l \<le> u" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
440 |
shows "emeasure lborel {l .. u} = u - l" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50418
diff
changeset
|
441 |
proof - |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
442 |
have "((\<lambda>f. f 1) -` {l..u} \<inter> space (Pi\<^sub>M {1} (\<lambda>b. interval_measure (\<lambda>x. x)))) = {1::real} \<rightarrow>\<^sub>E {l..u}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
443 |
by (auto simp: space_PiM) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
444 |
then show ?thesis |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
445 |
by (simp add: lborel_def emeasure_distr emeasure_PiM emeasure_interval_measure_Icc continuous_on_id) |
50104 | 446 |
qed |
447 |
||
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
448 |
lemma emeasure_lborel_Icc_eq: "emeasure lborel {l .. u} = ennreal (if l \<le> u then u - l else 0)" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
449 |
by simp |
47694 | 450 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
451 |
lemma emeasure_lborel_cbox[simp]: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
452 |
assumes [simp]: "\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
453 |
shows "emeasure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
41654 | 454 |
proof - |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
455 |
have "(\<lambda>x. \<Prod>b\<in>Basis. indicator {l\<bullet>b .. u\<bullet>b} (x \<bullet> b) :: ennreal) = indicator (cbox l u)" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
456 |
by (auto simp: fun_eq_iff cbox_def split: split_indicator) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
457 |
then have "emeasure lborel (cbox l u) = (\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. indicator {l\<bullet>b .. u\<bullet>b} (x \<bullet> b)) \<partial>lborel)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
458 |
by simp |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
459 |
also have "\<dots> = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
64272 | 460 |
by (subst nn_integral_lborel_prod) (simp_all add: prod_ennreal inner_diff_left) |
47694 | 461 |
finally show ?thesis . |
38656 | 462 |
qed |
463 |
||
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
464 |
lemma AE_lborel_singleton: "AE x in lborel::'a::euclidean_space measure. x \<noteq> c" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
465 |
using SOME_Basis AE_discrete_difference [of "{c}" lborel] emeasure_lborel_cbox [of c c] |
67982
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
466 |
by (auto simp add: power_0_left) |
47757
5e6fe71e2390
equate positive Lebesgue integral and MV-Analysis' Gauge integral
hoelzl
parents:
47694
diff
changeset
|
467 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
468 |
lemma emeasure_lborel_Ioo[simp]: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
469 |
assumes [simp]: "l \<le> u" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
470 |
shows "emeasure lborel {l <..< u} = ennreal (u - l)" |
40859 | 471 |
proof - |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
472 |
have "emeasure lborel {l <..< u} = emeasure lborel {l .. u}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
473 |
using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto |
47694 | 474 |
then show ?thesis |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
475 |
by simp |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
476 |
qed |
38656 | 477 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
478 |
lemma emeasure_lborel_Ioc[simp]: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
479 |
assumes [simp]: "l \<le> u" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
480 |
shows "emeasure lborel {l <.. u} = ennreal (u - l)" |
41654 | 481 |
proof - |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
482 |
have "emeasure lborel {l <.. u} = emeasure lborel {l .. u}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
483 |
using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
484 |
then show ?thesis |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
485 |
by simp |
38656 | 486 |
qed |
487 |
||
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
488 |
lemma emeasure_lborel_Ico[simp]: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
489 |
assumes [simp]: "l \<le> u" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
490 |
shows "emeasure lborel {l ..< u} = ennreal (u - l)" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
491 |
proof - |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
492 |
have "emeasure lborel {l ..< u} = emeasure lborel {l .. u}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
493 |
using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
494 |
then show ?thesis |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
495 |
by simp |
38656 | 496 |
qed |
497 |
||
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
498 |
lemma emeasure_lborel_box[simp]: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
499 |
assumes [simp]: "\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
500 |
shows "emeasure lborel (box l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
501 |
proof - |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
502 |
have "(\<lambda>x. \<Prod>b\<in>Basis. indicator {l\<bullet>b <..< u\<bullet>b} (x \<bullet> b) :: ennreal) = indicator (box l u)" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
503 |
by (auto simp: fun_eq_iff box_def split: split_indicator) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
504 |
then have "emeasure lborel (box l u) = (\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. indicator {l\<bullet>b <..< u\<bullet>b} (x \<bullet> b)) \<partial>lborel)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
505 |
by simp |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
506 |
also have "\<dots> = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
64272 | 507 |
by (subst nn_integral_lborel_prod) (simp_all add: prod_ennreal inner_diff_left) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
508 |
finally show ?thesis . |
40859 | 509 |
qed |
38656 | 510 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
511 |
lemma emeasure_lborel_cbox_eq: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
512 |
"emeasure lborel (cbox l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
513 |
using box_eq_empty(2)[THEN iffD2, of u l] by (auto simp: not_le) |
41654 | 514 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
515 |
lemma emeasure_lborel_box_eq: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
516 |
"emeasure lborel (box l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
517 |
using box_eq_empty(1)[THEN iffD2, of u l] by (auto simp: not_le dest!: less_imp_le) force |
40859 | 518 |
|
63886
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
519 |
lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0" |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
520 |
using emeasure_lborel_cbox[of x x] nonempty_Basis |
66164
2d79288b042c
New theorems and much tidying up of the old ones
paulson <lp15@cam.ac.uk>
parents:
65680
diff
changeset
|
521 |
by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: prod_constant) |
2d79288b042c
New theorems and much tidying up of the old ones
paulson <lp15@cam.ac.uk>
parents:
65680
diff
changeset
|
522 |
|
2d79288b042c
New theorems and much tidying up of the old ones
paulson <lp15@cam.ac.uk>
parents:
65680
diff
changeset
|
523 |
lemma fmeasurable_cbox [iff]: "cbox a b \<in> fmeasurable lborel" |
2d79288b042c
New theorems and much tidying up of the old ones
paulson <lp15@cam.ac.uk>
parents:
65680
diff
changeset
|
524 |
and fmeasurable_box [iff]: "box a b \<in> fmeasurable lborel" |
2d79288b042c
New theorems and much tidying up of the old ones
paulson <lp15@cam.ac.uk>
parents:
65680
diff
changeset
|
525 |
by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq) |
63886
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
526 |
|
40859 | 527 |
lemma |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
528 |
fixes l u :: real |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
529 |
assumes [simp]: "l \<le> u" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
530 |
shows measure_lborel_Icc[simp]: "measure lborel {l .. u} = u - l" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
531 |
and measure_lborel_Ico[simp]: "measure lborel {l ..< u} = u - l" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
532 |
and measure_lborel_Ioc[simp]: "measure lborel {l <.. u} = u - l" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
533 |
and measure_lborel_Ioo[simp]: "measure lborel {l <..< u} = u - l" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
534 |
by (simp_all add: measure_def) |
40859 | 535 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
536 |
lemma |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
537 |
assumes [simp]: "\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
538 |
shows measure_lborel_box[simp]: "measure lborel (box l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
539 |
and measure_lborel_cbox[simp]: "measure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
64272 | 540 |
by (simp_all add: measure_def inner_diff_left prod_nonneg) |
41654 | 541 |
|
63886
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
542 |
lemma measure_lborel_cbox_eq: |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
543 |
"measure lborel (cbox l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)" |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
544 |
using box_eq_empty(2)[THEN iffD2, of u l] by (auto simp: not_le) |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
545 |
|
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
546 |
lemma measure_lborel_box_eq: |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
547 |
"measure lborel (box l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)" |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
548 |
using box_eq_empty(1)[THEN iffD2, of u l] by (auto simp: not_le dest!: less_imp_le) force |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
549 |
|
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
550 |
lemma measure_lborel_singleton[simp]: "measure lborel {x} = 0" |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
551 |
by (simp add: measure_def) |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
552 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
553 |
lemma sigma_finite_lborel: "sigma_finite_measure lborel" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
554 |
proof |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
555 |
show "\<exists>A::'a set set. countable A \<and> A \<subseteq> sets lborel \<and> \<Union>A = space lborel \<and> (\<forall>a\<in>A. emeasure lborel a \<noteq> \<infinity>)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
556 |
by (intro exI[of _ "range (\<lambda>n::nat. box (- real n *\<^sub>R One) (real n *\<^sub>R One))"]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
557 |
(auto simp: emeasure_lborel_cbox_eq UN_box_eq_UNIV) |
49777 | 558 |
qed |
40859 | 559 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
560 |
end |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
561 |
|
67982
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
562 |
lemma emeasure_lborel_UNIV [simp]: "emeasure lborel (UNIV::'a::euclidean_space set) = \<infinity>" |
59741
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
563 |
proof - |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
564 |
{ fix n::nat |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
565 |
let ?Ba = "Basis :: 'a set" |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
566 |
have "real n \<le> (2::real) ^ card ?Ba * real n" |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
567 |
by (simp add: mult_le_cancel_right1) |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
568 |
also |
59741
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
569 |
have "... \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba" |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
570 |
apply (rule mult_left_mono) |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
571 |
apply (metis DIM_positive One_nat_def less_eq_Suc_le less_imp_le of_nat_le_iff of_nat_power self_le_power zero_less_Suc) |
59741
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
572 |
apply (simp add: DIM_positive) |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
573 |
done |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
574 |
finally have "real n \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba" . |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
575 |
} note [intro!] = this |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
576 |
show ?thesis |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
577 |
unfolding UN_box_eq_UNIV[symmetric] |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
578 |
apply (subst SUP_emeasure_incseq[symmetric]) |
64272 | 579 |
apply (auto simp: incseq_def subset_box inner_add_left prod_constant |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
580 |
simp del: Sup_eq_top_iff SUP_eq_top_iff |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
581 |
intro!: ennreal_SUP_eq_top) |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
582 |
done |
59741
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59554
diff
changeset
|
583 |
qed |
40859 | 584 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
585 |
lemma emeasure_lborel_countable: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
586 |
fixes A :: "'a::euclidean_space set" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
587 |
assumes "countable A" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
588 |
shows "emeasure lborel A = 0" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
589 |
proof - |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
590 |
have "A \<subseteq> (\<Union>i. {from_nat_into A i})" using from_nat_into_surj assms by force |
63262 | 591 |
then have "emeasure lborel A \<le> emeasure lborel (\<Union>i. {from_nat_into A i})" |
592 |
by (intro emeasure_mono) auto |
|
593 |
also have "emeasure lborel (\<Union>i. {from_nat_into A i}) = 0" |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
594 |
by (rule emeasure_UN_eq_0) auto |
63262 | 595 |
finally show ?thesis |
596 |
by (auto simp add: ) |
|
40859 | 597 |
qed |
598 |
||
59425 | 599 |
lemma countable_imp_null_set_lborel: "countable A \<Longrightarrow> A \<in> null_sets lborel" |
600 |
by (simp add: null_sets_def emeasure_lborel_countable sets.countable) |
|
601 |
||
602 |
lemma finite_imp_null_set_lborel: "finite A \<Longrightarrow> A \<in> null_sets lborel" |
|
603 |
by (intro countable_imp_null_set_lborel countable_finite) |
|
604 |
||
605 |
lemma lborel_neq_count_space[simp]: "lborel \<noteq> count_space (A::('a::ordered_euclidean_space) set)" |
|
606 |
proof |
|
607 |
assume asm: "lborel = count_space A" |
|
608 |
have "space lborel = UNIV" by simp |
|
609 |
hence [simp]: "A = UNIV" by (subst (asm) asm) (simp only: space_count_space) |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
610 |
have "emeasure lborel {undefined::'a} = 1" |
59425 | 611 |
by (subst asm, subst emeasure_count_space_finite) auto |
612 |
moreover have "emeasure lborel {undefined} \<noteq> 1" by simp |
|
613 |
ultimately show False by contradiction |
|
614 |
qed |
|
615 |
||
65204
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
616 |
lemma mem_closed_if_AE_lebesgue_open: |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
617 |
assumes "open S" "closed C" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
618 |
assumes "AE x \<in> S in lebesgue. x \<in> C" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
619 |
assumes "x \<in> S" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
620 |
shows "x \<in> C" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
621 |
proof (rule ccontr) |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
622 |
assume xC: "x \<notin> C" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
623 |
with openE[of "S - C"] assms |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
624 |
obtain e where e: "0 < e" "ball x e \<subseteq> S - C" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
625 |
by blast |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
626 |
then obtain a b where box: "x \<in> box a b" "box a b \<subseteq> S - C" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
627 |
by (metis rational_boxes order_trans) |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
628 |
then have "0 < emeasure lebesgue (box a b)" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
629 |
by (auto simp: emeasure_lborel_box_eq mem_box algebra_simps intro!: prod_pos) |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
630 |
also have "\<dots> \<le> emeasure lebesgue (S - C)" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
631 |
using assms box |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
632 |
by (auto intro!: emeasure_mono) |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
633 |
also have "\<dots> = 0" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
634 |
using assms |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
635 |
by (auto simp: eventually_ae_filter completion.complete2 set_diff_eq null_setsD1) |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
636 |
finally show False by simp |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
637 |
qed |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
638 |
|
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
639 |
lemma mem_closed_if_AE_lebesgue: "closed C \<Longrightarrow> (AE x in lebesgue. x \<in> C) \<Longrightarrow> x \<in> C" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
640 |
using mem_closed_if_AE_lebesgue_open[OF open_UNIV] by simp |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
641 |
|
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
642 |
|
61808 | 643 |
subsection \<open>Affine transformation on the Lebesgue-Borel\<close> |
49777 | 644 |
|
645 |
lemma lborel_eqI: |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
646 |
fixes M :: "'a::euclidean_space measure" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
647 |
assumes emeasure_eq: "\<And>l u. (\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b) \<Longrightarrow> emeasure M (box l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
49777 | 648 |
assumes sets_eq: "sets M = sets borel" |
649 |
shows "lborel = M" |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
650 |
proof (rule measure_eqI_generator_eq) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
651 |
let ?E = "range (\<lambda>(a, b). box a b::'a set)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
652 |
show "Int_stable ?E" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
653 |
by (auto simp: Int_stable_def box_Int_box) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
654 |
|
49777 | 655 |
show "?E \<subseteq> Pow UNIV" "sets lborel = sigma_sets UNIV ?E" "sets M = sigma_sets UNIV ?E" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
656 |
by (simp_all add: borel_eq_box sets_eq) |
49777 | 657 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
658 |
let ?A = "\<lambda>n::nat. box (- (real n *\<^sub>R One)) (real n *\<^sub>R One) :: 'a set" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
659 |
show "range ?A \<subseteq> ?E" "(\<Union>i. ?A i) = UNIV" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
660 |
unfolding UN_box_eq_UNIV by auto |
49777 | 661 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
662 |
{ fix i show "emeasure lborel (?A i) \<noteq> \<infinity>" by auto } |
49777 | 663 |
{ fix X assume "X \<in> ?E" then show "emeasure lborel X = emeasure M X" |
63886
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
664 |
apply (auto simp: emeasure_eq emeasure_lborel_box_eq) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
665 |
apply (subst box_eq_empty(1)[THEN iffD2]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
666 |
apply (auto intro: less_imp_le simp: not_le) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
667 |
done } |
49777 | 668 |
qed |
669 |
||
63886
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
670 |
lemma lborel_affine_euclidean: |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
671 |
fixes c :: "'a::euclidean_space \<Rightarrow> real" and t |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
672 |
defines "T x \<equiv> t + (\<Sum>j\<in>Basis. (c j * (x \<bullet> j)) *\<^sub>R j)" |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
673 |
assumes c: "\<And>j. j \<in> Basis \<Longrightarrow> c j \<noteq> 0" |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
674 |
shows "lborel = density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" (is "_ = ?D") |
49777 | 675 |
proof (rule lborel_eqI) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
676 |
let ?B = "Basis :: 'a set" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
677 |
fix l u assume le: "\<And>b. b \<in> ?B \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b" |
63886
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
678 |
have [measurable]: "T \<in> borel \<rightarrow>\<^sub>M borel" |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
679 |
by (simp add: T_def[abs_def]) |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
680 |
have eq: "T -` box l u = box |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
681 |
(\<Sum>j\<in>Basis. (((if 0 < c j then l - t else u - t) \<bullet> j) / c j) *\<^sub>R j) |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
682 |
(\<Sum>j\<in>Basis. (((if 0 < c j then u - t else l - t) \<bullet> j) / c j) *\<^sub>R j)" |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
683 |
using c by (auto simp: box_def T_def field_simps inner_simps divide_less_eq) |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
684 |
with le c show "emeasure ?D (box l u) = (\<Prod>b\<in>?B. (u - l) \<bullet> b)" |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
685 |
by (auto simp: emeasure_density emeasure_distr nn_integral_multc emeasure_lborel_box_eq inner_simps |
64272 | 686 |
field_simps divide_simps ennreal_mult'[symmetric] prod_nonneg prod.distrib[symmetric] |
687 |
intro!: prod.cong) |
|
49777 | 688 |
qed simp |
689 |
||
63886
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
690 |
lemma lborel_affine: |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
691 |
fixes t :: "'a::euclidean_space" |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
692 |
shows "c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c *\<^sub>R x)) (\<lambda>_. \<bar>c\<bar>^DIM('a))" |
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
693 |
using lborel_affine_euclidean[where c="\<lambda>_::'a. c" and t=t] |
64272 | 694 |
unfolding scaleR_scaleR[symmetric] scaleR_sum_right[symmetric] euclidean_representation prod_constant by simp |
63886
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63627
diff
changeset
|
695 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
696 |
lemma lborel_real_affine: |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
697 |
"c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c * x)) (\<lambda>_. ennreal (abs c))" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
698 |
using lborel_affine[of c t] by simp |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
699 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
700 |
lemma AE_borel_affine: |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
701 |
fixes P :: "real \<Rightarrow> bool" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
702 |
shows "c \<noteq> 0 \<Longrightarrow> Measurable.pred borel P \<Longrightarrow> AE x in lborel. P x \<Longrightarrow> AE x in lborel. P (t + c * x)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
703 |
by (subst lborel_real_affine[where t="- t / c" and c="1 / c"]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
704 |
(simp_all add: AE_density AE_distr_iff field_simps) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
705 |
|
56996 | 706 |
lemma nn_integral_real_affine: |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
707 |
fixes c :: real assumes [measurable]: "f \<in> borel_measurable borel" and c: "c \<noteq> 0" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
708 |
shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = \<bar>c\<bar> * (\<integral>\<^sup>+x. f (t + c * x) \<partial>lborel)" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
709 |
by (subst lborel_real_affine[OF c, of t]) |
56996 | 710 |
(simp add: nn_integral_density nn_integral_distr nn_integral_cmult) |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
711 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
712 |
lemma lborel_integrable_real_affine: |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
713 |
fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
714 |
assumes f: "integrable lborel f" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
715 |
shows "c \<noteq> 0 \<Longrightarrow> integrable lborel (\<lambda>x. f (t + c * x))" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
716 |
using f f[THEN borel_measurable_integrable] unfolding integrable_iff_bounded |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
717 |
by (subst (asm) nn_integral_real_affine[where c=c and t=t]) (auto simp: ennreal_mult_less_top) |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
718 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
719 |
lemma lborel_integrable_real_affine_iff: |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
720 |
fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
721 |
shows "c \<noteq> 0 \<Longrightarrow> integrable lborel (\<lambda>x. f (t + c * x)) \<longleftrightarrow> integrable lborel f" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
722 |
using |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
723 |
lborel_integrable_real_affine[of f c t] |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
724 |
lborel_integrable_real_affine[of "\<lambda>x. f (t + c * x)" "1/c" "-t/c"] |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
725 |
by (auto simp add: field_simps) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
726 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
727 |
lemma lborel_integral_real_affine: |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
728 |
fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" and c :: real |
57166
5cfcc616d485
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
hoelzl
parents:
57138
diff
changeset
|
729 |
assumes c: "c \<noteq> 0" shows "(\<integral>x. f x \<partial> lborel) = \<bar>c\<bar> *\<^sub>R (\<integral>x. f (t + c * x) \<partial>lborel)" |
5cfcc616d485
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
hoelzl
parents:
57138
diff
changeset
|
730 |
proof cases |
5cfcc616d485
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
hoelzl
parents:
57138
diff
changeset
|
731 |
assume f[measurable]: "integrable lborel f" then show ?thesis |
5cfcc616d485
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
hoelzl
parents:
57138
diff
changeset
|
732 |
using c f f[THEN borel_measurable_integrable] f[THEN lborel_integrable_real_affine, of c t] |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
733 |
by (subst lborel_real_affine[OF c, of t]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
734 |
(simp add: integral_density integral_distr) |
57166
5cfcc616d485
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
hoelzl
parents:
57138
diff
changeset
|
735 |
next |
5cfcc616d485
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
hoelzl
parents:
57138
diff
changeset
|
736 |
assume "\<not> integrable lborel f" with c show ?thesis |
5cfcc616d485
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
hoelzl
parents:
57138
diff
changeset
|
737 |
by (simp add: lborel_integrable_real_affine_iff not_integrable_integral_eq) |
5cfcc616d485
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
hoelzl
parents:
57138
diff
changeset
|
738 |
qed |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
739 |
|
63958
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
740 |
lemma |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
741 |
fixes c :: "'a::euclidean_space \<Rightarrow> real" and t |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
742 |
assumes c: "\<And>j. j \<in> Basis \<Longrightarrow> c j \<noteq> 0" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
743 |
defines "T == (\<lambda>x. t + (\<Sum>j\<in>Basis. (c j * (x \<bullet> j)) *\<^sub>R j))" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
744 |
shows lebesgue_affine_euclidean: "lebesgue = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" (is "_ = ?D") |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
745 |
and lebesgue_affine_measurable: "T \<in> lebesgue \<rightarrow>\<^sub>M lebesgue" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
746 |
proof - |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
747 |
have T_borel[measurable]: "T \<in> borel \<rightarrow>\<^sub>M borel" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
748 |
by (auto simp: T_def[abs_def]) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
749 |
{ fix A :: "'a set" assume A: "A \<in> sets borel" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
750 |
then have "emeasure lborel A = 0 \<longleftrightarrow> emeasure (density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))) A = 0" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
751 |
unfolding T_def using c by (subst lborel_affine_euclidean[symmetric]) auto |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
752 |
also have "\<dots> \<longleftrightarrow> emeasure (distr lebesgue lborel T) A = 0" |
64272 | 753 |
using A c by (simp add: distr_completion emeasure_density nn_integral_cmult prod_nonneg cong: distr_cong) |
63958
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
754 |
finally have "emeasure lborel A = 0 \<longleftrightarrow> emeasure (distr lebesgue lborel T) A = 0" . } |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
755 |
then have eq: "null_sets lborel = null_sets (distr lebesgue lborel T)" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
756 |
by (auto simp: null_sets_def) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
757 |
|
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
758 |
show "T \<in> lebesgue \<rightarrow>\<^sub>M lebesgue" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
759 |
by (rule completion.measurable_completion2) (auto simp: eq measurable_completion) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
760 |
|
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
761 |
have "lebesgue = completion (density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>)))" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
762 |
using c by (subst lborel_affine_euclidean[of c t]) (simp_all add: T_def[abs_def]) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
763 |
also have "\<dots> = density (completion (distr lebesgue lborel T)) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" |
64272 | 764 |
using c by (auto intro!: always_eventually prod_pos completion_density_eq simp: distr_completion cong: distr_cong) |
63958
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
765 |
also have "\<dots> = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
766 |
by (subst completion.completion_distr_eq) (auto simp: eq measurable_completion) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
767 |
finally show "lebesgue = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" . |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
768 |
qed |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
769 |
|
67399 | 770 |
lemma lebesgue_measurable_scaling[measurable]: "( *\<^sub>R) x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue" |
63959
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
771 |
proof cases |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
772 |
assume "x = 0" |
67399 | 773 |
then have "( *\<^sub>R) x = (\<lambda>x. 0::'a)" |
63959
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
774 |
by (auto simp: fun_eq_iff) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
775 |
then show ?thesis by auto |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
776 |
next |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
777 |
assume "x \<noteq> 0" then show ?thesis |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
778 |
using lebesgue_affine_measurable[of "\<lambda>_. x" 0] |
64267 | 779 |
unfolding scaleR_scaleR[symmetric] scaleR_sum_right[symmetric] euclidean_representation |
63959
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
780 |
by (auto simp add: ac_simps) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
781 |
qed |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
782 |
|
63958
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
783 |
lemma |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
784 |
fixes m :: real and \<delta> :: "'a::euclidean_space" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
785 |
defines "T r d x \<equiv> r *\<^sub>R x + d" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
786 |
shows emeasure_lebesgue_affine: "emeasure lebesgue (T m \<delta> ` S) = \<bar>m\<bar> ^ DIM('a) * emeasure lebesgue S" (is ?e) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
787 |
and measure_lebesgue_affine: "measure lebesgue (T m \<delta> ` S) = \<bar>m\<bar> ^ DIM('a) * measure lebesgue S" (is ?m) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
788 |
proof - |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
789 |
show ?e |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
790 |
proof cases |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
791 |
assume "m = 0" then show ?thesis |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
792 |
by (simp add: image_constant_conv T_def[abs_def]) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
793 |
next |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
794 |
let ?T = "T m \<delta>" and ?T' = "T (1 / m) (- ((1/m) *\<^sub>R \<delta>))" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
795 |
assume "m \<noteq> 0" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
796 |
then have s_comp_s: "?T' \<circ> ?T = id" "?T \<circ> ?T' = id" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
797 |
by (auto simp: T_def[abs_def] fun_eq_iff scaleR_add_right scaleR_diff_right) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
798 |
then have "inv ?T' = ?T" "bij ?T'" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
799 |
by (auto intro: inv_unique_comp o_bij) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
800 |
then have eq: "T m \<delta> ` S = T (1 / m) ((-1/m) *\<^sub>R \<delta>) -` S \<inter> space lebesgue" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
801 |
using bij_vimage_eq_inv_image[OF \<open>bij ?T'\<close>, of S] by auto |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
802 |
|
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
803 |
have trans_eq_T: "(\<lambda>x. \<delta> + (\<Sum>j\<in>Basis. (m * (x \<bullet> j)) *\<^sub>R j)) = T m \<delta>" for m \<delta> |
64267 | 804 |
unfolding T_def[abs_def] scaleR_scaleR[symmetric] scaleR_sum_right[symmetric] |
63958
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
805 |
by (auto simp add: euclidean_representation ac_simps) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
806 |
|
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
807 |
have T[measurable]: "T r d \<in> lebesgue \<rightarrow>\<^sub>M lebesgue" for r d |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
808 |
using lebesgue_affine_measurable[of "\<lambda>_. r" d] |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
809 |
by (cases "r = 0") (auto simp: trans_eq_T T_def[abs_def]) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
810 |
|
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
811 |
show ?thesis |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
812 |
proof cases |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
813 |
assume "S \<in> sets lebesgue" with \<open>m \<noteq> 0\<close> show ?thesis |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
814 |
unfolding eq |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
815 |
apply (subst lebesgue_affine_euclidean[of "\<lambda>_. m" \<delta>]) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
816 |
apply (simp_all add: emeasure_density trans_eq_T nn_integral_cmult emeasure_distr |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
817 |
del: space_completion emeasure_completion) |
64272 | 818 |
apply (simp add: vimage_comp s_comp_s prod_constant) |
63958
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
819 |
done |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
820 |
next |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
821 |
assume "S \<notin> sets lebesgue" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
822 |
moreover have "?T ` S \<notin> sets lebesgue" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
823 |
proof |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
824 |
assume "?T ` S \<in> sets lebesgue" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
825 |
then have "?T -` (?T ` S) \<inter> space lebesgue \<in> sets lebesgue" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
826 |
by (rule measurable_sets[OF T]) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
827 |
also have "?T -` (?T ` S) \<inter> space lebesgue = S" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
828 |
by (simp add: vimage_comp s_comp_s eq) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
829 |
finally show False using \<open>S \<notin> sets lebesgue\<close> by auto |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
830 |
qed |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
831 |
ultimately show ?thesis |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
832 |
by (simp add: emeasure_notin_sets) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
833 |
qed |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
834 |
qed |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
835 |
show ?m |
64272 | 836 |
unfolding measure_def \<open>?e\<close> by (simp add: enn2real_mult prod_nonneg) |
63958
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
837 |
qed |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
838 |
|
67135
1a94352812f4
Moved material from AFP to Analysis/Number_Theory
Manuel Eberl <eberlm@in.tum.de>
parents:
66164
diff
changeset
|
839 |
lemma lebesgue_real_scale: |
1a94352812f4
Moved material from AFP to Analysis/Number_Theory
Manuel Eberl <eberlm@in.tum.de>
parents:
66164
diff
changeset
|
840 |
assumes "c \<noteq> 0" |
1a94352812f4
Moved material from AFP to Analysis/Number_Theory
Manuel Eberl <eberlm@in.tum.de>
parents:
66164
diff
changeset
|
841 |
shows "lebesgue = density (distr lebesgue lebesgue (\<lambda>x. c * x)) (\<lambda>x. ennreal \<bar>c\<bar>)" |
1a94352812f4
Moved material from AFP to Analysis/Number_Theory
Manuel Eberl <eberlm@in.tum.de>
parents:
66164
diff
changeset
|
842 |
using assms by (subst lebesgue_affine_euclidean[of "\<lambda>_. c" 0]) simp_all |
1a94352812f4
Moved material from AFP to Analysis/Number_Theory
Manuel Eberl <eberlm@in.tum.de>
parents:
66164
diff
changeset
|
843 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
844 |
lemma divideR_right: |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
845 |
fixes x y :: "'a::real_normed_vector" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
846 |
shows "r \<noteq> 0 \<Longrightarrow> y = x /\<^sub>R r \<longleftrightarrow> r *\<^sub>R y = x" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
847 |
using scaleR_cancel_left[of r y "x /\<^sub>R r"] by simp |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
848 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
849 |
lemma lborel_has_bochner_integral_real_affine_iff: |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
850 |
fixes x :: "'a :: {banach, second_countable_topology}" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
851 |
shows "c \<noteq> 0 \<Longrightarrow> |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
852 |
has_bochner_integral lborel f x \<longleftrightarrow> |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
853 |
has_bochner_integral lborel (\<lambda>x. f (t + c * x)) (x /\<^sub>R \<bar>c\<bar>)" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
854 |
unfolding has_bochner_integral_iff lborel_integrable_real_affine_iff |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
855 |
by (simp_all add: lborel_integral_real_affine[symmetric] divideR_right cong: conj_cong) |
49777 | 856 |
|
59425 | 857 |
lemma lborel_distr_uminus: "distr lborel borel uminus = (lborel :: real measure)" |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
858 |
by (subst lborel_real_affine[of "-1" 0]) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
859 |
(auto simp: density_1 one_ennreal_def[symmetric]) |
59425 | 860 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
861 |
lemma lborel_distr_mult: |
59425 | 862 |
assumes "(c::real) \<noteq> 0" |
67399 | 863 |
shows "distr lborel borel (( * ) c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)" |
59425 | 864 |
proof- |
67399 | 865 |
have "distr lborel borel (( * ) c) = distr lborel lborel (( * ) c)" by (simp cong: distr_cong) |
59425 | 866 |
also from assms have "... = density lborel (\<lambda>_. inverse \<bar>c\<bar>)" |
867 |
by (subst lborel_real_affine[of "inverse c" 0]) (auto simp: o_def distr_density_distr) |
|
868 |
finally show ?thesis . |
|
869 |
qed |
|
870 |
||
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
871 |
lemma lborel_distr_mult': |
59425 | 872 |
assumes "(c::real) \<noteq> 0" |
67399 | 873 |
shows "lborel = density (distr lborel borel (( * ) c)) (\<lambda>_. \<bar>c\<bar>)" |
59425 | 874 |
proof- |
875 |
have "lborel = density lborel (\<lambda>_. 1)" by (rule density_1[symmetric]) |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
876 |
also from assms have "(\<lambda>_. 1 :: ennreal) = (\<lambda>_. inverse \<bar>c\<bar> * \<bar>c\<bar>)" by (intro ext) simp |
61945 | 877 |
also have "density lborel ... = density (density lborel (\<lambda>_. inverse \<bar>c\<bar>)) (\<lambda>_. \<bar>c\<bar>)" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
878 |
by (subst density_density_eq) (auto simp: ennreal_mult) |
67399 | 879 |
also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel (( * ) c)" |
59425 | 880 |
by (rule lborel_distr_mult[symmetric]) |
881 |
finally show ?thesis . |
|
882 |
qed |
|
883 |
||
67399 | 884 |
lemma lborel_distr_plus: "distr lborel borel ((+) c) = (lborel :: real measure)" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
885 |
by (subst lborel_real_affine[of 1 c]) (auto simp: density_1 one_ennreal_def[symmetric]) |
59425 | 886 |
|
61605 | 887 |
interpretation lborel: sigma_finite_measure lborel |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
888 |
by (rule sigma_finite_lborel) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
889 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
890 |
interpretation lborel_pair: pair_sigma_finite lborel lborel .. |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
891 |
|
59425 | 892 |
lemma lborel_prod: |
893 |
"lborel \<Otimes>\<^sub>M lborel = (lborel :: ('a::euclidean_space \<times> 'b::euclidean_space) measure)" |
|
894 |
proof (rule lborel_eqI[symmetric], clarify) |
|
895 |
fix la ua :: 'a and lb ub :: 'b |
|
896 |
assume lu: "\<And>a b. (a, b) \<in> Basis \<Longrightarrow> (la, lb) \<bullet> (a, b) \<le> (ua, ub) \<bullet> (a, b)" |
|
897 |
have [simp]: |
|
898 |
"\<And>b. b \<in> Basis \<Longrightarrow> la \<bullet> b \<le> ua \<bullet> b" |
|
899 |
"\<And>b. b \<in> Basis \<Longrightarrow> lb \<bullet> b \<le> ub \<bullet> b" |
|
900 |
"inj_on (\<lambda>u. (u, 0)) Basis" "inj_on (\<lambda>u. (0, u)) Basis" |
|
901 |
"(\<lambda>u. (u, 0)) ` Basis \<inter> (\<lambda>u. (0, u)) ` Basis = {}" |
|
902 |
"box (la, lb) (ua, ub) = box la ua \<times> box lb ub" |
|
903 |
using lu[of _ 0] lu[of 0] by (auto intro!: inj_onI simp add: Basis_prod_def ball_Un box_def) |
|
904 |
show "emeasure (lborel \<Otimes>\<^sub>M lborel) (box (la, lb) (ua, ub)) = |
|
67399 | 905 |
ennreal (prod ((\<bullet>) ((ua, ub) - (la, lb))) Basis)" |
64272 | 906 |
by (simp add: lborel.emeasure_pair_measure_Times Basis_prod_def prod.union_disjoint |
907 |
prod.reindex ennreal_mult inner_diff_left prod_nonneg) |
|
59425 | 908 |
qed (simp add: borel_prod[symmetric]) |
909 |
||
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
910 |
(* FIXME: conversion in measurable prover *) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
911 |
lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
912 |
lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
913 |
|
57138
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
914 |
lemma emeasure_bounded_finite: |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
915 |
assumes "bounded A" shows "emeasure lborel A < \<infinity>" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
916 |
proof - |
61808 | 917 |
from bounded_subset_cbox[OF \<open>bounded A\<close>] obtain a b where "A \<subseteq> cbox a b" |
57138
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
918 |
by auto |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
919 |
then have "emeasure lborel A \<le> emeasure lborel (cbox a b)" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
920 |
by (intro emeasure_mono) auto |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
921 |
then show ?thesis |
64272 | 922 |
by (auto simp: emeasure_lborel_cbox_eq prod_nonneg less_top[symmetric] top_unique split: if_split_asm) |
57138
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
923 |
qed |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
924 |
|
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
925 |
lemma emeasure_compact_finite: "compact A \<Longrightarrow> emeasure lborel A < \<infinity>" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
926 |
using emeasure_bounded_finite[of A] by (auto intro: compact_imp_bounded) |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
927 |
|
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
928 |
lemma borel_integrable_compact: |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
929 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}" |
57138
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
930 |
assumes "compact S" "continuous_on S f" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
931 |
shows "integrable lborel (\<lambda>x. indicator S x *\<^sub>R f x)" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
932 |
proof cases |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
933 |
assume "S \<noteq> {}" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
934 |
have "continuous_on S (\<lambda>x. norm (f x))" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
935 |
using assms by (intro continuous_intros) |
61808 | 936 |
from continuous_attains_sup[OF \<open>compact S\<close> \<open>S \<noteq> {}\<close> this] |
57138
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
937 |
obtain M where M: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> M" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
938 |
by auto |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
939 |
show ?thesis |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
940 |
proof (rule integrable_bound) |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
941 |
show "integrable lborel (\<lambda>x. indicator S x * M)" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
942 |
using assms by (auto intro!: emeasure_compact_finite borel_compact integrable_mult_left) |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
943 |
show "(\<lambda>x. indicator S x *\<^sub>R f x) \<in> borel_measurable lborel" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
944 |
using assms by (auto intro!: borel_measurable_continuous_on_indicator borel_compact) |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
945 |
show "AE x in lborel. norm (indicator S x *\<^sub>R f x) \<le> norm (indicator S x * M)" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
946 |
by (auto split: split_indicator simp: abs_real_def dest!: M) |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
947 |
qed |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
948 |
qed simp |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
949 |
|
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
950 |
lemma borel_integrable_atLeastAtMost: |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
951 |
fixes f :: "real \<Rightarrow> real" |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
952 |
assumes f: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x" |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
953 |
shows "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)" (is "integrable _ ?f") |
57138
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
954 |
proof - |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
955 |
have "integrable lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x)" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
956 |
proof (rule borel_integrable_compact) |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
957 |
from f show "continuous_on {a..b} f" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
958 |
by (auto intro: continuous_at_imp_continuous_on) |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
959 |
qed simp |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
960 |
then show ?thesis |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57447
diff
changeset
|
961 |
by (auto simp: mult.commute) |
57138
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
962 |
qed |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
963 |
|
67984 | 964 |
subsection\<open>Lebesgue measurable sets\<close> |
965 |
||
63958
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
966 |
abbreviation lmeasurable :: "'a::euclidean_space set set" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
967 |
where |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
968 |
"lmeasurable \<equiv> fmeasurable lebesgue" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
969 |
|
67982
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
970 |
lemma not_measurable_UNIV [simp]: "UNIV \<notin> lmeasurable" |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
971 |
by (simp add: fmeasurable_def) |
7643b005b29a
various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents:
67968
diff
changeset
|
972 |
|
63958
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
973 |
lemma lmeasurable_iff_integrable: |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
974 |
"S \<in> lmeasurable \<longleftrightarrow> integrable lebesgue (indicator S :: 'a::euclidean_space \<Rightarrow> real)" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
975 |
by (auto simp: fmeasurable_def integrable_iff_bounded borel_measurable_indicator_iff ennreal_indicator) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
976 |
|
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
977 |
lemma lmeasurable_cbox [iff]: "cbox a b \<in> lmeasurable" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
978 |
and lmeasurable_box [iff]: "box a b \<in> lmeasurable" |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
979 |
by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq) |
02de4a58e210
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
hoelzl
parents:
63918
diff
changeset
|
980 |
|
63959
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
981 |
lemma lmeasurable_compact: "compact S \<Longrightarrow> S \<in> lmeasurable" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
982 |
using emeasure_compact_finite[of S] by (intro fmeasurableI) (auto simp: borel_compact) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
983 |
|
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
984 |
lemma lmeasurable_open: "bounded S \<Longrightarrow> open S \<Longrightarrow> S \<in> lmeasurable" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
985 |
using emeasure_bounded_finite[of S] by (intro fmeasurableI) (auto simp: borel_open) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
986 |
|
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
987 |
lemma lmeasurable_ball: "ball a r \<in> lmeasurable" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
988 |
by (simp add: lmeasurable_open) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
989 |
|
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
990 |
lemma lmeasurable_interior: "bounded S \<Longrightarrow> interior S \<in> lmeasurable" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
991 |
by (simp add: bounded_interior lmeasurable_open) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
992 |
|
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
993 |
lemma null_sets_cbox_Diff_box: "cbox a b - box a b \<in> null_sets lborel" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
994 |
proof - |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
995 |
have "emeasure lborel (cbox a b - box a b) = 0" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
996 |
by (subst emeasure_Diff) (auto simp: emeasure_lborel_cbox_eq emeasure_lborel_box_eq box_subset_cbox) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
997 |
then have "cbox a b - box a b \<in> null_sets lborel" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
998 |
by (auto simp: null_sets_def) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
999 |
then show ?thesis |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1000 |
by (auto dest!: AE_not_in) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1001 |
qed |
67968 | 1002 |
|
67984 | 1003 |
lemma bounded_set_imp_lmeasurable: |
1004 |
assumes "bounded S" "S \<in> sets lebesgue" shows "S \<in> lmeasurable" |
|
1005 |
by (metis assms bounded_Un emeasure_bounded_finite emeasure_completion fmeasurableI main_part_null_part_Un) |
|
1006 |
||
67986
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1007 |
|
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1008 |
subsection\<open>Translation preserves Lebesgue measure\<close> |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1009 |
|
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1010 |
lemma sigma_sets_image: |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1011 |
assumes S: "S \<in> sigma_sets \<Omega> M" and "M \<subseteq> Pow \<Omega>" "f ` \<Omega> = \<Omega>" "inj_on f \<Omega>" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1012 |
and M: "\<And>y. y \<in> M \<Longrightarrow> f ` y \<in> M" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1013 |
shows "(f ` S) \<in> sigma_sets \<Omega> M" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1014 |
using S |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1015 |
proof (induct S rule: sigma_sets.induct) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1016 |
case (Basic a) then show ?case |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1017 |
by (simp add: M) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1018 |
next |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1019 |
case Empty then show ?case |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1020 |
by (simp add: sigma_sets.Empty) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1021 |
next |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1022 |
case (Compl a) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1023 |
then have "\<Omega> - a \<subseteq> \<Omega>" "a \<subseteq> \<Omega>" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1024 |
by (auto simp: sigma_sets_into_sp [OF \<open>M \<subseteq> Pow \<Omega>\<close>]) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1025 |
then show ?case |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1026 |
by (auto simp: inj_on_image_set_diff [OF \<open>inj_on f \<Omega>\<close>] assms intro: Compl sigma_sets.Compl) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1027 |
next |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1028 |
case (Union a) then show ?case |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1029 |
by (metis image_UN sigma_sets.simps) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1030 |
qed |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1031 |
|
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1032 |
lemma null_sets_translation: |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1033 |
assumes "N \<in> null_sets lborel" shows "{x. x - a \<in> N} \<in> null_sets lborel" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1034 |
proof - |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1035 |
have [simp]: "(\<lambda>x. x + a) ` N = {x. x - a \<in> N}" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1036 |
by force |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1037 |
show ?thesis |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1038 |
using assms emeasure_lebesgue_affine [of 1 a N] by (auto simp: null_sets_def) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1039 |
qed |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1040 |
|
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1041 |
lemma lebesgue_sets_translation: |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1042 |
fixes f :: "'a \<Rightarrow> 'a::euclidean_space" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1043 |
assumes S: "S \<in> sets lebesgue" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1044 |
shows "((\<lambda>x. a + x) ` S) \<in> sets lebesgue" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1045 |
proof - |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1046 |
have im_eq: "(+) a ` A = {x. x - a \<in> A}" for A |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1047 |
by force |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1048 |
have "((\<lambda>x. a + x) ` S) = ((\<lambda>x. -a + x) -` S) \<inter> (space lebesgue)" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1049 |
using image_iff by fastforce |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1050 |
also have "\<dots> \<in> sets lebesgue" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1051 |
proof (rule measurable_sets [OF measurableI assms]) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1052 |
fix A :: "'b set" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1053 |
assume A: "A \<in> sets lebesgue" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1054 |
have vim_eq: "(\<lambda>x. x - a) -` A = (+) a ` A" for A |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1055 |
by force |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1056 |
have "\<exists>s n N'. (+) a ` (S \<union> N) = s \<union> n \<and> s \<in> sets borel \<and> N' \<in> null_sets lborel \<and> n \<subseteq> N'" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1057 |
if "S \<in> sets borel" and "N' \<in> null_sets lborel" and "N \<subseteq> N'" for S N N' |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1058 |
proof (intro exI conjI) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1059 |
show "(+) a ` (S \<union> N) = (\<lambda>x. a + x) ` S \<union> (\<lambda>x. a + x) ` N" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1060 |
by auto |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1061 |
show "(\<lambda>x. a + x) ` N' \<in> null_sets lborel" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1062 |
using that by (auto simp: null_sets_translation im_eq) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1063 |
qed (use that im_eq in auto) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1064 |
with A have "(\<lambda>x. x - a) -` A \<in> sets lebesgue" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1065 |
by (force simp: vim_eq completion_def intro!: sigma_sets_image) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1066 |
then show "(+) (- a) -` A \<inter> space lebesgue \<in> sets lebesgue" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1067 |
by (auto simp: vimage_def im_eq) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1068 |
qed auto |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1069 |
finally show ?thesis . |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1070 |
qed |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1071 |
|
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1072 |
lemma measurable_translation: |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1073 |
"S \<in> lmeasurable \<Longrightarrow> ((\<lambda>x. a + x) ` S) \<in> lmeasurable" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1074 |
unfolding fmeasurable_def |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1075 |
apply (auto intro: lebesgue_sets_translation) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1076 |
using emeasure_lebesgue_affine [of 1 a S] |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1077 |
by (auto simp: add.commute [of _ a]) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1078 |
|
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1079 |
lemma measure_translation: |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1080 |
"measure lebesgue ((\<lambda>x. a + x) ` S) = measure lebesgue S" |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1081 |
using measure_lebesgue_affine [of 1 a S] |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1082 |
by (auto simp: add.commute [of _ a]) |
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
67984
diff
changeset
|
1083 |
|
67968 | 1084 |
subsection \<open>A nice lemma for negligibility proofs\<close> |
63959
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1085 |
|
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1086 |
lemma summable_iff_suminf_neq_top: "(\<And>n. f n \<ge> 0) \<Longrightarrow> \<not> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = top" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1087 |
by (metis summable_suminf_not_top) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1088 |
|
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1089 |
proposition starlike_negligible_bounded_gmeasurable: |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1090 |
fixes S :: "'a :: euclidean_space set" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1091 |
assumes S: "S \<in> sets lebesgue" and "bounded S" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1092 |
and eq1: "\<And>c x. \<lbrakk>(c *\<^sub>R x) \<in> S; 0 \<le> c; x \<in> S\<rbrakk> \<Longrightarrow> c = 1" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1093 |
shows "S \<in> null_sets lebesgue" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1094 |
proof - |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1095 |
obtain M where "0 < M" "S \<subseteq> ball 0 M" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1096 |
using \<open>bounded S\<close> by (auto dest: bounded_subset_ballD) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1097 |
|
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1098 |
let ?f = "\<lambda>n. root DIM('a) (Suc n)" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1099 |
|
67399 | 1100 |
have vimage_eq_image: "( *\<^sub>R) (?f n) -` S = ( *\<^sub>R) (1 / ?f n) ` S" for n |
63959
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1101 |
apply safe |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1102 |
subgoal for x by (rule image_eqI[of _ _ "?f n *\<^sub>R x"]) auto |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1103 |
subgoal by auto |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1104 |
done |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1105 |
|
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1106 |
have eq: "(1 / ?f n) ^ DIM('a) = 1 / Suc n" for n |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1107 |
by (simp add: field_simps) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1108 |
|
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1109 |
{ fix n x assume x: "root DIM('a) (1 + real n) *\<^sub>R x \<in> S" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1110 |
have "1 * norm x \<le> root DIM('a) (1 + real n) * norm x" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1111 |
by (rule mult_mono) auto |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1112 |
also have "\<dots> < M" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1113 |
using x \<open>S \<subseteq> ball 0 M\<close> by auto |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1114 |
finally have "norm x < M" by simp } |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1115 |
note less_M = this |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1116 |
|
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1117 |
have "(\<Sum>n. ennreal (1 / Suc n)) = top" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1118 |
using not_summable_harmonic[where 'a=real] summable_Suc_iff[where f="\<lambda>n. 1 / (real n)"] |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1119 |
by (intro summable_iff_suminf_neq_top) (auto simp add: inverse_eq_divide) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1120 |
then have "top * emeasure lebesgue S = (\<Sum>n. (1 / ?f n)^DIM('a) * emeasure lebesgue S)" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1121 |
unfolding ennreal_suminf_multc eq by simp |
67399 | 1122 |
also have "\<dots> = (\<Sum>n. emeasure lebesgue (( *\<^sub>R) (?f n) -` S))" |
63959
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1123 |
unfolding vimage_eq_image using emeasure_lebesgue_affine[of "1 / ?f n" 0 S for n] by simp |
67399 | 1124 |
also have "\<dots> = emeasure lebesgue (\<Union>n. ( *\<^sub>R) (?f n) -` S)" |
63959
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1125 |
proof (intro suminf_emeasure) |
67399 | 1126 |
show "disjoint_family (\<lambda>n. ( *\<^sub>R) (?f n) -` S)" |
63959
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1127 |
unfolding disjoint_family_on_def |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1128 |
proof safe |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1129 |
fix m n :: nat and x assume "m \<noteq> n" "?f m *\<^sub>R x \<in> S" "?f n *\<^sub>R x \<in> S" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1130 |
with eq1[of "?f m / ?f n" "?f n *\<^sub>R x"] show "x \<in> {}" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1131 |
by auto |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1132 |
qed |
67399 | 1133 |
have "( *\<^sub>R) (?f i) -` S \<in> sets lebesgue" for i |
63959
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1134 |
using measurable_sets[OF lebesgue_measurable_scaling[of "?f i"] S] by auto |
67399 | 1135 |
then show "range (\<lambda>i. ( *\<^sub>R) (?f i) -` S) \<subseteq> sets lebesgue" |
63959
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1136 |
by auto |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1137 |
qed |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1138 |
also have "\<dots> \<le> emeasure lebesgue (ball 0 M :: 'a set)" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1139 |
using less_M by (intro emeasure_mono) auto |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1140 |
also have "\<dots> < top" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1141 |
using lmeasurable_ball by (auto simp: fmeasurable_def) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1142 |
finally have "emeasure lebesgue S = 0" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1143 |
by (simp add: ennreal_top_mult split: if_split_asm) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1144 |
then show "S \<in> null_sets lebesgue" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1145 |
unfolding null_sets_def using \<open>S \<in> sets lebesgue\<close> by auto |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1146 |
qed |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1147 |
|
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1148 |
corollary starlike_negligible_compact: |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1149 |
"compact S \<Longrightarrow> (\<And>c x. \<lbrakk>(c *\<^sub>R x) \<in> S; 0 \<le> c; x \<in> S\<rbrakk> \<Longrightarrow> c = 1) \<Longrightarrow> S \<in> null_sets lebesgue" |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1150 |
using starlike_negligible_bounded_gmeasurable[of S] by (auto simp: compact_eq_bounded_closed) |
f77dca1abf1b
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63958
diff
changeset
|
1151 |
|
63968
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1152 |
lemma outer_regular_lborel: |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1153 |
assumes B: "B \<in> fmeasurable lborel" "0 < (e::real)" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1154 |
shows "\<exists>U. open U \<and> B \<subseteq> U \<and> emeasure lborel U \<le> emeasure lborel B + e" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1155 |
proof - |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1156 |
let ?\<mu> = "emeasure lborel" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1157 |
let ?B = "\<lambda>n::nat. ball 0 n :: 'a set" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1158 |
have B[measurable]: "B \<in> sets borel" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1159 |
using B by auto |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1160 |
let ?e = "\<lambda>n. e*((1/2)^Suc n)" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1161 |
have "\<forall>n. \<exists>U. open U \<and> ?B n \<inter> B \<subseteq> U \<and> ?\<mu> (U - B) < ?e n" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1162 |
proof |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1163 |
fix n :: nat |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1164 |
let ?A = "density lborel (indicator (?B n))" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1165 |
have emeasure_A: "X \<in> sets borel \<Longrightarrow> emeasure ?A X = ?\<mu> (?B n \<inter> X)" for X |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1166 |
by (auto simp add: emeasure_density borel_measurable_indicator indicator_inter_arith[symmetric]) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1167 |
|
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1168 |
have finite_A: "emeasure ?A (space ?A) \<noteq> \<infinity>" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1169 |
using emeasure_bounded_finite[of "?B n"] by (auto simp add: emeasure_A) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1170 |
interpret A: finite_measure ?A |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1171 |
by rule fact |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1172 |
have "emeasure ?A B + ?e n > (INF U:{U. B \<subseteq> U \<and> open U}. emeasure ?A U)" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1173 |
using \<open>0<e\<close> by (auto simp: outer_regular[OF _ finite_A B, symmetric]) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1174 |
then obtain U where U: "B \<subseteq> U" "open U" "?\<mu> (?B n \<inter> B) + ?e n > ?\<mu> (?B n \<inter> U)" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1175 |
unfolding INF_less_iff by (auto simp: emeasure_A) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1176 |
moreover |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1177 |
{ have "?\<mu> ((?B n \<inter> U) - B) = ?\<mu> ((?B n \<inter> U) - (?B n \<inter> B))" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1178 |
using U by (intro arg_cong[where f="?\<mu>"]) auto |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1179 |
also have "\<dots> = ?\<mu> (?B n \<inter> U) - ?\<mu> (?B n \<inter> B)" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1180 |
using U A.emeasure_finite[of B] |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1181 |
by (intro emeasure_Diff) (auto simp del: A.emeasure_finite simp: emeasure_A) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1182 |
also have "\<dots> < ?e n" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1183 |
using U(1,2,3) A.emeasure_finite[of B] |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1184 |
by (subst minus_less_iff_ennreal) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1185 |
(auto simp del: A.emeasure_finite simp: emeasure_A less_top ac_simps intro!: emeasure_mono) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1186 |
finally have "?\<mu> ((?B n \<inter> U) - B) < ?e n" . } |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1187 |
ultimately show "\<exists>U. open U \<and> ?B n \<inter> B \<subseteq> U \<and> ?\<mu> (U - B) < ?e n" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1188 |
by (intro exI[of _ "?B n \<inter> U"]) auto |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1189 |
qed |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1190 |
then obtain U |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1191 |
where U: "\<And>n. open (U n)" "\<And>n. ?B n \<inter> B \<subseteq> U n" "\<And>n. ?\<mu> (U n - B) < ?e n" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1192 |
by metis |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1193 |
then show ?thesis |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1194 |
proof (intro exI conjI) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1195 |
{ fix x assume "x \<in> B" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1196 |
moreover |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1197 |
have "\<exists>n. norm x < real n" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1198 |
by (simp add: reals_Archimedean2) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1199 |
then guess n .. |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1200 |
ultimately have "x \<in> (\<Union>n. U n)" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1201 |
using U(2)[of n] by auto } |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1202 |
note * = this |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1203 |
then show "open (\<Union>n. U n)" "B \<subseteq> (\<Union>n. U n)" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1204 |
using U(1,2) by auto |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1205 |
have "?\<mu> (\<Union>n. U n) = ?\<mu> (B \<union> (\<Union>n. U n - B))" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1206 |
using * U(2) by (intro arg_cong[where ?f="?\<mu>"]) auto |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1207 |
also have "\<dots> = ?\<mu> B + ?\<mu> (\<Union>n. U n - B)" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1208 |
using U(1) by (intro plus_emeasure[symmetric]) auto |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1209 |
also have "\<dots> \<le> ?\<mu> B + (\<Sum>n. ?\<mu> (U n - B))" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1210 |
using U(1) by (intro add_mono emeasure_subadditive_countably) auto |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1211 |
also have "\<dots> \<le> ?\<mu> B + (\<Sum>n. ennreal (?e n))" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1212 |
using U(3) by (intro add_mono suminf_le) (auto intro: less_imp_le) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1213 |
also have "(\<Sum>n. ennreal (?e n)) = ennreal (e * 1)" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1214 |
using \<open>0<e\<close> by (intro suminf_ennreal_eq sums_mult power_half_series) auto |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1215 |
finally show "emeasure lborel (\<Union>n. U n) \<le> emeasure lborel B + ennreal e" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1216 |
by simp |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1217 |
qed |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1218 |
qed |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1219 |
|
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1220 |
lemma lmeasurable_outer_open: |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1221 |
assumes S: "S \<in> lmeasurable" and "0 < e" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1222 |
obtains T where "open T" "S \<subseteq> T" "T \<in> lmeasurable" "measure lebesgue T \<le> measure lebesgue S + e" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1223 |
proof - |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1224 |
obtain S' where S': "S \<subseteq> S'" "S' \<in> sets borel" "emeasure lborel S' = emeasure lebesgue S" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1225 |
using completion_upper[of S lborel] S by auto |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1226 |
then have f_S': "S' \<in> fmeasurable lborel" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1227 |
using S by (auto simp: fmeasurable_def) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1228 |
from outer_regular_lborel[OF this \<open>0<e\<close>] guess U .. note U = this |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1229 |
show thesis |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1230 |
proof (rule that) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1231 |
show "open U" "S \<subseteq> U" "U \<in> lmeasurable" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1232 |
using f_S' U S' by (auto simp: fmeasurable_def less_top[symmetric] top_unique) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1233 |
then have "U \<in> fmeasurable lborel" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1234 |
by (auto simp: fmeasurable_def) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1235 |
with S U \<open>0<e\<close> show "measure lebesgue U \<le> measure lebesgue S + e" |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1236 |
unfolding S'(3) by (simp add: emeasure_eq_measure2 ennreal_plus[symmetric] del: ennreal_plus) |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1237 |
qed |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1238 |
qed |
4359400adfe7
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
hoelzl
parents:
63959
diff
changeset
|
1239 |
|
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
1240 |
lemma lebesgue_openin: |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
1241 |
"\<lbrakk>openin (subtopology euclidean S) T; S \<in> sets lebesgue\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue" |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
1242 |
by (metis borel_open openin_open sets.Int sets_completionI_sets sets_lborel) |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
1243 |
|
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
1244 |
lemma lebesgue_closedin: |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
1245 |
"\<lbrakk>closedin (subtopology euclidean S) T; S \<in> sets lebesgue\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue" |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
1246 |
by (metis borel_closed closedin_closed sets.Int sets_completionI_sets sets_lborel) |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
1247 |
|
38656 | 1248 |
end |