MellinPacketScale.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Normalized logarithmic windows at a prescribed scale

def OAI.JointDickman.normalizedSchwartzScale line 11
Source documentation
The normalized dilation w(v/δ)/δ, for a positive window scale.
```
noncomputable def normalizedSchwartzScale (w : 𝓢(ℝ, ℂ)) (δ : ℝ) (hδ : 0 < δ) :
    𝓢(ℝ, ℂ) :=
…
```
theorem OAI.JointDickman.normalizedSchwartzScale_apply line 16

theorem OAI.JointDickman.normalizedSchwartzScale_fourier line 25

Source documentation

The normalization removes the scale factor in the Fourier transform.

theorem normalizedSchwartzScale_fourier (w : 𝓢(ℝ, ℂ)) {δ : ℝ} (hδ : 0 < δ) (ξ : ℝ) :
    (𝓕 (normalizedSchwartzScale w δ hδ) : 𝓢(ℝ, ℂ)) ξ =
      (𝓕 w : 𝓢(ℝ, ℂ)) (δ * ξ) := by
…

Mentions: OAI.JointDickman.normalizedSchwartzScale

theorem OAI.JointDickman.scaled_mellinPacket_energy line 56

Source documentation

The exact energy identity at the short logarithmic scale δ.

theorem scaled_mellinPacket_energy (S : Finset ℕ) (a : ℕ → ℂ)
    (w : 𝓢(ℝ, ℂ)) {δ : ℝ} (hδ : 0 < δ) :
    (∫ v : ℝ, ‖mellinPacket S a (normalizedSchwartzScale w δ hδ) v‖ ^ 2) =
      ∫ ξ : ℝ, ‖(𝓕 w : 𝓢(ℝ, ℂ)) (δ * ξ)‖ ^ 2 *
        ‖mellinPolynomial S a ξ‖ ^ 2 := by
…

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