OAI/Combinatorics/Progressions/Estimates/EmptyLayerPrescribedScale.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.layerSamplerTailScaleFloor line 16
  2. theorem OAI.Erdos3.VectorPolynomial.layerSamplerTailWidth_of_scaleFloor line 21
  3. theorem OAI.Erdos3.VectorPolynomial.layerSamplerTailScaleFloor_le_exp line 35
  4. def OAI.Erdos3.VectorPolynomial.emptyLayerSamplerScale line 68
  5. theorem OAI.Erdos3.VectorPolynomial.emptyLayerSamplerScale_value line 77
  6. def OAI.Erdos3.VectorPolynomial.emptyLayerSamplerScaleOfFloor line 82
  7. theorem OAI.Erdos3.VectorPolynomial.emptyLayerSamplerScaleOfFloor_value line 89
  8. def OAI.Erdos3.VectorPolynomial.emptyLayerSamplerScaleOfExp line 95
  9. theorem OAI.Erdos3.VectorPolynomial.emptyLayerSamplerScaleOfExp_value line 108