Documentation Verification Report

Adjoint

📁 Source: PhysLean/Mathematics/InnerProductSpace/Adjoint.lean

Statistics

Metric	Count
Definitions `HasAdjoint`, `adjoint`	2
Theorems `hasAdjoint`, `add`, `adjoint`, `adjoint_apply_zero`, `adjoint_inner_left`, `adjoint_inner_right`, `comp`, `congr_adj`, `fst`, `neg`, `prodMk`, `smul_left`, `smul_right`, `snd`, `sub`, `adjoint_eq_clm_adjoint`, `hasAdjoint_id`, `hasAdjoint_zero`	18
Total	20

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasAdjoint` 📖	mathematical	—	`HasAdjoint` `InnerProductSpace'.toNormedAddCommGroupWitL2` `InnerProductSpace'.fromL2` `InnerProductSpace'.toInnerProductSpaceWithL2` `InnerProductSpace'.instCompleteSpaceWithLpOfNatENNReal` `InnerProductSpace'.toL2`	—	`InnerProductSpace'.instCompleteSpaceWithLpOfNatENNReal`

HasAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`HasAdjoint`	`HasAdjoint`	—	`inner_add_left'` `adjoint_inner_left` `inner_add_right'`
`adjoint` 📖	mathematical	`HasAdjoint`	`adjoint`	—	`ext_inner_right'` `adjoint_inner_left`
`adjoint_apply_zero` 📖	—	`HasAdjoint`	—	—	`inner_zero_left'` `adjoint_inner_left`
`adjoint_inner_left` 📖	mathematical	`HasAdjoint`	`instInnerOfInnerProductSpace'`	—	—
`adjoint_inner_right` 📖	mathematical	`HasAdjoint`	`instInnerOfInnerProductSpace'`	—	`inner_conj_symm'` `adjoint_inner_left`
`comp` 📖	mathematical	`HasAdjoint`	`HasAdjoint`	—	`adjoint_inner_left`
`congr_adj` 📖	mathematical	`HasAdjoint`	`HasAdjoint`	—	—
`fst` 📖	mathematical	`HasAdjoint` `instInnerProductSpace'Prod`	`HasAdjoint`	—	`adjoint_inner_left` `inner_zero_left'`
`neg` 📖	mathematical	`HasAdjoint`	`HasAdjoint`	—	`inner_neg_left'` `adjoint_inner_left` `inner_neg_right'`
`prodMk` 📖	mathematical	`HasAdjoint`	`HasAdjoint` `instInnerProductSpace'Prod`	—	`inner_add_left'` `adjoint_inner_left`
`smul_left` 📖	mathematical	`HasAdjoint`	`HasAdjoint`	—	`inner_smul_left'` `adjoint_inner_left` `inner_smul_right'`
`smul_right` 📖	mathematical	`HasAdjoint` `instInnerProductSpace'`	`HasAdjoint` `instInnerOfInnerProductSpace'`	—	`inner_conj_symm'` `adjoint_inner_left` `inner_smul_right'`
`snd` 📖	mathematical	`HasAdjoint` `instInnerProductSpace'Prod`	`HasAdjoint`	—	`adjoint_inner_left` `inner_zero_left'`
`sub` 📖	mathematical	`HasAdjoint`	`HasAdjoint`	—	`inner_add_left'` `adjoint_inner_left` `inner_neg_left'` `inner_add_right'` `inner_neg_right'`

(root)

Definitions

Name	Category	Theorems
`HasAdjoint` 📖	CompData	14 math math: `hasAdjoint_id`, `HasAdjoint.prodMk`, `HasAdjoint.smul_right`, `HasAdjFDerivAt.hasAdjoint_fderiv`, `ContinuousLinearMap.hasAdjoint`, `HasAdjoint.fst`, `HasAdjoint.comp`, `HasAdjoint.snd`, `HasAdjoint.sub`, `hasAdjoint_zero`, `HasAdjoint.smul_left`, `HasAdjoint.congr_adj`, `HasAdjoint.neg`, `HasAdjoint.add`
`adjoint` 📖	CompOp	3 math math: `HasVarAdjoint.clm_apply`, `adjoint_eq_clm_adjoint`, `HasAdjoint.adjoint`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoint_eq_clm_adjoint` 📖	mathematical	—	`adjoint` `InnerProductSpace'.toNormedAddCommGroupWitL2` `InnerProductSpace'.fromL2` `InnerProductSpace'.toInnerProductSpaceWithL2` `InnerProductSpace'.instCompleteSpaceWithLpOfNatENNReal` `InnerProductSpace'.toL2`	—	`InnerProductSpace'.instCompleteSpaceWithLpOfNatENNReal` `ext_inner_right'` `HasAdjoint.adjoint_inner_left` `ContinuousLinearMap.hasAdjoint`
`hasAdjoint_id` 📖	mathematical	—	`HasAdjoint`	—	—
`hasAdjoint_zero` 📖	mathematical	—	`HasAdjoint`	—	`inner_zero_left'` `inner_zero_right'`

---

← Back to Index