OAI/NumberTheory/CubicMoment/Estimates/ShrinkingProfile.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial seminorm costs for affine shrinking of a fixed cutoff.

  1. lemma OAI.CubicFirstMoment.iteratedFDeriv_comp_sub_real line 10
  2. def OAI.CubicFirstMoment.affineSchwartzProfile line 18
  3. lemma OAI.CubicFirstMoment.affineSchwartzProfile_apply line 22
  4. lemma OAI.CubicFirstMoment.affineSchwartzProfile_deriv_norm line 25
  5. theorem OAI.CubicFirstMoment.affineSchwartzProfile_seminorm line 35
  6. theorem OAI.CubicFirstMoment.affineSchwartzProfile_finite_cost line 64

    Source documentation

    Every fixed finite family of seminorms has a polynomial shrinking cost.

    theorem affineSchwartzProfile_finite_cost (f : 𝓢(ℝ,ℂ)) (I : Finset (ℕ × ℕ)) :
    ∃ (d : ℕ) (K : ℝ), 0 < K ∧ ∀ (J c : ℝ) (hJ : 1 ≤ J), |c| ≤ 2 →
      (I.sup (fun m => SchwartzMap.seminorm ℝ m.1 m.2))
        (affineSchwartzProfile f J c (by linarith)) ≤ K*J^d := by
…

    Mentions: OAI.CubicFirstMoment.affineSchwartzProfile