Basic

📁 Source: Mathlib/Analysis/Calculus/BumpFunction/Basic.lean

Statistics

Metric	Count
Definitions ContDiffBump, instCoeFunForallReal, instInhabited, rIn, rOut, toFun, ContDiffBumpBase, toFun, HasContDiffBump, someContDiffBumpBase	10
Theorems contDiffBump, contDiffBump, apply, contDiff, contDiffAt, contDiffWithinAt, continuous, eventuallyEq_one, eventuallyEq_one_of_mem_ball, hasCompactSupport, le_one, neg, nonneg, nonneg', one_lt_rOut_div_rIn, one_of_mem_closedBall, pos_of_mem_ball, rIn_lt_rOut, rIn_pos, rOut_pos, sub, support_eq, tsupport_eq, zero_of_le_dist, eq_one, mem_Icc, smooth, support, symmetric, contDiffBump, out	31
Total	41

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffBump 📖	mathematical	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField ContDiffBump.rIn ContDiffBump.rOut	ContDiffBump.toFun	—	contDiff_iff_contDiffAt ContDiffAt.contDiffBump

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffBump 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField ContDiffBump.rIn ContDiffBump.rOut	ContDiffBump.toFun	—	ContDiffWithinAt.contDiffBump

ContDiffBump

Definitions

Name	Category	Theorems
instCoeFunForallReal 📖	CompOp	—
instInhabited 📖	CompOp	—
rIn 📖	CompOp	7 math math: one_lt_rOut_div_rIn, rIn_lt_rOut, SmoothBumpFunction.updateRIn_rIn, measure_closedBall_le_integral, apply, normed_le_div_measure_closedBall_rIn, rIn_pos
rOut 📖	CompOp	21 math math: SmoothBumpFunction.support_eq_symm_image, SmoothBumpFunction.rOut_pos, support_normed_eq, SmoothBumpFunction.exists_r_pos_lt_subset_ball, one_lt_rOut_div_rIn, SmoothBumpFunction.support_eq_inter_preimage, SmoothBumpFunction.tsupport_subset_symm_image_closedBall, rIn_lt_rOut, SmoothBumpFunction.ball_subset, support_eq, SmoothBumpFunction.isClosed_symm_image_closedBall, apply, integral_le_measure_closedBall, tsupport_eq, tsupport_normed_eq, SmoothBumpFunction.nhdsWithin_range_basis, SmoothBumpFunction.image_eq_inter_preimage_of_subset_support, SmoothBumpFunction.closedBall_subset, SmoothBumpFunction.isCompact_symm_image_closedBall, SmoothBumpFunction.ball_inter_range_eq_ball_inter_target, rOut_pos
toFun 📖	CompOp	31 math math: integrable, eventuallyEq_one, pos_of_mem_ball, normed_def, measure_closedBall_div_le_integral, nonneg, contDiff, hasCompactSupport, support_eq, SmoothBumpFunction.eqOn_source, measure_closedBall_le_integral, SmoothBumpFunction.eventuallyEq_of_mem_source, apply, continuous, contDiffAt, integral_le_measure_closedBall, tsupport_eq, SmoothBumpFunction.coe_def, convolution_eq_right, eventuallyEq_one_of_mem_ball, neg, one_of_mem_closedBall, ContDiff.contDiffBump, ContDiffWithinAt.contDiffBump, nonneg', le_one, zero_of_le_dist, contDiffWithinAt, ContDiffAt.contDiffBump, integral_pos, sub

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply 📖	mathematical	—	toFun ContDiffBumpBase.toFun someContDiffBumpBase Real DivInvMonoid.toDiv Real.instDivInvMonoid rOut rIn SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Real.instInv SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	—
contDiff 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField WithTop.some ENat toFun	—	ContDiff.contDiffBump contDiff_const contDiff_id
contDiffAt 📖	mathematical	—	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField WithTop.some ENat toFun	—	ContDiff.contDiffAt contDiff
contDiffWithinAt 📖	mathematical	—	ContDiffWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField WithTop.some ENat toFun	—	ContDiffAt.contDiffWithinAt contDiffAt
continuous 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.pseudoMetricSpace toFun	—	contDiff_zero contDiff
eventuallyEq_one 📖	mathematical	—	Filter.EventuallyEq Real nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFun Pi.instOne Real.instOne	—	eventuallyEq_one_of_mem_ball Metric.mem_ball_self rIn_pos
eventuallyEq_one_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup rIn	Filter.EventuallyEq Real nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace toFun Pi.instOne Real.instOne	—	Filter.mem_of_superset Metric.closedBall_mem_nhds_of_mem one_of_mem_closedBall
hasCompactSupport 📖	mathematical	—	HasCompactSupport Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instZero toFun	—	tsupport_eq FiniteDimensional.proper_real
le_one 📖	mathematical	—	Real Real.instLE toFun Real.instOne	—	ContDiffBumpBase.mem_Icc
neg 📖	mathematical	—	toFun NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NegZeroClass.toNeg	—	toFun.congr_simp sub zero_add
nonneg 📖	mathematical	—	Real Real.instLE Real.instZero toFun	—	ContDiffBumpBase.mem_Icc
nonneg' 📖	mathematical	—	Real Real.instLE Real.instZero toFun	—	nonneg
one_lt_rOut_div_rIn 📖	mathematical	—	Real Real.instLT Real.instOne DivInvMonoid.toDiv Real.instDivInvMonoid rOut rIn	—	one_lt_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing rIn_pos rIn_lt_rOut
one_of_mem_closedBall 📖	mathematical	Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup rIn	toFun Real Real.instOne	—	ContDiffBumpBase.eq_one one_lt_rOut_div_rIn norm_smul NormedSpace.toNormSMulClass abs_inv Real.instIsStrictOrderedRing abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le rIn_pos div_le_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mem_closedBall_iff_norm
pos_of_mem_ball 📖	mathematical	Set Set.instMembership Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup rOut	Real Real.instLT Real.instZero toFun	—	LE.le.lt_of_ne' nonneg Function.mem_support support_eq
rIn_lt_rOut 📖	mathematical	—	Real Real.instLT rIn rOut	—	—
rIn_pos 📖	mathematical	—	Real Real.instLT Real.instZero rIn	—	—
rOut_pos 📖	mathematical	—	Real Real.instLT Real.instZero rOut	—	LT.lt.trans rIn_pos rIn_lt_rOut
sub 📖	mathematical	—	toFun SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	sub_sub_cancel_left smul_neg ContDiffBumpBase.symmetric add_sub_cancel_left
support_eq 📖	mathematical	—	Function.support Real Real.instZero toFun Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup rOut	—	ContDiffBumpBase.support one_lt_rOut_div_rIn Set.ext sub_zero norm_smul NormedSpace.toNormSMulClass abs_inv Real.instIsStrictOrderedRing abs_of_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid rIn_pos div_lt_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono
tsupport_eq 📖	mathematical	—	tsupport Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFun Metric.closedBall rOut	—	support_eq closure_ball LT.lt.ne' rOut_pos
zero_of_le_dist 📖	mathematical	Real Real.instLE rOut Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	toFun Real.instZero	—	Function.notMem_support support_eq Metric.mem_ball not_lt

ContDiffBumpBase

Definitions

Name	Category	Theorems
toFun 📖	CompOp	6 math math: smooth, mem_Icc, support, ContDiffBump.apply, symmetric, eq_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_one 📖	mathematical	Real Real.instLT Real.instOne Real.instLE Norm.norm NormedAddCommGroup.toNorm	toFun	—	—
mem_Icc 📖	mathematical	—	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne toFun	—	—
smooth 📖	mathematical	—	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Real.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup NormedField.toNormedSpace WithTop.some ENat Top.top instTopENat toFun SProd.sprod Set Set.instSProd Set.Ioi Real.instPreorder Real.instOne Set.univ	—	—
support 📖	mathematical	Real Real.instLT Real.instOne	Function.support Real.instZero toFun Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—
symmetric 📖	mathematical	—	toFun NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffBump 📖	mathematical	ContDiffWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField ContDiffBump.rIn ContDiffBump.rOut	ContDiffBump.toFun	—	ContDiffAt.comp_contDiffWithinAt ContDiffAt.of_le ContDiffOn.contDiffAt ContDiffBumpBase.smooth prod_mem_nhds Ioi_mem_nhds instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ContDiffBump.one_lt_rOut_div_rIn Filter.univ_mem le_top prodMk div LT.lt.ne' ContDiffBump.rIn_pos smul NormedSpace.toIsBoundedSMul IsScalarTower.left inv sub

HasContDiffBump

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	ContDiffBumpBase	—	—

(root)

Definitions

Name	Category	Theorems
ContDiffBump 📖	CompData	—
ContDiffBumpBase 📖	CompData	1 math math: HasContDiffBump.out
HasContDiffBump 📖	CompData	2 math math: ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal, hasContDiffBump_of_innerProductSpace
someContDiffBumpBase 📖	CompOp	1 math math: ContDiffBump.apply

---

← Back to Index