PeriodicRectangle.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Sparse errors for a periodic nonnegative weight in a rectangle

theorem OAI.JointDickman.nonnegative_periodic_rectangle_error line 13

Source documentation

The rectangle error retains the mass in a single residue square, which is essential when only a few residue lines are allowed.

theorem nonnegative_periodic_rectangle_error {q : ℕ} (hq : 0 < q)
    (F : ZMod q → ZMod q → ℝ) (hF : ∀ r s, 0 ≤ F r s)
    {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d) :
    |(∑ m ∈ Ico a b, ∑ n ∈ Ico c d, F m n) -
        (((b : ℝ) - a) * ((d : ℝ) - c) / (q : ℝ) ^ 2) *
          ∑ r ∈ range q, ∑ s ∈ range q, F r s| ≤
      2 * ((((b : ℝ) - a) + ((d : ℝ) - c)) / q + 2) *
        ∑ r ∈ range q, ∑ s ∈ range q, F r s := by
…