OAI/Combinatorics/Progressions/Estimates/AllocatedScalarLogBounds.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedLayerCenters line 19
  2. def OAI.Erdos3.VectorPolynomial.allocatedLayerWidths line 23
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerWidths_pos line 29
  4. def OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerPMFs line 34
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerColumns_chart line 45
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerSupported_polynomial_chart line 62
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerCenters_constant line 96
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerWidths_constant line 102
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerPMFs_constant line 108
  10. def OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerInterpolationCap line 130
  11. def OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerInterpolationLip line 137
  12. def OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerInterpolation line 148
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerInterpolation_spec line 156
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerInterpolation_lipschitz line 173
  15. def OAI.Erdos3.VectorPolynomial.allocatedPrincipalNormalizedSource line 204
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalNormalizedSource_law line 213
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalNormalizedSource_primitive line 236
  18. def OAI.Erdos3.VectorPolynomial.allocatedLayerCommonCap line 255
  19. def OAI.Erdos3.VectorPolynomial.allocatedLayerCommonLip line 258
  20. def OAI.Erdos3.VectorPolynomial.allocatedLayerWidthFloor line 261
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerCommonCap_one_le line 265
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerWidthFloor_pos line 268
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerWidths_floor line 278
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerInterpolation_common_bounds line 287
  25. theorem OAI.Erdos3.sum_le_exp_of_card_and_uniform_bound line 320
  26. def OAI.Erdos3.allocatedScalarLog line 327
  27. def OAI.Erdos3.allocatedCommonLog line 330
  28. def OAI.Erdos3.allocatedWidthLog line 332
  29. theorem OAI.Erdos3.allocatedScalarLog_nonneg line 334
  30. theorem OAI.Erdos3.allocatedCommonLog_nonneg line 338
  31. theorem OAI.Erdos3.allocatedWidthLog_nonneg line 343
  32. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerInterpolation_exp_bounds line 352
  33. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerCommonInterpolation_exp_bounds line 379
  34. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerWidthFloor_inv_exp line 401