Robertson–Schrödinger uncertainty relation

DefinitionNormalized expectation value of an observable#✓fully proved

The normalized real expectation is Mathlib's canonical Rayleigh quotient. For a nonzero state and self-adjoint observable it is the physical expectation. At zero this total definition is zero; zero is not a physical state.

noncomputable def meanValue (A : E →L[ℂ] E) (x : E) : ℝ :=
  A.rayleighQuotient x

Used by 8

Used byCentered state vector of an observable · Commutator expectation as the skew part of the centered inner product · Inner product of two centered vectors · Flipped expectation inner product of a self-adjoint operator · Expectation inner product of a self-adjoint operator · Normalized expectation on a unit vector · Variance as second moment minus squared mean · Normalized variance is invariant under nonzero scaling

TheoremNormalized expectation on a unit vector#✓fully proved

On a unit vector, normalized expectation equals the original quadratic mean.

theorem meanValue_of_norm_eq_one (A : E →L[ℂ] E) {x : E} (hx : ‖x‖ = 1) :
    meanValue A x = (⟪A x, x⟫_ℂ).re

Uses 1

Statement usesNormalized expectation value of an observable

DefinitionCentered state vector of an observable#✓fully proved

The centered vector subtracts the normalized real expectation times the state. Its squared norm divided by the squared state norm is variance.

noncomputable def centered (A : E →L[ℂ] E) (x : E) : E :=
  A x - (meanValue A x : ℂ) • x

Uses 1 · Used by 11

Statement usesNormalized expectation value of an observable

Used byCommutator expectation as the skew part of the centered inner product · Commutator expectation of self-adjoint operators is purely imaginary · Inner product of two centered vectors · Norm of the commutator expectation · Squared norm of the commutator expectation · Robertson's uncertainty principle · Robertson–Schrödinger uncertainty principle · Normalized variance of an observable · Variance as second moment minus squared mean · Normalized variance on the unit sphere · Normalized variance is invariant under nonzero scaling

DefinitionNormalized variance of an observable#✓fully proved

Normalized variance is the centered squared norm divided by the squared state norm. For a nonzero state and self-adjoint observable it is the physical variance. The totalized value at zero is zero. Off the unit sphere this corrects the raw quadratic quantities; agreement with the original formulas is asserted only for unit states.

noncomputable def variance (A : E →L[ℂ] E) (x : E) : ℝ :=
  ‖centered A x‖ ^ 2 / ‖x‖ ^ 2

Uses 1 · Used by 5

Statement usesCentered state vector of an observable

Used byRobertson's uncertainty principle · Robertson–Schrödinger uncertainty principle · Variance as second moment minus squared mean · Normalized variance on the unit sphere · Normalized variance is invariant under nonzero scaling

TheoremNormalized variance on the unit sphere#✓fully proved

On the unit sphere, normalized variance is the centered squared norm.

theorem variance_of_norm_eq_one (A : E →L[ℂ] E) {x : E} (hx : ‖x‖ = 1) :
    variance A x = ‖centered A x‖ ^ 2

Uses 2

Statement usesCentered state vector of an observable · Normalized variance of an observable

TheoremNormalized variance is invariant under nonzero scaling#✓fully proved

Nonzero scalar multiplication does not change normalized variance.

theorem variance_smul (A : E →L[ℂ] E) (x : E) {c : ℂ} (hc : c ≠ 0) :
    variance A (c • x) = variance A x

Uses 3

Statement usesNormalized variance of an observable

Proof usesCentered state vector of an observable · Normalized expectation value of an observable

TheoremExpectation inner product of a self-adjoint operator#✓fully proved

For a self-adjoint operator, the expectation inner product is the normalized mean multiplied by the squared state norm. The norm factor is required off the unit sphere.

theorem inner_self_of_isSelfAdjoint {A : E →L[ℂ] E} (hA : IsSelfAdjoint A) (x : E) :
    ⟪A x, x⟫_ℂ = ((meanValue A x * ‖x‖ ^ 2 : ℝ) : ℂ)

Uses 1 · Used by 3

Statement usesNormalized expectation value of an observable

Used byInner product of two centered vectors · Flipped expectation inner product of a self-adjoint operator · Variance as second moment minus squared mean

TheoremFlipped expectation inner product of a self-adjoint operator#✓fully proved

The flipped expectation has the same necessary squared-state-norm factor.

theorem inner_right_of_isSelfAdjoint {A : E →L[ℂ] E} (hA : IsSelfAdjoint A) (x : E) :
    ⟪x, A x⟫_ℂ = ((meanValue A x * ‖x‖ ^ 2 : ℝ) : ℂ)

Uses 2 · Used by 2

Statement usesNormalized expectation value of an observable

Proof usesExpectation inner product of a self-adjoint operator

Used byInner product of two centered vectors · Variance as second moment minus squared mean

TheoremInner product of two centered vectors#✓fully proved

The inner product of two centered vectors, for self-adjoint operators at a unit vector: the uncentered inner product minus the product of the mean values.

theorem inner_centered {A B : E →L[ℂ] E} (hA : IsSelfAdjoint A) (hB : IsSelfAdjoint B)
    {x : E} (hx : ‖x‖ = 1) :
    ⟪centered A x, centered B x⟫_ℂ
      = ⟪A x, B x⟫_ℂ - (meanValue A x : ℂ) * (meanValue B x : ℂ)

Uses 4 · Used by 1

Statement usesCentered state vector of an observable · Normalized expectation value of an observable

Proof usesFlipped expectation inner product of a self-adjoint operator · Expectation inner product of a self-adjoint operator

Used byCommutator expectation as the skew part of the centered inner product

TheoremCommutator expectation as the skew part of the centered inner product#✓fully proved

The commutator expectation is the skew part of the inner product of the centered vectors.

theorem commutator_inner {A B : E →L[ℂ] E} (hA : IsSelfAdjoint A) (hB : IsSelfAdjoint B)
    {x : E} (hx : ‖x‖ = 1) :
    ⟪(A ∘L B - B ∘L A) x, x⟫_ℂ
      = ⟪centered B x, centered A x⟫_ℂ - ⟪centered A x, centered B x⟫_ℂ

Uses 3 · Used by 2

Statement usesCentered state vector of an observable

Proof usesInner product of two centered vectors · Normalized expectation value of an observable

Used byCommutator expectation of self-adjoint operators is purely imaginary · Squared norm of the commutator expectation

TheoremCommutator expectation of self-adjoint operators is purely imaginary#✓fully proved

The commutator expectation of two self-adjoint operators is purely imaginary: its real part vanishes.

theorem commutator_inner_re {A B : E →L[ℂ] E} (hA : IsSelfAdjoint A) (hB : IsSelfAdjoint B)
    {x : E} (hx : ‖x‖ = 1) :
    (⟪(A ∘L B - B ∘L A) x, x⟫_ℂ).re = 0

Uses 2

Proof usesCentered state vector of an observable · Commutator expectation as the skew part of the centered inner product

TheoremSquared norm of the commutator expectation#✓fully proved

The squared norm of the commutator expectation is four times the squared imaginary part of the centered inner product.

theorem norm_sq_commutator_inner {A B : E →L[ℂ] E} (hA : IsSelfAdjoint A)
    (hB : IsSelfAdjoint B) {x : E} (hx : ‖x‖ = 1) :
    ‖⟪(A ∘L B - B ∘L A) x, x⟫_ℂ‖ ^ 2
      = 4 * (⟪centered A x, centered B x⟫_ℂ).im ^ 2

Uses 2 · Used by 2

Statement usesCentered state vector of an observable

Proof usesCommutator expectation as the skew part of the centered inner product

Used byNorm of the commutator expectation · Robertson–Schrödinger uncertainty principle

TheoremNorm of the commutator expectation#✓fully proved

The commutator expectation has norm twice the absolute imaginary part of the centered inner product.

theorem norm_commutator_inner_eq {A B : E →L[ℂ] E} (hA : IsSelfAdjoint A)
    (hB : IsSelfAdjoint B) {x : E} (hx : ‖x‖ = 1) :
    ‖⟪(A ∘L B - B ∘L A) x, x⟫_ℂ‖
      = 2 * |(⟪centered A x, centered B x⟫_ℂ).im|

Uses 2

Statement usesCentered state vector of an observable

Proof usesSquared norm of the commutator expectation

TheoremRobertson–Schrödinger uncertainty principle#✓fully proved

The Robertson–Schrödinger uncertainty principle: the product of the variances is at least the squared covariance plus a quarter of the squared norm of the commutator expectation.

theorem schrodinger {A B : E →L[ℂ] E} (hA : IsSelfAdjoint A) (hB : IsSelfAdjoint B)
    {x : E} (hx : ‖x‖ = 1) :
    (⟪centered A x, centered B x⟫_ℂ).re ^ 2
        + (1 / 4) * ‖⟪(A ∘L B - B ∘L A) x, x⟫_ℂ‖ ^ 2
      ≤ variance A x * variance B x

Uses 3 · Used by 1

Statement usesCentered state vector of an observable · Normalized variance of an observable

Proof usesSquared norm of the commutator expectation

Used byRobertson's uncertainty principle

TheoremRobertson's uncertainty principle#✓fully proved

The product of the variances is at least a quarter of the squared norm of the commutator expectation.

theorem robertson {A B : E →L[ℂ] E} (hA : IsSelfAdjoint A) (hB : IsSelfAdjoint B)
    {x : E} (hx : ‖x‖ = 1) :
    (1 / 4) * ‖⟪(A ∘L B - B ∘L A) x, x⟫_ℂ‖ ^ 2
      ≤ variance A x * variance B x

Uses 3

Statement usesNormalized variance of an observable

Proof usesCentered state vector of an observable · Robertson–Schrödinger uncertainty principle

TheoremCommutator of commuting operators vanishes#✓fully proved

The commutator of commuting operators vanishes.

theorem commutator_eq_zero_of_commute {A B : E →L[ℂ] E} (h : Commute A B) :
    A ∘L B - B ∘L A = 0

TheoremVariance as second moment minus squared mean#✓fully proved

The variance is the second moment minus the squared mean.

theorem variance_eq {A : E →L[ℂ] E} (hA : IsSelfAdjoint A) {x : E} (hx : ‖x‖ = 1) :
    variance A x = (⟪(A * A) x, x⟫_ℂ).re - (meanValue A x) ^ 2

Uses 5

Statement usesNormalized expectation value of an observable · Normalized variance of an observable

Proof usesCentered state vector of an observable · Flipped expectation inner product of a self-adjoint operator · Expectation inner product of a self-adjoint operator

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.