OAI/NumberTheory/JointDickman/Analysis/MellinSpectralWeights.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summable unit-interval bounds for a Schwartz spectral weight

  1. theorem OAI.JointDickman.schwartz_cell_norm_sq_bound line 12

    Source documentation

    A fixed Schwartz window has a summable quadratic Fourier majorant on unit intervals. This will weight the local Dirichlet mean-square estimates.

    theorem schwartz_cell_norm_sq_bound (w : š“¢(ā„, ā„‚)) :
    āˆƒ C : ā„, 0 < C āˆ§ āˆ€ (n : ā„¤) (u : ā„), (n : ā„) ā‰¤ u ā†’ u ā‰¤ n + 1 ā†’
      ā€–w uā€– ^ 2 ā‰¤ C / (1 + |(n : ā„)|) ^ 4 := by
ā€¦
  2. lemma OAI.JointDickman.summable_integer_window_weights line 42