Documentation Verification Report

Basic

📁 Source: PhysLean/QuantumMechanics/OneDimension/ReflectionlessPotential/Basic.lean

Statistics

Metric	Count
Definitions `ReflectionlessPotential`, `N`, `annihilationOperator`, `annihilationOperatorSchwartz`, `creationOperator`, `creationOperatorSchwartz`, `m`, `mulByTemperateGrowth`, `reflectionlessPotential`, `tanhOperator`, `tanhOperatorSchwartz`, `κ`, `ℏ`	13
Theorems `N_pos`, `m_pos`, `scaled_tanh_complex_hasTemperateGrowth`, `scaled_tanh_hasTemperateGrowth`, `κ_pos`, `ℏ_pos`	6
Total	19

QuantumMechanics.OneDimension

Definitions

Name	Category	Theorems
`ReflectionlessPotential` 📖	CompData	—

QuantumMechanics.OneDimension.ReflectionlessPotential

Definitions

Name	Category	Theorems
`N` 📖	CompOp	1 math math: `N_pos`
`annihilationOperator` 📖	CompOp	—
`annihilationOperatorSchwartz` 📖	CompOp	—
`creationOperator` 📖	CompOp	—
`creationOperatorSchwartz` 📖	CompOp	—
`m` 📖	CompOp	1 math math: `m_pos`
`mulByTemperateGrowth` 📖	CompOp	—
`reflectionlessPotential` 📖	CompOp	—
`tanhOperator` 📖	CompOp	—
`tanhOperatorSchwartz` 📖	CompOp	—
`κ` 📖	CompOp	1 math math: `κ_pos`
`ℏ` 📖	CompOp	1 math math: `ℏ_pos`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`N_pos` 📖	mathematical	—	`N`	—	—
`m_pos` 📖	mathematical	—	`m`	—	—
`scaled_tanh_complex_hasTemperateGrowth` 📖	—	—	—	—	`scaled_tanh_hasTemperateGrowth`
`scaled_tanh_hasTemperateGrowth` 📖	—	—	—	—	`tanh_const_mul_hasTemperateGrowth`
`κ_pos` 📖	mathematical	—	`κ`	—	—
`ℏ_pos` 📖	mathematical	—	`ℏ`	—	—

---

← Back to Index