OAI/Analysis/WeakInfiniteness/HalfFlipGenerators.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.norm_starHom_cuntzWord_sub_le line 31
2. def OAI.WeakPureInfiniteness.cuntzPolynomialHomWeight line 68
3. lemma OAI.WeakPureInfiniteness.cuntzPolynomialHomWeight_nonneg line 71
4. lemma OAI.WeakPureInfiniteness.norm_starHom_cuntzPolynomial_sub_le line 76
5. def OAI.WeakPureInfiniteness.GeneratorHalfFlip line 99
6. lemma OAI.WeakPureInfiniteness.ApproximateHalfFlip.generatorTests line 109
7. lemma OAI.WeakPureInfiniteness.GeneratorHalfFlip.halfFlip line 118
8. def OAI.WeakPureInfiniteness.OInfinityGeneratorHalfFlip line 183
9. lemma OAI.WeakPureInfiniteness.oInfinity_halfFlip_iff_generatorHalfFlip line 185