Documentation Verification Report

IsExtrema

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

Statistics

MetricCount
DefinitionsIsExtrema, IsExtrema
2
TheoremsisExterma_equivariant, isExterma_iff_tensor, isExtrema_iff_components, isExtrema_iff_gradLagrangian, isExtrema_iff_space_time, isExtrema_iff_vectorPotential, isExtrema_iff_fieldStrengthMatrix, isExtrema_iff_gauss_ampere_magneticFieldMatrix, isExtrema_iff_gradLagrangian, isExtrema_iff_tensors, isExtrema_lorentzGroup_apply_iff, time_deriv_electricField_of_isExtrema, time_deriv_time_deriv_electricField_of_isExtrema, time_deriv_time_deriv_magneticFieldMatrix_of_isExtrema
14
Total16

Electromagnetism.DistElectromagneticPotential

Definitions

NameCategoryTheorems
IsExtrema 📖MathDef
9 mathmath: isExtrema_iff_gradLagrangian, isExtrema_iff_space_time, isExterma_iff_tensor, isExtrema_iff_vectorPotential, isExterma_equivariant, infiniteWire_isExterma, oneDimPointParticle_isExterma, isExtrema_iff_components, threeDimPointParticle_isExterma

Theorems

NameKindAssumesProvesValidatesDepends On
isExterma_equivariant 📖mathematicalIsExtrema
LorentzGroup
Electromagnetism.DistElectromagneticPotential
SpaceTime.instSMulElemMatrixSumFinOfNatNatRealLorentzGroupDistribution
realLorentzTensor.Color
realLorentzTensor.Color.up
Lorentz.Vector
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector.tensorial
Electromagnetism.DistLorentzCurrentDensity
TensorSpecies.Tensor.contrT_decide
Lorentz.Vector.instFiniteDimensionalReal
TensorSpecies.Tensor.PermCond.auto
isExterma_iff_tensor
fieldStrength_equivariant
SpaceTime.distTensorDeriv_equivariant
SpaceTime.lorentzGroup_smul_dist_apply
TensorSpecies.Tensorial.instSMulCommClass
TensorSpecies.Tensorial.toTensor_smul
TensorSpecies.Tensor.actionT_smul
TensorSpecies.Tensor.contrT_equivariant
TensorSpecies.Tensor.permT_equivariant
TensorSpecies.Tensor.actionT_neg
TensorSpecies.Tensor.actionT_add
SpaceTime.schwartzAction_mul_apply
isExterma_iff_tensor 📖mathematicalIsExtrema
TensorSpecies.Tensor
realLorentzTensor.Color
LorentzGroup
lorentzGroupIsGroup
realLorentzTensor
realLorentzTensor.Color.down
realLorentzTensor.Color.up
TensorSpecies.Tensor.Pure.dropPairEmb
IndexNotation.OverColor
IndexNotation.instGroupoidOverColor
TensorSpecies.F
TensorSpecies.Tensor.contrT
TensorSpecies.Tensor.contrT_decide
TensorSpecies.τ
Lorentz.CoVector
Lorentz.Vector
Lorentz.Vector.instAddCommMonoid
Lorentz.Vector.instModuleReal
Lorentz.CoVector.instAddCommMonoid
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.innerProductSpace
Lorentz.CoVector.instModuleReal
TensorSpecies.Tensorial.toTensor
TensorSpecies.Tensorial.prod
Lorentz.CoVector.tensorial
Lorentz.Vector.tensorial
Electromagnetism.FreeSpace.μ₀
Distribution
SpaceTime
Lorentz.CoVector.isNormedAddCommGroup
Lorentz.CoVector.innerProductSpace
Lorentz.Vector.isNormedSpace
SpaceTime.distTensorDeriv
Lorentz.Vector.instFiniteDimensionalReal
Electromagnetism.DistElectromagneticPotential
Lorentz.Vector.instAddCommGroup
fieldStrength
TensorSpecies.Tensor.permT
TensorSpecies.Tensor.PermCond.auto
TensorSpecies.Tensor.PermCond
realLorentzTensor.instDecidableEqColor
Electromagnetism.DistLorentzCurrentDensity
TensorSpecies.Tensor.contrT_decide
Lorentz.Vector.instFiniteDimensionalReal
TensorSpecies.Tensor.PermCond.auto
minkowskiMatrix.η_diag_ne_zero
TensorSpecies.Tensor.PermCond.comp
TensorSpecies.Tensor.permT_permT
TensorSpecies.Tensor.permT.congr_simp
gradLagrangian_eq_tensor
TensorSpecies.Tensor.permT_eq_zero_iff
isExtrema_iff_components 📖mathematicalIsExtrema
Distribution
SpaceTime
Lorentz.Vector
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
gradLagrangian
isExtrema_iff_gradLagrangian
isExtrema_iff_gradLagrangian 📖mathematicalIsExtrema
gradLagrangian
Distribution
SpaceTime
Lorentz.Vector
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
isExtrema_iff_space_time 📖mathematicalIsExtrema
Distribution
Time
Space
Time.instNormedAddCommGroup
Space.instNormedAddCommGroup
Time.instNormedSpaceReal
Space.instInnerProductSpaceReal
Space.distSpaceDiv
Electromagnetism.DistElectromagneticPotential
SpaceTime
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector
Lorentz.Vector.instModuleReal
Lorentz.Vector.instAddCommMonoid
Lorentz.Vector.instAddCommGroup
electricField
Electromagnetism.FreeSpace.c
Electromagnetism.FreeSpace.ε₀
Electromagnetism.DistLorentzCurrentDensity
Electromagnetism.DistLorentzCurrentDensity.chargeDensity
Electromagnetism.FreeSpace.μ₀
Space.distTimeDeriv
Space.distSpaceDeriv
magneticFieldMatrix
Electromagnetism.DistLorentzCurrentDensity.currentDensity
isExtrema_iff_components
gradLagrangian_sum_inl_0
Electromagnetism.FreeSpace.c_sq
SpaceTime.distTimeSlice_symm_apply
gradLagrangian_sum_inr_i
isExtrema_iff_vectorPotential 📖mathematicalIsExtrema
Distribution
Time
Space
Time.instNormedAddCommGroup
Space.instNormedAddCommGroup
Time.instNormedSpaceReal
Space.instInnerProductSpaceReal
Space.distSpaceDiv
Electromagnetism.DistElectromagneticPotential
SpaceTime
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector
Lorentz.Vector.instModuleReal
Lorentz.Vector.instAddCommMonoid
Lorentz.Vector.instAddCommGroup
electricField
Electromagnetism.FreeSpace.c
Electromagnetism.FreeSpace.ε₀
Electromagnetism.DistLorentzCurrentDensity
Electromagnetism.DistLorentzCurrentDensity.chargeDensity
Electromagnetism.FreeSpace.μ₀
Space.distTimeDeriv
Space.distSpaceDeriv
vectorPotential
Electromagnetism.DistLorentzCurrentDensity.currentDensity
isExtrema_iff_space_time
magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential

Electromagnetism.ElectromagneticPotential

Definitions

NameCategoryTheorems
IsExtrema 📖MathDef
7 mathmath: isExtrema_lorentzGroup_apply_iff, isExtrema_iff_gradLagrangian, isExtrema_iff_tensors, isExtrema_iff_fieldStrengthMatrix, constantEB_isExtrema, harmonicWaveX_isExtrema, isExtrema_iff_gauss_ampere_magneticFieldMatrix

Theorems

NameKindAssumesProvesValidatesDepends On
isExtrema_iff_fieldStrengthMatrix 📖mathematicalSpaceTime
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector
IsExtrema
SpaceTime.deriv
fieldStrengthMatrix
Electromagnetism.FreeSpace.μ₀
isExtrema_iff_gradLagrangian
gradLagrangian_eq_sum_fieldStrengthMatrix
Lorentz.Vector.sum_basis_eq_zero_iff
minkowskiMatrix.η_diag_ne_zero
isExtrema_iff_gauss_ampere_magneticFieldMatrix 📖mathematicalSpaceTime
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector
IsExtrema
Space.div
electricField
Electromagnetism.FreeSpace.c
Electromagnetism.LorentzCurrentDensity.chargeDensity
Electromagnetism.FreeSpace.ε₀
Electromagnetism.FreeSpace.μ₀
Time.deriv
Space.deriv
magneticFieldMatrix
Electromagnetism.LorentzCurrentDensity.currentDensity
isExtrema_iff_gradLagrangian
gradLagrangian_eq_electricField_magneticField
Lorentz.Vector.sum_inl_inr_basis_eq_zero_iff
SpaceTime.time_toTimeAndSpace_symm
SpaceTime.space_toTimeAndSpace_symm
Electromagnetism.FreeSpace.c_sq
isExtrema_iff_gradLagrangian 📖mathematicalIsExtrema
gradLagrangian
SpaceTime
Lorentz.Vector
Lorentz.Vector.instAddCommGroup
isExtrema_iff_tensors 📖mathematicalSpaceTime
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector
IsExtrema
TensorSpecies.Tensor
realLorentzTensor.Color
LorentzGroup
lorentzGroupIsGroup
realLorentzTensor
realLorentzTensor.Color.down
realLorentzTensor.Color.up
TensorSpecies.Tensor.Pure.dropPairEmb
IndexNotation.OverColor
IndexNotation.instGroupoidOverColor
TensorSpecies.F
TensorSpecies.Tensor.contrT
TensorSpecies.Tensor.contrT_decide
TensorSpecies.τ
Lorentz.CoVector
Lorentz.Vector.instAddCommMonoid
Lorentz.Vector.instModuleReal
Lorentz.CoVector.instAddCommMonoid
Lorentz.Vector.innerProductSpace
Lorentz.CoVector.instModuleReal
TensorSpecies.Tensorial.toTensor
TensorSpecies.Tensorial.prod
Lorentz.CoVector.tensorial
Lorentz.Vector.tensorial
Electromagnetism.FreeSpace.μ₀
SpaceTime.tensorDeriv
toFieldStrength
TensorSpecies.Tensor.permT
TensorSpecies.Tensor.PermCond.auto
TensorSpecies.Tensor.PermCond
realLorentzTensor.instDecidableEqColor
TensorSpecies.Tensor.contrT_decide
TensorSpecies.Tensor.PermCond.auto
minkowskiMatrix.η_diag_ne_zero
TensorSpecies.Tensor.PermCond.comp
TensorSpecies.Tensor.permT_permT
TensorSpecies.Tensor.permT.congr_simp
gradLagrangian_eq_tensor
TensorSpecies.Tensor.permT_eq_zero_iff
isExtrema_lorentzGroup_apply_iff 📖mathematicalSpaceTime
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector
IsExtrema
LorentzGroup
TensorSpecies.Tensorial.smulAction
realLorentzTensor.Color
lorentzGroupIsGroup
realLorentzTensor
realLorentzTensor.Color.up
Lorentz.Vector.instAddCommMonoid
Lorentz.Vector.instModuleReal
Lorentz.Vector.tensorial
TensorSpecies.Tensor.contrT_decide
TensorSpecies.Tensor.PermCond.auto
isExtrema_iff_tensors
toFieldStrength_equivariant
SpaceTime.tensorDeriv_equivariant
toFieldStrength_differentiable
TensorSpecies.Tensorial.instSMulCommClass
TensorSpecies.Tensorial.toTensor_smul
TensorSpecies.Tensor.actionT_smul
TensorSpecies.Tensor.contrT_equivariant
TensorSpecies.Tensor.permT_equivariant
TensorSpecies.Tensor.actionT_neg
TensorSpecies.Tensor.actionT_add
time_deriv_electricField_of_isExtrema 📖mathematicalSpaceTime
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector
IsExtrema
Time.deriv
electricField
Electromagnetism.FreeSpace.c
Electromagnetism.FreeSpace.μ₀
Electromagnetism.FreeSpace.ε₀
Space.deriv
magneticFieldMatrix
Electromagnetism.LorentzCurrentDensity.currentDensity
isExtrema_iff_gauss_ampere_magneticFieldMatrix
time_deriv_time_deriv_electricField_of_isExtrema 📖mathematicalSpaceTime
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector
IsExtrema
Time.deriv
electricField
Electromagnetism.FreeSpace.c
SpeedOfLight.val
Space.deriv
Electromagnetism.FreeSpace.ε₀
Electromagnetism.LorentzCurrentDensity.chargeDensity
Electromagnetism.FreeSpace.μ₀
Electromagnetism.LorentzCurrentDensity.currentDensity
Time.deriv_euclid
electricField_differentiable_time
time_deriv_electricField_of_isExtrema
Time.deriv_eq
Space.space_deriv_differentiable_time
magneticFieldMatrix_contDiff
Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable_time
Space.time_deriv_comm_space_deriv
time_deriv_magneticFieldMatrix
Space.deriv_eq_fderiv_basis
Space.deriv_differentiable
electricField_apply_contDiff_space
Space.deriv_commute
isExtrema_iff_gauss_ampere_magneticFieldMatrix
Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable_space
Electromagnetism.FreeSpace.c_sq
time_deriv_time_deriv_magneticFieldMatrix_of_isExtrema 📖mathematicalSpaceTime
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector
IsExtrema
Time.deriv
magneticFieldMatrix
Electromagnetism.FreeSpace.c
SpeedOfLight.val
Space.deriv
Electromagnetism.FreeSpace.ε₀
Electromagnetism.LorentzCurrentDensity.currentDensity
time_deriv_time_deriv_magneticFieldMatrix
time_deriv_electricField_of_isExtrema
Space.deriv_eq_fderiv_basis
Space.deriv_differentiable
magneticFieldMatrix_space_contDiff
Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable_space
Electromagnetism.FreeSpace.c_sq
magneticFieldMatrix_space_deriv_eq
Space.deriv_commute

---

← Back to Index