OAI/NumberTheory/CubicMoment/Estimates/MellinWeightBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The height weight in the truncated Mellin integral

The interval transform has the expected 1/(1+|ξ|) bound, including at frequency zero. The cutoff and the scaling phase have norm at most one.

  1. lemma OAI.CubicFirstMoment.norm_dyadicFourierMultiplier_le_log line 17
  2. lemma OAI.CubicFirstMoment.norm_dyadicFourierMultiplier_nonzero line 28
  3. lemma OAI.CubicFirstMoment.norm_dyadicFourierMultiplier_le line 41
  4. lemma OAI.CubicFirstMoment.norm_frequencyCutoff_le_one line 56
  5. theorem OAI.CubicFirstMoment.norm_truncatedMellinWeight_le line 62

    Source documentation

    The common weight in the actual arithmetic integral has exactly the height decay needed for the later dyadic-height estimates.

    theorem norm_truncatedMellinWeight_le (X T ξ : ℝ) :
    ‖truncatedMellinWeight X T ξ‖ ≤ 2/(1+|ξ|) := by
…

    Mentions: OAI.CubicFirstMoment.truncatedMellinWeight