OAI/Combinatorics/Progressions/Estimates/AllocatedShortAxis.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.tailAxisInterpolation line 10
  2. def OAI.Erdos3.tailAxisInterpolationCap line 15
  3. def OAI.Erdos3.tailAxisInterpolationLip line 18
  4. theorem OAI.Erdos3.tailAxisInterpolation_spec line 22
  5. def OAI.Erdos3.allocatedProjectionPMFs line 76
  6. def OAI.Erdos3.allocatedMixedArrayLaw line 85
  7. theorem OAI.Erdos3.allocatedMixedArrayLaw_probability line 92
  8. theorem OAI.Erdos3.allocatedMixedArray_quotient_density line 99
  9. theorem OAI.Erdos3.allocatedMixedArray_ae_chart line 127
  10. def OAI.Erdos3.allocatedArrayCenters line 165
  11. def OAI.Erdos3.allocatedArrayWidths line 169
  12. theorem OAI.Erdos3.allocatedArrayWidths_pos line 174
  13. theorem OAI.Erdos3.allocatedArrayProfiles_bound line 179
  14. theorem OAI.Erdos3.allocatedArraySupported_iff_rows line 187
  15. theorem OAI.Erdos3.allocatedArrayLaw_rows line 195
  16. theorem OAI.Erdos3.allocatedArrayColumns_chart line 227
  17. theorem OAI.Erdos3.allocatedArraySupported_polynomial_chart line 247
  18. def OAI.Erdos3.allocatedWidthFloor line 276
  19. theorem OAI.Erdos3.allocatedWidthFloor_pos line 279
  20. theorem OAI.Erdos3.allocatedArrayWidths_floor line 286
  21. theorem OAI.Erdos3.allocatedProfile_inverse_power_bounds line 326
  22. theorem OAI.Erdos3.allocatedWidthFloor_inverse_power_bound line 356
  23. theorem OAI.Erdos3.allocatedProfile_inverse_exp_bounds line 385
  24. theorem OAI.Erdos3.allocatedWidthFloor_inverse_exp_bound line 405
  25. def OAI.Erdos3.allocatedScaleLog line 429
  26. theorem OAI.Erdos3.allocatedScaleLog_nonneg line 431
  27. theorem OAI.Erdos3.le_allocatedScaleLog line 435
  28. theorem OAI.Erdos3.VectorPolynomial.layerSamplerWidths_inverse_exp_bounds line 445
  29. theorem OAI.Erdos3.VectorPolynomial.layerSamplerScaleBound_exp line 460
  30. theorem OAI.Erdos3.VectorPolynomial.selectedLayerSamplerScale_exp_bound line 485
  31. theorem OAI.Erdos3.heterogeneousSamplerSides_long_or_bounded line 507
  32. theorem OAI.Erdos3.VectorPolynomial.selectedLayerSampler_integer_side_dichotomy line 527