Documentation Verification Report

DistConst

📁 Source: PhysLean/SpaceAndTime/Space/DistConst.lean

Statistics

Metric	Count
Definitions `distConst`	1
Theorems `distCurl_distConst`, `distDeriv_distConst`, `distDiv_distConst`, `distGrad_distConst`	4
Total	5

Space

Definitions

Name	Category	Theorems
`distConst` 📖	CompOp	4 math math: `distCurl_distConst`, `distDeriv_distConst`, `distGrad_distConst`, `distDiv_distConst`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`distCurl_distConst` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distCurl` `distConst`	—	`instFiniteDimensionalReal` `instBorelSpace` `Distribution.fderivD_const`
`distDeriv_distConst` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distDeriv` `distConst`	—	`instFiniteDimensionalReal` `instBorelSpace` `Distribution.fderivD_const`
`distDiv_distConst` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distDiv` `distConst`	—	`instFiniteDimensionalReal` `instBorelSpace` `Distribution.fderivD_const`
`distGrad_distConst` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distGrad` `distConst`	—	`instFiniteDimensionalReal` `instBorelSpace` `Distribution.fderivD_const`

---

← Back to Index