OAI/Analysis/WeakInfiniteness/NonunitalGram.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.finiteGram line 41
2. lemma OAI.WeakPureInfiniteness.finiteGram_apply line 45
3. lemma OAI.WeakPureInfiniteness.matrix_diagonal_mul_tendsto_nonunital line 48
4. lemma OAI.WeakPureInfiniteness.nonunital_positive_matrix_gram_approximation line 63