Documentation Verification Report

IsPlaneWave

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

Statistics

MetricCount
DefinitionsIsPlaneWave, electricFunction, magneticFunction
3
TheoremselectricField_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
Total23

Electromagnetism.ElectromagneticPotential

Definitions

NameCategoryTheorems
IsPlaneWave 📖MathDef
1 mathmath: harmonicWaveX_isPlaneWave

Electromagnetism.ElectromagneticPotential.IsPlaneWave

Definitions

NameCategoryTheorems
electricFunction 📖CompOp
6 mathmath: electricFunction_eq_electricField, electricField_eq_electricFunction, electricFunction_unique, electricFunction_differentiable, electricField_space_deriv, electricField_time_deriv
magneticFunction 📖CompOp
6 mathmath: magneticFunction_eq_magneticFieldMatrix, magneticFieldMatrix_time_deriv, magneticFunction_unique, magneticFieldMatrix_space_deriv, magneticFieldMatrix_eq_magneticFunction, magneticFunction_differentiable

Theorems

NameKindAssumesProvesValidatesDepends On
electricField_eq_electricFunction 📖mathematicalElectromagnetism.ElectromagneticPotential.IsPlaneWaveElectromagnetism.ElectromagneticPotential.electricField
Electromagnetism.FreeSpace.c
electricFunction
Space
Space.instInnerReal
Space.Direction.unit
SpeedOfLight.val
Time.val
electricField_eq_propogator_cross_magneticFieldMatrix 📖mathematicalElectromagnetism.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 📖mathematicalElectromagnetism.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 📖mathematicalElectromagnetism.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 📖mathematicalElectromagnetism.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 📖mathematicalElectromagnetism.ElectromagneticPotential.IsPlaneWave
SpaceTime
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector
electricFunctionelectricFunction_eq_electricField
Electromagnetism.ElectromagneticPotential.electricField_differentiable
electricFunction_eq_electricField 📖mathematicalElectromagnetism.ElectromagneticPotential.IsPlaneWaveelectricFunction
Electromagnetism.ElectromagneticPotential.electricField
Electromagnetism.FreeSpace.c
SpeedOfLight.val
Space
Space.instZero
electricField_eq_electricFunction
electricFunction_unique 📖mathematicalElectromagnetism.ElectromagneticPotential.IsPlaneWave
Electromagnetism.ElectromagneticPotential.electricField
Electromagnetism.FreeSpace.c
ClassicalMechanics.planeWave
SpeedOfLight.val
electricFunctionelectricField_eq_electricFunction
magneticFieldMatrix_eq_magneticFunction 📖mathematicalElectromagnetism.ElectromagneticPotential.IsPlaneWaveElectromagnetism.ElectromagneticPotential.magneticFieldMatrix
Electromagnetism.FreeSpace.c
magneticFunction
Space
Space.instInnerReal
Space.Direction.unit
SpeedOfLight.val
Time.val
magneticFieldMatrix_eq_propogator_cross_electricField 📖mathematicalElectromagnetism.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 📖mathematicalElectromagnetism.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 📖mathematicalElectromagnetism.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 📖mathematicalElectromagnetism.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 📖mathematicalElectromagnetism.ElectromagneticPotential.IsPlaneWave
SpaceTime
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector
magneticFunctionmagneticFunction_eq_magneticFieldMatrix
Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable
magneticFunction_eq_magneticFieldMatrix 📖mathematicalElectromagnetism.ElectromagneticPotential.IsPlaneWavemagneticFunction
Electromagnetism.ElectromagneticPotential.magneticFieldMatrix
Electromagnetism.FreeSpace.c
SpeedOfLight.val
Space
Space.instZero
magneticFieldMatrix_eq_magneticFunction
magneticFunction_unique 📖mathematicalElectromagnetism.ElectromagneticPotential.IsPlaneWave
Electromagnetism.ElectromagneticPotential.magneticFieldMatrix
Electromagnetism.FreeSpace.c
Space
Space.instInnerReal
Space.Direction.unit
SpeedOfLight.val
Time.val
magneticFunctionmagneticFieldMatrix_eq_magneticFunction
space_deriv_electricField_eq_magneticFieldMatrix 📖mathematicalElectromagnetism.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 📖mathematicalElectromagnetism.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 📖mathematicalElectromagnetism.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 📖mathematicalElectromagnetism.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