Skip to content
Jenkins
log in
Dashboard
Benedikt Seidl <benedikt.seidl@tum.de>
My Views
All
isabelle-repo
#538
Changes
Status
Changes
Console Output
View Build Information
Polling Log
Timings
Environment Variables
Mercurial Build Data
Embeddable Build Status
Previous Build
Next Build
Success
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)