MellinWeightedEnergy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

From interval Dirichlet energies to a Schwartz weighted energy

theorem OAI.JointDickman.schwartz_weighted_energy_bound line 13

Source documentation

The constant depends only on the fixed Schwartz window. A bound linear in the frequency cutoff gives a finite weighted energy, without a logarithmic loss from the number of frequency intervals.

theorem schwartz_weighted_energy_bound (w : 𝓢(ℝ, ℂ)) :
    ∃ C : ℝ, 0 < C ∧ ∀ (F : ℝ → ℂ), Continuous F → ∀ A B : ℝ,
      0 ≤ A → 0 ≤ B →
      Integrable (fun t : ℝ => ‖w t‖ ^ 2 * ‖F t‖ ^ 2) →
      (∀ T : ℝ, 1 ≤ T → (∫ t in -T..T, ‖F t‖ ^ 2) ≤ A + B * T) →
      (∫ t : ℝ, ‖w t‖ ^ 2 * ‖F t‖ ^ 2) ≤ C * (A + B) := by
…