Basic

Statistics

Metric	Count
Definitions `MemHS`, `mk`, `toBra`	3
Theorems `aeEqFun_mk_mem_iff`, `aeStronglyMeasurable_of_memHS`, `coe_hilbertSpace_memHS`, `coe_mk_ae`, `eLpNorm_mk`, `ext_iff`, `inner_mk_mk`, `memHS_add`, `memHS_iff`, `memHS_of_ae`, `memHS_smul`, `mem_iff'`, `mk_add`, `mk_eq_iff`, `mk_smul`, `mk_surjective`, `toBra_apply`, `toBra_injective`, `toBra_surjective`, `zero_fun_memHS`, `zero_memHS`	21
Total	24

Name	Category	Theorems
`MemHS` 📖	MathDef	7 math math: `memHS_iff`, `QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_memHS`, `gaussian_memHS`, `zero_fun_memHS`, `zero_memHS`, `aeEqFun_mk_mem_iff`, `coe_hilbertSpace_memHS`
`mk` 📖	CompOp	—
`toBra` 📖	CompOp	3 math math: `toBra_injective`, `toBra_apply`, `toBra_surjective`

Name	Kind	Assumes	Proves	Validates	Depends On
`aeEqFun_mk_mem_iff` 📖	mathematical	—	`QuantumMechanics.OneDimension.HilbertSpace` `MemHS`	—	—
`aeStronglyMeasurable_of_memHS` 📖	—	`MemHS`	—	—	—
`coe_hilbertSpace_memHS` 📖	mathematical	—	`MemHS`	—	`aeEqFun_mk_mem_iff`
`coe_mk_ae` 📖	—	`MemHS`	—	—	—
`eLpNorm_mk` 📖	—	`MemHS`	—	—	`coe_mk_ae`
`ext_iff` 📖	—	—	—	—	—
`inner_mk_mk` 📖	mathematical	`MemHS`	`QuantumMechanics.OneDimension.HilbertSpace`	—	`coe_mk_ae`
`memHS_add` 📖	—	`MemHS`	—	—	—
`memHS_iff` 📖	mathematical	—	`MemHS`	—	`MemHS.eq_1`
`memHS_of_ae` 📖	—	`MemHS`	—	—	—
`memHS_smul` 📖	—	`MemHS`	—	—	—
`mem_iff'` 📖	mathematical	—	`QuantumMechanics.OneDimension.HilbertSpace`	—	—
`mk_add` 📖	mathematical	`MemHS`	`memHS_add` `QuantumMechanics.OneDimension.HilbertSpace`	—	`memHS_add`
`mk_eq_iff` 📖	—	`MemHS`	—	—	—
`mk_smul` 📖	mathematical	`MemHS`	`memHS_smul` `QuantumMechanics.OneDimension.HilbertSpace`	—	`memHS_smul`
`mk_surjective` 📖	—	—	—	—	`coe_hilbertSpace_memHS`
`toBra_apply` 📖	mathematical	—	`QuantumMechanics.OneDimension.HilbertSpace` `toBra`	—	—
`toBra_injective` 📖	mathematical	—	`QuantumMechanics.OneDimension.HilbertSpace` `toBra`	—	—
`toBra_surjective` 📖	mathematical	—	`QuantumMechanics.OneDimension.HilbertSpace` `toBra`	—	—
`zero_fun_memHS` 📖	mathematical	—	`MemHS`	—	`zero_memHS`
`zero_memHS` 📖	mathematical	—	`MemHS`	—	`memHS_iff`

---