OAI/Analysis/KadisonKastler/FixedProductFactor.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The fixed product makes a cyclically represented factor type III₁

The only product-construction input contains finite matrix moments and the two site eigenoperators. The centralizer and core criteria then establish type III₁.

  1. theorem OAI.KadisonKastler.product_matrix_entry_ne_zero line 23
  2. theorem OAI.KadisonKastler.TwoRatioProductModel.tensor_typeIII1 line 32