MellinEnergyTransfer.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Scaled transfer of Dirichlet mean-square estimates to short windows

theorem OAI.JointDickman.continuous_mellinPolynomial line 10

theorem OAI.JointDickman.mellinPacket_energy_of_spectral_bound line 19

Source documentation

A Dirichlet energy bound A+B*T gives the expected short-window cost A+B/δ, with a constant depending only on the smoothing profile.

theorem mellinPacket_energy_of_spectral_bound (w : 𝓢(ℝ, ℂ)) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : Finset ℕ) (a : ℕ → ℂ)
      (δ : ℝ) (hδ : 0 < δ), δ ≤ 1 → ∀ A B : ℝ, 0 ≤ A → 0 ≤ B →
      (∀ T : ℝ, 1 ≤ T →
        (∫ t in -T..T, ‖mellinPolynomial S a t‖ ^ 2) ≤ A + B * T) →
      (∫ v : ℝ, ‖mellinPacket S a (normalizedSchwartzScale w δ hδ) v‖ ^ 2) ≤
        C * (A + B / δ) := by
…

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