OAI/Analysis/KadisonKastler/HilbertSumFieldReconstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous bounded-field reconstruction on the rank strata

The commutant test works directly on the Hilbert sum. In particular it does not assume, in advance, that the coordinate projections belong to the algebra.

  1. theorem OAI.KadisonKastler.l2LinearFieldMap_norm_le line 23
  2. theorem OAI.KadisonKastler.reconstruct_hilbertSum_field_of_commutant_fields line 43