OAI/NumberTheory/Ostmann/Arithmetic/MovingModulusAssembly.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

All CRT size conditions for the concrete pair frequency modulus

  1. theorem OAI.Ostmann.moving_pair_modulus_range line 14

    Source documentation

    A single eventual cutoff works for every actual history, frequency choice and spectator list in the prescribed ranges.

    theorem moving_pair_modulus_range (n k : ℕ) (A a : ℝ) (hA : 0 ≤ A) (ha : 0 < a) :
    ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
…

    Mentions: OAI.Ostmann.spectatorBulkCount