Basic

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

Statistics

Metric	Count
Definitions SpaceDHilbertSpace, MemHS, mk, toBra	4
Theorems aeEqFun_mk_mem_iff, aeStronglyMeasurable_of_memHS, coe_hilbertSpace_memHS, coe_mk_ae, eLpNorm_mk, ext_iff, inner_mk_mk, memHS_add, memHS_const_smul, memHS_iff, memHS_of_ae, mem_iff, mk_add, mk_const_smul, mk_eq_iff, mk_surjective, toBra_apply, toBra_injective, toBra_surjective, zero_fun_memHS, zero_memHS	21
Total	25

QuantumMechanics

Definitions

Name	Category	Theorems
SpaceDHilbertSpace 📖	CompOp	15 math math: radiusRegPowOperatorSchwartz_isSymmetric, SpaceDHilbertSpace.toBra_surjective, SpaceDHilbertSpace.toBra_injective, SpaceDHilbertSpace.inner_mk_mk, positionOperatorSchwartz_isSymmetric, SpaceDHilbertSpace.mk_add, SpaceDHilbertSpace.schwartzEquiv_inner, SpaceDHilbertSpace.mem_iff, momentumOperatorSchwartz_isSymmetric, SpaceDHilbertSpace.schwartzEquiv_coe_ae, SpaceDHilbertSpace.aeEqFun_mk_mem_iff, SpaceDHilbertSpace.val_eq_coe, SpaceDHilbertSpace.schwartzSubmodule_dense, SpaceDHilbertSpace.toBra_apply, SpaceDHilbertSpace.mk_const_smul

QuantumMechanics.SpaceDHilbertSpace

Definitions

Name	Category	Theorems
MemHS 📖	MathDef	10 math math: memHS_iff, zero_memHS, coe_hilbertSpace_memHS, memHS_of_ae, memHS_const_smul, memHS_add, QuantumMechanics.radiusPowOperator_apply_memHS, aeEqFun_mk_mem_iff, mk_surjective, zero_fun_memHS
mk 📖	CompOp	—
toBra 📖	CompOp	3 math math: toBra_surjective, toBra_injective, toBra_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeEqFun_mk_mem_iff 📖	mathematical	Space Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace	Space Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace QuantumMechanics.SpaceDHilbertSpace MemHS	—	Space.instFiniteDimensionalReal Space.instBorelSpace
aeStronglyMeasurable_of_memHS 📖	mathematical	MemHS	Space Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace
coe_hilbertSpace_memHS 📖	mathematical	—	MemHS Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace aeEqFun_mk_mem_iff
coe_mk_ae 📖	mathematical	MemHS	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace
eLpNorm_mk 📖	mathematical	MemHS	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace coe_mk_ae
ext_iff 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace
inner_mk_mk 📖	mathematical	MemHS	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace QuantumMechanics.SpaceDHilbertSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace coe_mk_ae
memHS_add 📖	mathematical	MemHS	MemHS Space	—	Space.instFiniteDimensionalReal Space.instBorelSpace
memHS_const_smul 📖	mathematical	MemHS	MemHS Space	—	Space.instFiniteDimensionalReal Space.instBorelSpace
memHS_iff 📖	mathematical	—	MemHS Space Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace MemHS.eq_1
memHS_of_ae 📖	mathematical	MemHS Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace	MemHS	—	Space.instFiniteDimensionalReal Space.instBorelSpace
mem_iff 📖	mathematical	Space Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace	Space Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace QuantumMechanics.SpaceDHilbertSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace
mk_add 📖	mathematical	MemHS	Space memHS_add Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace QuantumMechanics.SpaceDHilbertSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace memHS_add
mk_const_smul 📖	mathematical	MemHS	Space memHS_const_smul Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace QuantumMechanics.SpaceDHilbertSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace memHS_const_smul
mk_eq_iff 📖	mathematical	MemHS	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace
mk_surjective 📖	mathematical	—	MemHS	—	Space.instFiniteDimensionalReal Space.instBorelSpace coe_hilbertSpace_memHS
toBra_apply 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace QuantumMechanics.SpaceDHilbertSpace toBra	—	Space.instFiniteDimensionalReal Space.instBorelSpace
toBra_injective 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace QuantumMechanics.SpaceDHilbertSpace toBra	—	Space.instFiniteDimensionalReal Space.instBorelSpace
toBra_surjective 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace QuantumMechanics.SpaceDHilbertSpace toBra	—	Space.instFiniteDimensionalReal Space.instBorelSpace
zero_fun_memHS 📖	mathematical	—	MemHS	—	zero_memHS
zero_memHS 📖	mathematical	—	MemHS Space	—	Space.instFiniteDimensionalReal Space.instBorelSpace memHS_iff

---

← Back to Index