LongPeriodColoring.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The long-period case for the coloring pulled back from the actual two-system full labels of the cyclic progression.

def OAI.QuantitativeVanDerWaerden.literalProgressionHeavy line 18
Source documentation
Heavy positions are defined by their literal full-label multiplicity in the entire progression, rather than within an individual block.
```
noncomputable def literalProgressionHeavy
    (mesh : AdaptiveMesh) (q D lambda n k : ℕ) (hn : 0 < n)
    (a d : CyclicGroup q D) (M : ℝ) (j : Fin k) : Prop := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.CyclicGroup

theorem OAI.QuantitativeVanDerWaerden.block_color_count_of_regular_balance line 29

Source documentation

Quarter-balance on at least half the positions gives an eighth of the whole block. The restriction to regular positions is removed by inclusion.

theorem block_color_count_of_regular_balance {h : ℕ}
    (S : Finset (Fin h)) (color : Fin h → Bool) (c : Bool)
    (hmany : h ≤ 2 * S.card)
    (hbalanced : S.card ≤ 4 * (S.filter fun z => color z = c).card) :
    (h : ℝ) / 8 ≤ ((Finset.univ.filter fun z => color z = c).card : ℝ) := by
…

theorem OAI.QuantitativeVanDerWaerden.literal_long_period_balanced line 47

Source documentation

The long-period case of the dichotomy for the actual cyclic pullback coloring. Half-block regularity and eligibility are proved by the preceding grid and mesh lemmas. Full blocks are counted through literal indices.

theorem literal_long_period_balanced
    (mesh : AdaptiveMesh) (q D lambda n k h : ℕ) (hn : 0 < n)
    (a d : CyclicGroup q D) (M : ℝ) (u v : Fin D → ℝ)
    (t : Fin D → Fin h) (hh : 0 < h) (hD : 3 ≤ D)
    (cstar : FullLabel D (Fin n) mesh.Label → Bool)
    (hprimitive : PrimitiveVector h (fun i => ((t i).val : ℤ)))
    (hX : ∀ j, j < k → ∀ i : Fin D, ∃ e : ℤ,
      xRep q D (a + j • d) i - xRep q D a i -
        (j : ℝ) / h * ((t i).val + u i) = e)
    (hY : ∀ j, j < k → ∀ i : Fin D, ∃ e : ℤ,
      yRep q D lambda (a + j • d) i - yRep q D lambda a i -
        (j : ℝ) / h * ((lambda : ℝ) * (t i).val + v i) = e)
…

Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.FullLabel, OAI.QuantitativeVanDerWaerden.PrimitiveVector, OAI.QuantitativeVanDerWaerden.xRep, OAI.QuantitativeVanDerWaerden.yRep