OAI/Combinatorics/Progressions/Sampling/LayerSamplerWitnessScale.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.heterogeneousSamplerSides line 11
  2. theorem OAI.Erdos3.heterogeneousSamplerSides_pos line 18
  3. theorem OAI.Erdos3.heterogeneousSamplerSides_le line 28
  4. theorem OAI.Erdos3.heterogeneousSamplerSides_integer_principal line 38
  5. theorem OAI.Erdos3.heterogeneousSamplerSides_continuous_principal line 48
  6. abbrev OAI.Erdos3.VectorPolynomial.LayerSamplerAxis line 70
  7. def OAI.Erdos3.VectorPolynomial.layerSamplerDegree line 73
  8. abbrev OAI.Erdos3.VectorPolynomial.LayerSamplerVariables line 76
  9. def OAI.Erdos3.VectorPolynomial.layerContinuousPrincipalSlots line 82
  10. def OAI.Erdos3.VectorPolynomial.layerIntegerPrincipalSlots line 86
  11. theorem OAI.Erdos3.VectorPolynomial.layerContinuousPrincipalSlots_card line 90
  12. theorem OAI.Erdos3.VectorPolynomial.layerIntegerPrincipalSlots_card line 94
  13. theorem OAI.Erdos3.VectorPolynomial.layerContinuousPrincipalSlots_not_constant line 98
  14. theorem OAI.Erdos3.VectorPolynomial.layerIntegerPrincipalSlots_not_constant line 102
  15. def OAI.Erdos3.VectorPolynomial.layerSamplerDenominators line 110
  16. def OAI.Erdos3.VectorPolynomial.layerSamplerWidths line 113
  17. def OAI.Erdos3.VectorPolynomial.layerSamplerSides line 116
  18. theorem OAI.Erdos3.VectorPolynomial.layerSamplerSides_pos line 120
  19. theorem OAI.Erdos3.VectorPolynomial.layerSamplerSides_le line 124
  20. theorem OAI.Erdos3.VectorPolynomial.layerSamplerSides_integer_principal line 128
  21. theorem OAI.Erdos3.VectorPolynomial.layerSamplerSides_continuous_principal line 137
  22. def OAI.Erdos3.VectorPolynomial.layerSamplerTailWidth line 159
  23. def OAI.Erdos3.VectorPolynomial.layerSamplerGapWidth line 163
  24. def OAI.Erdos3.VectorPolynomial.layerSamplerScaleBound line 166
  25. structure OAI.Erdos3.VectorPolynomial.LayerSamplerScale line 170
  26. theorem OAI.Erdos3.VectorPolynomial.exists_layerSamplerScale line 178
  27. def OAI.Erdos3.VectorPolynomial.selectedLayerSamplerScale line 187
  28. theorem OAI.Erdos3.VectorPolynomial.selectedLayerSamplerScale_bounds line 191
  29. def OAI.Erdos3.VectorPolynomial.layerSamplerBox line 198
  30. theorem OAI.Erdos3.VectorPolynomial.layerSamplerBox_one_le line 201
  31. theorem OAI.Erdos3.VectorPolynomial.layerSamplerBox_le line 208
  32. theorem OAI.Erdos3.principalSamplingGapRatio_antitone line 221
  33. def OAI.Erdos3.VectorPolynomial.layerSamplerWitnessScaleBound line 236
  34. theorem OAI.Erdos3.VectorPolynomial.exists_layerSamplerWitnessScale line 241
  35. theorem OAI.Erdos3.VectorPolynomial.layerSamplerWitnessScaleBound_exp_bound line 274