Projection-valued measures

This file defines real projection-valued measures through strong-operator countable additivity and proves monotonicity of their associated scalar quadratic forms.

structure PVM (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] : Type u_2

A projection-valued measure on ℝ, countably additive in the strong operator topology. Laws hold for measurable sets only.

• proj : Set ℝ → E →L[ℂ] E

  The orthogonal projection assigned to a measurable subset of the real line.

• isOrthogonalProjection (S : Set ℝ) : MeasurableSet S → IsSelfAdjoint (self.proj S) ∧ IsIdempotentElem (self.proj S)
• empty : self.proj ∅ = 0
• univ : self.proj Set.univ = 1
• inter (S T : Set ℝ) : MeasurableSet S → MeasurableSet T → self.proj (S ∩ T) = self.proj S * self.proj T
• countably_additive (S : ℕ → Set ℝ) : (∀ (i : ℕ), MeasurableSet (S i)) → Pairwise (Function.onFun Disjoint S) → ∀ (x : E), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (self.proj (S i)) x) Filter.atTop (nhds ((self.proj (⋃ (i : ℕ), S i)) x))

theorem PVM.monotone {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) {S T : Set ℝ} (hS : MeasurableSet S) (hT : MeasurableSet T) (h : S ⊆ T) (x : E) : (inner ℂ ((E_pvm.proj S) x) x).re ≤ (inner ℂ ((E_pvm.proj T) x) x).re

Inclusion of measurable sets makes the real scalar quadratic form of a PVM projection monotone.

theorem PVM.proj_union {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) {S T : Set ℝ} (hS : MeasurableSet S) (hT : MeasurableSet T) (hdisj : Disjoint S T) : E_pvm.proj (S ∪ T) = E_pvm.proj S + E_pvm.proj T

A PVM sends the union of two disjoint measurable sets to the sum of their projections.

theorem PVM.proj_biUnion_finset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {I : Type u_2} (E_pvm : PVM E) (s : Finset I) (A : I → Set ℝ) (hmeas : ∀ i ∈ s, MeasurableSet (A i)) (hpair : (↑s).PairwiseDisjoint A) : E_pvm.proj (⋃ i ∈ ↑s, A i) = ∑ i ∈ s, E_pvm.proj (A i)

A PVM sends a finite pairwise-disjoint union of measurable sets to the sum of their projections.