Commit 2023-06-07 05:16 c76f0eb8

View on Github →

feat: port Analysis.Calculus.BumpFunctionInner (#4745)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/BumpFunctionInner.lean

added theorem ContDiff.contDiffBump

added theorem ContDiffBump.contDiff_normed

added theorem ContDiffBump.continuous_normed

added theorem ContDiffBump.eventuallyEq_one

added theorem ContDiffBump.eventuallyEq_one_of_mem_ball

added theorem ContDiffBump.hasCompactSupport_normed

added theorem ContDiffBump.integral_normed

added theorem ContDiffBump.integral_normed_smul

added theorem ContDiffBump.integral_pos

added theorem ContDiffBump.le_one

added theorem ContDiffBump.nonneg'

added theorem ContDiffBump.nonneg

added theorem ContDiffBump.nonneg_normed

added theorem ContDiffBump.normed_def

added theorem ContDiffBump.normed_neg

added theorem ContDiffBump.normed_sub

added theorem ContDiffBump.one_lt_rOut_div_rIn

added theorem ContDiffBump.one_of_mem_closedBall

added theorem ContDiffBump.pos_of_mem_ball

added theorem ContDiffBump.rOut_pos

added theorem ContDiffBump.support_eq

added theorem ContDiffBump.support_normed_eq

added theorem ContDiffBump.tendsto_support_normed_smallSets

added def ContDiffBump.toFun

added theorem ContDiffBump.tsupport_eq

added theorem ContDiffBump.tsupport_normed_eq

added theorem ContDiffBump.zero_of_le_dist

added structure ContDiffBump

added def ContDiffBumpBase.ofInnerProductSpace

added structure ContDiffBumpBase

added theorem Real.smoothTransition.le_one

added theorem Real.smoothTransition.lt_one_of_lt_one

added theorem Real.smoothTransition.nonneg

added theorem Real.smoothTransition.one_of_one_le

added theorem Real.smoothTransition.pos_denom

added theorem Real.smoothTransition.pos_of_pos

added theorem Real.smoothTransition.zero_of_nonpos

added def Real.smoothTransition

added theorem expNegInvGlue.contDiff_polynomial_eval_inv_mul

added theorem expNegInvGlue.continuous_polynomial_eval_inv_mul

added theorem expNegInvGlue.differentiable_polynomial_eval_inv_mul

added theorem expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul

added theorem expNegInvGlue.nonneg

added theorem expNegInvGlue.pos_of_pos

added theorem expNegInvGlue.tendsto_polynomial_inv_mul_zero

added theorem expNegInvGlue.zero_iff_nonpos

added theorem expNegInvGlue.zero_of_nonpos

added def expNegInvGlue

added def someContDiffBumpBase

Modified Mathlib/Analysis/Calculus/ContDiffDef.lean

added theorem ContDiffOn.contDiffAt

Created Mathlib/Analysis/SpecialFunctions/PolynomialExp.lean

added theorem Polynomial.tendsto_div_exp_atTop