OAI/NumberTheory/CubicMoment/Estimates/MellinWeights.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Smooth weights and Mellin twists

The derivative cost below explains why the unweighted published Hecke estimate continues to give any prescribed logarithmic saving after a fixed-logarithmic-height norm twist. It is used with weighted_cubic_prime_bound.

  1. def OAI.CubicFirstMoment.mellinPhase line 18
  2. theorem OAI.CubicFirstMoment.mellinPhase_norm line 20
  3. theorem OAI.CubicFirstMoment.normTwist_eq_mellinPhase line 23
  4. theorem OAI.CubicFirstMoment.hasDerivAt_mellinPhase line 26
  5. theorem OAI.CubicFirstMoment.norm_deriv_mellinPhase line 35
  6. theorem OAI.CubicFirstMoment.hasDerivAt_weighted_mellinPhase line 41
  7. theorem OAI.CubicFirstMoment.norm_deriv_weighted_mellinPhase line 49

    Source documentation

    The derivative loss is linear in the Mellin height and inversely proportional to the norm variable.

    theorem norm_deriv_weighted_mellinPhase {w : ℝ → ℂ} {w' : ℂ} {x : ℝ}
    (hw : HasDerivAt w w' x) (u : ℝ) (hx : 0 < x) :
    ‖deriv (fun t => w t * mellinPhase u t) x‖ ≤
      ‖w'‖ + ‖w x‖ * (|u| / x) := by
…

    Mentions: OAI.CubicFirstMoment.mellinPhase