Documentation Verification Report

HilbertSpace

📁 Source: PhysLean/QuantumMechanics/FiniteTarget/HilbertSpace.lean

Statistics

Metric	Count
Definitions `HilbertSpace`, `FiniteHilbertSpace`, `HilbertSpace`, `instAddCommGroupFiniteHilbertSpace`, `instInnerProductSpaceComplexFiniteHilbertSpace`, `instModuleComplexFiniteHilbertSpace`, `instNormedAddCommGroupFiniteHilbertSpace`	7
Theorems `instCompleteSpaceFiniteHilbertSpace`	1
Total	8

CondensedMatter.TightBindingChain

Definitions

Name	Category	Theorems
`HilbertSpace` 📖	CompOp	9 math math: `localizedState_orthonormal_eq_ite`, `localizedState_orthonormal`, `hamiltonian_hermitian`, `localizedComp_adjoint`, `energy_localizedState`, `energyEigenstate_orthogonal`, `localizedComp_apply_localizedState`, `hamiltonian_apply_localizedState`, `hamiltonian_energyEigenstate`

QuantumMechanics

Definitions

Name	Category	Theorems
`FiniteHilbertSpace` 📖	CompOp	6 math math: `CondensedMatter.TightBindingChain.localizedState_orthonormal_eq_ite`, `CondensedMatter.TightBindingChain.hamiltonian_hermitian`, `instCompleteSpaceFiniteHilbertSpace`, `CondensedMatter.TightBindingChain.localizedComp_adjoint`, `CondensedMatter.TightBindingChain.energy_localizedState`, `CondensedMatter.TightBindingChain.energyEigenstate_orthogonal`
`instAddCommGroupFiniteHilbertSpace` 📖	CompOp	1 math math: `CondensedMatter.TightBindingChain.localizedComp_apply_localizedState`
`instInnerProductSpaceComplexFiniteHilbertSpace` 📖	CompOp	9 math math: `CondensedMatter.TightBindingChain.localizedState_orthonormal_eq_ite`, `CondensedMatter.TightBindingChain.localizedState_orthonormal`, `CondensedMatter.TightBindingChain.hamiltonian_hermitian`, `CondensedMatter.TightBindingChain.localizedComp_adjoint`, `CondensedMatter.TightBindingChain.energy_localizedState`, `CondensedMatter.TightBindingChain.energyEigenstate_orthogonal`, `CondensedMatter.TightBindingChain.localizedComp_apply_localizedState`, `CondensedMatter.TightBindingChain.hamiltonian_apply_localizedState`, `CondensedMatter.TightBindingChain.hamiltonian_energyEigenstate`
`instModuleComplexFiniteHilbertSpace` 📖	CompOp	6 math math: `CondensedMatter.TightBindingChain.hamiltonian_hermitian`, `CondensedMatter.TightBindingChain.localizedComp_adjoint`, `CondensedMatter.TightBindingChain.energy_localizedState`, `CondensedMatter.TightBindingChain.localizedComp_apply_localizedState`, `CondensedMatter.TightBindingChain.hamiltonian_apply_localizedState`, `CondensedMatter.TightBindingChain.hamiltonian_energyEigenstate`
`instNormedAddCommGroupFiniteHilbertSpace` 📖	CompOp	10 math math: `CondensedMatter.TightBindingChain.localizedState_orthonormal_eq_ite`, `CondensedMatter.TightBindingChain.localizedState_orthonormal`, `CondensedMatter.TightBindingChain.hamiltonian_hermitian`, `instCompleteSpaceFiniteHilbertSpace`, `CondensedMatter.TightBindingChain.localizedComp_adjoint`, `CondensedMatter.TightBindingChain.energy_localizedState`, `CondensedMatter.TightBindingChain.energyEigenstate_orthogonal`, `CondensedMatter.TightBindingChain.localizedComp_apply_localizedState`, `CondensedMatter.TightBindingChain.hamiltonian_apply_localizedState`, `CondensedMatter.TightBindingChain.hamiltonian_energyEigenstate`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompleteSpaceFiniteHilbertSpace` 📖	mathematical	—	`FiniteHilbertSpace` `instNormedAddCommGroupFiniteHilbertSpace`	—	—

QuantumMechanics.OneDimension

Definitions

Name	Category	Theorems
`HilbertSpace` 📖	CompOp	16 math math: `HarmonicOscillator.eigenfunction_linearIndependent`, `HilbertSpace.inner_mk_mk`, `HilbertSpace.schwartzIncl_inner`, `HilbertSpace.toBra_injective`, `HilbertSpace.schwartzIncl_injective`, `HilbertSpace.mk_add`, `HarmonicOscillator.eigenfunction_orthonormal`, `HilbertSpace.schwartzIncl_coe_ae`, `HilbertSpace.toBra_apply`, `HilbertSpace.aeEqFun_mk_mem_iff`, `HilbertSpace.mem_iff'`, `HarmonicOscillator.eigenfunction_normalized`, `HarmonicOscillator.eigenfunction_completeness`, `HilbertSpace.mk_smul`, `HarmonicOscillator.eigenfunction_orthogonal`, `HilbertSpace.toBra_surjective`

---

← Back to Index