Commit 2023-06-23 18:07 03bb20be

View on Github →

feat: port Analysis.Calculus.BumpFunctionFindim (#5389)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/BumpFunctionFindim.lean

added def ExistsContDiffBumpBase.u

added theorem ExistsContDiffBumpBase.u_compact_support

added theorem ExistsContDiffBumpBase.u_continuous

added theorem ExistsContDiffBumpBase.u_exists

added theorem ExistsContDiffBumpBase.u_int_pos

added theorem ExistsContDiffBumpBase.u_le_one

added theorem ExistsContDiffBumpBase.u_neg

added theorem ExistsContDiffBumpBase.u_nonneg

added theorem ExistsContDiffBumpBase.u_smooth

added theorem ExistsContDiffBumpBase.u_support

added def ExistsContDiffBumpBase.w

added theorem ExistsContDiffBumpBase.w_compact_support

added theorem ExistsContDiffBumpBase.w_def

added theorem ExistsContDiffBumpBase.w_integral

added theorem ExistsContDiffBumpBase.w_mul_φ_nonneg

added theorem ExistsContDiffBumpBase.w_nonneg

added theorem ExistsContDiffBumpBase.w_support

added def ExistsContDiffBumpBase.y

added theorem ExistsContDiffBumpBase.y_eq_one_of_mem_closedBall

added theorem ExistsContDiffBumpBase.y_eq_zero_of_not_mem_ball

added theorem ExistsContDiffBumpBase.y_le_one

added theorem ExistsContDiffBumpBase.y_neg

added theorem ExistsContDiffBumpBase.y_nonneg

added theorem ExistsContDiffBumpBase.y_pos_of_mem_ball

added theorem ExistsContDiffBumpBase.y_smooth

added theorem ExistsContDiffBumpBase.y_support

added def ExistsContDiffBumpBase.φ

added theorem IsOpen.exists_smooth_support_eq

added theorem exists_smooth_tsupport_subset