Schwartz Bilinear Translation Decay

This file proves that bilinear integrals of Schwartz functions against a decaying kernel vanish at infinity under translation.

Main Result

schwartz_bilinear_translation_decay: For Schwartz functions f, g on a finite-dimensional real inner product space E, and a kernel K : E → ℝ with polynomial decay |K(z)| ≤ C/‖z‖^α for large ‖z‖, the bilinear integral against a translated g vanishes at infinity:

∫∫ f(x) · K(x - y) · g(y - a) dx dy → 0 as ‖a‖ → ∞

Proof Strategy (via convolutions)

The key theorem is: L¹ ⋆ C₀ → C₀ (convolution of integrable with vanishing-at-∞ vanishes)

Apply this pattern three times:

1. f ⋆ K_sing: f is C₀ (Schwartz), K_sing is L¹ → result is C₀
2. f ⋆ K_tail: f is L¹ (Schwartz), K_tail is C₀ (decay) → result is C₀
3. (f ⋆ K) ⋆ g: g is L¹, (f ⋆ K) is C₀ → result is C₀

References

• Glimm-Jaffe "Quantum Physics" Ch. 6 (clustering)
• Reed-Simon Vol. II, Ch. X (decay of correlations)

Helper lemmas for Schwartz functions

theorem schwartz_integrable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : SchwartzMap E ℂ) : MeasureTheory.Integrable (⇑f) MeasureTheory.volume

Schwartz functions are integrable.

theorem schwartz_tendsto_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : SchwartzMap E ℂ) : Filter.Tendsto (⇑f) (Filter.cocompact E) (nhds 0)

Schwartz functions vanish at infinity (C₀).

Proof: Schwartz decay gives ‖x‖^k · ‖f(x)‖ ≤ seminorm k 0 f for all k. Taking k = 1: ‖f(x)‖ ≤ C/‖x‖ → 0 as ‖x‖ → ∞.

Kernel decomposition

noncomputable def kernelSingular {E : Type u_1} [NormedAddCommGroup E] (K : E → ℝ) (R₀ : ℝ) : E → ℝ

The singular (compactly supported) part of the kernel.

Equations

• kernelSingular K R₀ x = K x * (Metric.closedBall 0 R₀).indicator (fun (x : E) => 1) x

noncomputable def kernelTail {E : Type u_1} [NormedAddCommGroup E] (K : E → ℝ) (R₀ : ℝ) : E → ℝ

The tail (decaying) part of the kernel.

Equations

• kernelTail K R₀ x = K x * (Metric.closedBall 0 R₀)ᶜ.indicator (fun (x : E) => 1) x

theorem kernel_decomposition {E : Type u_1} [NormedAddCommGroup E] (K : E → ℝ) (R₀ : ℝ) : K = fun (x : E) => kernelSingular K R₀ x + kernelTail K R₀ x

Kernel decomposes into singular and tail parts.

theorem kernelTail_tendsto_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (K : E → ℝ) (R₀ α : ℝ) (hα : α > 0) (C : ℝ) (hK_decay : ∀ (z : E), ‖z‖ ≥ R₀ → |K z| ≤ C / ‖z‖ ^ α) : Filter.Tendsto (kernelTail K R₀) (Filter.cocompact E) (nhds 0)

K_tail vanishes at infinity when K has polynomial decay.

Key theorem: L¹ ⋆ C₀ → C₀

This is the main engine of the proof. In Mathlib this should be something like convolution_tendsto_zero_of_integrable_of_continuous_vanishing or similar.

theorem bounded_of_continuous_tendsto_zero {E : Type u_1} [NormedAddCommGroup E] {g : E → ℂ} (hg_cont : Continuous g) (hg_zero : Filter.Tendsto g (Filter.cocompact E) (nhds 0)) : ∃ (C : ℝ), ∀ (x : E), ‖g x‖ ≤ C

A continuous function vanishing at infinity is bounded.

theorem integrable_tail_small {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {f : E → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (ε : ℝ) (hε : 0 < ε) : ∃ (K : Set E), IsCompact K ∧ ∫ (x : E) in Kᶜ, ‖f x‖ < ε

For integrable f and ε > 0, there exists a compact set K with small tail integral.

This is a standard consequence of integrability - the integral concentrates on compact sets.

theorem convolution_vanishes_of_integrable_and_C0 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {f g : E → ℂ} (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (hg_C0 : Filter.Tendsto g (Filter.cocompact E) (nhds 0)) (hg_cont : Continuous g) : Filter.Tendsto (fun (y : E) => ∫ (x : E), f x * g (x - y)) (Filter.cocompact E) (nhds 0)

Convolution of an integrable function with a function vanishing at infinity also vanishes at infinity. This is a fundamental result in harmonic analysis.

Product Space Integrability for Fubini

The bilinear integrand f(x) K(x-y) g(y-a) is integrable on E × E when:

• f, g are Schwartz functions
• K is locally integrable with bounded tail (e.g., exponential/polynomial decay)

This is used for Fubini swaps in bilinear integral proofs.

theorem schwartz_bilinear_prod_integrable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f g : SchwartzMap E ℂ) (K : E → ℝ) (hK_meas : Measurable K) (hK_loc : MeasureTheory.LocallyIntegrable K MeasureTheory.volume) (R₀ : ℝ) (_hR₀ : R₀ > 0) (hK_tail_bdd : ∃ (M : ℝ), ∀ (z : E), |kernelTail K R₀ z| ≤ M) (a : E) : MeasureTheory.Integrable (Function.uncurry fun (x y : E) => f x * ↑(K (x - y)) * g (y - a)) (MeasureTheory.volume.prod MeasureTheory.volume)

Product integrability for Schwartz bilinear forms with locally integrable kernel

For Schwartz f, g and kernel K = K_sing + K_tail where K_sing is compactly supported (hence integrable) and K_tail is bounded, the product f(x) K(x-y) g(y-a) is integrable on E × E.

This enables Fubini's theorem to swap integration order: ∫∫ f(x) K(x-y) g(y-a) dx dy = ∫ (∫ f(x) K(x-y) dx) g(y-a) dy

Main theorem

noncomputable def schwartzBilinearIntegral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f g : SchwartzMap E ℂ) (K : E → ℝ) (a : E) : ℂ

The bilinear integral of Schwartz functions against a decaying kernel

Equations

• schwartzBilinearIntegral f g K a = ∫ (x : E) (y : E), f x * ↑(K (x - y)) * g (y - a)

theorem schwartz_bilinear_translation_decay_proof {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f g : SchwartzMap E ℂ) (K : E → ℝ) (hK_meas : Measurable K) (hK_loc : MeasureTheory.LocallyIntegrable K MeasureTheory.volume) (α : ℝ) (hα : α > 0) (C R₀ : ℝ) (hC : C > 0) (hR₀ : R₀ > 0) (hK_cont : ContinuousOn K (Metric.closedBall 0 R₀)ᶜ) (hK_decay : ∀ (z : E), ‖z‖ ≥ R₀ → |K z| ≤ C / ‖z‖ ^ α) : Filter.Tendsto (schwartzBilinearIntegral f g K) (Filter.cocompact E) (nhds 0)

Clustering decay for Schwartz bilinear forms (proof version)

For Schwartz functions f, g and a kernel K with polynomial decay, the bilinear integral tends to 0 as the translation parameter a → ∞.

This version adds LocallyIntegrable hypothesis to handle kernel singularities.