OAI/Analysis/FiniteFactor/CrossedProduct/ProjectionColumns.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceProjectionColumn line 12
2. def OAI.FiniteFactor.sourceComplementColumn line 16
3. def OAI.FiniteFactor.sourceProjectionLeftCoefficient line 20
4. def OAI.FiniteFactor.sourceProjectionRightCoefficient line 25
5. theorem OAI.FiniteFactor.fiberProjection_column_norm_le_one line 30
6. theorem OAI.FiniteFactor.sourceProjection_columns_norm line 38
7. theorem OAI.FiniteFactor.sourceProjectionLeftCoefficient_measurable line 45
8. theorem OAI.FiniteFactor.sourceProjectionRightCoefficient_measurable line 51