IsTestFunction

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

Statistics

Metric	Count
Definitions `IsTestFunction`, `toCompactlySupportedContinuousMap`	2
Theorems `add`, `adjFDeriv`, `comp_left`, `contDiff`, `coord`, `deriv`, `differentiable`, `divergence`, `family_linearMap_comp`, `fderiv_apply`, `gradient`, `inner`, `inner_left`, `inner_right`, `integrable`, `linearMap_comp`, `mul`, `mul_left`, `mul_right`, `neg`, `of_compactlySupportedContinuousMap`, `of_div`, `of_fderiv`, `pi`, `prodMk`, `prod_fst`, `prod_snd`, `smooth`, `smul`, `smul_left`, `smul_right`, `space_component`, `sub`, `sum`, `supp`, `zero`	36
Total	38

IsTestFunction

Definitions

Name	Category	Theorems
`toCompactlySupportedContinuousMap` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	—	`IsTestFunction`	—	—	`comp_left` `prodMk`
`adjFDeriv` 📖	mathematical	`IsTestFunction`	`adjFDeriv`	—	`InnerProductSpace'.instCompleteSpaceWithLpOfNatENNReal` `adjoint_eq_clm_adjoint` `comp_left` `contDiff` `of_fderiv` `supp`
`comp_left` 📖	—	`IsTestFunction`	—	—	`smooth` `supp`
`contDiff` 📖	—	`IsTestFunction`	—	—	`smooth`
`coord` 📖	mathematical	`IsTestFunction` `Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal`	`Space.coord`	—	`comp_left` `Space.inner_basis` `Space.zero_apply` `Space.coord_contDiff`
`deriv` 📖	—	`IsTestFunction`	—	—	`smooth` `supp`
`differentiable` 📖	—	`IsTestFunction`	—	—	`smooth`
`divergence` 📖	mathematical	`IsTestFunction`	`divergence`	—	`divergence_eq_sum_fderiv'` `sum` `comp_left` `fderiv_apply`
`family_linearMap_comp` 📖	—	`IsTestFunction`	—	—	`contDiff` `supp`
`fderiv_apply` 📖	—	`IsTestFunction`	—	—	`contDiff` `supp`
`gradient` 📖	mathematical	`IsTestFunction` `Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal`	`Space.instSeminormedAddCommGroup` `Space.instFiniteDimensionalReal`	—	`Space.instFiniteDimensionalReal` `gradient_eq_adjFDeriv` `differentiable` `adjFDeriv`
`inner` 📖	mathematical	`IsTestFunction`	`instInnerOfInnerProductSpace'`	—	`comp_left` `prodMk` `inner_zero_right'` `ContDiff.inner'`
`inner_left` 📖	mathematical	`IsTestFunction`	`instInnerOfInnerProductSpace'`	—	`ContDiff.inner'` `smooth` `supp` `inner_zero_right'`
`inner_right` 📖	mathematical	`IsTestFunction`	`instInnerOfInnerProductSpace'`	—	`ContDiff.inner'` `smooth` `supp` `inner_zero_left'`
`integrable` 📖	—	`IsTestFunction`	—	—	`smooth` `supp`
`linearMap_comp` 📖	—	`IsTestFunction`	—	—	`comp_left`
`mul` 📖	—	`IsTestFunction`	—	—	`comp_left` `prodMk`
`mul_left` 📖	—	`IsTestFunction`	—	—	`smooth` `supp`
`mul_right` 📖	—	`IsTestFunction`	—	—	`smooth` `supp`
`neg` 📖	—	`IsTestFunction`	—	—	`comp_left`
`of_compactlySupportedContinuousMap` 📖	mathematical	—	`IsTestFunction`	—	—
`of_div` 📖	mathematical	`IsTestFunction` `Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal`	`Space.div`	—	`sum` `fderiv_apply` `comp_left`
`of_fderiv` 📖	—	`IsTestFunction`	—	—	`contDiff` `supp`
`pi` 📖	—	`IsTestFunction`	—	—	`smooth` `supp`
`prodMk` 📖	—	`IsTestFunction`	—	—	`contDiff` `supp`
`prod_fst` 📖	—	`IsTestFunction`	—	—	`comp_left`
`prod_snd` 📖	—	`IsTestFunction`	—	—	`comp_left`
`smooth` 📖	—	`IsTestFunction`	—	—	—
`smul` 📖	—	`IsTestFunction`	—	—	`comp_left` `prodMk`
`smul_left` 📖	—	`IsTestFunction`	—	—	`smooth` `supp`
`smul_right` 📖	—	`IsTestFunction`	—	—	`smooth` `supp`
`space_component` 📖	mathematical	`IsTestFunction` `Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal`	`Space.val`	—	`smooth` `Space.eval_contDiff` `supp` `Space.zero_apply`
`sub` 📖	—	`IsTestFunction`	—	—	`comp_left` `prodMk`
`sum` 📖	—	`IsTestFunction`	—	—	`comp_left` `pi`
`supp` 📖	—	`IsTestFunction`	—	—	—
`zero` 📖	mathematical	—	`IsTestFunction`	—	—

(root)

Definitions

Name	Category	Theorems
`IsTestFunction` 📖	CompData	2 math math: `IsTestFunction.zero`, `IsTestFunction.of_compactlySupportedContinuousMap`

---

← Back to Index