Convolution

📁 Source: Mathlib/Analysis/Calculus/ContDiff/Convolution.lean

Statistics

Metric	Count
Definitions	0
Theorems contDiff_convolution_left, contDiff_convolution_right, hasDerivAt_convolution_left, hasDerivAt_convolution_right, hasFDerivAt_convolution_left, hasFDerivAt_convolution_right, contDiffOn_convolution_left_with_param, contDiffOn_convolution_left_with_param_comp, contDiffOn_convolution_right_with_param, contDiffOn_convolution_right_with_param_aux, contDiffOn_convolution_right_with_param_comp, hasFDerivAt_convolution_right_with_param	12
Total	12

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiff_convolution_left 📖	mathematical	HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ContDiff DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField WithTop.some ENat MeasureTheory.LocallyIntegrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	MeasureTheory.convolution SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids MeasureTheory.convolution_flip ContinuousNeg.measurableNeg IsTopologicalAddGroup.toContinuousNeg ContinuousAdd.measurableAdd contDiff_convolution_right
contDiff_convolution_right 📖	mathematical	HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.LocallyIntegrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContDiff DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField WithTop.some ENat	MeasureTheory.convolution SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul exists_compact_iff_hasCompactSupport instR1Space TopologicalSpace.PseudoMetrizableSpace.regularSpace PseudoEMetricSpace.pseudoMetrizableSpace contDiffOn_univ MeasureTheory.contDiffOn_convolution_right_with_param_comp contDiffOn_id isOpen_univ ContDiff.contDiffOn ContDiff.comp contDiff_snd
hasDerivAt_convolution_left 📖	mathematical	HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ContDiff DenselyNormedField.toNontriviallyNormedField NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing InnerProductSpace.toNormedSpace NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat MeasureTheory.LocallyIntegrable RCLike.measurableSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	HasDerivAt NormedSpace.toModule IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul MeasureTheory.convolution SubNegMonoid.toSub NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup deriv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsBoundedSMul.continuousSMul RingHomIsometric.ids HasDerivAt.congr_simp ContinuousNeg.measurableNeg RCLike.borelSpace IsTopologicalRing.toContinuousNeg IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousAdd.measurableAdd IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring hasDerivAt_convolution_right
hasDerivAt_convolution_right 📖	mathematical	MeasureTheory.LocallyIntegrable RCLike.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup HasCompactSupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ContDiff DenselyNormedField.toNontriviallyNormedField NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	HasDerivAt NormedSpace.toModule IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul MeasureTheory.convolution SubNegMonoid.toSub NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup deriv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsBoundedSMul.continuousSMul RingHomIsometric.ids IsScalarTower.to_smulCommClass' Real.isScalarTower TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MeasureTheory.convolution_precompR_apply RCLike.borelSpace fderiv ContDiff.continuous_fderiv one_ne_zero NeZero.charZero_one WithTop.charZero HasFDerivAt.hasDerivAt hasFDerivAt_convolution_right
hasFDerivAt_convolution_left 📖	mathematical	HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ContDiff DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat MeasureTheory.LocallyIntegrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField MeasureTheory.convolution SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id AddCommGroup.toAddCommMonoid DenselyNormedField.toNormedField ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real Real.normedField IsScalarTower.to_smulCommClass' Real.instCommSemiring NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero fderiv ContinuousLinearMap.precompL	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousNeg.measurableNeg IsTopologicalAddGroup.toContinuousNeg ContinuousAdd.measurableAdd hasFDerivAt_convolution_right
hasFDerivAt_convolution_right 📖	mathematical	HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.LocallyIntegrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContDiff DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField MeasureTheory.convolution SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id AddCommGroup.toAddCommMonoid DenselyNormedField.toNormedField ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real Real.normedField IsScalarTower.to_smulCommClass' Real.instCommSemiring NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero fderiv ContinuousLinearMap.precompR	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace eq_zero_or_finiteDimensional RCLike.toCompleteSpace T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace ContDiff.continuous fderiv_const MeasureTheory.convolution_zero ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul hasFDerivAt_const FiniteDimensional.proper_rclike Filter.Eventually.of_forall MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd ContinuousAdd.measurableMul₂ secondCountable_of_proper ContinuousNeg.measurableNeg IsTopologicalAddGroup.toContinuousNeg MeasureTheory.IsAddLeftInvariant.isAddRightInvariant MeasureTheory.LocallyIntegrable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace Continuous.aestronglyMeasurable BorelSpace.opensMeasurable secondCountableTopologyEither_of_left ContDiff.continuous_fderiv one_ne_zero NeZero.charZero_one WithTop.charZero RingHomCompTriple.ids ContinuousLinearMap.comp.congr_simp sub_zero ContinuousLinearMap.comp_id HasFDerivAt.comp DifferentiableAt.hasFDerivAt Differentiable.differentiableAt ContDiff.differentiable HasFDerivAt.sub hasFDerivAt_id IsCompact.add IsCompact.neg isCompact fderiv ProperSpace.isCompact_closedBall hasFDerivAt_integral_of_dominated_of_fderiv_le Metric.ball_mem_nhds zero_lt_one Real.instZeroLEOneClass RCLike.charZero_rclike convolutionExists_right Filter.univ_mem' MeasureTheory.Measure.instOuterMeasureClass convolution_integrand_bound_right Metric.ball_subset_closedBall MeasureTheory.integrable_indicator_iff IsCompact.measurableSet MeasureTheory.Integrable.mul_const MeasureTheory.Integrable.const_mul MeasureTheory.Integrable.norm MeasureTheory.LocallyIntegrable.integrableOn_isCompact ContinuousLinearMap.hasFDerivAt

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffOn_convolution_left_with_param 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsCompact NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup LocallyIntegrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContDiffOn DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField WithTop.some ENat Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase SProd.sprod Set Set.instSProd Set.univ	convolution SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids convolution_flip ContinuousNeg.measurableNeg IsTopologicalAddGroup.toContinuousNeg ContinuousAdd.measurableAdd contDiffOn_convolution_right_with_param
contDiffOn_convolution_left_with_param_comp 📖	mathematical	ContDiffOn DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField WithTop.some ENat IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsCompact NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup LocallyIntegrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase SProd.sprod Set Set.instSProd Set.univ	convolution SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContDiffOn.comp contDiffOn_convolution_left_with_param ContDiffOn.prodMk contDiffOn_id
contDiffOn_convolution_right_with_param 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsCompact NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup LocallyIntegrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContDiffOn DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField WithTop.some ENat Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase SProd.sprod Set Set.instSProd Set.univ	convolution SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids RingHomCompTriple.ids Topology.IsClosedEmbedding.isCompact_preimage Homeomorph.isClosedEmbedding Continuous.isOpen_preimage ContinuousLinearEquiv.continuous contDiffOn_convolution_right_with_param_aux locallyIntegrable_map_homeomorph ContDiff.comp_contDiffOn ContinuousLinearEquiv.contDiff ContDiffOn.comp ContDiff.contDiffOn ContinuousLinearEquiv.apply_symm_apply Topology.IsClosedEmbedding.integral_map ContinuousLinearEquiv.integral_comp_comm
contDiffOn_convolution_right_with_param_aux 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsCompact NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup LocallyIntegrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContDiffOn DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField WithTop.some ENat Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase SProd.sprod Set Set.instSProd Set.univ	convolution SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ENat.nat_induction WithTop.coe_zero contDiffOn_zero continuousOn_convolution_right_with_param Nat.cast_add Nat.cast_one RingHomIsometric.ids IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace hasFDerivAt_convolution_right_with_param ContDiffOn.one_of_succ contDiffOn_succ_iff_fderiv_of_isOpen IsOpen.prod isOpen_univ DifferentiableAt.differentiableWithinAt HasFDerivAt.differentiableAt instIsEmptyFalse HasFDerivAt.fderiv Prod.continuousAdd Prod.continuousSMul hasFDerivAt_zero_of_eventually_const IsOpen.mem_nhds IsClosed.isOpen_compl IsCompact.isClosed nhds_prod_eq Filter.mp_mem Filter.prod_mem_prod Filter.univ_mem' ContDiffOn.congr contDiffOn_infty
contDiffOn_convolution_right_with_param_comp 📖	mathematical	ContDiffOn DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField WithTop.some ENat IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsCompact NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup LocallyIntegrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase SProd.sprod Set Set.instSProd Set.univ	convolution SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContDiffOn.comp contDiffOn_convolution_right_with_param ContDiffOn.prodMk contDiffOn_id
hasFDerivAt_convolution_right_with_param 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsCompact NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup LocallyIntegrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContDiffOn DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase SProd.sprod Set Set.instSProd Set.univ Set.instMembership	HasFDerivAt SeminormedAddCommGroup.toAddCommGroup Prod.seminormedAddCommGroup NormedSpace.toModule convolution SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id instTopologicalSpaceProd AddCommGroup.toAddCommMonoid Prod.instAddCommGroup Prod.instModule ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DenselyNormedField.toNormedField ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real Real.normedField IsScalarTower.to_smulCommClass' Real.instCommSemiring NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero fderiv ContinuousLinearMap.precompR	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousOn.comp_continuous ContDiffOn.continuousOn Continuous.prodMk_right IsOpen.mem_nhds IsOpen.prod isOpen_univ HasFDerivAt.fderiv Prod.continuousAdd Prod.continuousSMul IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace hasFDerivAt_zero_of_eventually_const IsClosed.isOpen_compl IsCompact.isClosed nhds_prod_eq Filter.mp_mem Filter.prod_mem_prod Filter.univ_mem' RingHomIsometric.ids IsScalarTower.to_smulCommClass' Real.isScalarTower IsCompact.prod isCompact_singleton ContDiffOn.continuousOn_fderiv_of_isOpen le_rfl Metric.exists_isOpen_isBounded_image_of_isCompact_of_continuousOn IsCompact.exists_thickening_subset_open Metric.isOpen_iff lt_min Set.Subset.trans Metric.thickening_mono min_le_left Metric.ball_subset_ball min_le_right Bornology.IsBounded.subset_closedBall_lt mem_ball_iff_norm Metric.mem_thickening_iff Set.singleton_prod dist_self dist_eq_norm Set.mem_image_of_mem mem_closedBall_zero_iff norm_zero LT.lt.le HasCompactSupport.convolutionExists_right IsCompact.of_isClosed_subset isClosed_tsupport closure_minimal Function.support_subset_iff' HasCompactSupport.intro instR1Space TopologicalSpace.PseudoMetrizableSpace.regularSpace PseudoEMetricSpace.pseudoMetrizableSpace RingHomCompTriple.ids IsCompact.add IsCompact.neg IsTopologicalAddGroup.toContinuousNeg LocallyIntegrable.integrableOn_nhds_isCompact compact_open_separated_add_right Metric.mem_nhds_iff HasSubset.Subset.trans Set.instIsTransSubset Set.add_subset_add_left ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul Measure.instOuterMeasureClass add_assoc Set.add_subset_add Set.neg_subset_neg LT.lt.trans_le LE.le.trans_lt le_max_left Prod.dist_eq add_ball Metric.thickening_singleton zero_vadd Set.instReflSubset convolution_integrand_bound_right_of_le_of_subset le_max_right integrable_indicator_iff IsOpen.measurableSet BorelSpace.opensMeasurable Integrable.mul_const Integrable.const_mul Integrable.norm HasFDerivAt.comp ContinuousLinearMap.hasFDerivAt lt_of_lt_of_le lt_of_le_of_lt DifferentiableAt.hasFDerivAt DifferentiableOn.differentiableAt ContDiffOn.differentiableOn one_ne_zero NeZero.charZero_one WithTop.charZero sub_zero HasFDerivAt.sub_const hasFDerivAt_id hasFDerivAt_integral_of_dominated_of_fderiv_le Metric.ball_mem_nhds

---

← Back to Index