OAI/NumberTheory/Ostmann/Construction/RepeatRemovalPointwise.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A moment-sensitive bound for deleting repeated indices

A square-root shift gives a convenient alternative to the cycle expansion: |D_k-S^k| ≤ (|S|+sqrt(k*J))^k-|S|^k. After normalization and Hölder, this has the same vanishing relative error at the manuscript's scales.

  1. theorem OAI.Ostmann.recurrence_power_error line 17
  2. theorem OAI.Ostmann.ternary_distinct_product_error line 62
  3. theorem OAI.Ostmann.normalized_ternary_distinct_product_error line 94