OAI/Combinatorics/Progressions/Linear/KernelCoefficientLogBudget.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.kernelJetInterpolationAllowance_le_exp line 9
  2. theorem OAI.Erdos3.kernelJetEntryAllowance_le_exp line 40
  3. theorem OAI.Erdos3.kernelJetMinorThreshold_inv_le_exp line 52
  4. theorem OAI.Erdos3.kernelJetInverseAllowance_le_exp line 65
  5. theorem OAI.Erdos3.goodKernel_common_period line 97
  6. theorem OAI.Erdos3.goodKernel_mapped_pivots line 122
  7. theorem OAI.Erdos3.scalarKernel_real_entry_bound line 190
  8. theorem OAI.Erdos3.scalarKernelFixed_operator_bounds line 201
  9. theorem OAI.Erdos3.goodKernel_fixed_pivots line 219
  10. theorem OAI.Erdos3.fixedKernel_mapped_control line 238
  11. def OAI.Erdos3.kernelPeriodCandidate line 300
  12. theorem OAI.Erdos3.kernelPeriodCandidate_pos line 303
  13. instance OAI.Erdos3.kernelPeriodCandidate_neZero line 307
  14. theorem OAI.Erdos3.kernelPeriodCandidate_le line 311
  15. theorem OAI.Erdos3.kernelPeriodCandidate_le_exp line 315
  16. theorem OAI.Erdos3.goodKernel_periodFamily line 323
  17. theorem OAI.Erdos3.goodKernel_periodFamily_uniform_rows line 359
  18. def OAI.Erdos3.goodKernelUniformCandidate line 386
  19. theorem OAI.Erdos3.goodKernelUniformCandidate_spec line 394
  20. theorem OAI.Erdos3.integerScalarLattice_le_of_nat_dvd line 422
  21. theorem OAI.Erdos3.kernelPeriodCandidate_cover line 430
  22. def OAI.Erdos3.kernelInverseLog line 452
  23. def OAI.Erdos3.kernelGeometryLog line 456
  24. theorem OAI.Erdos3.kernelGeometryLog_bounds line 459
  25. theorem OAI.Erdos3.nat_mul_kernelEntry_le_exp line 477
  26. theorem OAI.Erdos3.fixedKernel_geometry_le_exp line 485
  27. def OAI.Erdos3.kernelRowOutputLog line 515
  28. theorem OAI.Erdos3.kernelRowOutputLog_nonneg line 520
  29. theorem OAI.Erdos3.fixedKernel_output_le_exp line 528
  30. def OAI.Erdos3.kernelFamilyIndexLog line 591
  31. theorem OAI.Erdos3.kernelFamilyIndexLog_nonneg line 595
  32. theorem OAI.Erdos3.kernelFamilyIndexLog_row line 599
  33. def OAI.Erdos3.kernelCoefficientLog line 620
  34. theorem OAI.Erdos3.kernelCoefficientLog_bounds line 623