OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternActualLines.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPatternValueData line 11
2. theorem OAI.Ostmann.movingPatternActualBaseAverage line 23

   Source documentation

   The field average over both original giant residues is precisely the simultaneous line probability appearing in the fixed-coordinate comparison. This identification needs no assumptions forbidding sample coincidences.

   theorem movingPatternActualBaseAverage {A B C : Type*} {N : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (prime : A → ℕ) (hprime : ∀ a, (prime a).Prime)
       (n : ℕ) (t : Bool → FrequencyTree ℤ n) (small bulk : Bool → TreeLeafTuple (List B) n)
       (pattern : Bool × MovingSampleIndex n → C) (x : Fin (N + 1) → A) (c : C) :
       let p := prime (x (e.symm (.inr c)))
   …

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