Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-14 17:40 5040c81d

View on Github →

feat(measure_theory/integration): dominated convergence theorem (#1123)

Create .DS_Store
Revert "Create .DS_Store" This reverts commit 5612886d493aef59205eddc5a34a75e6e5ba22c1.
feat(measure_theory/integration): dominated convergence theorem
Changes to styles
Update ordered.lean
Changes to styles
Update integration.lean
Changes to styles

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.sub_left_inj

Modified src/measure_theory/borel_space.lean

added theorem ennreal.measurable_add

added theorem ennreal.measurable_sub

added theorem measure_theory.measurable.infi_Prop

added theorem measure_theory.measurable.supr_Prop

added theorem nnreal.measurable_add

added theorem nnreal.measurable_mul

added theorem nnreal.measurable_sub

Modified src/measure_theory/integration.lean

added theorem measure_theory.dominated_convergence_nn

added theorem measure_theory.limsup_lintegral_le

added theorem measure_theory.lintegral_infi_ae

added theorem measure_theory.lintegral_liminf_le

added theorem measure_theory.lintegral_sub

added theorem measure_theory.lintegral_supr_ae

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.all_ae_of_all

Modified src/order/liminf_limsup.lean

added theorem filter.liminf_eq_supr_infi_of_nat

added theorem filter.liminf_le_limsup

added theorem filter.limsup_eq_infi_supr_of_nat

Modified src/topology/algebra/ordered.lean

added theorem liminf_eq_of_tendsto

added theorem limsup_eq_of_tendsto

added theorem tendsto_of_liminf_eq_limsup

Modified src/topology/instances/nnreal.lean

added theorem nnreal.continuous_sub'

added theorem nnreal.continuous_sub