Mercurial
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
branches
|
file
| revisions |
annotate
|
diff
|
rss
src/HOL/Probability/Borel_Space.thy
2011-10-28
hoelzl
2011-10-28
allow to build Probability and MV-Analysis with one ROOT.ML
file
|
diff
|
annotate
2011-09-14
hoelzl
2011-09-14
renamed Complete_Lattices lemmas, removed legacy names
file
|
diff
|
annotate
2011-09-12
nipkow
2011-09-12
new fastforce replacing fastsimp - less confusing name
file
|
diff
|
annotate
2011-09-02
huffman
2011-09-02
remove more duplicate lemmas
file
|
diff
|
annotate
2011-08-26
huffman
2011-08-26
make HOL-Probability respect set/pred distinction
file
|
diff
|
annotate
2011-08-18
huffman
2011-08-18
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
file
|
diff
|
annotate
2011-07-19
hoelzl
2011-07-19
add ereal to typeclass infinity
file
|
diff
|
annotate
2011-07-19
hoelzl
2011-07-19
Rename extreal => ereal
file
|
diff
|
annotate
2011-05-26
hoelzl
2011-05-26
composition of convex and measurable function is measurable
file
|
diff
|
annotate
2011-05-23
hoelzl
2011-05-23
move lemmas to Extended_Reals and Extended_Real_Limits
file
|
diff
|
annotate
2011-05-17
hoelzl
2011-05-17
add borel_eq_atLeastLessThan
file
|
diff
|
annotate
2011-03-29
wenzelm
2011-03-29
tuned headers;
file
|
diff
|
annotate
2011-03-22
hoelzl
2011-03-22
standardized headers
file
|
diff
|
annotate
2011-03-14
hoelzl
2011-03-14
reworked Probability theory: measures are not type restricted to positive extended reals
file
|
diff
|
annotate
2011-03-14
hoelzl
2011-03-14
moved t2_spaces to HOL image
file
|
diff
|
annotate
2011-02-23
hoelzl
2011-02-23
log is borel measurable
file
|
diff
|
annotate
2011-01-14
hoelzl
2011-01-14
tuned formalization of subalgebra
file
|
diff
|
annotate
2010-12-08
hoelzl
2010-12-08
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
file
|
diff
|
annotate
2010-12-08
hoelzl
2010-12-08
integral over setprod
file
|
diff
|
annotate
2010-12-08
haftmann
2010-12-08
work around problems with eta-expansion of equations
file
|
diff
|
annotate
2010-12-08
haftmann
2010-12-08
nice syntax for lattice INFI, SUPR; various *_apply rules for lattice operations on fun; more default simplification rules
file
|
diff
|
annotate
2010-12-06
hoelzl
2010-12-06
folding on arbitrary Lebesgue integrable functions
file
|
diff
|
annotate
2010-12-06
hoelzl
2010-12-06
fixed spelling errors
file
|
diff
|
annotate
2010-12-03
hoelzl
2010-12-03
it is known as the extended reals, not the infinite reals
file
|
diff
|
annotate
2010-12-01
hoelzl
2010-12-01
Tuned setup for borel_measurable with min, max and psuminf.
file
|
diff
|
annotate
2010-12-01
hoelzl
2010-12-01
Replace algebra_eqI by algebra.equality; Move sets_sigma_subset to Sigma_Algebra;
file
|
diff
|
annotate
2010-12-01
hoelzl
2010-12-01
Support product spaces on sigma finite measures. Introduce the almost everywhere quantifier. Introduce 'morphism' theorems for most constants. Prove uniqueness of measures on cut stable generators. Prove uniqueness of the Radon-Nikodym derivative. Removed misleading suffix from borel_space and lebesgue_space. Use product spaces to introduce Fubini on the Lebesgue integral. Combine Euclidean_Lebesgue and Lebesgue_Measure. Generalize theorems about mutual information and entropy to arbitrary probability spaces. Remove simproc mult_log as it does not work with interpretations. Introduce completion of measure spaces. Change type of sigma. Introduce dynkin systems.
file
|
diff
|
annotate
|
base