OAI/Analysis/KadisonKastler/CommonSpectralMeasurable.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Borel representations in the common spectral model

The common spectral construction gives representations and their L² action. A common-conull modification supplies Borel vector evaluations for every source element while retaining that action.

  1. theorem OAI.KadisonKastler.exists_measurable_common_representations line 35