MellinAngularEnergy.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Angular-frequency normalization for the published Dirichlet estimates

def OAI.JointDickman.angularMellinPolynomial line 11
Source documentation
The convention used in the Dirichlet-polynomial mean-square estimates.
```
noncomputable def angularMellinPolynomial (S : Finset ℕ) (a : ℕ → ℂ) (t : ℝ) : ℂ :=
…
```
theorem OAI.JointDickman.mellinPolynomial_eq_angular line 14

theorem OAI.JointDickman.mellinPolynomial_energy_of_angular line 27

Source documentation

Changing from angular to Fourier frequency preserves a linear spectral bound, since the constant term is reduced by the factor 2*pi.

theorem mellinPolynomial_energy_of_angular (S : Finset ℕ) (a : ℕ → ℂ)
    {A B : ℝ} (hA : 0 ≤ A) (_hB : 0 ≤ B)
    (hbound : ∀ T : ℝ, 1 ≤ T →
      (∫ t in -T..T, ‖angularMellinPolynomial S a t‖ ^ 2) ≤ A + B * T) :
    ∀ T : ℝ, 1 ≤ T →
      (∫ t in -T..T, ‖mellinPolynomial S a t‖ ^ 2) ≤ A + B * T := by
…

Mentions: OAI.JointDickman.angularMellinPolynomial, OAI.JointDickman.mellinPolynomial

theorem OAI.JointDickman.angularMellinPolynomial_consecutive line 46

theorem OAI.JointDickman.mellinPolynomial_two_dyadic_energy line 55

Source documentation

Only two dyadic spectral bounds are needed for the entire coefficient range used by the short-window transfer.

theorem mellinPolynomial_two_dyadic_energy (a : ℕ → ℂ) (N : ℕ)
    {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B)
    (hfirst : ∀ T : ℝ, 1 ≤ T →
      (∫ t in -T..T, ‖angularMellinPolynomial (Ioc N (2 * N)) a t‖ ^ 2) ≤ A + B * T)
    (hsecond : ∀ T : ℝ, 1 ≤ T →
      (∫ t in -T..T, ‖angularMellinPolynomial (Ioc (2 * N) (4 * N)) a t‖ ^ 2) ≤ A + B * T) :
    ∀ T : ℝ, 1 ≤ T →
      (∫ t in -T..T, ‖mellinPolynomial (Ioc N (4 * N)) a t‖ ^ 2) ≤ 4 * A + (4 * B) * T := by
…

Mentions: OAI.JointDickman.angularMellinPolynomial, OAI.JointDickman.mellinPolynomial