fourier/

This directory does Fourier analysis of probability laws without complex numbers, which MathComp-Analysis lacks. A characteristic function is a pair of real integrals, E[cos (t X)] and E[sin (t X)], and a pair (a, b) stands for a + i b, with the complex product cmul and modulus cmod.

Laws on the line are probabilities on measurableTypeR R, the type of normal_prob. Independence is a product measure, P1 \x P2 or tuple_prod mu n (probability/lindeberg.v). The law of a sum or an image is a parameter nu, assumed to be that image measure. Here <x, theta> is mxdot x theta and |x| is the Euclidean norm frobenius x.

The files lead to the vector small-ball estimate of Koehler and Sohn (arXiv 2608.27372, Proposition 2.4), used in the satisfiable phase of the universality proof in extension/. On the way they prove Esseen's inequality, a concentration bound for independent sums, and a bound of probabilities by the integral of |cf|, without inversion. The last file proves Fourier inversion on row vectors.

Reading order

1. charfun.v: characteristic functions on the line: images, affine maps, independent sums, symmetrization, the normal law.
2. esseen.v: the Levy concentration function, Esseen's inequality, the concentration of sums.
3. gauss_factor.v: Lemma 3.5 of Koehler and Sohn and its first half.
4. charfun_rV.v: characteristic functions on 'rV[R]_m, the Gaussian case, independent sums, Gaussian regularization.
5. small_ball.v: Lemma 3.8 of Koehler and Sohn and the vector small-ball estimate.
6. inversion.v: the Fourier inversion theorem on 'rV[R]_m.

Core definitions

• cf_re, cf_im, cf, cf_norm (charfun.v): E[cos (t X)] and E[sin (t X)] for X of law mu on the line, their pair and its modulus.
• cf_rV_re, cf_rV_im, cf_rV, cf_rV_norm (charfun_rV.v): the same for a law on 'rV[R]_m, with cos <x, theta> and sin <x, theta>.
• conc_fun (esseen.v): the Levy concentration function Q(mu, L) = sup_a mu [a, a + L].
• sym_law (gauss_factor.v): the law of X - X' for independent X, X' of law mu.
• cf_rV_density (inversion.v): (2 pi)^-m \int (cos <theta, w> cf_rV_re nu theta + sin <theta, w> cf_rV_im nu theta) dtheta. cf_rV_inv_prob is the probability with this density, when |cf_rV nu| is integrable.

Main results

On the line.

• cf_sym, cf_normal: the law of X - X', for X, X' independent of law mu, has the characteristic function (cf_norm mu t ^ 2, 0); for nonzero s, cf (normal_prob m s) t = exp (- (s t)^2 / 2) (cos (m t), sin (m t)).

Concentration.

• esseen: Q(mu, 2 pi / T) <= pi^2 / (4 T) \int_{-T}^{T} cf_norm mu t dt for every law mu and T > 0.
• conc_fun_sum: for n >= 1, v, lambda, eps > 0, L >= 0 and independent x_1, ..., x_n of laws mu_k with E[x_k^2] <= v and Q(mu_k, lambda) <= 1 - eps, the law nu of the sum satisfies Q(nu, L) <= 2 pi^2 sqrt pi (L + sqrt (v / eps)) / (lambda sqrt (eps n)).

Lemma 3.5 of Koehler and Sohn.

• gauss_factor_le: for v, lambda, eps > 0, a law mu with E[X^2] <= v and Q(mu, lambda) <= 1 - eps, 0 < r <= 1/2 and r <= s, \int |cf mu u|^(1/r^2) exp (- s^2 u^2 / (2 r^2)) du <= r gauss_factor_const v lambda eps.
• conc_fun_truncated_level: a law with mean 0, E[X^2] = 1 and E[X^2 1_{|X| <= M}] >= c, M > 0, has Q(mu, L) <= 1 - min ((c - 4 L^2) / M^2, L^2 / (2 L^2 + 1)) for every L > 0.

On row vectors.

• cf_rV_gauss, cf_rV_tuple_prod: cf_rV (gauss m) theta = (exp (- |theta|^2 / 2), 0); if nu is the law of sum_k x_k w_k under tuple_prod mu n, cf_rV nu theta is the complex product of the cf (mu k) <w_k, theta>.
• prod_gauss_le_cf_rV: for Y of law nu, an independent G of law gauss m, s > 0 and B measurable, P(Y + s G in B) <= (2 pi)^-m (\int exp (- s^2 |theta|^2 / 2) |cf_rV nu theta| dtheta) lebesgue_rV m B.
• ball_le_cf_rV: if \int |cf_rV nu| < +oo, the same bound holds with s = 0 for P(Y in B), B a closed Euclidean ball of radius r > 0.

Small balls.

• vector_small_ball: for v, lambda, eps > 0 there is C > 0 such that, if x has law tuple_prod mu n with E[x_k^2] <= v and Q(mu_k, lambda) <= 1 - eps, and the w_k in 'rV[R]_m satisfy sum_k <y, w_k>^2 >= |y|^2 for all y and |w_k| <= rho, rho > 0, then P(|sum_k x_k w_k - z| <= eta sqrt m) <= (C eta)^m for all eta >= C rho and all z.
• vector_small_ball_moments: the same for laws with mean 0, E[x^2] = 1 and E[x^2 1_{|x| <= M}] >= 1/2, with C depending only on M > 0, as in Proposition 2.4.

Inversion.

• cf_rV_inversion: if \int |cf_rV nu| < +oo against lebesgue_rV m, then nu X = \int_X cf_rV_density nu for every measurable X; the density is continuous, nonnegative and at most (2 pi)^-m \int |cf_rV nu| (continuous_cf_rV_density, cf_rV_density_ge0, cf_rV_density_le).

How the proofs go

• esseen uses fejer T, half the Fejer kernel, which fejer_ge bounds below by 2 T / pi^2 for |z| <= pi / T (Jordan's inequality). conc_fun_sum writes |cf nu| as a product (cf_norm_tuple_prod), bounds each factor through the symmetrization X - X' (sym_cf_bound) and applies esseen0.
• gauss_factor_le bounds |cf mu|^(1/r^2) by the characteristic function of a sum of floor (1 / (2 r^2)) independent copies of sym_law mu (cf_re_sum_sym); a Gaussian Fubini identity and conc_fun_sum conclude.
• prod_gauss_le_cf_rV writes E[exp (- |z - Y|^2 / (2 s^2))] as a Gaussian average of cf_rV nu (cf_rV_regularization), after Ball and Nazarov. ball_le_cf_rV lets s tend to 0.
• vector_small_ball_fourier combines Lemma 3.8 (cf_rV_regularized_le, from the Brascamp-Lieb inequality brascamp_lieb_ge0 with u_k = w_k / |w_k| and c_k = |w_k|^2), the removal of the Gaussian (ball_le_add_gauss) and a whitening matrix turning the w_k into a frame. vector_small_ball takes that matrix from whitening_exists and the constant from gauss_factor_exists.
• cf_rV_inversion shows that Y + s G has the same law whether Y has law nu or cf_rV_inv_prob, and concludes with lipschitz_add_gauss and measure_lipschitz_unique.

Connections

• Requires probability/lindeberg.v, seven files of gaussian/ (among them gaussian/gauss.v and gaussian/lebesgue_rV.v), matrix/euclidean.v, matrix/real_spectral.v, matrix/whitening.v, and five of comparison/, among them comparison/gauss_law.v and comparison/brascamp_lieb_lebesgue.v.
• Used by matrix/covering.v and random_matrix/goe.v. Outside the library, extension/Sat/OneStage.v uses vector_small_ball_moments, and extension/Paired/ uses Rintegral_FTC and Rintegral_even of esseen.v. applications/ does not require it.