tuned proofs

uniform naming

isabelle update -u control_cartouches;

uniform naming of strong congruence rules

various new results on measures, integrals, etc., and some simplified proofs

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

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

more accurate cong del;
tuned proofs;

eliminated old 'def';
tuned comments;

Probability: move emeasure and nn_integral from ereal to ennreal

--HG--
extra : rebase_source : 5f2ac8a84abb43927a58086db8bbe10e190b2e77

more canonical names

isabelle update_cartouches -c -t;

Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.

tuned proofs -- less legacy;

tuned proofs;

Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.

modernized header;

fact consolidation

properties of normal distributed random variables (by Sudeep Kanav)

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

--HG--
extra : rebase_source : b821e7a52658fa32f598433901729ddc5fc949dd

use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules

--HG--
extra : rebase_source : 768e923634e619b4e9e3d904c01eda79077c3963

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

added divide_nonneg_nonneg and co; made it a simp rule

--HG--
extra : rebase_source : 998eadb7cfbf8720cf961ac2e149ce4537557a47

made mult_pos_pos a simp rule

made divide_pos_pos a simp rule

made mult_nonneg_nonneg a simp rule

--HG--
extra : rebase_source : 3f70ac991fa0f02839309ce9b8f418ff53f87c36

revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules

removing simprule status for divide_minus_left and divide_minus_right

more complete set of lemmas wrt. image and composition

tuned proofs -- clarified flow of facts wrt. calculation;

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

add exponential and uniform distributions

qualified interpretation of sigma_algebra, to avoid name clashes

--HG--
extra : rebase_source : aaeab4e40463c23ef5a5a07ee360db0335376105

use measurability prover

add measurability prover; add support for Borel sets

for the product measure it is enough if only one measure is sigma-finite

cleanup borel_measurable_positive_integral_(fst|snd)

add finite entropy

continuous version of mutual_information_eq_entropy_conditional_entropy

remove unnecessary assumption from conditional_entropy_eq

alternative definition of conditional entropy

remove unneeded assumption from conditional_entropy_generic_eq

show and use distributed_swap and distributed_jointI

rule to show that conditional mutual information is non-negative in the continuous case

continuous version of entropy_le

simplified entropy_uniform

tuned product measurability

reworked Probability theory

--HG--
extra : rebase_source : 04bef352ab6c7feafcf64ecca49fecffac43bb41

prefer abs_def over def_raw;

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

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

remove duplicate theorem setsum_real_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

move conditional expectation to its own theory file

lemma: independence is equal to mutual information = 0

rename Probability_Space to Probability_Measure

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

standardized headers

reworked Probability theory: measures are not type restricted to positive extended reals

add lemma KL_divergence_vimage, mutual_information_generic

the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
changed syntax for simple_function, simple_integral, positive_integral, integral and RN_deriv.
introduced binder variants for simple_integral, positive_integral and integral.

use pre-image measure, instead of image

explicit file specifications -- avoid secondary load path;

cleanup bijectivity btw. product spaces and pairs

it is known as the extended reals, not the infinite reals

--HG--
rename : src/HOL/Probability/Positive_Infinite_Real.thy => src/HOL/Probability/Positive_Extended_Real.thy

Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.

--HG--
rename : src/HOL/Probability/Borel.thy => src/HOL/Probability/Borel_Space.thy

renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI

expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets

Moved lemmas to appropriate locations

move lemmas to correct theory files

Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.

--HG--
rename : src/HOL/Probability/Lebesgue.thy => src/HOL/Probability/Lebesgue_Integration.thy

Corrected imports; better approximation of dependencies.

Cleanup information theory

Moved Convex theory to library.

Added Information theory and Example: dining cryptographers