Position

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

Statistics

Metric	Count
Definitions normRegularizedPow, positionOperator, positionOperatorSchwartz, positionUnboundedOperator, radiusPowOperator, radiusRegPowOperator, radiusRegPowOperatorSchwartz, radiusRegPowUnboundedOperator, «term𝐫[_,_,_]», «term𝐫[_,_]», «term𝐫[_]», «term𝐱[_]»	12
Theorems normRegularizedPow_hasTemperateGrowth, normRegularizedPow_pos, norm_sq_add_unit_sq_pos, positionOperatorSchwartz_isSymmetric, positionOperatorSqr_eq, positionOperator_apply, positionOperator_apply_fun, radiusPowOperator_apply, radiusPowOperator_apply_contDiffAt, radiusPowOperator_apply_fun, radiusPowOperator_apply_memHS, radiusPowOperator_apply_stronglyMeasurable, radiusRegPowOperatorSchwartz_isSymmetric, radiusRegPowOperator_apply, radiusRegPowOperator_apply_fun, radiusRegPowOperator_comp_eq, radiusRegPowOperator_zero	17
Total	29

QuantumMechanics

Definitions

Name	Category	Theorems
normRegularizedPow 📖	CompOp	2 math math: normRegularizedPow_pos, normRegularizedPow_hasTemperateGrowth
positionOperator 📖	CompOp	22 math math: radiusRegPow_commutation_momentumSqr, position_comp_radiusRegPow_commute, position_commutation_momentum_momentum, position_commutation_radiusRegPow, positionOperatorSqr_eq, angularMomentum_commutation_position, positionOperator_apply, radiusRegPow_commutation_momentum, angularMomentumOperator_apply_fun, HydrogenAtom.lrlOperator_eq'', position_commutation_momentum, momentum_comp_position_eq, position_commutation_momentumSqr, HydrogenAtom.hamiltonianReg_commutation_lrl, position_commutation_position, HydrogenAtom.lrlOperator_eq', position_position_commutation_momentum, positionOperator_apply_fun, HydrogenAtom.lrlOperator_eq, angularMomentumOperator_apply, position_comp_commute, momentum_comp_radiusRegPow_eq
positionOperatorSchwartz 📖	CompOp	1 math math: positionOperatorSchwartz_isSymmetric
positionUnboundedOperator 📖	CompOp	—
radiusPowOperator 📖	CompOp	5 math math: radiusPowOperator_apply_stronglyMeasurable, radiusPowOperator_apply, radiusPowOperator_apply_fun, radiusPowOperator_apply_memHS, radiusPowOperator_apply_contDiffAt
radiusRegPowOperator 📖	CompOp	18 math math: angularMomentum_commutation_radiusRegPow, radiusRegPow_commutation_momentumSqr, radiusRegPowOperator_apply, position_comp_radiusRegPow_commute, position_commutation_radiusRegPow, radiusRegPowOperator_apply_fun, positionOperatorSqr_eq, radiusRegPow_commutation_momentum, angularMomentumSqr_commutation_radiusRegPow, HydrogenAtom.lrlOperator_eq'', HydrogenAtom.hamiltonianReg_commutation_lrl, HydrogenAtom.lrlOperator_eq', HydrogenAtom.lrlOperatorSqr_eq, HydrogenAtom.lrlOperator_eq, radiusRegPowOperator_comp_eq, radiusRegPowOperator_zero, momentum_comp_radiusRegPow_eq, radiusRegPow_commutation_radiusRegPow
radiusRegPowOperatorSchwartz 📖	CompOp	1 math math: radiusRegPowOperatorSchwartz_isSymmetric
radiusRegPowUnboundedOperator 📖	CompOp	—
«term𝐫[_,_,_]» 📖	CompOp	—
«term𝐫[_,_]» 📖	CompOp	—
«term𝐫[_]» 📖	CompOp	—
«term𝐱[_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
normRegularizedPow_hasTemperateGrowth 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal normRegularizedPow	—	—
normRegularizedPow_pos 📖	mathematical	—	normRegularizedPow	—	norm_sq_add_unit_sq_pos
norm_sq_add_unit_sq_pos 📖	mathematical	—	Space Space.instNorm	—	—
positionOperatorSchwartz_isSymmetric 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace SpaceDHilbertSpace SpaceDHilbertSpace.schwartzSubmodule positionOperatorSchwartz	—	Space.instFiniteDimensionalReal Space.instBorelSpace SpaceDHilbertSpace.schwartzEquiv_inner positionOperator_apply
positionOperatorSqr_eq 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator radiusRegPowOperator	—	positionOperator_apply radiusRegPowOperator_apply Space.norm_sq_eq
positionOperator_apply 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator Space.val	—	positionOperator_apply_fun
positionOperator_apply_fun 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator Space.val	—	Space.coordCLM_apply Space.coord_apply
radiusPowOperator_apply 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal radiusPowOperator Space.instNorm	—	radiusPowOperator_apply_fun
radiusPowOperator_apply_contDiffAt 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal radiusPowOperator	—	Space.inner_apply_contDiff
radiusPowOperator_apply_fun 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal radiusPowOperator Space.instNorm	—	—
radiusPowOperator_apply_memHS 📖	mathematical	—	SpaceDHilbertSpace.MemHS Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal radiusPowOperator	—	Space.instFiniteDimensionalReal Space.instBorelSpace Space.instSubsingletonOfNatNat radiusPowOperator_apply_stronglyMeasurable Space.integrableOn_norm_rpow_ball_iff Space.integrableOn_norm_rpow_ball_compl_iff
radiusPowOperator_apply_stronglyMeasurable 📖	mathematical	—	Space Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal radiusPowOperator	—	radiusPowOperator_apply_fun Space.instBorelSpace
radiusRegPowOperatorSchwartz_isSymmetric 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace SpaceDHilbertSpace SpaceDHilbertSpace.schwartzSubmodule radiusRegPowOperatorSchwartz	—	Space.instFiniteDimensionalReal Space.instBorelSpace SpaceDHilbertSpace.schwartzEquiv_inner radiusRegPowOperator_apply
radiusRegPowOperator_apply 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal radiusRegPowOperator Space.instNorm	—	radiusRegPowOperator_apply_fun
radiusRegPowOperator_apply_fun 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal radiusRegPowOperator Space.instNorm	—	normRegularizedPow_hasTemperateGrowth
radiusRegPowOperator_comp_eq 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal radiusRegPowOperator	—	radiusRegPowOperator_apply norm_sq_add_unit_sq_pos
radiusRegPowOperator_zero 📖	mathematical	—	radiusRegPowOperator Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal	—	radiusRegPowOperator_apply

---

← Back to Index