Physlib.QuantumMechanics.Operators.Covariance

Imports

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

public import Physlib.QuantumMechanics.Operators.StateObservables.Variance

Covariance

i. Overview

In this module we define the covariance of two partial linear maps A and B in a common state ψ as the real part of the inner product of their centered vectors.

ii. Key results

covariance : the real part of the centered inner product.

covariance_comm : covariance is symmetric in the two observables.

covariance_eq_re_symm_centered : covariance as the real part of the symmetrized centered inner product.

covariance_self_eq_variance : the covariance of an observable with itself is its variance.

iii. Table of contents

A. Covariance

iv. References

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

@[expose] public section

A. Covariance

Covariance, defined as the real part of the centered inner product.

def covariance : ℝ :=
  (⟪centered A ψ, centered B ⟨ψ, hψB⟩⟫_ℂ).re

Covariance, unfolded to the real part of the centered inner product.

lemma covariance_eq_re_inner_centered :
    covariance A B ψ hψB =
      (⟪centered A ψ, centered B ⟨ψ, hψB⟩⟫_ℂ).re :=
  rfl

Swapping the two observables does not change the covariance.


lemma covariance_comm :
    covariance A B ψ hψB = covariance B A ⟨ψ, hψB⟩ ψ.2 := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domain⊢ A.covariance B ψ hψB = B.covariance A ⟨↑ψ, hψB⟩ ⋯
  rw [covariance_eq_re_inner_centered,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domain⊢ (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ).re = B.covariance A ⟨↑ψ, hψB⟩ ⋯H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domain⊢ (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ).re = (⟪B.centered ⟨↑ψ, hψB⟩, A.centered ⟨↑⟨↑ψ, hψB⟩, ⋯⟩⟫_ℂ).re covariance_eq_re_inner_centeredH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domain⊢ (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ).re = (⟪B.centered ⟨↑ψ, hψB⟩, A.centered ⟨↑⟨↑ψ, hψB⟩, ⋯⟩⟫_ℂ).reH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domain⊢ (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ).re = (⟪B.centered ⟨↑ψ, hψB⟩, A.centered ⟨↑⟨↑ψ, hψB⟩, ⋯⟩⟫_ℂ).re]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domain⊢ (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ).re = (⟪B.centered ⟨↑ψ, hψB⟩, A.centered ⟨↑⟨↑ψ, hψB⟩, ⋯⟩⟫_ℂ).re
  calc
    (⟪centered A ψ, centered B ⟨ψ, hψB⟩⟫_ℂ).re =
        (((starRingEnd ℂ) ⟪centered B ⟨ψ, hψB⟩, centered A ψ⟫_ℂ)).re := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domain⊢ (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ).re = ((starRingEnd ℂ) ⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ).re
      rw [inner_conj_symmH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domain⊢ (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ).re = (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ).reAll goals completed! 🐙]All goals completed! 🐙
    _ = (⟪centered B ⟨ψ, hψB⟩, centered A ψ⟫_ℂ).re := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domain⊢ ((starRingEnd ℂ) ⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ).re = (⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ).re
      change (star ⟪centered B ⟨ψ, hψB⟩, centered A ψ⟫_ℂ).re =
        (⟪centered B ⟨ψ, hψB⟩, centered A ψ⟫_ℂ).reH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domain⊢ (star ⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ).re = (⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ).re
      rw [Complex.star_def,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domain⊢ ((starRingEnd ℂ) ⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ).re = (⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ).reAll goals completed! 🐙 Complex.conj_reH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domain⊢ (⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ).re = (⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ).reAll goals completed! 🐙]All goals completed! 🐙

Covariance as the real part of the symmetrized centered inner product.


lemma covariance_eq_re_symm_centered :
    covariance A B ψ hψB =
      ((⟪centered A ψ, centered B ⟨ψ, hψB⟩⟫_ℂ +
        ⟪centered B ⟨ψ, hψB⟩, centered A ψ⟫_ℂ).re) / 2 := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domain⊢ A.covariance B ψ hψB = (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ + ⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ).re / 2
  let z : ℂ := ⟪centered A ψ, centered B ⟨ψ, hψB⟩⟫_ℂH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainz:ℂ := ⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ⊢ A.covariance B ψ hψB = (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ + ⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ).re / 2
  have hz : ⟪centered B ⟨ψ, hψB⟩, centered A ψ⟫_ℂ = star z := by
    simp [z, inner_conj_symm]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainz:ℂ := ⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂhz:⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ = star z⊢ A.covariance B ψ hψB = (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ + ⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ).re / 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainz:ℂ := ⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂhz:⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ = star z⊢ A.covariance B ψ hψB = (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ + ⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ).re / 2
  rw [covariance_eq_re_inner_centered,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainz:ℂ := ⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂhz:⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ = star z⊢ (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ).re =
  (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ + ⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ).re / 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainz:ℂ := ⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂhz:⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ = star z⊢ (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ).re = (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ + star z).re / 2 hzH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainz:ℂ := ⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂhz:⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ = star z⊢ (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ).re = (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ + star z).re / 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainz:ℂ := ⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂhz:⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ = star z⊢ (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ).re = (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ + star z).re / 2]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainz:ℂ := ⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂhz:⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ = star z⊢ (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ).re = (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ + star z).re / 2
  change z.re = ((z + star z).re) / 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainz:ℂ := ⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂhz:⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ = star z⊢ z.re = (z + star z).re / 2
  simp only [Complex.add_re, Complex.star_def, Complex.conj_re, add_self_div_two]All goals completed! 🐙



@[simp]
lemma covariance_self_eq_variance (A : H →ₗ.[ℂ] H) (ψ : A.domain) :
    covariance A A ψ (byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA✝:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ✝:↥A✝.domainhψB:↑ψ✝ ∈ B.domainA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ ↑ψ ∈ A.domain exact ψ.2All goals completed! 🐙) = variance A ψ := byH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ A.covariance A ψ ⋯ = A.variance ψ
  rw [covariance_eq_re_inner_centered,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ (⟪A.centered ψ, A.centered ⟨↑ψ, ⋯⟩⟫_ℂ).re = A.variance ψH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ (↑‖A.centered ψ‖ ^ 2).re = ‖A.centered ψ‖ ^ 2 variance_eq_centered_norm_sq,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ (⟪A.centered ψ, A.centered ⟨↑ψ, ⋯⟩⟫_ℂ).re = ‖A.centered ψ‖ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ (↑‖A.centered ψ‖ ^ 2).re = ‖A.centered ψ‖ ^ 2 inner_self_eq_norm_sq_to_KH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ (↑‖A.centered ψ‖ ^ 2).re = ‖A.centered ψ‖ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ (↑‖A.centered ψ‖ ^ 2).re = ‖A.centered ψ‖ ^ 2]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ (↑‖A.centered ψ‖ ^ 2).re = ‖A.centered ψ‖ ^ 2
  rw [sq,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ (↑‖A.centered ψ‖ * ↑‖A.centered ψ‖).re = ‖A.centered ψ‖ ^ 2H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ (↑‖A.centered ψ‖).re * (↑‖A.centered ψ‖).re - (↑‖A.centered ψ‖).im * (↑‖A.centered ψ‖).im =
  ‖A.centered ψ‖ * ‖A.centered ψ‖ sq,H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ (↑‖A.centered ψ‖ * ↑‖A.centered ψ‖).re = ‖A.centered ψ‖ * ‖A.centered ψ‖H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ (↑‖A.centered ψ‖).re * (↑‖A.centered ψ‖).re - (↑‖A.centered ψ‖).im * (↑‖A.centered ψ‖).im =
  ‖A.centered ψ‖ * ‖A.centered ψ‖ Complex.mul_reH:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ (↑‖A.centered ψ‖).re * (↑‖A.centered ψ‖).re - (↑‖A.centered ψ‖).im * (↑‖A.centered ψ‖).im =
  ‖A.centered ψ‖ * ‖A.centered ψ‖H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ (↑‖A.centered ψ‖).re * (↑‖A.centered ψ‖).re - (↑‖A.centered ψ‖).im * (↑‖A.centered ψ‖).im =
  ‖A.centered ψ‖ * ‖A.centered ψ‖]H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] Hψ:↥A.domain⊢ (↑‖A.centered ψ‖).re * (↑‖A.centered ψ‖).re - (↑‖A.centered ψ‖).im * (↑‖A.centered ψ‖).im =
  ‖A.centered ψ‖ * ‖A.centered ψ‖
  simp [Complex.ofReal_re, Complex.ofReal_im]All goals completed! 🐙