OAI/Combinatorics/Progressions/Linear/AllocatedExternalCandidateCommonKeepPositiveKernelPreparation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrecenterKernelSelection line 41
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_precenterKernelSelection line 66
3. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrecenterKernelSelection.problem line 111
4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrecenterKernelSelection.positive_mass line 120
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrecenterKernelSelection.problem_productive line 123
6. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelPreparationExponent line 166
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelPreparationExponent_ge_two line 169
8. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelPreparationParameter line 173
9. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelPreparationBinLog line 176
10. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PositiveKernelPreparation line 179
11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_positiveKernelPreparation line 197
12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelPreparationParameter_ge_input line 288
13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelPreparationParameter_nonneg line 298
14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelPreparationBinLog_nonneg line 303
15. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelResidualPrecisionParameter line 309
16. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelMarkovPrecisionParameter line 313
17. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_positiveKernelPreparationParameters_bound line 318
18. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelPreparationBudgetExponent line 355
19. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelPreparationBudgetExponent_ge_two line 358
20. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelPreparationBudget_bounds line 362
21. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PositiveKernelPreparation.conclusion_of_selected line 417
22. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CommonKeepPositiveKernelPreparation line 502
23. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_commonKeepPositiveKernelPreparation line 508
24. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CommonKeepPositiveKernelPreparation.problem line 558
25. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CommonKeepPositiveKernelPreparation.problem_keep line 560
26. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CommonKeepPositiveKernelPreparation.conclusion_of_selected line 563