Documentation Verification Report

Basic

📁 Source: PhysLean/Mathematics/Distribution/Basic.lean

Statistics

Metric	Count
Definitions `const`, `diracDelta`, `diracDelta'`, `fderivD`, `fourierTransform`, `heavisideStep`, `ofLinear`, `«term_→d[_]_»`	8
Theorems `const_apply`, `diracDelta'_apply`, `diracDelta_apply`, `fderivD_apply`, `fderivD_const`, `fourierTransform_apply`, `heavisideStep_apply`, `ofLinear_apply`	8
Total	16

Distribution

Definitions

Name	Category	Theorems
`const` 📖	CompOp	2 math math: `const_apply`, `fderivD_const`
`diracDelta` 📖	CompOp	7 math math: `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField`, `Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst`, `Space.distDiv_inv_pow_eq_dim`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField`, `diracDelta_apply`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity`
`diracDelta'` 📖	CompOp	3 math math: `Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate`, `diracDelta'_apply`
`fderivD` 📖	CompOp	8 math math: `Space.distSpaceDeriv_apply`, `Space.distGrad_inner_eq`, `SpaceTime.distDeriv_apply`, `Space.distDiv_apply_eq_sum_fderivD`, `Space.distDeriv_apply`, `Space.distTimeDeriv_apply`, `fderivD_apply`, `fderivD_const`
`fourierTransform` 📖	CompOp	1 math math: `fourierTransform_apply`
`heavisideStep` 📖	CompOp	1 math math: `heavisideStep_apply`
`ofLinear` 📖	CompOp	1 math math: `ofLinear_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_apply` 📖	mathematical	—	`Distribution` `const`	—	—
`diracDelta'_apply` 📖	mathematical	—	`Distribution` `diracDelta'`	—	—
`diracDelta_apply` 📖	mathematical	—	`Distribution` `diracDelta`	—	—
`fderivD_apply` 📖	mathematical	—	`Distribution` `fderivD`	—	—
`fderivD_const` 📖	mathematical	—	`Distribution` `fderivD` `const`	—	`fderivD_apply` `const_apply`
`fourierTransform_apply` 📖	mathematical	—	`Distribution` `fourierTransform`	—	—
`heavisideStep_apply` 📖	mathematical	—	`Distribution` `heavisideStep`	—	—
`ofLinear_apply` 📖	mathematical	—	`Distribution` `ofLinear`	—	—

(root)

Definitions

Name	Category	Theorems
`«term_→d[_]_»` 📖	CompOp	—

---

← Back to Index