OAI/Analysis/IrrationalRotation/Spectral/ProductTracialSpectral.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.weightedOperator_tracialDeterminant_eq_vector line 14
2. theorem OAI.Invariant233.ProductModel.weightedOperator_tracialDeterminant_zero_of_cost_divergence line 20
3. theorem OAI.Invariant233.ProductModel.weightedOperator_tracialDeterminant_zero_of_block_bounds line 29
4. theorem OAI.Invariant233.ProductModel.weightedOperator_factorSpectrum_eq_singleton_zero line 42
5. theorem OAI.Invariant233.ProductModel.weightedOperator_isBrownMeasure_iff_vector line 60