OAI/Analysis/WeakInfiniteness/PolarCFC.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.initial_mul_cfc line 31
2. lemma OAI.WeakPureInfiniteness.norm_mul_cfc_initial_le line 46
3. lemma OAI.WeakPureInfiniteness.sandwich_cfc_initial line 60
4. lemma OAI.WeakPureInfiniteness.cfc_real_mul_three line 69
5. lemma OAI.WeakPureInfiniteness.norm_separationR line 76
6. lemma OAI.WeakPureInfiniteness.norm_separation_polar line 83
7. lemma OAI.WeakPureInfiniteness.norm_separation_low line 90
8. lemma OAI.WeakPureInfiniteness.norm_separation_mixedR line 100
9. lemma OAI.WeakPureInfiniteness.norm_separation_mixedV line 110