IsExtrema

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

Statistics

Metric	Count
Definitions IsExtrema, IsExtrema	2
Theorems isExterma_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
Total	16

Electromagnetism.DistElectromagneticPotential

Definitions

Name	Category	Theorems
IsExtrema 📖	MathDef	9 math math: 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

Name	Kind	Assumes	Proves	Validates	Depends On
isExterma_equivariant 📖	mathematical	—	IsExtrema 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 📖	mathematical	—	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 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 📖	mathematical	—	IsExtrema Distribution SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace gradLagrangian	—	isExtrema_iff_gradLagrangian
isExtrema_iff_gradLagrangian 📖	mathematical	—	IsExtrema gradLagrangian Distribution SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace	—	—
isExtrema_iff_space_time 📖	mathematical	—	IsExtrema 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 📖	mathematical	—	IsExtrema 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

Name	Category	Theorems
IsExtrema 📖	MathDef	7 math math: isExtrema_lorentzGroup_apply_iff, isExtrema_iff_gradLagrangian, isExtrema_iff_tensors, isExtrema_iff_fieldStrengthMatrix, constantEB_isExtrema, harmonicWaveX_isExtrema, isExtrema_iff_gauss_ampere_magneticFieldMatrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isExtrema_iff_fieldStrengthMatrix 📖	mathematical	SpaceTime 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 📖	mathematical	SpaceTime 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 📖	mathematical	—	IsExtrema gradLagrangian SpaceTime Lorentz.Vector Lorentz.Vector.instAddCommGroup	—	—
isExtrema_iff_tensors 📖	mathematical	SpaceTime 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 📖	mathematical	SpaceTime 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 📖	mathematical	SpaceTime 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 📖	mathematical	SpaceTime 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 📖	mathematical	SpaceTime 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