Documentation Verification Report

Translations

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

Statistics

Metric	Count
Definitions `distTranslate`, `translateSchwartz`	2
Theorems `distDiv_distTranslate`, `distTranslate_apply`, `distTranslate_distGrad`, `distTranslate_ofFunction`, `translateSchwartz_apply`, `translateSchwartz_coe_eq`	6
Total	8

Space

Definitions

Name	Category	Theorems
`distTranslate` 📖	CompOp	8 math math: `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate`, `distTranslate_apply`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate`, `distTranslate_ofFunction`, `distTranslate_distGrad`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate`, `distDiv_distTranslate`
`translateSchwartz` 📖	CompOp	3 math math: `translateSchwartz_apply`, `distTranslate_apply`, `translateSchwartz_coe_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`distDiv_distTranslate` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distDiv` `distTranslate`	—	`instFiniteDimensionalReal` `distDiv_apply_eq_sum_fderivD` `distTranslate_apply` `Distribution.fderivD_apply` `translateSchwartz_apply` `translateSchwartz_coe_eq`
`distTranslate_apply` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distTranslate` `translateSchwartz`	—	—
`distTranslate_distGrad` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distGrad` `distTranslate`	—	`distGrad_eq_of_inner` `instFiniteDimensionalReal` `distTranslate_apply` `distGrad_inner_eq` `Distribution.fderivD_apply` `translateSchwartz_coe_eq`
`distTranslate_ofFunction` 📖	mathematical	`IsDistBounded`	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distTranslate` `distOfFunction` `basis` `IsDistBounded.comp_add_right` `instNeg`	—	`IsDistBounded.comp_add_right` `distTranslate_apply` `instFiniteDimensionalReal` `instBorelSpace` `distOfFunction_apply`
`translateSchwartz_apply` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `translateSchwartz` `basis`	—	—
`translateSchwartz_coe_eq` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `translateSchwartz` `basis`	—	—

---

← Back to Index