Functional Analysis for AQFT #
This file provides functional analysis tools for Algebraic Quantum Field Theory, focusing on integrability, Schwartz function properties, and L² embeddings.
Key Definitions & Theorems: #
Schwartz Space Properties:
SchwartzMap.hasTemperateGrowth_general: Schwartz functions have temperate growthSchwartzMap.integrable_mul_bounded: Schwartz × bounded → integrableSchwartzMap.integrable_conj: Conjugate of Schwartz function is integrableSchwartzMap.translate: Translation of Schwartz functionsschwartz_integrable_decay: Decay bounds for Schwartz function integrals
Complex Embeddings:
Complex.ofRealCLM_isometry: Real→Complex embedding is isometricComplex.ofRealCLM_continuous_compLp: Continuous lifting to Lp spacesembeddingRealToComplex: Canonical ℝ→ℂ embedding for Lp functions
Schwartz→L² Embedding:
schwartzToL2: Embedding Schwartz functions into L² spaceschwartzToL2': Alternative embedding for EuclideanSpace types
L∞·L² Multiplication:
linftyMulL2CLM: Continuous bilinear map L∞ × L² → L²linfty_mul_L2_CLM_norm_bound: Norm bound ‖f · g‖₂ ≤ ‖f‖∞ · ‖g‖₂
Integrability Results:
integrableOn_ball_of_radial: Radial functions integrable on ballsintegrableOn_ball_of_rpow_decay: Power-law decay integrable on ballsintegrableOn_compact_diff_ball: Integrability on compact ∖ balllocallyIntegrable_of_rpow_decay_real: Local integrability from power decay (d ≥ 3)polynomial_decay_integrable_3d: 1/‖x‖ integrable on 3D ballsschwartz_bilinear_integrable_of_translationInvariant_L1: Bilinear Schwartz integrability
Vanishing & Bounds:
schwartz_vanishing_linear_bound_general: Linear vanishing bounds for Schwartz functions
Bump Function Convolutions:
bumpSelfConv: Self-convolution of bump functionsbumpSelfConv_nonneg,bumpSelfConv_integral: Properties of self-convolutionbumpSelfConv_support_subset,bumpSelfConv_support_tendsto: Support controldouble_mollifier_convergence: Convergence of double mollifier approximations
Utility Lemmas:
norm_exp_I_mul_real,norm_exp_neg_I_mul_real: ‖exp(±i·r)‖ = 1sub_const_hasTemperateGrowth: Translation has temperate growth
Proven theorems in this file #
The following L∞ × L² multiplication theorems are fully proven (2025-12-13):
linftyMulL2CLM(line ~607): L∞ × L² → L² bounded linear operatorlinfty_mul_L2_CLM_spec(line ~639): pointwise specification (g·f)(x) = g(x)·f(x) a.e.linfty_mul_L2_CLM_norm_bound(line ~650): operator norm bound ‖T_g f‖ ≤ C·‖f‖
Schwartz function properties #
Equations
Equations
Compose an Lp function with a continuous linear map. This should be the canonical way to lift real Lp functions to complex Lp functions.
Equations
- composedFunction f A = A.compLp f
Instances For
Embedding from real Lp functions to complex Lp functions using the canonical embedding ℝ → ℂ.
Equations
Instances For
Lifts a probability measure from the space of real Lp functions to the space of complex Lp functions, with support on the real subspace.
Equations
- liftMeasureRealToComplex dμ_real = ⟨MeasureTheory.Measure.map embeddingRealToComplex ↑dμ_real, ⋯⟩
Instances For
Fourier Transform as Linear Isometry on L² Spaces #
The key challenge in defining the Fourier transform on L² spaces is that the Fourier integral ∫ f(x) e^(-2πi⟨x,ξ⟩) dx may not converge for arbitrary f ∈ L²(ℝᵈ).
Construction Strategy (following the Schwartz space approach):
- Dense Core: Use Schwartz functions 𝒮(ℝᵈ) as the dense subset where Fourier integrals converge
- Schwartz Fourier: Apply the Fourier transform on Schwartz space (unitary)
- Embedding to L²: Embed Schwartz functions into L² space
- Plancherel on Core: Show ‖ℱf‖₂ = ‖f‖₂ for f ∈ 𝒮(ℝᵈ)
- Extension: Use the universal property of L² to extend to all of L²
This construction gives a unitary operator ℱ : L²(ℝᵈ) ≃ₗᵢ[ℂ] L²(ℝᵈ).
The EuclideanRd declaration.
Equations
- EuclideanRd d = EuclideanSpace ℝ (Fin d)
Instances For
The SchwartzRd declaration.
Equations
- SchwartzRd d = SchwartzMap (EuclideanRd d) ℂ
Instances For
Core construction components (using Mathlib APIs) #
Embedding Schwartz functions into L² space using Mathlib's toLpCLM. This is a continuous linear map from Schwartz space to L²(ℝᵈ, ℂ). OK IMPLEMENTED: Uses SchwartzMap.toLpCLM from Mathlib
Equations
Instances For
Alternative embedding that produces the exact L² type expected by the unprimed theorems. This maps Schwartz functions to Lp ℂ 2 (volume : Measure (EuclideanSpace ℝ (Fin d))). The difference from schwartzToL2 is only in the type representation, not the mathematical content.
Equations
Instances For
L∞ Multiplication on L² Spaces #
This section proves that multiplication by L∞ functions defines bounded operators on L².
Mathematical background:
- If g ∈ L∞(μ) with ‖g‖∞ ≤ C, then f ↦ g·f is a bounded linear operator L² → L²
- The operator norm satisfies ‖Mg‖ ≤ C
- The action is pointwise a.e.: (Mg f)(x) = g(x) · f(x) a.e.
Proof method (2025-12-13):
- Uses Mathlib's
eLpNorm_smul_le_eLpNorm_top_mul_eLpNormfor the L∞ × Lp → Lp bound - For ℂ, multiplication equals scalar multiplication (g * f = g • f)
- Hölder's inequality via
MemLp.mulwith HolderTriple ∞ 2 2
These theorems are used to construct specific multiplication operators (e.g., momentumWeightSqrtMulCLM) without repeating technical details.
Given a measurable function g that is essentially bounded by C,
multiplication by g defines a bounded linear operator on L².
Equations
- linftyMulL2CLM g hg_meas C hg_bound = (ContinuousLinearMap.holderL μ ⊤ 2 2 (ContinuousLinearMap.mul ℂ ℂ)) (MeasureTheory.MemLp.toLp g ⋯)
Instances For
The multiplication operator acts pointwise almost everywhere on L².
The operator norm of the multiplication operator is bounded by C. This gives ‖Mg f‖₂ ≤ C · ‖f‖₂ for all f ∈ L².
Local Integrability of Power-Law Decay Functions #
Functions with polynomial decay are locally integrable in finite dimensions.
Local version of integrable_fun_norm_addHaar: integrability of radial functions on balls.
If the radial part is integrable on (0, r), then the function is integrable on ball 0 r.
Key technique: Use indicator functions to reduce to the global integrable_fun_norm_addHaar.
- Define g := indicator (Iio r) f, so g(y) = f(y) for y < r, else 0
- Then indicator (ball 0 r) (f ∘ ‖·‖) = g ∘ ‖·‖
- Apply global lemma to g
Integrability on balls for power-law decay functions. If |f(x)| ≤ C‖x‖^{-α} with α < d, then f is integrable on any ball centered at 0.
Integrability away from the origin for bounded functions on compact sets.
Functions with polynomial decay are locally integrable. For d-dimensional space, if α < d and |f(x)| ≤ C‖x‖^{-α}, then f is locally integrable.
Polynomial decay is integrable in 3D: The function 1/(1+‖x‖)^4 is integrable over SpatialCoords = EuclideanSpace ℝ (Fin 3).
This is a standard result: decay rate 4 > dimension 3 ensures integrability.
Mathematical content: In ℝ³ with spherical coordinates, ∫ 1/(1+r)^4 · r² dr dΩ = 4π ∫₀^∞ r²/(1+r)^4 dr < ∞ since the integrand decays as r⁻² for large r.
Used by: spatialNormIntegral_linear_bound and F_norm_bound_via_linear_vanishing
to show that spatial integrals of Schwartz functions with linear time vanishing
are bounded by C·t.
Bilinear Integrability for L¹ Translation-Invariant Kernels #
For translation-invariant kernels K₀ that are integrable (L¹), the bilinear form f(x) K₀(x-y) g(y) with Schwartz test functions f, g is integrable on E × E.
This applies to exponentially decaying kernels like the massive free covariance.
For translation-invariant kernels K₀ that are integrable (L¹), the bilinear form with Schwartz test functions is integrable. This is the easiest case and applies to exponentially decaying kernels like the massive free covariance.
Proof idea:
- Schwartz functions are bounded: ‖f‖_∞ < ∞ (via toBoundedContinuousFunction)
- Schwartz functions are integrable: ‖g‖_{L¹} < ∞
- K₀ is integrable: ‖K₀‖_{L¹} < ∞
- Then: ∫∫ |f(x) K₀(x-y) g(y)| dx dy ≤ ‖f‖∞ · ‖K₀‖{L¹} · ‖g‖_{L¹} < ∞
Schwartz Functions Times Bounded Functions #
These lemmas establish integrability of Schwartz functions multiplied by bounded measurable functions, which is essential for Fourier transform computations.
A Schwartz function times a bounded measurable function is integrable. This is the key technical lemma for Fourier-type integrals.
The conjugate of a Schwartz function is integrable.
Phase Exponential Lemmas #
Lemmas about complex exponentials of pure imaginary arguments, used in Fourier analysis.
Complex exponential of pure imaginary argument has norm 1.
Complex exponential of negative pure imaginary argument has norm 1.
Linear Vanishing Bound for Schwartz Functions #
If a Schwartz function on ℝ × E vanishes for t ≤ 0, then it grows at most linearly in t. This is a key lemma for UV regularization in QFT integrals.
The Linear Vanishing Bound (general version). If f : 𝓢(ℝ × E, ℂ) vanishes for t ≤ 0, it grows at most linearly in t for t > 0.
This follows from the Mean Value Theorem: f(t,x) - f(0,x) = ∫₀ᵗ ∂ₜf dt, and since ∂ₜf is bounded (Schwartz), we get |f(t,x)| ≤ C·t.
Schwartz Translation Invariance #
Translation by a constant vector preserves Schwartz class. This is a fundamental fact in harmonic analysis: if f ∈ 𝒮(ℝⁿ), then f(· - a) ∈ 𝒮(ℝⁿ) for any a ∈ ℝⁿ.
Mathematical proof:
- Smoothness: f(x - a) is C∞ if f is (composition with smooth translation)
- Decay: ‖x‖^k |D^n f(x-a)| ≤ C' follows from ‖y‖^m |D^n f(y)| ≤ C for y = x - a using the triangle inequality ‖x‖ ≤ ‖x-a‖ + ‖a‖ and taking m large enough
Reference: Stein-Weiss, "Fourier Analysis", Chapter 1; any Schwartz space text
Translation x ↦ x - a is antilipschitz (actually an isometry).
Schwartz functions are invariant under translation. For f ∈ 𝒮(E, F) and a ∈ E, the translated function f(· - a) is also in 𝒮(E, F).
This is proved using Mathlib's compCLMOfAntilipschitz: translation is composition
with x ↦ x - a, which has temperate growth and is antilipschitz (an isometry).
Equations
- f.translate a = (SchwartzMap.compCLMOfAntilipschitz ℝ ⋯ ⋯) f
Instances For
Schwartz Integrable Decay #
Schwartz functions decay faster than any polynomial inverse. This justifies integrability conditions.
Schwartz L¹ bound: Schwartz functions are integrable with explicit decay. For f ∈ 𝓢(ℝⁿ), we have ∫ |f(x)| dx < ∞.
More precisely, for any N, there exists C such that |f(x)| ≤ C / (1 + |x|)^N. If N > dim(V), this implies integrability.
Reference: Stein-Weiss, Chapter 1, Proposition 1.1
Double Mollifier Convergence #
This section proves the double mollifier convergence theorem: for a continuous kernel C (away from the origin), the double convolution with mollifiers converges to the kernel value at separated points:
∫∫ φ_ε(x-a) C(x-y) φ_ε(y) dx dy → C(a) as ε → 0
The key insight is that the self-convolution φ ⋆ φ is itself an approximate identity, so by associativity we reduce to a single convolution limit.
The self-convolution of a normalized bump function.
Equations
Instances For
Self-convolution is nonnegative.
Self-convolution has mass 1: ∫(φ ⋆ φ) = (∫φ)(∫φ) = 1·1 = 1.
Support of self-convolution is contained in ball of radius 2*rOut.
Self-convolution support shrinks to {0} as rOut → 0.
Main theorem: Double mollifier convergence via associativity.
For C continuous on {x ≠ 0}, the double mollifier integral converges: ∫∫ φ_ε(x-a) C(x-y) φ_ε(y) dx dy → C(a) as ε → 0
Proof strategy:
- Recognize that ψ := φ ⋆ φ (self-convolution) is an approximate identity:
- Nonnegative (integral of product of nonneg functions)
- Mass 1: ∫ψ = (∫φ)² = 1
- Shrinking support: supp(ψ) ⊆ B(0, 2·rOut)
- By associativity: ∫∫ φ(x-a) C(x-y) φ(y) dx dy = (ψ ⋆ C)(a)
- Apply single-convolution theorem: (ψ ⋆ C)(a) → C(a)