Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-18 15:36 eb1253fe

View on Github →

feat(measure_theory): add Giry monad

Estimated changes

Created src/measure_theory/giry_monad.lean

added def measure_theory.measure.bind

added theorem measure_theory.measure.bind_apply

added theorem measure_theory.measure.bind_bind

added theorem measure_theory.measure.bind_dirac

added theorem measure_theory.measure.dirac_bind

added theorem measure_theory.measure.integral_bind

added theorem measure_theory.measure.integral_join

added def measure_theory.measure.join

added theorem measure_theory.measure.join_apply

added theorem measure_theory.measure.measurable_bind'

added theorem measure_theory.measure.measurable_coe

added theorem measure_theory.measure.measurable_dirac

added theorem measure_theory.measure.measurable_integral

added theorem measure_theory.measure.measurable_join

added theorem measure_theory.measure.measurable_map

added theorem measure_theory.measure.measurable_of_measurable_coe

Modified src/measure_theory/integration.lean

added theorem le_sequence_of_directed

added theorem measure_theory.lintegral_finset_sum

added theorem measure_theory.lintegral_supr_directed

added theorem measure_theory.lintegral_tsum

added def measure_theory.measure.integral

added theorem measure_theory.measure.integral_dirac

added theorem measure_theory.measure.integral_map

added theorem measure_theory.measure.integral_zero

added def measure_theory.measure.with_density

added theorem measure_theory.measure.with_density_apply

added theorem measure_theory.simple_func.approx_comp

added theorem measure_theory.simple_func.eapprox_comp

added theorem measure_theory.simple_func.integral_map

added theorem monotone_sequence_of_directed

deleted theorem supr_eq_of_tendsto

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.measure.of_measurable_apply

Modified src/order/basic.lean

added theorem monotone_of_monotone_nat

Modified src/topology/algebra/topological_structures.lean

added theorem supr_eq_of_tendsto