Distribution

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

Statistics

Metric	Count
Definitions Distribution, mapCLM, «term𝓓'(_,_)»»), «term𝓓'^{_}(_,_)»»)	4
Theorems mapCLM_apply	1
Total	5

Distribution

Definitions

Name	Category	Theorems
mapCLM 📖	CompOp	1 math math: mapCLM_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapCLM_apply 📖	mathematical	—	DFunLike.coe Distribution TestFunction Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField UniformConvergenceCLM.instFunLike 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	1 math math: Distribution.mapCLM_apply

---

← Back to Index