Basic

📁 Source: PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean

Statistics

Metric	Count
Definitions deriv, distDeriv, «term∂[_]»	3
Theorems deriv_add, deriv_commute, deriv_component, deriv_component_diff, deriv_component_same, deriv_component_sq, deriv_const, deriv_coord_add, deriv_coord_smul, deriv_differentiable, deriv_eq, deriv_eq_fderiv_basis, deriv_eq_inner_self, deriv_euclid, deriv_inner_left, deriv_inner_right, deriv_lorentz_vector, deriv_norm_sq, deriv_smul, distDeriv_apply, distDeriv_commute, fderiv_eq_sum_deriv, inner_apply_contDiff, inner_apply_differentiable, inner_apply_differentiableAt, inner_contDiff, inner_differentiable, inner_differentiableAt, norm_sq_differentiable, schwartMap_fderiv_comm	30
Total	33

Space

Definitions

Name	Category	Theorems
deriv 📖	CompOp	67 math math: Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_space_deriv_same, deriv_lorentz_vector, IsDistBounded.normPowerSeries_deriv, time_deriv_comm_space_deriv, Electromagnetism.ElectromagneticPotential.time_deriv_magneticFieldMatrix, SpaceTime.deriv_sum_inr, Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_space_deriv_succ, Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_space_deriv_succ, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_space_deriv_eq, deriv_normPowerSeries_tendsto, grad_apply, space_deriv_differentiable_time, deriv_commute, deriv_inner_right, deriv_eq_fderiv_basis, Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic, inner_grad_eq, grad_eq_sum, deriv_coord_2nd_add, Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_magneticFieldMatrix, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField, deriv_coord_add, deriv_add, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv_eq_time_deriv, Electromagnetism.ElectromagneticPotential.IsPlaneWave.space_deriv_electricField_eq_magneticFieldMatrix, fderiv_eq_sum_deriv, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_space_deriv, Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_magneticFieldMatrix_of_isExtrema, deriv_normPowerSeries, ClassicalMechanics.planeWave_space_deriv_space_deriv, deriv_eq, deriv_component, deriv_normPowerSeries_zpow, Electromagnetism.ElectromagneticPotential.time_deriv_comp_vectorPotential_eq_electricField, deriv_differentiable, Electromagnetism.ElectromagneticPotential.constantEB_vectorPotential_space_deriv, ClassicalMechanics.planeWave_space_deriv, deriv_inner_left, deriv_euclid, QuantumMechanics.momentumOperator_apply, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv, ClassicalMechanics.planeWave_apply_space_deriv, deriv_smul, Electromagnetism.ElectromagneticPotential.IsPlaneWave.space_deriv_magneticFieldMatrix_eq_electricField_mul_propogator, gradient_eq_sum, QuantumMechanics.momentumOperator_apply_fun, deriv_component_diff, grad_inner_single, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, Electromagnetism.ElectromagneticPotential.magneticField_curl_eq_magneticFieldMatrix, ClassicalMechanics.planeWave_apply_space_deriv_space_deriv, deriv_const, Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ_space_deriv_zero, deriv_component_same, Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_electricField_of_isExtrema, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_space_deriv_eq_time_deriv, deriv_log_normPowerSeries, Electromagnetism.ElectromagneticPotential.isExtrema_iff_gauss_ampere_magneticFieldMatrix, Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_zero_succ_space_deriv_zero, deriv_coord_2nd_sub, deriv_eq_inner_self, grad_inner_eq, deriv_coord_smul, deriv_component_sq, Electromagnetism.ElectromagneticPotential.time_deriv_electricField_of_isExtrema, deriv_norm_sq
distDeriv 📖	CompOp	9 math math: distDeriv_distConst, distGrad_apply, distDeriv_constantSliceDist_same, distDeriv_constantSliceDist_succAbove, distDeriv_apply, distDiv_apply_eq_sum_distDeriv, constantTime_distSpaceDeriv, distDeriv_commute, distGrad_toFun_eq_distDeriv
«term∂[_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv_add 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup	deriv	—	—
deriv_commute 📖	mathematical	Space instNormedAddCommGroup instInnerProductSpaceReal	deriv	—	—
deriv_component 📖	mathematical	—	deriv val	—	deriv_component_same deriv_component_diff
deriv_component_diff 📖	mathematical	—	deriv val	—	coord_apply deriv_eq inner_basis basis_apply
deriv_component_same 📖	mathematical	—	deriv val	—	coord_apply deriv_eq inner_basis basis_self
deriv_component_sq 📖	mathematical	—	deriv val	—	deriv_eq_fderiv_basis eval_differentiable deriv_component
deriv_const 📖	mathematical	—	deriv	—	deriv.eq_1
deriv_coord_add 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup	deriv	—	—
deriv_coord_smul 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup	deriv	—	—
deriv_differentiable 📖	mathematical	Space instNormedAddCommGroup instInnerProductSpaceReal	instAddCommGroup instModuleReal instSeminormedAddCommGroup deriv	—	—
deriv_eq 📖	mathematical	—	deriv Space instSeminormedAddCommGroup instAddCommGroup instModuleReal instNormedAddCommGroup instInnerProductSpaceReal basis	—	—
deriv_eq_fderiv_basis 📖	mathematical	—	deriv Space instSeminormedAddCommGroup instAddCommGroup instModuleReal instNormedAddCommGroup instInnerProductSpaceReal basis	—	—
deriv_eq_inner_self 📖	mathematical	—	deriv Space instInnerReal val	—	deriv_norm_sq
deriv_euclid 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup	deriv	—	deriv_eq_fderiv_basis
deriv_inner_left 📖	mathematical	—	deriv Space instInnerReal val	—	deriv_eq_fderiv_basis basis_inner
deriv_inner_right 📖	mathematical	—	deriv Space instInnerReal val	—	deriv_eq_fderiv_basis inner_basis
deriv_lorentz_vector 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup Lorentz.Vector Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup	deriv	—	deriv_eq_fderiv_basis
deriv_norm_sq 📖	mathematical	—	deriv Space instNorm val	—	norm_sq_eq deriv_eq_fderiv_basis eval_differentiable deriv_component_sq
deriv_smul 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup	deriv	—	—
distDeriv_apply 📖	mathematical	—	Distribution Space instNormedAddCommGroup instInnerProductSpaceReal distDeriv Distribution.fderivD instFiniteDimensionalReal basis	—	instFiniteDimensionalReal
distDeriv_commute 📖	mathematical	—	Distribution Space instNormedAddCommGroup instInnerProductSpaceReal distDeriv	—	instFiniteDimensionalReal schwartMap_fderiv_comm
fderiv_eq_sum_deriv 📖	mathematical	—	Space instSeminormedAddCommGroup instAddCommGroup instModuleReal val deriv	—	deriv_eq_fderiv_basis
inner_apply_contDiff 📖	mathematical	Space instNormedAddCommGroup instInnerProductSpaceReal	instInnerReal	—	—
inner_apply_differentiable 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup	instInnerReal	—	—
inner_apply_differentiableAt 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup	instInnerReal	—	—
inner_contDiff 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal instInnerReal	—	—
inner_differentiable 📖	mathematical	—	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup instInnerReal	—	norm_sq_differentiable
inner_differentiableAt 📖	mathematical	—	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup instInnerReal	—	inner_differentiable
norm_sq_differentiable 📖	mathematical	—	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup instNorm	—	norm_sq_eq eval_differentiable
schwartMap_fderiv_comm 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal basis	—	—

---

← Back to Index