OAI/Analysis/WeakInfiniteness/NormKernelWitness.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.functional_norm_le_image line 20
2. lemma OAI.WeakPureInfiniteness.freeDiagonalFunctional_large_elementary_kernel line 34
3. lemma OAI.WeakPureInfiniteness.freeDiagonalFunctional_witness_gap line 39
4. lemma OAI.WeakPureInfiniteness.freeDiagonalFunctional_kernel_of_exact line 45
5. lemma OAI.WeakPureInfiniteness.freeDiagonalFunctional_bound_of_kernel line 53
6. theorem OAI.WeakPureInfiniteness.fullFreeTwo_not_exact line 61