Physlib

Physlib.QuantumMechanics.DDimensions.Operators.StateObservables.ExpectedValue

Expectation values and centered vectors

For a partial linear map `T` on a complex inner product space and `ψ ∈ T.domain`, this file defines the expectation value and the centered vector `Tψ - ⟨T⟩_ψ ψ`.

Main definitions

  • `LinearPMap.expectedValue`: the real part of `⟪ψ, Tψ⟫_ℂ`.
  • `LinearPMap.centered`: the centered vector `Tψ - ⟨T⟩ψ`.

Main statements

- `LinearPMap.expectedValue_eq_inner`: for symmetric `T`, the complex inner product is real and equals the real expectation value coerced to `ℂ`.

References

  • [B. C. Hall, *Quantum Theory for Mathematicians*, Chapter 12][hall2013quantum].

9 declarations

definition

Expectation value Re⟨ψ,Tψ⟩\text{Re} \langle \psi, T\psi \rangle of a partial linear map

Given a complex inner product space HH, a partial linear map TT on HH, and a vector ψ\psi in the domain of TT, the expectation value is defined as the real part of the complex inner product of ψ\psi and TψT\psi, denoted as Re⟨ψ,Tψ⟩\text{Re} \langle \psi, T\psi \rangle.

theorem

Expectation Value Equals Re⁡⟨ψ,Tψ⟩\operatorname{Re} \langle \psi, T\psi \rangle

Let HH be a complex inner product space, TT a partial linear map on HH, and ψ\psi a vector in the domain of TT. The expectation value of TT with respect to ψ\psi is equal to the real part of the complex inner product of ψ\psi and TψT\psi, denoted as Re⁡⟨ψ,Tψ⟩\operatorname{Re} \langle \psi, T\psi \rangle.

theorem

⟨ψ,Tψ⟩=⟨T⟩ψ\langle \psi, T\psi \rangle = \langle T \rangle_\psi for symmetric TT

Let HH be a complex inner product space and TT be a symmetric partial linear map on HH. For any vector ψ\psi in the domain of TT, the complex inner product ⟨ψ,Tψ⟩\langle \psi, T\psi \rangle is equal to the expectation value ⟨T⟩ψ\langle T \rangle_\psi (defined as Re⟨ψ,Tψ⟩\text{Re} \langle \psi, T\psi \rangle) coerced to a complex number.

theorem

For symmetric TT, expectedValue(T,ψ)=⟨ψ,Tψ⟩\text{expectedValue}(T, \psi) = \langle \psi, T\psi \rangle

Let HH be a complex inner product space and TT be a symmetric partial linear map on HH. For any vector ψ\psi in the domain of TT, the expectation value of TT with respect to ψ\psi (defined as Re⟨ψ,Tψ⟩\text{Re} \langle \psi, T\psi \rangle) is equal to the complex inner product ⟨ψ,Tψ⟩\langle \psi, T\psi \rangle when considered as a complex number.

definition

Centered vector Tψ−⟨T⟩ψψT\psi - \langle T \rangle_\psi \psi

Given a partial linear map TT on a complex inner product space HH and a vector ψ\psi in the domain of TT, the centered vector is defined as Tψ−⟨T⟩ψψT\psi - \langle T \rangle_\psi \psi, where ⟨T⟩ψ=Re⟨ψ,Tψ⟩\langle T \rangle_\psi = \text{Re} \langle \psi, T\psi \rangle is the expectation value of TT with respect to ψ\psi.

theorem

centered(T,ψ)=Tψ−⟨T⟩ψψ\text{centered}(T, \psi) = T\psi - \langle T \rangle_\psi \psi

Let HH be a complex inner product space, TT be a partial linear map on HH, and ψ\psi be a vector in the domain of TT. The centered vector of TT with respect to ψ\psi is equal to Tψ−⟨T⟩ψψT\psi - \langle T \rangle_\psi \psi, where ⟨T⟩ψ=Re⟨ψ,Tψ⟩\langle T \rangle_\psi = \text{Re} \langle \psi, T\psi \rangle is the expectation value of TT with respect to ψ\psi.

theorem

The centered vector of TT at ψ\psi is zero if and only if Tψ=⟨T⟩ψψT\psi = \langle T \rangle_\psi \psi

Let HH be a complex inner product space and TT be a partial linear map on HH. For any vector ψ\psi in the domain of TT, the centered vector, defined as Tψ−⟨T⟩ψψT\psi - \langle T \rangle_\psi \psi, is equal to zero if and only if Tψ=⟨T⟩ψψT\psi = \langle T \rangle_\psi \psi, where ⟨T⟩ψ=Re⟨ψ,Tψ⟩\langle T \rangle_\psi = \text{Re} \langle \psi, T\psi \rangle is the expectation value of TT with respect to ψ\psi.

theorem

⟨ψ,centered Tψ⟩=0\langle \psi, \text{centered } T \psi \rangle = 0 for symmetric TT and unit vector ψ\psi

Let HH be a complex inner product space and TT be a symmetric partial linear map on HH. For any vector ψ\psi in the domain of TT with unit norm (i.e., ∥ψ∥=1\|\psi\| = 1), the complex inner product of ψ\psi with the centered vector is zero: ⟨ψ,centered Tψ⟩C=0\langle \psi, \text{centered } T \psi \rangle_{\mathbb{C}} = 0 where the centered vector is defined as centered Tψ=Tψ−⟨T⟩ψψ\text{centered } T \psi = T\psi - \langle T \rangle_\psi \psi and ⟨T⟩ψ=Re⟨ψ,Tψ⟩C\langle T \rangle_\psi = \text{Re} \langle \psi, T\psi \rangle_{\mathbb{C}} is the expectation value of TT with respect to ψ\psi.

theorem

The inner product of the centered vector and the state ψ\psi is zero: ⟨Tψ−⟨T⟩ψψ,ψ⟩=0\langle T\psi - \langle T \rangle_\psi \psi, \psi \rangle = 0

Let HH be a complex inner product space and TT be a symmetric partial linear map on HH. For any unit vector ψ\psi in the domain of TT (i.e., ∥ψ∥=1\|\psi\| = 1), the complex inner product of the centered vector Tψ−⟨T⟩ψψT\psi - \langle T \rangle_\psi \psi and the vector ψ\psi is zero, where ⟨T⟩ψ=Re⟨ψ,Tψ⟩\langle T \rangle_\psi = \text{Re} \langle \psi, T\psi \rangle is the expectation value of TT with respect to ψ\psi. That is, ⟨Tψ−⟨T⟩ψψ,ψ⟩=0.\langle T\psi - \langle T \rangle_\psi \psi, \psi \rangle = 0.