Documentation Verification Report

ScalarPotential

📁 Source: PhysLean/Electromagnetism/Kinematics/ScalarPotential.lean

Statistics

Metric	Count
Definitions `scalarPotential`, `scalarPotential`	2
Theorems `scalarPotential_contDiff`, `scalarPotential_contDiff_space`, `scalarPotential_contDiff_time`, `scalarPotential_differentiable`, `scalarPotential_differentiable_space`, `scalarPotential_differentiable_time`	6
Total	8

Electromagnetism.DistElectromagneticPotential

Definitions

Name	Category	Theorems
`scalarPotential` 📖	CompOp	3 math math: `oneDimPointParticle_scalarPotential`, `threeDimPointParticle_scalarPotential`, `infiniteWire_scalarPotential`

Electromagnetism.ElectromagneticPotential

Definitions

Name	Category	Theorems
`scalarPotential` 📖	CompOp	15 math math: `hamiltonian_eq_electricField_scalarPotential`, `hamiltonian_eq_electricField_magneticField`, `scalarPotential_contDiff_space`, `scalarPotential_differentiable_time`, `electricField_eq`, `scalarPotential_contDiff`, `scalarPotential_differentiable_space`, `time_deriv_comp_vectorPotential_eq_electricField`, `harmonicWaveX_scalarPotential_eq_zero`, `scalarPotential_differentiable`, `time_deriv_vectorPotential_eq_electricField`, `freeCurrentPotential_eq_sum_scalarPotential_vectorPotential`, `constantEB_scalarPotential`, `lagrangian_eq_electric_magnetic`, `scalarPotential_contDiff_time`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scalarPotential_contDiff` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `scalarPotential`	—	`SpaceTime.timeSlice_contDiff` `SpaceTime.contDiff_vector`
`scalarPotential_contDiff_space` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `scalarPotential`	—	`scalarPotential_contDiff`
`scalarPotential_contDiff_time` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal` `scalarPotential`	—	`scalarPotential_contDiff`
`scalarPotential_differentiable` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`Time` `Space` `Time.instAddCommGroup` `Space.instAddCommGroup` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `Space.instSeminormedAddCommGroup` `scalarPotential`	—	`SpaceTime.timeSlice_differentiable` `SpaceTime.differentiable_vector`
`scalarPotential_differentiable_space` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`Space` `Space.instAddCommGroup` `Space.instModuleReal` `Space.instSeminormedAddCommGroup` `scalarPotential`	—	`scalarPotential_differentiable`
`scalarPotential_differentiable_time` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`Time` `Time.instAddCommGroup` `Time.instModuleReal` `Time.instSeminormedAddCommGroup` `scalarPotential`	—	`scalarPotential_differentiable`

---

← Back to Index