isabelle update -u control_cartouches;

ran isabelle update_op on all sources

session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;

setprod -> prod

setsum -> sum

HOL-Probability: more about probability, prepare for Markov processes in the AFP

--HG--
extra : rebase_source : f90e6cf5c47f7a2604d0eeacaf0181f3cfe64a14

move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel

--HG--
extra : rebase_source : 0321297c249a436ca0371010a76a1a026dd33222

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

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

Moved material from AFP/Randomised_Social_Choice to distribution

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

add the proof of the central limit theorem

--HG--
extra : rebase_source : 493d99e28392771c51f4102a11b90533880e289f
extra : amend_source : 3fb7b7c607104e57a2c3ba7f733dd570eb42fa3b

sorted out eventually_mono

isabelle update_cartouches -c -t;

qualifier is mandatory by default;

Qualifiers in locale expressions default to mandatory regardless of the command.

prod_case as canonical name for product type eliminator

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

--HG--
extra : rebase_source : cffce7b3e322f3c274d9117a0dfdd311d4ba66a1

tuned proofs -- less legacy;

prefer "uncurry" as canonical name for case distinction on products in combinatorial view

generalise lemma

import general thms from Density_Compiler

--HG--
extra : rebase_source : 48a3b47f755d8099564008b93076eae81453a674

allow line breaks in probability syntax

measurability prover: removed app splitting, replaced by more powerful destruction rules

import general theorems from AFP/Markov_Models

modernized header;

add print translation for probability notation \<P>

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

--HG--
extra : rebase_source : 03b2468f7b324b9d8add229ae59776b447283141

fact consolidation

moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin

--HG--
extra : rebase_source : cd4a9d91f2d415deaa6fd3411b5402ef770d74d2

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

--HG--
extra : rebase_source : b821e7a52658fa32f598433901729ddc5fc949dd

add various lemmas

renamed positive_integral to nn_integral

--HG--
extra : rebase_source : e7a432bee0942b6330cadfd1eb5da8e326238e06

fixed document generation for HOL-Probability

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

normalising simp rules for compound operators

measure of a countable union

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

generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector

introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it

add exponential and uniform distributions

qualified interpretation of sigma_algebra, to avoid name clashes

--HG--
extra : rebase_source : aaeab4e40463c23ef5a5a07ee360db0335376105

move theorems to be more generally useable

--HG--
extra : rebase_source : c1c0d1f5576f4d469d1b4618663774e2f297a214

rules for AE and prob

use measurability prover

add measurability prover; add support for Borel sets

add syntax and a.e.-rules for (conditional) probability on predicates

joint distribution of independent variables

show and use distributed_swap and distributed_jointI

continuous version of entropy_le

generalize from prob_space to finite_measure

tuned product measurability

reworked Probability theory

--HG--
extra : rebase_source : 04bef352ab6c7feafcf64ecca49fecffac43bb41

prefer abs_def over def_raw;

tuned proofs -- eliminated pointless chaining of facts after 'interpret';

avoid undeclared variables in let bindings;
tuned proofs;

add simp rules for enat and ereal

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

moved theorems about distribution to the definition; removed oopsed-lemma

rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution

new fastforce replacing fastsimp - less confusing name

Rename extreal => ereal

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

the borel probability measure is easier to handle with {0 ..< 1} (coverable by disjoint intervals {_ ..< _})

move conditional expectation to its own theory file

lemma: independence is equal to mutual information = 0

jensens inequality

integral strong monotone; finite subadditivity for measure

add lemma indep_distribution_eq_measure

add lemma indep_sets_collect_sigma

move lemmas to Extended_Reals and Extended_Real_Limits

Add restricted borel measure to {0 .. 1}

add lemma prob_finite_product

add Bernoulli space

add product of probability spaces with finite cardinality

remove double sum_over_space_real_distribution

remove unnecessary prob_preserving

add prob_space_vimage

rename Probability_Space to Probability_Measure

--HG--
rename : src/HOL/Probability/Probability_Space.thy => src/HOL/Probability/Probability_Measure.thy