| #
a4784f6f |
|
09-Oct-2019 |
haftmann <none@none> |
dedicated fact collections for algebraic simplification rules potentially splitting goals
--HG--
extra : rebase_source : ebbd8d0c13409f8fb536c42910e904c24e43dbe6
|
| #
e6ca3b44 |
|
17-Jul-2019 |
paulson <lp15@cam.ac.uk> |
a few new lemmas and a bit of tidying
|
| #
b15d33eb |
|
13-Apr-2018 |
paulson <lp15@cam.ac.uk> |
Probability builds with new definitions
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
9a8c3fb3 |
|
19-Sep-2016 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
| #
78a9e4a8 |
|
16-Sep-2016 |
hoelzl <none@none> |
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
--HG--
extra : rebase_source : 0321297c249a436ca0371010a76a1a026dd33222
|
| #
14001a0d |
|
22-Jul-2016 |
wenzelm <none@none> |
tuned proofs -- avoid unstructured calculation;
|
| #
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def';
tuned comments;
|
| #
79d3be54 |
|
14-Apr-2016 |
hoelzl <none@none> |
Probability: move emeasure and nn_integral from ereal to ennreal
--HG--
extra : rebase_source : 5f2ac8a84abb43927a58086db8bbe10e190b2e77
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
82353fd1 |
|
30-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
6d3e0a15 |
|
29-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
8e83c9d2 |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
3f106d8a |
|
10-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
| #
23d5df30 |
|
07-Oct-2015 |
hoelzl <none@none> |
cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
--HG--
extra : rebase_source : cffce7b3e322f3c274d9117a0dfdd311d4ba66a1
|
| #
48d44d43 |
|
17-Mar-2015 |
paulson <lp15@cam.ac.uk> |
Inserted real_of_nat to fix factorial-related problem
|
| #
3e14dd10 |
|
16-Mar-2015 |
paulson <lp15@cam.ac.uk> |
The factorial function, "fact", now has type "nat => 'a"
|
| #
e54b5053 |
|
04-Mar-2015 |
nipkow <none@none> |
Removed the obsolete functions "natfloor" and "natceiling"
|
| #
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
| #
f8e9ab7b |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
3c2ea5d6 |
|
19-Oct-2014 |
haftmann <none@none> |
prefer generic elimination rules for even/odd over specialized unfold rules for nat
|
| #
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
| #
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
| #
6c0336e5 |
|
30-Jun-2014 |
hoelzl <none@none> |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
--HG--
extra : rebase_source : 03b2468f7b324b9d8add229ae59776b447283141
|
| #
bf4e83d3 |
|
28-Jun-2014 |
haftmann <none@none> |
fact consolidation
|
| #
58c27ade |
|
17-Jun-2014 |
hoelzl <none@none> |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
--HG--
extra : rebase_source : cd4a9d91f2d415deaa6fd3411b5402ef770d74d2
|
| #
b0ac0132 |
|
16-Jun-2014 |
hoelzl <none@none> |
lemmas about the moments of the normal distribution
--HG--
extra : rebase_source : 614b198c1b9b5c3111bc69c44d5d82348aa23b61
|
| #
69ece7a6 |
|
13-Jun-2014 |
hoelzl <none@none> |
properties of normal distributed random variables (by Sudeep Kanav)
|
| #
33db321f |
|
12-Jun-2014 |
hoelzl <none@none> |
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
--HG--
extra : rebase_source : b821e7a52658fa32f598433901729ddc5fc949dd
|
| #
f281533d |
|
19-May-2014 |
hoelzl <none@none> |
renamed positive_integral to nn_integral
--HG--
extra : rebase_source : e7a432bee0942b6330cadfd1eb5da8e326238e06
|
| #
1a8832ef |
|
18-May-2014 |
hoelzl <none@none> |
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
--HG--
rename : src/HOL/Probability/Lebesgue_Integration.thy => src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
|
| #
66804330 |
|
14-Apr-2014 |
hoelzl <none@none> |
added divide_nonneg_nonneg and co; made it a simp rule
--HG--
extra : rebase_source : 998eadb7cfbf8720cf961ac2e149ce4537557a47
|
| #
a444e184 |
|
11-Apr-2014 |
nipkow <none@none> |
made mult_nonneg_nonneg a simp rule
--HG--
extra : rebase_source : 3f70ac991fa0f02839309ce9b8f418ff53f87c36
|
| #
85993f65 |
|
03-Apr-2014 |
hoelzl <none@none> |
merged DERIV_intros, has_derivative_intros into derivative_intros
|
| #
b50566a5 |
|
02-Apr-2014 |
hoelzl <none@none> |
extend continuous_intros; remove continuous_on_intros and isCont_intros
|
| #
f2e72a6a |
|
18-Aug-2013 |
wenzelm <none@none> |
more symbols;
|
| #
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
| #
1cbdc003 |
|
07-Dec-2012 |
hoelzl <none@none> |
add exponential and uniform distributions
|