dynkin -> Dynkin

removed legacy input syntax

removed legacy input syntax

Prefix form of infix with * on either side no longer needs special treatment
because (* and *) are no longer comment brackets in terms.

ran isabelle update_op on all sources

setprod -> prod

setsum -> sum

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

eliminated old 'def';
tuned comments;

Probability: move emeasure and nn_integral from ereal to ennreal

--HG--
extra : rebase_source : 5f2ac8a84abb43927a58086db8bbe10e190b2e77

more canonical names

prefer abbreviations for compound operators INFIMUM and SUPREMUM

isabelle update_cartouches -c -t;

cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution

--HG--
extra : rebase_source : cffce7b3e322f3c274d9117a0dfdd311d4ba66a1

import general theorems from AFP/Markov_Models

modernized header;

reduced name variants for assoc and commute on plus and mult

import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure

--HG--
extra : rebase_source : 03b2468f7b324b9d8add229ae59776b447283141

fact consolidation

properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)

--HG--
extra : rebase_source : b821e7a52658fa32f598433901729ddc5fc949dd

more complete set of lemmas wrt. image and composition

renamed '{prod,sum,bool,unit}_case' to 'case_...'

standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;

qualified interpretation of sigma_algebra, to avoid name clashes

--HG--
extra : rebase_source : aaeab4e40463c23ef5a5a07ee360db0335376105

merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure

--HG--
extra : rebase_source : e65af8d29763871aedf04aed10bdeb869effca0b

move theorems to be more generally useable

--HG--
extra : rebase_source : c1c0d1f5576f4d469d1b4618663774e2f297a214

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

add support for function application to measurability prover

--HG--
extra : rebase_source : a513410ce6805bf3ef64d93094df14352d5e4753

use measurability prover

joint distribution of independent variables

indep_vars does not need sigma-sets

remove incseq assumption from measure_eqI_generator_eq

simplified assumptions for kolmogorov_0_1_law

tuned product measurability

rename terminal_events to tail_event

reworked Probability theory

--HG--
extra : rebase_source : 04bef352ab6c7feafcf64ecca49fecffac43bb41

avoid undeclared variables in let bindings;
tuned proofs;

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

remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas

Rename extreal => ereal

--HG--
rename : src/HOL/Library/Extended_Reals.thy => src/HOL/Library/Extended_Real.thy

lemma: independence is equal to mutual information = 0

introduce independence of two random variables

add lemma indep_distribution_eq_measure

add lemma indep_rv_finite

add lemma borel_0_1_law

use abbrevitation events == sets M

add lemma kolmogorov_0_1_law

add lemma indep_sets_collect_sigma

Add formalization of probabilistic independence for families of sets