LabelFiber.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite fibers of labels in an indexed word

Natural-number indices make differences and return times convenient. The cardinality bridge identifies this fiber with the usual multiplicity counted over Fin k, and separation of the fiber excludes every earlier return.

def OAI.QuantitativeVanDerWaerden.labelFiber line 20
Source documentation
Indices before k at which the word has label l.
```
noncomputable def labelFiber {β : Type uBeta} (k : ℕ) (f : ℕ → β) (l : β) : Finset ℕ := by
…
```
theorem OAI.QuantitativeVanDerWaerden.mem_labelFiber line 25
theorem OAI.QuantitativeVanDerWaerden.card_labelFiber line 32
Source documentation
The natural-index fiber counts exactly the label multiplicity over Fin k.
```
theorem card_labelFiber {β : Type uBeta} (k : ℕ) (f : ℕ → β) (l : β) :
    (labelFiber k f l).card =
      (Finset.univ.filter (fun j : Fin k => f j.val = l)).card := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.labelFiber

theorem OAI.QuantitativeVanDerWaerden.no_earlier_label_return line 49

Source documentation

A minimum positive gap between occurrences of a label rules out a return at every positive time below that gap.

theorem no_earlier_label_return {β : Type uBeta} {k j h : ℕ} {f : ℕ → β} {l : β}
    (hj : j ∈ labelFiber k f l) (hjh : j + h < k)
    (hmin : ∀ a ∈ labelFiber k f l, ∀ b ∈ labelFiber k f l,
      a < b → h ≤ b - a) :
    ∀ t, 0 < t → t < h → f (j + t) ≠ l := by
…

Mentions: OAI.QuantitativeVanDerWaerden.labelFiber