Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-22 06:47 0d77f29f

View on Github →

feat(analysis/calculus/specific_functions): define normed bump functions (#13463)

Normed bump functions have integral 1 w.r.t. the specified measure.
Also add a few more properties of bump functions, including its smoothness in all arguments (including midpoint and the two radii).
From the sphere eversion project
Required for convolutions

Estimated changes

Modified src/analysis/calculus/specific_functions.lean

added theorem cont_diff.cont_diff_bump

added theorem cont_diff_bump_of_inner.cont_diff_normed

added theorem cont_diff_bump_of_inner.continuous_normed

added theorem cont_diff_bump_of_inner.has_compact_support_normed

added theorem cont_diff_bump_of_inner.integral_normed

added theorem cont_diff_bump_of_inner.integral_normed_smul

added theorem cont_diff_bump_of_inner.integral_pos

added theorem cont_diff_bump_of_inner.nonneg'

added theorem cont_diff_bump_of_inner.nonneg_normed

added theorem cont_diff_bump_of_inner.normed_def

added theorem cont_diff_bump_of_inner.normed_neg

added theorem cont_diff_bump_of_inner.normed_sub

added theorem cont_diff_bump_of_inner.support_normed_eq

added theorem cont_diff_bump_of_inner.tsupport_eq

added theorem cont_diff_bump_of_inner.tsupport_normed_eq

Modified src/analysis/normed/group/basic.lean

added theorem dist_self_sub_left

added theorem dist_self_sub_right

Modified src/measure_theory/function/l1_space.lean

added theorem measure_theory.integrable.div_const

Modified src/order/cover.lean

added theorem covby.Iio_eq

added theorem covby.Ioi_eq

Modified src/topology/algebra/order/basic.lean

added theorem continuous_at.eventually_lt

added theorem tendsto.eventually_lt