Changes

Summary

HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
HOL-Probability: move conditional expectation from AFP/Ergodic_Theory

Changeset 64284:f3b905b2eee2 by hoelzl: HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
The file was modified	`src/HOL/Analysis/Borel_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Complete_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Set_Integral.thy` (diff)
The file was modified	`src/HOL/Analysis/Topology_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Nonnegative_Real.thy` (diff)
The file was modified	`src/HOL/Library/Permutations.thy` (diff)
The file was modified	`src/HOL/Probability/Levy.thy` (diff)
The file was modified	`src/HOL/Topological_Spaces.thy` (diff)
Changeset 64283:979cdfdf7a79 by hoelzl: HOL-Probability: move conditional expectation from AFP/Ergodic_Theory
The file was added	`src/HOL/Probability/Conditional_Expectation.thy`
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/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/Radon_Nikodym.thy` (diff)
The file was modified	`src/HOL/Analysis/Set_Integral.thy` (diff)
The file was modified	`src/HOL/Probability/Characteristic_Functions.thy` (diff)
The file was modified	`src/HOL/Probability/Levy.thy` (diff)
The file was modified	`src/HOL/Probability/Probability.thy` (diff)
The file was modified	`src/HOL/Topological_Spaces.thy` (diff)