Changes

Summary

Probability: variant of central limit theorem with non-zero mean
HOL-Probability: more about probability, prepare for Markov processes in the AFP

Changeset 64009:a5d293f1af80 by hoelzl: Probability: variant of central limit theorem with non-zero mean
The file was modified	`src/HOL/Probability/Central_Limit_Theorem.thy` (diff)
Changeset 64008:17a20ca86d62 by hoelzl: HOL-Probability: more about probability, prepare for Markov processes in the AFP
The file was modified	`src/HOL/Analysis/Binary_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Bochner_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Borel_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Derivative.thy` (diff)
The file was modified	`src/HOL/Analysis/Finite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Lebesgue_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Measurable.thy` (diff)
The file was modified	`src/HOL/Analysis/Measure_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Sigma_Algebra.thy` (diff)
The file was modified	`src/HOL/Library/Countable_Set.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Nonnegative_Real.thy` (diff)
The file was modified	`src/HOL/Probability/Giry_Monad.thy` (diff)
The file was modified	`src/HOL/Probability/Infinite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Probability/Information.thy` (diff)
The file was modified	`src/HOL/Probability/Probability_Mass_Function.thy` (diff)
The file was modified	`src/HOL/Probability/Probability_Measure.thy` (diff)
The file was modified	`src/HOL/Probability/Stream_Space.thy` (diff)
The file was modified	`src/HOL/Topological_Spaces.thy` (diff)