OAI/NumberTheory/Ostmann/Arithmetic/BulkResidueCoprime.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulkResidueModuli_pairwise line 11
2. theorem OAI.Ostmann.bulkResidueModuli_pairwise_of_lt line 25
3. theorem OAI.Ostmann.bulkResidueModulus_positive line 33
4. theorem OAI.Ostmann.frequency_modulus_lt_spectators line 43

   Source documentation

   The split-prime lower range eventually exceeds every fixed-depth frequency modulus; this supplies the cross-block CRT coprimality.

   theorem frequency_modulus_lt_spectators (F K a : ℝ)
       (hF : 0 ≤ F) (hK : 0 ≤ K) (ha : 0 < a) :
       ∀ᶠ L : ℝ in atTop, ∀ (m r : ℕ) (p : Fin m → ℕ),
         (m : ℝ) ≤ K * L → (r : ℝ) ≤ Real.exp (F * m) →
         (∀ i, Real.exp (Real.exp (a * L)) ≤ (p i : ℝ)) → ∀ i, r < p i := by
   …