OAI/Analysis/WeakInfiniteness/ScalarDiagonal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.diagonalCoefficient line 23
2. lemma OAI.WeakPureInfiniteness.finite_diagonal_polynomial line 27
3. lemma OAI.WeakPureInfiniteness.finite_diagonal_polynomial_bound line 37
4. lemma OAI.WeakPureInfiniteness.norm_free_diagonalCoefficient_le line 55
5. def OAI.WeakPureInfiniteness.freeDiagonalFunctional line 77
6. lemma OAI.WeakPureInfiniteness.freeDiagonalFunctional_polynomial line 81
7. lemma OAI.WeakPureInfiniteness.norm_freeDiagonalFunctional_le line 86
8. lemma OAI.WeakPureInfiniteness.freeDiagonalFunctional_group_tensors line 91