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.

def LinearPMap.expectedValue {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (ψ : ↥T.domain) : ℝ

Expectation value re ⟪ψ, Tψ⟫_ℂ for ψ ∈ T.domain.

For symmetric T, this agrees with ⟪ψ, Tψ⟫_ℂ after coercion from ℝ; see expectedValue_eq_inner.

Equations

• T.expectedValue ψ = (inner ℂ (↑ψ) (↑T ψ)).re

theorem LinearPMap.expectedValue_eq_re_inner {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (ψ : ↥T.domain) : T.expectedValue ψ = (inner ℂ (↑ψ) (↑T ψ)).re

The expectation value, unfolded as a real part.

theorem LinearPMap.expectedValue_eq_inner {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (hT : T.IsSymmetric) (ψ : ↥T.domain) : inner ℂ (↑ψ) (↑T ψ) = ↑(T.expectedValue ψ)

If T is symmetric, ⟪ψ, Tψ⟫_ℂ is the expectation value, coerced to ℂ.

theorem LinearPMap.inner_eq_expectedValue {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (hT : T.IsSymmetric) (ψ : ↥T.domain) : ↑(T.expectedValue ψ) = inner ℂ (↑ψ) (↑T ψ)

Reverse orientation of LinearPMap.expectedValue_eq_inner.

def LinearPMap.centered {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (ψ : ↥T.domain) : H

The centered vector Tψ - ⟨T⟩_ψ ψ.

Equations

• T.centered ψ = ↑T ψ - ↑(T.expectedValue ψ) • ↑ψ

theorem LinearPMap.centered_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (ψ : ↥T.domain) : T.centered ψ = ↑T ψ - ↑(T.expectedValue ψ) • ↑ψ

The centered vector, unfolded to its raw expression.

theorem LinearPMap.centered_eq_zero_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (ψ : ↥T.domain) : T.centered ψ = 0 ↔ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ

A centered vector vanishes exactly when Tψ = ⟨T⟩_ψ ψ.

theorem LinearPMap.inner_state_centered_eq_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (hT : T.IsSymmetric) (ψ : ↥T.domain) (hψ_norm : ‖↑ψ‖ = 1) : inner ℂ (↑ψ) (T.centered ψ) = 0

For a unit vector and symmetric T, the centered vector is orthogonal to the state.

theorem LinearPMap.inner_centered_state_eq_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (hT : T.IsSymmetric) (ψ : ↥T.domain) (hψ_norm : ‖↑ψ‖ = 1) : inner ℂ (T.centered ψ) ↑ψ = 0

The conjugate orientation of LinearPMap.inner_state_centered_eq_zero.