OAI/Combinatorics/Progressions/Linear/GoodKernelJetBudget.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.goodScalarKernelTuple_index_le_expline 10 - theorem
OAI.Erdos3.goodScalarKernelTuple_period_powers_le_expline 22 - theorem
OAI.Erdos3.goodScalarKernelTuple_inverse_le_expline 35 - theorem
OAI.Erdos3.goodScalarKernelTuple_jet_budgetline 63