Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-22 08:41 b4641efe

View on Github →

feat(l1_space): add measurability to integrable (#4170) This PR defines integrable such that integrable implies measurable. The old version is called has_finite_integral. This allows us to drop many measurability conditions from lemmas that also require integrability. There are some lemmas that have extra measurability conditions, if it has integrable as conclusion without corresponding measurable hypothesis. There are many results that require an additional [measurable_space E] hypothesis, and some that require [borel_space E] or [second_countable_space E] (usually when using that addition is measurable).

Estimated changes

Modified src/measure_theory/bochner_integration.lean

modified theorem measure_theory.integral_add

added theorem measure_theory.integral_add_measure'

modified theorem measure_theory.integral_eq

modified theorem measure_theory.integral_eq_lintegral_max_sub_lintegral_min

modified theorem measure_theory.integral_finset_sum

modified theorem measure_theory.integral_mono

modified theorem measure_theory.integral_mono_of_nonneg

deleted theorem measure_theory.integral_non_integrable

modified theorem measure_theory.integral_sub

modified theorem measure_theory.integral_undef

modified theorem measure_theory.l1.integral_of_fun_eq_integral

modified theorem measure_theory.l1.norm_of_fun_eq_integral_norm

modified theorem measure_theory.l1.simple_func.of_simple_func_add

modified theorem measure_theory.l1.simple_func.of_simple_func_sub

modified theorem measure_theory.l1.simple_func.of_simple_func_zero

modified theorem measure_theory.norm_integral_le_of_norm_le

modified theorem measure_theory.simple_func.integrable_pair

modified theorem measure_theory.simple_func.integral_sub

modified theorem measure_theory.tendsto_integral_of_l1

Modified src/measure_theory/borel_space.lean

Modified src/measure_theory/interval_integral.lean

modified theorem filter.tendsto.eventually_interval_integrable

modified theorem filter.tendsto.eventually_interval_integrable_ae

modified theorem interval_integrable.add

modified theorem interval_integrable.neg

modified theorem interval_integrable.refl

modified theorem interval_integrable.sub

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_add

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

modified theorem interval_integral.integral_sub

Modified src/measure_theory/l1_space.lean

added theorem measurable.integrable_zero

added theorem measure_theory.has_finite_integral.add_measure

added theorem measure_theory.has_finite_integral.congr'

added theorem measure_theory.has_finite_integral.congr

added theorem measure_theory.has_finite_integral.const_mul

added theorem measure_theory.has_finite_integral.left_of_add_measure

added theorem measure_theory.has_finite_integral.max_zero

added theorem measure_theory.has_finite_integral.min_zero

added theorem measure_theory.has_finite_integral.mono'

added theorem measure_theory.has_finite_integral.mono

added theorem measure_theory.has_finite_integral.mono_measure

added theorem measure_theory.has_finite_integral.mul_const

added theorem measure_theory.has_finite_integral.neg

added theorem measure_theory.has_finite_integral.norm

added theorem measure_theory.has_finite_integral.right_of_add_measure

added theorem measure_theory.has_finite_integral.smul

added theorem measure_theory.has_finite_integral.smul_measure

added def measure_theory.has_finite_integral

added theorem measure_theory.has_finite_integral_add_measure

added theorem measure_theory.has_finite_integral_congr'

added theorem measure_theory.has_finite_integral_congr

added theorem measure_theory.has_finite_integral_const

added theorem measure_theory.has_finite_integral_const_iff

added theorem measure_theory.has_finite_integral_iff_edist

added theorem measure_theory.has_finite_integral_iff_norm

added theorem measure_theory.has_finite_integral_iff_of_real

added theorem measure_theory.has_finite_integral_neg_iff

added theorem measure_theory.has_finite_integral_norm_iff

added theorem measure_theory.has_finite_integral_of_bounded

added theorem measure_theory.has_finite_integral_of_dominated_convergence

added theorem measure_theory.has_finite_integral_smul_iff

added theorem measure_theory.has_finite_integral_zero

added theorem measure_theory.has_finite_integral_zero_measure

modified theorem measure_theory.integrable.add

modified theorem measure_theory.integrable.congr'

modified theorem measure_theory.integrable.congr

added theorem measure_theory.integrable.has_finite_integral

modified theorem measure_theory.integrable.left_of_add_measure

added theorem measure_theory.integrable.measurable

modified theorem measure_theory.integrable.mono'

modified theorem measure_theory.integrable.mono

modified theorem measure_theory.integrable.mono_measure

modified theorem measure_theory.integrable.neg

modified theorem measure_theory.integrable.norm

modified theorem measure_theory.integrable.right_of_add_measure

modified theorem measure_theory.integrable.smul

modified theorem measure_theory.integrable.sub

modified def measure_theory.integrable

modified theorem measure_theory.integrable_congr'

modified theorem measure_theory.integrable_congr

modified theorem measure_theory.integrable_finset_sum

deleted theorem measure_theory.integrable_iff_edist

deleted theorem measure_theory.integrable_iff_norm

deleted theorem measure_theory.integrable_iff_of_real

modified theorem measure_theory.integrable_map_measure

modified theorem measure_theory.integrable_neg_iff

modified theorem measure_theory.integrable_norm_iff

deleted theorem measure_theory.integrable_of_bounded

deleted theorem measure_theory.integrable_of_dominated_convergence

modified theorem measure_theory.integrable_smul_iff

modified theorem measure_theory.integrable_zero

deleted theorem measure_theory.integrable_zero_measure

modified theorem measure_theory.l1.dist_to_fun

modified theorem measure_theory.l1.norm_of_fun

modified theorem measure_theory.l1.norm_of_fun_eq_lintegral_norm

modified def measure_theory.l1.of_fun

modified theorem measure_theory.l1.of_fun_add

modified theorem measure_theory.l1.of_fun_eq_mk

modified theorem measure_theory.l1.of_fun_eq_of_fun

modified theorem measure_theory.l1.of_fun_neg

modified theorem measure_theory.l1.of_fun_smul

modified theorem measure_theory.l1.of_fun_sub

modified theorem measure_theory.l1.of_fun_to_fun

modified theorem measure_theory.l1.of_fun_zero

modified theorem measure_theory.l1.to_fun_of_fun

modified def measure_theory.l1

modified theorem measure_theory.lintegral_edist_lt_top

Modified src/measure_theory/set_integral.lean

modified def continuous_linear_map.comp_l1

modified theorem continuous_linear_map.comp_l1_apply

modified theorem continuous_linear_map.integrable_comp

modified theorem continuous_linear_map.integral_comp_comm

modified theorem continuous_linear_map.integral_comp_l1_comm

modified theorem continuous_linear_map.measurable_comp_l1

modified theorem continuous_linear_map.norm_comp_l1_apply_le

modified theorem continuous_on.integrable_on_compact

modified theorem is_compact.integrable_on_of_nhds_within

added theorem measure_theory.has_finite_integral_restrict_of_bounded

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

deleted theorem measure_theory.integrable_on_of_bounded

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

modified theorem measure_theory.simple_func_sequence_tendsto'