IsPlaneWave

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

Statistics

Metric	Count
Definitions IsPlaneWave, electricFunction, magneticFunction	3
Theorems electricField_eq_electricFunction, electricField_eq_propogator_cross_magneticFieldMatrix, electricField_space_deriv, electricField_space_deriv_eq_time_deriv, electricField_time_deriv, electricFunction_differentiable, electricFunction_eq_electricField, electricFunction_unique, magneticFieldMatrix_eq_magneticFunction, magneticFieldMatrix_eq_propogator_cross_electricField, magneticFieldMatrix_space_deriv, magneticFieldMatrix_space_deriv_eq_time_deriv, magneticFieldMatrix_time_deriv, magneticFunction_differentiable, magneticFunction_eq_magneticFieldMatrix, magneticFunction_unique, space_deriv_electricField_eq_magneticFieldMatrix, space_deriv_magneticFieldMatrix_eq_electricField_mul_propogator, time_deriv_electricField_eq_magneticFieldMatrix, time_deriv_magneticFieldMatrix_eq_electricField_mul_propogator	20
Total	23

Electromagnetism.ElectromagneticPotential

Definitions

Name	Category	Theorems
IsPlaneWave 📖	MathDef	1 math math: harmonicWaveX_isPlaneWave

Electromagnetism.ElectromagneticPotential.IsPlaneWave

Definitions

Name	Category	Theorems
electricFunction 📖	CompOp	6 math math: electricFunction_eq_electricField, electricField_eq_electricFunction, electricFunction_unique, electricFunction_differentiable, electricField_space_deriv, electricField_time_deriv
magneticFunction 📖	CompOp	6 math math: magneticFunction_eq_magneticFieldMatrix, magneticFieldMatrix_time_deriv, magneticFunction_unique, magneticFieldMatrix_space_deriv, magneticFieldMatrix_eq_magneticFunction, magneticFunction_differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
electricField_eq_electricFunction 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave	Electromagnetism.ElectromagneticPotential.electricField Electromagnetism.FreeSpace.c electricFunction Space Space.instInnerReal Space.Direction.unit SpeedOfLight.val Time.val	—	—
electricField_eq_propogator_cross_magneticFieldMatrix 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Electromagnetism.ElectromagneticPotential.IsExtrema Electromagnetism.LorentzCurrentDensity Lorentz.Vector.instAddCommGroup	Electromagnetism.ElectromagneticPotential.electricField Electromagnetism.FreeSpace.c SpeedOfLight.val Electromagnetism.ElectromagneticPotential.magneticFieldMatrix Space.val Space.Direction.unit	—	Space.equal_up_to_const_of_deriv_eq Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable time_deriv_electricField_eq_magneticFieldMatrix space_deriv_electricField_eq_magneticFieldMatrix
electricField_space_deriv 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	Space.deriv Electromagnetism.ElectromagneticPotential.electricField Electromagnetism.FreeSpace.c Space.val Space.Direction.unit electricFunction Space Space.instInnerReal SpeedOfLight.val Time.val	—	electricField_eq_electricFunction Space.deriv_eq_fderiv_basis electricFunction_differentiable Space.inner_apply_differentiableAt Space.deriv_inner_left
electricField_space_deriv_eq_time_deriv 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	Space.deriv Electromagnetism.ElectromagneticPotential.electricField Electromagnetism.FreeSpace.c Space.val Space.Direction.unit SpeedOfLight.val Time.deriv	—	Space.deriv_euclid Electromagnetism.ElectromagneticPotential.electricField_differentiable_space electricField_space_deriv Time.deriv_euclid Electromagnetism.ElectromagneticPotential.electricField_differentiable_time electricField_time_deriv
electricField_time_deriv 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	Time.deriv Electromagnetism.ElectromagneticPotential.electricField Electromagnetism.FreeSpace.c SpeedOfLight.val electricFunction Space Space.instInnerReal Space.Direction.unit Time.val	—	electricField_eq_electricFunction Time.deriv_eq electricFunction_differentiable Time.val_differentiable Time.fderiv_val
electricFunction_differentiable 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	electricFunction	—	electricFunction_eq_electricField Electromagnetism.ElectromagneticPotential.electricField_differentiable
electricFunction_eq_electricField 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave	electricFunction Electromagnetism.ElectromagneticPotential.electricField Electromagnetism.FreeSpace.c SpeedOfLight.val Space Space.instZero	—	electricField_eq_electricFunction
electricFunction_unique 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave Electromagnetism.ElectromagneticPotential.electricField Electromagnetism.FreeSpace.c ClassicalMechanics.planeWave SpeedOfLight.val	electricFunction	—	electricField_eq_electricFunction
magneticFieldMatrix_eq_magneticFunction 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave	Electromagnetism.ElectromagneticPotential.magneticFieldMatrix Electromagnetism.FreeSpace.c magneticFunction Space Space.instInnerReal Space.Direction.unit SpeedOfLight.val Time.val	—	—
magneticFieldMatrix_eq_propogator_cross_electricField 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	Electromagnetism.ElectromagneticPotential.magneticFieldMatrix Electromagnetism.FreeSpace.c SpeedOfLight.val Space.val Space.Direction.unit Electromagnetism.ElectromagneticPotential.electricField	—	Space.equal_up_to_const_of_deriv_eq Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable time_deriv_magneticFieldMatrix_eq_electricField_mul_propogator space_deriv_magneticFieldMatrix_eq_electricField_mul_propogator
magneticFieldMatrix_space_deriv 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	Space.deriv Electromagnetism.ElectromagneticPotential.magneticFieldMatrix Electromagnetism.FreeSpace.c Space.val Space.Direction.unit magneticFunction Space Space.instInnerReal SpeedOfLight.val Time.val	—	magneticFieldMatrix_eq_magneticFunction Space.deriv_eq_fderiv_basis magneticFunction_differentiable Space.inner_apply_differentiableAt Space.deriv_inner_left
magneticFieldMatrix_space_deriv_eq_time_deriv 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	Space.deriv Electromagnetism.ElectromagneticPotential.magneticFieldMatrix Electromagnetism.FreeSpace.c Space.val Space.Direction.unit SpeedOfLight.val Time.deriv	—	magneticFieldMatrix_space_deriv magneticFieldMatrix_time_deriv
magneticFieldMatrix_time_deriv 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	Time.deriv Electromagnetism.ElectromagneticPotential.magneticFieldMatrix Electromagnetism.FreeSpace.c SpeedOfLight.val magneticFunction Space Space.instInnerReal Space.Direction.unit Time.val	—	magneticFieldMatrix_eq_magneticFunction Time.deriv_eq magneticFunction_differentiable Time.val_differentiable Time.fderiv_val
magneticFunction_differentiable 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	magneticFunction	—	magneticFunction_eq_magneticFieldMatrix Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable
magneticFunction_eq_magneticFieldMatrix 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave	magneticFunction Electromagnetism.ElectromagneticPotential.magneticFieldMatrix Electromagnetism.FreeSpace.c SpeedOfLight.val Space Space.instZero	—	magneticFieldMatrix_eq_magneticFunction
magneticFunction_unique 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave Electromagnetism.ElectromagneticPotential.magneticFieldMatrix Electromagnetism.FreeSpace.c Space Space.instInnerReal Space.Direction.unit SpeedOfLight.val Time.val	magneticFunction	—	magneticFieldMatrix_eq_magneticFunction
space_deriv_electricField_eq_magneticFieldMatrix 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Electromagnetism.ElectromagneticPotential.IsExtrema Electromagnetism.LorentzCurrentDensity Lorentz.Vector.instAddCommGroup	Space.deriv Electromagnetism.ElectromagneticPotential.electricField Electromagnetism.FreeSpace.c SpeedOfLight.val Electromagnetism.ElectromagneticPotential.magneticFieldMatrix Space.val Space.Direction.unit	—	electricField_space_deriv_eq_time_deriv time_deriv_electricField_eq_magneticFieldMatrix Time.deriv_eq Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_time Space.deriv_eq_fderiv_basis Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_space magneticFieldMatrix_space_deriv_eq_time_deriv
space_deriv_magneticFieldMatrix_eq_electricField_mul_propogator 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	Space.deriv Electromagnetism.ElectromagneticPotential.magneticFieldMatrix Electromagnetism.FreeSpace.c Space.val Space.Direction.unit SpeedOfLight.val Electromagnetism.ElectromagneticPotential.electricField	—	magneticFieldMatrix_space_deriv_eq_time_deriv time_deriv_magneticFieldMatrix_eq_electricField_mul_propogator Space.deriv_eq_fderiv_basis Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable_space Time.deriv_eq Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable_time electricField_space_deriv_eq_time_deriv
time_deriv_electricField_eq_magneticFieldMatrix 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Electromagnetism.ElectromagneticPotential.IsExtrema Electromagnetism.LorentzCurrentDensity Lorentz.Vector.instAddCommGroup	Time.deriv Electromagnetism.ElectromagneticPotential.electricField Electromagnetism.FreeSpace.c SpeedOfLight.val Electromagnetism.ElectromagneticPotential.magneticFieldMatrix Space.val Space.Direction.unit	—	Time.deriv_euclid Electromagnetism.ElectromagneticPotential.electricField_differentiable_time Electromagnetism.ElectromagneticPotential.time_deriv_electricField_of_isExtrema Electromagnetism.LorentzCurrentDensity.currentDensity_zero magneticFieldMatrix_space_deriv_eq_time_deriv Time.deriv_eq Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable_time Electromagnetism.FreeSpace.c_sq Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_antisymm
time_deriv_magneticFieldMatrix_eq_electricField_mul_propogator 📖	mathematical	Electromagnetism.ElectromagneticPotential.IsPlaneWave SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	Time.deriv Electromagnetism.ElectromagneticPotential.magneticFieldMatrix Electromagnetism.FreeSpace.c Space.val Space.Direction.unit SpeedOfLight.val Electromagnetism.ElectromagneticPotential.electricField	—	Electromagnetism.ElectromagneticPotential.time_deriv_magneticFieldMatrix electricField_space_deriv_eq_time_deriv Time.deriv_eq Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable_time

---

← Back to Index