Suitable Window Conditions for Gaussian Functions

This file establishes that normalized Gaussian windows satisfy the suitable_window conditions required for the Zak frame theory.

Main Results

• suitable_window_of_normalized_gaussian: Shows that normalized Gaussian windows satisfy all requirements for suitable_window predicate

structure Frourio.Analysis.suitable_window (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Prop

Suitable window condition for frame theory

• normalized : ‖f‖ = 1
• time_localized : ∃ C > 0, ∀ᵐ (t : ℝ), ‖↑↑f t‖ ≤ C * (1 + |t|) ^ (-2)

theorem Frourio.Analysis.suitable_window_of_normalized_gaussian (δ : ℝ) (hδ : 0 < δ) : ∃ (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), ‖w‖ = 1 ∧ suitable_window w

Main theorem: Normalized Gaussian windows are suitable windows