Lagrangian

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

Statistics

Metric	Count
Definitions gradFreeCurrentPotential, gradLagrangian, freeCurrentPotential, gradFreeCurrentPotential, gradLagrangian, lagrangian	6
Theorems gradFreeCurrentPotential_eq_sum_basis, gradFreeCurrentPotential_eq_tensor, gradFreeCurrentPotential_sum_inl_0, gradFreeCurrentPotential_sum_inr_i, gradLagrangian_eq_tensor, gradLagrangian_sum_inl_0, gradLagrangian_sum_inr_i, freeCurrentPotential_add_const, freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, freeCurrentPotential_hasVarGradientAt, gradFreeCurrentPotential_eq_chargeDensity_currentDensity, gradFreeCurrentPotential_eq_sum_basis, gradFreeCurrentPotential_eq_tensor, gradLagrangian_eq_electricField_magneticField, gradLagrangian_eq_kineticTerm_sub, gradLagrangian_eq_sum_fieldStrengthMatrix, gradLagrangian_eq_tensor, lagrangian_add_const, lagrangian_eq_electric_magnetic, lagrangian_hasVarGradientAt_eq_add_gradKineticTerm, lagrangian_hasVarGradientAt_gradLagrangian	21
Total	27

Electromagnetism.DistElectromagneticPotential

Definitions

Name	Category	Theorems
gradFreeCurrentPotential 📖	CompOp	4 math math: gradFreeCurrentPotential_eq_sum_basis, gradFreeCurrentPotential_eq_tensor, gradFreeCurrentPotential_sum_inl_0, gradFreeCurrentPotential_sum_inr_i
gradLagrangian 📖	CompOp	5 math math: isExtrema_iff_gradLagrangian, gradLagrangian_sum_inr_i, gradLagrangian_eq_tensor, gradLagrangian_sum_inl_0, isExtrema_iff_components

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gradFreeCurrentPotential_eq_sum_basis 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Electromagnetism.DistLorentzCurrentDensity Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup gradFreeCurrentPotential minkowskiMatrix Lorentz.Vector.basis	—	—
gradFreeCurrentPotential_eq_tensor 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Electromagnetism.DistLorentzCurrentDensity Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup gradFreeCurrentPotential minkowskiMatrix TensorSpecies.Tensor realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.toTensor Lorentz.Vector.tensorial TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto	—	TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.permT_id_self Lorentz.Vector.basis_repr_apply gradFreeCurrentPotential_eq_sum_basis Lorentz.Vector.apply_sum Lorentz.Vector.basis_apply
gradFreeCurrentPotential_sum_inl_0 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Electromagnetism.DistLorentzCurrentDensity Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup gradFreeCurrentPotential SpeedOfLight.val Electromagnetism.FreeSpace.c Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal SpaceTime.distTimeSlice Electromagnetism.DistLorentzCurrentDensity.chargeDensity	—	Lorentz.Vector.apply_sum Lorentz.Vector.basis_apply minkowskiMatrix.inl_0_inl_0 Lorentz.Vector.instFiniteDimensionalReal SpaceTime.distTimeSlice_symm_apply
gradFreeCurrentPotential_sum_inr_i 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Electromagnetism.DistLorentzCurrentDensity Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup gradFreeCurrentPotential Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal SpaceTime.distTimeSlice Electromagnetism.FreeSpace.c Electromagnetism.DistLorentzCurrentDensity.currentDensity	—	Lorentz.Vector.apply_sum Lorentz.Vector.basis_apply minkowskiMatrix.inr_i_inr_i SpaceTime.distTimeSlice_symm_apply
gradLagrangian_eq_tensor 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace gradLagrangian minkowskiMatrix TensorSpecies.Tensor realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal TensorSpecies.Tensorial.toTensor Lorentz.Vector.tensorial realLorentzTensor.Color.down TensorSpecies.Tensor.Pure.dropPairEmb TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond realLorentzTensor.instDecidableEqColor TensorSpecies.Tensor.contrT TensorSpecies.Tensor.contrT_decide TensorSpecies.τ Lorentz.CoVector Lorentz.CoVector.instAddCommMonoid Lorentz.Vector.innerProductSpace Lorentz.CoVector.instModuleReal TensorSpecies.Tensorial.prod Lorentz.CoVector.tensorial Electromagnetism.FreeSpace.μ₀ Lorentz.CoVector.isNormedAddCommGroup Lorentz.CoVector.innerProductSpace SpaceTime.distTensorDeriv Lorentz.Vector.instFiniteDimensionalReal Electromagnetism.DistElectromagneticPotential Lorentz.Vector.instAddCommGroup fieldStrength Electromagnetism.DistLorentzCurrentDensity	—	TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.contrT_decide Lorentz.Vector.instFiniteDimensionalReal gradLagrangian.eq_1 TensorSpecies.Tensor.PermCond.comp Lorentz.Vector.apply_sub TensorSpecies.Tensor.permT_permT TensorSpecies.Tensor.permT.congr_simp gradKineticTerm_eq_distTensorDeriv gradFreeCurrentPotential_eq_tensor TensorSpecies.Tensor.permT_id_self TensorSpecies.Tensor.permT_congr_eq_id
gradLagrangian_sum_inl_0 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace gradLagrangian Electromagnetism.FreeSpace.μ₀ SpeedOfLight.val Electromagnetism.FreeSpace.c Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal SpaceTime.distTimeSlice Space.distSpaceDiv Electromagnetism.DistElectromagneticPotential Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup electricField Electromagnetism.DistLorentzCurrentDensity Electromagnetism.DistLorentzCurrentDensity.chargeDensity	—	Lorentz.Vector.apply_sub gradKineticTerm_sum_inl_eq gradFreeCurrentPotential_sum_inl_0
gradLagrangian_sum_inr_i 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace gradLagrangian Electromagnetism.FreeSpace.μ₀ SpeedOfLight.val Electromagnetism.FreeSpace.c Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal SpaceTime.distTimeSlice Space.distTimeDeriv Electromagnetism.DistElectromagneticPotential Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup electricField Space.distSpaceDeriv magneticFieldMatrix Electromagnetism.DistLorentzCurrentDensity Electromagnetism.DistLorentzCurrentDensity.currentDensity	—	Lorentz.Vector.apply_sub gradKineticTerm_sum_inr_eq gradFreeCurrentPotential_sum_inr_i

Electromagnetism.ElectromagneticPotential

Definitions

Name	Category	Theorems
freeCurrentPotential 📖	CompOp	3 math math: freeCurrentPotential_hasVarGradientAt, freeCurrentPotential_add_const, freeCurrentPotential_eq_sum_scalarPotential_vectorPotential
gradFreeCurrentPotential 📖	CompOp	5 math math: gradFreeCurrentPotential_eq_tensor, gradLagrangian_eq_kineticTerm_sub, gradFreeCurrentPotential_eq_sum_basis, lagrangian_hasVarGradientAt_eq_add_gradKineticTerm, gradFreeCurrentPotential_eq_chargeDensity_currentDensity
gradLagrangian 📖	CompOp	6 math math: gradLagrangian_eq_sum_fieldStrengthMatrix, gradLagrangian_eq_tensor, gradLagrangian_eq_kineticTerm_sub, gradLagrangian_eq_electricField_magneticField, isExtrema_iff_gradLagrangian, lagrangian_hasVarGradientAt_gradLagrangian
lagrangian 📖	CompOp	6 math math: hamiltonian_eq_electricField_scalarPotential, hamiltonian_eq_electricField_vectorPotential, lagrangian_hasVarGradientAt_eq_add_gradKineticTerm, lagrangian_hasVarGradientAt_gradLagrangian, lagrangian_add_const, lagrangian_eq_electric_magnetic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
freeCurrentPotential_add_const 📖	mathematical	—	freeCurrentPotential Lorentz.Vector Lorentz.Vector.instAddCommMonoid Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct	—	freeCurrentPotential.eq_1
freeCurrentPotential_eq_sum_scalarPotential_vectorPotential 📖	mathematical	—	freeCurrentPotential scalarPotential Electromagnetism.FreeSpace.c SpaceTime Time Lorentz.Vector.instAddCommMonoid Time.instSeminormedAddCommGroup Time.instNormedAddCommGroup Lorentz.Vector.instModuleReal Time.instModuleReal SpaceTime.time Lorentz.Vector.isNormedAddCommGroup Space Space.instSeminormedAddCommGroup Space.instAddCommMonoid Space.instModuleReal SpaceTime.space Electromagnetism.LorentzCurrentDensity.chargeDensity vectorPotential Electromagnetism.LorentzCurrentDensity.currentDensity	—	freeCurrentPotential.eq_1 Lorentz.Vector.minkowskiProduct_toCoord_minkowskiMatrix minkowskiMatrix.inl_0_inl_0 minkowskiMatrix.inr_i_inr_i SpaceTime.toTimeAndSpace_symm_apply_time_space
freeCurrentPotential_hasVarGradientAt 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	HasVarGradientAt SpaceTime.instMeasureSpace instInnerProductSpace' Lorentz.Vector.innerProductSpace freeCurrentPotential Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal minkowskiMatrix Lorentz.Vector.basis	—	freeCurrentPotential.eq_1 Lorentz.Vector.minkowskiProduct_toCoord_minkowskiMatrix HasVarGradientAt.sum SpaceTime.instBorelSpace SpaceTime.instIsFiniteMeasureOnCompactsVolume hasVarAdjDerivAt_component Lorentz.Vector.contDiff_apply HasVarAdjDerivAt.fun_mul
gradFreeCurrentPotential_eq_chargeDensity_currentDensity 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradFreeCurrentPotential Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal SpeedOfLight.val Electromagnetism.FreeSpace.c Electromagnetism.LorentzCurrentDensity.chargeDensity Time Time.instSeminormedAddCommGroup Time.instNormedAddCommGroup Time.instModuleReal SpaceTime.time Space Space.instSeminormedAddCommGroup Space.instAddCommMonoid Space.instModuleReal SpaceTime.space Lorentz.Vector.basis Electromagnetism.LorentzCurrentDensity.currentDensity	—	gradFreeCurrentPotential_eq_sum_basis minkowskiMatrix.inl_0_inl_0 minkowskiMatrix.inr_i_inr_i SpaceTime.toTimeAndSpace_symm_apply_time_space
gradFreeCurrentPotential_eq_sum_basis 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradFreeCurrentPotential Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal minkowskiMatrix Lorentz.Vector.basis	—	HasVarGradientAt.varGradient Lorentz.Vector.instFiniteDimensionalReal SpaceTime.instBorelSpace SpaceTime.instIsFiniteMeasureOnCompactsVolume SpaceTime.instIsOpenPosMeasureVolume freeCurrentPotential_hasVarGradientAt
gradFreeCurrentPotential_eq_tensor 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradFreeCurrentPotential minkowskiMatrix TensorSpecies.Tensor realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal TensorSpecies.Tensorial.toTensor Lorentz.Vector.tensorial TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto	—	TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.permT_id_self Lorentz.Vector.basis_repr_apply gradFreeCurrentPotential_eq_sum_basis Lorentz.Vector.apply_sum Lorentz.Vector.basis_apply
gradLagrangian_eq_electricField_magneticField 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradLagrangian Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Electromagnetism.FreeSpace.μ₀ SpeedOfLight.val Electromagnetism.FreeSpace.c Space.div electricField Time Time.instSeminormedAddCommGroup Time.instNormedAddCommGroup Time.instModuleReal SpaceTime.time Space Space.instSeminormedAddCommGroup Space.instAddCommMonoid Space.instModuleReal SpaceTime.space Electromagnetism.LorentzCurrentDensity.chargeDensity Lorentz.Vector.basis Electromagnetism.FreeSpace.ε₀ Time.deriv Space.deriv magneticFieldMatrix Electromagnetism.LorentzCurrentDensity.currentDensity	—	gradLagrangian_eq_kineticTerm_sub gradKineticTerm_eq_electric_magnetic gradFreeCurrentPotential_eq_chargeDensity_currentDensity Electromagnetism.FreeSpace.c_sq
gradLagrangian_eq_kineticTerm_sub 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradLagrangian gradKineticTerm gradFreeCurrentPotential	—	HasVarGradientAt.varGradient Lorentz.Vector.instFiniteDimensionalReal SpaceTime.instBorelSpace SpaceTime.instIsFiniteMeasureOnCompactsVolume SpaceTime.instIsOpenPosMeasureVolume lagrangian_hasVarGradientAt_eq_add_gradKineticTerm
gradLagrangian_eq_sum_fieldStrengthMatrix 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradLagrangian Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal minkowskiMatrix Electromagnetism.FreeSpace.μ₀ SpaceTime.deriv fieldStrengthMatrix Lorentz.Vector.basis	—	gradLagrangian_eq_kineticTerm_sub gradKineticTerm_eq_fieldStrength gradFreeCurrentPotential_eq_sum_basis
gradLagrangian_eq_tensor 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradLagrangian minkowskiMatrix TensorSpecies.Tensor realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal TensorSpecies.Tensorial.toTensor Lorentz.Vector.tensorial realLorentzTensor.Color.down TensorSpecies.Tensor.Pure.dropPairEmb TensorSpecies.Tensor.permT TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.PermCond realLorentzTensor.instDecidableEqColor TensorSpecies.Tensor.contrT TensorSpecies.Tensor.contrT_decide TensorSpecies.τ Lorentz.CoVector Lorentz.CoVector.instAddCommMonoid Lorentz.Vector.innerProductSpace Lorentz.CoVector.instModuleReal TensorSpecies.Tensorial.prod Lorentz.CoVector.tensorial Electromagnetism.FreeSpace.μ₀ SpaceTime.tensorDeriv toFieldStrength	—	TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.contrT_decide gradLagrangian_eq_kineticTerm_sub TensorSpecies.Tensor.PermCond.comp Lorentz.Vector.apply_sub TensorSpecies.Tensor.permT_permT TensorSpecies.Tensor.permT.congr_simp gradKineticTerm_eq_tensorDeriv gradFreeCurrentPotential_eq_tensor TensorSpecies.Tensor.permT_id_self TensorSpecies.Tensor.permT_congr_eq_id
lagrangian_add_const 📖	mathematical	—	lagrangian Lorentz.Vector Lorentz.Vector.instAddCommMonoid Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommGroup Lorentz.Vector.minkowskiProduct	—	lagrangian.eq_1 kineticTerm_add_const freeCurrentPotential_add_const
lagrangian_eq_electric_magnetic 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	lagrangian Electromagnetism.FreeSpace.ε₀ electricField Electromagnetism.FreeSpace.c Time Lorentz.Vector.instAddCommMonoid Time.instSeminormedAddCommGroup Time.instNormedAddCommGroup Lorentz.Vector.instModuleReal Time.instModuleReal SpaceTime.time Space Space.instSeminormedAddCommGroup Space.instAddCommMonoid Space.instModuleReal SpaceTime.space Electromagnetism.FreeSpace.μ₀ magneticFieldMatrix scalarPotential Electromagnetism.LorentzCurrentDensity.chargeDensity vectorPotential Electromagnetism.LorentzCurrentDensity.currentDensity	—	lagrangian.eq_1 kineticTerm_eq_electricMatrix_magneticFieldMatrix freeCurrentPotential_eq_sum_scalarPotential_vectorPotential
lagrangian_hasVarGradientAt_eq_add_gradKineticTerm 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	HasVarGradientAt SpaceTime.instMeasureSpace instInnerProductSpace' Lorentz.Vector.innerProductSpace lagrangian gradKineticTerm gradFreeCurrentPotential	—	lagrangian.eq_1 HasVarGradientAt.add SpaceTime.instBorelSpace SpaceTime.instIsFiniteMeasureOnCompactsVolume kineticTerm_hasVarGradientAt HasVarGradientAt.neg gradFreeCurrentPotential_eq_sum_basis freeCurrentPotential_hasVarGradientAt
lagrangian_hasVarGradientAt_gradLagrangian 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	HasVarGradientAt SpaceTime.instMeasureSpace instInnerProductSpace' Lorentz.Vector.innerProductSpace lagrangian gradLagrangian	—	gradLagrangian_eq_kineticTerm_sub lagrangian_hasVarGradientAt_eq_add_gradKineticTerm

---

← Back to Index