Distribution

📁 Source: Mathlib/Analysis/Distribution/Distribution.lean

Statistics

Metric	Count
Definitions Distribution, delta, mapCLM, «term𝓓'(_,_)»»), «term𝓓'^{_}(_,_)»»)	5
Theorems delta_apply, delta_eq_zero_of_notMem, mapCLM_apply	3
Total	8

Distribution

Definitions

Name	Category	Theorems
delta 📖	CompOp	2 math math: delta_apply, delta_eq_zero_of_notMem
mapCLM 📖	CompOp	1 math math: mapCLM_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
delta_apply 📖	mathematical	—	DFunLike.coe Distribution Real Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace TestFunction Real.normedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup UniformConvergenceCLM.instFunLike RingHom.id Semiring.toNonAssocSemiring Real.semiring TestFunction.instAddCommGroup TestFunction.instModuleOfSMulCommClassRealOfContinuousConstSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField TestFunction.topologicalSpace setOf Set IsCompact delta TestFunctionClass.toDFunLike TestFunction.toTestFunctionClass	—	—
delta_eq_zero_of_notMem 📖	mathematical	TopologicalSpace.Opens UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.instMembership TopologicalSpace.Opens.instSetLike	delta Distribution Real Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid UniformConvergenceCLM.instAddCommGroup RingHom.id Semiring.toNonAssocSemiring Real.semiring TestFunction Real.normedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup TestFunction.instAddCommGroup TestFunction.instModuleOfSMulCommClassRealOfContinuousConstSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField TestFunction.topologicalSpace instIsTopologicalAddGroupReal setOf Set IsCompact	—	UniformConvergenceCLM.ext instIsTopologicalAddGroupReal TestFunction.tsupport_subset image_eq_zero_of_notMem_tsupport
mapCLM_apply 📖	mathematical	—	DFunLike.coe Distribution TestFunction Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformConvergenceCLM.instFunLike Real.normedField RingHom.id Semiring.toNonAssocSemiring Real.semiring TestFunction.instAddCommGroup TestFunction.instModuleOfSMulCommClassRealOfContinuousConstSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing TestFunction.topologicalSpace setOf Set IsCompact ContinuousLinearMap UniformConvergenceCLM.instTopologicalSpace AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing ContinuousSMul.continuousConstSMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike mapCLM	—	smulCommClass_self ContinuousSMul.continuousConstSMul

Distributions

Definitions

Name	Category	Theorems
«term𝓓'(_,_)» 📖» "API Documentation")	CompOp	—
«term𝓓'^{_}(_,_)»(_,_)»} 📖» "API Documentation")	CompOp	—

(root)

Definitions

Name	Category	Theorems
Distribution 📖	CompOp	3 math math: Distribution.delta_apply, Distribution.delta_eq_zero_of_notMem, Distribution.mapCLM_apply

---

← Back to Index