OAI/NumberTheory/CubicMoment/Estimates/ConductorNeighborhoods.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Uniform exceptional moments hold throughout a fixed open neighborhood of each exceptional conductor exponent. The neighborhoods are constructed by contradiction from actual short-factor sequences, not assumed as analytic inputs.

  1. lemma OAI.CubicFirstMoment.HasPowerExponent.of_shrinking_window line 15
  2. theorem OAI.CubicFirstMoment.neighborhood_saving_of_no_countersequence line 36
  3. lemma OAI.CubicFirstMoment.neighborhood_scale_tendsto line 53
  4. lemma OAI.CubicFirstMoment.neighborhood_lower_exponent line 58
  5. lemma OAI.CubicFirstMoment.neighborhood_lower_ge_one line 65
  6. structure OAI.CubicFirstMoment.ConductorMomentInstance line 73
  7. def OAI.CubicFirstMoment.neighborhoodFamily line 76
  8. def OAI.CubicFirstMoment.cubicNeighborhoodAdmissible line 88
  9. theorem OAI.CubicFirstMoment.cubic_short_neighborhood_power line 99
  10. def OAI.CubicFirstMoment.mixedNeighborhoodAdmissible line 128
  11. theorem OAI.CubicFirstMoment.mixed_short_neighborhood_power line 140