OAI/NumberTheory/CubicMoment/Estimates/PoissonProfileBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A quantitative profile budget is constructed from finitely many Schwartz seminorms. It records only the two analytic costs used by the Poisson argument; it is not an additional published input.

  1. def OAI.CubicFirstMoment.poissonProfileLogWidth line 15
  2. lemma OAI.CubicFirstMoment.poissonProfileLogWidth_pos line 17
  3. structure OAI.CubicFirstMoment.PoissonProfileBudget line 22
  4. lemma OAI.CubicFirstMoment.PoissonProfileBudget.mellin_le line 36
  5. lemma OAI.CubicFirstMoment.PoissonProfileBudget.radial_le line 44
  6. lemma OAI.CubicFirstMoment.radialDualProfile_seminorm_control line 49
  7. theorem OAI.CubicFirstMoment.exists_poissonProfileBudget_control line 72

    Source documentation

    Every smooth compact profile has a budget bounded by the same finite set of derivatives, chosen before the profile.

    theorem exists_poissonProfileBudget_control :
    ∃ (I : Finset (ℕ × ℕ)) (C : ℝ), 0 < C ∧
      ∀ (V : ℝ → ℂ) (hV : HasCompactSupport V) (hV' : ContDiff ℝ ∞ V),
      ∃ P : PoissonProfileBudget, P.V = V ∧
        P.cost ≤ 1+C*(I.sup (fun m => SchwartzMap.seminorm ℝ m.1 m.2))
          (normProfileFourierSchwartz V hV hV') := by
…

    Mentions: OAI.CubicFirstMoment.PoissonProfileBudget, OAI.CubicFirstMoment.normProfileFourierSchwartz