PeriodicNonnegative.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Periodic interval counts with a sparse error

For a nonnegative periodic weight, the error is bounded by its total mass in one period. This retains the number of allowed residues in sieve errors.

theorem OAI.JointDickman.real_periodic_sum_div_mod line 15

theorem OAI.JointDickman.nonnegative_periodic_prefix_error line 22

Source documentation

A prefix costs at most the mass of one complete period.

theorem nonnegative_periodic_prefix_error {q : ℕ} (hq : 0 < q)
    (f : ZMod q → ℝ) (hf : ∀ a, 0 ≤ f a) (N : ℕ) :
    |(∑ n ∈ range N, f n) - (N : ℝ) / q * ∑ n ∈ range q, f n| ≤
      ∑ n ∈ range q, f n := by
…

theorem OAI.JointDickman.nonnegative_periodic_interval_error line 49

Source documentation

Two prefix errors give the interval error, uniformly in its location.

theorem nonnegative_periodic_interval_error {q : ℕ} (hq : 0 < q)
    (f : ZMod q → ℝ) (hf : ∀ a, 0 ≤ f a) {a b : ℕ} (hab : a ≤ b) :
    |(∑ n ∈ Ico a b, f n) - ((b : ℝ) - a) / q * ∑ n ∈ range q, f n| ≤
      2 * ∑ n ∈ range q, f n := by
…