LabelCounts.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.QuantitativeVanDerWaerden.FullLabel line 16
Source documentation
A full label retains the literal first and second interval labels.
```
abbrev FullLabel (D : ℕ) (U : Type uU) (V : Type uV) := (Fin D → U) × (Fin D → V)
```
def OAI.QuantitativeVanDerWaerden.assembleLabel line 21
Source documentation
The full output is dummy exactly when some second-coordinate output is dummy. Stationary coordinates are supplied as some of their untruncated label; rotating coordinates use the actual truncated output.
```
noncomputable def assembleLabel {D : ℕ} {U : Type uU} {V : Type uV}
    (first : Fin D → U) (second : Fin D → Option V) : Option (FullLabel D U V) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.FullLabel
theorem OAI.QuantitativeVanDerWaerden.assembleLabel_eq_none_iff line 27
theorem OAI.QuantitativeVanDerWaerden.assembleLabel_some line 48

def OAI.QuantitativeVanDerWaerden.assembleWord line 60

Source documentation

Pointwise reconstruction introduces no independent choice of a mask.

noncomputable def assembleWord {D h : ℕ} {U : Type uU} {V : Type uV}
    (first : Fin D → Fin h → U) (second : Fin D → Fin h → Option V) :
    Fin h → Option (FullLabel D U V) :=
…

Mentions: OAI.QuantitativeVanDerWaerden.FullLabel

theorem OAI.QuantitativeVanDerWaerden.assembleWord_dummy_iff line 65
def OAI.QuantitativeVanDerWaerden.coordinateFamily line 72
Source documentation
All tuples of independently allowed scalar words. Dependent coordinate types permit first words and truncated second words to have different types.
```
noncomputable def coordinateFamily {n : ℕ} {α : Fin n → Type uAlpha}
    (S : ∀ i, Finset (α i)) : Finset (∀ i, α i) := by
…
```
theorem OAI.QuantitativeVanDerWaerden.card_coordinateFamily_le line 77

theorem OAI.QuantitativeVanDerWaerden.card_decoded_coordinateFamily_le line 89

Source documentation

Arbitrary decoding cannot increase the product count. This applies to literal full words and to pointwise dummy reconstruction alike.

theorem card_decoded_coordinateFamily_le {n B : ℕ} {α : Fin n → Type uAlpha}
    {Word : Type uWord} [DecidableEq Word]
    (S : ∀ i, Finset (α i)) (decode : (∀ i, α i) → Word)
    (hS : ∀ i, (S i).card ≤ B) :
    ((coordinateFamily S).image decode).card ≤ B ^ n :=
…

Mentions: OAI.QuantitativeVanDerWaerden.coordinateFamily

def OAI.QuantitativeVanDerWaerden.anchoredFamily line 99

Source documentation

The finite union over all rational step vectors and all possible anchor positions. The scalar families can depend on both, as in the actual re-anchored breakpoint construction.

noncomputable def anchoredFamily {D h : ℕ} {α : Fin (2 * D) → Type uAlpha}
    {Word : Type uWord} [DecidableEq Word]
    (S : (Fin D → Fin h) → Fin h → ∀ i, Finset (α i))
    (decode : (Fin D → Fin h) → Fin h → (∀ i, α i) → Word) : Finset Word := by
…

theorem OAI.QuantitativeVanDerWaerden.card_anchoredFamily_le line 107
theorem OAI.QuantitativeVanDerWaerden.anchored_polynomial_estimate line 128