MovingPatternOriginalPrimeNorm.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The published giant comparison under the unchanged original prior

theorem OAI.Ostmann.PublishedProgressionInput.movingPattern_original_prime_norm line 17

Source documentation

Apply the published progression input before the signed arithmetic norm. The internal modulus is the actual image of the sampled internal primes. Its CRT coprimality and all compensation data are derived here.

theorem PublishedProgressionInput.movingPattern_original_prime_norm
    (input : PublishedProgressionInput) (n : ℕ) (Cbudget : ℝ) (d : ℕ) :
    ∀ᶠ L : ℝ in atTop,
      ∀ (B C I : Type) [Fintype B] [Fintype C] [Fintype I] (N m : ℕ)
        (e : Fin (N + 1) ≃ B ⊕ C) (tierB : B → ℕ) (tierC : C → ℕ)
        (t : Bool → FrequencyTree ℤ n) (small : TreeLeafTuple (List B) n)
        (slot : (TreeLeafIndex n × Fin m) ↪ B) (pattern : Bool × MovingSampleIndex n → C)
        (_rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c})
        (primes : Finset ℕ) (hprimes : ∀ p ∈ primes, p.Prime)
        (μ : ℕ → primes → ℝ) (ν : B → primes → ℝ)
        (p : I → ℕ) [∀ i, Fact (p i).Prime] (_hinjp : Function.Injective p)
        (g : ∀ i, ZMod (p i) → ℂ) (Dq : ∀ i, (ZMod (p i))ˣ)
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.primes