OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternEnumeration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A concrete finite enumeration for every equality pattern

  1. theorem OAI.Ostmann.movingPattern_enumeration line 11

    Source documentation

    The same ambient coordinate budget covers every quotient pattern.

    theorem movingPattern_enumeration (B : Type) [Fintype B] (b : B) (n : ℕ) :
    ∃ (N : Setoid (Bool × MovingSampleIndex n) → ℕ)
      (_e : ∀ s : Setoid (Bool × MovingSampleIndex n), Fin (N s + 1) ≃ B ⊕ Quotient s),
      ∀ s, N s + 1 ≤ Fintype.card B + 4 * n * 2 ^ n := by
…

    Mentions: OAI.Ostmann.MovingSampleIndex