OAI/NumberTheory/CubicMoment/Estimates/LowCoreHeightMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual finite small-core frequency set at arbitrary height. This mean-value bound complements the low-height Kummer prime estimate.

  1. theorem OAI.CubicFirstMoment.low_core_height_mean line 14