OAI/Combinatorics/ProgressionColoring/LabelIncidences.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.QuantitativeVanDerWaerden.card_decoded_twoSystems_le line 11

   Source documentation

   Decode two independent coordinate systems without identifying their scalar output types. This is also the global full-word product estimate.

   theorem card_decoded_twoSystems_le {D B : ℕ} {α : Type uAlpha} {β : Type uBeta} {Word : Type uWord}
       [DecidableEq Word] (firstS : Fin D → Finset α) (secondS : Fin D → Finset β)
       (decode : ((Fin D → α) × (Fin D → β)) → Word)
       (hfirst : ∀ i, (firstS i).card ≤ B) (hsecond : ∀ i, (secondS i).card ≤ B) :
       (((coordinateFamily firstS).product (coordinateFamily secondS)).image decode).card ≤
         B ^ (2 * D) := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.coordinateFamily

2. def OAI.QuantitativeVanDerWaerden.anchoredIncidences line 31

   Source documentation

   Literal (step vector, recorded word) incidences, retaining the step vector even when two different steps yield the same word. The two scalar systems have their actual different output types.

   noncomputable def anchoredIncidences {D h : ℕ} {U : Type uU} {V : Type uV}
       (firstS : (Fin D → Fin h) → Fin h → Fin D → Finset (Fin h → U))
       (secondS : (Fin D → Fin h) → Fin h → Fin D → Finset (Fin h → Option V)) :
       Finset ((Fin D → Fin h) × (Fin h → Option (FullLabel D U V))) := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.FullLabel

3. theorem OAI.QuantitativeVanDerWaerden.mem_anchoredIncidences_of_mem line 40
4. theorem OAI.QuantitativeVanDerWaerden.card_anchoredIncidences_le line 56
5. theorem OAI.QuantitativeVanDerWaerden.card_anchoredIncidences_polynomial_le line 78