Documentation Verification Report

Hamiltonian

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

Statistics

Metric	Count
Definitions `canonicalMomentum`, `hamiltonian`	2
Theorems `canonicalMomentum_eq`, `canonicalMomentum_eq_electricField`, `canonicalMomentum_eq_gradient_kineticTerm`, `hamiltonian_eq_electricField_magneticField`, `hamiltonian_eq_electricField_scalarPotential`, `hamiltonian_eq_electricField_vectorPotential`	6
Total	8

Electromagnetism.ElectromagneticPotential

Definitions

Name	Category	Theorems
`canonicalMomentum` 📖	CompOp	3 math math: `canonicalMomentum_eq_electricField`, `canonicalMomentum_eq_gradient_kineticTerm`, `canonicalMomentum_eq`
`hamiltonian` 📖	CompOp	3 math math: `hamiltonian_eq_electricField_scalarPotential`, `hamiltonian_eq_electricField_magneticField`, `hamiltonian_eq_electricField_vectorPotential`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`canonicalMomentum_eq` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`canonicalMomentum` `Electromagnetism.FreeSpace.μ₀` `minkowskiMatrix` `fieldStrengthMatrix`	—	`Lorentz.Vector.instFiniteDimensionalReal` `canonicalMomentum_eq_gradient_kineticTerm` `kineticTerm_add_time_mul_const` `Lorentz.Vector.coord_differentiableAt` `Lorentz.Vector.fderiv_coord` `fieldStrengthMatrix.eq_1` `toFieldStrength_basis_repr_apply_eq_single` `minkowskiMatrix.inl_0_inl_0` `minkowskiMatrix.η_apply_sq_eq_one`
`canonicalMomentum_eq_electricField` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`canonicalMomentum` `Electromagnetism.FreeSpace.μ₀` `SpeedOfLight.val` `Electromagnetism.FreeSpace.c` `electricField` `Time` `Lorentz.Vector.instAddCommMonoid` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Lorentz.Vector.instModuleReal` `Time.instModuleReal` `SpaceTime.time` `Space` `Space.instSeminormedAddCommGroup` `Space.instAddCommMonoid` `Space.instModuleReal` `SpaceTime.space`	—	`canonicalMomentum_eq` `minkowskiMatrix.inl_0_inl_0` `fieldStrengthMatrix_diag_eq_zero` `minkowskiMatrix.inr_i_inr_i` `electricField_eq_fieldStrengthMatrix` `SpaceTime.toTimeAndSpace_symm_apply_time_space` `fieldStrengthMatrix_antisymm`
`canonicalMomentum_eq_gradient_kineticTerm` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`canonicalMomentum` `Lorentz.Vector.innerProductSpace` `Lorentz.Vector.instFiniteDimensionalReal` `kineticTerm` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.instAddCommGroup`	—	`Lorentz.Vector.instFiniteDimensionalReal` `canonicalMomentum.eq_1` `lagrangian_add_const` `kineticTerm_add_time_mul_const` `Lorentz.Vector.coord_differentiable`
`hamiltonian_eq_electricField_magneticField` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`hamiltonian` `Electromagnetism.FreeSpace.ε₀` `electricField` `Electromagnetism.FreeSpace.c` `Time` `Lorentz.Vector.instAddCommMonoid` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Lorentz.Vector.instModuleReal` `Time.instModuleReal` `SpaceTime.time` `Space` `Space.instSeminormedAddCommGroup` `Space.instAddCommMonoid` `Space.instModuleReal` `SpaceTime.space` `SpeedOfLight.val` `magneticFieldMatrix` `instInnerOfInnerProductSpace'` `instInnerProductSpace'` `Space.grad` `scalarPotential` `Electromagnetism.LorentzCurrentDensity.chargeDensity` `vectorPotential` `Electromagnetism.LorentzCurrentDensity.currentDensity`	—	`hamiltonian_eq_electricField_scalarPotential` `lagrangian_eq_electric_magnetic` `Electromagnetism.FreeSpace.c_sq`
`hamiltonian_eq_electricField_scalarPotential` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`hamiltonian` `SpeedOfLight.val` `Electromagnetism.FreeSpace.c` `Electromagnetism.FreeSpace.μ₀` `electricField` `Time` `Lorentz.Vector.instAddCommMonoid` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Lorentz.Vector.instModuleReal` `Time.instModuleReal` `SpaceTime.time` `Space` `Space.instSeminormedAddCommGroup` `Space.instAddCommMonoid` `Space.instModuleReal` `SpaceTime.space` `instInnerOfInnerProductSpace'` `instInnerProductSpace'` `Space.grad` `scalarPotential` `lagrangian`	—	`hamiltonian_eq_electricField_vectorPotential` `time_deriv_vectorPotential_eq_electricField`
`hamiltonian_eq_electricField_vectorPotential` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`hamiltonian` `SpeedOfLight.val` `Electromagnetism.FreeSpace.c` `Electromagnetism.FreeSpace.μ₀` `electricField` `Time` `Lorentz.Vector.instAddCommMonoid` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Lorentz.Vector.instModuleReal` `Time.instModuleReal` `SpaceTime.time` `Space` `Space.instSeminormedAddCommGroup` `Space.instAddCommMonoid` `Space.instModuleReal` `SpaceTime.space` `Time.deriv` `vectorPotential` `lagrangian`	—	`hamiltonian.eq_1` `canonicalMomentum_eq_electricField` `SpaceTime.deriv_sum_inl` `Time.deriv_euclid` `vectorPotential_differentiable_time` `Time.deriv_lorentzVector`

---

← Back to Index