Div

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

Statistics

Metric	Count
Definitions distDiv, div, divNotation	3
Theorems distDiv_apply_eq_sum_distDeriv, distDiv_apply_eq_sum_fderivD, distDiv_ofFunction, div_add, div_const, div_linear_map, div_smul, div_zero	8
Total	11

Space

Definitions

Name	Category	Theorems
distDiv 📖	CompOp	7 math math: distDiv_inv_pow_eq_dim, distDiv_apply_eq_sum_fderivD, distDiv_ofFunction, constantTime_distSpaceDiv, distDiv_distConst, distDiv_apply_eq_sum_distDeriv, distDiv_distTranslate
div 📖	CompOp	25 math math: div_smul, HasVarAdjoint.gradient, HasVarAdjoint.grad, Electromagnetism.ElectromagneticPotential.harmonicWaveX_div_electricField_eq_zero, HasVarAdjDerivAt.gradient, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.div_electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField, div_of_curl_eq_zero, div_linear_map, laplacian_eq_div_of_grad, HasVarAdjoint.div, IsLocalizedFunctionTransform.div_comp_repr, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three, IsTestFunction.of_div, divergence_eq_space_div, Electromagnetism.ElectromagneticPotential.magneticField_div_eq_zero, HasVarAdjDerivAt.grad, div_add, IsLocalizedFunctionTransform.div, div_const, curl_of_curl, Electromagnetism.ElectromagneticPotential.isExtrema_iff_gauss_ampere_magneticFieldMatrix, HasVarAdjDerivAt.div, div_zero
divNotation 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
distDiv_apply_eq_sum_distDeriv 📖	mathematical	—	Distribution Space instNormedAddCommGroup instInnerProductSpaceReal distDiv distDeriv	—	instFiniteDimensionalReal distDiv_apply_eq_sum_fderivD
distDiv_apply_eq_sum_fderivD 📖	mathematical	—	Distribution Space instNormedAddCommGroup instInnerProductSpaceReal distDiv Distribution.fderivD instFiniteDimensionalReal basis	—	instFiniteDimensionalReal
distDiv_ofFunction 📖	mathematical	IsDistBounded	Distribution Space instNormedAddCommGroup instInnerProductSpaceReal distDiv distOfFunction instFiniteDimensionalReal instMeasurableSpace instBorelSpace grad	—	instFiniteDimensionalReal instBorelSpace distDiv_apply_eq_sum_fderivD grad_eq_sum Distribution.fderivD_apply distOfFunction_apply IsDistBounded.integrable_space IsDistBounded.pi_comp deriv_eq_fderiv_basis
div_add 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup	div	—	—
div_const 📖	mathematical	—	div Space	—	—
div_linear_map 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup	div	—	div_add div_smul
div_smul 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup	div	—	—
div_zero 📖	mathematical	—	div Space	—	—

---

← Back to Index