--- a/src/HOL/Probability/Borel_Space.thy Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Tue Mar 22 20:06:10 2011 +0100
@@ -1,4 +1,7 @@
-(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)
+(* Title: HOL/Probability/Lebesgue_Integration.thy
+ Author: Johannes Hölzl, TU München
+ Author: Armin Heller, TU München
+*)
header {*Borel spaces*}
--- a/src/HOL/Probability/Caratheodory.thy Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Tue Mar 22 20:06:10 2011 +0100
@@ -1,9 +1,18 @@
+(* Title: HOL/Probability/Caratheodory.thy
+ Author: Lawrence C Paulson
+ Author: Johannes Hölzl, TU München
+*)
+
header {*Caratheodory Extension Theorem*}
theory Caratheodory
imports Sigma_Algebra Extended_Real_Limits
begin
+text {*
+ Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
+*}
+
lemma suminf_extreal_2dimen:
fixes f:: "nat \<times> nat \<Rightarrow> extreal"
assumes pos: "\<And>p. 0 \<le> f p"
@@ -36,8 +45,6 @@
SUPR_extreal_setsum[symmetric] incseq_setsumI setsum_nonneg)
qed
-text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
-
subsection {* Measure Spaces *}
record 'a measure_space = "'a algebra" +
--- a/src/HOL/Probability/Information.thy Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Information.thy Tue Mar 22 20:06:10 2011 +0100
@@ -1,3 +1,10 @@
+(* Title: HOL/Probability/Information.thy
+ Author: Johannes Hölzl, TU München
+ Author: Armin Heller, TU München
+*)
+
+header {*Information theory*}
+
theory Information
imports
Probability_Space
--- a/src/HOL/Probability/Lebesgue_Integration.thy Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Mar 22 20:06:10 2011 +0100
@@ -1,4 +1,7 @@
-(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)
+(* Title: HOL/Probability/Lebesgue_Integration.thy
+ Author: Johannes Hölzl, TU München
+ Author: Armin Heller, TU München
+*)
header {*Lebesgue Integration*}
--- a/src/HOL/Probability/Lebesgue_Measure.thy Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Tue Mar 22 20:06:10 2011 +0100
@@ -1,5 +1,10 @@
-(* Author: Robert Himmelmann, TU Muenchen *)
+(* Title: HOL/Probability/Lebesgue_Measure.thy
+ Author: Johannes Hölzl, TU München
+ Author: Robert Himmelmann, TU München
+*)
+
header {* Lebsegue measure *}
+
theory Lebesgue_Measure
imports Product_Measure
begin
--- a/src/HOL/Probability/Measure.thy Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Measure.thy Tue Mar 22 20:06:10 2011 +0100
@@ -1,4 +1,10 @@
-(* Author: Lawrence C Paulson; Armin Heller, Johannes Hoelzl, TU Muenchen *)
+(* Title: HOL/Probability/Measure.thy
+ Author: Lawrence C Paulson
+ Author: Johannes Hölzl, TU München
+ Author: Armin Heller, TU München
+*)
+
+header {* Properties about measure spaces *}
theory Measure
imports Caratheodory
--- a/src/HOL/Probability/Probability_Space.thy Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Probability_Space.thy Tue Mar 22 20:06:10 2011 +0100
@@ -1,3 +1,10 @@
+(* Title: HOL/Probability/Probability_Space.thy
+ Author: Johannes Hölzl, TU München
+ Author: Armin Heller, TU München
+*)
+
+header {*Probability spaces*}
+
theory Probability_Space
imports Lebesgue_Integration Radon_Nikodym Product_Measure
begin
--- a/src/HOL/Probability/Product_Measure.thy Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Product_Measure.thy Tue Mar 22 20:06:10 2011 +0100
@@ -1,3 +1,9 @@
+(* Title: HOL/Probability/Product_Measure.thy
+ Author: Johannes Hölzl, TU München
+*)
+
+header {*Product measure spaces*}
+
theory Product_Measure
imports Lebesgue_Integration
begin
--- a/src/HOL/Probability/Radon_Nikodym.thy Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Mar 22 20:06:10 2011 +0100
@@ -1,3 +1,9 @@
+(* Title: HOL/Probability/Radon_Nikodym.thy
+ Author: Johannes Hölzl, TU München
+*)
+
+header {*Radon-Nikod{\'y}m derivative*}
+
theory Radon_Nikodym
imports Lebesgue_Integration
begin
--- a/src/HOL/Probability/Sigma_Algebra.thy Tue Mar 22 18:53:05 2011 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Mar 22 20:06:10 2011 +0100
@@ -1,5 +1,6 @@
(* Title: HOL/Probability/Sigma_Algebra.thy
- Author: Stefan Richter, Markus Wenzel, TU Muenchen
+ Author: Stefan Richter, Markus Wenzel, TU München
+ Author: Johannes Hölzl, TU München
Plus material from the Hurd/Coble measure theory development,
translated by Lawrence Paulson.
*)