Fri, 07 Dec 2012 14:29:09 +0100 
hoelzl 
add exponential and uniform distributions

file 
diff 
annotate

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

file 
diff 
annotate

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

file 
diff 
annotate

Fri, 02 Nov 2012 14:23:40 +0100 
hoelzl 
add measurability prover; add support for Borel sets

file 
diff 
annotate

Fri, 02 Nov 2012 14:00:39 +0100 
hoelzl 
for the product measure it is enough if only one measure is sigmafinite

file 
diff 
annotate

Thu, 11 Oct 2012 14:38:58 +0200 
hoelzl 
cleanup borel_measurable_positive_integral_(fstsnd)

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:36 +0200 
hoelzl 
add finite entropy

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:36 +0200 
hoelzl 
continuous version of mutual_information_eq_entropy_conditional_entropy

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:29 +0200 
hoelzl 
remove unnecessary assumption from conditional_entropy_eq

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:28 +0200 
hoelzl 
alternative definition of conditional entropy

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:27 +0200 
hoelzl 
remove unneeded assumption from conditional_entropy_generic_eq

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:26 +0200 
hoelzl 
show and use distributed_swap and distributed_jointI

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:25 +0200 
hoelzl 
rule to show that conditional mutual information is nonnegative in the continuous case

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:25 +0200 
hoelzl 
continuous version of entropy_le

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:24 +0200 
hoelzl 
simplified entropy_uniform

file 
diff 
annotate

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

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, 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

Thu, 01 Dec 2011 14:03:57 +0100 
hoelzl 
moved theorems about distribution to the definition; removed oopsedlemma

file 
diff 
annotate

Thu, 01 Dec 2011 14:03:57 +0100 
hoelzl 
remove duplicate theorem setsum_real_distribution

file 
diff 
annotate

Mon, 12 Sep 2011 07:55:43 +0200 
nipkow 
new fastforce replacing fastsimp  less confusing name

file 
diff 
annotate

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

file 
diff 
annotate

Mon, 27 Jun 2011 09:42:46 +0200 
hoelzl 
move conditional expectation to its own theory file

file 
diff 
annotate

Thu, 09 Jun 2011 14:04:34 +0200 
hoelzl 
lemma: independence is equal to mutual information = 0

file 
diff 
annotate

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

file 
diff 
annotate

Tue, 22 Mar 2011 20:06:10 +0100 
hoelzl 
standardized headers

file 
diff 
annotate

Mon, 14 Mar 2011 14:37:49 +0100 
hoelzl 
reworked Probability theory: measures are not type restricted to positive extended reals

file 
diff 
annotate

Wed, 23 Feb 2011 11:40:18 +0100 
hoelzl 
add lemma KL_divergence_vimage, mutual_information_generic

file 
diff 
annotate

Wed, 02 Feb 2011 12:34:45 +0100 
hoelzl 
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;

file 
diff 
annotate

Mon, 24 Jan 2011 22:29:50 +0100 
hoelzl 
use preimage measure, instead of image

file 
diff 
annotate

Wed, 29 Dec 2010 17:34:41 +0100 
wenzelm 
explicit file specifications  avoid secondary load path;

file 
diff 
annotate

Wed, 08 Dec 2010 16:15:14 +0100 
hoelzl 
cleanup bijectivity btw. product spaces and pairs

file 
diff 
annotate

Fri, 03 Dec 2010 15:25:14 +0100 
hoelzl 
it is known as the extended reals, not the infinite reals

file 
diff 
annotate

Wed, 01 Dec 2010 19:20:30 +0100 
hoelzl 
Support product spaces on sigma finite measures.

file 
diff 
annotate

Mon, 13 Sep 2010 11:13:15 +0200 
nipkow 
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI

file 
diff 
annotate

Tue, 07 Sep 2010 10:05:19 +0200 
nipkow 
expand_fun_eq > ext_iff

file 
diff 
annotate

Thu, 02 Sep 2010 19:51:53 +0200 
hoelzl 
Moved lemmas to appropriate locations

file 
diff 
annotate

Thu, 02 Sep 2010 17:12:40 +0200 
hoelzl 
move lemmas to correct theory files

file 
diff 
annotate

Mon, 23 Aug 2010 19:35:57 +0200 
hoelzl 
Rewrite the Probability theory.

file 
diff 
annotate

Tue, 04 May 2010 18:19:24 +0200 
hoelzl 
Corrected imports; better approximation of dependencies.

file 
diff 
annotate

Mon, 03 May 2010 14:35:10 +0200 
hoelzl 
Cleanup information theory

file 
diff 
annotate

Mon, 03 May 2010 14:35:10 +0200 
hoelzl 
Moved Convex theory to library.

file 
diff 
annotate

Wed, 07 Apr 2010 17:24:44 +0200 
hoelzl 
Added Information theory and Example: dining cryptographers

file 
diff 
annotate
