OAI/Analysis/Pureness/Completion/CompletedSourceLowerBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.positive_matrix_eq_zero_of_diagonal_sum_eq_zero line 10
2. theorem OAI.CuntzPureness.exists_completedSourceU_ne_zero line 27
3. theorem OAI.CuntzPureness.completedSourceU_uniform_lower_bound line 50