Documentation Verification Report

CurrentDensity

📁 Source: PhysLean/Electromagnetism/Dynamics/CurrentDensity.lean

Statistics

Metric	Count
Definitions `CurrentDensity`, `DistLorentzCurrentDensity`, `chargeDensity`, `currentDensity`, `LorentzCurrentDensity`, `chargeDensity`, `currentDensity`	7
Theorems `chargeDensity_contDiff`, `chargeDensity_differentiable`, `chargeDensity_differentiable_space`, `chargeDensity_eq_timeSlice`, `chargeDensity_zero`, `currentDensity_ContDiff`, `currentDensity_apply_differentiable`, `currentDensity_apply_differentiable_space`, `currentDensity_apply_differentiable_time`, `currentDensity_differentiable`, `currentDensity_differentiable_space`, `currentDensity_differentiable_time`, `currentDensity_eq_timeSlice`, `currentDensity_zero`	14
Total	21

Electromagnetism

Definitions

Name	Category	Theorems
`CurrentDensity` 📖	CompOp	—
`DistLorentzCurrentDensity` 📖	CompOp	20 math math: `DistElectromagneticPotential.gradLagrangian_sum_inr_i`, `DistElectromagneticPotential.gradLagrangian_eq_tensor`, `DistElectromagneticPotential.isExtrema_iff_space_time`, `DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity`, `DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst`, `DistElectromagneticPotential.isExterma_iff_tensor`, `DistElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis`, `DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity`, `DistElectromagneticPotential.wireCurrentDensity_chargeDesnity`, `DistElectromagneticPotential.isExtrema_iff_vectorPotential`, `DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor`, `DistElectromagneticPotential.gradLagrangian_sum_inl_0`, `DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity`, `DistElectromagneticPotential.isExterma_equivariant`, `DistElectromagneticPotential.infiniteWire_isExterma`, `DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0`, `DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd`, `DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd`, `DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity`, `DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i`
`LorentzCurrentDensity` 📖	CompOp	4 math math: `LorentzCurrentDensity.chargeDensity_zero`, `LorentzCurrentDensity.currentDensity_zero`, `ElectromagneticPotential.constantEB_isExtrema`, `ElectromagneticPotential.harmonicWaveX_isExtrema`

Electromagnetism.DistLorentzCurrentDensity

Definitions

Name	Category	Theorems
`chargeDensity` 📖	CompOp	7 math math: `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time`, `Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity`, `Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity`
`currentDensity` 📖	CompOp	9 math math: `Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity`, `Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential`, `Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd`, `Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd`, `Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i`

Electromagnetism.LorentzCurrentDensity

Definitions

Name	Category	Theorems
`chargeDensity` 📖	CompOp	12 math math: `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField`, `chargeDensity_differentiable`, `chargeDensity_contDiff`, `Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField`, `chargeDensity_zero`, `chargeDensity_differentiable_space`, `Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential`, `chargeDensity_eq_timeSlice`, `Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_electricField_of_isExtrema`, `Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic`, `Electromagnetism.ElectromagneticPotential.isExtrema_iff_gauss_ampere_magneticFieldMatrix`, `Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity`
`currentDensity` 📖	CompOp	18 math math: `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField`, `currentDensity_differentiable_space`, `Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField`, `currentDensity_apply_differentiable_space`, `Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_magneticFieldMatrix_of_isExtrema`, `currentDensity_eq_timeSlice`, `currentDensity_zero`, `currentDensity_apply_differentiable`, `currentDensity_differentiable`, `currentDensity_ContDiff`, `Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential`, `currentDensity_differentiable_time`, `currentDensity_apply_differentiable_time`, `Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_electricField_of_isExtrema`, `Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic`, `Electromagnetism.ElectromagneticPotential.isExtrema_iff_gauss_ampere_magneticFieldMatrix`, `Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity`, `Electromagnetism.ElectromagneticPotential.time_deriv_electricField_of_isExtrema`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chargeDensity_contDiff` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `chargeDensity`	—	`chargeDensity_eq_timeSlice` `SpaceTime.timeSlice_contDiff` `SpaceTime.contDiff_vector`
`chargeDensity_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` `chargeDensity`	—	`chargeDensity_eq_timeSlice` `SpaceTime.timeSlice_differentiable` `SpaceTime.differentiable_vector`
`chargeDensity_differentiable_space` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`Space` `Space.instAddCommGroup` `Space.instModuleReal` `Space.instSeminormedAddCommGroup` `chargeDensity`	—	`chargeDensity_differentiable`
`chargeDensity_eq_timeSlice` 📖	mathematical	—	`chargeDensity` `SpaceTime.timeSlice` `SpeedOfLight.val`	—	—
`chargeDensity_zero` 📖	mathematical	—	`chargeDensity` `Electromagnetism.LorentzCurrentDensity` `SpaceTime` `Lorentz.Vector` `Lorentz.Vector.instAddCommGroup` `Time` `Space`	—	`chargeDensity_eq_timeSlice`
`currentDensity_ContDiff` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `currentDensity`	—	`currentDensity_eq_timeSlice` `SpaceTime.timeSlice_contDiff` `SpaceTime.contDiff_vector`
`currentDensity_apply_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` `currentDensity`	—	`currentDensity_differentiable`
`currentDensity_apply_differentiable_space` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`Space` `Space.instAddCommGroup` `Space.instModuleReal` `Space.instSeminormedAddCommGroup` `currentDensity`	—	`currentDensity_differentiable`
`currentDensity_apply_differentiable_time` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`Time` `Time.instAddCommGroup` `Time.instModuleReal` `Time.instSeminormedAddCommGroup` `currentDensity`	—	`currentDensity_differentiable`
`currentDensity_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` `currentDensity`	—	`currentDensity_eq_timeSlice` `SpaceTime.timeSlice_differentiable` `SpaceTime.differentiable_vector`
`currentDensity_differentiable_space` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`Space` `Space.instAddCommGroup` `Space.instModuleReal` `Space.instSeminormedAddCommGroup` `currentDensity`	—	`currentDensity_differentiable`
`currentDensity_differentiable_time` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`Time` `Time.instAddCommGroup` `Time.instModuleReal` `Time.instSeminormedAddCommGroup` `currentDensity`	—	`currentDensity_differentiable`
`currentDensity_eq_timeSlice` 📖	mathematical	—	`currentDensity` `SpaceTime.timeSlice`	—	—
`currentDensity_zero` 📖	mathematical	—	`currentDensity` `Electromagnetism.LorentzCurrentDensity` `SpaceTime` `Lorentz.Vector` `Lorentz.Vector.instAddCommGroup` `Time` `Space`	—	`currentDensity_eq_timeSlice`

---

← Back to Index