Documentation Verification Report

IsLocalizedfunctionTransform

📁 Source: PhysLean/Mathematics/VariationalCalculus/IsLocalizedfunctionTransform.lean

Statistics

Metric	Count
Definitions `IsLocalizedFunctionTransform`	1
Theorems `add`, `adjFDeriv`, `clm_apply`, `comp`, `deriv`, `div`, `div_comp_repr`, `fderiv`, `fst`, `fun_comp`, `grad`, `gradient`, `id`, `mul_left`, `mul_right`, `neg`, `prod`, `smul_left`, `snd`	19
Total	20

IsLocalizedFunctionTransform

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsLocalizedFunctionTransform`	`IsLocalizedFunctionTransform`	—	—
`adjFDeriv` 📖	mathematical	—	`IsLocalizedFunctionTransform` `adjFDeriv`	—	—
`clm_apply` 📖	mathematical	—	`IsLocalizedFunctionTransform`	—	—
`comp` 📖	mathematical	`IsLocalizedFunctionTransform`	`IsLocalizedFunctionTransform`	—	—
`deriv` 📖	mathematical	—	`IsLocalizedFunctionTransform`	—	—
`div` 📖	mathematical	—	`IsLocalizedFunctionTransform` `Space` `Space.instNormedAddCommGroup` `Space.div`	—	`Space.instFiniteDimensionalReal`
`div_comp_repr` 📖	mathematical	—	`IsLocalizedFunctionTransform` `Space` `Space.instNormedAddCommGroup` `Space.div` `Space.instInnerProductSpaceReal` `Space.basis`	—	`Space.instFiniteDimensionalReal` `Space.basis_repr_apply`
`fderiv` 📖	mathematical	—	`IsLocalizedFunctionTransform`	—	—
`fst` 📖	mathematical	`IsLocalizedFunctionTransform`	`IsLocalizedFunctionTransform`	—	—
`fun_comp` 📖	mathematical	`IsLocalizedFunctionTransform`	`IsLocalizedFunctionTransform`	—	`comp`
`grad` 📖	mathematical	—	`IsLocalizedFunctionTransform` `Space` `Space.instNormedAddCommGroup` `Space.grad`	—	`Space.instFiniteDimensionalReal` `Space.grad_eq_sum`
`gradient` 📖	mathematical	—	`IsLocalizedFunctionTransform` `Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `Space.instPseudoMetricSpace` `Space.instFiniteDimensionalReal`	—	`Space.instFiniteDimensionalReal` `Space.gradient_eq_sum`
`id` 📖	mathematical	—	`IsLocalizedFunctionTransform`	—	—
`mul_left` 📖	mathematical	`IsLocalizedFunctionTransform`	`IsLocalizedFunctionTransform`	—	—
`mul_right` 📖	mathematical	`IsLocalizedFunctionTransform`	`IsLocalizedFunctionTransform`	—	—
`neg` 📖	mathematical	`IsLocalizedFunctionTransform`	`IsLocalizedFunctionTransform`	—	—
`prod` 📖	mathematical	`IsLocalizedFunctionTransform`	`IsLocalizedFunctionTransform`	—	—
`smul_left` 📖	mathematical	`IsLocalizedFunctionTransform`	`IsLocalizedFunctionTransform`	—	—
`snd` 📖	mathematical	`IsLocalizedFunctionTransform`	`IsLocalizedFunctionTransform`	—	—

(root)

Definitions

Name	Category	Theorems
`IsLocalizedFunctionTransform` 📖	MathDef	20 math math: `IsLocalizedFunctionTransform.fst`, `IsLocalizedFunctionTransform.mul_right`, `IsLocalizedFunctionTransform.adjFDeriv`, `IsLocalizedFunctionTransform.mul_left`, `IsLocalizedFunctionTransform.smul_left`, `HasVarAdjoint.ext'`, `IsLocalizedFunctionTransform.prod`, `IsLocalizedFunctionTransform.neg`, `IsLocalizedFunctionTransform.snd`, `IsLocalizedFunctionTransform.fun_comp`, `IsLocalizedFunctionTransform.div_comp_repr`, `IsLocalizedFunctionTransform.fderiv`, `IsLocalizedFunctionTransform.gradient`, `IsLocalizedFunctionTransform.add`, `IsLocalizedFunctionTransform.div`, `IsLocalizedFunctionTransform.grad`, `IsLocalizedFunctionTransform.deriv`, `IsLocalizedFunctionTransform.comp`, `IsLocalizedFunctionTransform.id`, `IsLocalizedFunctionTransform.clm_apply`

---

← Back to Index