Commit 2023-07-18 23:02 2a2e08c9

View on Github →

refactor: split BumpFunctionInner (#5940) Fixes #4755

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/BumpFunction/Basic.lean

added theorem ContDiff.contDiffBump

added theorem ContDiffBump.eventuallyEq_one

added theorem ContDiffBump.eventuallyEq_one_of_mem_ball

added theorem ContDiffBump.le_one

added theorem ContDiffBump.nonneg'

added theorem ContDiffBump.nonneg

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 def ContDiffBump.toFun

added theorem ContDiffBump.tsupport_eq

added theorem ContDiffBump.zero_of_le_dist

added structure ContDiffBump

added structure ContDiffBumpBase

added def someContDiffBumpBase

Created Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean

added theorem ContDiffBump.convolution_eq_right

added theorem ContDiffBump.convolution_tendsto_right_of_continuous

added theorem ContDiffBump.dist_normed_convolution_le

added theorem ContDiffBump.normed_convolution_eq_right

Renamed Mathlib/Analysis/Calculus/BumpFunctionFindim.lean to Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

Created Mathlib/Analysis/Calculus/BumpFunction/InnerProduct.lean

Created Mathlib/Analysis/Calculus/BumpFunction/Normed.lean

added theorem ContDiffBump.contDiff_normed

added theorem ContDiffBump.continuous_normed

added theorem ContDiffBump.hasCompactSupport_normed

added theorem ContDiffBump.integral_normed

added theorem ContDiffBump.integral_normed_smul

added theorem ContDiffBump.integral_pos

added theorem ContDiffBump.nonneg_normed

added theorem ContDiffBump.normed_def

added theorem ContDiffBump.normed_neg

added theorem ContDiffBump.normed_sub

added theorem ContDiffBump.support_normed_eq

added theorem ContDiffBump.tendsto_support_normed_smallSets

added theorem ContDiffBump.tsupport_normed_eq

Deleted Mathlib/Analysis/Calculus/BumpFunctionInner.lean

deleted theorem ContDiff.contDiffBump

deleted theorem ContDiffBump.contDiff_normed

deleted theorem ContDiffBump.continuous_normed

deleted theorem ContDiffBump.eventuallyEq_one

deleted theorem ContDiffBump.eventuallyEq_one_of_mem_ball

deleted theorem ContDiffBump.hasCompactSupport_normed

deleted theorem ContDiffBump.integral_normed

deleted theorem ContDiffBump.integral_normed_smul

deleted theorem ContDiffBump.integral_pos

deleted theorem ContDiffBump.le_one

deleted theorem ContDiffBump.nonneg'

deleted theorem ContDiffBump.nonneg

deleted theorem ContDiffBump.nonneg_normed

deleted theorem ContDiffBump.normed_def

deleted theorem ContDiffBump.normed_neg

deleted theorem ContDiffBump.normed_sub

deleted theorem ContDiffBump.one_lt_rOut_div_rIn

deleted theorem ContDiffBump.one_of_mem_closedBall

deleted theorem ContDiffBump.pos_of_mem_ball

deleted theorem ContDiffBump.rOut_pos

deleted theorem ContDiffBump.support_eq

deleted theorem ContDiffBump.support_normed_eq

deleted theorem ContDiffBump.tendsto_support_normed_smallSets

deleted def ContDiffBump.toFun

deleted theorem ContDiffBump.tsupport_eq

deleted theorem ContDiffBump.tsupport_normed_eq

deleted theorem ContDiffBump.zero_of_le_dist

deleted structure ContDiffBump

deleted def ContDiffBumpBase.ofInnerProductSpace

deleted structure ContDiffBumpBase

deleted theorem Real.smoothTransition.le_one

deleted theorem Real.smoothTransition.lt_one_of_lt_one

deleted theorem Real.smoothTransition.nonneg

deleted theorem Real.smoothTransition.one_of_one_le

deleted theorem Real.smoothTransition.pos_denom

deleted theorem Real.smoothTransition.pos_of_pos

deleted theorem Real.smoothTransition.zero_of_nonpos

deleted def Real.smoothTransition

deleted theorem expNegInvGlue.contDiff_polynomial_eval_inv_mul

deleted theorem expNegInvGlue.continuous_polynomial_eval_inv_mul

deleted theorem expNegInvGlue.differentiable_polynomial_eval_inv_mul

deleted theorem expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul

deleted theorem expNegInvGlue.nonneg

deleted theorem expNegInvGlue.pos_of_pos

deleted theorem expNegInvGlue.tendsto_polynomial_inv_mul_zero

deleted theorem expNegInvGlue.zero_iff_nonpos

deleted theorem expNegInvGlue.zero_of_nonpos

deleted def expNegInvGlue

deleted def someContDiffBumpBase

Modified Mathlib/Analysis/Convolution.lean

deleted theorem ContDiffBump.convolution_eq_right

deleted theorem ContDiffBump.convolution_tendsto_right_of_continuous

deleted theorem ContDiffBump.dist_normed_convolution_le

deleted theorem ContDiffBump.normed_convolution_eq_right

Created Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean

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

Modified Mathlib/Geometry/Manifold/BumpFunction.lean