OuterWordTests.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The first family of outer-coloring tests

For each full word with sufficiently many light positions, choose the proved cyclic row decomposition of its light positions. Its tests are the actual sets of distinct labels occurring in these rows. All choices depend on the word and the parameters, before a coloring is chosen.

def OAI.QuantitativeVanDerWaerden.OuterWordTests.multiplicity line 25
Source documentation
Full-word multiplicity of a label.
```
def multiplicity (word : Fin k → Label) (b : Label) : ℕ :=
…
```
def OAI.QuantitativeVanDerWaerden.OuterWordTests.lightPositions line 29
Source documentation
Lightness is measured in the full word, before restriction to light positions.
```
def lightPositions (M : ℕ) (word : Fin k → Label) : Finset (Fin k) :=
…
```
theorem OAI.QuantitativeVanDerWaerden.OuterWordTests.mem_lightPositions line 33
abbrev OAI.QuantitativeVanDerWaerden.OuterWordTests.LightPosition line 37

theorem OAI.QuantitativeVanDerWaerden.OuterWordTests.light_fiber_card_le line 40

Source documentation

Each restricted label fibre is bounded by the full-word light multiplicity.

theorem light_fiber_card_le {Label : Type uLabel} [Fintype Label] [DecidableEq Label]
    {k : ℕ}
    (M : ℕ) (hM : 0 < M) (word : Fin k → Label)
    (b : Label) :
    Fintype.card {i : LightPosition M word // word i = b} ≤ k / M := by
…

Mentions: OAI.QuantitativeVanDerWaerden.OuterWordTests.LightPosition

theorem OAI.QuantitativeVanDerWaerden.OuterWordTests.word_rows_exist line 69

Source documentation

The actual row decomposition exists for each eligible full word.

theorem word_rows_exist (M : ℕ) (hM : 0 < M) (hMk : M ≤ k)
    (word : Fin k → Label) (heligible : k ≤ 10 * (lightPositions M word).card) :
    ∃ rows : Fin (k / M) → Finset (LightPosition M word),
      (∀ i, ∃! r, i ∈ rows r) ∧
      (∀ r, Set.InjOn (fun i : LightPosition M word => word i) (rows r)) ∧
      (∀ r, M / 10 ≤ (rows r).card) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.OuterWordTests.lightPositions, OAI.QuantitativeVanDerWaerden.OuterWordTests.LightPosition

def OAI.QuantitativeVanDerWaerden.OuterWordTests.wordRows line 82
theorem OAI.QuantitativeVanDerWaerden.OuterWordTests.wordRows_spec line 87
def OAI.QuantitativeVanDerWaerden.OuterWordTests.eligibleWords line 95
abbrev OAI.QuantitativeVanDerWaerden.OuterWordTests.TestIndex line 98
theorem OAI.QuantitativeVanDerWaerden.OuterWordTests.testIndex_card_le line 102
def OAI.QuantitativeVanDerWaerden.OuterWordTests.support line 113
Source documentation
Literal support of an indexed first-family row test.
```
noncomputable def support (M : ℕ) (hM : 0 < M) (hMk : M ≤ k)
    (words : Finset (Fin k → Label)) (i : TestIndex M words) : Finset Label :=
…
```
Mentions: OAI.QuantitativeVanDerWaerden.OuterWordTests.TestIndex
theorem OAI.QuantitativeVanDerWaerden.OuterWordTests.support_card_eq line 118
theorem OAI.QuantitativeVanDerWaerden.OuterWordTests.support_card_lower line 125
theorem OAI.QuantitativeVanDerWaerden.OuterWordTests.support_card_real_lower line 131
theorem OAI.QuantitativeVanDerWaerden.OuterWordTests.light_selected_card line 138
Source documentation
Restricting to the subtype of light positions does not change selected counts.
```
theorem light_selected_card (M : ℕ) (word : Fin k → Label) (p : Fin k → Prop)
    [DecidablePred p] :
    (Finset.univ.filter (fun i : LightPosition M word => p i)).card =
      ((lightPositions M word).filter p).card := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.OuterWordTests.LightPosition, OAI.QuantitativeVanDerWaerden.OuterWordTests.lightPositions

theorem OAI.QuantitativeVanDerWaerden.OuterWordTests.supports_balance_words line 162

Source documentation

Balancing every constructed support balances the light positions of each eligible input word, with its original position multiplicities retained.

theorem supports_balance_words (M : ℕ) (hM : 0 < M) (hMk : M ≤ k)
    (words : Finset (Fin k → Label)) (color : Label → Bool)
    (hbalance : ∀ i b, (support M hM hMk words i).card ≤
      4 * ((support M hM hMk words i).filter fun a => color a = b).card) :
    ∀ word ∈ words, k ≤ 10 * (lightPositions M word).card → ∀ b,
      (lightPositions M word).card ≤
        4 * ((lightPositions M word).filter fun i => color (word i) = b).card := by
…

Mentions: OAI.QuantitativeVanDerWaerden.OuterWordTests.support, OAI.QuantitativeVanDerWaerden.OuterWordTests.lightPositions

theorem OAI.QuantitativeVanDerWaerden.OuterWordTests.incident_weight_le line 198

Source documentation

A first-family label-incident sum is bounded using the total test count. The row index is retained even when supports happen to coincide.

theorem incident_weight_le (M : ℕ) (hM : 0 < M) (hMk : M ≤ k)
    (words : Finset (Fin k → Label)) (b : Label) :
    (∑ i ∈ Finset.univ.filter (fun i : TestIndex M words => b ∈ support M hM hMk words i),
        Real.exp (-((support M hM hMk words i).card : ℝ) / 32)) ≤
      ((k * words.card : ℕ) : ℝ) * Real.exp (-((M : ℝ) / 10 - 1) / 32) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.OuterWordTests.TestIndex, OAI.QuantitativeVanDerWaerden.OuterWordTests.support