Step 5: STMT Gaussian windows and width control (design-level).

We introduce a Gaussian window and record decay/overlap bounds as Prop-level signatures to be supplied in later phases. This keeps downstream APIs stable without committing to full analytic proofs here.

noncomputable def Frourio.gaussianFun (α t : ℝ) : ℝ

Continuous Gaussian profile (real-valued).

Equations

• Frourio.gaussianFun α t = Real.exp (-Real.pi * α * t ^ 2)

noncomputable def Frourio.gaussian : ℝ → ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

L² window (placeholder): the actual Lp element will be provided when we install the precise isometry context.

Equations

• Frourio.gaussian x✝ = 0

def Frourio.gaussian_decay (α : ℝ) : Prop

Decay statement for the Gaussian profile (signature). Intended: ‖gaussianFun α t‖ ≤ exp(−c α t²) with a suitable constant c>0.

Equations

• Frourio.gaussian_decay α = ∃ (c : ℝ), 0 < c ∧ ∀ (t : ℝ), |Frourio.gaussianFun α t| ≤ Real.exp (-c * α * t ^ 2)

def Frourio.overlap_bound (α Δτ : ℝ) : Prop

Overlap bound between shifted Gaussian peaks at lattice spacing Δτ (signature). Intended: for k ≠ 0, ‖g( k Δτ )‖ ≲ exp(−c α (Δτ)² k²) for some c>0.

Equations

• Frourio.overlap_bound α Δτ = ∃ (c : ℝ), 0 < c ∧ ∀ (k : ℤ), k ≠ 0 → |Frourio.gaussianFun α (↑k * Δτ)| ≤ Real.exp (-c * α * Δτ ^ 2 * ↑k ^ 2)

theorem Frourio.gaussian_decay_of_nonneg {α : ℝ} (hα : 0 ≤ α) : gaussian_decay α

Concrete decay bound holds for any nonnegative α with an explicit constant.