OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternSeparatedConditions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Supplying the giant arithmetic conditions from the original prime priors

  1. theorem OAI.Ostmann.movingPattern_separated_giant_conditions line 18

    Source documentation

    All assignment-dependent conditions of the giant comparison follow from actual prime ranges, original-prior support, and the prescribed conductor prime deletion. No arithmetic comparison is assumed in this statement.

    theorem movingPattern_separated_giant_conditions (input : PublishedProgressionInput)
    (n r₀ k : ℕ) (Cfreq : ℝ) (hCfreq : 0 ≤ Cfreq) :
    ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
…

    Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.spectatorBulkCount