OAI/Combinatorics/Progressions/Linear/AllocatedKernelPrimitiveBudget.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.GoodScalarKernelTuple line 13
  2. theorem OAI.Erdos3.scalarKernel_bad_event_le line 18
  3. theorem OAI.Erdos3.exists_uniform_good_scalar_kernel_tuples line 40
  4. def OAI.Erdos3.scalarKernelConditioningConstant line 74
  5. def OAI.Erdos3.scalarKernelTailConstant line 77
  6. def OAI.Erdos3.scalarKernelAdjustedAccuracy line 80
  7. def OAI.Erdos3.scalarKernelThreshold line 83
  8. def OAI.Erdos3.scalarKernelCutoff line 88
  9. theorem OAI.Erdos3.scalarKernelConditioningConstant_pos line 95
  10. theorem OAI.Erdos3.scalarKernelTailConstant_pos line 99
  11. theorem OAI.Erdos3.scalarKernelAdjustedAccuracy_pos line 104
  12. theorem OAI.Erdos3.scalarKernelThreshold_pos line 109
  13. theorem OAI.Erdos3.scalarKernelCutoff_bounds line 120
  14. def OAI.Erdos3.normalizedScalarCubePivot line 135
  15. theorem OAI.Erdos3.normalizedScalarCubePivot_det line 139
  16. theorem OAI.Erdos3.normalizedScalarCubePivot_entry_bound line 149
  17. theorem OAI.Erdos3.goodScalarKernelTuple_pivot_inverse line 159
  18. theorem OAI.Erdos3.hasBoundedScalarPeriod_mono line 174
  19. theorem OAI.Erdos3.hasBoundedScalarPeriod_index_le line 180
  20. theorem OAI.Erdos3.goodScalarKernelTuple_mono line 187
  21. theorem OAI.Erdos3.exists_uniform_good_scalar_kernel_bound line 194
  22. def OAI.Erdos3.scalarKernelCutoffLogBudget line 220
  23. theorem OAI.Erdos3.scalarKernelCutoff_le_exp_of_bounds line 223
  24. theorem OAI.Erdos3.univariateSublevelConstant_le_exp line 269
  25. theorem OAI.Erdos3.multivariateSublevelConstant_le_exp line 290
  26. theorem OAI.Erdos3.integerScalarCubeDensityCap_le_exp line 307
  27. theorem OAI.Erdos3.scalarKernelTailConstant_le_exp line 319
  28. theorem OAI.Erdos3.coordinateDeterminantVariation_le_exp line 337
  29. theorem OAI.Erdos3.scalarKernel_explicit_probability_le line 351
  30. theorem OAI.Erdos3.scalarKernelConditioningConstant_le_exp line 399
  31. theorem OAI.Erdos3.scalarKernelAdjustedAccuracy_inv_le_exp line 422
  32. theorem OAI.Erdos3.scalarKernelMinorConstant_le_exp line 431
  33. theorem OAI.Erdos3.scalarKernelMinorScale_le_exp line 446
  34. def OAI.Erdos3.scalarKernelInputBudget line 455
  35. theorem OAI.Erdos3.scalarKernelInputBudget_bounds line 458
  36. def OAI.Erdos3.scalarKernelLogarithmicBudget line 496
  37. theorem OAI.Erdos3.scalarKernelCutoff_le_exp line 499
  38. theorem OAI.Erdos3.scalarKernelLogarithmicBudget_eq line 506
  39. def OAI.Erdos3.VectorPolynomial.allocatedKernelPrimitiveBudget line 518
  40. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelPrimitiveBudget_bounds line 524
  41. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelPrimitiveBudget_mono line 541
  42. theorem OAI.Erdos3.VectorPolynomial.scalarKernelLogarithmicBudget_le_allocatedPrimitive line 551
  43. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedKernelThreshold_bound line 572