KineticTerm

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

Statistics

Metric	Count
Definitions gradKineticTerm, gradKineticTerm, kineticTerm	3
Theorems gradKineticTerm_eq_distTensorDeriv, gradKineticTerm_eq_fieldStrength, gradKineticTerm_eq_sum_sum, gradKineticTerm_sum_inl_eq, gradKineticTerm_sum_inr_eq, gradKineticTerm_add, gradKineticTerm_eq_electric_magnetic, gradKineticTerm_eq_electric_magnetic_three, gradKineticTerm_eq_fieldStrength, gradKineticTerm_eq_sum_fderiv, gradKineticTerm_eq_sum_sum, gradKineticTerm_eq_tensorDeriv, gradKineticTerm_smul, kineticTerm_add_const, kineticTerm_add_time_mul_const, kineticTerm_const, kineticTerm_contDiff, kineticTerm_eq_electricMatrix_magneticFieldMatrix, kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space, kineticTerm_eq_electric_magnetic, kineticTerm_eq_electric_magnetic', kineticTerm_eq_sum, kineticTerm_eq_sum_fieldStrengthMatrix, kineticTerm_eq_sum_fieldStrengthMatrix_sq, kineticTerm_eq_sum_potential, kineticTerm_equivariant, kineticTerm_hasVarGradientAt	27
Total	30

Electromagnetism.DistElectromagneticPotential

Definitions

Name	Category	Theorems
gradKineticTerm 📖	CompOp	5 math math: gradKineticTerm_sum_inl_eq, gradKineticTerm_eq_sum_sum, gradKineticTerm_eq_distTensorDeriv, gradKineticTerm_sum_inr_eq, gradKineticTerm_eq_fieldStrength

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gradKineticTerm_eq_distTensorDeriv 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Electromagnetism.DistElectromagneticPotential Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup gradKineticTerm minkowskiMatrix TensorSpecies.Tensor realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F 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 fieldStrength	—	TensorSpecies.Tensor.PermCond.auto TensorSpecies.Tensor.contrT_decide Lorentz.Vector.instFiniteDimensionalReal Lorentz.Vector.basis_eq_map_tensor_basis TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.Tensor.permT_basis_repr_symm_apply realLorentzTensor.repDim_eq_one_plus_dim realLorentzTensor.contrT_basis_repr_apply_eq_fin gradKineticTerm_eq_fieldStrength Lorentz.Vector.apply_sum Lorentz.Vector.basis_apply SpaceTime.distTensorDeriv_toTensor_basis_repr TensorSpecies.Tensorial.basis_toTensor_apply TensorSpecies.Tensorial.basis_map_prod Lorentz.Vector.tensor_basis_map_eq_basis_reindex
gradKineticTerm_eq_fieldStrength 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Electromagnetism.DistElectromagneticPotential Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup gradKineticTerm Electromagnetism.FreeSpace.μ₀ minkowskiMatrix Lorentz.Vector.basis Lorentz.Vector.innerProductSpace SpaceTime.distDeriv fieldStrength	—	gradKineticTerm_eq_sum_sum Lorentz.Vector.instFiniteDimensionalReal SpaceTime.distDeriv_apply Distribution.fderivD_apply fieldStrength_basis_repr_eq_single SpaceTime.apply_fderiv_eq_distDeriv minkowskiMatrix.η_apply_sq_eq_one
gradKineticTerm_eq_sum_sum 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Electromagnetism.DistElectromagneticPotential Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup gradKineticTerm Electromagnetism.FreeSpace.μ₀ minkowskiMatrix SpaceTime.distDeriv Lorentz.Vector.basis	—	—
gradKineticTerm_sum_inl_eq 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Electromagnetism.DistElectromagneticPotential Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup gradKineticTerm Electromagnetism.FreeSpace.μ₀ SpeedOfLight.val Electromagnetism.FreeSpace.c Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal SpaceTime.distTimeSlice Space.distSpaceDiv electricField	—	gradKineticTerm_eq_fieldStrength Lorentz.Vector.apply_sum SpaceTime.distTimeSlice_symm_apply Space.distSpaceDiv_apply_eq_sum_distSpaceDeriv Lorentz.Vector.basis_apply minkowskiMatrix.inl_0_inl_0 distDeriv_fieldStrength_diag_zero Space.distSpaceDeriv_apply' electricField_eq_fieldStrength SpaceTime.distTimeSlice_apply fieldStrength_antisymmetric_basis Space.apply_fderiv_eq_distSpaceDeriv SpaceTime.distTimeSlice_distDeriv_inr
gradKineticTerm_sum_inr_eq 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Electromagnetism.DistElectromagneticPotential Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup gradKineticTerm Electromagnetism.FreeSpace.μ₀ SpeedOfLight.val Electromagnetism.FreeSpace.c Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal SpaceTime.distTimeSlice Space.distTimeDeriv electricField Space.distSpaceDeriv magneticFieldMatrix	—	gradKineticTerm_eq_fieldStrength Lorentz.Vector.apply_sum Lorentz.Vector.basis_apply minkowskiMatrix.inr_i_inr_i SpaceTime.distTimeSlice_symm_apply Space.distTimeDeriv_apply' electricField_eq_fieldStrength Space.apply_fderiv_eq_distTimeDeriv SpaceTime.distTimeSlice_symm_distTimeDeriv_eq Space.distSpaceDeriv_apply' magneticFieldMatrix_basis_repr_eq_fieldStrength Space.apply_fderiv_eq_distSpaceDeriv

Electromagnetism.ElectromagneticPotential

Definitions

Name	Category	Theorems
gradKineticTerm 📖	CompOp	11 math math: gradKineticTerm_eq_fieldStrength, gradKineticTerm_eq_sum_sum, gradKineticTerm_eq_sum_fderiv, gradLagrangian_eq_kineticTerm_sub, gradKineticTerm_eq_electric_magnetic, kineticTerm_hasVarGradientAt, gradKineticTerm_add, gradKineticTerm_smul, gradKineticTerm_eq_tensorDeriv, lagrangian_hasVarGradientAt_eq_add_gradKineticTerm, gradKineticTerm_eq_electric_magnetic_three
kineticTerm 📖	CompOp	15 math math: kineticTerm_eq_electric_magnetic', kineticTerm_eq_sum_potential, kineticTerm_contDiff, kineticTerm_eq_sum, kineticTerm_hasVarGradientAt, canonicalMomentum_eq_gradient_kineticTerm, kineticTerm_eq_electric_magnetic, kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space, kineticTerm_eq_sum_fieldStrengthMatrix_sq, kineticTerm_const, kineticTerm_eq_sum_fieldStrengthMatrix, kineticTerm_add_time_mul_const, kineticTerm_add_const, kineticTerm_eq_electricMatrix_magneticFieldMatrix, kineticTerm_equivariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gradKineticTerm_add 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradKineticTerm Electromagnetism.ElectromagneticPotential Lorentz.Vector.instAddCommMonoid	—	gradKineticTerm_eq_fieldStrength SpaceTime.deriv_eq fieldStrengthMatrix_add fieldStrengthMatrix_differentiable
gradKineticTerm_eq_electric_magnetic 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradKineticTerm 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 Lorentz.Vector.basis Time.deriv Space.deriv magneticFieldMatrix	—	Lorentz.Vector.differentiable_apply toFieldStrength_basis_repr_apply_eq_single SpaceTime.deriv_eq gradKineticTerm_eq_fieldStrength div_electricField_eq_fieldStrengthMatrix minkowskiMatrix.inl_0_inl_0 SpaceTime.toTimeAndSpace_symm_apply_time_space minkowskiMatrix.inr_i_inr_i curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix
gradKineticTerm_eq_electric_magnetic_three 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradKineticTerm 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 Lorentz.Vector.basis Time.deriv Space.curl magneticField	—	gradKineticTerm_eq_electric_magnetic magneticField_curl_eq_magneticFieldMatrix
gradKineticTerm_eq_fieldStrength 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradKineticTerm Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Electromagnetism.FreeSpace.μ₀ minkowskiMatrix SpaceTime.deriv fieldStrengthMatrix Lorentz.Vector.basis	—	Lorentz.Vector.differentiable_apply gradKineticTerm_eq_sum_sum minkowskiMatrix.η_apply_sq_eq_one SpaceTime.deriv_eq toFieldStrength_basis_repr_apply_eq_single
gradKineticTerm_eq_sum_fderiv 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradKineticTerm Lorentz.Vector.instAddCommMonoid Electromagnetism.FreeSpace.μ₀	—	HasVarGradientAt.varGradient Lorentz.Vector.instFiniteDimensionalReal SpaceTime.instBorelSpace SpaceTime.instIsFiniteMeasureOnCompactsVolume SpaceTime.instIsOpenPosMeasureVolume kineticTerm_eq_sum_potential HasVarAdjDerivAt.mul deriv_hasVarAdjDerivAt HasVarAdjDerivAt.const_mul HasVarAdjDerivAt.neg HasVarAdjDerivAt.add HasVarAdjDerivAt.sum
gradKineticTerm_eq_sum_sum 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradKineticTerm Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Electromagnetism.FreeSpace.μ₀ minkowskiMatrix SpaceTime.deriv Lorentz.Vector.instAddCommGroup Lorentz.Vector.basis	—	Lorentz.Vector.differentiable_apply gradKineticTerm_eq_sum_fderiv SpaceTime.deriv_eq
gradKineticTerm_eq_tensorDeriv 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradKineticTerm 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 Lorentz.Vector.basis_eq_map_tensor_basis TensorSpecies.Tensor.PermCond.inv_perserve_color TensorSpecies.Tensor.permT_basis_repr_symm_apply realLorentzTensor.repDim_eq_one_plus_dim realLorentzTensor.contrT_basis_repr_apply_eq_fin SpaceTime.tensorDeriv_toTensor_basis_repr toFieldStrength_differentiable toFieldStrength_tensor_basis_eq_basis gradKineticTerm_eq_fieldStrength Lorentz.Vector.apply_sum Lorentz.Vector.basis_apply Lorentz.Vector.basis_repr_apply
gradKineticTerm_smul 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	gradKineticTerm Electromagnetism.ElectromagneticPotential Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal	—	gradKineticTerm_eq_fieldStrength SpaceTime.deriv_eq fieldStrengthMatrix_differentiable fieldStrengthMatrix_smul
kineticTerm_add_const 📖	mathematical	—	kineticTerm Lorentz.Vector Lorentz.Vector.instAddCommMonoid	—	kineticTerm_eq_sum_potential SpaceTime.deriv_eq
kineticTerm_add_time_mul_const 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	kineticTerm Lorentz.Vector.instAddCommMonoid Electromagnetism.FreeSpace.μ₀ minkowskiMatrix SpaceTime.deriv	—	SpaceTime.deriv_eq Lorentz.Vector.coord_differentiableAt Lorentz.Vector.instFiniteDimensionalReal Lorentz.Vector.fderiv_coord Lorentz.Vector.basis_apply kineticTerm_eq_sum_potential minkowskiMatrix.inl_0_inl_0
kineticTerm_const 📖	mathematical	—	kineticTerm SpaceTime	—	kineticTerm_eq_sum_potential SpaceTime.deriv_eq
kineticTerm_contDiff 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	kineticTerm	—	kineticTerm_eq_sum_fieldStrengthMatrix fieldStrengthMatrix_contDiff
kineticTerm_eq_electricMatrix_magneticFieldMatrix 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	kineticTerm Electromagnetism.FreeSpace.ε₀ electricField Electromagnetism.FreeSpace.c Time Lorentz.Vector.instAddCommMonoid Time.instSeminormedAddCommGroup Time.instNormedAddCommGroup Time.instModuleReal SpaceTime.time Space Space.instSeminormedAddCommGroup Space.instAddCommMonoid Space.instModuleReal SpaceTime.space Electromagnetism.FreeSpace.μ₀ magneticFieldMatrix	—	kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space SpaceTime.toTimeAndSpace_symm_apply_time_space
kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	kineticTerm Time Space Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Time.instNormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.instAddCommMonoid Time.instModuleReal Space.instModuleReal SpaceTime.toTimeAndSpace Electromagnetism.FreeSpace.c Electromagnetism.FreeSpace.ε₀ electricField Electromagnetism.FreeSpace.μ₀ magneticFieldMatrix	—	kineticTerm_eq_sum_fieldStrengthMatrix_sq minkowskiMatrix.inl_0_inl_0 minkowskiMatrix.inr_i_inr_i fieldStrengthMatrix_diag_eq_zero electricField_eq_fieldStrengthMatrix Electromagnetism.FreeSpace.c_abs fieldStrengthMatrix_antisymm Electromagnetism.FreeSpace.c_sq
kineticTerm_eq_electric_magnetic 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	kineticTerm Time Space Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Time.instNormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.instAddCommMonoid Time.instModuleReal Space.instModuleReal SpaceTime.toTimeAndSpace Electromagnetism.FreeSpace.c Electromagnetism.FreeSpace.ε₀ electricField Electromagnetism.FreeSpace.μ₀ magneticField	—	kineticTerm_eq_sum fieldStrengthMatrix_eq_electric_magnetic minkowskiMatrix.off_diag_zero minkowskiMatrix.inl_0_inl_0 minkowskiMatrix.inr_i_inr_i Electromagnetism.FreeSpace.c_sq
kineticTerm_eq_electric_magnetic' 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	kineticTerm Electromagnetism.FreeSpace.ε₀ electricField Electromagnetism.FreeSpace.c Time Lorentz.Vector.instAddCommMonoid Time.instSeminormedAddCommGroup Time.instNormedAddCommGroup Time.instModuleReal SpaceTime.time Space Space.instSeminormedAddCommGroup Space.instAddCommMonoid Space.instModuleReal SpaceTime.space Electromagnetism.FreeSpace.μ₀ magneticField	—	kineticTerm_eq_electric_magnetic SpaceTime.toTimeAndSpace_symm_apply_time_space
kineticTerm_eq_sum 📖	mathematical	—	kineticTerm Electromagnetism.FreeSpace.μ₀ minkowskiMatrix Lorentz.CoVector Lorentz.Vector Lorentz.CoVector.instAddCommMonoid Lorentz.Vector.instAddCommMonoid Lorentz.CoVector.instModuleReal Lorentz.Vector.instModuleReal Lorentz.CoVector.basis Lorentz.Vector.basis toFieldStrength	—	kineticTerm.eq_1 TensorSpecies.Tensor.toField_eq_repr realLorentzTensor.repDim_eq_one_plus_dim realLorentzTensor.contrT_basis_repr_apply_eq_fin TensorSpecies.Tensor.prodT_basis_repr_apply realLorentzTensor.coMetric_repr_apply_eq_minkowskiMatrix toFieldStrength_tensor_basis_eq_basis
kineticTerm_eq_sum_fieldStrengthMatrix 📖	mathematical	—	kineticTerm Electromagnetism.FreeSpace.μ₀ minkowskiMatrix fieldStrengthMatrix	—	kineticTerm_eq_sum
kineticTerm_eq_sum_fieldStrengthMatrix_sq 📖	mathematical	—	kineticTerm Electromagnetism.FreeSpace.μ₀ minkowskiMatrix fieldStrengthMatrix	—	kineticTerm_eq_sum_fieldStrengthMatrix minkowskiMatrix.off_diag_zero
kineticTerm_eq_sum_potential 📖	mathematical	—	kineticTerm Electromagnetism.FreeSpace.μ₀ minkowskiMatrix SpaceTime.deriv Lorentz.Vector Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup	—	kineticTerm_eq_sum toFieldStrength_basis_repr_apply_eq_single minkowskiMatrix.off_diag_zero minkowskiMatrix.η_apply_sq_eq_one
kineticTerm_equivariant 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	kineticTerm LorentzGroup TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.tensorial	—	kineticTerm.eq_1 toFieldStrength_equivariant TensorSpecies.Tensorial.toTensor_smul realLorentzTensor.actionT_coMetric TensorSpecies.Tensor.prodT_equivariant TensorSpecies.Tensor.contrT_equivariant TensorSpecies.Tensor.toField_equivariant
kineticTerm_hasVarGradientAt 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	HasVarGradientAt SpaceTime.instMeasureSpace instInnerProductSpace' Lorentz.Vector.innerProductSpace kineticTerm gradKineticTerm	—	gradKineticTerm_eq_sum_fderiv kineticTerm_eq_sum_potential HasVarAdjDerivAt.mul SpaceTime.instBorelSpace SpaceTime.instIsFiniteMeasureOnCompactsVolume deriv_hasVarAdjDerivAt HasVarAdjDerivAt.const_mul HasVarAdjDerivAt.neg HasVarAdjDerivAt.add HasVarAdjDerivAt.sum

---

← Back to Index