Variance and standard deviation

The variance of a partial linear map T in a state ψ is ‖Tψ - ⟨T⟩_ψ ψ‖ ^ 2. It only requires ψ ∈ T.domain.

When T is symmetric, ‖ψ‖ = 1, and Tψ ∈ T.domain, it also equals ⟨T^2⟩_ψ - ⟨T⟩_ψ ^ 2.

Main definitions

• LinearPMap.variance and LinearPMap.standardDeviation.

Main statements

• LinearPMap.variance_eq_norm_sq_sub_expectedValue_sq: for a unit vector and symmetric T, the variance is ‖Tψ‖ ^ 2 - ⟨T⟩_ψ ^ 2.
• LinearPMap.variance_eq_re_inner_sub_expectedValue_sq: the second-order formula when Tψ ∈ T.domain.
• LinearPMap.variance_eq_zero_iff_isEigenvector and LinearPMap.standardDeviation_eq_zero_iff_isEigenvector: for a unit vector, zero variance or standard deviation is equivalent to the eigenvector condition.

References

• B. C. Hall, Quantum Theory for Mathematicians, Chapter 12.

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

Variance ‖Tψ - ⟨T⟩_ψ ψ‖ ^ 2; only ψ ∈ T.domain is required.

Equations

• T.variance ψ = ‖T.centered ψ‖ ^ 2

theorem LinearPMap.variance_eq_centered_norm_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (ψ : ↥T.domain) : T.variance ψ = ‖T.centered ψ‖ ^ 2

The variance is the squared norm of the centered vector.

theorem LinearPMap.variance_eq_norm_sub_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (ψ : ↥T.domain) : T.variance ψ = ‖↑T ψ - ↑(T.expectedValue ψ) • ↑ψ‖ ^ 2

variance with centered unfolded to Tψ - ⟨T⟩_ψ • ψ.

theorem LinearPMap.variance_eq_norm_sq_sub_expectedValue_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (hT : T.IsSymmetric) (ψ : ↥T.domain) (hψ_norm : ‖↑ψ‖ = 1) : T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2

For symmetric T and ‖ψ‖ = 1, variance equals ‖Tψ‖ ^ 2 - ⟨T⟩_ψ ^ 2.

theorem LinearPMap.variance_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (ψ : ↥T.domain) : 0 ≤ T.variance ψ

Variance is nonnegative.

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

Zero variance is the same as a zero centered vector.

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

Zero variance is the same as Tψ = ⟨T⟩_ψ ψ.

theorem LinearPMap.variance_eq_zero_iff_isEigenvector {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (ψ : ↥T.domain) (hψ_norm : ‖↑ψ‖ = 1) : T.variance ψ = 0 ↔ T.IsEigenvector ψ ↑(T.expectedValue ψ)

For ‖ψ‖ = 1, zero variance iff ψ is an eigenvector with eigenvalue ⟨T⟩_ψ.

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

Standard deviation √(variance) for ψ ∈ T.domain.

Equations

• T.standardDeviation ψ = √(T.variance ψ)

theorem LinearPMap.standardDeviation_eq_sqrt_variance {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (ψ : ↥T.domain) : T.standardDeviation ψ = √(T.variance ψ)

The standard deviation, unfolded to the square root of the variance.

theorem LinearPMap.standardDeviation_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (ψ : ↥T.domain) : 0 ≤ T.standardDeviation ψ

Standard deviation is nonnegative.

@[simp]

theorem LinearPMap.standardDeviation_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (ψ : ↥T.domain) : T.standardDeviation ψ ^ 2 = T.variance ψ

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

Zero standard deviation is the same as a zero centered vector.

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

Zero standard deviation is the same as Tψ = ⟨T⟩_ψ ψ.

theorem LinearPMap.standardDeviation_eq_zero_iff_isEigenvector {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (ψ : ↥T.domain) (hψ_norm : ‖↑ψ‖ = 1) : T.standardDeviation ψ = 0 ↔ T.IsEigenvector ψ ↑(T.expectedValue ψ)

For ‖ψ‖ = 1, zero standard deviation iff the eigenvector condition holds.

theorem LinearPMap.re_inner_apply_sq_eq_norm_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (hT : T.IsSymmetric) (ψ : ↥T.domain) (hTψ : ↑T ψ ∈ T.domain) : (inner ℂ (↑ψ) (↑T ⟨↑T ψ, hTψ⟩)).re = ‖↑T ψ‖ ^ 2

For symmetric T, re ⟪ψ, T(Tψ)⟫ is ‖Tψ‖ ^ 2.

theorem LinearPMap.variance_eq_re_inner_sub_expectedValue_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (hT : T.IsSymmetric) (ψ : ↥T.domain) (hTψ : ↑T ψ ∈ T.domain) (hψ_norm : ‖↑ψ‖ = 1) : T.variance ψ = (inner ℂ (↑ψ) (↑T ⟨↑T ψ, hTψ⟩)).re - T.expectedValue ψ ^ 2

When Tψ ∈ T.domain, variance equals ⟨T^2⟩_ψ - ⟨T⟩_ψ ^ 2.