OAI/NumberTheory/CubicMoment/Estimates/PrimeMassIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating the exact common-divisor decomposition. The large-divisor majorant may be uniform in height; the empty row retains its full Mellin integral.

  1. theorem OAI.CubicFirstMoment.fullPrime_coprime_mass_integral_le line 15