OAI/NumberTheory/Ostmann/Construction/IntegerIntervalDistribution.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.integer_interval_residue_error line 16
2. theorem OAI.Ostmann.real_interval_residue_error line 46
3. theorem OAI.Ostmann.integer_log_interval_residue_error line 70

   Source documentation

   The logarithmic integer coordinate has main density exp(t)/q. Multiplication by its original normalization costs exactly the same factor on the uniform absolute error.

   theorem integer_log_interval_residue_error (q a : ℕ) (hq : 0 < q)
       (s t G : ℝ) (hst : s ≤ t) :
       |Real.exp (-G) *
         (((Finset.Ioc ⌊Real.exp s⌋₊ ⌊Real.exp t⌋₊).filter fun n => Nat.ModEq q n a).card : ℝ) -
         Real.exp (-G) * ((Real.exp t - Real.exp s) / q)| ≤ 2 * Real.exp (-G) := by
   …

4. def OAI.Ostmann.integerLogDensity line 80
5. theorem OAI.Ostmann.integerLogDensity_integral line 83
6. theorem OAI.Ostmann.integer_log_density_error line 100

   Source documentation

   The external integer coordinate has the claimed real log density, with an explicit absolute error uniform in every residue class.

   theorem integer_log_density_error (q a : ℕ) (hq : 0 < q)
       (s t G : ℝ) (hst : s ≤ t) :
       |Real.exp (-G) *
         (((Finset.Ioc ⌊Real.exp s⌋₊ ⌊Real.exp t⌋₊).filter fun n => Nat.ModEq q n a).card : ℝ) -
         ∫ y in Set.Ioc s t, integerLogDensity q G y| ≤ 2 * Real.exp (-G) := by
   …

   Mentions: OAI.Ostmann.integerLogDensity