OAI/NumberTheory/JointDickman/Probability/GeometricHistogramErrors.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The summed fine-histogram and residue losses in geometric boxes

  1. def OAI.JointDickman.geometricHistogramWindow line 12
  2. theorem OAI.JointDickman.geometric_histogram_error_sum line 16