Documentation Verification Report

ElectricField

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

Statistics

Metric	Count
Definitions `electricField`, `ElectricField`, `electricField`	3
Theorems `electricField_eq_fieldStrength`, `div_electricField_eq_fieldStrengthMatrix`, `electricField_apply_contDiff`, `electricField_apply_contDiff_space`, `electricField_apply_contDiff_time`, `electricField_apply_differentiable`, `electricField_apply_differentiable_space`, `electricField_apply_differentiable_time`, `electricField_contDiff`, `electricField_differentiable`, `electricField_differentiable_space`, `electricField_differentiable_time`, `electricField_eq`, `electricField_eq_fieldStrengthMatrix`, `fieldStrengthMatrix_inl_inr_eq_electricField`, `fieldStrengthMatrix_inr_inl_eq_electricField`, `time_deriv_comp_vectorPotential_eq_electricField`, `time_deriv_electricField_eq_fieldStrengthMatrix`, `time_deriv_vectorPotential_eq_electricField`	19
Total	22

Electromagnetism

Definitions

Name	Category	Theorems
`ElectricField` 📖	CompOp	2 math math: `ElectromagneticPotential.electricField_differentiable`, `ElectromagneticPotential.electricField_contDiff`

Electromagnetism.DistElectromagneticPotential

Definitions

Name	Category	Theorems
`electricField` 📖	CompOp	14 math math: `gradLagrangian_sum_inr_i`, `oneDimPointParticle_div_electricField`, `gradKineticTerm_sum_inl_eq`, `infiniteWire_electricField`, `isExtrema_iff_space_time`, `oneDimPointParticle_electricField_timeDeriv`, `gradKineticTerm_sum_inr_eq`, `threeDimPointParticle_electricField`, `oneDimPointParticle_electricField`, `isExtrema_iff_vectorPotential`, `gradLagrangian_sum_inl_0`, `threeDimPointParticle_div_electricField`, `electricField_eq_fieldStrength`, `threeDimPointParticle_electricField_timeDeriv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`electricField_eq_fieldStrength` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `Electromagnetism.DistElectromagneticPotential` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instAddCommGroup` `electricField` `SpeedOfLight.val` `Lorentz.Vector.basis` `Lorentz.Vector.innerProductSpace` `SpaceTime.distTimeSlice` `fieldStrength`	—	`SpaceTime.distTimeSlice_apply` `fieldStrength_basis_repr_eq_single` `minkowskiMatrix.inl_0_inl_0` `minkowskiMatrix.inr_i_inr_i` `Lorentz.Vector.instFiniteDimensionalReal` `Space.distTimeDeriv_apply_CLM` `Space.distSpaceGrad_apply` `Space.distSpaceDeriv_apply_CLM` `SpaceTime.distTimeSlice_distDeriv_inl` `SpaceTime.distTimeSlice_distDeriv_inr`

Electromagnetism.ElectromagneticPotential

Definitions

Name	Category	Theorems
`electricField` 📖	CompOp	59 math math: `harmonicWaveX_polarization_ellipse`, `harmonicWaveX_electricField_space_deriv_same`, `hamiltonian_eq_electricField_scalarPotential`, `IsPlaneWave.magneticFieldMatrix_eq_propogator_cross_electricField`, `kineticTerm_eq_electric_magnetic'`, `hamiltonian_eq_electricField_magneticField`, `canonicalMomentum_eq_electricField`, `harmonicWaveX_electricField_succ_time_deriv`, `electricField_apply_contDiff`, `constantEB_electricField`, `fieldStrengthMatrix_inr_inl_eq_electricField`, `electricField_differentiable_space`, `time_deriv_magneticFieldMatrix`, `hamiltonian_eq_electricField_vectorPotential`, `harmonicWaveX_div_electricField_eq_zero`, `electricField_eq`, `fieldStrengthMatrix_eq_electric_magnetic`, `curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix`, `gradKineticTerm_eq_electric_magnetic`, `div_electricField_eq_fieldStrengthMatrix`, `harmonicWaveX_electricField_succ`, `electricField_differentiable`, `time_deriv_time_deriv_magneticFieldMatrix`, `gradLagrangian_eq_electricField_magneticField`, `harmonicWaveX_electricField_zero`, `IsPlaneWave.electricField_space_deriv_eq_time_deriv`, `IsPlaneWave.space_deriv_electricField_eq_magneticFieldMatrix`, `IsPlaneWave.time_deriv_electricField_eq_magneticFieldMatrix`, `kineticTerm_eq_electric_magnetic`, `electricField_apply_contDiff_space`, `kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space`, `IsPlaneWave.electricFunction_eq_electricField`, `electricField_contDiff`, `IsPlaneWave.electricField_eq_electricFunction`, `time_deriv_comp_vectorPotential_eq_electricField`, `electricField_apply_differentiable_space`, `electricField_differentiable_time`, `IsPlaneWave.electricField_space_deriv`, `IsPlaneWave.space_deriv_magneticFieldMatrix_eq_electricField_mul_propogator`, `time_deriv_vectorPotential_eq_electricField`, `gradKineticTerm_eq_electric_magnetic_three`, `IsPlaneWave.electricField_time_deriv`, `electricField_apply_differentiable_time`, `electricField_eq_fieldStrengthMatrix`, `time_deriv_electricField_eq_fieldStrengthMatrix`, `electricField_apply_differentiable`, `electricField_apply_x_boost_zero`, `fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime`, `time_deriv_time_deriv_electricField_of_isExtrema`, `electricField_apply_contDiff_time`, `IsPlaneWave.electricField_eq_propogator_cross_magneticFieldMatrix`, `magneticFieldMatrix_apply_x_boost_zero_succ`, `IsPlaneWave.time_deriv_magneticFieldMatrix_eq_electricField_mul_propogator`, `lagrangian_eq_electric_magnetic`, `isExtrema_iff_gauss_ampere_magneticFieldMatrix`, `kineticTerm_eq_electricMatrix_magneticFieldMatrix`, `fieldStrengthMatrix_inl_inr_eq_electricField`, `electricField_apply_x_boost_succ`, `time_deriv_electricField_of_isExtrema`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div_electricField_eq_fieldStrengthMatrix` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Space.div` `electricField` `SpeedOfLight.val` `SpaceTime.deriv` `fieldStrengthMatrix` `Time` `Space` `Time.instSeminormedAddCommGroup` `Space.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `Lorentz.Vector.instModuleReal` `SpaceTime.toTimeAndSpace`	—	`fieldStrengthMatrix_diag_eq_zero` `SpaceTime.deriv_zero` `SpaceTime.deriv_sum_inr` `fieldStrengthMatrix_differentiable` `Space.div.eq_1` `electricField_eq_fieldStrengthMatrix` `fieldStrengthMatrix_antisymm` `Space.deriv_eq_fderiv_basis` `fieldStrengthMatrix_differentiable_space`
`electricField_apply_contDiff` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `electricField`	—	`electricField_contDiff`
`electricField_apply_contDiff_space` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `electricField`	—	`electricField_contDiff`
`electricField_apply_contDiff_time` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal` `electricField`	—	`electricField_contDiff`
`electricField_apply_differentiable` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Space` `Time.instAddCommGroup` `Space.instAddCommGroup` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `Space.instSeminormedAddCommGroup` `electricField`	—	`electricField_differentiable`
`electricField_apply_differentiable_space` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Space` `Space.instAddCommGroup` `Space.instModuleReal` `Space.instSeminormedAddCommGroup` `electricField`	—	`electricField_differentiable_space`
`electricField_apply_differentiable_time` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Time.instAddCommGroup` `Time.instModuleReal` `Time.instSeminormedAddCommGroup` `electricField`	—	`electricField_differentiable_time`
`electricField_contDiff` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `Electromagnetism.ElectricField` `electricField`	—	`electricField_eq_fieldStrengthMatrix` `fieldStrengthMatrix_contDiff`
`electricField_differentiable` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Space` `Time.instAddCommGroup` `Space.instAddCommGroup` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `Space.instSeminormedAddCommGroup` `Electromagnetism.ElectricField` `electricField`	—	`electricField_eq_fieldStrengthMatrix` `fieldStrengthMatrix_differentiable`
`electricField_differentiable_space` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Space` `Space.instAddCommGroup` `Space.instModuleReal` `Space.instSeminormedAddCommGroup` `electricField`	—	`electricField_differentiable`
`electricField_differentiable_time` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Time.instAddCommGroup` `Time.instModuleReal` `Time.instSeminormedAddCommGroup` `electricField`	—	`electricField_differentiable`
`electricField_eq` 📖	mathematical	—	`electricField` `Space.grad` `scalarPotential` `Time.deriv` `vectorPotential`	—	—
`electricField_eq_fieldStrengthMatrix` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`electricField` `SpeedOfLight.val` `fieldStrengthMatrix` `Time` `Space` `Time.instSeminormedAddCommGroup` `Space.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `SpaceTime.toTimeAndSpace`	—	`toFieldStrength_basis_repr_apply_eq_single` `minkowskiMatrix.inl_0_inl_0` `minkowskiMatrix.inr_i_inr_i` `electricField.eq_1` `Space.grad_apply` `SpaceTime.deriv_sum_inr` `differentiable_component` `Space.deriv_eq_fderiv_basis` `SpaceTime.deriv_eq` `Lorentz.Vector.fderiv_apply` `SpaceTime.deriv_sum_inl` `Time.deriv_eq` `vectorPotential.eq_1` `Time.fderiv_euclid` `Time.differentiable_euclid` `Lorentz.Vector.differentiable_apply`
`fieldStrengthMatrix_inl_inr_eq_electricField` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`fieldStrengthMatrix` `SpeedOfLight.val` `electricField` `Time` `Lorentz.Vector.instAddCommMonoid` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Time.instModuleReal` `SpaceTime.time` `Space` `Space.instSeminormedAddCommGroup` `Space.instAddCommMonoid` `Space.instModuleReal` `SpaceTime.space`	—	`electricField_eq_fieldStrengthMatrix` `SpaceTime.toTimeAndSpace_symm_apply_time_space`
`fieldStrengthMatrix_inr_inl_eq_electricField` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`fieldStrengthMatrix` `SpeedOfLight.val` `electricField` `Time` `Lorentz.Vector.instAddCommMonoid` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Time.instModuleReal` `SpaceTime.time` `Space` `Space.instSeminormedAddCommGroup` `Space.instAddCommMonoid` `Space.instModuleReal` `SpaceTime.space`	—	`electricField_eq_fieldStrengthMatrix` `SpaceTime.toTimeAndSpace_symm_apply_time_space` `fieldStrengthMatrix_antisymm`
`time_deriv_comp_vectorPotential_eq_electricField` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`Time.deriv` `vectorPotential` `electricField` `Space.deriv` `scalarPotential`	—	`Time.deriv_euclid` `vectorPotential_differentiable_time` `time_deriv_vectorPotential_eq_electricField`
`time_deriv_electricField_eq_fieldStrengthMatrix` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time.deriv` `electricField` `SpeedOfLight.val` `SpaceTime.deriv` `fieldStrengthMatrix` `Time` `Space` `Time.instSeminormedAddCommGroup` `Space.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `Lorentz.Vector.instModuleReal` `SpaceTime.toTimeAndSpace`	—	`SpaceTime.deriv_sum_inl` `fieldStrengthMatrix_differentiable` `Time.deriv_euclid` `electricField_differentiable_time` `electricField_eq_fieldStrengthMatrix` `Time.deriv_eq` `fieldStrengthMatrix_differentiable_time`
`time_deriv_vectorPotential_eq_electricField` 📖	mathematical	—	`Time.deriv` `vectorPotential` `electricField` `Space.grad` `scalarPotential`	—	`electricField.eq_1`

---

← Back to Index