EMPotential

📁 Source: PhysLean/Electromagnetism/Kinematics/EMPotential.lean

Statistics

Metric	Count
Definitions DistElectromagneticPotential, deriv, ElectromagneticPotential, deriv	4
Theorems deriv_basis_repr_apply, deriv_eq_sum_sum, deriv_equivariant, toTensor_deriv_basis_repr_apply, deriv_basis_repr_apply, deriv_equivariant, deriv_hasVarAdjDerivAt, differentiable_component, hasVarAdjDerivAt_component, spaceTime_deriv_action_eq_sum, toTensor_deriv_basis_repr_apply	11
Total	15

Electromagnetism

Definitions

Name	Category	Theorems
DistElectromagneticPotential 📖	CompOp	51 math math: DistElectromagneticPotential.fieldStrength_antisymmetric_basis, DistElectromagneticPotential.gradLagrangian_sum_inr_i, DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, DistElectromagneticPotential.oneDimPointParticle_scalarPotential, DistElectromagneticPotential.oneDimPointParticle_div_electricField, DistElectromagneticPotential.gradKineticTerm_sum_inl_eq, DistElectromagneticPotential.infiniteWire_electricField, DistElectromagneticPotential.threeDimPointParticle_vectorPotential, DistElectromagneticPotential.gradKineticTerm_eq_sum_sum, DistElectromagneticPotential.distDeriv_fieldStrength_diag_zero, DistElectromagneticPotential.gradLagrangian_eq_tensor, DistElectromagneticPotential.isExtrema_iff_space_time, DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, DistElectromagneticPotential.deriv_eq_sum_sum, DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, DistElectromagneticPotential.infiniteWire_vectorPotential_fst, DistElectromagneticPotential.isExterma_iff_tensor, DistElectromagneticPotential.oneDimPointParticle_vectorPotential, DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv, DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, DistElectromagneticPotential.fieldStrengthAux_eq_add, DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, DistElectromagneticPotential.threeDimPointParticle_electricField, DistElectromagneticPotential.fieldStrength_basis_repr_eq_single, DistElectromagneticPotential.infiniteWire_vectorPotential, DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, DistElectromagneticPotential.oneDimPointParticle_electricField, DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, DistElectromagneticPotential.fieldStrength_eq_basis, DistElectromagneticPotential.infiniteWire_vectorPotential_snd, DistElectromagneticPotential.isExtrema_iff_vectorPotential, DistElectromagneticPotential.fieldStrength_eq_fieldStrengthAux, DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential, DistElectromagneticPotential.gradLagrangian_sum_inl_0, DistElectromagneticPotential.toTensor_fieldStrengthAux, DistElectromagneticPotential.deriv_basis_repr_apply, DistElectromagneticPotential.isExterma_equivariant, DistElectromagneticPotential.threeDimPointParticle_scalarPotential, DistElectromagneticPotential.infiniteWire_scalarPotential, DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, DistElectromagneticPotential.fieldStrength_diag_zero, DistElectromagneticPotential.deriv_equivariant, DistElectromagneticPotential.threeDimPointParticle_div_electricField, DistElectromagneticPotential.electricField_eq_fieldStrength, DistElectromagneticPotential.fieldStrength_equivariant, DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, DistElectromagneticPotential.gradKineticTerm_eq_fieldStrength, DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix
ElectromagneticPotential 📖	CompOp	6 math math: ElectromagneticPotential.fieldStrengthMatrix_add, ElectromagneticPotential.gradKineticTerm_add, ElectromagneticPotential.gradKineticTerm_smul, ElectromagneticPotential.fieldStrengthMatrix_smul, ElectromagneticPotential.toFieldStrength_smul, ElectromagneticPotential.toFieldStrength_add

Electromagnetism.DistElectromagneticPotential

Definitions

Name	Category	Theorems
deriv 📖	CompOp	6 math math: deriv_eq_sum_sum, fieldStrengthAux_eq_add, toTensor_deriv_basis_repr_apply, toTensor_fieldStrengthAux, deriv_basis_repr_apply, deriv_equivariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv_basis_repr_apply 📖	mathematical	—	Lorentz.CoVector Lorentz.Vector Lorentz.CoVector.instAddCommMonoid Lorentz.Vector.instAddCommMonoid Lorentz.CoVector.instModuleReal Lorentz.Vector.instModuleReal Lorentz.CoVector.basis Lorentz.Vector.basis Distribution SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.CoVector.isNormedAddCommGroup Lorentz.CoVector.innerProductSpace Lorentz.Vector.innerProductSpace Lorentz.Vector.isNormedSpace Electromagnetism.DistElectromagneticPotential Lorentz.Vector.instAddCommGroup deriv SpaceTime.distDeriv	—	deriv_eq_sum_sum
deriv_eq_sum_sum 📖	mathematical	—	Distribution SpaceTime Lorentz.CoVector Lorentz.Vector Lorentz.CoVector.instAddCommMonoid Lorentz.Vector.instAddCommMonoid Lorentz.CoVector.instModuleReal Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.CoVector.isNormedAddCommGroup Lorentz.CoVector.innerProductSpace Lorentz.Vector.innerProductSpace Lorentz.Vector.isNormedSpace Electromagnetism.DistElectromagneticPotential Lorentz.Vector.instAddCommGroup deriv SpaceTime.distDeriv Lorentz.CoVector.basis Lorentz.Vector.basis	—	Lorentz.Vector.instFiniteDimensionalReal SpaceTime.distTensorDeriv_apply
deriv_equivariant 📖	mathematical	—	Electromagnetism.DistElectromagneticPotential Distribution SpaceTime Lorentz.CoVector Lorentz.Vector Lorentz.CoVector.instAddCommMonoid Lorentz.Vector.instAddCommMonoid Lorentz.CoVector.instModuleReal Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.CoVector.isNormedAddCommGroup Lorentz.CoVector.innerProductSpace Lorentz.Vector.innerProductSpace Lorentz.Vector.isNormedSpace Lorentz.Vector.instAddCommGroup deriv LorentzGroup SpaceTime.instSMulElemMatrixSumFinOfNatNatRealLorentzGroupDistribution realLorentzTensor.Color realLorentzTensor.Color.up Lorentz.Vector.tensorial realLorentzTensor.Color.down TensorSpecies.Tensorial.prod lorentzGroupIsGroup realLorentzTensor Lorentz.CoVector.tensorial	—	Lorentz.Vector.instFiniteDimensionalReal deriv.eq_1 SpaceTime.distTensorDeriv_equivariant
toTensor_deriv_basis_repr_apply 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down realLorentzTensor.Color.up TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.basis Lorentz.CoVector Lorentz.Vector Lorentz.CoVector.instAddCommMonoid Lorentz.Vector.instAddCommMonoid Lorentz.CoVector.instModuleReal Lorentz.Vector.instModuleReal TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.prod Lorentz.CoVector.tensorial Lorentz.Vector.tensorial Distribution SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.CoVector.isNormedAddCommGroup Lorentz.CoVector.innerProductSpace Lorentz.Vector.innerProductSpace Lorentz.Vector.isNormedSpace Electromagnetism.DistElectromagneticPotential Lorentz.Vector.instAddCommGroup deriv SpaceTime.distDeriv	—	TensorSpecies.Tensorial.basis_toTensor_apply TensorSpecies.Tensorial.basis_map_prod Lorentz.Vector.tensor_basis_map_eq_basis_reindex Lorentz.CoVector.tensor_basis_map_eq_basis_reindex deriv_basis_repr_apply

Electromagnetism.ElectromagneticPotential

Definitions

Name	Category	Theorems
deriv 📖	CompOp	5 math math: toTensor_toFieldStrength, deriv_basis_repr_apply, toTensor_deriv_basis_repr_apply, toFieldStrength_eq_add, deriv_equivariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv_basis_repr_apply 📖	mathematical	—	Lorentz.CoVector Lorentz.Vector Lorentz.CoVector.instAddCommMonoid Lorentz.Vector.instAddCommMonoid Lorentz.CoVector.instModuleReal Lorentz.Vector.instModuleReal Lorentz.CoVector.basis Lorentz.Vector.basis deriv SpaceTime.deriv Lorentz.Vector.instAddCommGroup Lorentz.Vector.isNormedAddCommGroup	—	deriv.eq_1
deriv_equivariant 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	deriv LorentzGroup TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.tensorial Lorentz.CoVector Lorentz.CoVector.instAddCommMonoid Lorentz.CoVector.instModuleReal realLorentzTensor.Color.down TensorSpecies.Tensorial.prod Lorentz.CoVector.tensorial	—	spaceTime_deriv_action_eq_sum Lorentz.CoVector.smul_basis Lorentz.Vector.smul_basis TensorSpecies.Tensorial.smul_prod deriv.eq_1 TensorSpecies.Tensorial.smulLinearMap_apply
deriv_hasVarAdjDerivAt 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	HasVarAdjDerivAt SpaceTime.instMeasureSpace instInnerProductSpace' Lorentz.Vector.innerProductSpace SpaceTime.deriv Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.basis	—	HasVarAdjDerivAt.fderiv' hasVarAdjDerivAt_component Lorentz.Vector.instFiniteDimensionalReal SpaceTime.instBorelSpace SpaceTime.instIsAddHaarMeasureVolume HasVarAdjDerivAt.congr SpaceTime.deriv_apply_eq
differentiable_component 📖	—	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	—	—	SpaceTime.differentiable_vector
hasVarAdjDerivAt_component 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	HasVarAdjDerivAt SpaceTime.instMeasureSpace instInnerProductSpace' Lorentz.Vector.innerProductSpace Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.basis	—	HasVarAdjDerivAt.fmap Lorentz.Vector.instFiniteDimensionalReal Lorentz.Vector.coord_contDiff Lorentz.Vector.coord_differentiableAt Lorentz.Vector.fderiv_coord Lorentz.Vector.basis_inner
spaceTime_deriv_action_eq_sum 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	SpaceTime.deriv LorentzGroup TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.tensorial	—	SpaceTime.differentiable_vector Lorentz.Vector.actionCLM_apply SpaceTime.deriv_eq SpaceTime.fderiv_vector Lorentz.Vector.smul_eq_sum SpaceTime.deriv_comp_lorentz_action Lorentz.Vector.apply_sum
toTensor_deriv_basis_repr_apply 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down realLorentzTensor.Color.up TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.basis Lorentz.CoVector Lorentz.Vector Lorentz.CoVector.instAddCommMonoid Lorentz.Vector.instAddCommMonoid Lorentz.CoVector.instModuleReal Lorentz.Vector.instModuleReal TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.prod Lorentz.CoVector.tensorial Lorentz.Vector.tensorial deriv SpaceTime.deriv Lorentz.Vector.instAddCommGroup Lorentz.Vector.isNormedAddCommGroup	—	TensorSpecies.Tensorial.basis_toTensor_apply TensorSpecies.Tensorial.basis_map_prod Lorentz.Vector.tensor_basis_map_eq_basis_reindex Lorentz.CoVector.tensor_basis_map_eq_basis_reindex deriv_basis_repr_apply

---

← Back to Index