Changes

Summary

HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.

Changeset 73253:f6bb31879698 by manuel eberl _eberlm@in.tum.de_: HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
The file was added	`src/HOL/Probability/Hoeffding.thy`
The file was added	`src/HOL/Probability/Product_PMF.thy`
The file was modified	`CONTRIBUTORS` (diff)
The file was modified	`NEWS` (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/Nonnegative_Lebesgue_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Set_Integral.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Nonnegative_Real.thy` (diff)
The file was modified	`src/HOL/Probability/Central_Limit_Theorem.thy` (diff)
The file was modified	`src/HOL/Probability/Conditional_Expectation.thy` (diff)
The file was modified	`src/HOL/Probability/Giry_Monad.thy` (diff)
The file was modified	`src/HOL/Probability/Independent_Family.thy` (diff)
The file was modified	`src/HOL/Probability/Infinite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Probability/Probability.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)