Documentation Verification Report

AdjFDeriv

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

Statistics

Metric	Count
Definitions `HasAdjFDerivAt`, `adjFDeriv`	2
Theorems `isBoundedBilinearMap_real`, `hasAdjFDerivAt`, `adjFDeriv`, `comp`, `contDiffAt_deriv`, `differentiableAt`, `hasAdjoint_fderiv`, `inner`, `neg`, `prodMk`, `smul`, `sub`, `add`, `fst`, `snd`, `adjFDeriv_add`, `adjFDeriv_comp`, `adjFDeriv_const`, `adjFDeriv_fst`, `adjFDeriv_id`, `adjFDeriv_id'`, `adjFDeriv_inner`, `adjFDeriv_neg`, `adjFDeriv_prod_fst`, `adjFDeriv_prod_snd`, `adjFDeriv_smul`, `adjFDeriv_snd`, `adjFDeriv_sub`, `adjFDeriv_uncurry`, `gradient_eq_adjFDeriv`, `hasAdjFDerivAt_const`, `hasAdjFDerivAt_id`, `hasAdjFDerivAt_uncurry`	33
Total	35

ContinuousLinearMap.adjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBoundedBilinearMap_real` 📖	—	—	—	—	—

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasAdjFDerivAt` 📖	mathematical	—	`HasAdjFDerivAt` `adjFDeriv`	—	`HasAdjoint.congr_adj` `InnerProductSpace'.instCompleteSpaceWithLpOfNatENNReal` `ContinuousLinearMap.hasAdjoint` `adjoint_eq_clm_adjoint`

HasAdjFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjFDeriv` 📖	mathematical	`HasAdjFDerivAt`	`adjFDeriv`	—	`HasAdjoint.adjoint` `hasAdjoint_fderiv`
`comp` 📖	—	`HasAdjFDerivAt`	—	—	`differentiableAt` `HasAdjoint.comp` `hasAdjoint_fderiv`
`contDiffAt_deriv` 📖	—	`HasAdjFDerivAt`	—	—	`adjFDeriv` `InnerProductSpace'.instCompleteSpaceWithLpOfNatENNReal` `adjoint_eq_clm_adjoint` `ContinuousLinearMap.adjoint.isBoundedBilinearMap_real`
`differentiableAt` 📖	—	`HasAdjFDerivAt`	—	—	—
`hasAdjoint_fderiv` 📖	mathematical	`HasAdjFDerivAt`	`HasAdjoint`	—	—
`inner` 📖	mathematical	—	`HasAdjFDerivAt` `instInnerProductSpace'Prod` `instInnerProductSpace'` `instInnerOfInnerProductSpace'`	—	`DifferentiableAt.inner'` `fderiv_inner_apply'` `inner_smul_left'` `real_inner_comm'`
`neg` 📖	—	`HasAdjFDerivAt`	—	—	`differentiableAt` `HasAdjoint.neg` `hasAdjoint_fderiv`
`prodMk` 📖	mathematical	`HasAdjFDerivAt`	`instInnerProductSpace'Prod`	—	`differentiableAt` `HasAdjoint.prodMk` `hasAdjoint_fderiv`
`smul` 📖	mathematical	`HasAdjFDerivAt` `instInnerProductSpace'`	`instInnerOfInnerProductSpace'`	—	`differentiableAt` `HasAdjoint.add` `HasAdjoint.smul_left` `hasAdjoint_fderiv` `HasAdjoint.smul_right`
`sub` 📖	—	`HasAdjFDerivAt`	—	—	`differentiableAt` `HasAdjoint.sub` `hasAdjoint_fderiv`

HasAjdFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	—	`HasAdjFDerivAt`	—	—	`HasAdjFDerivAt.differentiableAt` `HasAdjoint.add` `HasAdjFDerivAt.hasAdjoint_fderiv`
`fst` 📖	—	`HasAdjFDerivAt` `instInnerProductSpace'Prod`	—	—	`HasAdjFDerivAt.differentiableAt` `HasAdjoint.fst` `HasAdjFDerivAt.hasAdjoint_fderiv`
`snd` 📖	—	`HasAdjFDerivAt` `instInnerProductSpace'Prod`	—	—	`HasAdjFDerivAt.differentiableAt` `HasAdjoint.snd` `HasAdjFDerivAt.hasAdjoint_fderiv`

(root)

Definitions

Name	Category	Theorems
`HasAdjFDerivAt` 📖	CompData	4 math math: `hasAdjFDerivAt_id`, `HasAdjFDerivAt.inner`, `hasAdjFDerivAt_const`, `DifferentiableAt.hasAdjFDerivAt`
`adjFDeriv` 📖	CompOp	21 math math: `adjFDeriv_uncurry`, `adjFDeriv_sub`, `adjFDeriv_fst`, `adjFDeriv_prod_fst`, `adjFDeriv_comp`, `IsLocalizedFunctionTransform.adjFDeriv`, `gradient_eq_adjFDeriv`, `HasVarAdjoint.adjFDeriv_apply`, `IsTestFunction.adjFDeriv`, `adjFDeriv_id`, `adjFDeriv_const`, `HasAdjFDerivAt.adjFDeriv`, `adjFDeriv_neg`, `adjFDeriv_add`, `adjFDeriv_prod_snd`, `adjFDeriv_inner`, `divergence_smul`, `adjFDeriv_smul`, `adjFDeriv_id'`, `DifferentiableAt.hasAdjFDerivAt`, `adjFDeriv_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjFDeriv_add` 📖	mathematical	—	`adjFDeriv`	—	`HasAdjFDerivAt.adjFDeriv` `HasAjdFDerivAt.add` `DifferentiableAt.hasAdjFDerivAt`
`adjFDeriv_comp` 📖	mathematical	—	`adjFDeriv`	—	`HasAdjFDerivAt.adjFDeriv` `HasAdjFDerivAt.comp` `DifferentiableAt.hasAdjFDerivAt`
`adjFDeriv_const` 📖	mathematical	—	`adjFDeriv`	—	`HasAdjFDerivAt.adjFDeriv` `hasAdjFDerivAt_const`
`adjFDeriv_fst` 📖	mathematical	—	`adjFDeriv` `instInnerProductSpace'Prod`	—	`HasAdjFDerivAt.adjFDeriv` `HasAjdFDerivAt.fst` `DifferentiableAt.hasAdjFDerivAt`
`adjFDeriv_id` 📖	mathematical	—	`adjFDeriv`	—	`HasAdjFDerivAt.adjFDeriv` `hasAdjFDerivAt_id`
`adjFDeriv_id'` 📖	mathematical	—	`adjFDeriv`	—	`adjFDeriv_id`
`adjFDeriv_inner` 📖	mathematical	—	`adjFDeriv` `instInnerProductSpace'Prod` `instInnerProductSpace'` `instInnerOfInnerProductSpace'`	—	`HasAdjFDerivAt.adjFDeriv` `HasAdjFDerivAt.inner`
`adjFDeriv_neg` 📖	mathematical	—	`adjFDeriv`	—	`HasAdjFDerivAt.adjFDeriv` `HasAdjFDerivAt.neg` `DifferentiableAt.hasAdjFDerivAt`
`adjFDeriv_prod_fst` 📖	mathematical	—	`adjFDeriv` `instInnerProductSpace'Prod`	—	`adjFDeriv_fst` `adjFDeriv_id'`
`adjFDeriv_prod_snd` 📖	mathematical	—	`adjFDeriv` `instInnerProductSpace'Prod`	—	`adjFDeriv_snd` `adjFDeriv_id'`
`adjFDeriv_smul` 📖	mathematical	—	`adjFDeriv` `instInnerProductSpace'` `instInnerOfInnerProductSpace'`	—	`HasAdjFDerivAt.adjFDeriv` `HasAdjFDerivAt.smul` `DifferentiableAt.hasAdjFDerivAt`
`adjFDeriv_snd` 📖	mathematical	—	`adjFDeriv` `instInnerProductSpace'Prod`	—	`HasAdjFDerivAt.adjFDeriv` `HasAjdFDerivAt.snd` `DifferentiableAt.hasAdjFDerivAt`
`adjFDeriv_sub` 📖	mathematical	—	`adjFDeriv`	—	`HasAdjFDerivAt.adjFDeriv` `HasAdjFDerivAt.sub` `DifferentiableAt.hasAdjFDerivAt`
`adjFDeriv_uncurry` 📖	mathematical	—	`adjFDeriv` `instInnerProductSpace'Prod`	—	`HasAdjFDerivAt.adjFDeriv` `hasAdjFDerivAt_uncurry` `DifferentiableAt.hasAdjFDerivAt`
`gradient_eq_adjFDeriv` 📖	mathematical	—	`adjFDeriv` `instInnerProductSpace'`	—	`HasAdjoint.adjoint_inner_left` `HasAdjFDerivAt.hasAdjoint_fderiv` `DifferentiableAt.hasAdjFDerivAt`
`hasAdjFDerivAt_const` 📖	mathematical	—	`HasAdjFDerivAt`	—	`hasAdjoint_zero`
`hasAdjFDerivAt_id` 📖	mathematical	—	`HasAdjFDerivAt`	—	`hasAdjoint_id`
`hasAdjFDerivAt_uncurry` 📖	mathematical	`HasAdjFDerivAt`	`instInnerProductSpace'Prod`	—	`fderiv_uncurry` `HasAdjoint.congr_adj` `HasAdjoint.add` `HasAdjoint.comp` `HasAdjFDerivAt.hasAdjoint_fderiv` `HasAdjoint.fst` `hasAdjoint_id` `HasAdjoint.snd`

---

← Back to Index