Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-06 06:58 3eea1091

View on Github →

feat(measure_theory/interval_integral): introduce ∫ x in a..b, f x, prove FTC-1 (#3640) Define ∫ x in a..b, f x ∂μ as ∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ. With this definition for a probability measure μ we have F_μ(b)-F_μ(a)=∫ x in a..b, f x ∂μ, where F_μ is the cumulative distribution function.

Estimated changes

Modified src/measure_theory/bochner_integration.lean

modified theorem measure_theory.integral_add_meas

added theorem measure_theory.integral_map_meas

added theorem measure_theory.integral_mono_of_nonneg

added theorem measure_theory.norm_integral_le_of_norm_le

added theorem measure_theory.norm_integral_le_of_norm_le_const

Created src/measure_theory/interval_integral.lean

added theorem interval_integrable.add

added theorem interval_integrable.neg

added theorem interval_integrable.refl

added theorem interval_integrable.smul

added theorem interval_integrable.sub

added theorem interval_integrable.symm

added theorem interval_integrable.trans

added def interval_integrable

added theorem interval_integral.integral_add

added theorem interval_integral.integral_add_adjacent_intervals

added theorem interval_integral.integral_add_adjacent_intervals_cancel

added theorem interval_integral.integral_cases

added theorem interval_integral.integral_has_deriv_at_of_tendsto_ae

added theorem interval_integral.integral_neg

added theorem interval_integral.integral_of_ge

added theorem interval_integral.integral_of_le

added theorem interval_integral.integral_same

added theorem interval_integral.integral_same_has_deriv_at_of_tendsto_ae

added theorem interval_integral.integral_sub_linear_is_o_of_tendsto_ae

added theorem interval_integral.integral_symm

added theorem interval_integral.norm_integral_eq_norm_integral_Ioc

added theorem interval_integral.norm_integral_le_abs_integral_norm

added theorem interval_integral.norm_integral_le_integral_norm_Ioc

added theorem interval_integral.norm_integral_le_of_norm_le_const

added theorem interval_integral.norm_integral_le_of_norm_le_const_ae

added def interval_integral

Modified src/measure_theory/l1_space.lean

added theorem measure_theory.integrable.congr'

added theorem measure_theory.integrable.mono'

deleted theorem measure_theory.integrable.mono_set

deleted theorem measure_theory.integrable.union

added theorem measure_theory.integrable_add_meas

added theorem measure_theory.integrable_congr'

modified theorem measure_theory.integrable_const

added theorem measure_theory.integrable_const_iff

added theorem measure_theory.integrable_map_meas

added theorem measure_theory.integrable_of_bounded

deleted theorem measure_theory.integrable_of_integrable_bound

added theorem measure_theory.integrable_zero_meas

Modified src/measure_theory/set_integral.lean

added theorem continuous.integrable_on_compact

added theorem continuous_at.integral_sub_linear_is_o_ae

added theorem continuous_on.integrable_on_compact

added theorem filter.tendsto.integral_sub_linear_is_o_ae

added theorem indicator_ae_eq_restrict

added theorem indicator_ae_eq_restrict_compl

added theorem is_compact.integrable_on_of_nhds_within

added theorem measure_theory.integrable.integrable_on'

added theorem measure_theory.integrable.integrable_on

added theorem measure_theory.integrable_at_filter.filter_mono

added theorem measure_theory.integrable_at_filter.inf_ae_iff

added theorem measure_theory.integrable_at_filter.inf_of_left

added theorem measure_theory.integrable_at_filter.inf_of_right

added def measure_theory.integrable_at_filter

added theorem measure_theory.integrable_indicator_iff

added theorem measure_theory.integrable_on.add_meas

added theorem measure_theory.integrable_on.indicator

added theorem measure_theory.integrable_on.integrable

added theorem measure_theory.integrable_on.left_of_union

added theorem measure_theory.integrable_on.mono

added theorem measure_theory.integrable_on.mono_meas

added theorem measure_theory.integrable_on.mono_set

added theorem measure_theory.integrable_on.mono_set_ae

added theorem measure_theory.integrable_on.right_of_union

added theorem measure_theory.integrable_on.union

added def measure_theory.integrable_on

added theorem measure_theory.integrable_on_add_meas

added theorem measure_theory.integrable_on_const

added theorem measure_theory.integrable_on_empty

added theorem measure_theory.integrable_on_finite_union

added theorem measure_theory.integrable_on_finset_union

added theorem measure_theory.integrable_on_of_bounded

added theorem measure_theory.integrable_on_union

added theorem measure_theory.integrable_on_univ

added theorem measure_theory.integrable_on_zero

added theorem measure_theory.integral_add_compl

added theorem measure_theory.integral_empty

added theorem measure_theory.integral_indicator

added theorem measure_theory.integral_union

added theorem measure_theory.integral_univ

added theorem measure_theory.measure.finite_at_filter.integrable_at_filter

added theorem measure_theory.measure.finite_at_filter.integrable_at_filter_of_tendsto

added theorem measure_theory.measure.finite_at_filter.integrable_at_filter_of_tendsto_ae

added theorem measure_theory.norm_set_integral_le_of_norm_le_const'

added theorem measure_theory.norm_set_integral_le_of_norm_le_const

added theorem measure_theory.norm_set_integral_le_of_norm_le_const_ae''

added theorem measure_theory.norm_set_integral_le_of_norm_le_const_ae'

added theorem measure_theory.norm_set_integral_le_of_norm_le_const_ae

added theorem measure_theory.set_integral_const

added theorem piecewise_ae_eq_restrict

added theorem piecewise_ae_eq_restrict_compl