OAI/NumberTheory/CubicMoment/Decomposition/StoppedRoughSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Prime-factor roughness of the actual stopped coefficient. The selected factor is rough because its bins precede the stopping bin; the distinguished factor is rough because its coefficient vanishes at small primes.

  1. lemma OAI.CubicFirstMoment.geometricBinLower_antitone line 16
  2. theorem OAI.CubicFirstMoment.stoppingSideTest_prime_roughness line 21
  3. theorem OAI.CubicFirstMoment.stoppedBeta_prime_roughness line 32
  4. theorem OAI.CubicFirstMoment.stoppedBeta_early_prime_roughness line 65