#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
9f786ce6 |
|
17-Jan-2017 |
wenzelm <none@none> |
more symbols via abbrevs;
|
#
593ff4b4 |
|
17-Oct-2016 |
nipkow <none@none> |
setprod -> prod
|
#
fad39d02 |
|
30-Sep-2016 |
hoelzl <none@none> |
HOL-Probability: more about probability, prepare for Markov processes in the AFP --HG-- extra : rebase_source : f90e6cf5c47f7a2604d0eeacaf0181f3cfe64a14
|
#
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
|
#
14001a0d |
|
22-Jul-2016 |
wenzelm <none@none> |
tuned proofs -- avoid unstructured calculation;
|
#
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
|
#
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
#
6d3e0a15 |
|
29-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
#
8e83c9d2 |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
7fd06540 |
|
04-Nov-2015 |
ballarin <none@none> |
Qualifiers in locale expressions default to mandatory regardless of the command.
|
#
f3752ace |
|
08-Oct-2015 |
hoelzl <none@none> |
generalize eqI theorems for product measures --HG-- extra : rebase_source : 8ba647ae0abab594ceca74071725a61b9f84472e
|
#
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
|
#
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
#
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
#
f8e9ab7b |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
#
737ce617 |
|
04-Sep-2014 |
hoelzl <none@none> |
cleanup Wfrec; introduce dependent_wf/wellorder_choice --HG-- extra : rebase_source : f2bcd9c9ab7554ffc3fe445f9603d177ca3724e7
|
#
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
#
bf4e83d3 |
|
28-Jun-2014 |
haftmann <none@none> |
fact consolidation
|
#
f281533d |
|
19-May-2014 |
hoelzl <none@none> |
renamed positive_integral to nn_integral --HG-- extra : rebase_source : e7a432bee0942b6330cadfd1eb5da8e326238e06
|
#
dd44ffb4 |
|
20-Feb-2014 |
blanchet <none@none> |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
#
aff8c6a4 |
|
12-Feb-2014 |
blanchet <none@none> |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
|
#
40e0ba91 |
|
12-Feb-2014 |
blanchet <none@none> |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
#
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
#
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;
|
#
f4d4f9e9 |
|
05-Mar-2013 |
hoelzl <none@none> |
generalized lemmas in Extended_Real_Limits
|
#
a51f97fb |
|
28-Nov-2012 |
wenzelm <none@none> |
eliminated slightly odd identifiers;
|
#
ba5f9f86 |
|
27-Nov-2012 |
immler <none@none> |
qualified interpretation of sigma_algebra, to avoid name clashes --HG-- extra : rebase_source : aaeab4e40463c23ef5a5a07ee360db0335376105
|
#
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
|
#
6b883201 |
|
16-Nov-2012 |
hoelzl <none@none> |
measurability for nat_case and comb_seq
|
#
81100640 |
|
16-Nov-2012 |
immler <none@none> |
renamed to more appropriate lim_P for projective limit
|
#
0af98a2c |
|
15-Nov-2012 |
immler <none@none> |
regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards --HG-- extra : rebase_source : f535a1f0a613567ad927269eca5c0ba4e00f737b
|
#
c931d9ef |
|
09-Nov-2012 |
immler@in.tum.de <immler@in.tum.de> |
moved lemmas into projective_family; added header for theory Projective_Family
|
#
a470030a |
|
09-Nov-2012 |
immler@in.tum.de <immler@in.tum.de> |
removed redundant/unnecessary assumptions from projective_family --HG-- extra : rebase_source : 31291167471e134480d8b83cfc14a4f96008f522
|
#
6f87109b |
|
07-Nov-2012 |
immler@in.tum.de <immler@in.tum.de> |
assume probability spaces; allow empty index set --HG-- extra : rebase_source : b3d95630019975c608692231481caa8c9db431aa
|
#
4c752152 |
|
07-Nov-2012 |
immler@in.tum.de <immler@in.tum.de> |
added projective_family; generalized generator in product_prob_space to projective_family --HG-- extra : rebase_source : 841ddd7f5a7409751925f93c41f6429a7160c7a4
|
#
1f977b74 |
|
06-Nov-2012 |
immler@in.tum.de <immler@in.tum.de> |
moved lemmas further up --HG-- extra : rebase_source : 4c6685cd2523ee2d6bc5c3519495244644f2e8cc
|
#
fde36cfd |
|
02-Nov-2012 |
hoelzl <none@none> |
use measurability prover
|
#
bdfc83c7 |
|
02-Nov-2012 |
hoelzl <none@none> |
infinite product measure is invariant under adding prefixes
|
#
f3f961d4 |
|
09-Oct-2012 |
hoelzl <none@none> |
infprod generator works also with empty index set
|
#
f104dba4 |
|
09-Oct-2012 |
hoelzl <none@none> |
remove incseq assumption from measure_eqI_generator_eq
|
#
eb33a928 |
|
09-Oct-2012 |
hoelzl <none@none> |
merge should operate on pairs
|
#
73a18021 |
|
09-Oct-2012 |
hoelzl <none@none> |
tuned product measurability
|
#
6e6e572a |
|
25-Apr-2012 |
hoelzl <none@none> |
add Caratheodories theorem for semi-rings of sets
|
#
11c87ed0 |
|
22-Apr-2012 |
hoelzl <none@none> |
reworked Probability theory --HG-- extra : rebase_source : 04bef352ab6c7feafcf64ecca49fecffac43bb41
|
#
95291102 |
|
13-Mar-2012 |
wenzelm <none@none> |
prefer abs_def over def_raw;
|
#
a3193ed0 |
|
13-Mar-2012 |
wenzelm <none@none> |
tuned proofs -- eliminated pointless chaining of facts after 'interpret';
|
#
33cd0191 |
|
28-Feb-2012 |
wenzelm <none@none> |
avoid undeclared variables in let bindings; tuned proofs;
|
#
f083f9a4 |
|
07-Dec-2011 |
hoelzl <none@none> |
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
|
#
7e65ae14 |
|
14-Sep-2011 |
hoelzl <none@none> |
renamed Complete_Lattices lemmas, removed legacy names
|
#
7f546ab9 |
|
19-Jul-2011 |
hoelzl <none@none> |
Rename extreal => ereal --HG-- rename : src/HOL/Library/Extended_Reals.thy => src/HOL/Library/Extended_Real.thy
|
#
6000a27b |
|
05-Jul-2011 |
hoelzl <none@none> |
rename lemma Infinite_Product_Measure.sigma_sets_subseteq, it hides Sigma_Algebra.sigma_sets_subseteq
|
#
e7dc5e83 |
|
23-May-2011 |
hoelzl <none@none> |
move lemmas to Extended_Reals and Extended_Real_Limits
|
#
9d453186 |
|
17-May-2011 |
hoelzl <none@none> |
the measurable sets with null measure form a ring
|
#
06c0f07e |
|
16-May-2011 |
hoelzl <none@none> |
add some lemmas for infinite product measure
|
#
132b8521 |
|
05-Apr-2011 |
hoelzl <none@none> |
prove measurable_into_infprod_algebra and measure_infprod
|
#
ed5d29c5 |
|
30-Mar-2011 |
hoelzl <none@none> |
products of probability measures are probability measures
|
#
de7c70f0 |
|
29-Mar-2011 |
hoelzl <none@none> |
rename Probability_Space to Probability_Measure --HG-- rename : src/HOL/Probability/Probability_Space.thy => src/HOL/Probability/Probability_Measure.thy
|
#
1b75a356 |
|
29-Mar-2011 |
hoelzl <none@none> |
add infinite product measure
|