OAI/NumberTheory/TwoPoint/Bounds/WeightedThetaError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The bounded-error form of partial summation needed for the padding oscillation. The constants retain the uniform derivative bounds explicitly.

  1. theorem OAI.TwoPointCorrelations.weighted_theta_error line 13

    Also declared: OAI/NumberTheory/TwoPointCorrelations/WeightedThetaError.lean:13 (same declaration text).