TimeSlice

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

Statistics

Metric	Count
Definitions distTimeSlice, timeSlice, timeSliceLinearEquiv	3
Theorems distDeriv_inl_distTimeSlice_symm, distDeriv_inr_distTimeSlice_symm, distTimeSlice_apply, distTimeSlice_distDeriv_inl, distTimeSlice_distDeriv_inr, distTimeSlice_symm_apply, distTimeSlice_symm_distTimeDeriv_eq, timeSliceLinearEquiv_apply, timeSliceLinearEquiv_symm_apply, timeSlice_contDiff, timeSlice_differentiable	11
Total	14

SpaceTime

Definitions

Name	Category	Theorems
distTimeSlice 📖	CompOp	19 math math: distTimeSlice_distDeriv_inl, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, distTimeSlice_symm_apply, distTimeSlice_symm_distTimeDeriv_eq, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, distTimeSlice_apply, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, distTimeSlice_distDeriv_inr, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, distDeriv_inr_distTimeSlice_symm, distDeriv_inl_distTimeSlice_symm, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i
timeSlice 📖	CompOp	6 math math: timeSlice_differentiable, timeSliceLinearEquiv_symm_apply, timeSliceLinearEquiv_apply, Electromagnetism.LorentzCurrentDensity.currentDensity_eq_timeSlice, timeSlice_contDiff, Electromagnetism.LorentzCurrentDensity.chargeDensity_eq_timeSlice
timeSliceLinearEquiv 📖	CompOp	2 math math: timeSliceLinearEquiv_symm_apply, timeSliceLinearEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
distDeriv_inl_distTimeSlice_symm 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace distDeriv Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal distTimeSlice SpeedOfLight.val Space.distTimeDeriv	—	distTimeSlice_distDeriv_inl
distDeriv_inr_distTimeSlice_symm 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace distDeriv Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal distTimeSlice Space.distSpaceDeriv	—	distTimeSlice_distDeriv_inr
distTimeSlice_apply 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace distTimeSlice toTimeAndSpace	—	—
distTimeSlice_distDeriv_inl 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal distTimeSlice distDeriv SpeedOfLight.val Space.distTimeDeriv	—	distTimeSlice_apply Lorentz.Vector.instFiniteDimensionalReal distDeriv_apply Distribution.fderivD_apply Time.instFiniteDimensionalReal Space.instFiniteDimensionalReal Space.distTimeDeriv_apply toTimeAndSpace_fderiv toTimeAndSpace_basis_inl'
distTimeSlice_distDeriv_inr 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal distTimeSlice distDeriv Space.distSpaceDeriv	—	distTimeSlice_apply Lorentz.Vector.instFiniteDimensionalReal distDeriv_apply Distribution.fderivD_apply Time.instFiniteDimensionalReal Space.instFiniteDimensionalReal Space.distSpaceDeriv_apply toTimeAndSpace_fderiv toTimeAndSpace_basis_inr
distTimeSlice_symm_apply 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal distTimeSlice Lorentz.Vector.instAddCommMonoid Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.instModuleReal Time.instModuleReal Space.instModuleReal toTimeAndSpace	—	—
distTimeSlice_symm_distTimeDeriv_eq 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace distTimeSlice Space.distTimeDeriv SpeedOfLight.val distDeriv	—	distDeriv_inl_distTimeSlice_symm
timeSliceLinearEquiv_apply 📖	mathematical	—	SpaceTime Time Space timeSliceLinearEquiv timeSlice	—	—
timeSliceLinearEquiv_symm_apply 📖	mathematical	—	Time Space SpaceTime timeSliceLinearEquiv timeSlice	—	—
timeSlice_contDiff 📖	mathematical	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace	Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal timeSlice	—	—
timeSlice_differentiable 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup	Time Space Time.instAddCommGroup Space.instAddCommGroup Time.instSeminormedAddCommGroup Time.instNormedAddCommGroup Space.instAddCommMonoid Time.instModuleReal Space.instModuleReal Space.instSeminormedAddCommGroup timeSlice	—	—

---

← Back to Index