Tue, 05 Mar 2013 15:43:22 +0100 
hoelzl 
generalized lemmas in Extended_Real_Limits

file 
diff 
annotate

Wed, 28 Nov 2012 15:59:18 +0100 
wenzelm 
eliminated slightly odd identifiers;

file 
diff 
annotate

Tue, 27 Nov 2012 11:29:47 +0100 
immler 
qualified interpretation of sigma_algebra, to avoid name clashes

file 
diff 
annotate

Mon, 19 Nov 2012 12:29:02 +0100 
hoelzl 
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure

file 
diff 
annotate

Fri, 16 Nov 2012 14:46:23 +0100 
hoelzl 
measurability for nat_case and comb_seq

file 
diff 
annotate

Fri, 16 Nov 2012 11:34:34 +0100 
immler 
renamed to more appropriate lim_P for projective limit

file 
diff 
annotate

Thu, 15 Nov 2012 10:49:58 +0100 
immler 
regularity of measures, therefore:

file 
diff 
annotate

Fri, 09 Nov 2012 14:31:26 +0100 
immler 
moved lemmas into projective_family; added header for theory Projective_Family

file 
diff 
annotate

Fri, 09 Nov 2012 14:14:45 +0100 
immler 
removed redundant/unnecessary assumptions from projective_family

file 
diff 
annotate

Wed, 07 Nov 2012 14:41:49 +0100 
immler 
assume probability spaces; allow empty index set

file 
diff 
annotate

Wed, 07 Nov 2012 11:33:27 +0100 
immler 
added projective_family; generalized generator in product_prob_space to projective_family

file 
diff 
annotate

Tue, 06 Nov 2012 11:03:28 +0100 
immler 
moved lemmas further up

file 
diff 
annotate

Fri, 02 Nov 2012 14:23:54 +0100 
hoelzl 
use measurability prover

file 
diff 
annotate

Fri, 02 Nov 2012 14:00:39 +0100 
hoelzl 
infinite product measure is invariant under adding prefixes

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:37 +0200 
hoelzl 
infprod generator works also with empty index set

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:23 +0200 
hoelzl 
remove incseq assumption from measure_eqI_generator_eq

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:21 +0200 
hoelzl 
merge should operate on pairs

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:18 +0200 
hoelzl 
tuned product measurability

file 
diff 
annotate

Wed, 25 Apr 2012 19:26:27 +0200 
hoelzl 
add Caratheodories theorem for semirings of sets

file 
diff 
annotate

Mon, 23 Apr 2012 12:14:35 +0200 
hoelzl 
reworked Probability theory

file 
diff 
annotate

Tue, 13 Mar 2012 16:56:56 +0100 
wenzelm 
prefer abs_def over def_raw;

file 
diff 
annotate

Tue, 13 Mar 2012 13:31:26 +0100 
wenzelm 
tuned proofs  eliminated pointless chaining of facts after 'interpret';

file 
diff 
annotate

Tue, 28 Feb 2012 21:53:36 +0100 
wenzelm 
avoid undeclared variables in let bindings;

file 
diff 
annotate

Wed, 07 Dec 2011 15:10:29 +0100 
hoelzl 
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space

file 
diff 
annotate

Wed, 14 Sep 2011 10:08:52 0400 
hoelzl 
renamed Complete_Lattices lemmas, removed legacy names

file 
diff 
annotate

Tue, 19 Jul 2011 14:36:12 +0200 
hoelzl 
Rename extreal => ereal

file 
diff 
annotate

Tue, 05 Jul 2011 19:11:29 +0200 
hoelzl 
rename lemma Infinite_Product_Measure.sigma_sets_subseteq, it hides Sigma_Algebra.sigma_sets_subseteq

file 
diff 
annotate

Mon, 23 May 2011 19:21:05 +0200 
hoelzl 
move lemmas to Extended_Reals and Extended_Real_Limits

file 
diff 
annotate

Tue, 17 May 2011 14:36:54 +0200 
hoelzl 
the measurable sets with null measure form a ring

file 
diff 
annotate

Tue, 17 May 2011 12:24:48 +0200 
hoelzl 
add some lemmas for infinite product measure

file 
diff 
annotate

Tue, 05 Apr 2011 19:55:04 +0200 
hoelzl 
prove measurable_into_infprod_algebra and measure_infprod

file 
diff 
annotate

Wed, 30 Mar 2011 17:54:10 +0200 
hoelzl 
products of probability measures are probability measures

file 
diff 
annotate

Tue, 29 Mar 2011 14:27:42 +0200 
hoelzl 
rename Probability_Space to Probability_Measure

file 
diff 
annotate

Tue, 29 Mar 2011 14:27:41 +0200 
hoelzl 
add infinite product measure

file 
diff 
annotate
