OAI/Analysis/WeakInfiniteness/OrthogonalCores.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.exists_two_exact_core_columns line 36
2. lemma OAI.WeakPureInfiniteness.norm_spectralRamp_le_one line 61
3. lemma OAI.WeakPureInfiniteness.norm_spectralRamp_eq_one line 68
4. lemma OAI.WeakPureInfiniteness.exists_two_orthogonal_cores line 79