OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternLines.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingPatternLineProbability line 15

   Source documentation

   The uniqueness and tier conditions of the fixed row system are consequences of the exact equality-pattern coordinates. They are not additional arithmetic assumptions about the original samples.

   theorem movingPatternLineProbability {I A : Type*} [Fintype I]
       (s : Setoid I) {N n : ℕ} (hcard : Fintype.card (Quotient s) = N + 1)
       (z : Quotient s → A) (hz : Function.Injective z)
       (prime : A → ℕ) (hpInj : Function.Injective prime) (hprime : ∀ a, (prime a).Prime)
       (T : Bool → MovingSlotData I n) (tier : I → ℕ)
       (htier : ∀ i j, s i j → tier i = tier j) (hlevels : ∀ side, (T side).Levels tier)
       (c : Fin (N + 1))
       (base : MovingPairRepresentativeOccurrences
         (fun side => (T side).map (samplePatternLabels s hcard)) c)
       (hf : ∀ side, (T side).Frequencies (fun a =>
         (a : ZMod (prime (samplePatternValues s hcard z c))) ≠ 0)) :
       let v := fun i => prime (z (Quotient.mk'' i))
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingPairRepresentativeOccurrences, OAI.Ostmann.samplePatternLabels, OAI.Ostmann.samplePatternValues