OAI/Combinatorics/ProgressionColoring/LiteralLabelRectangles.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QuantitativeVanDerWaerden.literalFullLabel line 11

   Source documentation

   The actual two-system full label of a cyclic point.

   def literalFullLabel (mesh : AdaptiveMesh) (q D lam Ucount : ℕ)
       (hU : 0 < Ucount) (n : CyclicGroup q D) :
       (Fin D → Fin Ucount) × (Fin D → mesh.Label) :=
   …

   Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.CyclicGroup

2. theorem OAI.QuantitativeVanDerWaerden.uniformLabel_xRep_eq_iff line 17
3. theorem OAI.QuantitativeVanDerWaerden.meshLabel_yRep_eq_iff line 24
4. theorem OAI.QuantitativeVanDerWaerden.literalFullLabel_first_mem line 32
5. theorem OAI.QuantitativeVanDerWaerden.literalFullLabel_second_mem line 38
6. theorem OAI.QuantitativeVanDerWaerden.literalFullLabel_eq_iff line 45

   Source documentation

   Both directions use the actual half-open mesh labels.

   theorem literalFullLabel_eq_iff (mesh : AdaptiveMesh) (q D lam Ucount : ℕ)
       (hU : 0 < Ucount) (n : CyclicGroup q D)
       (beta : (Fin D → Fin Ucount) × (Fin D → mesh.Label)) :
       literalFullLabel mesh q D lam Ucount hU n = beta ↔
         (∀ i, UniformMesh.Contains Ucount (beta.1 i) (xRep q D n i)) ∧
         (∀ i, mesh.Contains (beta.2 i) (yRep q D lam n i)) := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.literalFullLabel, OAI.QuantitativeVanDerWaerden.UniformMesh.Contains, OAI.QuantitativeVanDerWaerden.xRep, OAI.QuantitativeVanDerWaerden.yRep

7. theorem OAI.QuantitativeVanDerWaerden.literalFullLabel_eq_iff_mem_rectangle line 68

   Source documentation

   An unfolded rectangle API, retaining every excluded upper endpoint.

   theorem literalFullLabel_eq_iff_mem_rectangle (mesh : AdaptiveMesh)
       (q D lam Ucount : ℕ) (hU : 0 < Ucount) (n : CyclicGroup q D)
       (beta : (Fin D → Fin Ucount) × (Fin D → mesh.Label)) :
       literalFullLabel mesh q D lam Ucount hU n = beta ↔
         (∀ i, UniformMesh.left Ucount (beta.1 i) ≤ xRep q D n i ∧
           xRep q D n i < UniformMesh.right Ucount (beta.1 i)) ∧
         (∀ i, mesh.left (beta.2 i) ≤ yRep q D lam n i ∧
           yRep q D lam n i < mesh.right (beta.2 i)) :=
   …

   Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.literalFullLabel, OAI.QuantitativeVanDerWaerden.UniformMesh.left, OAI.QuantitativeVanDerWaerden.xRep, OAI.QuantitativeVanDerWaerden.UniformMesh.right, OAI.QuantitativeVanDerWaerden.yRep

8. theorem OAI.QuantitativeVanDerWaerden.literalFullLabel_first_endpoints line 78
9. theorem OAI.QuantitativeVanDerWaerden.literalFullLabel_second_endpoints line 88
10. theorem OAI.QuantitativeVanDerWaerden.literalFullLabel_same_first_distance line 97
11. theorem OAI.QuantitativeVanDerWaerden.literalFullLabel_same_second_distance line 111