Step 3: Discretization of the quadratic form via Zak coefficients (design-level).

We define a discrete quadratic form Qdisc indexed by the lattice steps and provide a bounds predicate Q_bounds that will relate it to the continuous quadratic form Qℝ. At this phase, Qdisc is a placeholder and the bounds are recorded as a Prop to be supplied in later phases using frame inequalities and boundedness assumptions on K.

noncomputable def Frourio.Qdisc (_K : ℝ → ℝ) (_w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (_Δτ _Δξ : ℝ) (_g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ℝ

Discrete quadratic form built from K and Zak coefficients (placeholder 0).

Equations

• Frourio.Qdisc _K _w _Δτ _Δξ _g = 0

def Frourio.Q_bounds (K : ℝ → ℝ) (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (Δτ Δξ : ℝ) : Prop

Bounds predicate connecting the continuous and discrete quadratic forms.

Equations

• One or more equations did not get rendered due to their size.

Phase 1.1: Zak–Mellin frame building blocks (function-level forms + L² stubs).

We introduce the intended time-shift and modulation operators at the function level and keep the Lp-level maps as identity placeholders to preserve the API while avoiding heavy measure-theoretic proofs in this phase.

noncomputable def Frourio.timeShiftFun (τ : ℝ) (g : ℝ → ℂ) : ℝ → ℂ

Function-level time shift: (timeShiftFun τ g) t = g (t - τ).

Equations

• Frourio.timeShiftFun τ g t = g (t - τ)

noncomputable def Frourio.modFun (ξ : ℝ) (g : ℝ → ℂ) : ℝ → ℂ

Function-level modulation: (modFun ξ g) t = exp(i ξ t) · g t.

Equations

• Frourio.modFun ξ g t = Complex.exp (Complex.I * ↑ξ * ↑t) * g t

Step 1: translation map and basic measurability/measure-preserving skeleton. These will support the manual lifting to Lp in subsequent steps.

def Frourio.translationMap (τ : ℝ) : ℝ → ℝ

Equations

• Frourio.translationMap τ t = t - τ

theorem Frourio.measurable_translation (τ : ℝ) : Measurable (translationMap τ)

theorem Frourio.measurableEmbedding_translation (τ : ℝ) : MeasurableEmbedding (translationMap τ)

theorem Frourio.translation_measurePreserving (τ : ℝ) : MeasureTheory.MeasurePreserving (translationMap τ) MeasureTheory.volume MeasureTheory.volume

theorem Frourio.ae_comp_translation_iff {p : ℝ → Prop} (hp : MeasurableSet {y : ℝ | p y}) (τ : ℝ) : (∀ᵐ (y : ℝ), p y) ↔ ∀ᵐ (x : ℝ), p (translationMap τ x)

Helper lemmas for transporting a.e. equalities along translations

theorem Frourio.ae_comp_translation_of_ae_eq {u v : ℝ → ℂ} (τ : ℝ) (hu : MeasureTheory.AEStronglyMeasurable u MeasureTheory.volume) (hv : MeasureTheory.AEStronglyMeasurable v MeasureTheory.volume) (h : u =ᵐ[MeasureTheory.volume] v) : (fun (x : ℝ) => u (x - τ)) =ᵐ[MeasureTheory.volume] fun (x : ℝ) => v (x - τ)

L² time shift as a continuous linear map. At the function level it acts by (timeShift τ g) t = g (t - τ). We use translation_measurePreserving to construct the L² isometry.

theorem Frourio.comp_translation_memLp (τ : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : MeasureTheory.MemLp (fun (t : ℝ) => ↑↑f (t - τ)) 2 MeasureTheory.volume

noncomputable def Frourio.timeShift_linearMap (τ : ℝ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →ₗ[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Equations

• One or more equations did not get rendered due to their size.

theorem Frourio.timeShift_norm_eq (τ : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖(timeShift_linearMap τ) f‖ = ‖f‖

noncomputable def Frourio.timeShift (τ : ℝ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Equations

• Frourio.timeShift τ = (Frourio.timeShift_linearMap τ).mkContinuous 1 ⋯

theorem Frourio.integral_comp_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : ℝ → E) (τ : ℝ) : ∫ (t : ℝ), f (t - τ) = ∫ (t : ℝ), f t

Change of variables formula for integration: ∫f(t-τ) = ∫f(t)

theorem Frourio.eLpNorm_comp_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (p : ENNReal) (τ : ℝ) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) : MeasureTheory.eLpNorm (fun (t : ℝ) => f (t - τ)) p MeasureTheory.volume = MeasureTheory.eLpNorm f p MeasureTheory.volume

L^p norm is preserved under translation

theorem Frourio.L2_norm_comp_sub (f : ℝ → ℂ) (τ : ℝ) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) : MeasureTheory.eLpNorm (fun (t : ℝ) => f (t - τ)) 2 MeasureTheory.volume = MeasureTheory.eLpNorm f 2 MeasureTheory.volume

Special case for L² norm

Modulation on L²: multiplication by the unit-modulus phase t ↦ exp(i ξ t)

theorem Frourio.phase_abs_one (ξ t : ℝ) : ‖Complex.exp (Complex.I * ↑ξ * ↑t)‖ = 1

theorem Frourio.mod_add_ae (ξ : ℝ) (f g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : (fun (t : ℝ) => Complex.exp (Complex.I * ↑ξ * ↑t) * ↑↑(f + g) t) =ᵐ[MeasureTheory.volume] fun (t : ℝ) => Complex.exp (Complex.I * ↑ξ * ↑t) * ↑↑f t + Complex.exp (Complex.I * ↑ξ * ↑t) * ↑↑g t

theorem Frourio.mod_smul_ae (ξ : ℝ) (c : ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : (fun (t : ℝ) => Complex.exp (Complex.I * ↑ξ * ↑t) * ↑↑(c • f) t) =ᵐ[MeasureTheory.volume] fun (t : ℝ) => c • (Complex.exp (Complex.I * ↑ξ * ↑t) * ↑↑f t)

theorem Frourio.mod_memLp (ξ : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : MeasureTheory.MemLp (fun (t : ℝ) => Complex.exp (Complex.I * ↑ξ * ↑t) * ↑↑f t) 2 MeasureTheory.volume

noncomputable def Frourio.mod_linearMap (ξ : ℝ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →ₗ[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Equations

• One or more equations did not get rendered due to their size.

theorem Frourio.mod_norm_eq (ξ : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖(mod_linearMap ξ) f‖ = ‖f‖

noncomputable def Frourio.mod (ξ : ℝ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Equations

• Frourio.mod ξ = (Frourio.mod_linearMap ξ).mkContinuous 1 ⋯

noncomputable def Frourio.ZakCoeff (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (Δτ Δξ : ℝ) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ℤ × ℤ → ℂ

Zak coefficients: inner products against time–frequency shifts of w. ZakCoeff w Δτ Δξ g (n,k) = ⟪ g, mod (kΔξ) (timeShift (nΔτ) w) ⟫

Equations

• Frourio.ZakCoeff w Δτ Δξ g nk = inner ℂ g ((Frourio.mod (↑nk.2 * Δξ)) ((Frourio.timeShift (↑nk.1 * Δτ)) w))

noncomputable def Frourio.FrameEnergy (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (Δτ Δξ : ℝ) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ℝ

Placeholder frame energy built from ZakCoeff (currently 0).

Equations

• Frourio.FrameEnergy w Δτ Δξ g = ∑' (nk : ℤ × ℤ), ‖Frourio.ZakCoeff w Δτ Δξ g nk‖ ^ 2

def Frourio.besselBound (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (Δτ Δξ B : ℝ) : Prop

Bessel 上界: Zak 係数の有限和が B‖g‖² 以下で抑えられる。

Equations

• Frourio.besselBound w Δτ Δξ B = (0 ≤ B ∧ ∀ (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (s : Finset (ℤ × ℤ)), ∑ x ∈ s, ‖Frourio.ZakCoeff w Δτ Δξ g x‖ ^ 2 ≤ B * ‖g‖ ^ 2)

def Frourio.HasBesselBound (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (Δτ Δξ : ℝ) : Prop

存在形式の Bessel 上界。

Equations

• Frourio.HasBesselBound w Δτ Δξ = ∃ (B : ℝ), Frourio.besselBound w Δτ Δξ B

theorem Frourio.frameEnergy_le_of_bessel {w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} {Δτ Δξ B : ℝ} (hb : besselBound w Δτ Δξ B) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : FrameEnergy w Δτ Δξ g ≤ B * ‖g‖ ^ 2

Bessel 上界のもとでフレームエネルギーは有限で、B‖g‖² に抑えられる。

Phase 2.1: Frame inequality (statement-level API).

We introduce a minimal predicate suitable_window and a Prop capturing the Zak–Mellin frame bounds. Proofs will be supplied in a later phase once the time-shift/modulation operators are fully implemented on L² and the standard Gabor-frame machinery is available.

def Frourio.suitable_window (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Prop

Window suitability predicate: we require unit L²-norm.

Equations

• Frourio.suitable_window w = (‖w‖ = 1)

def Frourio.ZakFrame_inequality (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (Δτ Δξ : ℝ) : Prop

Zak–Mellin frame bounds predicate for steps (Δτ, Δξ).

Equations

• One or more equations did not get rendered due to their size.

theorem Frourio.ZakFrame_inequality_proof (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (Δτ Δξ : ℝ) (hB : ∃ (B : ℝ), besselBound w Δτ Δξ B) (hA : ∃ (A : ℝ), 0 < A ∧ ∀ (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), A * ‖g‖ ^ 2 ≤ FrameEnergy w Δτ Δξ g) : ZakFrame_inequality w Δτ Δξ

Statement-level proof schema for the Zak–Mellin frame inequality. Assuming a Bessel upper bound and a lower frame bound, produce the inequality. In later phases, one derives these bounds from critical sampling Δτ·Δξ = 2π and a suitable window.