| #
ab32308e |
|
21-Jan-2019 |
paulson <lp15@cam.ac.uk> |
renamings and new material
|
| #
97b2ecf5 |
|
08-Nov-2018 |
haftmann <none@none> |
removed relics of ASCII syntax for indexed big operators
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
c2d49d41 |
|
17-Aug-2017 |
eberlm <eberlm@in.tum.de> |
Replaced subseq with strict_mono
|
| #
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
|
| #
bef11030 |
|
15-Sep-2016 |
Lars Hupel <lars.hupel@mytum.de> |
new type for finite maps; use it in HOL-Probability
|
| #
9e5f909f |
|
05-Aug-2016 |
hoelzl <none@none> |
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
--HG--
rename : src/HOL/Probability/Binary_Product_Measure.thy => src/HOL/Multivariate_Analysis/Binary_Product_Measure.thy
rename : src/HOL/Probability/Bochner_Integration.thy => src/HOL/Multivariate_Analysis/Bochner_Integration.thy
rename : src/HOL/Probability/Borel_Space.thy => src/HOL/Multivariate_Analysis/Borel_Space.thy
rename : src/HOL/Probability/Caratheodory.thy => src/HOL/Multivariate_Analysis/Caratheodory.thy
rename : src/HOL/Probability/Complete_Measure.thy => src/HOL/Multivariate_Analysis/Complete_Measure.thy
rename : src/HOL/Probability/Embed_Measure.thy => src/HOL/Multivariate_Analysis/Embed_Measure.thy
rename : src/HOL/Probability/Finite_Product_Measure.thy => src/HOL/Multivariate_Analysis/Finite_Product_Measure.thy
rename : src/HOL/Probability/Interval_Integral.thy => src/HOL/Multivariate_Analysis/Interval_Integral.thy
rename : src/HOL/Probability/Lebesgue_Integral_Substitution.thy => src/HOL/Multivariate_Analysis/Lebesgue_Integral_Substitution.thy
rename : src/HOL/Probability/Lebesgue_Measure.thy => src/HOL/Multivariate_Analysis/Lebesgue_Measure.thy
rename : src/HOL/Probability/Measurable.thy => src/HOL/Multivariate_Analysis/Measurable.thy
rename : src/HOL/Probability/Measure_Space.thy => src/HOL/Multivariate_Analysis/Measure_Space.thy
rename : src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy => src/HOL/Multivariate_Analysis/Nonnegative_Lebesgue_Integration.thy
rename : src/HOL/Probability/Radon_Nikodym.thy => src/HOL/Multivariate_Analysis/Radon_Nikodym.thy
rename : src/HOL/Probability/Regularity.thy => src/HOL/Multivariate_Analysis/Regularity.thy
rename : src/HOL/Probability/Set_Integral.thy => src/HOL/Multivariate_Analysis/Set_Integral.thy
rename : src/HOL/Probability/Sigma_Algebra.thy => src/HOL/Multivariate_Analysis/Sigma_Algebra.thy
rename : src/HOL/Probability/measurable.ML => src/HOL/Multivariate_Analysis/measurable.ML
extra : rebase_source : 30ab39c42165c1c5622833cf256065cbfff030f9
|
| #
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
|
| #
15ee6658 |
|
24-Feb-2016 |
paulson <lp15@cam.ac.uk> |
Substantial new material for multivariate analysis. Also removal of some duplicates.
|
| #
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;
|
| #
53483153 |
|
16-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
|
| #
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.
|
| #
be9ace2b |
|
09-Nov-2015 |
wenzelm <none@none> |
qualifier is mandatory by default;
|
| #
6daef852 |
|
27-Oct-2015 |
paulson <lp15@cam.ac.uk> |
Cauchy's integral formula, required lemmas, and a bit of reorganisation
|
| #
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
|
| #
5cdcf3d3 |
|
28-Jul-2015 |
paulson <lp15@cam.ac.uk> |
the Cauchy integral theorem and related material
|
| #
6f0c89b5 |
|
26-Jun-2015 |
wenzelm <none@none> |
tuned whitespace;
|
| #
f8e9ab7b |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
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
|
| #
4cda3a80 |
|
18-Mar-2014 |
hoelzl <none@none> |
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
|
| #
7237bdd9 |
|
02-Sep-2013 |
wenzelm <none@none> |
tuned proofs -- clarified flow of facts wrt. calculation;
|
| #
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
| #
7189af92 |
|
17-Jul-2013 |
immler <none@none> |
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
|
| #
f4d4f9e9 |
|
05-Mar-2013 |
hoelzl <none@none> |
generalized lemmas in Extended_Real_Limits
|
| #
7fe17c3e |
|
18-Jan-2013 |
hoelzl <none@none> |
tune prove compact_eq_totally_bounded
|
| #
0ca9348e |
|
14-Jan-2013 |
hoelzl <none@none> |
differentiate (cover) compactness and sequential compactness
--HG--
extra : rebase_source : 616a2c5ff07a4cf13ca9187e8c8fa1d191d0fcc6
|
| #
a51f97fb |
|
28-Nov-2012 |
wenzelm <none@none> |
eliminated slightly odd identifiers;
|
| #
21822db4 |
|
27-Nov-2012 |
immler <none@none> |
based countable topological basis on Countable_Set
--HG--
extra : rebase_source : 326111b06e0d89bbbef5c168b8314ab6023d8fb2
|
| #
ba5f9f86 |
|
27-Nov-2012 |
immler <none@none> |
qualified interpretation of sigma_algebra, to avoid name clashes
--HG--
extra : rebase_source : aaeab4e40463c23ef5a5a07ee360db0335376105
|
| #
8867b83b |
|
22-Nov-2012 |
immler <none@none> |
eliminated finite_set_sequence with countable set
--HG--
extra : rebase_source : 92fc5c9511c5c9169b8664781eeabf3c636e337a
|
| #
0859e8ef |
|
19-Nov-2012 |
hoelzl <none@none> |
tuned: use induction rule sigma_sets_induct_disjoint
--HG--
extra : rebase_source : ccec2d4dbff6f08b46c1149b2cf945c12f5de742
|
| #
a0853ad0 |
|
19-Nov-2012 |
hoelzl <none@none> |
tuned FinMap
--HG--
extra : rebase_source : 8291b62bb69ca72f48d94c100f98e12c28076978
|
| #
2e3f9613 |
|
18-Nov-2012 |
hoelzl <none@none> |
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
--HG--
extra : rebase_source : e65af8d29763871aedf04aed10bdeb869effca0b
|
| #
652a0bf3 |
|
16-Nov-2012 |
hoelzl <none@none> |
renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space
|
| #
81100640 |
|
16-Nov-2012 |
immler <none@none> |
renamed to more appropriate lim_P for projective limit
|
| #
08adb1df |
|
15-Nov-2012 |
immler <none@none> |
corrected headers
|
| #
cd4516de |
|
15-Nov-2012 |
immler <none@none> |
hide constants of auxiliary type finmap
|
| #
de502a80 |
|
15-Nov-2012 |
immler <none@none> |
added projective limit;
proof is based on auxiliary type finmap::polish_space
--HG--
extra : rebase_source : 08af71f8dedbbe8cb079512c97691cc68592d86f
|