Documentation Verification Report

VectorPotential

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

Statistics

Metric	Count
Definitions `vectorPotential`, `vectorPotential`, `VectorPotential`	3
Theorems `vectorPotential_apply_contDiff`, `vectorPotential_apply_contDiff_space`, `vectorPotential_comp_contDiff`, `vectorPotential_contDiff`, `vectorPotential_contDiff_of_smooth`, `vectorPotential_contDiff_space`, `vectorPotential_contDiff_time`, `vectorPotential_differentiable`, `vectorPotential_differentiable_time`	9
Total	12

Electromagnetism

Definitions

Name	Category	Theorems
`VectorPotential` 📖	CompOp	—

Electromagnetism.DistElectromagneticPotential

Definitions

Name	Category	Theorems
`vectorPotential` 📖	CompOp	12 math math: `infiniteWire_vectorPotential_thrd`, `threeDimPointParticle_vectorPotential`, `magneticFieldMatrix_eq_vectorPotential`, `infiniteWire_vectorPotential_fst`, `oneDimPointParticle_vectorPotential`, `infiniteWire_vectorPotential`, `infiniteWire_vectorPotential_distTimeDeriv`, `magneticFieldMatrix_basis_repr_eq_vector_potential`, `infiniteWire_vectorPotential_snd`, `isExtrema_iff_vectorPotential`, `magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential`, `infiniteWire_vectorPotential_distSpaceDeriv_0`

Electromagnetism.ElectromagneticPotential

Definitions

Name	Category	Theorems
`vectorPotential` 📖	CompOp	28 math math: `hamiltonian_eq_electricField_magneticField`, `constantEB_vectorPotential_time_deriv`, `harmonicWaveX_vectorPotential_space_deriv_succ`, `hamiltonian_eq_electricField_vectorPotential`, `magneticField_eq`, `vectorPotential_contDiff_of_smooth`, `vectorPotential_contDiff_time`, `harmonicWaveX_vectorPotential_succ`, `electricField_eq`, `harmonicWaveX_vectorPotential_succ'`, `vectorPotential_apply_contDiff`, `vectorPotential_differentiable_time`, `Electromagnetism.ThreeDimension.magneticField_eq_3D`, `vectorPotential_contDiff`, `time_deriv_comp_vectorPotential_eq_electricField`, `constantEB_vectorPotential_space_deriv`, `vectorPotential_contDiff_space`, `time_deriv_vectorPotential_eq_electricField`, `freeCurrentPotential_eq_sum_scalarPotential_vectorPotential`, `vectorPotential_comp_contDiff`, `magneticFieldMatrix_eq_vectorPotential`, `vectorPotential_apply_contDiff_space`, `constantEB_vectorPotential`, `harmonicWaveX_vectorPotential_succ_space_deriv_zero`, `harmonicWaveX_vectorPotential_zero_eq_zero`, `lagrangian_eq_electric_magnetic`, `vectorPotential_differentiable`, `Electromagnetism.ThreeDimension.electricField_eq_3D`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vectorPotential_apply_contDiff` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector` `val`	`Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `vectorPotential`	—	`vectorPotential_contDiff`
`vectorPotential_apply_contDiff_space` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector` `val`	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `vectorPotential`	—	`vectorPotential_contDiff_space`
`vectorPotential_comp_contDiff` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector` `val`	`Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `vectorPotential`	—	`vectorPotential_contDiff`
`vectorPotential_contDiff` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector` `val`	`Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `vectorPotential`	—	`SpaceTime.timeSlice_contDiff` `SpaceTime.contDiff_vector`
`vectorPotential_contDiff_of_smooth` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector` `val`	`Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `vectorPotential`	—	`vectorPotential_contDiff`
`vectorPotential_contDiff_space` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector` `val`	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `vectorPotential`	—	`vectorPotential_contDiff`
`vectorPotential_contDiff_time` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector` `val`	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal` `vectorPotential`	—	`vectorPotential_contDiff`
`vectorPotential_differentiable` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector` `val`	`Time` `Space` `Time.instAddCommGroup` `Space.instAddCommGroup` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `Space.instPseudoMetricSpace` `vectorPotential`	—	`SpaceTime.timeSlice_differentiable` `SpaceTime.differentiable_vector`
`vectorPotential_differentiable_time` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector` `val`	`Time` `Time.instAddCommGroup` `Time.instModuleReal` `Time.instSeminormedAddCommGroup` `vectorPotential`	—	`vectorPotential_differentiable`

---

← Back to Index