-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathFiltered_Measure.thy
More file actions
106 lines (78 loc) · 5.25 KB
/
Copy pathFiltered_Measure.thy
File metadata and controls
106 lines (78 loc) · 5.25 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
(* Author: Ata Keskin, TU München
*)
theory Filtered_Measure
imports "HOL-Probability.Conditional_Expectation"
begin
section \<open>Filtered Measure Spaces\<close>
subsection \<open>Filtered Measure\<close>
locale filtered_measure =
fixes M F and t\<^sub>0 :: "'b :: {second_countable_topology, order_topology, t2_space}"
assumes subalgebras: "\<And>i. t\<^sub>0 \<le> i \<Longrightarrow> subalgebra M (F i)"
and sets_F_mono: "\<And>i j. t\<^sub>0 \<le> i \<Longrightarrow> i \<le> j \<Longrightarrow> sets (F i) \<le> sets (F j)"
begin
lemma space_F[simp]:
assumes "t\<^sub>0 \<le> i"
shows "space (F i) = space M"
using subalgebras assms by (simp add: subalgebra_def)
lemma sets_F_subset[simp]:
assumes "t\<^sub>0 \<le> i"
shows "sets (F i) \<subseteq> sets M"
using subalgebras assms by (simp add: subalgebra_def)
lemma subalgebra_F[intro]:
assumes "t\<^sub>0 \<le> i" "i \<le> j"
shows "subalgebra (F j) (F i)"
unfolding subalgebra_def using assms by (simp add: sets_F_mono)
lemma borel_measurable_mono:
assumes "t\<^sub>0 \<le> i" "i \<le> j"
shows "borel_measurable (F i) \<subseteq> borel_measurable (F j)"
unfolding subset_iff by (metis assms subalgebra_F measurable_from_subalg)
end
locale linearly_filtered_measure = filtered_measure M F t\<^sub>0 for M and F :: "_ :: {linorder_topology, conditionally_complete_lattice} \<Rightarrow> _" and t\<^sub>0
locale nat_filtered_measure = linearly_filtered_measure M F 0 for M and F :: "nat \<Rightarrow> _"
locale enat_filtered_measure = linearly_filtered_measure M F 0 for M and F :: "enat \<Rightarrow> _"
locale real_filtered_measure = linearly_filtered_measure M F 0 for M and F :: "real \<Rightarrow> _"
locale ennreal_filtered_measure = linearly_filtered_measure M F 0 for M and F :: "ennreal \<Rightarrow> _"
subsection \<open>\<open>\<sigma>\<close>-Finite Filtered Measure\<close>
text \<open>The locale presented here is a generalization of the \<^locale>\<open>sigma_finite_subalgebra\<close> for a particular filtration.\<close>
locale sigma_finite_filtered_measure = filtered_measure +
assumes sigma_finite_initial: "sigma_finite_subalgebra M (F t\<^sub>0)"
lemma (in sigma_finite_filtered_measure) sigma_finite_subalgebra_F[intro]:
assumes "t\<^sub>0 \<le> i"
shows "sigma_finite_subalgebra M (F i)"
using assms by (metis dual_order.refl sets_F_mono sigma_finite_initial sigma_finite_subalgebra.nested_subalg_is_sigma_finite subalgebras subalgebra_def)
locale nat_sigma_finite_filtered_measure = sigma_finite_filtered_measure M F "0 :: nat" for M F
locale enat_sigma_finite_filtered_measure = sigma_finite_filtered_measure M F "0 :: enat" for M F
locale real_sigma_finite_filtered_measure = sigma_finite_filtered_measure M F "0 :: real" for M F
locale ennreal_sigma_finite_filtered_measure = sigma_finite_filtered_measure M F "0 :: ennreal" for M F
sublocale nat_sigma_finite_filtered_measure \<subseteq> nat_filtered_measure ..
sublocale enat_sigma_finite_filtered_measure \<subseteq> enat_filtered_measure ..
sublocale real_sigma_finite_filtered_measure \<subseteq> real_filtered_measure ..
sublocale ennreal_sigma_finite_filtered_measure \<subseteq> ennreal_filtered_measure ..
sublocale nat_sigma_finite_filtered_measure \<subseteq> sigma_finite_subalgebra M "F i" by blast
sublocale enat_sigma_finite_filtered_measure \<subseteq> sigma_finite_subalgebra M "F i" by fastforce
sublocale real_sigma_finite_filtered_measure \<subseteq> sigma_finite_subalgebra M "F \<bar>i\<bar>" by fastforce
sublocale ennreal_sigma_finite_filtered_measure \<subseteq> sigma_finite_subalgebra M "F i" by fastforce
subsection \<open>Finite Filtered Measure\<close>
locale finite_filtered_measure = filtered_measure + finite_measure
sublocale finite_filtered_measure \<subseteq> sigma_finite_filtered_measure
using subalgebras by (unfold_locales, blast, meson dual_order.refl finite_measure_axioms finite_measure_def finite_measure_restr_to_subalg sigma_finite_measure.sigma_finite_countable)
locale nat_finite_filtered_measure = finite_filtered_measure M F "0 :: nat" for M F
locale enat_finite_filtered_measure = finite_filtered_measure M F "0 :: enat" for M F
locale real_finite_filtered_measure = finite_filtered_measure M F "0 :: real" for M F
locale ennreal_finite_filtered_measure = finite_filtered_measure M F "0 :: ennreal" for M F
sublocale nat_finite_filtered_measure \<subseteq> nat_sigma_finite_filtered_measure ..
sublocale enat_finite_filtered_measure \<subseteq> enat_sigma_finite_filtered_measure ..
sublocale real_finite_filtered_measure \<subseteq> real_sigma_finite_filtered_measure ..
sublocale ennreal_finite_filtered_measure \<subseteq> ennreal_sigma_finite_filtered_measure ..
subsection \<open>Constant Filtration\<close>
lemma filtered_measure_constant_filtration:
assumes "subalgebra M F"
shows "filtered_measure M (\<lambda>_. F) t\<^sub>0"
using assms by (unfold_locales) blast+
sublocale sigma_finite_subalgebra \<subseteq> constant_filtration: sigma_finite_filtered_measure M "\<lambda>_ :: 't :: {second_countable_topology, linorder_topology}. F" t\<^sub>0
using subalg by (unfold_locales) blast+
lemma (in finite_measure) filtered_measure_constant_filtration:
assumes "subalgebra M F"
shows "finite_filtered_measure M (\<lambda>_. F) t\<^sub>0"
using assms by (unfold_locales) blast+
end