OAI/NumberTheory/CubicMoment/Estimates/LogarithmicPhase.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Logarithmically bounded height twists preserve the smooth weight family used by the low-height Type-I theorem.

  1. def OAI.CubicFirstMoment.linearHeightPhase line 12
  2. lemma OAI.CubicFirstMoment.linearHeightPhase_derivative line 14
  3. lemma OAI.CubicFirstMoment.linearHeightPhase_iteratedDeriv line 22
  4. lemma OAI.CubicFirstMoment.linearHeightPhase_derivative_norm line 34
  5. abbrev OAI.CubicFirstMoment.logarithmicPhaseIndex line 40
  6. def OAI.CubicFirstMoment.logarithmicPhaseWeight line 43
  7. def OAI.CubicFirstMoment.LogarithmicWeightFamily.phase line 47