Commit 2022-03-22 08:03 3ce4161c

View on Github →

refactor(measure_theory/integral): restrict interval integrals to real intervals (#12754) This way ∫ x in 0 .. 1, (1 : real) means what it should, not ∫ x : nat in 0 .. 1, (1 : real).

Estimated changes

Modified src/analysis/calculus/parametric_interval_integral.lean

modified theorem interval_integral.has_deriv_at_integral_of_dominated_loc_of_deriv_le

modified theorem interval_integral.has_deriv_at_integral_of_dominated_loc_of_lip

modified theorem interval_integral.has_fderiv_at_integral_of_dominated_loc_of_lip

modified theorem interval_integral.has_fderiv_at_integral_of_dominated_of_fderiv_le

Modified src/measure_theory/integral/integral_eq_improper.lean

modified theorem measure_theory.integrable_of_interval_integral_norm_bounded

modified theorem measure_theory.integrable_of_interval_integral_norm_tendsto

modified theorem measure_theory.integrable_on_Iic_of_interval_integral_norm_bounded

modified theorem measure_theory.integrable_on_Iic_of_interval_integral_norm_tendsto

modified theorem measure_theory.integrable_on_Ioi_of_interval_integral_norm_bounded

modified theorem measure_theory.integrable_on_Ioi_of_interval_integral_norm_tendsto

modified theorem measure_theory.interval_integral_tendsto_integral

modified theorem measure_theory.interval_integral_tendsto_integral_Iic

modified theorem measure_theory.interval_integral_tendsto_integral_Ioi

Modified src/measure_theory/integral/interval_integral.lean

modified theorem antitone.interval_integrable

modified theorem antitone_on.interval_integrable

modified theorem filter.tendsto.eventually_interval_integrable

modified theorem filter.tendsto.eventually_interval_integrable_ae

modified theorem interval_integrable.abs

modified theorem interval_integrable.continuous_on_mul

modified theorem interval_integrable.def

modified theorem interval_integrable.mono

modified theorem interval_integrable.mono_fun'

modified theorem interval_integrable.mono_fun

modified theorem interval_integrable.mono_measure

modified theorem interval_integrable.mono_set

modified theorem interval_integrable.mono_set_ae

modified theorem interval_integrable.mul_continuous_on

modified theorem interval_integrable.trans_iterate

modified def interval_integrable

modified theorem interval_integrable_const

modified theorem interval_integrable_const_iff

modified theorem interval_integrable_iff

modified theorem interval_integrable_iff_integrable_Ioc_of_le

modified theorem interval_integral.FTC_filter.finite_at_inner

modified theorem interval_integral.abs_integral_eq_abs_integral_interval_oc

modified theorem interval_integral.continuous_of_dominated_interval

modified theorem interval_integral.continuous_on_primitive

modified theorem interval_integral.continuous_on_primitive_Icc

modified theorem interval_integral.continuous_on_primitive_interval'

modified theorem interval_integral.continuous_on_primitive_interval

modified theorem interval_integral.continuous_on_primitive_interval_left

modified theorem interval_integral.continuous_primitive

modified theorem interval_integral.continuous_within_at_primitive

modified theorem interval_integral.integral_cases

modified theorem interval_integral.integral_congr

modified theorem interval_integral.integral_congr_ae'

modified theorem interval_integral.integral_congr_ae

modified theorem interval_integral.integral_const

modified theorem interval_integral.integral_const_mul

modified theorem interval_integral.integral_div

modified theorem interval_integral.integral_eq_integral_of_support_subset

modified theorem interval_integral.integral_finset_sum

modified theorem interval_integral.integral_indicator

modified theorem interval_integral.integral_mono_on

modified theorem interval_integral.integral_mul_const

modified theorem interval_integral.integral_nonneg

modified theorem interval_integral.integral_smul_const

modified theorem interval_integral.integral_zero_ae

modified theorem interval_integral.interval_integral_eq_integral_interval_oc

modified theorem interval_integral.norm_integral_eq_norm_integral_Ioc

modified theorem interval_integral.norm_integral_min_max

modified theorem interval_integral.sub_le_integral_of_has_deriv_right_of_le

modified theorem interval_integral.sum_integral_adjacent_intervals

modified def interval_integral

modified theorem measure_theory.integrable.continuous_primitive

modified theorem measure_theory.integrable.interval_integrable

modified theorem measure_theory.integrable_on.interval_integrable

modified theorem monotone.interval_integrable

modified theorem monotone_on.interval_integrable