OAI/NumberTheory/CubicMoment/Estimates/TwoRangeMellinTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A Mellin tail with a proved mean up to a power cutoff and a coarse mean afterwards. Rapid decay suppresses the coarse part by the cutoff power; the good mean is not silently extended to every height.

  1. theorem OAI.CubicFirstMoment.weighted_positive_mellin_tail_two_ranges line 12