OAI/NumberTheory/CubicMoment/Estimates/SparseStoppedSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The sparse support belongs to the actual late stopped coefficient. Nonvanishing selects a literal product fibre, and the failed first stage constructs its large small-prime divisor.

  1. theorem OAI.CubicFirstMoment.stoppedBeta_late_mem_sparse line 16
  2. theorem OAI.CubicFirstMoment.sparse_stopped_beta_energy line 47