OAI/NumberTheory/Ostmann/Arithmetic/MovingSampleModulusRange.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The full modulus of the actual sampled histories at the giant scale

  1. theorem OAI.Ostmann.list_nat_prod_exp_bound line 12
  2. theorem OAI.Ostmann.movingSample_pair_modulus_bound line 25
  3. theorem OAI.Ostmann.sampled_modulus_exponent_bound line 71
  4. theorem OAI.Ostmann.movingSample_pair_modulus_giant_range line 118

    Source documentation

    The cutoff is uniform in the actual histories and all sampled prime values. It permits the full .011 internal range and the original bulk size.

    theorem movingSample_pair_modulus_giant_range (n r₀ k : ℕ) (A : ℝ) (hA : 0 ≤ A) :
    ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
…

    Mentions: OAI.Ostmann.spectatorBulkCount