HarmonicWave

📁 Source: PhysLean/Electromagnetism/Vacuum/HarmonicWave.lean

Statistics

Metric	Count
Definitions harmonicWaveX	1
Theorems harmonicWaveX_contDiff, harmonicWaveX_differentiable, harmonicWaveX_div_electricField_eq_zero, harmonicWaveX_electricField_space_deriv_same, harmonicWaveX_electricField_succ, harmonicWaveX_electricField_succ_time_deriv, harmonicWaveX_electricField_zero, harmonicWaveX_isExtrema, harmonicWaveX_isPlaneWave, harmonicWaveX_magneticFieldMatrix_space_deriv_succ, harmonicWaveX_magneticFieldMatrix_succ_succ, harmonicWaveX_magneticFieldMatrix_succ_zero, harmonicWaveX_magneticFieldMatrix_zero_succ, harmonicWaveX_magneticFieldMatrix_zero_succ_space_deriv_zero, harmonicWaveX_polarization_ellipse, harmonicWaveX_scalarPotential_eq_zero, harmonicWaveX_vectorPotential_space_deriv_succ, harmonicWaveX_vectorPotential_succ, harmonicWaveX_vectorPotential_succ', harmonicWaveX_vectorPotential_succ_space_deriv_zero, harmonicWaveX_vectorPotential_zero_eq_zero	21
Total	22

Electromagnetism.ElectromagneticPotential

Definitions

Name	Category	Theorems
harmonicWaveX 📖	CompOp	21 math math: harmonicWaveX_polarization_ellipse, harmonicWaveX_electricField_space_deriv_same, harmonicWaveX_electricField_succ_time_deriv, harmonicWaveX_magneticFieldMatrix_space_deriv_succ, harmonicWaveX_vectorPotential_space_deriv_succ, harmonicWaveX_div_electricField_eq_zero, harmonicWaveX_differentiable, harmonicWaveX_vectorPotential_succ, harmonicWaveX_vectorPotential_succ', harmonicWaveX_magneticFieldMatrix_zero_succ, harmonicWaveX_electricField_succ, harmonicWaveX_electricField_zero, harmonicWaveX_isPlaneWave, harmonicWaveX_magneticFieldMatrix_succ_zero, harmonicWaveX_scalarPotential_eq_zero, harmonicWaveX_contDiff, harmonicWaveX_vectorPotential_succ_space_deriv_zero, harmonicWaveX_magneticFieldMatrix_succ_succ, harmonicWaveX_vectorPotential_zero_eq_zero, harmonicWaveX_isExtrema, harmonicWaveX_magneticFieldMatrix_zero_succ_space_deriv_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
harmonicWaveX_contDiff 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector harmonicWaveX	—	Lorentz.Vector.contDiff_apply SpaceTime.time_val_toCoord_symm Lorentz.Vector.coord_contDiff
harmonicWaveX_differentiable 📖	mathematical	—	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector harmonicWaveX	—	Lorentz.Vector.differentiable_apply SpaceTime.time_val_toCoord_symm Lorentz.Vector.coord_differentiable
harmonicWaveX_div_electricField_eq_zero 📖	mathematical	—	Space.div electricField Electromagnetism.FreeSpace.c harmonicWaveX	—	harmonicWaveX_electricField_space_deriv_same
harmonicWaveX_electricField_space_deriv_same 📖	mathematical	—	Space.deriv electricField Electromagnetism.FreeSpace.c harmonicWaveX	—	harmonicWaveX_electricField_zero Space.deriv_const harmonicWaveX_electricField_succ Space.deriv_eq Space.eval_differentiable Space.deriv_component
harmonicWaveX_electricField_succ 📖	mathematical	—	electricField Electromagnetism.FreeSpace.c harmonicWaveX SpeedOfLight.val Time.val Space.val	—	harmonicWaveX_scalarPotential_eq_zero Space.grad_zero Time.deriv_euclid vectorPotential_differentiable_time harmonicWaveX_differentiable harmonicWaveX_vectorPotential_succ Time.deriv_eq Time.val_differentiable Time.fderiv_val
harmonicWaveX_electricField_succ_time_deriv 📖	mathematical	—	Time.deriv electricField Electromagnetism.FreeSpace.c harmonicWaveX SpeedOfLight.val Time.val Space.val	—	harmonicWaveX_electricField_succ Time.deriv_eq Time.val_differentiable Time.fderiv_val
harmonicWaveX_electricField_zero 📖	mathematical	—	electricField Electromagnetism.FreeSpace.c harmonicWaveX	—	harmonicWaveX_scalarPotential_eq_zero Space.grad_zero Time.deriv_euclid vectorPotential_differentiable_time harmonicWaveX_differentiable harmonicWaveX_vectorPotential_zero_eq_zero Time.deriv_const
harmonicWaveX_isExtrema 📖	mathematical	—	IsExtrema harmonicWaveX Electromagnetism.LorentzCurrentDensity SpaceTime Lorentz.Vector Lorentz.Vector.instAddCommGroup	—	isExtrema_iff_gauss_ampere_magneticFieldMatrix harmonicWaveX_contDiff Electromagnetism.LorentzCurrentDensity.chargeDensity_zero harmonicWaveX_div_electricField_eq_zero harmonicWaveX_magneticFieldMatrix_space_deriv_succ Electromagnetism.LorentzCurrentDensity.currentDensity_zero magneticFieldMatrix_diag_eq_zero Space.deriv_const Time.deriv_euclid electricField_differentiable_time harmonicWaveX_electricField_zero Time.deriv_const harmonicWaveX_magneticFieldMatrix_zero_succ_space_deriv_zero harmonicWaveX_electricField_succ_time_deriv Electromagnetism.FreeSpace.c_sq
harmonicWaveX_isPlaneWave 📖	mathematical	—	IsPlaneWave harmonicWaveX Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.basis	—	harmonicWaveX_electricField_zero Space.inner_basis harmonicWaveX_electricField_succ magneticFieldMatrix_diag_eq_zero harmonicWaveX_magneticFieldMatrix_zero_succ harmonicWaveX_magneticFieldMatrix_succ_zero harmonicWaveX_magneticFieldMatrix_succ_succ
harmonicWaveX_magneticFieldMatrix_space_deriv_succ 📖	mathematical	—	Space.deriv magneticFieldMatrix Electromagnetism.FreeSpace.c harmonicWaveX	—	magneticFieldMatrix_diag_eq_zero Space.deriv_const harmonicWaveX_magneticFieldMatrix_succ_succ harmonicWaveX_magneticFieldMatrix_zero_succ Space.deriv_eq Space.eval_differentiable Space.deriv_component harmonicWaveX_magneticFieldMatrix_succ_zero
harmonicWaveX_magneticFieldMatrix_succ_succ 📖	mathematical	—	magneticFieldMatrix Electromagnetism.FreeSpace.c harmonicWaveX	—	magneticFieldMatrix_eq_vectorPotential harmonicWaveX_differentiable harmonicWaveX_vectorPotential_space_deriv_succ
harmonicWaveX_magneticFieldMatrix_succ_zero 📖	mathematical	—	magneticFieldMatrix Electromagnetism.FreeSpace.c harmonicWaveX SpeedOfLight.val Time.val Space.val	—	magneticFieldMatrix_eq_vectorPotential harmonicWaveX_differentiable harmonicWaveX_vectorPotential_zero_eq_zero Space.deriv_const harmonicWaveX_vectorPotential_succ_space_deriv_zero
harmonicWaveX_magneticFieldMatrix_zero_succ 📖	mathematical	—	magneticFieldMatrix Electromagnetism.FreeSpace.c harmonicWaveX SpeedOfLight.val Time.val Space.val	—	magneticFieldMatrix_eq_vectorPotential harmonicWaveX_differentiable harmonicWaveX_vectorPotential_zero_eq_zero Space.deriv_const harmonicWaveX_vectorPotential_succ_space_deriv_zero
harmonicWaveX_magneticFieldMatrix_zero_succ_space_deriv_zero 📖	mathematical	—	Space.deriv magneticFieldMatrix Electromagnetism.FreeSpace.c harmonicWaveX SpeedOfLight.val Time.val Space.val	—	harmonicWaveX_magneticFieldMatrix_zero_succ Space.deriv_eq Space.eval_differentiable Space.deriv_component
harmonicWaveX_polarization_ellipse 📖	mathematical	—	electricField Electromagnetism.FreeSpace.c harmonicWaveX	—	harmonicWaveX_electricField_succ
harmonicWaveX_scalarPotential_eq_zero 📖	mathematical	—	scalarPotential Electromagnetism.FreeSpace.c harmonicWaveX Time Space	—	—
harmonicWaveX_vectorPotential_space_deriv_succ 📖	mathematical	—	Space.deriv vectorPotential Electromagnetism.FreeSpace.c harmonicWaveX	—	harmonicWaveX_vectorPotential_zero_eq_zero Space.deriv_const harmonicWaveX_vectorPotential_succ' Space.deriv_eq Space.eval_differentiable Space.deriv_component
harmonicWaveX_vectorPotential_succ 📖	mathematical	—	vectorPotential Electromagnetism.FreeSpace.c harmonicWaveX SpeedOfLight.val Time.val Space.val	—	SpaceTime.time_val_toCoord_symm SpaceTime.toTimeAndSpace_symm_apply_inl SpaceTime.space_toTimeAndSpace_symm
harmonicWaveX_vectorPotential_succ' 📖	mathematical	—	vectorPotential Electromagnetism.FreeSpace.c harmonicWaveX SpeedOfLight.val Time.val Space.val	—	SpaceTime.time_val_toCoord_symm SpaceTime.toTimeAndSpace_symm_apply_inl SpaceTime.space_toTimeAndSpace_symm
harmonicWaveX_vectorPotential_succ_space_deriv_zero 📖	mathematical	—	Space.deriv vectorPotential Electromagnetism.FreeSpace.c harmonicWaveX SpeedOfLight.val Time.val Space.val	—	harmonicWaveX_vectorPotential_succ Space.deriv_eq_fderiv_basis Space.eval_differentiable Space.deriv_component
harmonicWaveX_vectorPotential_zero_eq_zero 📖	mathematical	—	vectorPotential Electromagnetism.FreeSpace.c harmonicWaveX	—	SpaceTime.time_val_toCoord_symm SpaceTime.toTimeAndSpace_symm_apply_inl SpaceTime.space_toTimeAndSpace_symm

---

← Back to Index