author | hoelzl |
Mon, 08 Aug 2016 14:13:14 +0200 | |
changeset 63627 | 6ddb43c6b711 |
parent 63626 | src/HOL/Multivariate_Analysis/Lebesgue_Measure.thy@44ce6b524ff3 |
child 63886 | 685fb01256af |
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 |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
11 |
imports Finite_Product_Measure Bochner_Integration Caratheodory |
38656 | 12 |
begin |
13 |
||
61808 | 14 |
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
|
15 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
16 |
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
|
17 |
"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 | 18 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
19 |
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
|
20 |
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
|
21 |
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
|
22 |
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
|
23 |
shows "emeasure (interval_measure F) {a <.. b} = F b - F a" |
61808 | 24 |
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
|
25 |
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
|
26 |
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
|
27 |
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
|
28 |
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
|
29 |
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
|
30 |
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
|
31 |
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
|
32 |
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
|
33 |
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
|
34 |
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
|
35 |
next |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
36 |
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
|
37 |
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
|
38 |
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
|
39 |
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
|
40 |
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
|
41 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
42 |
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
|
43 |
next |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
44 |
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
|
45 |
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
|
46 |
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
|
47 |
|
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
|
48 |
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
|
49 |
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
|
50 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
51 |
{ fix S :: "nat set" assume "finite S" |
61808 | 52 |
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
|
53 |
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
|
54 |
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
|
55 |
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
|
56 |
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
|
57 |
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
|
58 |
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
|
59 |
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
|
60 |
assume "\<exists>i\<in>S. l i < r i" |
61808 | 61 |
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
|
62 |
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
|
63 |
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
|
64 |
by fastforce |
50104 | 65 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
66 |
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))" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
67 |
using m psubset by (intro setsum.remove) auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
68 |
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
|
69 |
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
|
70 |
show "S - {m} \<subset> S" |
61808 | 71 |
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
|
72 |
show "r m \<le> b" |
61808 | 73 |
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
|
74 |
next |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
75 |
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
|
76 |
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
|
77 |
{ assume i': "l i < r i" "l i < r m" |
63540 | 78 |
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
|
79 |
by auto |
63540 | 80 |
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
|
81 |
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
|
82 |
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
|
83 |
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
|
84 |
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
|
85 |
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
|
86 |
then show "{l i <.. r i} \<subseteq> {r m <.. b}" |
61808 | 87 |
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
|
88 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
89 |
also have "F (r m) - F (l m) \<le> F (r m) - F a" |
61808 | 90 |
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
|
91 |
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
|
92 |
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
|
93 |
by (auto intro: add_mono) |
61808 | 94 |
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
|
95 |
qed } |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
96 |
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
|
97 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
98 |
(* 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
|
99 |
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
|
100 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
101 |
{ 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
|
102 |
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
|
103 |
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
|
104 |
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
|
105 |
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
|
106 |
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
|
107 |
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
|
108 |
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
|
109 |
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
|
110 |
next |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
111 |
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
|
112 |
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
|
113 |
by auto |
47694 | 114 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
115 |
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
|
116 |
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
|
117 |
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
|
118 |
assume "?R" |
61808 | 119 |
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
|
120 |
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
|
121 |
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
|
122 |
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
|
123 |
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
|
124 |
done |
61808 | 125 |
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
|
126 |
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
|
127 |
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
|
128 |
using psubset.prems |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
129 |
by (intro setsum_mono2 psubset) (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
|
130 |
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
|
131 |
next |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
132 |
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
|
133 |
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
|
134 |
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
|
135 |
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
|
136 |
let ?S2 = "{i \<in> S. r i > r j}" |
40859 | 137 |
|
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 |
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 | 139 |
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
|
140 |
by (intro setsum_mono2) (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
|
141 |
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
|
142 |
(\<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
|
143 |
using psubset(1) psubset.prems(1) j |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
144 |
apply (subst setsum.union_disjoint) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
145 |
apply simp_all |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
146 |
apply (subst setsum.union_disjoint) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
147 |
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
|
148 |
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
|
149 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
150 |
also (xtrans) have "(\<Sum>i\<in>?S1. F (r i) - F (l i)) \<ge> F (l j) - F u" |
61808 | 151 |
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
|
152 |
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
|
153 |
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
|
154 |
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
|
155 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
156 |
also (xtrans) have "(\<Sum>i\<in>?S2. F (r i) - F (l i)) \<ge> F v - F (r j)" |
61808 | 157 |
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
|
158 |
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
|
159 |
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
|
160 |
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
|
161 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
162 |
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
|
163 |
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
|
164 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
165 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
166 |
qed } |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
167 |
note claim2 = this |
49777 | 168 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
169 |
(* 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
|
170 |
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
|
171 |
proof (rule ennreal_le_epsilon) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
172 |
fix epsilon :: real assume egt0: "epsilon > 0" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
173 |
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
|
174 |
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
|
175 |
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
|
176 |
note right_cont_F [of "r i"] |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
177 |
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
|
178 |
apply - |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
179 |
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
|
180 |
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
|
181 |
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
|
182 |
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
|
183 |
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
|
184 |
qed |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
185 |
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
|
186 |
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
|
187 |
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
|
188 |
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
|
189 |
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
|
190 |
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
|
191 |
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
|
192 |
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
|
193 |
apply (drule_tac x = "epsilon / 2" in spec) |
59554
4044f53326c9
inlined rules to free user-space from technical names
haftmann
parents:
59425
diff
changeset
|
194 |
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
|
195 |
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
|
196 |
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
|
197 |
by auto |
63040 | 198 |
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
|
199 |
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
|
200 |
"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
|
201 |
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
|
202 |
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
|
203 |
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
|
204 |
by (rule compact_Icc) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
205 |
show "\<forall>i \<in> S'. open ({l i<..<r i + delta 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
|
206 |
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
|
207 |
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
|
208 |
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
|
209 |
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
|
210 |
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
|
211 |
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
|
212 |
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
|
213 |
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
|
214 |
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
|
215 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
216 |
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
|
217 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
218 |
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
|
219 |
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
|
220 |
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
|
221 |
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
|
222 |
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
|
223 |
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
|
224 |
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
|
225 |
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
|
226 |
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
|
227 |
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
|
228 |
by (rule deltai_gt0) |
61954 | 229 |
also have "... \<le> (\<Sum>i \<in> S. F(r i) - F(l 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
|
230 |
apply (rule setsum_mono) |
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 simp |
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 (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
|
233 |
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
|
234 |
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
|
235 |
by auto |
61954 | 236 |
also have "... = (\<Sum>i \<in> S. F(r i) - F(l i)) + |
237 |
(epsilon / 4) * (\<Sum>i \<in> S. (1 / 2)^i)" (is "_ = ?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
|
238 |
by (subst setsum.distrib) (simp add: field_simps setsum_right_distrib) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
239 |
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
|
240 |
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
|
241 |
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
|
242 |
apply (rule setsum_mono2) |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
243 |
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
|
244 |
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
|
245 |
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
|
246 |
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
|
247 |
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
|
248 |
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
|
249 |
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
|
250 |
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
|
251 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
252 |
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
|
253 |
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
|
254 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
255 |
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
|
256 |
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
|
257 |
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
|
258 |
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
|
259 |
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
|
260 |
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
|
261 |
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
|
262 |
done |
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 "... = (\<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
|
264 |
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
|
265 |
also have "... \<le> (\<Sum>i\<le>n. 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
|
266 |
using finS Sbound Sprop by (auto intro!: add_right_mono setsum_mono3) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
267 |
finally have "ennreal (F b - F a) \<le> (\<Sum>i\<le>n. ennreal (F (r i) - F (l i))) + epsilon" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
268 |
using egt0 by (simp add: ennreal_plus[symmetric] setsum_nonneg del: ennreal_plus) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
269 |
then show "ennreal (F b - F a) \<le> (\<Sum>i. ennreal (F (r i) - F (l i))) + (epsilon :: real)" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
270 |
by (rule order_trans) (auto intro!: add_mono setsum_le_suminf simp del: setsum_ennreal) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
271 |
qed |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
272 |
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
|
273 |
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
|
274 |
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
|
275 |
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
|
276 |
qed (auto simp: Ioc_inj mono_F) |
38656 | 277 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
278 |
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
|
279 |
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
|
280 |
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
|
281 |
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
|
282 |
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
|
283 |
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
|
284 |
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
|
285 |
apply fact+ |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
286 |
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
|
287 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
288 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
289 |
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
|
290 |
"(\<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
|
291 |
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
|
292 |
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
|
293 |
|
59048 | 294 |
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
|
295 |
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
|
296 |
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
|
297 |
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
|
298 |
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
|
299 |
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
|
300 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
301 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
302 |
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
|
303 |
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
|
304 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
305 |
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
|
306 |
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
|
307 |
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
|
308 |
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
|
309 |
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
|
310 |
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
|
311 |
{ 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
|
312 |
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
|
313 |
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
|
314 |
(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
|
315 |
note * = this |
38656 | 316 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
317 |
let ?F = "interval_measure F" |
61973 | 318 |
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
|
319 |
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
|
320 |
show "a - 1 < a" by simp |
61969 | 321 |
fix X assume "\<And>n. X n < a" "incseq X" "X \<longlonglongrightarrow> a" |
322 |
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
|
323 |
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
|
324 |
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
|
325 |
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
|
326 |
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
|
327 |
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
|
328 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
329 |
also have "(\<Inter>n. {X n <..b}) = {a..b}" |
61808 | 330 |
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
|
331 |
apply auto |
61969 | 332 |
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
|
333 |
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
|
334 |
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
|
335 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
336 |
also have "(\<lambda>n. emeasure ?F {X n<..b}) = (\<lambda>n. F b - F (X n))" |
61808 | 337 |
using \<open>\<And>n. X n < a\<close> \<open>a \<le> b\<close> by (subst *) (auto intro: less_imp_le less_le_trans) |
61969 | 338 |
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
|
339 |
qed |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
340 |
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
|
341 |
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
|
342 |
(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
|
343 |
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
|
344 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
345 |
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
|
346 |
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
|
347 |
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
|
348 |
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
|
349 |
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
|
350 |
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
|
351 |
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
|
352 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
353 |
|
61808 | 354 |
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
|
355 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
356 |
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
|
357 |
"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
|
358 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
359 |
lemma |
59048 | 360 |
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
|
361 |
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
|
362 |
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
|
363 |
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
|
364 |
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
|
365 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
366 |
context |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
367 |
begin |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
368 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
369 |
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
|
370 |
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
|
371 |
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
|
372 |
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
|
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 |
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
|
375 |
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
|
376 |
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
|
377 |
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
|
378 |
(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
|
379 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
380 |
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
|
381 |
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
|
382 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
383 |
lemma nn_integral_lborel_setprod: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
384 |
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
|
385 |
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
|
386 |
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))" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
387 |
by (simp add: lborel_def nn_integral_distr product_nn_integral_setprod |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
388 |
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
|
389 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
390 |
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
|
391 |
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
|
392 |
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
|
393 |
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
|
394 |
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
|
395 |
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
|
396 |
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
|
397 |
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
|
398 |
by (simp add: lborel_def emeasure_distr emeasure_PiM emeasure_interval_measure_Icc continuous_on_id) |
50104 | 399 |
qed |
400 |
||
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
401 |
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
|
402 |
by simp |
47694 | 403 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
404 |
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
|
405 |
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
|
406 |
shows "emeasure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
41654 | 407 |
proof - |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
408 |
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
|
409 |
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
|
410 |
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
|
411 |
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
|
412 |
also have "\<dots> = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
413 |
by (subst nn_integral_lborel_setprod) (simp_all add: setprod_ennreal inner_diff_left) |
47694 | 414 |
finally show ?thesis . |
38656 | 415 |
qed |
416 |
||
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
417 |
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
|
418 |
using SOME_Basis AE_discrete_difference [of "{c}" lborel] emeasure_lborel_cbox [of c c] |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
419 |
by (auto simp add: cbox_sing setprod_constant power_0_left) |
47757
5e6fe71e2390
equate positive Lebesgue integral and MV-Analysis' Gauge integral
hoelzl
parents:
47694
diff
changeset
|
420 |
|
57447
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 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
|
422 |
assumes [simp]: "l \<le> u" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
423 |
shows "emeasure lborel {l <..< u} = ennreal (u - l)" |
40859 | 424 |
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
|
425 |
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
|
426 |
using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto |
47694 | 427 |
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
|
428 |
by simp |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
429 |
qed |
38656 | 430 |
|
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 |
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
|
432 |
assumes [simp]: "l \<le> u" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
433 |
shows "emeasure lborel {l <.. u} = ennreal (u - l)" |
41654 | 434 |
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
|
435 |
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
|
436 |
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
|
437 |
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
|
438 |
by simp |
38656 | 439 |
qed |
440 |
||
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
441 |
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
|
442 |
assumes [simp]: "l \<le> u" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
443 |
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
|
444 |
proof - |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
445 |
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
|
446 |
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
|
447 |
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
|
448 |
by simp |
38656 | 449 |
qed |
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_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
|
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 (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
|
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 (box 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 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
|
457 |
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
|
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)" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
460 |
by (subst nn_integral_lborel_setprod) (simp_all add: setprod_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
|
461 |
finally show ?thesis . |
40859 | 462 |
qed |
38656 | 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 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
|
465 |
"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
|
466 |
using box_eq_empty(2)[THEN iffD2, of u l] by (auto simp: not_le) |
41654 | 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_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
|
469 |
"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
|
470 |
using box_eq_empty(1)[THEN iffD2, of u l] by (auto simp: not_le dest!: less_imp_le) force |
40859 | 471 |
|
472 |
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
|
473 |
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
|
474 |
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
|
475 |
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
|
476 |
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
|
477 |
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
|
478 |
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
|
479 |
by (simp_all add: measure_def) |
40859 | 480 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
481 |
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
|
482 |
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
|
483 |
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
|
484 |
and measure_lborel_cbox[simp]: "measure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
485 |
by (simp_all add: measure_def inner_diff_left setprod_nonneg) |
41654 | 486 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
487 |
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
|
488 |
proof |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
489 |
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
|
490 |
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
|
491 |
(auto simp: emeasure_lborel_cbox_eq UN_box_eq_UNIV) |
49777 | 492 |
qed |
40859 | 493 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
494 |
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
|
495 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
496 |
lemma emeasure_lborel_UNIV: "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
|
497 |
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
|
498 |
{ 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
|
499 |
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
|
500 |
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
|
501 |
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
|
502 |
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
|
503 |
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
|
504 |
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
|
505 |
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
|
506 |
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
|
507 |
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
|
508 |
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
|
509 |
} 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
|
510 |
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
|
511 |
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
|
512 |
apply (subst SUP_emeasure_incseq[symmetric]) |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
513 |
apply (auto simp: incseq_def subset_box inner_add_left setprod_constant |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
514 |
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
|
515 |
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
|
516 |
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
|
517 |
qed |
40859 | 518 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
519 |
lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
520 |
using emeasure_lborel_cbox[of x x] nonempty_Basis |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
521 |
by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: cbox_sing setprod_constant) |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
522 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
523 |
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
|
524 |
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
|
525 |
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
|
526 |
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
|
527 |
proof - |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
528 |
have "A \<subseteq> (\<Union>i. {from_nat_into A i})" using from_nat_into_surj assms by force |
63262 | 529 |
then have "emeasure lborel A \<le> emeasure lborel (\<Union>i. {from_nat_into A i})" |
530 |
by (intro emeasure_mono) auto |
|
531 |
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
|
532 |
by (rule emeasure_UN_eq_0) auto |
63262 | 533 |
finally show ?thesis |
534 |
by (auto simp add: ) |
|
40859 | 535 |
qed |
536 |
||
59425 | 537 |
lemma countable_imp_null_set_lborel: "countable A \<Longrightarrow> A \<in> null_sets lborel" |
538 |
by (simp add: null_sets_def emeasure_lborel_countable sets.countable) |
|
539 |
||
540 |
lemma finite_imp_null_set_lborel: "finite A \<Longrightarrow> A \<in> null_sets lborel" |
|
541 |
by (intro countable_imp_null_set_lborel countable_finite) |
|
542 |
||
543 |
lemma lborel_neq_count_space[simp]: "lborel \<noteq> count_space (A::('a::ordered_euclidean_space) set)" |
|
544 |
proof |
|
545 |
assume asm: "lborel = count_space A" |
|
546 |
have "space lborel = UNIV" by simp |
|
547 |
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
|
548 |
have "emeasure lborel {undefined::'a} = 1" |
59425 | 549 |
by (subst asm, subst emeasure_count_space_finite) auto |
550 |
moreover have "emeasure lborel {undefined} \<noteq> 1" by simp |
|
551 |
ultimately show False by contradiction |
|
552 |
qed |
|
553 |
||
61808 | 554 |
subsection \<open>Affine transformation on the Lebesgue-Borel\<close> |
49777 | 555 |
|
556 |
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
|
557 |
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
|
558 |
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 | 559 |
assumes sets_eq: "sets M = sets borel" |
560 |
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
|
561 |
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
|
562 |
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
|
563 |
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
|
564 |
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
|
565 |
|
49777 | 566 |
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
|
567 |
by (simp_all add: borel_eq_box sets_eq) |
49777 | 568 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
569 |
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
|
570 |
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
|
571 |
unfolding UN_box_eq_UNIV by auto |
49777 | 572 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
573 |
{ fix i show "emeasure lborel (?A i) \<noteq> \<infinity>" by auto } |
49777 | 574 |
{ fix X assume "X \<in> ?E" then show "emeasure lborel X = emeasure M X" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
575 |
apply (auto simp: emeasure_eq 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
|
576 |
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
|
577 |
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
|
578 |
done } |
49777 | 579 |
qed |
580 |
||
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
581 |
lemma lborel_affine: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
582 |
fixes t :: "'a::euclidean_space" assumes "c \<noteq> 0" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
583 |
shows "lborel = density (distr lborel borel (\<lambda>x. t + c *\<^sub>R x)) (\<lambda>_. \<bar>c\<bar>^DIM('a))" (is "_ = ?D") |
49777 | 584 |
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
|
585 |
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
|
586 |
fix l u assume le: "\<And>b. b \<in> ?B \<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
|
587 |
show "emeasure ?D (box l u) = (\<Prod>b\<in>?B. (u - l) \<bullet> b)" |
49777 | 588 |
proof cases |
589 |
assume "0 < 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
|
590 |
then have "(\<lambda>x. t + c *\<^sub>R x) -` box l u = box ((l - t) /\<^sub>R c) ((u - t) /\<^sub>R c)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
591 |
by (auto simp: field_simps box_def inner_simps) |
61808 | 592 |
with \<open>0 < c\<close> 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
|
593 |
using le |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
594 |
by (auto simp: field_simps inner_simps setprod_dividef setprod_constant setprod_nonneg |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
595 |
ennreal_mult[symmetric] emeasure_density nn_integral_distr emeasure_distr |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
596 |
nn_integral_cmult emeasure_lborel_box_eq borel_measurable_indicator') |
49777 | 597 |
next |
61808 | 598 |
assume "\<not> 0 < c" with \<open>c \<noteq> 0\<close> have "c < 0" 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
|
599 |
then have "box ((u - t) /\<^sub>R c) ((l - t) /\<^sub>R c) = (\<lambda>x. t + c *\<^sub>R x) -` box 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
|
600 |
by (auto simp: field_simps box_def inner_simps) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
601 |
then have *: "\<And>x. indicator (box l u) (t + c *\<^sub>R x) = (indicator (box ((u - t) /\<^sub>R c) ((l - t) /\<^sub>R c)) x :: ennreal)" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
602 |
by (auto split: split_indicator) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
603 |
have **: "(\<Prod>x\<in>Basis. (l \<bullet> x - u \<bullet> x) / c) = (\<Prod>x\<in>Basis. u \<bullet> x - l \<bullet> x) / (-c) ^ card (Basis::'a set)" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
604 |
using \<open>c < 0\<close> |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
605 |
by (auto simp add: field_simps setprod_dividef[symmetric] setprod_constant[symmetric] |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
606 |
intro!: setprod.cong) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
607 |
show ?thesis |
61808 | 608 |
using \<open>c < 0\<close> le |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
609 |
by (auto simp: * ** field_simps emeasure_density nn_integral_distr nn_integral_cmult |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
610 |
emeasure_lborel_box_eq inner_simps setprod_nonneg ennreal_mult[symmetric] |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
611 |
borel_measurable_indicator') |
49777 | 612 |
qed |
613 |
qed simp |
|
614 |
||
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
615 |
lemma lborel_real_affine: |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
616 |
"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
|
617 |
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
|
618 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
619 |
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
|
620 |
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
|
621 |
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
|
622 |
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
|
623 |
(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
|
624 |
|
56996 | 625 |
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
|
626 |
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
|
627 |
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
|
628 |
by (subst lborel_real_affine[OF c, of t]) |
56996 | 629 |
(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
|
630 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
631 |
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
|
632 |
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
|
633 |
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
|
634 |
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
|
635 |
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
|
636 |
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
|
637 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
638 |
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
|
639 |
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
|
640 |
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
|
641 |
using |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
642 |
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
|
643 |
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
|
644 |
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
|
645 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
646 |
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
|
647 |
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
|
648 |
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
|
649 |
proof cases |
5cfcc616d485
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
hoelzl
parents:
57138
diff
changeset
|
650 |
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
|
651 |
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
|
652 |
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
|
653 |
(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
|
654 |
next |
5cfcc616d485
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
hoelzl
parents:
57138
diff
changeset
|
655 |
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
|
656 |
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
|
657 |
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
|
658 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
659 |
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
|
660 |
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
|
661 |
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
|
662 |
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
|
663 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
664 |
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
|
665 |
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
|
666 |
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
|
667 |
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
|
668 |
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
|
669 |
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
|
670 |
by (simp_all add: lborel_integral_real_affine[symmetric] divideR_right cong: conj_cong) |
49777 | 671 |
|
59425 | 672 |
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
|
673 |
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
|
674 |
(auto simp: density_1 one_ennreal_def[symmetric]) |
59425 | 675 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
676 |
lemma lborel_distr_mult: |
59425 | 677 |
assumes "(c::real) \<noteq> 0" |
678 |
shows "distr lborel borel (op * c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)" |
|
679 |
proof- |
|
680 |
have "distr lborel borel (op * c) = distr lborel lborel (op * c)" by (simp cong: distr_cong) |
|
681 |
also from assms have "... = density lborel (\<lambda>_. inverse \<bar>c\<bar>)" |
|
682 |
by (subst lborel_real_affine[of "inverse c" 0]) (auto simp: o_def distr_density_distr) |
|
683 |
finally show ?thesis . |
|
684 |
qed |
|
685 |
||
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
686 |
lemma lborel_distr_mult': |
59425 | 687 |
assumes "(c::real) \<noteq> 0" |
61945 | 688 |
shows "lborel = density (distr lborel borel (op * c)) (\<lambda>_. \<bar>c\<bar>)" |
59425 | 689 |
proof- |
690 |
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
|
691 |
also from assms have "(\<lambda>_. 1 :: ennreal) = (\<lambda>_. inverse \<bar>c\<bar> * \<bar>c\<bar>)" by (intro ext) simp |
61945 | 692 |
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
|
693 |
by (subst density_density_eq) (auto simp: ennreal_mult) |
61945 | 694 |
also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel (op * c)" |
59425 | 695 |
by (rule lborel_distr_mult[symmetric]) |
696 |
finally show ?thesis . |
|
697 |
qed |
|
698 |
||
699 |
lemma lborel_distr_plus: "distr lborel borel (op + c) = (lborel :: real measure)" |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
700 |
by (subst lborel_real_affine[of 1 c]) (auto simp: density_1 one_ennreal_def[symmetric]) |
59425 | 701 |
|
61605 | 702 |
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
|
703 |
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
|
704 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
705 |
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
|
706 |
|
59425 | 707 |
lemma lborel_prod: |
708 |
"lborel \<Otimes>\<^sub>M lborel = (lborel :: ('a::euclidean_space \<times> 'b::euclidean_space) measure)" |
|
709 |
proof (rule lborel_eqI[symmetric], clarify) |
|
710 |
fix la ua :: 'a and lb ub :: 'b |
|
711 |
assume lu: "\<And>a b. (a, b) \<in> Basis \<Longrightarrow> (la, lb) \<bullet> (a, b) \<le> (ua, ub) \<bullet> (a, b)" |
|
712 |
have [simp]: |
|
713 |
"\<And>b. b \<in> Basis \<Longrightarrow> la \<bullet> b \<le> ua \<bullet> b" |
|
714 |
"\<And>b. b \<in> Basis \<Longrightarrow> lb \<bullet> b \<le> ub \<bullet> b" |
|
715 |
"inj_on (\<lambda>u. (u, 0)) Basis" "inj_on (\<lambda>u. (0, u)) Basis" |
|
716 |
"(\<lambda>u. (u, 0)) ` Basis \<inter> (\<lambda>u. (0, u)) ` Basis = {}" |
|
717 |
"box (la, lb) (ua, ub) = box la ua \<times> box lb ub" |
|
718 |
using lu[of _ 0] lu[of 0] by (auto intro!: inj_onI simp add: Basis_prod_def ball_Un box_def) |
|
719 |
show "emeasure (lborel \<Otimes>\<^sub>M lborel) (box (la, lb) (ua, ub)) = |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
720 |
ennreal (setprod (op \<bullet> ((ua, ub) - (la, lb))) Basis)" |
59425 | 721 |
by (simp add: lborel.emeasure_pair_measure_Times Basis_prod_def setprod.union_disjoint |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
722 |
setprod.reindex ennreal_mult inner_diff_left setprod_nonneg) |
59425 | 723 |
qed (simp add: borel_prod[symmetric]) |
724 |
||
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
725 |
(* 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
|
726 |
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
|
727 |
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
|
728 |
|
61808 | 729 |
subsection \<open>Equivalence Lebesgue integral on @{const lborel} and HK-integral\<close> |
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset
|
730 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
731 |
lemma has_integral_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
|
732 |
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
|
733 |
assumes A[measurable]: "A \<in> sets borel" and finite: "emeasure lborel A < \<infinity>" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
734 |
shows "((\<lambda>x. 1) has_integral measure lborel A) A" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
735 |
proof - |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
736 |
{ fix l u :: 'a |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
737 |
have "((\<lambda>x. 1) has_integral measure lborel (box l u)) (box 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
|
738 |
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
|
739 |
assume "\<forall>b\<in>Basis. 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
|
740 |
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
|
741 |
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
|
742 |
apply (subst has_integral_restrict[symmetric, OF box_subset_cbox]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
743 |
apply (subst has_integral_spike_interior_eq[where g="\<lambda>_. 1"]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
744 |
using has_integral_const[of "1::real" 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
|
745 |
apply (simp_all add: inner_diff_left[symmetric] content_cbox_cases) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
746 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
747 |
next |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
748 |
assume "\<not> (\<forall>b\<in>Basis. 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
|
749 |
then have "box 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
|
750 |
unfolding box_eq_empty by (auto simp: not_le 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
|
751 |
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
|
752 |
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
|
753 |
qed } |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
754 |
note has_integral_box = this |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
755 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
756 |
{ fix a b :: 'a let ?M = "\<lambda>A. measure lborel (A \<inter> box 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
|
757 |
have "Int_stable (range (\<lambda>(a, b). box 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
|
758 |
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
|
759 |
moreover have "(range (\<lambda>(a, b). box a b)) \<subseteq> Pow UNIV" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
760 |
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
|
761 |
moreover have "A \<in> sigma_sets UNIV (range (\<lambda>(a, b). box 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
|
762 |
using A unfolding borel_eq_box 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
|
763 |
ultimately have "((\<lambda>x. 1) has_integral ?M A) (A \<inter> box 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
|
764 |
proof (induction rule: sigma_sets_induct_disjoint) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
765 |
case (basic A) 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
|
766 |
by (auto simp: box_Int_box has_integral_box) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
767 |
next |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
768 |
case empty 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
|
769 |
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
|
770 |
next |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
771 |
case (compl A) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
772 |
then have [measurable]: "A \<in> sets borel" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
773 |
by (simp add: borel_eq_box) |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
774 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
775 |
have "((\<lambda>x. 1) has_integral ?M (box a b)) (box 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
|
776 |
by (simp add: has_integral_box) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
777 |
moreover have "((\<lambda>x. if x \<in> A \<inter> box a b then 1 else 0) has_integral ?M A) (box 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
|
778 |
by (subst has_integral_restrict) (auto intro: compl) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
779 |
ultimately have "((\<lambda>x. 1 - (if x \<in> A \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box 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
|
780 |
by (rule has_integral_sub) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
781 |
then have "((\<lambda>x. (if x \<in> (UNIV - A) \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)" |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
782 |
by (rule has_integral_cong[THEN iffD1, rotated 1]) 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
|
783 |
then have "((\<lambda>x. 1) has_integral ?M (box a b) - ?M A) ((UNIV - A) \<inter> box 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
|
784 |
by (subst (asm) has_integral_restrict) auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
785 |
also have "?M (box a b) - ?M A = ?M (UNIV - A)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
786 |
by (subst measure_Diff[symmetric]) (auto simp: emeasure_lborel_box_eq Diff_Int_distrib2) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
787 |
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
|
788 |
next |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
789 |
case (union F) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
790 |
then have [measurable]: "\<And>i. F i \<in> sets borel" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
791 |
by (simp add: borel_eq_box subset_eq) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
792 |
have "((\<lambda>x. if x \<in> UNION UNIV F \<inter> box a b then 1 else 0) has_integral ?M (\<Union>i. F i)) (box 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
|
793 |
proof (rule has_integral_monotone_convergence_increasing) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
794 |
let ?f = "\<lambda>k x. \<Sum>i<k. if x \<in> F i \<inter> box a b then 1 else 0 :: real" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
795 |
show "\<And>k. (?f k has_integral (\<Sum>i<k. ?M (F i))) (box 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
|
796 |
using union.IH by (auto intro!: has_integral_setsum simp del: Int_iff) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
797 |
show "\<And>k x. ?f k x \<le> ?f (Suc k) x" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
798 |
by (intro setsum_mono2) auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
799 |
from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
800 |
by (auto simp add: disjoint_family_on_def) |
61969 | 801 |
show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> UNION UNIV F \<inter> box a b then 1 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
|
802 |
apply (auto simp: * setsum.If_cases Iio_Int_singleton) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
803 |
apply (rule_tac k="Suc xa" in LIMSEQ_offset) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
804 |
apply 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
|
805 |
done |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
806 |
have *: "emeasure lborel ((\<Union>x. F x) \<inter> box a b) \<le> emeasure lborel (box 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
|
807 |
by (intro emeasure_mono) auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
808 |
|
61969 | 809 |
with union(1) show "(\<lambda>k. \<Sum>i<k. ?M (F i)) \<longlonglongrightarrow> ?M (\<Union>i. F 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
|
810 |
unfolding sums_def[symmetric] UN_extend_simps |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
811 |
by (intro measure_UNION) (auto simp: disjoint_family_on_def emeasure_lborel_box_eq top_unique) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
812 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
813 |
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
|
814 |
by (subst (asm) has_integral_restrict) auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
815 |
qed } |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
816 |
note * = this |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
817 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
818 |
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
|
819 |
proof (rule has_integral_monotone_convergence_increasing) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
820 |
let ?B = "\<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
|
821 |
let ?f = "\<lambda>n::nat. \<lambda>x. if x \<in> A \<inter> ?B n then 1 else 0 :: real" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
822 |
let ?M = "\<lambda>n. measure lborel (A \<inter> ?B n)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
823 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
824 |
show "\<And>n::nat. (?f n has_integral ?M n) A" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
825 |
using * by (subst has_integral_restrict) simp_all |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
826 |
show "\<And>k x. ?f k x \<le> ?f (Suc k) x" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
827 |
by (auto simp: box_def) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
828 |
{ fix x assume "x \<in> A" |
61969 | 829 |
moreover have "(\<lambda>k. indicator (A \<inter> ?B k) x :: real) \<longlonglongrightarrow> indicator (\<Union>k::nat. A \<inter> ?B k) x" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
830 |
by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def box_def) |
61969 | 831 |
ultimately show "(\<lambda>k. if x \<in> A \<inter> ?B k then 1 else 0::real) \<longlonglongrightarrow> 1" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
832 |
by (simp add: indicator_def UN_box_eq_UNIV) } |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
833 |
|
61969 | 834 |
have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> emeasure lborel (\<Union>n::nat. A \<inter> ?B 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
|
835 |
by (intro Lim_emeasure_incseq) (auto simp: incseq_def box_def) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
836 |
also have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) = (\<lambda>n. measure lborel (A \<inter> ?B n))" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
837 |
proof (intro ext emeasure_eq_ennreal_measure) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
838 |
fix n have "emeasure lborel (A \<inter> ?B n) \<le> emeasure lborel (?B n)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
839 |
by (intro emeasure_mono) auto |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
840 |
then show "emeasure lborel (A \<inter> ?B n) \<noteq> top" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
841 |
by (auto simp: top_unique) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
842 |
qed |
61969 | 843 |
finally show "(\<lambda>n. measure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> measure lborel A" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
844 |
using emeasure_eq_ennreal_measure[of lborel A] finite |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
845 |
by (simp add: UN_box_eq_UNIV less_top) |
41654 | 846 |
qed |
40859 | 847 |
qed |
848 |
||
56996 | 849 |
lemma nn_integral_has_integral: |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
850 |
fixes f::"'a::euclidean_space \<Rightarrow> real" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
851 |
assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r" |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
852 |
shows "(f has_integral r) UNIV" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
853 |
using f proof (induct f arbitrary: r rule: borel_measurable_induct_real) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
854 |
case (set A) |
63540 | 855 |
then have "((\<lambda>x. 1) has_integral measure lborel A) A" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
856 |
by (intro has_integral_measure_lborel) (auto simp: ennreal_indicator) |
63540 | 857 |
with set show ?case |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
858 |
by (simp add: ennreal_indicator measure_def) (simp add: indicator_def) |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
859 |
next |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
860 |
case (mult g c) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
861 |
then have "ennreal c * (\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal r" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
862 |
by (subst nn_integral_cmult[symmetric]) (auto simp: ennreal_mult) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
863 |
with \<open>0 \<le> r\<close> \<open>0 \<le> c\<close> |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
864 |
obtain r' where "(c = 0 \<and> r = 0) \<or> (0 \<le> r' \<and> (\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel) = ennreal r' \<and> r = c * r')" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
865 |
by (cases "\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel" rule: ennreal_cases) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
866 |
(auto split: if_split_asm simp: ennreal_mult_top ennreal_mult[symmetric]) |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
867 |
with mult show ?case |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
868 |
by (auto intro!: has_integral_cmult_real) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
869 |
next |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
870 |
case (add g h) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
871 |
then have "(\<integral>\<^sup>+ x. h x + g x \<partial>lborel) = (\<integral>\<^sup>+ x. h x \<partial>lborel) + (\<integral>\<^sup>+ x. g x \<partial>lborel)" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
872 |
by (simp add: nn_integral_add) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
873 |
with add obtain a b where "0 \<le> a" "0 \<le> b" "(\<integral>\<^sup>+ x. h x \<partial>lborel) = ennreal a" "(\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal b" "r = a + b" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
874 |
by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ennreal2_cases) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
875 |
(auto simp: add_top nn_integral_add top_add ennreal_plus[symmetric] simp del: ennreal_plus) |
63540 | 876 |
with add show ?case |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
877 |
by (auto intro!: has_integral_add) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
878 |
next |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
879 |
case (seq U) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
880 |
note seq(1)[measurable] and f[measurable] |
40859 | 881 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
882 |
{ fix i x |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
883 |
have "U i x \<le> f x" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
884 |
using seq(5) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
885 |
apply (rule LIMSEQ_le_const) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
886 |
using seq(4) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
887 |
apply (auto intro!: exI[of _ i] simp: incseq_def le_fun_def) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
888 |
done } |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
889 |
note U_le_f = this |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
890 |
|
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
891 |
{ fix i |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
892 |
have "(\<integral>\<^sup>+x. U i x \<partial>lborel) \<le> (\<integral>\<^sup>+x. f x \<partial>lborel)" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
893 |
using seq(2) f(2) U_le_f by (intro nn_integral_mono) simp |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
894 |
then obtain p where "(\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p" "p \<le> r" "0 \<le> p" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
895 |
using seq(6) \<open>0\<le>r\<close> by (cases "\<integral>\<^sup>+x. U i x \<partial>lborel" rule: ennreal_cases) (auto simp: top_unique) |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
896 |
moreover note seq |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
897 |
ultimately have "\<exists>p. (\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p \<and> 0 \<le> p \<and> p \<le> r \<and> (U i has_integral p) UNIV" |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
898 |
by auto } |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
899 |
then obtain p where p: "\<And>i. (\<integral>\<^sup>+x. ennreal (U i x) \<partial>lborel) = ennreal (p i)" |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
900 |
and bnd: "\<And>i. p i \<le> r" "\<And>i. 0 \<le> p i" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
901 |
and U_int: "\<And>i.(U i has_integral (p i)) UNIV" by metis |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
902 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
903 |
have int_eq: "\<And>i. integral UNIV (U i) = p i" using U_int by (rule integral_unique) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
904 |
|
61969 | 905 |
have *: "f integrable_on UNIV \<and> (\<lambda>k. integral UNIV (U k)) \<longlonglongrightarrow> integral UNIV f" |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
906 |
proof (rule monotone_convergence_increasing) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
907 |
show "\<forall>k. U k integrable_on UNIV" using U_int by auto |
61808 | 908 |
show "\<forall>k. \<forall>x\<in>UNIV. U k x \<le> U (Suc k) x" using \<open>incseq U\<close> by (auto simp: incseq_def le_fun_def) |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
909 |
then show "bounded {integral UNIV (U k) |k. True}" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
910 |
using bnd int_eq by (auto simp: bounded_real intro!: exI[of _ r]) |
61969 | 911 |
show "\<forall>x\<in>UNIV. (\<lambda>k. U k x) \<longlonglongrightarrow> f x" |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
912 |
using seq by auto |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset
|
913 |
qed |
61969 | 914 |
moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lborel)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. f x \<partial>lborel)" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
915 |
using seq f(2) U_le_f by (intro nn_integral_dominated_convergence[where w=f]) auto |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
916 |
ultimately have "integral UNIV f = r" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
917 |
by (auto simp add: bnd int_eq p seq intro: LIMSEQ_unique) |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
918 |
with * show ?case |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
919 |
by (simp add: has_integral_integral) |
40859 | 920 |
qed |
921 |
||
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
922 |
lemma nn_integral_lborel_eq_integral: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
923 |
fixes f::"'a::euclidean_space \<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
|
924 |
assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
925 |
shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = integral UNIV f" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
926 |
proof - |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
927 |
from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
928 |
by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) 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
|
929 |
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
|
930 |
using nn_integral_has_integral[OF f(1,2) r] by (simp add: integral_unique) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
931 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
932 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
933 |
lemma nn_integral_integrable_on: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
934 |
fixes f::"'a::euclidean_space \<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
|
935 |
assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
936 |
shows "f integrable_on UNIV" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
937 |
proof - |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
938 |
from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
939 |
by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) 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
|
940 |
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
|
941 |
by (intro has_integral_integrable[where i=r] nn_integral_has_integral[where r=r] f) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
942 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
943 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
944 |
lemma nn_integral_has_integral_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
|
945 |
fixes f :: "'a::euclidean_space \<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
|
946 |
assumes f_borel: "f \<in> borel_measurable borel" and nonneg: "\<And>x. 0 \<le> f x" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
947 |
assumes I: "(f has_integral 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
|
948 |
shows "integral\<^sup>N lborel f = I" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
949 |
proof - |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
950 |
from f_borel have "(\<lambda>x. ennreal (f x)) \<in> borel_measurable lborel" 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
|
951 |
from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
952 |
let ?B = "\<lambda>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^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
|
953 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
954 |
note F(1)[THEN borel_measurable_simple_function, measurable] |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
955 |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
956 |
have "0 \<le> I" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
957 |
using I by (rule has_integral_nonneg) (simp add: nonneg) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
958 |
|
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
959 |
have F_le_f: "enn2real (F i x) \<le> f x" for i x |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
960 |
using F(3,4)[where x=x] nonneg SUP_upper[of i UNIV "\<lambda>i. F i x"] |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
961 |
by (cases "F i x" rule: ennreal_cases) 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
|
962 |
let ?F = "\<lambda>i x. F i x * indicator (?B i) x" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
963 |
have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (SUP i. integral\<^sup>N lborel (\<lambda>x. ?F i x))" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
964 |
proof (subst nn_integral_monotone_convergence_SUP[symmetric]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
965 |
{ fix x |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
966 |
obtain j where j: "x \<in> ?B j" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
967 |
using UN_box_eq_UNIV by auto |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
968 |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
969 |
have "ennreal (f x) = (SUP i. F i x)" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
970 |
using F(4)[of x] nonneg[of x] by (simp add: max_def) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
971 |
also have "\<dots> = (SUP i. ?F i x)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
972 |
proof (rule SUP_eq) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
973 |
fix i show "\<exists>j\<in>UNIV. F i x \<le> ?F j x" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
974 |
using j F(2) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
975 |
by (intro bexI[of _ "max i j"]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
976 |
(auto split: split_max split_indicator simp: incseq_def le_fun_def box_def) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
977 |
qed (auto intro!: F split: split_indicator) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
978 |
finally have "ennreal (f x) = (SUP i. ?F i x)" . } |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
979 |
then show "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (\<integral>\<^sup>+ x. (SUP i. ?F i x) \<partial>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
|
980 |
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
|
981 |
qed (insert F, auto simp: incseq_def le_fun_def box_def split: split_indicator) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
982 |
also have "\<dots> \<le> ennreal 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
|
983 |
proof (rule SUP_least) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
984 |
fix i :: nat |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
985 |
have finite_F: "(\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel) < \<infinity>" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
986 |
proof (rule nn_integral_bound_simple_function) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
987 |
have "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} \<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
|
988 |
emeasure lborel (?B i)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
989 |
by (intro emeasure_mono) (auto split: split_indicator) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
990 |
then show "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} < \<infinity>" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
991 |
by (auto simp: less_top[symmetric] top_unique) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
992 |
qed (auto split: split_indicator |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
993 |
intro!: F simple_function_compose1[where g="enn2real"] simple_function_ennreal) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
994 |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
995 |
have int_F: "(\<lambda>x. enn2real (F i x) * indicator (?B i) x) integrable_on UNIV" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
996 |
using F(4) finite_F |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
997 |
by (intro nn_integral_integrable_on) (auto split: split_indicator simp: enn2real_nonneg) |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
998 |
|
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
999 |
have "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) = |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1000 |
(\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel)" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1001 |
using F(3,4) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1002 |
by (intro nn_integral_cong) (auto simp: image_iff eq_commute split: split_indicator) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1003 |
also have "\<dots> = ennreal (integral UNIV (\<lambda>x. enn2real (F i x) * indicator (?B i) x))" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1004 |
using F |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1005 |
by (intro nn_integral_lborel_eq_integral[OF _ _ finite_F]) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1006 |
(auto split: split_indicator intro: enn2real_nonneg) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1007 |
also have "\<dots> \<le> ennreal 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
|
1008 |
by (auto intro!: has_integral_le[OF integrable_integral[OF int_F] I] nonneg F_le_f |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1009 |
simp: \<open>0 \<le> I\<close> split: split_indicator ) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1010 |
finally show "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) \<le> ennreal 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
|
1011 |
qed |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1012 |
finally have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) < \<infinity>" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1013 |
by (auto simp: less_top[symmetric] top_unique) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1014 |
from nn_integral_lborel_eq_integral[OF assms(1,2) this] I 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
|
1015 |
by (simp add: integral_unique) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1016 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1017 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1018 |
lemma has_integral_iff_emeasure_lborel: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1019 |
fixes A :: "'a::euclidean_space set" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1020 |
assumes A[measurable]: "A \<in> sets borel" and [simp]: "0 \<le> r" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1021 |
shows "((\<lambda>x. 1) has_integral r) A \<longleftrightarrow> emeasure lborel A = ennreal r" |
63540 | 1022 |
proof (cases "emeasure lborel A = \<infinity>") |
1023 |
case emeasure_A: True |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1024 |
have "\<not> (\<lambda>x. 1::real) integrable_on A" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1025 |
proof |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1026 |
assume int: "(\<lambda>x. 1::real) integrable_on A" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1027 |
then have "(indicator A::'a \<Rightarrow> real) integrable_on UNIV" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1028 |
unfolding indicator_def[abs_def] integrable_restrict_univ . |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1029 |
then obtain r where "((indicator A::'a\<Rightarrow>real) has_integral r) UNIV" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1030 |
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
|
1031 |
from nn_integral_has_integral_lborel[OF _ _ this] emeasure_A show False |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1032 |
by (simp add: ennreal_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
|
1033 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1034 |
with emeasure_A 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
|
1035 |
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
|
1036 |
next |
63540 | 1037 |
case False |
1038 |
then have "((\<lambda>x. 1) has_integral measure lborel A) A" |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1039 |
by (simp add: has_integral_measure_lborel less_top) |
63540 | 1040 |
with False show ?thesis |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1041 |
by (auto simp: emeasure_eq_ennreal_measure has_integral_unique) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1042 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1043 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1044 |
lemma has_integral_integral_real: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1045 |
fixes f::"'a::euclidean_space \<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
|
1046 |
assumes f: "integrable lborel f" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1047 |
shows "(f has_integral (integral\<^sup>L lborel f)) UNIV" |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1048 |
using f proof induct |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1049 |
case (base A c) then show ?case |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1050 |
by (auto intro!: has_integral_mult_left simp: ) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1051 |
(simp add: emeasure_eq_ennreal_measure indicator_def has_integral_measure_lborel) |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1052 |
next |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1053 |
case (add f g) then show ?case |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1054 |
by (auto intro!: has_integral_add) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1055 |
next |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1056 |
case (lim f s) |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1057 |
show ?case |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1058 |
proof (rule has_integral_dominated_convergence) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1059 |
show "\<And>i. (s i has_integral integral\<^sup>L lborel (s i)) UNIV" by fact |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1060 |
show "(\<lambda>x. norm (2 * f x)) integrable_on UNIV" |
61808 | 1061 |
using \<open>integrable lborel f\<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
|
1062 |
by (intro nn_integral_integrable_on) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1063 |
(auto simp: integrable_iff_bounded abs_mult nn_integral_cmult ennreal_mult 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
|
1064 |
show "\<And>k. \<forall>x\<in>UNIV. norm (s k x) \<le> norm (2 * f x)" |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1065 |
using lim by (auto simp add: abs_mult) |
61969 | 1066 |
show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) \<longlonglongrightarrow> f x" |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1067 |
using lim by auto |
61969 | 1068 |
show "(\<lambda>k. integral\<^sup>L lborel (s k)) \<longlonglongrightarrow> integral\<^sup>L lborel 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
|
1069 |
using lim lim(1)[THEN borel_measurable_integrable] |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1070 |
by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1071 |
qed |
40859 | 1072 |
qed |
1073 |
||
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1074 |
context |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1075 |
fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1076 |
begin |
41546
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset
|
1077 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1078 |
lemma has_integral_integral_lborel: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1079 |
assumes f: "integrable lborel f" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51478
diff
changeset
|
1080 |
shows "(f has_integral (integral\<^sup>L lborel f)) UNIV" |
41546
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset
|
1081 |
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
|
1082 |
have "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b)) UNIV" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1083 |
using f by (intro has_integral_setsum finite_Basis ballI has_integral_scaleR_left has_integral_integral_real) auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1084 |
also have eq_f: "(\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) = f" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1085 |
by (simp add: fun_eq_iff euclidean_representation) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1086 |
also have "(\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b) = integral\<^sup>L lborel f" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1087 |
using f by (subst (2) eq_f[symmetric]) simp |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1088 |
finally show ?thesis . |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1089 |
qed |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1090 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1091 |
lemma integrable_on_lborel: "integrable lborel f \<Longrightarrow> f integrable_on UNIV" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1092 |
using has_integral_integral_lborel 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
|
1093 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1094 |
lemma integral_lborel: "integrable lborel f \<Longrightarrow> integral UNIV f = (\<integral>x. f x \<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
|
1095 |
using has_integral_integral_lborel by auto |
49777 | 1096 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1097 |
end |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1098 |
|
61808 | 1099 |
subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close> |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1100 |
|
57138
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1101 |
lemma emeasure_bounded_finite: |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1102 |
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
|
1103 |
proof - |
61808 | 1104 |
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
|
1105 |
by auto |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1106 |
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
|
1107 |
by (intro emeasure_mono) auto |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1108 |
then show ?thesis |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1109 |
by (auto simp: emeasure_lborel_cbox_eq setprod_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
|
1110 |
qed |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1111 |
|
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1112 |
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
|
1113 |
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
|
1114 |
|
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1115 |
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
|
1116 |
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
|
1117 |
assumes "compact S" "continuous_on S f" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1118 |
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
|
1119 |
proof cases |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1120 |
assume "S \<noteq> {}" |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1121 |
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
|
1122 |
using assms by (intro continuous_intros) |
61808 | 1123 |
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
|
1124 |
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
|
1125 |
by auto |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1126 |
|
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1127 |
show ?thesis |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1128 |
proof (rule integrable_bound) |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1129 |
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
|
1130 |
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
|
1131 |
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
|
1132 |
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
|
1133 |
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
|
1134 |
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
|
1135 |
qed |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1136 |
qed simp |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1137 |
|
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1138 |
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
|
1139 |
fixes f :: "real \<Rightarrow> real" |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1140 |
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
|
1141 |
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
|
1142 |
proof - |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1143 |
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
|
1144 |
proof (rule borel_integrable_compact) |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1145 |
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
|
1146 |
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
|
1147 |
qed simp |
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1148 |
then show ?thesis |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57447
diff
changeset
|
1149 |
by (auto simp: mult.commute) |
57138
7b3146180291
generalizd measurability on restricted space; rule for integrability on compact sets
hoelzl
parents:
57137
diff
changeset
|
1150 |
qed |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1151 |
|
61808 | 1152 |
text \<open> |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1153 |
|
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
1154 |
For the positive integral we replace continuity with Borel-measurability. |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1155 |
|
61808 | 1156 |
\<close> |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1157 |
|
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1158 |
lemma |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1159 |
fixes f :: "real \<Rightarrow> real" |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1160 |
assumes [measurable]: "f \<in> borel_measurable borel" |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1161 |
assumes f: "\<And>x. x \<in> {a..b} \<Longrightarrow> DERIV F x :> f x" "\<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x" and "a \<le> b" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1162 |
shows nn_integral_FTC_Icc: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?nn) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1163 |
and has_bochner_integral_FTC_Icc_nonneg: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1164 |
"has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1165 |
and integral_FTC_Icc_nonneg: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq) |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1166 |
and integrable_FTC_Icc_nonneg: "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)" (is ?int) |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1167 |
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
|
1168 |
have *: "(\<lambda>x. f x * indicator {a..b} x) \<in> borel_measurable borel" "\<And>x. 0 \<le> f x * indicator {a..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
|
1169 |
using f(2) by (auto split: split_indicator) |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
1170 |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1171 |
have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b\<Longrightarrow> F x \<le> F y" for x y |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1172 |
using f by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1173 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1174 |
have "(f has_integral F b - F a) {a..b}" |
56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
56020
diff
changeset
|
1175 |
by (intro fundamental_theorem_of_calculus) |
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
56020
diff
changeset
|
1176 |
(auto simp: has_field_derivative_iff_has_vector_derivative[symmetric] |
61808 | 1177 |
intro: has_field_derivative_subset[OF f(1)] \<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
|
1178 |
then have i: "((\<lambda>x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1179 |
unfolding indicator_def if_distrib[where f="\<lambda>x. a * x" for a] |
63566 | 1180 |
by (simp cong del: if_weak_cong del: atLeastAtMost_iff) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1181 |
then have nn: "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = 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
|
1182 |
by (rule nn_integral_has_integral_lborel[OF *]) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1183 |
then show ?has |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1184 |
by (rule has_bochner_integral_nn_integral[rotated 3]) (simp_all add: * F_mono \<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
|
1185 |
then show ?eq ?int |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1186 |
unfolding has_bochner_integral_iff by auto |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1187 |
show ?nn |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1188 |
by (subst nn[symmetric]) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1189 |
(auto intro!: nn_integral_cong simp add: ennreal_mult f split: split_indicator) |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1190 |
qed |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1191 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1192 |
lemma |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1193 |
fixes f :: "real \<Rightarrow> 'a :: euclidean_space" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1194 |
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
|
1195 |
assumes "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {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
|
1196 |
assumes cont: "continuous_on {a .. b} f" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1197 |
shows has_bochner_integral_FTC_Icc: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1198 |
"has_bochner_integral lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) (F b - F a)" (is ?has) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1199 |
and integral_FTC_Icc: "(\<integral>x. indicator {a .. b} x *\<^sub>R f x \<partial>lborel) = F b - F a" (is ?eq) |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56218
diff
changeset
|
1200 |
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
|
1201 |
let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1202 |
have int: "integrable lborel ?f" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1203 |
using borel_integrable_compact[OF _ cont] 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
|
1204 |
have "(f has_integral F b - F a) {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
|
1205 |
using assms(1,2) by (intro fundamental_theorem_of_calculus) auto |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
1206 |
moreover |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1207 |
have "(f has_integral integral\<^sup>L lborel ?f) {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
|
1208 |
using has_integral_integral_lborel[OF int] |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1209 |
unfolding indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] |
63566 | 1210 |
by (simp cong del: if_weak_cong del: atLeastAtMost_iff) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1211 |
ultimately show ?eq |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1212 |
by (auto dest: has_integral_unique) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1213 |
then show ?has |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1214 |
using int by (auto simp: has_bochner_integral_iff) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1215 |
qed |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1216 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1217 |
lemma |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1218 |
fixes f :: "real \<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
|
1219 |
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
|
1220 |
assumes deriv: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> DERIV F x :> f x" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1221 |
assumes cont: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1222 |
shows has_bochner_integral_FTC_Icc_real: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1223 |
"has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1224 |
and integral_FTC_Icc_real: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1225 |
proof - |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1226 |
have 1: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {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
|
1227 |
unfolding has_field_derivative_iff_has_vector_derivative[symmetric] |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1228 |
using deriv by (auto intro: DERIV_subset) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1229 |
have 2: "continuous_on {a .. b} f" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1230 |
using cont by (intro continuous_at_imp_continuous_on) auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1231 |
show ?has ?eq |
61808 | 1232 |
using has_bochner_integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2] integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2] |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57447
diff
changeset
|
1233 |
by (auto simp: mult.commute) |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1234 |
qed |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1235 |
|
56996 | 1236 |
lemma nn_integral_FTC_atLeast: |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1237 |
fixes f :: "real \<Rightarrow> real" |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1238 |
assumes f_borel: "f \<in> borel_measurable borel" |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
1239 |
assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x" |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1240 |
assumes nonneg: "\<And>x. a \<le> x \<Longrightarrow> 0 \<le> f x" |
61973 | 1241 |
assumes lim: "(F \<longlongrightarrow> T) at_top" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1242 |
shows "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a ..} x \<partial>lborel) = T - F a" |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1243 |
proof - |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1244 |
let ?f = "\<lambda>(i::nat) (x::real). ennreal (f x) * indicator {a..a + real i} x" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1245 |
let ?fR = "\<lambda>x. ennreal (f x) * indicator {a ..} x" |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1246 |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1247 |
have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> F x \<le> F y" for x y |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1248 |
using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1249 |
then have F_le_T: "a \<le> x \<Longrightarrow> F x \<le> T" for x |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1250 |
by (intro tendsto_le_const[OF _ lim]) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1251 |
(auto simp: trivial_limit_at_top_linorder eventually_at_top_linorder) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1252 |
|
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1253 |
have "(SUP i::nat. ?f i x) = ?fR x" for x |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1254 |
proof (rule LIMSEQ_unique[OF LIMSEQ_SUP]) |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1255 |
from reals_Archimedean2[of "x - a"] guess n .. |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1256 |
then have "eventually (\<lambda>n. ?f n x = ?fR x) sequentially" |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1257 |
by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator) |
61969 | 1258 |
then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x" |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1259 |
by (rule Lim_eventually) |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1260 |
qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator) |
56996 | 1261 |
then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)" |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1262 |
by simp |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51478
diff
changeset
|
1263 |
also have "\<dots> = (SUP i::nat. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))" |
56996 | 1264 |
proof (rule nn_integral_monotone_convergence_SUP) |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1265 |
show "incseq ?f" |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1266 |
using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator) |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1267 |
show "\<And>i. (?f i) \<in> borel_measurable lborel" |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1268 |
using f_borel by auto |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1269 |
qed |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1270 |
also have "\<dots> = (SUP i::nat. ennreal (F (a + real i) - F 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
|
1271 |
by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1272 |
also have "\<dots> = T - F a" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1273 |
proof (rule LIMSEQ_unique[OF LIMSEQ_SUP]) |
61969 | 1274 |
have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T" |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1275 |
apply (rule filterlim_compose[OF lim filterlim_tendsto_add_at_top]) |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1276 |
apply (rule LIMSEQ_const_iff[THEN iffD2, OF refl]) |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1277 |
apply (rule filterlim_real_sequentially) |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1278 |
done |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1279 |
then show "(\<lambda>n. ennreal (F (a + real n) - F a)) \<longlonglongrightarrow> ennreal (T - F a)" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1280 |
by (simp add: F_mono F_le_T tendsto_diff) |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
1281 |
qed (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono) |
50418
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1282 |
finally show ?thesis . |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1283 |
qed |
bd68cf816dd3
fundamental theorem of calculus for the Lebesgue integral
hoelzl
parents:
50385
diff
changeset
|
1284 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1285 |
lemma integral_power: |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1286 |
"a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k - a^Suc k) / Suc k" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1287 |
proof (subst integral_FTC_Icc_real) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1288 |
fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1289 |
by (intro derivative_eq_intros) auto |
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
|
1290 |
qed (auto simp: field_simps simp del: of_nat_Suc) |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset
|
1291 |
|
61808 | 1292 |
subsection \<open>Integration by parts\<close> |
57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1293 |
|
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1294 |
lemma integral_by_parts_integrable: |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1295 |
fixes f g F G::"real \<Rightarrow> real" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1296 |
assumes "a \<le> b" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1297 |
assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1298 |
assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1299 |
assumes [intro]: "!!x. DERIV F x :> f x" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1300 |
assumes [intro]: "!!x. DERIV G x :> g x" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1301 |
shows "integrable lborel (\<lambda>x.((F x) * (g x) + (f x) * (G x)) * indicator {a .. b} x)" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1302 |
by (auto intro!: borel_integrable_atLeastAtMost continuous_intros) (auto intro!: DERIV_isCont) |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1303 |
|
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1304 |
lemma integral_by_parts: |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1305 |
fixes f g F G::"real \<Rightarrow> real" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1306 |
assumes [arith]: "a \<le> b" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1307 |
assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1308 |
assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1309 |
assumes [intro]: "!!x. DERIV F x :> f x" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1310 |
assumes [intro]: "!!x. DERIV G x :> g x" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1311 |
shows "(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
1312 |
= F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel" |
57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1313 |
proof- |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1314 |
have 0: "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a" |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
1315 |
by (rule integral_FTC_Icc_real, auto intro!: derivative_eq_intros continuous_intros) |
57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1316 |
(auto intro!: DERIV_isCont) |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1317 |
|
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1318 |
have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1319 |
(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1320 |
apply (subst integral_add[symmetric]) |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1321 |
apply (auto intro!: borel_integrable_atLeastAtMost continuous_intros) |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1322 |
by (auto intro!: DERIV_isCont integral_cong split:split_indicator) |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1323 |
|
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1324 |
thus ?thesis using 0 by auto |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1325 |
qed |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1326 |
|
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1327 |
lemma integral_by_parts': |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1328 |
fixes f g F G::"real \<Rightarrow> real" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1329 |
assumes "a \<le> b" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1330 |
assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1331 |
assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1332 |
assumes "!!x. DERIV F x :> f x" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1333 |
assumes "!!x. DERIV G x :> g x" |
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1334 |
shows "(\<integral>x. indicator {a .. b} x *\<^sub>R (F x * g x) \<partial>lborel) |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
1335 |
= F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel" |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
1336 |
using integral_by_parts[OF assms] by (simp add: ac_simps) |
57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1337 |
|
57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1338 |
lemma has_bochner_integral_even_function: |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1339 |
fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1340 |
assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1341 |
assumes even: "\<And>x. f (- x) = f x" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1342 |
shows "has_bochner_integral lborel f (2 *\<^sub>R x)" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1343 |
proof - |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1344 |
have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1345 |
by (auto split: split_indicator) |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1346 |
have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) x" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1347 |
by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0]) |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1348 |
(auto simp: indicator even f) |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1349 |
with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + x)" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1350 |
by (rule has_bochner_integral_add) |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1351 |
then have "has_bochner_integral lborel f (x + x)" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1352 |
by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4]) |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1353 |
(auto split: split_indicator) |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1354 |
then show ?thesis |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1355 |
by (simp add: scaleR_2) |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1356 |
qed |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1357 |
|
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1358 |
lemma has_bochner_integral_odd_function: |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1359 |
fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1360 |
assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1361 |
assumes odd: "\<And>x. f (- x) = - f x" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1362 |
shows "has_bochner_integral lborel f 0" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1363 |
proof - |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1364 |
have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1365 |
by (auto split: split_indicator) |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1366 |
have "has_bochner_integral lborel (\<lambda>x. - indicator {.. 0} x *\<^sub>R f x) x" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1367 |
by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0]) |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1368 |
(auto simp: indicator odd f) |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1369 |
from has_bochner_integral_minus[OF this] |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1370 |
have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) (- x)" |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
1371 |
by simp |
57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1372 |
with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + - x)" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1373 |
by (rule has_bochner_integral_add) |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1374 |
then have "has_bochner_integral lborel f (x + - x)" |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1375 |
by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4]) |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1376 |
(auto split: split_indicator) |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1377 |
then show ?thesis |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1378 |
by simp |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57235
diff
changeset
|
1379 |
qed |
57235
b0b9a10e4bf4
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
hoelzl
parents:
57166
diff
changeset
|
1380 |
|
38656 | 1381 |
end |