OAI/Analysis/WeakInfiniteness/FixedRows.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.exists_fixed_comparison_row line 31
2. lemma OAI.WeakPureInfiniteness.spectralRamp_mul_ramp line 45
3. lemma OAI.WeakPureInfiniteness.fixed_row_shallow_support line 60
4. lemma OAI.WeakPureInfiniteness.fixed_row_partial_isometry line 70