OAI/Combinatorics/ProgressionColoring/ConstructionModel.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformCount line 17

    Source documentation

    The number of first-system intervals: exactly 1 / Hx.

    def uniformCount (k : ℕ) : ℕ := k ^ 2 * lambda k

    Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda

  2. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformCount_pos line 19
  3. def OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh line 23

    Source documentation

    The actual exponential second-system mesh, using the selected base.

    def mesh (s : Data k) (hk : 3 ≤ k) : AdaptiveMesh :=
…

    Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.AdaptiveMesh

  4. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh_H line 26
  5. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh_alpha line 29
  6. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh_R line 32
  7. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh_m line 35
  8. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh_small line 39
  9. abbrev OAI.QuantitativeVanDerWaerden.ConstructionModel.Label line 42
  10. def OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabel line 48

    Source documentation

    Actual full labels of actual cyclic points. This specializes the generic literal-label definition also used in the heavy-label return proof.

    def fullLabel (s : Data k) (hk : 3 ≤ k) (n : Group s) : Label s hk :=
…

    Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.Group, OAI.QuantitativeVanDerWaerden.ConstructionModel.Label

  11. def OAI.QuantitativeVanDerWaerden.ConstructionModel.firstLabel line 52
  12. def OAI.QuantitativeVanDerWaerden.ConstructionModel.secondLabel line 55
  13. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.firstLabel_apply line 58
  14. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.secondLabel_apply line 63
  15. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabel_eq_pair line 68
  16. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.firstLabel_contains line 71
  17. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.secondLabel_contains line 78
  18. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabel_eq_iff line 87

    Source documentation

    Full-label equality means exactly membership in all the specified half-open coordinate intervals, including their boundary conventions.

    theorem fullLabel_eq_iff (s : Data k) (hk : 3 ≤ k)
    (n : Group s) (label : Label s hk) :
    fullLabel s hk n = label ↔
      (∀ i, UniformMesh.Contains (uniformCount k) (label.1 i)
        (xRep s.q (dimension k) n i)) ∧
      (∀ i, (mesh s hk).Contains (label.2 i)
        (yRep s.q (dimension k) (lambda k) n i)) :=
…

    Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.Group, OAI.QuantitativeVanDerWaerden.ConstructionModel.Label, OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabel, OAI.QuantitativeVanDerWaerden.UniformMesh.Contains, OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformCount, OAI.QuantitativeVanDerWaerden.xRep, OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh, OAI.QuantitativeVanDerWaerden.yRep, OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda

  19. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformWidth_eq line 97
  20. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.first_width line 101
  21. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabel_same_first_distance line 106
  22. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabel_same_second_distance line 115
  23. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.card_first_labels line 123
  24. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.card_second_labels line 126
  25. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.card_labels line 130
  26. theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.card_second_labels_le line 136
  27. def OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabelWord line 143

    Source documentation

    The actual label word of an ordered cyclic progression. No nonzero-step condition is needed to define the word; event families impose it separately.

    def fullLabelWord (s : Data k) (hk : 3 ≤ k) (ad : Group s × Group s) :
    Fin k → Label s hk :=
…

    Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.Group, OAI.QuantitativeVanDerWaerden.ConstructionModel.Label