Documentation Verification Report

SchwartzSubmodule

📁 Source: PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean

Statistics

Metric	Count
Definitions `instCoeFunSubtypeAEEqFunSpaceComplexVolumeMemAddSubgroupSubmoduleSchwartzSubmoduleForall`, `schwartzEquiv`, `schwartzIncl`, `schwartzSubmodule`	4
Theorems `schwartzEquiv_ae_eq`, `schwartzEquiv_coe_ae`, `schwartzEquiv_inner`, `schwartzSubmodule_dense`, `val_eq_coe`	5
Total	9

QuantumMechanics.SpaceDHilbertSpace

Definitions

Name	Category	Theorems
`instCoeFunSubtypeAEEqFunSpaceComplexVolumeMemAddSubgroupSubmoduleSchwartzSubmoduleForall` 📖	CompOp	—
`schwartzEquiv` 📖	CompOp	2 math math: `schwartzEquiv_inner`, `schwartzEquiv_coe_ae`
`schwartzIncl` 📖	CompOp	—
`schwartzSubmodule` 📖	CompOp	7 math math: `QuantumMechanics.radiusRegPowOperatorSchwartz_isSymmetric`, `QuantumMechanics.positionOperatorSchwartz_isSymmetric`, `schwartzEquiv_inner`, `QuantumMechanics.momentumOperatorSchwartz_isSymmetric`, `schwartzEquiv_coe_ae`, `val_eq_coe`, `schwartzSubmodule_dense`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`schwartzEquiv_ae_eq` 📖	—	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `Space.instFiniteDimensionalReal` `Space.instMeasurableSpace` `Space.instBorelSpace` `QuantumMechanics.SpaceDHilbertSpace` `schwartzSubmodule` `schwartzEquiv`	—	—	`Space.instFiniteDimensionalReal` `Space.instBorelSpace` `ext_iff`
`schwartzEquiv_coe_ae` 📖	mathematical	—	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `Space.instFiniteDimensionalReal` `Space.instMeasurableSpace` `Space.instBorelSpace` `QuantumMechanics.SpaceDHilbertSpace` `schwartzSubmodule` `schwartzEquiv`	—	`Space.instFiniteDimensionalReal` `Space.instBorelSpace`
`schwartzEquiv_inner` 📖	mathematical	—	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `Space.instFiniteDimensionalReal` `Space.instMeasurableSpace` `Space.instBorelSpace` `QuantumMechanics.SpaceDHilbertSpace` `schwartzSubmodule` `schwartzEquiv`	—	`Space.instFiniteDimensionalReal` `Space.instBorelSpace` `schwartzEquiv_coe_ae`
`schwartzSubmodule_dense` 📖	mathematical	—	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `Space.instFiniteDimensionalReal` `Space.instMeasurableSpace` `Space.instBorelSpace` `QuantumMechanics.SpaceDHilbertSpace` `schwartzSubmodule`	—	`Space.instFiniteDimensionalReal` `Space.instBorelSpace`
`val_eq_coe` 📖	mathematical	—	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `Space.instFiniteDimensionalReal` `Space.instMeasurableSpace` `Space.instBorelSpace` `QuantumMechanics.SpaceDHilbertSpace` `schwartzSubmodule`	—	`Space.instFiniteDimensionalReal` `Space.instBorelSpace`

---

← Back to Index