OAI/Analysis/KadisonKastler/FieldReconstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Reconstructing bounded fields from the commutant

A measurable bounded field in the fiber algebra defines an operator on L². Actual fields for the commutant show that this operator belongs to the original von Neumann algebra, by the bicommutant theorem.

  1. theorem OAI.KadisonKastler.reconstruct_field_of_commutant_fields line 24
  2. theorem OAI.KadisonKastler.operatorFieldDecomposition_of_commutant_fields line 49