OAI/NumberTheory/Ostmann/Arithmetic/WeightedIntegerIntervals.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.finite_weight_freeze line 13
2. def OAI.Ostmann.integerResidueAtom line 31
3. def OAI.Ostmann.integerLogCellMass line 34
4. def OAI.Ostmann.weightedIntegerLogInterval line 37
5. theorem OAI.Ostmann.integerLogCellMass_eq line 40
6. theorem OAI.Ostmann.integerLogCellMass_error line 48
7. theorem OAI.Ostmann.weightedIntegerLogInterval_freeze line 55
8. theorem OAI.Ostmann.integerLogDensity_abs_le line 66
9. theorem OAI.Ostmann.integerLogDensity_integral_abs_le line 74
10. theorem OAI.Ostmann.integerLogDensity_integral_freeze line 86
11. theorem OAI.Ostmann.weighted_integer_log_density_error line 121

    Source documentation

    The integer analogue of the weighted prime progression estimate.

    theorem weighted_integer_log_density_error (q a : ℕ) (hq : 0 < q) (s t G : ℝ)
        (hst : s ≤ t) (hshort : t ≤ s + 1)
        (w : ℝ → ℝ) (hwc : ContinuousOn w (Set.Icc s t)) (w₀ η : ℝ) (hη : 0 ≤ η)
        (hw : ∀ y ∈ Set.Ioc s t, |w y - w₀| ≤ η) :
        |weightedIntegerLogInterval q a s t G w -
          ∫ y in Set.Ioc s t, w y * integerLogDensity q G y| ≤
          (|w₀| + η) * (2 * Real.exp (-G)) + 2 * η * Real.exp (t - G) := by
    …

    Mentions: OAI.Ostmann.weightedIntegerLogInterval, OAI.Ostmann.integerLogDensity