Basic

📁 Source: PhysLean/SpaceAndTime/TimeAndSpace/Basic.lean

Statistics

Metric	Count
Definitions `distSpaceCurl`, `distSpaceDeriv`, `distSpaceDiv`, `distSpaceGrad`, `distTimeDeriv`	5
Theorems `apply_fderiv_eq_distSpaceDeriv`, `apply_fderiv_eq_distTimeDeriv`, `const_of_time_deriv_space_deriv_eq_zero`, `curl_differentiable_time`, `distSpaceDeriv_apply`, `distSpaceDeriv_apply'`, `distSpaceDeriv_apply_CLM`, `distSpaceDeriv_commute`, `distSpaceDiv_apply_eq_sum_distSpaceDeriv`, `distSpaceGrad_apply`, `distTimeDeriv_apply`, `distTimeDeriv_apply'`, `distTimeDeriv_apply_CLM`, `distTimeDeriv_commute_distSpaceDeriv`, `equal_up_to_const_of_deriv_eq`, `fderiv_space_eq_fderiv_curry`, `fderiv_time_commute_fderiv_space`, `fderiv_time_eq_fderiv_curry`, `space_deriv_differentiable_time`, `space_fun_of_time_deriv_eq_zero`, `time_deriv_comm_space_deriv`, `time_deriv_curl_commute`, `time_deriv_differentiable_space`, `time_fun_of_space_deriv_eq_zero`	24
Total	29

Space

Definitions

Name	Category	Theorems
`distSpaceCurl` 📖	CompOp	1 math math: `constantTime_spaceCurlD`
`distSpaceDeriv` 📖	CompOp	19 math math: `Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i`, `distSpaceDeriv_apply`, `distSpaceDeriv_apply'`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time`, `Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq`, `SpaceTime.distTimeSlice_distDeriv_inr`, `Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential`, `Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential`, `distSpaceGrad_apply`, `constantTime_distSpaceDeriv`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0`, `distSpaceDiv_apply_eq_sum_distSpaceDeriv`, `distSpaceDeriv_commute`, `SpaceTime.distDeriv_inr_distTimeSlice_symm`, `distTimeDeriv_commute_distSpaceDeriv`, `apply_fderiv_eq_distSpaceDeriv`, `distSpaceDeriv_apply_CLM`
`distSpaceDiv` 📖	CompOp	8 math math: `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time`, `constantTime_distSpaceDiv`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0`, `distSpaceDiv_apply_eq_sum_distSpaceDeriv`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField`
`distSpaceGrad` 📖	CompOp	2 math math: `distSpaceGrad_apply`, `constantTime_distSpaceGrad`
`distTimeDeriv` 📖	CompOp	16 math math: `SpaceTime.distTimeSlice_distDeriv_inl`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i`, `distTimeDeriv_apply'`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time`, `SpaceTime.distTimeSlice_symm_distTimeDeriv_eq`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq`, `distTimeDeriv_apply_CLM`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential`, `distTimeDeriv_apply`, `apply_fderiv_eq_distTimeDeriv`, `SpaceTime.distDeriv_inl_distTimeSlice_symm`, `distTimeDeriv_commute_distSpaceDeriv`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv`, `constantTime_distTimeDeriv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_fderiv_eq_distSpaceDeriv` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal` `Time.instOfNat` `basis` `distSpaceDeriv`	—	`distSpaceDeriv_apply'`
`apply_fderiv_eq_distTimeDeriv` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal` `Time.instOfNat` `instZero` `distTimeDeriv`	—	`distTimeDeriv_apply'`
`const_of_time_deriv_space_deriv_eq_zero` 📖	—	`Time` `Space` `Time.instAddCommGroup` `instAddCommGroup` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `instAddCommMonoid` `Time.instModuleReal` `instModuleReal` `instSeminormedAddCommGroup` `Time.deriv` `deriv`	—	—	`space_fun_of_time_deriv_eq_zero` `time_fun_of_space_deriv_eq_zero`
`curl_differentiable_time` 📖	mathematical	`Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal`	`Time.instAddCommGroup` `Time.instModuleReal` `Time.instSeminormedAddCommGroup` `curl`	—	`space_deriv_differentiable_time`
`distSpaceDeriv_apply` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal` `distSpaceDeriv` `Distribution.fderivD` `Time.instSeminormedAddCommGroup` `instAddCommMonoid` `Time.instFiniteDimensionalReal` `instFiniteDimensionalReal` `Time.instOfNat` `basis`	—	—
`distSpaceDeriv_apply'` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal` `distSpaceDeriv` `Time.instOfNat` `basis`	—	`Time.instFiniteDimensionalReal` `instFiniteDimensionalReal` `distSpaceDeriv_apply` `Distribution.fderivD_apply`
`distSpaceDeriv_apply_CLM` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal` `distSpaceDeriv`	—	`Time.instFiniteDimensionalReal` `instFiniteDimensionalReal` `distSpaceDeriv_apply` `Distribution.fderivD_apply`
`distSpaceDeriv_commute` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal` `distSpaceDeriv`	—	`Time.instFiniteDimensionalReal` `instFiniteDimensionalReal` `distSpaceDeriv_apply` `Distribution.fderivD_apply`
`distSpaceDiv_apply_eq_sum_distSpaceDeriv` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal` `distSpaceDiv` `distSpaceDeriv`	—	—
`distSpaceGrad_apply` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal` `distSpaceGrad` `distSpaceDeriv`	—	—
`distTimeDeriv_apply` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal` `distTimeDeriv` `Distribution.fderivD` `Time.instSeminormedAddCommGroup` `instAddCommMonoid` `Time.instFiniteDimensionalReal` `instFiniteDimensionalReal` `Time.instOfNat` `instZero`	—	—
`distTimeDeriv_apply'` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal` `distTimeDeriv` `Time.instOfNat` `instZero`	—	`Time.instFiniteDimensionalReal` `instFiniteDimensionalReal` `distTimeDeriv_apply` `Distribution.fderivD_apply`
`distTimeDeriv_apply_CLM` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal` `distTimeDeriv`	—	`Time.instFiniteDimensionalReal` `instFiniteDimensionalReal` `distTimeDeriv_apply` `Distribution.fderivD_apply`
`distTimeDeriv_commute_distSpaceDeriv` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal` `distTimeDeriv` `distSpaceDeriv`	—	`Time.instFiniteDimensionalReal` `instFiniteDimensionalReal` `distTimeDeriv_apply` `distSpaceDeriv_apply` `Distribution.fderivD_apply`
`equal_up_to_const_of_deriv_eq` 📖	—	`Time` `Space` `Time.instAddCommGroup` `instAddCommGroup` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `instAddCommMonoid` `Time.instModuleReal` `instModuleReal` `instSeminormedAddCommGroup` `Time.deriv` `deriv`	—	—	`const_of_time_deriv_space_deriv_eq_zero` `Time.deriv_eq` `deriv_eq_fderiv_basis`
`fderiv_space_eq_fderiv_curry` 📖	mathematical	`Time` `Space` `Time.instAddCommGroup` `instAddCommGroup` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `instAddCommMonoid` `Time.instModuleReal` `instModuleReal` `instSeminormedAddCommGroup`	`Time.instOfNat`	—	—
`fderiv_time_commute_fderiv_space` 📖	mathematical	`Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal`	`Time.instSeminormedAddCommGroup` `Time.instAddCommGroup` `Time.instModuleReal` `instSeminormedAddCommGroup` `instAddCommGroup` `instModuleReal`	—	`fderiv_space_eq_fderiv_curry` `fderiv_time_eq_fderiv_curry`
`fderiv_time_eq_fderiv_curry` 📖	mathematical	`Time` `Space` `Time.instAddCommGroup` `instAddCommGroup` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `instAddCommMonoid` `Time.instModuleReal` `instModuleReal` `instSeminormedAddCommGroup`	`instZero`	—	—
`space_deriv_differentiable_time` 📖	mathematical	`Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal`	`Time.instAddCommGroup` `Time.instModuleReal` `Time.instSeminormedAddCommGroup` `deriv`	—	`deriv_eq_fderiv_basis` `fderiv_space_eq_fderiv_curry`
`space_fun_of_time_deriv_eq_zero` 📖	—	`Time` `Space` `Time.instAddCommGroup` `instAddCommGroup` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `instAddCommMonoid` `Time.instModuleReal` `instModuleReal` `instSeminormedAddCommGroup` `Time.deriv`	—	—	`Time.ext` `Time.one_val`
`time_deriv_comm_space_deriv` 📖	mathematical	`Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal`	`Time.deriv` `deriv`	—	`deriv_eq_fderiv_basis` `fderiv_time_commute_fderiv_space`
`time_deriv_curl_commute` 📖	mathematical	`Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal`	`Time.deriv` `curl`	—	`Time.deriv_euclid` `curl_differentiable_time` `Time.deriv_eq` `space_deriv_differentiable_time` `time_deriv_comm_space_deriv`
`time_deriv_differentiable_space` 📖	mathematical	`Time` `Space` `Time.instNormedAddCommGroup` `instNormedAddCommGroup` `Time.instNormedSpaceReal` `instInnerProductSpaceReal`	`instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup` `Time.deriv`	—	`Time.deriv_eq` `fderiv_time_eq_fderiv_curry`
`time_fun_of_space_deriv_eq_zero` 📖	—	`Time` `Space` `Time.instAddCommGroup` `instAddCommGroup` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `instAddCommMonoid` `Time.instModuleReal` `instModuleReal` `instSeminormedAddCommGroup` `deriv`	—	—	`deriv_eq_fderiv_basis`

---

← Back to Index