OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternPrimeGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.exists_movingPatternPrimeGain line 14

   Source documentation

   A single mixed-character tolerance and prime threshold work for all actual pattern trees and bulk lengths. No local cancellation bound is an assumption here: it is derived from the quartet theorem.

   theorem exists_movingPatternPrimeGain (ψ : 𝓢(ℝ, ℂ)) (n r₀ : ℕ)
       (A lo hi B D F gain : ℝ) (hA : 0 ≤ A) (hhi : lo ≤ hi) :
       ∃ ε δ : ℝ, 0 < ε ∧ ε ≤ 1 ∧ 0 < δ ∧ ∃ cutoff : ℕ, 3 ≤ cutoff ∧
         ∀ (m : ℕ), 1 ≤ m → ∀ (Bidx Cidx : Type) (N : ℕ)
           (e : Fin (N + 1) ≃ Bidx ⊕ Cidx) (base : Fin (N + 1) → ℕ)
           (t : Bool → FrequencyTree ℤ (n + 2))
           (small : Bool → TreeLeafTuple (List Bidx) (n + 2))
           (pattern : Bool × MovingSampleIndex (n + 2) → Cidx)
           (p : Fin m → ℕ) [∀ i, Fact (p i).Prime],
         (∀ i, cutoff ≤ p i) →
         (∀ i b, ∀ s ∈ allFrequencyList (n + 2) (t b), s ≠ 0 ∧ s.natAbs < p i) →
         (∀ i b, ∀ j ∈ flattenMovingSlots (n + 2) (small b),
   …

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