OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternFinite.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingPairRepresentative_map_nonempty line 12
2. def OAI.Ostmann.movingPatternFinData line 26
3. theorem OAI.Ostmann.movingPatternFinData_levels line 31
4. def OAI.Ostmann.movingPatternFinRepresentative line 44

   Source documentation

   The base row is selected from a proved original occurrence, then mapped into the finite coordinate system used by polynomial comparison.

   noncomputable def movingPatternFinRepresentative {B C : Type*} {N : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (n : ℕ) (t : Bool → FrequencyTree ℤ n)
       (small bulk : Bool → TreeLeafTuple (List B) n) (pattern : Bool × MovingSampleIndex n → C)
       (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c}) (c : C) :
       MovingPairRepresentativeOccurrences (movingPatternFinData e n t small bulk pattern)
         (e.symm (.inr c)) :=
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.MovingPairRepresentativeOccurrences, OAI.Ostmann.movingPatternFinData

5. theorem OAI.Ostmann.movingPatternFin_unique line 55

   Source documentation

   Original class injectivity and separation from external slots imply the unique-prime condition required by the simultaneous line comparison.

   theorem movingPatternFin_unique {A B C : Type*} {N : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (prime : A → ℕ) (hinj : Function.Injective prime)
       (x : Fin (N + 1) → A)
       (hclasses : Function.Injective (fun c => x (e.symm (.inr c))))
       (hcross : ∀ b c, prime (x (e.symm (.inl b))) ≠ prime (x (e.symm (.inr c))))
       (c : C) (i : Fin (N + 1)) (hi : prime (x i) = prime (x (e.symm (.inr c)))) :
       i = e.symm (.inr c) := by
   …