MellinPackets.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Smoothed logarithmic windows and their Dirichlet energy

A finite sum of translates of a Schwartz window is itself Schwartz. Its Fourier transform factors into the window transform and the actual finite Dirichlet polynomial. Plancherel therefore identifies the two energies without a truncation or an arithmetic hypothesis.

def OAI.JointDickman.mellinPolynomial line 17
Source documentation
The reciprocal-weighted Dirichlet polynomial in Fourier normalization.
```
noncomputable def mellinPolynomial (S : Finset ℕ) (a : ℕ → ℂ) (ξ : ℝ) : ℂ :=
…
```
def OAI.JointDickman.mellinPacket line 21
Source documentation
A smoothed logarithmic window, retaining the literal coefficients.
```
noncomputable def mellinPacket (S : Finset ℕ) (a : ℕ → ℂ) (w : 𝓢(ℝ, ℂ)) :
    𝓢(ℝ, ℂ) :=
…
```
theorem OAI.JointDickman.mellinPacket_apply line 25
theorem OAI.JointDickman.fourier_schwartz_translate line 30
theorem OAI.JointDickman.mellinPacket_fourier line 53

theorem OAI.JointDickman.mellinPacket_energy line 65

Source documentation

Exact Plancherel transfer for the smoothed logarithmic window.

theorem mellinPacket_energy (S : Finset ℕ) (a : ℕ → ℂ) (w : 𝓢(ℝ, ℂ)) :
    (∫ v : ℝ, ‖mellinPacket S a w v‖ ^ 2) =
      ∫ ξ : ℝ, ‖(𝓕 w : 𝓢(ℝ, ℂ)) ξ‖ ^ 2 * ‖mellinPolynomial S a ξ‖ ^ 2 := by
…

Mentions: OAI.JointDickman.mellinPacket, OAI.JointDickman.mellinPolynomial