standardized headers
authorhoelzl
Tue Mar 22 20:06:10 2011 +0100 (2011-03-22)
changeset 4206766c8281349ec
parent 42066 6db76c88907a
child 42068 b579e787b582
standardized headers
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measure.thy
src/HOL/Probability/Probability_Space.thy
src/HOL/Probability/Product_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Mar 22 18:53:05 2011 +0100
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Mar 22 20:06:10 2011 +0100
     1.3 @@ -1,4 +1,7 @@
     1.4 -(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)
     1.5 +(*  Title:      HOL/Probability/Lebesgue_Integration.thy
     1.6 +    Author:     Johannes Hölzl, TU München
     1.7 +    Author:     Armin Heller, TU München
     1.8 +*)
     1.9  
    1.10  header {*Borel spaces*}
    1.11  
     2.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 18:53:05 2011 +0100
     2.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 20:06:10 2011 +0100
     2.3 @@ -1,9 +1,18 @@
     2.4 +(*  Title:      HOL/Probability/Caratheodory.thy
     2.5 +    Author:     Lawrence C Paulson
     2.6 +    Author:     Johannes Hölzl, TU München
     2.7 +*)
     2.8 +
     2.9  header {*Caratheodory Extension Theorem*}
    2.10  
    2.11  theory Caratheodory
    2.12    imports Sigma_Algebra Extended_Real_Limits
    2.13  begin
    2.14  
    2.15 +text {*
    2.16 +  Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
    2.17 +*}
    2.18 +
    2.19  lemma suminf_extreal_2dimen:
    2.20    fixes f:: "nat \<times> nat \<Rightarrow> extreal"
    2.21    assumes pos: "\<And>p. 0 \<le> f p"
    2.22 @@ -36,8 +45,6 @@
    2.23                       SUPR_extreal_setsum[symmetric] incseq_setsumI setsum_nonneg)
    2.24  qed
    2.25  
    2.26 -text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
    2.27 -
    2.28  subsection {* Measure Spaces *}
    2.29  
    2.30  record 'a measure_space = "'a algebra" +
     3.1 --- a/src/HOL/Probability/Information.thy	Tue Mar 22 18:53:05 2011 +0100
     3.2 +++ b/src/HOL/Probability/Information.thy	Tue Mar 22 20:06:10 2011 +0100
     3.3 @@ -1,3 +1,10 @@
     3.4 +(*  Title:      HOL/Probability/Information.thy
     3.5 +    Author:     Johannes Hölzl, TU München
     3.6 +    Author:     Armin Heller, TU München
     3.7 +*)
     3.8 +
     3.9 +header {*Information theory*}
    3.10 +
    3.11  theory Information
    3.12  imports
    3.13    Probability_Space
     4.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 22 18:53:05 2011 +0100
     4.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 22 20:06:10 2011 +0100
     4.3 @@ -1,4 +1,7 @@
     4.4 -(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)
     4.5 +(*  Title:      HOL/Probability/Lebesgue_Integration.thy
     4.6 +    Author:     Johannes Hölzl, TU München
     4.7 +    Author:     Armin Heller, TU München
     4.8 +*)
     4.9  
    4.10  header {*Lebesgue Integration*}
    4.11  
     5.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Mar 22 18:53:05 2011 +0100
     5.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Mar 22 20:06:10 2011 +0100
     5.3 @@ -1,5 +1,10 @@
     5.4 -(*  Author: Robert Himmelmann, TU Muenchen *)
     5.5 +(*  Title:      HOL/Probability/Lebesgue_Measure.thy
     5.6 +    Author:     Johannes Hölzl, TU München
     5.7 +    Author:     Robert Himmelmann, TU München
     5.8 +*)
     5.9 +
    5.10  header {* Lebsegue measure *}
    5.11 +
    5.12  theory Lebesgue_Measure
    5.13    imports Product_Measure
    5.14  begin
     6.1 --- a/src/HOL/Probability/Measure.thy	Tue Mar 22 18:53:05 2011 +0100
     6.2 +++ b/src/HOL/Probability/Measure.thy	Tue Mar 22 20:06:10 2011 +0100
     6.3 @@ -1,4 +1,10 @@
     6.4 -(* Author: Lawrence C Paulson; Armin Heller, Johannes Hoelzl, TU Muenchen *)
     6.5 +(*  Title:      HOL/Probability/Measure.thy
     6.6 +    Author:     Lawrence C Paulson
     6.7 +    Author:     Johannes Hölzl, TU München
     6.8 +    Author:     Armin Heller, TU München
     6.9 +*)
    6.10 +
    6.11 +header {* Properties about measure spaces *}
    6.12  
    6.13  theory Measure
    6.14    imports Caratheodory
     7.1 --- a/src/HOL/Probability/Probability_Space.thy	Tue Mar 22 18:53:05 2011 +0100
     7.2 +++ b/src/HOL/Probability/Probability_Space.thy	Tue Mar 22 20:06:10 2011 +0100
     7.3 @@ -1,3 +1,10 @@
     7.4 +(*  Title:      HOL/Probability/Probability_Space.thy
     7.5 +    Author:     Johannes Hölzl, TU München
     7.6 +    Author:     Armin Heller, TU München
     7.7 +*)
     7.8 +
     7.9 +header {*Probability spaces*}
    7.10 +
    7.11  theory Probability_Space
    7.12  imports Lebesgue_Integration Radon_Nikodym Product_Measure
    7.13  begin
     8.1 --- a/src/HOL/Probability/Product_Measure.thy	Tue Mar 22 18:53:05 2011 +0100
     8.2 +++ b/src/HOL/Probability/Product_Measure.thy	Tue Mar 22 20:06:10 2011 +0100
     8.3 @@ -1,3 +1,9 @@
     8.4 +(*  Title:      HOL/Probability/Product_Measure.thy
     8.5 +    Author:     Johannes Hölzl, TU München
     8.6 +*)
     8.7 +
     8.8 +header {*Product measure spaces*}
     8.9 +
    8.10  theory Product_Measure
    8.11  imports Lebesgue_Integration
    8.12  begin
     9.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Mar 22 18:53:05 2011 +0100
     9.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Mar 22 20:06:10 2011 +0100
     9.3 @@ -1,3 +1,9 @@
     9.4 +(*  Title:      HOL/Probability/Radon_Nikodym.thy
     9.5 +    Author:     Johannes Hölzl, TU München
     9.6 +*)
     9.7 +
     9.8 +header {*Radon-Nikod{\'y}m derivative*}
     9.9 +
    9.10  theory Radon_Nikodym
    9.11  imports Lebesgue_Integration
    9.12  begin
    10.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Mar 22 18:53:05 2011 +0100
    10.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Mar 22 20:06:10 2011 +0100
    10.3 @@ -1,5 +1,6 @@
    10.4  (*  Title:      HOL/Probability/Sigma_Algebra.thy
    10.5 -    Author:     Stefan Richter, Markus Wenzel, TU Muenchen
    10.6 +    Author:     Stefan Richter, Markus Wenzel, TU München
    10.7 +    Author:     Johannes Hölzl, TU München
    10.8      Plus material from the Hurd/Coble measure theory development,
    10.9      translated by Lawrence Paulson.
   10.10  *)