Unbounded

📁 Source: PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean

Statistics

Metric	Count
Definitions `UnboundedOperator`, `IsClosed`, `IsEssentiallySelfAdjoint`, `IsGeneralizedEigenvector`, `IsSymmetric`, `adjoint`, `closure`, `instAdd`, `instAddZeroClass`, `instCoeFunForallSubtypeMemSubmoduleComplexDomain`, `instDistribSMulComplex`, `instInhabited`, `instPartialOrder`, `instSMulComplex`, `instStar`, `instZero`, `ofSymmetric`, `toLinearPMap`, `«term_†»`	19
Theorems `add_apply_of_dense_closable`, `add_assoc`, `add_domain_of_dense`, `add_domain_of_not_dense`, `add_toLinearPMap_of_dense_closable`, `add_toLinearPMap_of_dense_not_closable`, `add_toLinearPMap_of_not_dense`, `adjoint_adjoint_eq_closure`, `adjoint_closure_eq_adjoint`, `adjoint_dense_of_isClosable`, `adjoint_ge_adjoint_of_le`, `adjoint_isClosed`, `adjoint_toLinearPMap`, `closure_adjoint_eq_adjoint`, `closure_isClosed`, `closure_mono`, `closure_toLinearPMap`, `dense_domain`, `ext`, `ext_iff`, `inner_map_polarization`, `inner_map_polarization'`, `isClosable_of_zero`, `isClosed_def`, `isClosed_iff`, `isClosed_of_isSelfAdjoint`, `isEssentiallySelfAdjoint_def`, `isGeneralizedEigenvector_ofSymmetric_iff`, `isSelfAdjoint_def`, `isSelfAdjoint_iff`, `isSelfAdjoint_isEssentiallySelfAdjoint`, `isSymmetric_iff_inner_map_self_real`, `isSymmetric_iff_le_adjoint`, `isSymmetric_of_isSelfAdjoint`, `is_closable`, `le_adjoint_adjoint`, `le_closure`, `mem_domain_of_dense`, `ofSymmetric_apply`, `smul_domain`, `smul_isClosable_of_isClosable`, `smul_mem_graph_of_mem_smul_graph`, `smul_toLinearPMap`, `zero_smul_le_zero`, `zero_toLinearPMap`	45
Total	64

QuantumMechanics

Definitions

Name	Category	Theorems
`UnboundedOperator` 📖	CompData	19 math math: `UnboundedOperator.add_assoc`, `UnboundedOperator.add_toLinearPMap_of_dense_not_closable`, `UnboundedOperator.adjoint_ge_adjoint_of_le`, `UnboundedOperator.smul_domain`, `UnboundedOperator.isSymmetric_iff_le_adjoint`, `UnboundedOperator.closure_mono`, `UnboundedOperator.mem_domain_of_dense`, `UnboundedOperator.add_toLinearPMap_of_not_dense`, `UnboundedOperator.zero_smul_le_zero`, `UnboundedOperator.le_closure`, `UnboundedOperator.le_adjoint_adjoint`, `UnboundedOperator.add_domain_of_dense`, `UnboundedOperator.isSelfAdjoint_def`, `UnboundedOperator.isSelfAdjoint_iff`, `UnboundedOperator.smul_toLinearPMap`, `UnboundedOperator.add_apply_of_dense_closable`, `UnboundedOperator.zero_toLinearPMap`, `UnboundedOperator.add_toLinearPMap_of_dense_closable`, `UnboundedOperator.add_domain_of_not_dense`

QuantumMechanics.UnboundedOperator

Definitions

Name	Category	Theorems
`IsClosed` 📖	MathDef	5 math math: `closure_isClosed`, `isClosed_iff`, `isClosed_def`, `adjoint_isClosed`, `isClosed_of_isSelfAdjoint`
`IsEssentiallySelfAdjoint` 📖	MathDef	2 math math: `isSelfAdjoint_isEssentiallySelfAdjoint`, `isEssentiallySelfAdjoint_def`
`IsGeneralizedEigenvector` 📖	MathDef	1 math math: `isGeneralizedEigenvector_ofSymmetric_iff`
`IsSymmetric` 📖	MathDef	3 math math: `isSymmetric_iff_le_adjoint`, `isSymmetric_of_isSelfAdjoint`, `isSymmetric_iff_inner_map_self_real`
`adjoint` 📖	CompOp	11 math math: `adjoint_toLinearPMap`, `adjoint_ge_adjoint_of_le`, `isSymmetric_iff_le_adjoint`, `le_adjoint_adjoint`, `adjoint_closure_eq_adjoint`, `isClosed_iff`, `isSelfAdjoint_def`, `isEssentiallySelfAdjoint_def`, `adjoint_adjoint_eq_closure`, `adjoint_isClosed`, `closure_adjoint_eq_adjoint`
`closure` 📖	CompOp	9 math math: `closure_toLinearPMap`, `closure_mono`, `le_closure`, `closure_isClosed`, `adjoint_closure_eq_adjoint`, `isEssentiallySelfAdjoint_def`, `isClosed_def`, `adjoint_adjoint_eq_closure`, `closure_adjoint_eq_adjoint`
`instAdd` 📖	CompOp	8 math math: `add_assoc`, `add_toLinearPMap_of_dense_not_closable`, `mem_domain_of_dense`, `add_toLinearPMap_of_not_dense`, `add_domain_of_dense`, `add_apply_of_dense_closable`, `add_toLinearPMap_of_dense_closable`, `add_domain_of_not_dense`
`instAddZeroClass` 📖	CompOp	—
`instCoeFunForallSubtypeMemSubmoduleComplexDomain` 📖	CompOp	—
`instDistribSMulComplex` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	6 math math: `adjoint_ge_adjoint_of_le`, `isSymmetric_iff_le_adjoint`, `closure_mono`, `zero_smul_le_zero`, `le_closure`, `le_adjoint_adjoint`
`instSMulComplex` 📖	CompOp	3 math math: `smul_domain`, `zero_smul_le_zero`, `smul_toLinearPMap`
`instStar` 📖	CompOp	2 math math: `isSelfAdjoint_def`, `isSelfAdjoint_iff`
`instZero` 📖	CompOp	2 math math: `zero_smul_le_zero`, `zero_toLinearPMap`
`ofSymmetric` 📖	CompOp	2 math math: `isGeneralizedEigenvector_ofSymmetric_iff`, `ofSymmetric_apply`
`toLinearPMap` 📖	CompOp	20 math math: `dense_domain`, `adjoint_toLinearPMap`, `add_toLinearPMap_of_dense_not_closable`, `smul_domain`, `closure_toLinearPMap`, `mem_domain_of_dense`, `ext_iff`, `inner_map_polarization`, `inner_map_polarization'`, `add_toLinearPMap_of_not_dense`, `add_domain_of_dense`, `isSelfAdjoint_iff`, `ofSymmetric_apply`, `smul_toLinearPMap`, `add_apply_of_dense_closable`, `is_closable`, `isSymmetric_iff_inner_map_self_real`, `zero_toLinearPMap`, `add_toLinearPMap_of_dense_closable`, `add_domain_of_not_dense`
`«term_†»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply_of_dense_closable` 📖	mathematical	`toLinearPMap`	`toLinearPMap` `QuantumMechanics.UnboundedOperator` `instAdd` `mem_domain_of_dense`	—	`mem_domain_of_dense` `add_toLinearPMap_of_dense_closable`
`add_assoc` 📖	mathematical	`toLinearPMap`	`QuantumMechanics.UnboundedOperator` `instAdd`	—	`ext` `add_domain_of_dense` `add_toLinearPMap_of_dense_closable` `add_toLinearPMap_of_dense_not_closable` `add_toLinearPMap_of_not_dense`
`add_domain_of_dense` 📖	mathematical	`toLinearPMap`	`toLinearPMap` `QuantumMechanics.UnboundedOperator` `instAdd`	—	`HAdd.hAdd.eq_1` `instHAdd.eq_1` `Add.add.eq_1` `instAdd.eq_1`
`add_domain_of_not_dense` 📖	mathematical	`toLinearPMap`	`toLinearPMap` `QuantumMechanics.UnboundedOperator` `instAdd`	—	`HAdd.hAdd.eq_1` `instHAdd.eq_1` `Add.add.eq_1` `instAdd.eq_1`
`add_toLinearPMap_of_dense_closable` 📖	mathematical	`toLinearPMap`	`toLinearPMap` `QuantumMechanics.UnboundedOperator` `instAdd`	—	`HAdd.hAdd.eq_1` `instHAdd.eq_1` `Add.add.eq_1` `instAdd.eq_1`
`add_toLinearPMap_of_dense_not_closable` 📖	mathematical	`toLinearPMap`	`toLinearPMap` `QuantumMechanics.UnboundedOperator` `instAdd`	—	`HAdd.hAdd.eq_1` `instHAdd.eq_1` `Add.add.eq_1` `instAdd.eq_1`
`add_toLinearPMap_of_not_dense` 📖	mathematical	`toLinearPMap`	`toLinearPMap` `QuantumMechanics.UnboundedOperator` `instAdd`	—	`HAdd.hAdd.eq_1` `instHAdd.eq_1` `Add.add.eq_1` `instAdd.eq_1`
`adjoint_adjoint_eq_closure` 📖	mathematical	—	`adjoint` `closure`	—	`ext` `adjoint_toLinearPMap` `dense_domain` `closure_toLinearPMap` `is_closable` `InnerProductSpaceSubmodule.mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal` `InnerProductSpaceSubmodule.mem_submodule_closure_iff_mem_submoduleToLp_closure`
`adjoint_closure_eq_adjoint` 📖	mathematical	—	`closure` `adjoint`	—	`isClosed_def` `adjoint_isClosed`
`adjoint_dense_of_isClosable` 📖	—	—	—	—	`InnerProductSpaceSubmodule.mem_submodule_closure_iff_mem_submoduleToLp_closure` `InnerProductSpaceSubmodule.mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal` `InnerProductSpaceSubmodule.mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal`
`adjoint_ge_adjoint_of_le` 📖	mathematical	`QuantumMechanics.UnboundedOperator` `instPartialOrder`	`QuantumMechanics.UnboundedOperator` `instPartialOrder` `adjoint`	—	`dense_domain`
`adjoint_isClosed` 📖	mathematical	—	`IsClosed` `adjoint`	—	`dense_domain`
`adjoint_toLinearPMap` 📖	mathematical	—	`toLinearPMap` `adjoint`	—	—
`closure_adjoint_eq_adjoint` 📖	mathematical	—	`adjoint` `closure`	—	`ext` `adjoint_toLinearPMap` `dense_domain` `closure_toLinearPMap` `is_closable` `InnerProductSpaceSubmodule.mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal` `InnerProductSpaceSubmodule.mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal`
`closure_isClosed` 📖	mathematical	—	`IsClosed` `closure`	—	`is_closable`
`closure_mono` 📖	mathematical	`QuantumMechanics.UnboundedOperator` `instPartialOrder`	`QuantumMechanics.UnboundedOperator` `instPartialOrder` `closure`	—	`adjoint_adjoint_eq_closure` `adjoint_ge_adjoint_of_le`
`closure_toLinearPMap` 📖	mathematical	—	`toLinearPMap` `closure`	—	—
`dense_domain` 📖	mathematical	—	`toLinearPMap`	—	—
`ext` 📖	—	`toLinearPMap`	—	—	—
`ext_iff` 📖	mathematical	—	`toLinearPMap`	—	`ext`
`inner_map_polarization` 📖	mathematical	—	`toLinearPMap`	—	—
`inner_map_polarization'` 📖	mathematical	—	`toLinearPMap`	—	—
`isClosable_of_zero` 📖	—	—	—	—	—
`isClosed_def` 📖	mathematical	—	`IsClosed` `closure`	—	`ext_iff` `closure_toLinearPMap` `is_closable` `closure_isClosed`
`isClosed_iff` 📖	mathematical	—	`IsClosed` `adjoint`	—	`isClosed_def` `adjoint_adjoint_eq_closure`
`isClosed_of_isSelfAdjoint` 📖	mathematical	`QuantumMechanics.UnboundedOperator` `instStar`	`IsClosed`	—	`adjoint_isClosed`
`isEssentiallySelfAdjoint_def` 📖	mathematical	—	`IsEssentiallySelfAdjoint` `adjoint` `closure`	—	`IsEssentiallySelfAdjoint.eq_1` `isSelfAdjoint_def` `closure_adjoint_eq_adjoint`
`isGeneralizedEigenvector_ofSymmetric_iff` 📖	mathematical	—	`IsGeneralizedEigenvector` `ofSymmetric`	—	—
`isSelfAdjoint_def` 📖	mathematical	—	`QuantumMechanics.UnboundedOperator` `instStar` `adjoint`	—	—
`isSelfAdjoint_iff` 📖	mathematical	—	`QuantumMechanics.UnboundedOperator` `instStar` `toLinearPMap`	—	`isSelfAdjoint_def` `adjoint_toLinearPMap` `ext_iff`
`isSelfAdjoint_isEssentiallySelfAdjoint` 📖	mathematical	`QuantumMechanics.UnboundedOperator` `instStar`	`IsEssentiallySelfAdjoint`	—	`isEssentiallySelfAdjoint_def` `adjoint_closure_eq_adjoint`
`isSymmetric_iff_inner_map_self_real` 📖	mathematical	—	`IsSymmetric` `toLinearPMap`	—	`inner_map_polarization` `inner_map_polarization'`
`isSymmetric_iff_le_adjoint` 📖	mathematical	—	`IsSymmetric` `QuantumMechanics.UnboundedOperator` `instPartialOrder` `adjoint`	—	`dense_domain`
`isSymmetric_of_isSelfAdjoint` 📖	mathematical	`QuantumMechanics.UnboundedOperator` `instStar`	`IsSymmetric`	—	`isSymmetric_iff_le_adjoint`
`is_closable` 📖	mathematical	—	`toLinearPMap`	—	—
`le_adjoint_adjoint` 📖	mathematical	—	`QuantumMechanics.UnboundedOperator` `instPartialOrder` `adjoint`	—	`le_closure` `adjoint_adjoint_eq_closure`
`le_closure` 📖	mathematical	—	`QuantumMechanics.UnboundedOperator` `instPartialOrder` `closure`	—	—
`mem_domain_of_dense` 📖	mathematical	`toLinearPMap`	`toLinearPMap` `QuantumMechanics.UnboundedOperator` `instAdd`	—	`add_domain_of_dense`
`ofSymmetric_apply` 📖	mathematical	—	`toLinearPMap` `ofSymmetric`	—	—
`smul_domain` 📖	mathematical	—	`toLinearPMap` `QuantumMechanics.UnboundedOperator` `instSMulComplex`	—	—
`smul_isClosable_of_isClosable` 📖	—	—	—	—	`isClosable_of_zero` `smul_mem_graph_of_mem_smul_graph`
`smul_mem_graph_of_mem_smul_graph` 📖	—	—	—	—	—
`smul_toLinearPMap` 📖	mathematical	—	`toLinearPMap` `QuantumMechanics.UnboundedOperator` `instSMulComplex`	—	—
`zero_smul_le_zero` 📖	mathematical	—	`QuantumMechanics.UnboundedOperator` `instPartialOrder` `instSMulComplex` `instZero`	—	—
`zero_toLinearPMap` 📖	mathematical	—	`toLinearPMap` `QuantumMechanics.UnboundedOperator` `instZero`	—	—

---

← Back to Index