Derivatives

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

Statistics

Metric	Count
Definitions `deriv`, `distDeriv`, `distTensorDeriv`, `tensorDeriv`, `«term∂_»`	5
Theorems `sum_apply`, `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`	22
Total	27

SchwartzMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_apply` 📖	—	—	—	—	—

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.instAddCommMonoid` `Lorentz.Vector.basis`	—	`deriv_eq`
`deriv_comp_lorentz_action` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup`	`deriv` `LorentzGroup` `TensorSpecies.Tensorial.smulAction` `realLorentzTensor.Color` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `Lorentz.Vector.instAddCommMonoid` `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` `realLorentzTensor.Color.up` `Lorentz.Vector.instAddCommMonoid` `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.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Time.instModuleReal` `Space.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.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Time.instModuleReal` `Space.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` `SchwartzMap.sum_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` 📖	—	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	—	—	—
`tensorDeriv_equivariant` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup`	`tensorDeriv` `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`	—	`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