OAI/NumberTheory/Ostmann/Characters/SchwartzWeightVariation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Concrete variation bounds for the quadratic Schwartz weight

  1. theorem OAI.Ostmann.schwartz_norm_sub_le line 13
  2. def OAI.Ostmann.quadraticSchwartzWeight line 23

    Source documentation

    Pullback along the squaring map is still a Schwartz function on the line. This is the weight appearing after writing a frequency as s*v*w^2.

    noncomputable def quadraticSchwartzWeight (Φ : 𝓢(ℝ, ℂ)) : 𝓢(ℝ, ℂ) :=
…
  3. theorem OAI.Ostmann.quadraticSchwartzWeight_apply line 29
  4. theorem OAI.Ostmann.schwartz_rescaled_variation line 32
  5. theorem OAI.Ostmann.quadratic_schwartz_rescaled_variation line 41