OAI/Combinatorics/Progressions/Sampling/ForecastPreparedScaleBudget.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.preparedSamplerBlockCount line 15
  2. theorem OAI.Erdos3.VectorPolynomial.preparedSamplerBlockCount_positive line 21
  3. theorem OAI.Erdos3.VectorPolynomial.preparedSamplerBlockCount_spectrum line 24
  4. theorem OAI.Erdos3.VectorPolynomial.preparedSamplerBlockCount_jets line 30
  5. abbrev OAI.Erdos3.VectorPolynomial.PreparedSamplerContinuous line 37
  6. def OAI.Erdos3.VectorPolynomial.preparedSamplerTransverse line 39
  7. abbrev OAI.Erdos3.VectorPolynomial.PreparedSamplerBlock line 42
  8. def OAI.Erdos3.VectorPolynomial.preparedSamplerDimension line 46
  9. theorem OAI.Erdos3.VectorPolynomial.preparedSamplerDimension_ge line 49
  10. theorem OAI.Erdos3.VectorPolynomial.preparedSampler_axis_card line 53
  11. theorem OAI.Erdos3.VectorPolynomial.preparedSampler_variables_card line 59
  12. theorem OAI.Erdos3.VectorPolynomial.preparedSampler_dimensions line 75
  13. def OAI.Erdos3.VectorPolynomial.preparedCommonBlockCount line 118
  14. theorem OAI.Erdos3.VectorPolynomial.preparedCommonBlockCount_ge line 121
  15. theorem OAI.Erdos3.VectorPolynomial.preparedCommonBlockCount_positive line 127
  16. theorem OAI.Erdos3.VectorPolynomial.preparedCommonBlockCount_spectrum line 131
  17. theorem OAI.Erdos3.VectorPolynomial.preparedCommonBlockCount_jets line 138
  18. abbrev OAI.Erdos3.VectorPolynomial.PreparedCommonKernel line 142
  19. theorem OAI.Erdos3.VectorPolynomial.preparedCommonKernel_card line 144
  20. abbrev OAI.Erdos3.VectorPolynomial.PreparedCommonSamplerBlock line 151
  21. def OAI.Erdos3.VectorPolynomial.preparedCommonSamplerDimension line 155
  22. theorem OAI.Erdos3.VectorPolynomial.preparedCommonSamplerDimension_ge line 158
  23. theorem OAI.Erdos3.VectorPolynomial.preparedCommonSampler_variables_card line 162
  24. theorem OAI.Erdos3.VectorPolynomial.preparedCommonSampler_dimensions line 178
  25. def OAI.Erdos3.VectorPolynomial.preparedCommonBlockCountWithCutoff line 220
  26. theorem OAI.Erdos3.VectorPolynomial.preparedCommonBlockCountWithCutoff_ge line 223
  27. theorem OAI.Erdos3.VectorPolynomial.preparedCommonBlockCountWithCutoff_positive line 229
  28. theorem OAI.Erdos3.VectorPolynomial.preparedCommonBlockCountWithCutoff_spectrum line 233
  29. theorem OAI.Erdos3.VectorPolynomial.preparedCommonBlockCountWithCutoff_jets line 240
  30. def OAI.Erdos3.VectorPolynomial.preparedCommonSamplerDimensionWithCutoff line 244
  31. abbrev OAI.Erdos3.VectorPolynomial.EnlargedPreparedCommonKernelWithCutoff line 247
  32. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonKernelWithCutoff_analytic_capacity line 250
  33. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonKernelWithCutoff_allocation_capacity line 255
  34. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonKernelWithCutoff_multiple_capacity line 263
  35. def OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonCanonicalSelectionWithCutoff line 268
  36. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonCanonicalSelectionWithCutoff_val line 278
  37. def OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerDimensionWithCutoff line 282
  38. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerDimensionWithCutoff_polynomial line 286
  39. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerDimensionWithCutoff_ge line 294
  40. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerDimensionWithCutoff_allocation line 299
  41. abbrev OAI.Erdos3.VectorPolynomial.EnlargedPreparedCommonSamplerBlockWithCutoff line 306
  42. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlockWithCutoff_allocation line 310
  43. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlockWithCutoff_positive line 316
  44. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlockWithCutoff_jets line 322
  45. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlockWithCutoff_spectrum line 330
  46. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlockWithCutoff_positiveModerate line 340
  47. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlockWithCutoff_uniform line 353
  48. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerWithCutoff_variables_card line 360
  49. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerWithCutoff_dimensions line 377
  50. theorem OAI.Erdos3.VectorPolynomial.preparedForecastJacobian_budget line 419
  51. abbrev OAI.Erdos3.VectorPolynomial.EnlargedPreparedCommonKernel line 496
  52. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonKernel_analytic_capacity line 499
  53. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonKernel_allocation_capacity line 504
  54. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonKernel_multiple_capacity line 512
  55. def OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonCanonicalSelection line 517
  56. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonCanonicalSelection_val line 527
  57. def OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerDimension line 531
  58. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerDimension_polynomial line 535
  59. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerDimension_ge line 543
  60. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerDimension_allocation line 548
  61. abbrev OAI.Erdos3.VectorPolynomial.EnlargedPreparedCommonSamplerBlock line 555
  62. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlock_allocation line 559
  63. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlock_positive line 565
  64. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlock_jets line 571
  65. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlock_spectrum line 579
  66. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlock_positiveModerate line 589
  67. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlock_uniform line 602
  68. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSampler_variables_card line 609
  69. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSampler_dimensions line 626
  70. theorem OAI.Erdos3.VectorPolynomial.forecast_block_card_le_variables line 667
  71. theorem OAI.Erdos3.VectorPolynomial.prepared_forecast_independent_scale_budget line 678