OAI/Combinatorics/Progressions/Nilpotent/UnconditionedScalarScaleNiltestBase.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.BooleanCubeKernel.exists_unconditioned_latePrime_niltest_base line 13
2. theorem OAI.Erdos3.BooleanCubeKernel.exists_unconditioned_chosenLatePrime_niltest_base line 129
3. def OAI.Erdos3.unconditionedScalarPrimeRatio line 233
4. theorem OAI.Erdos3.unconditionedScalarPrimeRatio_two_le line 236
5. theorem OAI.Erdos3.unconditionedScalarPrimeRatio_exp_bound line 241
6. theorem OAI.Erdos3.lateScalarScale_ge_input line 255
7. theorem OAI.Erdos3.BooleanCubeKernel.exists_unconditioned_scalarScale_niltest_base line 270