OAI/Analysis/WeakInfiniteness/IndividualInfiniteness.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.properlyInfinite_zero line 36
2. lemma OAI.WeakPureInfiniteness.weak_amplification_all line 43
3. lemma OAI.WeakPureInfiniteness.norm_sub_positiveCut_le line 53
4. lemma OAI.WeakPureInfiniteness.blockSum_diagonalCopies_one line 73
5. lemma OAI.WeakPureInfiniteness.properlyInfinite_of_cuts line 88
6. lemma OAI.WeakPureInfiniteness.exists_binary_splitting_over_norm_slice_one line 119
7. theorem OAI.WeakPureInfiniteness.exact_weaklyPurelyInfinite_individuallyProperlyInfinite_one line 144