equal
deleted
inserted
replaced
|
1 (* Title: HOL/Probability/Caratheodory.thy |
|
2 Author: Lawrence C Paulson |
|
3 Author: Johannes Hölzl, TU München |
|
4 *) |
|
5 |
1 header {*Caratheodory Extension Theorem*} |
6 header {*Caratheodory Extension Theorem*} |
2 |
7 |
3 theory Caratheodory |
8 theory Caratheodory |
4 imports Sigma_Algebra Extended_Real_Limits |
9 imports Sigma_Algebra Extended_Real_Limits |
5 begin |
10 begin |
|
11 |
|
12 text {* |
|
13 Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson. |
|
14 *} |
6 |
15 |
7 lemma suminf_extreal_2dimen: |
16 lemma suminf_extreal_2dimen: |
8 fixes f:: "nat \<times> nat \<Rightarrow> extreal" |
17 fixes f:: "nat \<times> nat \<Rightarrow> extreal" |
9 assumes pos: "\<And>p. 0 \<le> f p" |
18 assumes pos: "\<And>p. 0 \<le> f p" |
10 assumes "\<And>m. g m = (\<Sum>n. f (m,n))" |
19 assumes "\<And>m. g m = (\<Sum>n. f (m,n))" |
33 show ?thesis unfolding g_def using pos |
42 show ?thesis unfolding g_def using pos |
34 by (auto intro!: SUPR_eq simp: setsum_cartesian_product reindex le_SUPI2 |
43 by (auto intro!: SUPR_eq simp: setsum_cartesian_product reindex le_SUPI2 |
35 setsum_nonneg suminf_extreal_eq_SUPR SUPR_pair |
44 setsum_nonneg suminf_extreal_eq_SUPR SUPR_pair |
36 SUPR_extreal_setsum[symmetric] incseq_setsumI setsum_nonneg) |
45 SUPR_extreal_setsum[symmetric] incseq_setsumI setsum_nonneg) |
37 qed |
46 qed |
38 |
|
39 text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*} |
|
40 |
47 |
41 subsection {* Measure Spaces *} |
48 subsection {* Measure Spaces *} |
42 |
49 |
43 record 'a measure_space = "'a algebra" + |
50 record 'a measure_space = "'a algebra" + |
44 measure :: "'a set \<Rightarrow> extreal" |
51 measure :: "'a set \<Rightarrow> extreal" |