Physlib.QuantumMechanics.Operators.StateObservables.Variance

Imports

/-
Copyright (c) 2026 Axiomatic-AI. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Matteo Cipollina, Krystian Nowakowski
-/
module

public import Physlib.QuantumMechanics.Operators.StateObservables.ExpectedValue
public import Physlib.QuantumMechanics.Operators.StateObservables.IsEigenvector
public import Mathlib.Analysis.SpecialFunctions.Sqrt

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][hall2013quantum].

@[expose] public section

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

def variance (T : H →ₗ.[ℂ] H) (ψ : T.domain) : ℝ :=
  ‖centered T ψ‖ ^ 2

The variance is the squared norm of the centered vector.

lemma variance_eq_centered_norm_sq (T : H →ₗ.[ℂ] H) (ψ : T.domain) :
    variance T ψ = ‖centered T ψ‖ ^ 2 :=
  rfl

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

lemma variance_eq_norm_sub_sq (T : H →ₗ.[ℂ] H) (ψ : T.domain) :
    variance T ψ =
      ‖T ψ - (expectedValue T ψ : ℂ) • (ψ : H)‖ ^ 2 :=
  rfl

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


lemma variance_eq_norm_sq_sub_expectedValue_sq (T : H →ₗ.[ℂ] H)
    (hT : T.IsSymmetric) (ψ : T.domain) (hψ_norm : ‖(ψ : H)‖ = 1) :
    variance T ψ = ‖T ψ‖ ^ 2 - expectedValue T ψ ^ 2 := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2
  let μ := expectedValue T ψH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψ⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2
  let a : H := T ψH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψ⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2
  have hμ_right : ⟪(ψ : H), a⟫_ℂ = (μ : ℂ) := by
    simpa [a, μ] using expectedValue_eq_inner T hT ψH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μ⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μ⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2
  have hμ_left : ⟪a, (ψ : H)⟫_ℂ = (μ : ℂ) := by
    simpa [inner_conj_symm] using congrArg star hμ_rightH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μ⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μ⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2
  have h_re_inner_centered : (⟪a, (μ : ℂ) • (ψ : H)⟫_ℂ).re = μ ^ 2 := by
    rw [inner_smul_right,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μ⊢ (↑μ * ⟪a, ↑ψ⟫_ℂ).re = μ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μ⊢ (↑μ * ↑μ).re = μ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2 hμ_leftH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μ⊢ (↑μ * ↑μ).re = μ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μ⊢ (↑μ * ↑μ).re = μ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μ⊢ (↑μ * ↑μ).re = μ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2
    simp [μ]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μ⊢ T.expectedValue ψ * T.expectedValue ψ = T.expectedValue ψ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2
    ringH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2
  have h_norm_centered_smul : ‖(μ : ℂ) • (ψ : H)‖ ^ 2 = μ ^ 2 := by
    rw [norm_smul,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2⊢ (‖↑μ‖ * ‖↑ψ‖) ^ 2 = μ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2⊢ (‖↑μ‖ * 1) ^ 2 = μ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2 hψ_normH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2⊢ (‖↑μ‖ * 1) ^ 2 = μ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2⊢ (‖↑μ‖ * 1) ^ 2 = μ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2⊢ (‖↑μ‖ * 1) ^ 2 = μ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2
    simp [μ]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2
  have h_norm_sub_sq :
      ‖a - (μ : ℂ) • (ψ : H)‖ ^ 2 =
        ‖a‖ ^ 2 - 2 * (⟪a, (μ : ℂ) • (ψ : H)⟫_ℂ).re + ‖(μ : ℂ) • (ψ : H)‖ ^ 2 := by
    simpa using (norm_sub_sq (𝕜 := ℂ) a ((μ : ℂ) • (ψ : H)))H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2h_norm_sub_sq:‖a - ↑μ • ↑ψ‖ ^ 2 = ‖a‖ ^ 2 - 2 * (⟪a, ↑μ • ↑ψ⟫_ℂ).re + ‖↑μ • ↑ψ‖ ^ 2⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2h_norm_sub_sq:‖a - ↑μ • ↑ψ‖ ^ 2 = ‖a‖ ^ 2 - 2 * (⟪a, ↑μ • ↑ψ⟫_ℂ).re + ‖↑μ • ↑ψ‖ ^ 2⊢ T.variance ψ = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2
  rw [variance_eq_norm_sub_sq,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2h_norm_sub_sq:‖a - ↑μ • ↑ψ‖ ^ 2 = ‖a‖ ^ 2 - 2 * (⟪a, ↑μ • ↑ψ⟫_ℂ).re + ‖↑μ • ↑ψ‖ ^ 2⊢ ‖↑T ψ - ↑(T.expectedValue ψ) • ↑ψ‖ ^ 2 = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2h_norm_sub_sq:‖a - ↑μ • ↑ψ‖ ^ 2 = ‖a‖ ^ 2 - 2 * (⟪a, ↑μ • ↑ψ⟫_ℂ).re + ‖↑μ • ↑ψ‖ ^ 2⊢ ‖a‖ ^ 2 - 2 * μ ^ 2 + μ ^ 2 = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2 h_norm_sub_sq,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2h_norm_sub_sq:‖a - ↑μ • ↑ψ‖ ^ 2 = ‖a‖ ^ 2 - 2 * (⟪a, ↑μ • ↑ψ⟫_ℂ).re + ‖↑μ • ↑ψ‖ ^ 2⊢ ‖a‖ ^ 2 - 2 * (⟪a, ↑μ • ↑ψ⟫_ℂ).re + ‖↑μ • ↑ψ‖ ^ 2 = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2h_norm_sub_sq:‖a - ↑μ • ↑ψ‖ ^ 2 = ‖a‖ ^ 2 - 2 * (⟪a, ↑μ • ↑ψ⟫_ℂ).re + ‖↑μ • ↑ψ‖ ^ 2⊢ ‖a‖ ^ 2 - 2 * μ ^ 2 + μ ^ 2 = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2 h_re_inner_centered,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2h_norm_sub_sq:‖a - ↑μ • ↑ψ‖ ^ 2 = ‖a‖ ^ 2 - 2 * (⟪a, ↑μ • ↑ψ⟫_ℂ).re + ‖↑μ • ↑ψ‖ ^ 2⊢ ‖a‖ ^ 2 - 2 * μ ^ 2 + ‖↑μ • ↑ψ‖ ^ 2 = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2h_norm_sub_sq:‖a - ↑μ • ↑ψ‖ ^ 2 = ‖a‖ ^ 2 - 2 * (⟪a, ↑μ • ↑ψ⟫_ℂ).re + ‖↑μ • ↑ψ‖ ^ 2⊢ ‖a‖ ^ 2 - 2 * μ ^ 2 + μ ^ 2 = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2
    h_norm_centered_smulH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2h_norm_sub_sq:‖a - ↑μ • ↑ψ‖ ^ 2 = ‖a‖ ^ 2 - 2 * (⟪a, ↑μ • ↑ψ⟫_ℂ).re + ‖↑μ • ↑ψ‖ ^ 2⊢ ‖a‖ ^ 2 - 2 * μ ^ 2 + μ ^ 2 = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2h_norm_sub_sq:‖a - ↑μ • ↑ψ‖ ^ 2 = ‖a‖ ^ 2 - 2 * (⟪a, ↑μ • ↑ψ⟫_ℂ).re + ‖↑μ • ↑ψ‖ ^ 2⊢ ‖a‖ ^ 2 - 2 * μ ^ 2 + μ ^ 2 = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhψ_norm:‖↑ψ‖ = 1μ:ℝ := T.expectedValue ψa:H := ↑T ψhμ_right:⟪↑ψ, a⟫_ℂ = ↑μhμ_left:⟪a, ↑ψ⟫_ℂ = ↑μh_re_inner_centered:(⟪a, ↑μ • ↑ψ⟫_ℂ).re = μ ^ 2h_norm_centered_smul:‖↑μ • ↑ψ‖ ^ 2 = μ ^ 2h_norm_sub_sq:‖a - ↑μ • ↑ψ‖ ^ 2 = ‖a‖ ^ 2 - 2 * (⟪a, ↑μ • ↑ψ⟫_ℂ).re + ‖↑μ • ↑ψ‖ ^ 2⊢ ‖a‖ ^ 2 - 2 * μ ^ 2 + μ ^ 2 = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2
  ringAll goals completed! 🐙

Variance is nonnegative.


lemma variance_nonneg (T : H →ₗ.[ℂ] H) (ψ : T.domain) :
    0 ≤ variance T ψ := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ T.variance ψ
  rw [variance_eq_centered_norm_sqH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ ‖T.centered ψ‖ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ ‖T.centered ψ‖ ^ 2]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ ‖T.centered ψ‖ ^ 2
  exact sq_nonneg _All goals completed! 🐙

Zero variance is the same as a zero centered vector.


lemma variance_eq_zero_iff_centered_eq_zero (T : H →ₗ.[ℂ] H) (ψ : T.domain) :
    variance T ψ = 0 ↔ centered T ψ = 0 := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ T.variance ψ = 0 ↔ T.centered ψ = 0
  rw [variance_eq_centered_norm_sqH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ ‖T.centered ψ‖ ^ 2 = 0 ↔ T.centered ψ = 0H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ ‖T.centered ψ‖ ^ 2 = 0 ↔ T.centered ψ = 0]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ ‖T.centered ψ‖ ^ 2 = 0 ↔ T.centered ψ = 0
  exact sq_eq_zero_iff.trans norm_eq_zeroAll goals completed! 🐙

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


lemma variance_eq_zero_iff (T : H →ₗ.[ℂ] H) (ψ : T.domain) :
    variance T ψ = 0 ↔ T ψ = (expectedValue T ψ : ℂ) • (ψ : H) := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ T.variance ψ = 0 ↔ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ
  rw [variance_eq_zero_iff_centered_eq_zero,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ T.centered ψ = 0 ↔ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψAll goals completed! 🐙 centered_eq_zero_iffH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ ↔ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψAll goals completed! 🐙]All goals completed! 🐙

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


lemma variance_eq_zero_iff_isEigenvector (T : H →ₗ.[ℂ] H)
    (ψ : T.domain) (hψ_norm : ‖(ψ : H)‖ = 1) :
    variance T ψ = 0 ↔
      T.IsEigenvector ψ (expectedValue T ψ : ℂ) := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ T.variance ψ = 0 ↔ T.IsEigenvector ψ ↑(T.expectedValue ψ)
  rw [variance_eq_zero_iffH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ ↔ T.IsEigenvector ψ ↑(T.expectedValue ψ)H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ ↔ T.IsEigenvector ψ ↑(T.expectedValue ψ)]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ ↔ T.IsEigenvector ψ ↑(T.expectedValue ψ)
  constructormpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ → T.IsEigenvector ψ ↑(T.expectedValue ψ)mprH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ T.IsEigenvector ψ ↑(T.expectedValue ψ) → ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ
  ·mpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ → T.IsEigenvector ψ ↑(T.expectedValue ψ) intro h_centeredmpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψ⊢ T.IsEigenvector ψ ↑(T.expectedValue ψ)
    refine ⟨h_centered, ?_⟩mpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψ⊢ ↑ψ ≠ 0
    intro h_zerompH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0⊢ False
    have h_zero' : (ψ : H) = 0 := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ T.variance ψ = 0 ↔ T.IsEigenvector ψ ↑(T.expectedValue ψ)mpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0h_zero':↑ψ = 0⊢ False simpa using h_zerompH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0h_zero':↑ψ = 0⊢ FalsempH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0h_zero':↑ψ = 0⊢ False
    have h_norm_zero : ‖(ψ : H)‖ = 0 := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ T.variance ψ = 0 ↔ T.IsEigenvector ψ ↑(T.expectedValue ψ)mpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0h_zero':↑ψ = 0h_norm_zero:‖↑ψ‖ = 0⊢ False simp [h_zero']mpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0h_zero':↑ψ = 0h_norm_zero:‖↑ψ‖ = 0⊢ FalsempH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0h_zero':↑ψ = 0h_norm_zero:‖↑ψ‖ = 0⊢ False
    have : (0 : ℝ) = 1 := h_norm_zero.symm.trans hψ_normmpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0h_zero':↑ψ = 0h_norm_zero:‖↑ψ‖ = 0this:0 = 1⊢ False
    norm_num at thisAll goals completed! 🐙
  ·mprH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ T.IsEigenvector ψ ↑(T.expectedValue ψ) → ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ intro h_eigenmprH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_eigen:T.IsEigenvector ψ ↑(T.expectedValue ψ)⊢ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ
    exact h_eigen.1All goals completed! 🐙

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

def standardDeviation (T : H →ₗ.[ℂ] H) (ψ : T.domain) : ℝ :=
  Real.sqrt (variance T ψ)

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

lemma standardDeviation_eq_sqrt_variance (T : H →ₗ.[ℂ] H) (ψ : T.domain) :
    standardDeviation T ψ = Real.sqrt (variance T ψ) :=
  rfl

Standard deviation is nonnegative.


lemma standardDeviation_nonneg (T : H →ₗ.[ℂ] H) (ψ : T.domain) :
    0 ≤ standardDeviation T ψ := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ T.standardDeviation ψ
  rw [standardDeviation_eq_sqrt_varianceH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ √(T.variance ψ)H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ √(T.variance ψ)]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ √(T.variance ψ)
  exact Real.sqrt_nonneg _All goals completed! 🐙



@[simp]
lemma standardDeviation_sq (T : H →ₗ.[ℂ] H) (ψ : T.domain) :
    standardDeviation T ψ ^ 2 = variance T ψ := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ T.standardDeviation ψ ^ 2 = T.variance ψ
  rw [standardDeviation_eq_sqrt_variance,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ √(T.variance ψ) ^ 2 = T.variance ψH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ T.variance ψ Real.sq_sqrtH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ T.variance ψ = T.variance ψH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ T.variance ψH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ T.variance ψ]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ T.variance ψ
  exact variance_nonneg T ψAll goals completed! 🐙

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


lemma standardDeviation_eq_zero_iff_centered_eq_zero (T : H →ₗ.[ℂ] H)
    (ψ : T.domain) :
    standardDeviation T ψ = 0 ↔ centered T ψ = 0 := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ T.standardDeviation ψ = 0 ↔ T.centered ψ = 0
  rw [standardDeviation_eq_sqrt_variance,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ √(T.variance ψ) = 0 ↔ T.centered ψ = 0H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ T.variance ψ = 0 ↔ T.centered ψ = 0H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ T.variance ψ Real.sqrt_eq_zeroH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ T.variance ψ = 0 ↔ T.centered ψ = 0H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ T.variance ψH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ T.variance ψ = 0 ↔ T.centered ψ = 0H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ T.variance ψ]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ T.variance ψ = 0 ↔ T.centered ψ = 0H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ T.variance ψ
  ·H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ T.variance ψ = 0 ↔ T.centered ψ = 0 exact variance_eq_zero_iff_centered_eq_zero T ψAll goals completed! 🐙
  ·H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ 0 ≤ T.variance ψ exact variance_nonneg T ψAll goals completed! 🐙

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


lemma standardDeviation_eq_zero_iff (T : H →ₗ.[ℂ] H) (ψ : T.domain) :
    standardDeviation T ψ = 0 ↔ T ψ = (expectedValue T ψ : ℂ) • (ψ : H) := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ T.standardDeviation ψ = 0 ↔ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ
  rw [standardDeviation_eq_zero_iff_centered_eq_zero,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ T.centered ψ = 0 ↔ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψAll goals completed! 🐙 centered_eq_zero_iffH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domain⊢ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ ↔ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψAll goals completed! 🐙]All goals completed! 🐙

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


lemma standardDeviation_eq_zero_iff_isEigenvector (T : H →ₗ.[ℂ] H)
    (ψ : T.domain) (hψ_norm : ‖(ψ : H)‖ = 1) :
    standardDeviation T ψ = 0 ↔
      T.IsEigenvector ψ (expectedValue T ψ : ℂ) := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ T.standardDeviation ψ = 0 ↔ T.IsEigenvector ψ ↑(T.expectedValue ψ)
  rw [standardDeviation_eq_zero_iffH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ ↔ T.IsEigenvector ψ ↑(T.expectedValue ψ)H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ ↔ T.IsEigenvector ψ ↑(T.expectedValue ψ)]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ ↔ T.IsEigenvector ψ ↑(T.expectedValue ψ)
  constructormpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ → T.IsEigenvector ψ ↑(T.expectedValue ψ)mprH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ T.IsEigenvector ψ ↑(T.expectedValue ψ) → ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ
  ·mpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ → T.IsEigenvector ψ ↑(T.expectedValue ψ) intro h_centeredmpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψ⊢ T.IsEigenvector ψ ↑(T.expectedValue ψ)
    refine ⟨h_centered, ?_⟩mpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψ⊢ ↑ψ ≠ 0
    intro h_zerompH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0⊢ False
    have h_zero' : (ψ : H) = 0 := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ T.standardDeviation ψ = 0 ↔ T.IsEigenvector ψ ↑(T.expectedValue ψ)mpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0h_zero':↑ψ = 0⊢ False simpa using h_zerompH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0h_zero':↑ψ = 0⊢ FalsempH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0h_zero':↑ψ = 0⊢ False
    have h_norm_zero : ‖(ψ : H)‖ = 0 := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ T.standardDeviation ψ = 0 ↔ T.IsEigenvector ψ ↑(T.expectedValue ψ)mpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0h_zero':↑ψ = 0h_norm_zero:‖↑ψ‖ = 0⊢ False simp [h_zero']mpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0h_zero':↑ψ = 0h_norm_zero:‖↑ψ‖ = 0⊢ FalsempH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0h_zero':↑ψ = 0h_norm_zero:‖↑ψ‖ = 0⊢ False
    have : (0 : ℝ) = 1 := h_norm_zero.symm.trans hψ_normmpH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_centered:↑T ψ = ↑(T.expectedValue ψ) • ↑ψh_zero:↑ψ = 0h_zero':↑ψ = 0h_norm_zero:‖↑ψ‖ = 0this:0 = 1⊢ False
    norm_num at thisAll goals completed! 🐙
  ·mprH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1⊢ T.IsEigenvector ψ ↑(T.expectedValue ψ) → ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ intro h_eigenmprH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hψ:↥T.domainhψ_norm:‖↑ψ‖ = 1h_eigen:T.IsEigenvector ψ ↑(T.expectedValue ψ)⊢ ↑T ψ = ↑(T.expectedValue ψ) • ↑ψ
    exact h_eigen.1All goals completed! 🐙

include hT

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


lemma re_inner_apply_sq_eq_norm_sq :
    (⟪(ψ : H), T ⟨T ψ, hTψ⟩⟫_ℂ).re = ‖T ψ‖ ^ 2 := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domain⊢ (⟪↑ψ, ↑T ⟨↑T ψ, hTψ⟩⟫_ℂ).re = ‖↑T ψ‖ ^ 2
  rw [← hT ψ ⟨T ψ, hTψ⟩,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domain⊢ (⟪↑T ψ, ↑⟨↑T ψ, hTψ⟩⟫_ℂ).re = ‖↑T ψ‖ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domain⊢ (↑‖↑T ψ‖ ^ 2).re = ‖↑T ψ‖ ^ 2 inner_self_eq_norm_sq_to_KH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domain⊢ (↑‖↑T ψ‖ ^ 2).re = ‖↑T ψ‖ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domain⊢ (↑‖↑T ψ‖ ^ 2).re = ‖↑T ψ‖ ^ 2]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domain⊢ (↑‖↑T ψ‖ ^ 2).re = ‖↑T ψ‖ ^ 2
  rw [sq,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domain⊢ (↑‖↑T ψ‖ * ↑‖↑T ψ‖).re = ‖↑T ψ‖ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domain⊢ (↑‖↑T ψ‖).re * (↑‖↑T ψ‖).re - (↑‖↑T ψ‖).im * (↑‖↑T ψ‖).im = ‖↑T ψ‖ * ‖↑T ψ‖ sq,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domain⊢ (↑‖↑T ψ‖ * ↑‖↑T ψ‖).re = ‖↑T ψ‖ * ‖↑T ψ‖H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domain⊢ (↑‖↑T ψ‖).re * (↑‖↑T ψ‖).re - (↑‖↑T ψ‖).im * (↑‖↑T ψ‖).im = ‖↑T ψ‖ * ‖↑T ψ‖ Complex.mul_reH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domain⊢ (↑‖↑T ψ‖).re * (↑‖↑T ψ‖).re - (↑‖↑T ψ‖).im * (↑‖↑T ψ‖).im = ‖↑T ψ‖ * ‖↑T ψ‖H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domain⊢ (↑‖↑T ψ‖).re * (↑‖↑T ψ‖).re - (↑‖↑T ψ‖).im * (↑‖↑T ψ‖).im = ‖↑T ψ‖ * ‖↑T ψ‖]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domain⊢ (↑‖↑T ψ‖).re * (↑‖↑T ψ‖).re - (↑‖↑T ψ‖).im * (↑‖↑T ψ‖).im = ‖↑T ψ‖ * ‖↑T ψ‖
  simp [Complex.ofReal_re, Complex.ofReal_im]All goals completed! 🐙

include hψ_norm

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


lemma variance_eq_re_inner_sub_expectedValue_sq :
    variance T ψ =
      (⟪(ψ : H), T ⟨T ψ, hTψ⟩⟫_ℂ).re - expectedValue T ψ ^ 2 := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domainhψ_norm:‖↑ψ‖ = 1⊢ T.variance ψ = (⟪↑ψ, ↑T ⟨↑T ψ, hTψ⟩⟫_ℂ).re - T.expectedValue ψ ^ 2
  rw [variance_eq_norm_sq_sub_expectedValue_sq T hT ψ hψ_norm,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domainhψ_norm:‖↑ψ‖ = 1⊢ ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2 = (⟪↑ψ, ↑T ⟨↑T ψ, hTψ⟩⟫_ℂ).re - T.expectedValue ψ ^ 2All goals completed! 🐙
    re_inner_apply_sq_eq_norm_sq T hT ψ hTψH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricψ:↥T.domainhTψ:↑T ψ ∈ T.domainhψ_norm:‖↑ψ‖ = 1⊢ ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2 = ‖↑T ψ‖ ^ 2 - T.expectedValue ψ ^ 2All goals completed! 🐙]All goals completed! 🐙