Documentation Verification Report

Divergence

📁 Source: PhysLean/Mathematics/Calculus/Divergence.lean

Statistics

Metric	Count
Definitions `divergence`	1
Theorems `divergence_add`, `divergence_const_smul`, `divergence_eq_space_div`, `divergence_eq_sum_fderiv`, `divergence_eq_sum_fderiv'`, `divergence_neg`, `divergence_prodMk`, `divergence_smul`, `divergence_sub`, `divergence_zero`	10
Total	11

(root)

Definitions

Name	Category	Theorems
`divergence` 📖	CompOp	12 math math: `divergence_zero`, `HasVarAdjoint.adjFDeriv_apply`, `divergence_eq_sum_fderiv'`, `divergence_neg`, `divergence_add`, `divergence_eq_sum_fderiv`, `divergence_prodMk`, `IsTestFunction.divergence`, `divergence_eq_space_div`, `divergence_smul`, `divergence_const_smul`, `divergence_sub`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`divergence_add` 📖	mathematical	—	`divergence`	—	—
`divergence_const_smul` 📖	mathematical	—	`divergence`	—	—
`divergence_eq_space_div` 📖	mathematical	`Space` `Space.instAddCommGroup` `Space.instModuleReal` `Space.instSeminormedAddCommGroup`	`divergence` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `Space.div` `Space.basis`	—	`divergence_eq_sum_fderiv'` `Space.basis_repr_apply` `Space.coordCLM_apply` `Space.coord_apply`
`divergence_eq_sum_fderiv` 📖	mathematical	—	`divergence`	—	—
`divergence_eq_sum_fderiv'` 📖	mathematical	—	`divergence`	—	`divergence_eq_sum_fderiv`
`divergence_neg` 📖	mathematical	—	`divergence`	—	—
`divergence_prodMk` 📖	mathematical	—	`divergence`	—	`divergence_eq_sum_fderiv'` `fderiv_wrt_prod`
`divergence_smul` 📖	mathematical	—	`divergence` `instInnerOfInnerProductSpace'` `adjFDeriv` `instInnerProductSpace'`	—	`HasAdjoint.adjoint_inner_left` `HasAdjFDerivAt.hasAdjoint_fderiv` `DifferentiableAt.hasAdjFDerivAt`
`divergence_sub` 📖	mathematical	—	`divergence`	—	—
`divergence_zero` 📖	mathematical	—	`divergence`	—	—

---

← Back to Index