Quantitative Decay for Schwartz Bilinear Forms

This file proves that bilinear integrals of Schwartz functions against an exponentially decaying kernel have polynomial decay at any rate.

Main Result

schwartz_bilinear_translation_decay_polynomial_proof: For Schwartz functions f, g and a kernel K with exponential decay |K(z)| ≤ C_K * exp(-m‖z‖), the bilinear integral decays polynomially:

|∫∫ f(x) · K(x - y) · g(y - a) dx dy| ≤ c * (1 + ‖a‖)^{-α}

for any α > 0.

Proof Strategy

1. Define a PolynomialDecayBound structure to track decay constants
2. Show Schwartz functions have polynomial decay (via Mathlib seminorms)
3. Prove exponential decay implies polynomial decay at any rate
4. Prove split convolution lemma: conv of two polynomial-decay functions decays
5. Apply to the bilinear integral by decomposing K = K_sing + K_tail

References

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

Phase 1: Polynomial Decay Structure and Schwartz Bridge

structure PolynomialDecayBound {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] (f : E → F) (N : ℝ) : Type

A function f has polynomial decay of order N with constant C if ‖f(x)‖ ≤ C / (1 + ‖x‖)^N for all x.

• C : ℝ

  Positive constant controlling the polynomial decay bound.

• hC_pos : self.C > 0
• bound (x : E) : ‖f x‖ ≤ self.C / (1 + ‖x‖) ^ N

noncomputable def schwartzHasPolynomialDecay {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : SchwartzMap E ℂ) (k : ℕ) : PolynomialDecayBound ⇑f ↑k

Schwartz functions have polynomial decay at any natural number rate.

This follows from SchwartzMap.one_add_le_sup_seminorm_apply: (1 + ‖x‖)^k * ‖D^n f(x)‖ ≤ 2^k * seminorm_{k,n} f

Taking n = 0 and rearranging gives ‖f(x)‖ ≤ C * (1 + ‖x‖)^{-k}.

Equations

• schwartzHasPolynomialDecay f k = { C := 2 ^ k * ((Finset.Iic (k, 0)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm ℂ m.1 m.2) f + 1, hC_pos := ⋯, bound := ⋯ }

noncomputable def schwartzHasPolynomialDecayReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : SchwartzMap E ℂ) (N : ℝ) (_hN : N > 0) : PolynomialDecayBound (⇑f) N

Schwartz functions have polynomial decay at any real rate (via ceiling).

Equations

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

Phase 2: Exponential to Polynomial Conversion

theorem exp_decay_implies_polynomial_decay (m α : ℝ) (hm : m > 0) (hα : α > 0) : ∃ C > 0, ∀ x ≥ 0, Real.exp (-m * x) ≤ C * (1 + x) ^ (-α)

For any α > 0 and m > 0, exponential decay implies polynomial decay: exp(-mx) ≤ C * (1 + x)^{-α} for all x ≥ 0.

This uses the fact that x^α * exp(-mx) is bounded (it tends to 0 at infinity).

noncomputable def normExpDecayImpliesPolynomialDecay {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] (g : E → F) (m C_exp R₀ : ℝ) (hm : m > 0) (hC_exp : C_exp > 0) (hR₀ : R₀ > 0) (hg_decay : ∀ (z : E), ‖z‖ ≥ R₀ → ‖g z‖ ≤ C_exp * Real.exp (-m * ‖z‖)) (hg_bdd : ∃ (M : ℝ), ∀ (z : E), ‖g z‖ ≤ M) (α : ℝ) (hα : α > 0) : PolynomialDecayBound g α

Exponential decay of norms implies polynomial decay bounds.

Equations

• normExpDecayImpliesPolynomialDecay g m C_exp R₀ hm hC_exp hR₀ hg_decay hg_bdd α hα = { C := max (C_exp * Classical.choose ⋯) (Classical.choose hg_bdd * (1 + R₀) ^ α) + 1, hC_pos := ⋯, bound := ⋯ }

Phase 3: Split Convolution Lemma

theorem one_add_half_pow_le (x : ℝ) (hx : x ≥ 0) (N : ℝ) (hN : N > 0) : (1 + x / 2) ^ (-N) ≤ 2 ^ N * (1 + x) ^ (-N)

Helper: (1 + x/2)^{-N} ≤ 2^N * (1 + x)^{-N} for x ≥ 0 and N > 0.

This follows from 1 + x ≤ 2 + x = 2(1 + x/2), so (1+x)^N ≤ 2^N(1+x/2)^N.

noncomputable def convolutionPolynomialDecay {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u v : E → ℂ} {N : ℝ} (hN_dim : N > ↑(Module.finrank ℝ E)) (hu_decay : PolynomialDecayBound u N) (hv_decay : PolynomialDecayBound v N) (hu_int : MeasureTheory.Integrable u MeasureTheory.volume) (hv_int : MeasureTheory.Integrable v MeasureTheory.volume) : PolynomialDecayBound (fun (x : E) => ∫ (y : E), u y * v (x - y)) N

If two integrable functions have polynomial decay of order N > dim E, then their convolution has polynomial decay of the same order.

Equations

• convolutionPolynomialDecay hN_dim hu_decay hv_decay hu_int hv_int = ⋯.choose

Phase 4: Kernel Decomposition Bounds

noncomputable def convolutionCompactSupportDecay {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : SchwartzMap E ℂ) (K : E → ℝ) (R₀ : ℝ) (hR₀ : R₀ > 0) (hK_loc : MeasureTheory.LocallyIntegrable K MeasureTheory.volume) (N : ℕ) (_hN : N > 0) : PolynomialDecayBound (fun (y : E) => ∫ (x : E), f x * ↑(kernelSingular K R₀ (x - y))) ↑N

Convolution of a Schwartz function with the compactly supported singular kernel part has polynomial decay.

Equations

• convolutionCompactSupportDecay f K R₀ hR₀ hK_loc N _hN = ⋯.choose

noncomputable def convolutionExpDecayPolynomialDecay {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : SchwartzMap E ℂ) (K : E → ℝ) (R₀ m C_K : ℝ) (hR₀ : R₀ > 0) (hm : m > 0) (hC_K : C_K > 0) (hK_loc : MeasureTheory.LocallyIntegrable K MeasureTheory.volume) (hK_decay : ∀ (z : E), ‖z‖ ≥ R₀ → |K z| ≤ C_K * Real.exp (-m * ‖z‖)) (hK_bdd : ∃ (M : ℝ), ∀ (z : E), |kernelTail K R₀ z| ≤ M) (N : ℝ) (hN_dim : N > ↑(Module.finrank ℝ E)) (hN : N > 0) : PolynomialDecayBound (fun (y : E) => ∫ (x : E), f x * ↑(kernelTail K R₀ (x - y))) N

Convolution of a Schwartz function with the exponentially decaying kernel tail has polynomial decay at any rate above the dimension.

Equations

• convolutionExpDecayPolynomialDecay f K R₀ m C_K hR₀ hm hC_K hK_loc hK_decay hK_bdd N hN_dim hN = ⋯.choose

Phase 5: Main Theorem Assembly

theorem schwartz_bilinear_translation_decay_polynomial_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) (m : ℝ) (hm : m > 0) (C_K R₀ : ℝ) (hC_K : C_K > 0) (hR₀ : R₀ > 0) (_hK_cont : ContinuousOn K (Metric.closedBall 0 R₀)ᶜ) (hK_decay : ∀ (z : E), ‖z‖ ≥ R₀ → |K z| ≤ C_K * Real.exp (-m * ‖z‖)) (α : ℝ) (hα : α > 0) : ∃ c ≥ 0, ∀ (a : E), ‖∫ (x : E) (y : E), f x * ↑(K (x - y)) * g (y - a)‖ ≤ c * (1 + ‖a‖) ^ (-α)

Quantitative polynomial decay for Schwartz bilinear forms (proven theorem)

For Schwartz functions f, g and a kernel K with exponential decay |K(z)| ≤ C_K · e^{-m‖z‖} (for large ‖z‖, from mass gap m > 0), the bilinear integral decays polynomially at any rate α > 0:

|∫∫ f(x) · K(x - y) · g(y - a) dx dy| ≤ c(f,g,α) · (1 + ‖a‖)^{-α}

The proof structure:

1. Decompose K = K_sing + K_tail
2. Show H(y) = ∫ f(x) K(x-y) dx = H_sing(y) + H_tail(y) has polynomial decay
3. The integral I(a) = ∫ H(y) g(y-a) dy = (H ⋆ gtilde)(a) where gtilde(z) = g(-z)
4. Apply convolutionPolynomialDecay to get the result