OAI/Analysis/WeakInfiniteness/UniformGap.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.tensorCut_wordTensor line 34
2. lemma OAI.WeakPureInfiniteness.wordTensorCost_cut_le line 43
3. lemma OAI.WeakPureInfiniteness.norm_tensorCut_wordTensor_le_of_models line 52
4. structure OAI.WeakPureInfiniteness.ExactModelData line 65
5. lemma OAI.WeakPureInfiniteness.exact_universal_of_arbitrarily_good_models line 75
6. theorem OAI.WeakPureInfiniteness.exists_uniform_gap_one line 146