OAI/Analysis/WeakInfiniteness/CompatibleInverse.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.exists_small_inverse line 28
2. lemma OAI.WeakPureInfiniteness.exists_factored_inverse line 49
3. lemma OAI.WeakPureInfiniteness.norm_one_add_le line 72
4. lemma OAI.WeakPureInfiniteness.norm_factored_perturbation_le line 75
5. lemma OAI.WeakPureInfiniteness.normalized_inverse_difference_bound line 84