Documentation Verification Report

EMPotential

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

Statistics

Metric	Count
Definitions `DistElectromagneticPotential`, `deriv`, `ElectromagneticPotential`, `deriv`, `instAdd`, `instCoeFunForallSpaceTimeVector`, `instSMulReal`, `val`	8
Theorems `deriv_basis_repr_apply`, `deriv_eq_sum_sum`, `deriv_equivariant`, `toTensor_deriv_basis_repr_apply`, `add_apply`, `add_val`, `deriv_basis_repr_apply`, `deriv_equivariant`, `deriv_hasVarAdjDerivAt`, `differentiable_component`, `hasVarAdjDerivAt_component`, `smul_apply`, `smul_val`, `spaceTime_deriv_action_eq_sum`, `toTensor_deriv_basis_repr_apply`	15
Total	23

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` 📖	CompData	10 math math: `ElectromagneticPotential.smul_apply`, `ElectromagneticPotential.add_val`, `ElectromagneticPotential.fieldStrengthMatrix_add`, `ElectromagneticPotential.gradKineticTerm_add`, `ElectromagneticPotential.gradKineticTerm_smul`, `ElectromagneticPotential.fieldStrengthMatrix_smul`, `ElectromagneticPotential.toFieldStrength_smul`, `ElectromagneticPotential.smul_val`, `ElectromagneticPotential.add_apply`, `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`	—	`SpaceTime.distTensorDeriv_apply` `Lorentz.Vector.instFiniteDimensionalReal`
`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`
`instAdd` 📖	CompOp	5 math math: `add_val`, `fieldStrengthMatrix_add`, `gradKineticTerm_add`, `add_apply`, `toFieldStrength_add`
`instCoeFunForallSpaceTimeVector` 📖	CompOp	—
`instSMulReal` 📖	CompOp	5 math math: `smul_apply`, `gradKineticTerm_smul`, `fieldStrengthMatrix_smul`, `toFieldStrength_smul`, `smul_val`
`val` 📖	CompOp	36 math math: `kineticTerm_eq_sum_potential`, `smul_apply`, `harmonicWaveX_inr_zero`, `freeCurrentPotential_hasVarGradientAt`, `harmonicWaveX_differentiable`, `gradKineticTerm_eq_sum_sum`, `add_val`, `kineticTerm_hasVarGradientAt`, `fieldStrengthMatrix_equivariant`, `canonicalMomentum_eq_gradient_kineticTerm`, `isExtrema_lorentzGroup_apply_iff`, `toTensor_toFieldStrength_basis_repr`, `spaceTime_deriv_action_eq_sum`, `deriv_basis_repr_apply`, `harmonicWaveX_inl_zero`, `magneticFieldMatrix_apply_x_boost_succ_succ`, `toTensor_deriv_basis_repr_apply`, `freeCurrentPotential_add_const`, `differentiable_component`, `lagrangian_hasVarGradientAt_eq_add_gradKineticTerm`, `smul_val`, `harmonicWaveX_contDiff`, `add_apply`, `toFieldStrength_basis_repr_apply_eq_single`, `electricField_apply_x_boost_zero`, `toFieldStrength_basis_repr_apply`, `kineticTerm_add_time_mul_const`, `lagrangian_hasVarGradientAt_gradLagrangian`, `lagrangian_add_const`, `deriv_equivariant`, `magneticFieldMatrix_apply_x_boost_zero_succ`, `kineticTerm_add_const`, `constantEB_smooth`, `electricField_apply_x_boost_succ`, `toFieldStrength_equivariant`, `kineticTerm_equivariant`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`val` `Electromagnetism.ElectromagneticPotential` `instAdd` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid`	—	—
`add_val` 📖	mathematical	—	`val` `Electromagnetism.ElectromagneticPotential` `instAdd` `SpaceTime` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid`	—	—
`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` `val`	—	`deriv.eq_1`
`deriv_equivariant` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector` `val`	`deriv` `LorentzGroup` `Lorentz.Vector` `TensorSpecies.Tensorial.smulAction` `realLorentzTensor.Color` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.tensorial` `val` `SpaceTime` `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` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `SpaceTime.instMeasureSpace` `Lorentz.Vector` `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` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector` `val`	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `val`	—	`SpaceTime.differentiable_vector`
`hasVarAdjDerivAt_component` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`HasVarAdjDerivAt` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `SpaceTime.instMeasureSpace` `Lorentz.Vector` `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`
`smul_apply` 📖	mathematical	—	`val` `Electromagnetism.ElectromagneticPotential` `instSMulReal` `Lorentz.Vector` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal`	—	—
`smul_val` 📖	mathematical	—	`val` `Electromagnetism.ElectromagneticPotential` `instSMulReal` `SpaceTime` `Lorentz.Vector` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal`	—	—
`spaceTime_deriv_action_eq_sum` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector` `val`	`SpaceTime.deriv` `Lorentz.Vector` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `LorentzGroup` `TensorSpecies.Tensorial.smulAction` `realLorentzTensor.Color` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.tensorial` `val` `SpaceTime`	—	`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` `val`	—	`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