#
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
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;
|
#
593ff4b4 |
|
17-Oct-2016 |
nipkow <none@none> |
setprod -> prod
|
#
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
#
fad39d02 |
|
30-Sep-2016 |
hoelzl <none@none> |
HOL-Probability: more about probability, prepare for Markov processes in the AFP --HG-- extra : rebase_source : f90e6cf5c47f7a2604d0eeacaf0181f3cfe64a14
|
#
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
|
#
53d65c13 |
|
08-Aug-2016 |
hoelzl <none@none> |
rename HOL-Multivariate_Analysis to HOL-Analysis. --HG-- rename : src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy => src/HOL/Analysis/Analysis.thy rename : src/HOL/Multivariate_Analysis/Binary_Product_Measure.thy => src/HOL/Analysis/Binary_Product_Measure.thy rename : src/HOL/Multivariate_Analysis/Bochner_Integration.thy => src/HOL/Analysis/Bochner_Integration.thy rename : src/HOL/Multivariate_Analysis/Borel_Space.thy => src/HOL/Analysis/Borel_Space.thy rename : src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy => src/HOL/Analysis/Bounded_Continuous_Function.thy rename : src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy => src/HOL/Analysis/Bounded_Linear_Function.thy rename : src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy => src/HOL/Analysis/Brouwer_Fixpoint.thy rename : src/HOL/Multivariate_Analysis/Caratheodory.thy => src/HOL/Analysis/Caratheodory.thy rename : src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy => src/HOL/Analysis/Cartesian_Euclidean_Space.thy rename : src/HOL/Multivariate_Analysis/Cauchy_Integral_Theorem.thy => src/HOL/Analysis/Cauchy_Integral_Theorem.thy rename : src/HOL/Multivariate_Analysis/Complete_Measure.thy => src/HOL/Analysis/Complete_Measure.thy rename : src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy => src/HOL/Analysis/Complex_Analysis_Basics.thy rename : src/HOL/Multivariate_Analysis/Complex_Transcendental.thy => src/HOL/Analysis/Complex_Transcendental.thy rename : src/HOL/Multivariate_Analysis/Conformal_Mappings.thy => src/HOL/Analysis/Conformal_Mappings.thy rename : src/HOL/Multivariate_Analysis/Continuous_Extension.thy => src/HOL/Analysis/Continuous_Extension.thy rename : src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy => src/HOL/Analysis/Convex_Euclidean_Space.thy rename : src/HOL/Multivariate_Analysis/Derivative.thy => src/HOL/Analysis/Derivative.thy rename : src/HOL/Multivariate_Analysis/Determinants.thy => src/HOL/Analysis/Determinants.thy rename : src/HOL/Multivariate_Analysis/Embed_Measure.thy => src/HOL/Analysis/Embed_Measure.thy rename : src/HOL/Multivariate_Analysis/Euclidean_Space.thy => src/HOL/Analysis/Euclidean_Space.thy rename : src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy => src/HOL/Analysis/Extended_Real_Limits.thy rename : src/HOL/Multivariate_Analysis/Fashoda_Theorem.thy => src/HOL/Analysis/Fashoda_Theorem.thy rename : src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy => src/HOL/Analysis/Finite_Cartesian_Product.thy rename : src/HOL/Multivariate_Analysis/Finite_Product_Measure.thy => src/HOL/Analysis/Finite_Product_Measure.thy rename : src/HOL/Multivariate_Analysis/Gamma_Function.thy => src/HOL/Analysis/Gamma_Function.thy rename : src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy => src/HOL/Analysis/Generalised_Binomial_Theorem.thy rename : src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy => src/HOL/Analysis/Harmonic_Numbers.thy rename : src/HOL/Multivariate_Analysis/Henstock_Kurzweil_Integration.thy => src/HOL/Analysis/Henstock_Kurzweil_Integration.thy rename : src/HOL/Multivariate_Analysis/Homeomorphism.thy => src/HOL/Analysis/Homeomorphism.thy rename : src/HOL/Multivariate_Analysis/Integral_Test.thy => src/HOL/Analysis/Integral_Test.thy rename : src/HOL/Multivariate_Analysis/Interval_Integral.thy => src/HOL/Analysis/Interval_Integral.thy rename : src/HOL/Multivariate_Analysis/L2_Norm.thy => src/HOL/Analysis/L2_Norm.thy rename : src/HOL/Multivariate_Analysis/Lebesgue_Integral_Substitution.thy => src/HOL/Analysis/Lebesgue_Integral_Substitution.thy rename : src/HOL/Multivariate_Analysis/Lebesgue_Measure.thy => src/HOL/Analysis/Lebesgue_Measure.thy rename : src/HOL/Multivariate_Analysis/Linear_Algebra.thy => src/HOL/Analysis/Linear_Algebra.thy rename : src/HOL/Multivariate_Analysis/Measurable.thy => src/HOL/Analysis/Measurable.thy rename : src/HOL/Multivariate_Analysis/Measure_Space.thy => src/HOL/Analysis/Measure_Space.thy rename : src/HOL/Multivariate_Analysis/Nonnegative_Lebesgue_Integration.thy => src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy rename : src/HOL/Multivariate_Analysis/Norm_Arith.thy => src/HOL/Analysis/Norm_Arith.thy rename : src/HOL/Multivariate_Analysis/Operator_Norm.thy => src/HOL/Analysis/Operator_Norm.thy rename : src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy => src/HOL/Analysis/Ordered_Euclidean_Space.thy rename : src/HOL/Multivariate_Analysis/Path_Connected.thy => src/HOL/Analysis/Path_Connected.thy rename : src/HOL/Multivariate_Analysis/Poly_Roots.thy => src/HOL/Analysis/Poly_Roots.thy rename : src/HOL/Multivariate_Analysis/Polytope.thy => src/HOL/Analysis/Polytope.thy rename : src/HOL/Multivariate_Analysis/Radon_Nikodym.thy => src/HOL/Analysis/Radon_Nikodym.thy rename : src/HOL/Multivariate_Analysis/Regularity.thy => src/HOL/Analysis/Regularity.thy rename : src/HOL/Multivariate_Analysis/Set_Integral.thy => src/HOL/Analysis/Set_Integral.thy rename : src/HOL/Multivariate_Analysis/Sigma_Algebra.thy => src/HOL/Analysis/Sigma_Algebra.thy rename : src/HOL/Multivariate_Analysis/Summation_Tests.thy => src/HOL/Analysis/Summation_Tests.thy rename : src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy => src/HOL/Analysis/Topology_Euclidean_Space.thy rename : src/HOL/Multivariate_Analysis/Uniform_Limit.thy => src/HOL/Analysis/Uniform_Limit.thy rename : src/HOL/Multivariate_Analysis/Weierstrass_Theorems.thy => src/HOL/Analysis/Weierstrass_Theorems.thy rename : src/HOL/Multivariate_Analysis/document/root.tex => src/HOL/Analysis/document/root.tex rename : src/HOL/Multivariate_Analysis/ex/Approximations.thy => src/HOL/Analysis/ex/Approximations.thy rename : src/HOL/Multivariate_Analysis/measurable.ML => src/HOL/Analysis/measurable.ML rename : src/HOL/Multivariate_Analysis/normarith.ML => src/HOL/Analysis/normarith.ML
|
#
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
|
#
94ba250a |
|
17-May-2016 |
eberlm <none@none> |
Moved material from AFP/Randomised_Social_Choice to distribution
|
#
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
|
#
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
#
5ad25152 |
|
05-Jan-2016 |
hoelzl <none@none> |
add the proof of the central limit theorem --HG-- extra : rebase_source : 493d99e28392771c51f4102a11b90533880e289f extra : amend_source : 3fb7b7c607104e57a2c3ba7f733dd570eb42fa3b
|
#
474064bd |
|
09-Dec-2015 |
paulson <lp15@cam.ac.uk> |
sorted out eventually_mono
|
#
8e83c9d2 |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
be9ace2b |
|
09-Nov-2015 |
wenzelm <none@none> |
qualifier is mandatory by default;
|
#
7fd06540 |
|
04-Nov-2015 |
ballarin <none@none> |
Qualifiers in locale expressions default to mandatory regardless of the command.
|
#
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
#
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;
|
#
4930226f |
|
06-Sep-2015 |
haftmann <none@none> |
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
|
#
0ed8f303 |
|
22-Jan-2015 |
Andreas Lochbihler <none@none> |
generalise lemma
|
#
6c7ab2bf |
|
22-Jan-2015 |
hoelzl <none@none> |
import general thms from Density_Compiler --HG-- extra : rebase_source : 48a3b47f755d8099564008b93076eae81453a674
|
#
071e4dc0 |
|
14-Jan-2015 |
Andreas Lochbihler <none@none> |
allow line breaks in probability syntax
|
#
fa19e9d0 |
|
13-Jan-2015 |
hoelzl <none@none> |
measurability prover: removed app splitting, replaced by more powerful destruction rules
|
#
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
#
f8e9ab7b |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
#
eef0bf84 |
|
22-Oct-2014 |
Andreas Lochbihler <none@none> |
add print translation for probability notation \<P>
|
#
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
|
#
33db321f |
|
12-Jun-2014 |
hoelzl <none@none> |
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav) --HG-- extra : rebase_source : b821e7a52658fa32f598433901729ddc5fc949dd
|
#
18c12fa6 |
|
20-May-2014 |
hoelzl <none@none> |
add various lemmas
|
#
f281533d |
|
19-May-2014 |
hoelzl <none@none> |
renamed positive_integral to nn_integral --HG-- extra : rebase_source : e7a432bee0942b6330cadfd1eb5da8e326238e06
|
#
ab027a86 |
|
19-May-2014 |
hoelzl <none@none> |
fixed document generation for HOL-Probability
|
#
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
|
#
4f5ebd94 |
|
16-Mar-2014 |
haftmann <none@none> |
normalising simp rules for compound operators
|
#
e808a13b |
|
12-Nov-2013 |
hoelzl <none@none> |
measure of a countable union
|
#
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
#
619117b4 |
|
10-Apr-2013 |
hoelzl <none@none> |
generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
|
#
f983e67a |
|
22-Mar-2013 |
hoelzl <none@none> |
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
|
#
1cbdc003 |
|
07-Dec-2012 |
hoelzl <none@none> |
add exponential and uniform distributions
|
#
ba5f9f86 |
|
27-Nov-2012 |
immler <none@none> |
qualified interpretation of sigma_algebra, to avoid name clashes --HG-- extra : rebase_source : aaeab4e40463c23ef5a5a07ee360db0335376105
|
#
22db1436 |
|
16-Nov-2012 |
hoelzl <none@none> |
move theorems to be more generally useable --HG-- extra : rebase_source : c1c0d1f5576f4d469d1b4618663774e2f297a214
|
#
4adc9523 |
|
16-Nov-2012 |
hoelzl <none@none> |
rules for AE and prob
|
#
fde36cfd |
|
02-Nov-2012 |
hoelzl <none@none> |
use measurability prover
|
#
e7b50b43 |
|
02-Nov-2012 |
hoelzl <none@none> |
add measurability prover; add support for Borel sets
|
#
8e603759 |
|
02-Nov-2012 |
hoelzl <none@none> |
add syntax and a.e.-rules for (conditional) probability on predicates
|
#
bc86b8cc |
|
09-Oct-2012 |
hoelzl <none@none> |
joint distribution of independent variables
|
#
2cfd7071 |
|
09-Oct-2012 |
hoelzl <none@none> |
show and use distributed_swap and distributed_jointI
|
#
78bc643f |
|
09-Oct-2012 |
hoelzl <none@none> |
continuous version of entropy_le
|
#
60c88875 |
|
09-Oct-2012 |
hoelzl <none@none> |
generalize from prob_space to finite_measure
|
#
73a18021 |
|
09-Oct-2012 |
hoelzl <none@none> |
tuned product measurability
|
#
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;
|
#
efc317e6 |
|
20-Dec-2011 |
noschinl <none@none> |
add simp rules for enat and ereal
|
#
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
|
#
d5c9d81f |
|
01-Dec-2011 |
hoelzl <none@none> |
moved theorems about distribution to the definition; removed oopsed-lemma
|
#
4150e14d |
|
01-Dec-2011 |
hoelzl <none@none> |
rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution
|
#
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
#
7f546ab9 |
|
19-Jul-2011 |
hoelzl <none@none> |
Rename extreal => ereal --HG-- rename : src/HOL/Library/Extended_Reals.thy => src/HOL/Library/Extended_Real.thy
|
#
1fdf7774 |
|
04-Jul-2011 |
hoelzl <none@none> |
the borel probability measure is easier to handle with {0 ..< 1} (coverable by disjoint intervals {_ ..< _})
|
#
78fb9bbf |
|
27-Jun-2011 |
hoelzl <none@none> |
move conditional expectation to its own theory file
|
#
04d61436 |
|
09-Jun-2011 |
hoelzl <none@none> |
lemma: independence is equal to mutual information = 0
|
#
33bd0504 |
|
09-Jun-2011 |
hoelzl <none@none> |
jensens inequality
|
#
2e23b219 |
|
26-May-2011 |
hoelzl <none@none> |
integral strong monotone; finite subadditivity for measure
|
#
3b282378 |
|
26-May-2011 |
hoelzl <none@none> |
add lemma indep_distribution_eq_measure
|
#
1efdcfb6 |
|
26-May-2011 |
hoelzl <none@none> |
add lemma indep_sets_collect_sigma
|
#
e7dc5e83 |
|
23-May-2011 |
hoelzl <none@none> |
move lemmas to Extended_Reals and Extended_Real_Limits
|
#
1134420c |
|
20-May-2011 |
hoelzl <none@none> |
Add restricted borel measure to {0 .. 1}
|
#
295e9a5e |
|
20-May-2011 |
hoelzl <none@none> |
add lemma prob_finite_product
|
#
9eaed9c4 |
|
19-May-2011 |
hoelzl <none@none> |
add Bernoulli space
|
#
45663afe |
|
19-May-2011 |
hoelzl <none@none> |
add product of probability spaces with finite cardinality
|
#
120e9718 |
|
19-May-2011 |
hoelzl <none@none> |
remove double sum_over_space_real_distribution
|
#
41efd578 |
|
01-Apr-2011 |
hoelzl <none@none> |
remove unnecessary prob_preserving
|
#
9e0c4c87 |
|
01-Apr-2011 |
hoelzl <none@none> |
add prob_space_vimage
|
#
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
|