Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-10 22:50 a25e4a81

View on Github →

feat(analysis/measure_theory/integration): lebesgue integration [WIP]

Estimated changes

Modified analysis/measure_theory/borel_space.lean

added theorem measure_theory.borel_eq_generate_Iio

added theorem measure_theory.borel_eq_generate_Ioi

added theorem measure_theory.measurable.infi

added theorem measure_theory.measurable.is_glb

added theorem measure_theory.measurable.is_lub

added theorem measure_theory.measurable.supr

Created analysis/measure_theory/integration.lean

added def measure_theory.indicator.size

added def measure_theory.indicator.to_fun

added theorem measure_theory.indicator.to_fun_val

added structure measure_theory.indicator

added def measure_theory.simple_func'.bind

added theorem measure_theory.simple_func'.bind_apply

added theorem measure_theory.simple_func'.bind_const

added theorem measure_theory.simple_func'.bind_itg

added theorem measure_theory.simple_func'.bind_sum_measure

added theorem measure_theory.simple_func'.coe_def

added theorem measure_theory.simple_func'.coe_le_coe

added def measure_theory.simple_func'.const

added theorem measure_theory.simple_func'.const_apply

added theorem measure_theory.simple_func'.ext

added theorem measure_theory.simple_func'.is_measurable_cut

added def measure_theory.simple_func'.ite

added theorem measure_theory.simple_func'.ite_apply

added def measure_theory.simple_func'.itg

added theorem measure_theory.simple_func'.le_def

added def measure_theory.simple_func'.map

added theorem measure_theory.simple_func'.map_apply

added theorem measure_theory.simple_func'.map_itg

added theorem measure_theory.simple_func'.measurable

added theorem measure_theory.simple_func'.mem_range

added def measure_theory.simple_func'.pair

added theorem measure_theory.simple_func'.preimage_measurable

added def measure_theory.simple_func'.restrict

added theorem measure_theory.simple_func'.restrict_apply

added theorem measure_theory.simple_func'.restrict_preimage

added def measure_theory.simple_func'.seq

added theorem measure_theory.simple_func'.seq_itg

added theorem measure_theory.simple_func.add_congr

added theorem measure_theory.simple_func.add_sub_cancel_of_le

added theorem measure_theory.simple_func.coe_add

added theorem measure_theory.simple_func.coe_def

added theorem measure_theory.simple_func.coe_le_coe

added theorem measure_theory.simple_func.equiv_def

added theorem measure_theory.simple_func.equiv_iff

added theorem measure_theory.simple_func.finite_range

added def measure_theory.simple_func.itg'

added theorem measure_theory.simple_func.itg'_add

added theorem measure_theory.simple_func.itg'_eq_sum

added theorem measure_theory.simple_func.itg'_eq_sum_of_subset

added theorem measure_theory.simple_func.itg'_indicator

added theorem measure_theory.simple_func.itg'_mono

added theorem measure_theory.simple_func.itg'_zero

added def measure_theory.simple_func.itg

added theorem measure_theory.simple_func.itg_add

added theorem measure_theory.simple_func.itg_mono

added theorem measure_theory.simple_func.itg_zero

added theorem measure_theory.simple_func.le_antisymm

added theorem measure_theory.simple_func.le_antisymm_iff

added theorem measure_theory.simple_func.le_def

added theorem measure_theory.simple_func.le_iff_exists_add

added theorem measure_theory.simple_func.le_of_multiset_le

added def measure_theory.simple_func.lift₂

added theorem measure_theory.simple_func.lift₂_finite

added theorem measure_theory.simple_func.lift₂_is_measurable

added theorem measure_theory.simple_func.lift₂_val

added theorem measure_theory.simple_func.measurable

added def measure_theory.simple_func.of_fun

added theorem measure_theory.simple_func.of_fun_apply

added theorem measure_theory.simple_func.of_fun_val

added theorem measure_theory.simple_func.preimage_measurable

added theorem measure_theory.simple_func.sub_add_cancel_of_le

added theorem measure_theory.simple_func.sub_val

added def measure_theory.simple_func.to_fun

added def measure_theory.simple_func

added theorem measure_theory.simple_itg_eq

added def measure_theory.upper_itg

added theorem measure_theory.upper_itg_add_le

added def measure_theory.upper_itg_def_subtype

added theorem measure_theory.upper_itg_simple

added structure measure_theory.{u

Modified analysis/measure_theory/lebesgue_measure.lean

deleted def measure_theory.lebesgue

deleted theorem measure_theory.lebesgue_Icc

deleted theorem measure_theory.lebesgue_Ico

deleted theorem measure_theory.lebesgue_Ioo

deleted theorem measure_theory.lebesgue_singleton

modified theorem measure_theory.lebesgue_to_outer_measure

deleted theorem measure_theory.lebesgue_val

added theorem measure_theory.real.volume_Icc

added theorem measure_theory.real.volume_Ico

added theorem measure_theory.real.volume_Ioo

added theorem measure_theory.real.volume_singleton

added theorem measure_theory.real.volume_val

Modified analysis/measure_theory/measurable_space.lean

added theorem is_measurable.Inter_Prop

added theorem is_measurable.Union_Prop

added theorem is_measurable.const

added theorem is_measurable.univ

deleted theorem is_measurable_univ

Modified analysis/measure_theory/measure_space.lean

added def measure_theory.measure.a_e

modified theorem measure_theory.measure_sUnion

added def measure_theory.volume

added theorem measure_theory.volume_Union

added theorem measure_theory.volume_Union_le

added theorem measure_theory.volume_Union_null

added theorem measure_theory.volume_bUnion

added theorem measure_theory.volume_diff

added theorem measure_theory.volume_empty

added theorem measure_theory.volume_mono

added theorem measure_theory.volume_mono_null

added theorem measure_theory.volume_sUnion

added theorem measure_theory.volume_union

added theorem measure_theory.volume_union_le

added theorem measure_theory.volume_union_null

Modified analysis/topology/topological_space.lean

added theorem topological_space.is_open_Union_countable

Modified data/set/basic.lean

added theorem set.image_subset_range

added theorem set.preimage_image_preimage

added theorem set.preimage_inter_range

Modified data/set/finite.lean

modified theorem set.finite_bUnion

Modified data/set/lattice.lean

added theorem set.bUnion_of_singleton

added theorem set.bUnion_subset_Union

added theorem set.preimage_bUnion

Modified order/bounds.lean

modified theorem is_glb_Inf

added theorem is_glb_lt_iff

modified theorem is_lub_Sup

added theorem is_lub_le_iff

added theorem le_is_glb_iff

added theorem lower_bounds_mono

added theorem lt_is_lub_iff

added theorem upper_bounds_mono

Modified order/order_iso.lean

added theorem preimage_equivalence

Modified tactic/interactive.lean