OAI/Analysis/WeakInfiniteness/FiniteReducingModelsExtension.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WeakPureInfiniteness.UniformCStarProduct line 51
2. instance OAI.WeakPureInfiniteness.(instance at line 53) line 53
3. instance OAI.WeakPureInfiniteness.(instance at line 57) line 57
4. def OAI.WeakPureInfiniteness.uniformProductHom line 61
5. lemma OAI.WeakPureInfiniteness.uniformProductHom_injective line 72
6. lemma OAI.WeakPureInfiniteness.norm_le_iff_representations line 80
7. lemma OAI.WeakPureInfiniteness.norm_matrix_le_iff_representations line 91
8. instance OAI.WeakPureInfiniteness.(instance at line 109) line 109
9. instance OAI.WeakPureInfiniteness.(instance at line 112) line 112
10. instance OAI.WeakPureInfiniteness.(instance at line 114) line 114
11. instance OAI.WeakPureInfiniteness.(instance at line 116) line 116
12. def OAI.WeakPureInfiniteness.universalMatrixPolynomial line 121
13. def OAI.WeakPureInfiniteness.matrixPolynomialOperator line 125
14. lemma OAI.WeakPureInfiniteness.matrixPolynomialOperator_apply line 132
15. lemma OAI.WeakPureInfiniteness.norm_universalMatrixPolynomial_le_iff line 139
16. def OAI.WeakPureInfiniteness.piLpSubmoduleInclusion line 170
17. lemma OAI.WeakPureInfiniteness.piLpSubmoduleInclusion_apply line 180
18. lemma OAI.WeakPureInfiniteness.polynomialOperator_family_compression_exact line 184
19. lemma OAI.WeakPureInfiniteness.matrixPolynomialOperator_compression_exact line 207
20. lemma OAI.WeakPureInfiniteness.norm_universalMatrixPolynomial_le_of_finite_tests line 226