Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-05 14:50 1de608d8

View on Github →

refactor(measure_theory): integrate almost everywhere measurable functions (#5510) Currently, the Bochner integral is only defined for measurable functions. This means that, if f is continuous on an interval [a, b], to be able to make sense of ∫ x in a..b, f, one has to add a global measurability assumption, which is very much unnatural. This PR redefines the Bochner integral so that it makes sense for functions that are almost everywhere measurable, i.e., they coincide almost everywhere with a measurable function (This is equivalent to measurability for the completed measure, but we don't state or prove this as it is not needed to develop the theory).

Estimated changes

Modified src/analysis/convex/integral.lean

modified theorem convex.smul_integral_mem

Modified src/analysis/mean_inequalities.lean

Modified src/measure_theory/ae_eq_fun.lean

modified def measure_theory.ae_eq_fun.const

modified def measure_theory.ae_eq_fun.mk

modified theorem measure_theory.ae_eq_fun.mk_coe_fn

modified theorem measure_theory.ae_eq_fun.one_def

deleted theorem measure_theory.ae_eq_fun.quotient_out'_eq_coe_fn

modified def measure_theory.measure.ae_eq_setoid

Modified src/measure_theory/bochner_integration.lean

deleted theorem measure_theory.integral_add_measure'

modified theorem measure_theory.integral_congr_ae

modified theorem measure_theory.integral_eq_lintegral_of_nonneg_ae

added theorem measure_theory.integral_map_of_measurable

added theorem measure_theory.integral_non_ae_measurable

deleted theorem measure_theory.integral_non_measurable

modified theorem measure_theory.integral_to_real

deleted theorem measure_theory.tendsto_integral_approx_on_univ

added theorem measure_theory.tendsto_integral_approx_on_univ_of_measurable

Modified src/measure_theory/haar_measure.lean

Modified src/measure_theory/integration.lean

added theorem measure_theory.lintegral_add'

added theorem measure_theory.lintegral_const_mul''

added theorem measure_theory.lintegral_eq_zero_iff'

added theorem measure_theory.lintegral_map'

added theorem measure_theory.lintegral_mul_const''

added theorem measure_theory.tendsto_lintegral_of_dominated_convergence'

Modified src/measure_theory/interval_integral.lean

modified theorem continuous_on.interval_integrable

modified theorem continuous_on.interval_integrable_of_Icc

modified theorem filter.tendsto.eventually_interval_integrable

modified theorem filter.tendsto.eventually_interval_integrable_ae

modified theorem interval_integrable.refl

modified theorem interval_integrable.trans

modified theorem interval_integral.deriv_integral_left

modified theorem interval_integral.deriv_integral_of_tendsto_ae_left

modified theorem interval_integral.deriv_integral_of_tendsto_ae_right

modified theorem interval_integral.deriv_integral_right

modified theorem interval_integral.deriv_within_integral_left

modified theorem interval_integral.deriv_within_integral_of_tendsto_ae_left

modified theorem interval_integral.deriv_within_integral_of_tendsto_ae_right

modified theorem interval_integral.deriv_within_integral_right

modified theorem interval_integral.fderiv_integral

modified theorem interval_integral.fderiv_integral_of_tendsto_ae

modified theorem interval_integral.fderiv_within_integral_of_tendsto_ae

modified theorem interval_integral.integral_comp_add_right

modified theorem interval_integral.integral_comp_mul_right

modified theorem interval_integral.integral_comp_neg

modified theorem interval_integral.integral_has_deriv_at_left

modified theorem interval_integral.integral_has_deriv_at_of_tendsto_ae_left

modified theorem interval_integral.integral_has_deriv_at_of_tendsto_ae_right

modified theorem interval_integral.integral_has_deriv_at_right

modified theorem interval_integral.integral_has_deriv_within_at_left

modified theorem interval_integral.integral_has_deriv_within_at_of_tendsto_ae_left

modified theorem interval_integral.integral_has_deriv_within_at_of_tendsto_ae_right

modified theorem interval_integral.integral_has_deriv_within_at_right

modified theorem interval_integral.integral_has_fderiv_at

modified theorem interval_integral.integral_has_fderiv_at_of_tendsto_ae

modified theorem interval_integral.integral_has_fderiv_within_at

modified theorem interval_integral.integral_has_fderiv_within_at_of_tendsto_ae

modified theorem interval_integral.integral_has_strict_deriv_at_left

modified theorem interval_integral.integral_has_strict_deriv_at_of_tendsto_ae_left

modified theorem interval_integral.integral_has_strict_deriv_at_of_tendsto_ae_right

modified theorem interval_integral.integral_has_strict_deriv_at_right

modified theorem interval_integral.integral_has_strict_fderiv_at

modified theorem interval_integral.integral_has_strict_fderiv_at_of_tendsto_ae

added theorem interval_integral.integral_non_ae_measurable

deleted theorem interval_integral.integral_non_measurable

modified theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae

Modified src/measure_theory/l1_space.lean

added theorem integrable_zero_measure

deleted theorem measurable.integrable_zero

modified theorem measure_theory.ae_eq_fun.integrable_mk

added theorem measure_theory.integrable.ae_measurable

modified theorem measure_theory.integrable.congr'

modified theorem measure_theory.integrable.congr

deleted theorem measure_theory.integrable.measurable

modified theorem measure_theory.integrable.mono'

modified theorem measure_theory.integrable.mono

modified theorem measure_theory.integrable_congr'

modified theorem measure_theory.integrable_congr

modified theorem measure_theory.integrable_norm_iff

modified theorem measure_theory.l1.mk_to_fun

Modified src/measure_theory/lp_space.lean

modified theorem ℒp_space.mem_ℒp_of_snorm_lt_top

modified theorem ℒp_space.snorm_add_le

Modified src/measure_theory/outer_measure.lean

Modified src/measure_theory/prod.lean

added theorem ae_measurable.integral_prod_right'

added theorem ae_measurable.prod_mk_left

added theorem ae_measurable.prod_swap

added theorem measure_theory.has_finite_integral_prod_iff'

modified theorem measure_theory.integrable_prod_iff'

modified theorem measure_theory.integrable_prod_iff

modified theorem measure_theory.integral_fn_integral_add

modified theorem measure_theory.integral_fn_integral_sub

added theorem measure_theory.lintegral_prod'

added theorem measure_theory.lintegral_prod_symm'

Modified src/measure_theory/set_integral.lean

added theorem continuous_on.ae_measurable

modified theorem continuous_on.integrable_on_compact

added theorem measure_theory.ae_measurable_indicator_iff

modified theorem measure_theory.integrable_indicator_iff

modified theorem measure_theory.integrable_on_empty

modified theorem measure_theory.integrable_on_finite_union

modified theorem measure_theory.integrable_on_finset_union

modified theorem measure_theory.integral_indicator

modified theorem measure_theory.measure.finite_at_filter.integrable_at_filter

modified theorem measure_theory.measure.finite_at_filter.integrable_at_filter_of_tendsto

modified theorem measure_theory.measure.finite_at_filter.integrable_at_filter_of_tendsto_ae

Modified src/measure_theory/simple_func_dense.lean