OAI/Analysis/WeakInfiniteness/SeparationFourColumns.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.map_positive_sqrt line 32
2. lemma OAI.WeakPureInfiniteness.norm_column_le_sqrt_sum line 39
3. lemma OAI.WeakPureInfiniteness.norm_other_column_le_sqrt_sum line 48
4. def OAI.WeakPureInfiniteness.twoEntryRow line 54
5. lemma OAI.WeakPureInfiniteness.twoEntryRow_range line 57
6. lemma OAI.WeakPureInfiniteness.norm_two_sqrt_sums_le line 62
7. lemma OAI.WeakPureInfiniteness.inr_snd_inr_mul line 89
8. lemma OAI.WeakPureInfiniteness.unitizedRight_mem_principal line 94
9. lemma OAI.WeakPureInfiniteness.norm_sqrt_sum_representation line 103