Documentation Verification Report

LorentzAction

📁 Source: PhysLean/SpaceAndTime/SpaceTime/LorentzAction.lean

Statistics

Metric	Count
Definitions `distActionLinearMap`, `instDistribMulActionElemMatrixSumFinOfNatNatRealLorentzGroupDistribution`, `instSMulElemMatrixSumFinOfNatNatRealLorentzGroupDistribution`, `schwartzAction`	4
Theorems `instSMulCommClassRealElemMatrixSumFinOfNatNatLorentzGroupDistribution`, `lorentzGroup_smul_dist_apply`, `schwartzAction_apply`, `schwartzAction_injective`, `schwartzAction_mul_apply`, `schwartzAction_surjective`	6
Total	10

SpaceTime

Definitions

Name	Category	Theorems
`distActionLinearMap` 📖	CompOp	—
`instDistribMulActionElemMatrixSumFinOfNatNatRealLorentzGroupDistribution` 📖	CompOp	—
`instSMulElemMatrixSumFinOfNatNatRealLorentzGroupDistribution` 📖	CompOp	7 math math: `distDeriv_comp_lorentz_action`, `distTensorDeriv_equivariant`, `instSMulCommClassRealElemMatrixSumFinOfNatNatLorentzGroupDistribution`, `Electromagnetism.DistElectromagneticPotential.isExterma_equivariant`, `Electromagnetism.DistElectromagneticPotential.deriv_equivariant`, `Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant`, `lorentzGroup_smul_dist_apply`
`schwartzAction` 📖	CompOp	5 math math: `schwartzAction_surjective`, `schwartzAction_apply`, `schwartzAction_mul_apply`, `lorentzGroup_smul_dist_apply`, `schwartzAction_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instSMulCommClassRealElemMatrixSumFinOfNatNatLorentzGroupDistribution` 📖	mathematical	—	`LorentzGroup` `Distribution` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `instSMulElemMatrixSumFinOfNatNatRealLorentzGroupDistribution`	—	`TensorSpecies.Tensorial.instSMulCommClass`
`lorentzGroup_smul_dist_apply` 📖	mathematical	—	`Distribution` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `LorentzGroup` `instSMulElemMatrixSumFinOfNatNatRealLorentzGroupDistribution` `TensorSpecies.Tensorial.smulAction` `realLorentzTensor.Color` `lorentzGroupIsGroup` `realLorentzTensor` `schwartzAction`	—	—
`schwartzAction_apply` 📖	mathematical	—	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `LorentzGroup` `lorentzGroupIsGroup` `schwartzAction` `TensorSpecies.Tensorial.smulAction` `realLorentzTensor.Color` `realLorentzTensor` `realLorentzTensor.Color.up` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.tensorial`	—	—
`schwartzAction_injective` 📖	mathematical	—	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `LorentzGroup` `lorentzGroupIsGroup` `schwartzAction`	—	—
`schwartzAction_mul_apply` 📖	mathematical	—	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `LorentzGroup` `lorentzGroupIsGroup` `schwartzAction`	—	—
`schwartzAction_surjective` 📖	mathematical	—	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `LorentzGroup` `lorentzGroupIsGroup` `schwartzAction`	—	—

---

← Back to Index