| Wed, 11 Feb 2015 15:22:37 +0100 |
Andreas Lochbihler |
more lemmas
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:06:57 +0100 |
hoelzl |
merged
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 13:50:30 +0100 |
hoelzl |
add bind_cond_pmf_cancel
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 12:15:05 +0100 |
hoelzl |
add cond_map_pmf
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 12:09:32 +0100 |
hoelzl |
introduce discrete conditional probabilities, use it to simplify bnf proof of pmf
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 12:27:30 +0100 |
Andreas Lochbihler |
tuned proof
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 12:10:26 +0100 |
Andreas Lochbihler |
tune proof
|
file |
diff |
annotate
|
| Fri, 30 Jan 2015 17:29:51 +0100 |
hoelzl |
simp rules for return_pmf
|
file |
diff |
annotate
|
| Thu, 22 Jan 2015 14:51:08 +0100 |
hoelzl |
import general thms from Density_Compiler
|
file |
diff |
annotate
|
| Fri, 09 Jan 2015 10:49:35 +0100 |
hoelzl |
rel_pmf OO: conversion to nat is not necessary
|
file |
diff |
annotate
|
| Fri, 09 Jan 2015 09:16:51 +0100 |
Andreas Lochbihler |
simplify construction for distribution of rel_pmf over op OO
|
file |
diff |
annotate
|
| Fri, 12 Dec 2014 10:58:40 +0100 |
hoelzl |
rel_pmf commutes with rel_prod
|
file |
diff |
annotate
|
| Fri, 05 Dec 2014 13:39:59 +0100 |
hoelzl |
add Poisson and Binomial distribution
|
file |
diff |
annotate
|
| Fri, 05 Dec 2014 12:06:18 +0100 |
hoelzl |
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
|
file |
diff |
annotate
|
| Tue, 25 Nov 2014 17:30:05 +0100 |
hoelzl |
tuned proof that pmfs are bnfs
|
file |
diff |
annotate
|
| Tue, 25 Nov 2014 17:29:39 +0100 |
hoelzl |
projections of pair_pmf (by D. Traytel)
|
file |
diff |
annotate
|
| Mon, 24 Nov 2014 12:20:14 +0100 |
hoelzl |
add congruence solver to measurability prover
|
file |
diff |
annotate
|
| Fri, 21 Nov 2014 12:24:59 +0100 |
Andreas Lochbihler |
add lemma
|
file |
diff |
annotate
|
| Fri, 21 Nov 2014 12:11:44 +0100 |
Andreas Lochbihler |
register pmf as BNF
|
file |
diff |
annotate
|
| Fri, 14 Nov 2014 13:18:33 +0100 |
hoelzl |
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 17:19:52 +0100 |
hoelzl |
import general theorems from AFP/Markov_Models
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 17:00:42 +0200 |
hoelzl |
add transfer rule for set_pmf
|
file |
diff |
annotate
|
| Tue, 07 Oct 2014 10:34:24 +0200 |
hoelzl |
add Giry monad
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 16:27:07 +0200 |
hoelzl |
add type for probability mass functions, i.e. discrete probability distribution
|
file |
diff |
annotate
|