Bochner's theorem + Fourier inversion (L¹ case)

Proved

ClockRoPE.fourierTransform_bochner_inversion

by Elsie66 · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

fourier-analysisharmonic-analysismeasure-theorypositive-definite-kernels

Bochner's theorem together with the Fourier inversion formula, packaged as one black-box fact, superseding the narrower ClockRoPE.fourierTransform_nonneg_and_integral_eq_one_v2 (theorem_id bd16893f-1445-41e5-9cc8-5a7c7b2c94ed), which is now deprecated: that version asserted only nonnegativity and normalization of the Fourier transform, but the unbiasedness argument for Proposition 3.1 also needs the Fourier inversion formula recovering $f$ from $\tau$ , which this version adds.

Let $f:\mathbb R\to\mathbb R$ be continuous, Lebesgue-integrable, positive-definite (IsPositiveDefiniteKernel, Definitions.Def_PositiveDefiniteKernel), and normalized ( $f(0)=1$ ). Let $\tau(\xi) = \operatorname{Re}\int_{\mathbb R} f(x)e^{-i2\pi\xi x}\,dx$ (fourierTransform f) be its Fourier transform. The theorem asserts that $\tau$ is continuous, everywhere nonnegative, integrates to $1$ , and recovers $f$ by Fourier inversion at every point:

\tau \text{ is continuous}, \qquad \tau(\xi) \ge 0 \text{ for every } \xi, \qquad \int_{\mathbb R} \tau(\xi)\,d\xi = 1,

f(x) = \int_{\mathbb R} e^{i2\pi\xi x}\,\tau(\xi)\,d\xi \quad \text{for every } x \in \mathbb R.

This packages exactly the two classical facts (Bochner's theorem and Fourier inversion) that Chen et al., ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling (arXiv:2607.26369), combine without proof at the start of the proof of Proposition 3.1 (Eq. 6: $f(p_m-p_n) = \int e^{i2\pi\xi(p_m-p_n)}\tau(\xi)\,d\xi$ ), generalized here to hold at every point $x$ , not only at the specific difference $p_m - p_n$ the paper needs.

Formalization Note The inversion formula is stated as an equality of complex numbers (f x : ℂ on the left) since the right-hand side integral is naturally complex-valued; it collapses to a real equality once combined with the fact that the integral is real (which follows from $\tau$ being even, IsPositiveDefiniteKernel.even).

Preamble

import Mathlib
import Definitions.Def_PositiveDefiniteKernel

Formal statement

namespace ClockRoPE

open MeasureTheory

/-- **Bochner's theorem + Fourier inversion, L¹ case.** If `f : ℝ → ℝ` is continuous,
Lebesgue-integrable, positive-definite, and normalized (`f 0 = 1`), then its Fourier transform
`fourierTransform f` is everywhere nonnegative, integrates to `1`, and recovers `f` by Fourier
inversion. This packages exactly the two classical facts (Bochner's theorem and the Fourier
inversion formula) that Chen et al., *ClockRoPE: Random Fourier Rotations for Temporal Routine
Modeling* (arXiv:2607.26369), combine without proof at the start of the proof of Proposition 3.1
(Eq. 6: `f(p_m-p_n) = ∫ e^{i2πξ(p_m-p_n)} τ(ξ) dξ`), generalized here to hold at every point `x`,
not only at the specific difference `p_m - p_n` the paper needs. -/
theorem fourierTransform_bochner_inversion
    (f : ℝ → ℝ) (hf_cont : Continuous f) (hf_int : Integrable f (volume : Measure ℝ))
    (hf_pd : IsPositiveDefiniteKernel f) (hf0 : f 0 = 1) :
    Continuous (fourierTransform f) ∧
      (∀ ξ : ℝ, 0 ≤ fourierTransform f ξ) ∧
      (∫ ξ : ℝ, fourierTransform f ξ = 1) ∧
      (∀ x : ℝ, (f x : ℂ) =
        ∫ ξ : ℝ, Complex.exp (2 * Real.pi * Complex.I * ξ * x) * (fourierTransform f ξ : ℂ)) := by
  sorry

end ClockRoPE

Source

Salomon Bochner, Monotone Funktionen, Stieltjessche Integrale und harmonische Analyse, Springer, 1933; Fourier inversion theorem (classical, e.g. Rudin, Real and Complex Analysis, Thm 9.11); as invoked in Chen et al., ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling, arXiv:2607.26369, p.3, footnote 1 and proof of Proposition 3.1 (Eq. 6)

View graph