Commit 2023-06-07 04:25 1a01c22d

View on Github →

feat: port MeasureTheory.Integral.PeakFunction (#4772)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/PeakFunction.lean

added theorem Set.disjoint_sdiff_inter

added theorem integrableOn_peak_smul_of_integrableOn_of_continuousWithinAt

added theorem tendsto_set_integral_peak_smul_of_integrableOn_of_continuousWithinAt

added theorem tendsto_set_integral_peak_smul_of_integrableOn_of_continuousWithinAt_aux

added theorem tendsto_set_integral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn

added theorem tendsto_set_integral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn

added theorem tendsto_set_integral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos