Commit 2021-02-19 14:14 845654a1

View on Github →

feat(analysis/calculus): define a smooth bump function (#4458) Define an infinitely smooth function which is 1 on the closed ball of radius 1 and is 0 outside of the open ball of radius 2.

Estimated changes

Modified src/analysis/calculus/specific_functions.lean

added theorem exists_times_cont_diff_bump_function_of_mem_nhds

deleted theorem exp_neg_inv_glue.smooth

added theorem smooth_bump_function.eventually_eq_one

added theorem smooth_bump_function.eventually_eq_one_of_norm_lt_one

added theorem smooth_bump_function.le_one

added theorem smooth_bump_function.lt_one_of_one_lt_norm

added theorem smooth_bump_function.nonneg

added theorem smooth_bump_function.one_of_norm_le_one

added theorem smooth_bump_function.pos_of_norm_lt_two

added theorem smooth_bump_function.support_eq

added theorem smooth_bump_function.zero_of_two_le_norm

added def smooth_bump_function

added theorem smooth_transition.le_one

added theorem smooth_transition.lt_one_of_lt_one

added theorem smooth_transition.nonneg

added theorem smooth_transition.one_of_one_le

added theorem smooth_transition.pos_denom

added theorem smooth_transition.pos_of_pos

added theorem smooth_transition.zero_of_nonpos

added def smooth_transition

Modified src/data/support.lean

added theorem function.support_comp_eq_preimage

Modified src/topology/algebra/module.lean

added theorem continuous_linear_equiv.image_closure