OAI/Combinatorics/ProgressionColoring/Asymptotics.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Absolute thresholds for the construction

The eventual assertions here concern natural progression lengths only. In particular, their thresholds are chosen before any number of colors is supplied.

  1. structure OAI.QuantitativeVanDerWaerden.Parameters.BasicScales line 23

    Source documentation

    A convenient finite list of stronger scale inequalities. Existence is proved below from the actual parameter definitions.

    structure BasicScales (k : ℕ) : Prop where
…
  2. theorem OAI.QuantitativeVanDerWaerden.Parameters.dimension_tendsto line 31
  3. theorem OAI.QuantitativeVanDerWaerden.Parameters.cutoff_tendsto line 37
  4. theorem OAI.QuantitativeVanDerWaerden.Parameters.flipProbability_tendsto line 43
  5. theorem OAI.QuantitativeVanDerWaerden.Parameters.eventually_basicScales line 49
  6. theorem OAI.QuantitativeVanDerWaerden.Parameters.exists_basicScales_threshold line 76
  7. structure OAI.QuantitativeVanDerWaerden.Parameters.GeometryScales line 80

    Source documentation

    All elementary small-mesh inequalities used in the geometric dichotomy.

    structure GeometryScales (k : ℕ) : Prop where
…
  8. theorem OAI.QuantitativeVanDerWaerden.Parameters.geometryScales_of_basic line 95
  9. theorem OAI.QuantitativeVanDerWaerden.Parameters.eventually_geometryScales line 141
  10. theorem OAI.QuantitativeVanDerWaerden.Parameters.exists_geometryScales_threshold line 146