Derivatives

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

Statistics

Metric	Count
Definitions deriv, distDeriv, distTensorDeriv, tensorDeriv, «term∂_»	5
Theorems apply_fderiv_eq_distDeriv, contDiff_vector, deriv_apply_eq, deriv_comp_lorentz_action, deriv_coord, deriv_eq, deriv_equivariant, deriv_sum_inl, deriv_sum_inr, deriv_zero, differentiable_vector, distDeriv_apply, distDeriv_apply', distDeriv_commute, distDeriv_comp_lorentz_action, distTensorDeriv_apply, distTensorDeriv_equivariant, distTensorDeriv_toTensor_basis_repr, fderiv_vector, tensorDeriv_equivariant, tensorDeriv_toTensor_basis_repr	21
Total	26

SpaceTime

Definitions

Name	Category	Theorems
deriv 📖	CompOp	25 math math: Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum_potential, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_sum_fieldStrengthMatrix, deriv_coord, deriv_zero, deriv_sum_inr, deriv_eq, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_fieldStrength, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_sum_sum, tensorDeriv_toTensor_basis_repr, deriv_sum_inl, Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.div_electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.deriv_hasVarAdjDerivAt, deriv_equivariant, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr, deriv_comp_lorentz_action, Electromagnetism.ElectromagneticPotential.spaceTime_deriv_action_eq_sum, Electromagnetism.ElectromagneticPotential.deriv_basis_repr_apply, Electromagnetism.ElectromagneticPotential.isExtrema_iff_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply, deriv_apply_eq, Electromagnetism.ElectromagneticPotential.time_deriv_electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply_eq_single, Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply, Electromagnetism.ElectromagneticPotential.kineticTerm_add_time_mul_const
distDeriv 📖	CompOp	24 math math: distTimeSlice_distDeriv_inl, distDeriv_apply', distTensorDeriv_toTensor_basis_repr, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_sum_sum, Electromagnetism.DistElectromagneticPotential.distDeriv_fieldStrength_diag_zero, distDeriv_comp_lorentz_action, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, distTimeSlice_symm_distTimeDeriv_eq, distDeriv_commute, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply_eq_single, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, distTimeSlice_distDeriv_inr, Electromagnetism.DistElectromagneticPotential.fieldStrength_basis_repr_eq_single, distDeriv_apply, apply_fderiv_eq_distDeriv, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_basis, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, distDeriv_inr_distTimeSlice_symm, distDeriv_inl_distTimeSlice_symm, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_basis, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_fieldStrength, distTensorDeriv_apply, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr
distTensorDeriv 📖	CompOp	6 math math: distTensorDeriv_toTensor_basis_repr, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, distTensorDeriv_equivariant, distTensorDeriv_apply
tensorDeriv 📖	CompOp	5 math math: tensorDeriv_toTensor_basis_repr, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor, tensorDeriv_equivariant, Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv
«term∂_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_fderiv_eq_distDeriv 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.basis distDeriv	—	distDeriv_apply'
contDiff_vector 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector	—	—
deriv_apply_eq 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	deriv Lorentz.Vector Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup SpaceTime Lorentz.Vector.instAddCommMonoid Lorentz.Vector.basis	—	deriv_eq
deriv_comp_lorentz_action 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup	deriv LorentzGroup SpaceTime TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.tensorial	—	Lorentz.Vector.smul_basis
deriv_coord 📖	mathematical	—	deriv SpaceTime	—	deriv_eq Lorentz.Vector.basis_apply
deriv_eq 📖	mathematical	—	deriv SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector Lorentz.Vector.instAddCommMonoid Lorentz.Vector.basis	—	—
deriv_equivariant 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup	deriv LorentzGroup TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor SpaceTime realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.tensorial	—	deriv_eq deriv_comp_lorentz_action
deriv_sum_inl 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup	deriv SpeedOfLight.val Time.deriv Time Space Time.instSeminormedAddCommGroup Space.instPseudoMetricSpace Time.instNormedAddCommGroup Space.instAddCommMonoid SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Time.instModuleReal Space.instModuleReal Lorentz.Vector.instModuleReal toTimeAndSpace	—	deriv_eq Time.deriv_eq toTimeAndSpace_symm_fderiv toTimeAndSpace_basis_inl'
deriv_sum_inr 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup	deriv Space.deriv Time Space Time.instSeminormedAddCommGroup Space.instPseudoMetricSpace Time.instNormedAddCommGroup Space.instAddCommMonoid SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Time.instModuleReal Space.instModuleReal Lorentz.Vector.instModuleReal toTimeAndSpace	—	deriv_eq Space.deriv_eq toTimeAndSpace_symm_fderiv toTimeAndSpace_basis_inr
deriv_zero 📖	mathematical	—	deriv SpaceTime	—	deriv_eq
differentiable_vector 📖	mathematical	—	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	—	—
distDeriv_apply 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace distDeriv Distribution.fderivD Lorentz.Vector.instFiniteDimensionalReal Lorentz.Vector Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.basis	—	Lorentz.Vector.instFiniteDimensionalReal
distDeriv_apply' 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace distDeriv Lorentz.Vector Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.basis	—	Lorentz.Vector.instFiniteDimensionalReal distDeriv_apply
distDeriv_commute 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace distDeriv	—	Lorentz.Vector.instFiniteDimensionalReal distDeriv_apply Distribution.fderivD_apply
distDeriv_comp_lorentz_action 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace distDeriv LorentzGroup instSMulElemMatrixSumFinOfNatNatRealLorentzGroupDistribution lorentzGroupIsGroup	—	instSMulCommClassRealElemMatrixSumFinOfNatNatLorentzGroupDistribution lorentzGroup_smul_dist_apply Lorentz.Vector.instFiniteDimensionalReal distDeriv_apply Distribution.fderivD_apply schwartzAction_surjective schwartzAction_mul_apply deriv_comp_lorentz_action
distTensorDeriv_apply 📖	mathematical	—	Distribution SpaceTime Lorentz.CoVector Lorentz.CoVector.instAddCommMonoid Lorentz.CoVector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.CoVector.isNormedAddCommGroup Lorentz.CoVector.innerProductSpace Lorentz.Vector.isNormedSpace distTensorDeriv Lorentz.CoVector.basis distDeriv	—	—
distTensorDeriv_equivariant 📖	mathematical	—	Distribution SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.CoVector Lorentz.CoVector.instAddCommMonoid Lorentz.CoVector.instModuleReal Lorentz.CoVector.isNormedAddCommGroup Lorentz.CoVector.innerProductSpace distTensorDeriv LorentzGroup instSMulElemMatrixSumFinOfNatNatRealLorentzGroupDistribution realLorentzTensor.Color realLorentzTensor.Color.down TensorSpecies.Tensorial.prod lorentzGroupIsGroup realLorentzTensor Lorentz.CoVector.tensorial	—	distTensorDeriv_apply distDeriv_comp_lorentz_action lorentzGroup_smul_dist_apply Lorentz.CoVector.smul_basis TensorSpecies.Tensorial.smul_prod
distTensorDeriv_toTensor_basis_repr 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.basis Lorentz.CoVector Lorentz.CoVector.instAddCommMonoid Lorentz.CoVector.instModuleReal TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.prod Lorentz.CoVector.tensorial Distribution SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.CoVector.isNormedAddCommGroup Lorentz.CoVector.innerProductSpace Lorentz.Vector.isNormedSpace distTensorDeriv distDeriv Lorentz.CoVector.indexEquiv TensorSpecies.Tensor.ComponentIdx.prodEquiv	—	TensorSpecies.Tensorial.toTensor_tprod TensorSpecies.Tensor.prodT_basis_repr_apply Lorentz.CoVector.toTensor_basis_eq_tensor_basis
fderiv_vector 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommGroup Lorentz.Vector Lorentz.Vector.instModuleReal	—	—
tensorDeriv_equivariant 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup	tensorDeriv LorentzGroup TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor SpaceTime realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.tensorial Lorentz.CoVector Lorentz.CoVector.instAddCommMonoid Lorentz.CoVector.instModuleReal realLorentzTensor.Color.down TensorSpecies.Tensorial.prod Lorentz.CoVector.tensorial	—	deriv_equivariant Lorentz.CoVector.smul_basis TensorSpecies.Tensorial.smul_prod
tensorDeriv_toTensor_basis_repr 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup	TensorSpecies.Tensor.ComponentIdx realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.down TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.basis Lorentz.CoVector Lorentz.CoVector.instAddCommMonoid Lorentz.CoVector.instModuleReal TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.prod Lorentz.CoVector.tensorial tensorDeriv deriv Lorentz.CoVector.indexEquiv TensorSpecies.Tensor.ComponentIdx.prodEquiv	—	TensorSpecies.Tensorial.toTensor_tprod TensorSpecies.Tensor.prodT_basis_repr_apply Lorentz.CoVector.toTensor_basis_eq_tensor_basis deriv_eq

---

← Back to Index