Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. Multivariate_Analysis: add continuous_on_vec_lambda
  2. Probability: show that measures form a complete lattice
  3. move open_Collect_eq/less to HOL
  4. move Conditional_Complete_Lattices to Main
  5. Probability: introduce Hahn decomposition; use it to clean up Radon_Nikodym
  6. Probability: tuned headers; cleanup Radon_Nikodym
Changeset 63334:bd37a72a940a by hoelzl:
Multivariate_Analysis: add continuous_on_vec_lambda
The file was modified src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy (diff)
Changeset 63333:158ab2239496 by hoelzl:
Probability: show that measures form a complete lattice
The file was modified src/HOL/Probability/Binary_Product_Measure.thy (diff)
The file was modified src/HOL/Probability/Embed_Measure.thy (diff)
The file was modified src/HOL/Probability/Finite_Product_Measure.thy (diff)
The file was modified src/HOL/Probability/Giry_Monad.thy (diff)
The file was modified src/HOL/Probability/Measurable.thy (diff)
The file was modified src/HOL/Probability/Measure_Space.thy (diff)
The file was modified src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy (diff)
The file was modified src/HOL/Probability/Radon_Nikodym.thy (diff)
The file was modified src/HOL/Probability/SPMF.thy (diff)
The file was modified src/HOL/Probability/Sigma_Algebra.thy (diff)
The file was modified src/HOL/Probability/Stream_Space.thy (diff)
Changeset 63332:f164526d8727 by hoelzl:
move open_Collect_eq/less to HOL
The file was modified src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Probability/Borel_Space.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
Changeset 63331:247eac9758dd by hoelzl:
move Conditional_Complete_Lattices to Main
The file was modified src/HOL/Archimedean_Field.thy (diff)
The file was modified src/HOL/Conditionally_Complete_Lattices.thy (diff)
The file was modified src/HOL/Library/FSet.thy (diff)
The file was modified src/HOL/Main.thy (diff)
The file was modified src/HOL/Real.thy (diff)
Changeset 63330:8d591640c3bd by hoelzl:
Probability: introduce Hahn decomposition; use it to clean up Radon_Nikodym
The file was modified src/HOL/Probability/Radon_Nikodym.thy (diff)
Changeset 63329:6b26c378ab35 by hoelzl:
Probability: tuned headers; cleanup Radon_Nikodym
The file was modified src/HOL/Probability/Central_Limit_Theorem.thy (diff)
The file was modified src/HOL/Probability/Characteristic_Functions.thy (diff)
The file was modified src/HOL/Probability/Distribution_Functions.thy (diff)
The file was modified src/HOL/Probability/Helly_Selection.thy (diff)
The file was modified src/HOL/Probability/Interval_Integral.thy (diff)
The file was modified src/HOL/Probability/Levy.thy (diff)
The file was modified src/HOL/Probability/Radon_Nikodym.thy (diff)
The file was modified src/HOL/Probability/Set_Integral.thy (diff)
The file was modified src/HOL/Probability/Sinc_Integral.thy (diff)
The file was modified src/HOL/Probability/Weak_Convergence.thy (diff)