OAI/Combinatorics/ProgressionColoring/ConstructionModelBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Elementary bounds for the actual coordinate cells

These inequalities follow from the selected mesh and dilation definitions. They are not extra hypotheses on the finite geometric construction.

  1. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformWidth_le_meshH line 20
  2. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda_mul_uniformWidth line 26
  3. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh_alpha_le line 32