OAI/NumberTheory/TwoPoint/Bounds/PaddingLogMoment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The same fixed-modulus input bounds the logarithmic moment of the reciprocal padding-divisor law, as needed for mass retained in bins.

  1. lemma OAI.TwoPointCorrelations.modFivePrimeBand_log_mass line 14
  2. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.padding_log_mass line 25
  3. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_reciprocal_padding_log_mean line 63