OAI/NumberTheory/Ostmann/Characters/SparseTailMassBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sparse balanced tail spectra have small harmonic mass

This is the contradiction step of Proposition 5.1, using the original nonnegative sparse weight and the actual positive and reflected summand tails.

  1. theorem OAI.Ostmann.EventuallyPrimeSumset.sparse_tail_mass_bound line 17