| #
4dd97d4d |
|
20-Feb-2018 |
paulson <lp15@cam.ac.uk> |
Lots of new material about matrices, etc.
|
| #
229f8947 |
|
29-Jan-2017 |
wenzelm <none@none> |
added inj_def (redundant, analogous to surj_def, bij_def);
tuned proofs;
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
a5d16d15 |
|
29-Sep-2016 |
hoelzl <none@none> |
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
--HG--
extra : rebase_source : 1dd56fb9b7e10114813c9a20fb209cc08f283d12
|
| #
0bd59400 |
|
10-Aug-2016 |
wenzelm <none@none> |
tuned proofs;
|
| #
b75f21d1 |
|
16-Jun-2016 |
wenzelm <none@none> |
tuned;
|
| #
94ba250a |
|
17-May-2016 |
eberlm <none@none> |
Moved material from AFP/Randomised_Social_Choice to distribution
|
| #
1daf8189 |
|
13-May-2016 |
wenzelm <none@none> |
eliminated use of empty "assms";
|
| #
5d907b91 |
|
17-Mar-2016 |
hoelzl <none@none> |
more stuff for extended nonnegative real numbers
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
6d3e0a15 |
|
29-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
d42838c4 |
|
28-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
375ba3ef |
|
11-Nov-2015 |
Andreas Lochbihler <none@none> |
add lemmas
|
| #
6f0c89b5 |
|
26-Jun-2015 |
wenzelm <none@none> |
tuned whitespace;
|
| #
a0af5cdd |
|
17-Jun-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
92a516b8 |
|
14-Nov-2014 |
hoelzl <none@none> |
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
|
| #
34a3534a |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
a7682ac4 |
|
20-Oct-2014 |
hoelzl <none@none> |
add tendsto_const and tendsto_ident_at as simp and intro rules
--HG--
extra : rebase_source : 22eac3c1e90ec123e3d2513334c670b5eb22d7e7
|
| #
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
|
| #
b2dd2600 |
|
30-Jun-2014 |
hoelzl <none@none> |
some lemmas about the indicator function; removed lemma sums_def2
--HG--
extra : rebase_source : 9ae9272141b62f9a284c2547ec1e24d4f1edf4e5
|
| #
bf4e83d3 |
|
28-Jun-2014 |
haftmann <none@none> |
fact consolidation
|
| #
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
|
| #
df9a19dd |
|
12-Nov-2013 |
hoelzl <none@none> |
equation when indicator function equals 0 or 1
|
| #
23ca6e88 |
|
09-Nov-2011 |
wenzelm <none@none> |
avoid inconsistent sort constraints;
|
| #
7569156a |
|
01-Jul-2010 |
hoelzl <none@none> |
Add theory for indicator function.
|