Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `FreeSpace`, `c`, `ε₀`, `μ₀`	4
Theorems `c_abs`, `c_sq`, `c_val`, `ε₀_ne_zero`, `ε₀_nonneg`, `ε₀_pos`, `μ₀_ne_zero`, `μ₀_nonneg`, `μ₀_pos`	9
Total	13

Electromagnetism

Definitions

Name	Category	Theorems
`FreeSpace` 📖	CompData	—

Electromagnetism.FreeSpace

Definitions

Name	Category	Theorems
`c` 📖	CompOp	88 math math: `Electromagnetism.ElectromagneticPotential.harmonicWaveX_polarization_ellipse`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_space_deriv_same`, `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_eq_propogator_cross_electricField`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic'`, `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField`, `Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFunction_eq_magneticFieldMatrix`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_succ_time_deriv`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate`, `c_abs`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_vectorPotential`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_space_deriv_succ`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_space_deriv_succ`, `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_time_deriv`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_div_electricField_eq_zero`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ'`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_zero_succ`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_succ`, `Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_zero`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv_eq_time_deriv`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.space_deriv_electricField_eq_magneticFieldMatrix`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.time_deriv_electricField_eq_magneticFieldMatrix`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_space_deriv`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_eq_magneticFunction`, `Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_magneticFieldMatrix_of_isExtrema`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_succ_zero`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricFunction_eq_electricField`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_eq_electricFunction`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_scalarPotential_eq_zero`, `c_val`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_isExterma`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.space_deriv_magneticFieldMatrix_eq_electricField_mul_propogator`, `Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_time_deriv`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0`, `Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0`, `Electromagnetism.ElectromagneticPotential.constantEB_isExtrema`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ_space_deriv_zero`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_isExterma`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_succ_succ`, `Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_electricField_of_isExtrema`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_zero_eq_zero`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_eq_propogator_cross_magneticFieldMatrix`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_space_deriv_eq_time_deriv`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.time_deriv_magneticFieldMatrix_eq_electricField_mul_propogator`, `Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic`, `c_sq`, `Electromagnetism.ElectromagneticPotential.isExtrema_iff_gauss_ampere_magneticFieldMatrix`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_zero_succ_space_deriv_zero`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix`, `Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity`, `Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_isExterma`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix`, `Electromagnetism.ElectromagneticPotential.time_deriv_electricField_of_isExtrema`
`ε₀` 📖	CompOp	20 math math: `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic'`, `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time`, `ε₀_pos`, `Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField`, `Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_magneticFieldMatrix_of_isExtrema`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential`, `c_val`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential`, `Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_electricField_of_isExtrema`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField`, `Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic`, `c_sq`, `Electromagnetism.ElectromagneticPotential.isExtrema_iff_gauss_ampere_magneticFieldMatrix`, `ε₀_nonneg`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix`, `Electromagnetism.ElectromagneticPotential.time_deriv_electricField_of_isExtrema`
`μ₀` 📖	CompOp	50 math math: `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic'`, `Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum_potential`, `Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_sum_fieldStrengthMatrix`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField`, `μ₀_nonneg`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_sum_sum`, `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_fieldStrength`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_sum_sum`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_sum_fderiv`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time`, `Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate`, `Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic`, `Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq`, `μ₀_pos`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential`, `Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum_fieldStrengthMatrix_sq`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0`, `c_val`, `Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors`, `Electromagnetism.ElectromagneticPotential.isExtrema_iff_fieldStrengthMatrix`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum_fieldStrengthMatrix`, `Electromagnetism.ElectromagneticPotential.kineticTerm_add_time_mul_const`, `Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_electricField_of_isExtrema`, `Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic`, `c_sq`, `Electromagnetism.ElectromagneticPotential.isExtrema_iff_gauss_ampere_magneticFieldMatrix`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_fieldStrength`, `Electromagnetism.ElectromagneticPotential.time_deriv_electricField_of_isExtrema`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`c_abs` 📖	mathematical	—	`SpeedOfLight.val` `c`	—	`SpeedOfLight.val_pos`
`c_sq` 📖	mathematical	—	`SpeedOfLight.val` `c` `ε₀` `μ₀`	—	`c_val` `ε₀_nonneg` `μ₀_nonneg`
`c_val` 📖	mathematical	—	`SpeedOfLight.val` `c` `ε₀` `μ₀`	—	—
`ε₀_ne_zero` 📖	—	—	—	—	`ε₀_pos`
`ε₀_nonneg` 📖	mathematical	—	`ε₀`	—	`ε₀_pos`
`ε₀_pos` 📖	mathematical	—	`ε₀`	—	—
`μ₀_ne_zero` 📖	—	—	—	—	`μ₀_pos`
`μ₀_nonneg` 📖	mathematical	—	`μ₀`	—	`μ₀_pos`
`μ₀_pos` 📖	mathematical	—	`μ₀`	—	—

---

← Back to Index