OAI/NumberTheory/CubicMoment/Estimates/LogarithmicPrimeInput.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform rescaled prime sums for the given logarithmic weight family. Every variation cost is derived from the family's actual derivative bounds.

  1. theorem OAI.CubicFirstMoment.logarithmic_scaled_cubic_prime_bound line 11