Null sets of a projection-valued measure

A projection-valued measure P has a diagonal scalar measure P.diag ξ for each vector ξ. The filter P.ae records sets that are conull for every diagonal measure. A measurable set is null for this filter precisely when its spectral projection vanishes.

The null measurable sets are closed under taking measurable subsets and countable unions. This is the shared almost-everywhere interface needed for the bounded Borel spectral integral.

Provenance

The finite diagonal scalar measures and projection identities are from the maintained AIQ-Kitware DKPS formalization (Kitware, Inc.; Apache-2.0): https://github.com/AIQ-Kitware/aiq-dkps-formalization (ForTauCeti/Analysis/InnerProductSpace/ProjValMeasure/Basic.lean). The filter packages those existing results with Mathlib's native almost-everywhere API.

noncomputable def TauCeti.ProjValMeasure.ae {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) : Filter X

The filter of sets conull for every diagonal measure of the PVM.

theorem TauCeti.ProjValMeasure.eventually_ae_iff {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (R : X → Prop) : (∀ᶠ (x : X) in P.ae, R x) ↔ ∀ (ξ : H), ∀ᵐ (x : X) ∂P.diag ξ, R x

PVM-almost-everywhere predicates hold for every diagonal scalar measure.

theorem TauCeti.ProjValMeasure.ae_diag_le_ae {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (ξ : H) : MeasureTheory.ae (P.diag ξ) ≤ P.ae

The almost-everywhere filter of each diagonal measure lies below the PVM filter.

theorem TauCeti.ProjValMeasure.ae_diag_of_ae {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (ξ : H) {R : X → Prop} (hR : ∀ᶠ (x : X) in P.ae, R x) : ∀ᵐ (x : X) ∂P.diag ξ, R x

A PVM-almost-everywhere statement holds for an individual diagonal measure.

@[simp]

theorem TauCeti.ProjValMeasure.mem_ae_iff {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (s : Set X) : s ∈ P.ae ↔ ∀ (ξ : H), (P.diag ξ) sᶜ = 0

Membership in the PVM's almost-everywhere filter is simultaneous conullity for all its diagonal scalar measures.

theorem TauCeti.ProjValMeasure.compl_mem_ae_iff {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (s : Set X) : sᶜ ∈ P.ae ↔ ∀ (ξ : H), (P.diag ξ) s = 0

A set is null for the PVM iff each diagonal measure vanishes on it.

theorem TauCeti.ProjValMeasure.proj_eq_zero_iff_forall_diag_apply_eq_zero {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (s : Set X) (hs : MeasurableSet s) : P.proj s hs = 0 ↔ ∀ (ξ : H), (P.diag ξ) s = 0

A measurable spectral projection is zero exactly when every diagonal measure assigns its set zero mass.

theorem TauCeti.ProjValMeasure.proj_eq_zero_iff_compl_mem_ae {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) (s : Set X) (hs : MeasurableSet s) : P.proj s hs = 0 ↔ sᶜ ∈ P.ae

A measurable set is PVM-null iff its orthogonal projection vanishes.

theorem TauCeti.ProjValMeasure.proj_eq_zero_of_subset {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {s t : Set X} (hst : s ⊆ t) (hs : MeasurableSet s) (ht : MeasurableSet t) (h : P.proj t ht = 0) : P.proj s hs = 0

PVM-null measurable sets are downward closed.

theorem TauCeti.ProjValMeasure.proj_iUnion_eq_zero {X : Type u_1} {H : Type u_2} [MeasurableSpace X] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : ProjValMeasure X H) {ι : Type u_3} [Countable ι] (s : ι → Set X) (hs : ∀ (i : ι), MeasurableSet (s i)) (h : ∀ (i : ι), P.proj (s i) ⋯ = 0) : P.proj (⋃ (i : ι), s i) ⋯ = 0

PVM-null measurable sets are closed under countable unions.