OAI/Combinatorics/ProgressionColoring/OuterPatternColoring.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous balancing of words and recorded local patterns

The global tests are constructed from the actual light-position fibers. The local tests retain precisely the labels recorded by their Option-valued words. The only counting inputs are the finite word and anchored-pattern bounds; all probability, row partitioning and support-to-position conversions are proved.

  1. theorem OAI.QuantitativeVanDerWaerden.exists_outer_word_pattern_coloring line 22
  2. theorem OAI.QuantitativeVanDerWaerden.rich_of_light_balanced line 85

    Source documentation

    The light-position alternative already gives the required whole-word frequency bound, with slack from one fortieth to one hundredth.

    theorem rich_of_light_balanced {Label : Type uLabel} [DecidableEq Label] {k M : ℕ}
    (word : Fin k → Label) (color : Label → Bool)
    (hlight : k ≤ 10 * (OuterWordTests.lightPositions M word).card)
    (hbalance : ∀ b, (OuterWordTests.lightPositions M word).card ≤
      4 * ((OuterWordTests.lightPositions M word).filter fun j => color (word j) = b).card) :
    ∀ b, k ≤ 100 * (Finset.univ.filter fun j => color (word j) = b).card := by
…

    Mentions: OAI.QuantitativeVanDerWaerden.OuterWordTests.lightPositions