Documentation Verification Report

Basic

📁 Source: PhysLean/CondensedMatter/TightBindingChain/Basic.lean

Statistics

Metric	Count
Definitions `TightBindingChain`, `BrillouinZone`, `E0`, `N`, `QuantaWaveNumber`, `a`, `energyEigenstate`, `energyEigenvalue`, `hamiltonian`, `localizedComp`, `localizedState`, `t`, `«term\|_⟩»`, `«term\|_⟩⟨_\|»`, `«term⟨_\|_⟩»`	15
Theorems `N_ne_zero`, `a_pos`, `energyEigenstate_orthogonal`, `energy_localizedState`, `hamiltonian_apply_localizedState`, `hamiltonian_energyEigenstate`, `hamiltonian_hermitian`, `instNeZeroNatN`, `localizedComp_adjoint`, `localizedComp_apply_localizedState`, `localizedState_orthonormal`, `localizedState_orthonormal_eq_ite`, `quantaWaveNumber_exp_N`, `quantaWaveNumber_exp_add_one`, `quantaWaveNumber_exp_sub_one`, `quantaWaveNumber_subset_brillouinZone`	16
Total	31

CondensedMatter

Definitions

Name	Category	Theorems
`TightBindingChain` 📖	CompData	—

CondensedMatter.TightBindingChain

Definitions

Name	Category	Theorems
`BrillouinZone` 📖	CompOp	1 math math: `quantaWaveNumber_subset_brillouinZone`
`E0` 📖	CompOp	2 math math: `energy_localizedState`, `hamiltonian_apply_localizedState`
`N` 📖	CompOp	13 math math: `localizedState_orthonormal_eq_ite`, `localizedState_orthonormal`, `quantaWaveNumber_exp_N`, `N_ne_zero`, `hamiltonian_hermitian`, `quantaWaveNumber_exp_add_one`, `localizedComp_adjoint`, `quantaWaveNumber_exp_sub_one`, `energyEigenstate_orthogonal`, `localizedComp_apply_localizedState`, `instNeZeroNatN`, `hamiltonian_apply_localizedState`, `hamiltonian_energyEigenstate`
`QuantaWaveNumber` 📖	CompOp	5 math math: `quantaWaveNumber_exp_N`, `quantaWaveNumber_exp_add_one`, `quantaWaveNumber_exp_sub_one`, `energyEigenstate_orthogonal`, `quantaWaveNumber_subset_brillouinZone`
`a` 📖	CompOp	4 math math: `quantaWaveNumber_exp_N`, `quantaWaveNumber_exp_add_one`, `a_pos`, `quantaWaveNumber_exp_sub_one`
`energyEigenstate` 📖	CompOp	2 math math: `energyEigenstate_orthogonal`, `hamiltonian_energyEigenstate`
`energyEigenvalue` 📖	CompOp	1 math math: `hamiltonian_energyEigenstate`
`hamiltonian` 📖	CompOp	4 math math: `hamiltonian_hermitian`, `energy_localizedState`, `hamiltonian_apply_localizedState`, `hamiltonian_energyEigenstate`
`localizedComp` 📖	CompOp	2 math math: `localizedComp_adjoint`, `localizedComp_apply_localizedState`
`localizedState` 📖	CompOp	5 math math: `localizedState_orthonormal_eq_ite`, `localizedState_orthonormal`, `energy_localizedState`, `localizedComp_apply_localizedState`, `hamiltonian_apply_localizedState`
`t` 📖	CompOp	1 math math: `hamiltonian_apply_localizedState`
`«term\|_⟩»` 📖	CompOp	—
`«term\|_⟩⟨_\|»` 📖	CompOp	—
`«term⟨_\|_⟩»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`N_ne_zero` 📖	mathematical	—	`N`	—	—
`a_pos` 📖	mathematical	—	`a`	—	—
`energyEigenstate_orthogonal` 📖	mathematical	—	`QuantaWaveNumber` `HilbertSpace` `QuantumMechanics.FiniteHilbertSpace` `N` `QuantumMechanics.instNormedAddCommGroupFiniteHilbertSpace` `QuantumMechanics.instInnerProductSpaceComplexFiniteHilbertSpace` `energyEigenstate`	—	`localizedState_orthonormal` `quantaWaveNumber_exp_N` `a_pos` `instNeZeroNatN`
`energy_localizedState` 📖	mathematical	`N`	`HilbertSpace` `QuantumMechanics.FiniteHilbertSpace` `QuantumMechanics.instNormedAddCommGroupFiniteHilbertSpace` `QuantumMechanics.instInnerProductSpaceComplexFiniteHilbertSpace` `localizedState` `QuantumMechanics.instModuleComplexFiniteHilbertSpace` `hamiltonian` `E0`	—	`instNeZeroNatN` `hamiltonian_apply_localizedState` `localizedState_orthonormal_eq_ite`
`hamiltonian_apply_localizedState` 📖	mathematical	—	`HilbertSpace` `QuantumMechanics.instNormedAddCommGroupFiniteHilbertSpace` `N` `QuantumMechanics.instModuleComplexFiniteHilbertSpace` `hamiltonian` `QuantumMechanics.instInnerProductSpaceComplexFiniteHilbertSpace` `localizedState` `E0` `t` `instNeZeroNatN`	—	`instNeZeroNatN` `localizedComp_apply_localizedState`
`hamiltonian_energyEigenstate` 📖	mathematical	—	`HilbertSpace` `QuantumMechanics.instNormedAddCommGroupFiniteHilbertSpace` `N` `QuantumMechanics.instModuleComplexFiniteHilbertSpace` `hamiltonian` `energyEigenstate` `QuantumMechanics.instInnerProductSpaceComplexFiniteHilbertSpace` `energyEigenvalue`	—	`energyEigenstate.eq_1` `instNeZeroNatN` `hamiltonian_apply_localizedState` `quantaWaveNumber_exp_sub_one` `quantaWaveNumber_exp_add_one`
`hamiltonian_hermitian` 📖	mathematical	—	`HilbertSpace` `QuantumMechanics.FiniteHilbertSpace` `N` `QuantumMechanics.instNormedAddCommGroupFiniteHilbertSpace` `QuantumMechanics.instInnerProductSpaceComplexFiniteHilbertSpace` `QuantumMechanics.instModuleComplexFiniteHilbertSpace` `hamiltonian`	—	`instNeZeroNatN` `localizedComp_adjoint`
`instNeZeroNatN` 📖	mathematical	—	`N`	—	`N_ne_zero`
`localizedComp_adjoint` 📖	mathematical	—	`HilbertSpace` `QuantumMechanics.FiniteHilbertSpace` `N` `QuantumMechanics.instNormedAddCommGroupFiniteHilbertSpace` `QuantumMechanics.instInnerProductSpaceComplexFiniteHilbertSpace` `QuantumMechanics.instModuleComplexFiniteHilbertSpace` `localizedComp`	—	—
`localizedComp_apply_localizedState` 📖	mathematical	—	`HilbertSpace` `QuantumMechanics.instNormedAddCommGroupFiniteHilbertSpace` `N` `QuantumMechanics.instModuleComplexFiniteHilbertSpace` `localizedComp` `QuantumMechanics.instInnerProductSpaceComplexFiniteHilbertSpace` `localizedState` `QuantumMechanics.instAddCommGroupFiniteHilbertSpace`	—	`localizedComp.eq_1` `localizedState_orthonormal`
`localizedState_orthonormal` 📖	mathematical	—	`HilbertSpace` `QuantumMechanics.instNormedAddCommGroupFiniteHilbertSpace` `N` `QuantumMechanics.instInnerProductSpaceComplexFiniteHilbertSpace` `localizedState`	—	—
`localizedState_orthonormal_eq_ite` 📖	mathematical	—	`HilbertSpace` `QuantumMechanics.FiniteHilbertSpace` `N` `QuantumMechanics.instNormedAddCommGroupFiniteHilbertSpace` `QuantumMechanics.instInnerProductSpaceComplexFiniteHilbertSpace` `localizedState`	—	`localizedState_orthonormal`
`quantaWaveNumber_exp_N` 📖	mathematical	—	`QuantaWaveNumber` `N` `a`	—	`instNeZeroNatN` `a_pos`
`quantaWaveNumber_exp_add_one` 📖	mathematical	—	`QuantaWaveNumber` `N` `instNeZeroNatN` `a`	—	`instNeZeroNatN` `quantaWaveNumber_exp_sub_one`
`quantaWaveNumber_exp_sub_one` 📖	mathematical	—	`QuantaWaveNumber` `N` `instNeZeroNatN` `a`	—	`instNeZeroNatN` `quantaWaveNumber_exp_N`
`quantaWaveNumber_subset_brillouinZone` 📖	mathematical	—	`QuantaWaveNumber` `BrillouinZone`	—	`instNeZeroNatN` `a_pos`

---

← Back to Index