Grad

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

Statistics

Metric	Count
Definitions distGrad, grad, «term∇»	3
Theorems distGrad_apply, distGrad_eq_of_inner, distGrad_eq_sum_basis, distGrad_inner_eq, distGrad_toFun_eq_distDeriv, euclid_gradient_eq_sum, grad_add, grad_apply, grad_const, grad_eq_gradiant, grad_eq_sum, grad_inner, grad_inner_eq, grad_inner_left, grad_inner_repr_eq, grad_inner_right, grad_inner_single, grad_inner_space, grad_inner_space_unit_vector, grad_neg, grad_norm_sq, grad_smul, grad_zero, gradient_eq_grad, gradient_eq_sum, inner_grad_eq, integrable_isDistBounded_inner_grad_schwartzMap, integrable_isDistBounded_inner_grad_schwartzMap_spherical, repr_grad_inner_eq	29
Total	32

Space

Definitions

Name	Category	Theorems
distGrad 📖	CompOp	17 math math: gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm, gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm, distGrad_inner_eq, distGrad_distConst, gradient_dist_normPowerSeries_log, gradient_dist_normPowerSeries_zpow_tendsTo, distGrad_apply, gradient_dist_normPowerSeries_zpow, distTranslate_distGrad, distGrad_distOfFunction_log_norm, distGrad_distOfFunction_norm_zpow, distGrad_eq_sum_basis, distGrad_eq_of_inner, distGrad_toFun_eq_distDeriv, gradient_dist_normPowerSeries_log_tendsTo, constantTime_distSpaceGrad, distCurl_distGrad_eq_zero
grad 📖	CompOp	34 math math: Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField, grad_zero, integrable_isDistBounded_inner_grad_schwartzMap_spherical, HasVarAdjoint.grad, grad_apply, grad_norm_sq, Electromagnetism.ElectromagneticPotential.electricField_eq, inner_grad_eq, grad_eq_sum, repr_grad_inner_eq, grad_add, gradient_eq_grad, distDiv_ofFunction, grad_inner_space_unit_vector, grad_eq_gradiant, grad_inner_repr_eq, laplacian_eq_div_of_grad, HasVarAdjoint.div, grad_neg, integrable_isDistBounded_inner_grad_schwartzMap, grad_const, Electromagnetism.ElectromagneticPotential.time_deriv_vectorPotential_eq_electricField, grad_inner_single, grad_inner_right, grad_smul, HasVarAdjDerivAt.grad, IsLocalizedFunctionTransform.grad, grad_inner, curl_of_curl, grad_inner_space, grad_inner_eq, HasVarAdjDerivAt.div, grad_inner_left
«term∇» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
distGrad_apply 📖	mathematical	—	Distribution Space instNormedAddCommGroup instInnerProductSpaceReal distGrad distDeriv	—	distGrad_toFun_eq_distDeriv
distGrad_eq_of_inner 📖	mathematical	Space instNormedAddCommGroup instInnerProductSpaceReal Distribution Distribution.fderivD instFiniteDimensionalReal basis	distGrad	—	instFiniteDimensionalReal distGrad_inner_eq
distGrad_eq_sum_basis 📖	mathematical	—	Distribution Space instNormedAddCommGroup instInnerProductSpaceReal distGrad basis	—	instFiniteDimensionalReal Distribution.fderivD_apply distGrad_inner_eq
distGrad_inner_eq 📖	mathematical	—	Distribution Space instNormedAddCommGroup instInnerProductSpaceReal distGrad Distribution.fderivD instFiniteDimensionalReal basis	—	instFiniteDimensionalReal distGrad.eq_1 basis_repr_inner_eq
distGrad_toFun_eq_distDeriv 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal Distribution distGrad distDeriv	—	distGrad_eq_sum_basis
euclid_gradient_eq_sum 📖	—	—	—	—	—
grad_add 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup	grad	—	deriv_add
grad_apply 📖	mathematical	—	grad deriv	—	grad_eq_sum
grad_const 📖	mathematical	—	grad Space	—	—
grad_eq_gradiant 📖	mathematical	—	grad Space instNormedAddCommGroup instInnerProductSpaceReal basis instSeminormedAddCommGroup instFiniteDimensionalReal	—	instFiniteDimensionalReal basis_repr_inner_eq fderiv_eq_sum_deriv basis_repr_symm_apply grad_inner_eq
grad_eq_sum 📖	mathematical	—	grad deriv	—	deriv_eq
grad_inner 📖	mathematical	—	grad Space instInnerReal instNormedAddCommGroup instInnerProductSpaceReal basis	—	basis_repr_apply deriv.eq_1 inner_basis
grad_inner_eq 📖	mathematical	—	grad deriv	—	grad_inner_single
grad_inner_left 📖	mathematical	—	grad Space instInnerReal instNormedAddCommGroup instInnerProductSpaceReal basis	—	deriv_inner_left basis_repr_apply
grad_inner_repr_eq 📖	mathematical	—	grad Space instNormedAddCommGroup instInnerProductSpaceReal basis instSeminormedAddCommGroup instAddCommGroup instModuleReal	—	grad_inner_eq fderiv_eq_sum_deriv basis_repr_apply
grad_inner_right 📖	mathematical	—	grad Space instInnerReal instNormedAddCommGroup instInnerProductSpaceReal basis	—	grad_inner_left
grad_inner_single 📖	mathematical	—	grad deriv	—	—
grad_inner_space 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup	grad instNormedAddCommGroup instInnerProductSpaceReal basis instNorm instSMulReal	—	grad_inner_space_unit_vector
grad_inner_space_unit_vector 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup	grad instNorm instNormedAddCommGroup instInnerProductSpaceReal basis instSMulReal	—	grad_inner_eq fderiv_eq_sum_deriv basis_repr_apply
grad_neg 📖	mathematical	—	grad Space	—	deriv_eq
grad_norm_sq 📖	mathematical	—	grad Space instNorm instNormedAddCommGroup instInnerProductSpaceReal basis	—	grad_eq_sum inner_basis basis_repr_apply
grad_smul 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup	grad	—	deriv_smul
grad_zero 📖	mathematical	—	grad Space	—	—
gradient_eq_grad 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal instSeminormedAddCommGroup instFiniteDimensionalReal basis grad	—	instFiniteDimensionalReal grad_eq_gradiant eq_of_apply
gradient_eq_sum 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal instSeminormedAddCommGroup instFiniteDimensionalReal instAddCommMonoid instSMulReal deriv basis	—	instFiniteDimensionalReal gradient_eq_grad grad_eq_sum
inner_grad_eq 📖	mathematical	—	grad deriv	—	grad_inner_eq
integrable_isDistBounded_inner_grad_schwartzMap 📖	mathematical	IsDistBounded	Space instNormedAddCommGroup instInnerProductSpaceReal instFiniteDimensionalReal instMeasurableSpace instBorelSpace grad	—	instFiniteDimensionalReal instBorelSpace grad_eq_sum IsDistBounded.integrable_space IsDistBounded.pi_comp deriv_eq_fderiv_basis
integrable_isDistBounded_inner_grad_schwartzMap_spherical 📖	mathematical	IsDistBounded	Space instNormedAddCommGroup instInnerProductSpaceReal instFiniteDimensionalReal instMeasurableSpace instBorelSpace grad instAddCommMonoid instModuleReal	—	instFiniteDimensionalReal instBorelSpace integrable_isDistBounded_inner_grad_schwartzMap
repr_grad_inner_eq 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal basis grad instSeminormedAddCommGroup instAddCommGroup instModuleReal	—	grad_inner_repr_eq

---

← Back to Index