Raphaël Lachièze-Rey

Giovanni Peccati

Fine Gaussian fluctuations on the Poisson space, I: contractions, cumulants and geometric random graphs

Keywords: Central Limit Theorems, Contractions, Malliavin Calculus, Poisson Limit Theorems, Poisson Space, Random Graphs, Stein's Method, U -statistics, Wasserstein Distance, Wiener Chaos 2000 Mathematics Subject Classification: 60H07, 60F05, 60G55, 60D05

We study the normal approximation of functionals of Poisson measures having the form of a finite sum of multiple integrals. When the integrands are nonnegative, our results yield necessary and sufficient conditions for central limit theorems. These conditions can always be expressed in terms of contraction operators or, equivalently, fourth cumulants. Our findings are specifically tailored to deal with the normal approximation of the geometric U -statistics introduced by Reitzner and Schulte (2011). In particular, we shall provide a new analytic characterization of geometric random graphs whose edge-counting statistics exhibit asymptotic Gaussian fluctuations, and describe a new form of Poisson convergence for stationary random graphs with sparse connections. In a companion paper, the above analysis is extended to general U -statistics of marked point processes with possibly rescaled kernels.

Introduction

This paper concerns the normal approximation of random variables living inside a fixed sum of Wiener chaoses associated with a Poisson measure over a Borel measure space. Our main theoretical tools come from the two papers [START_REF] Peccati | Stein's method and normal approximation of Poisson functionals[END_REF][START_REF] Peccati | Multi-dimensional Gaussian fluctuations on the Poisson space[END_REF], respectively by Peccati et al. and Peccati and Zheng, where the normal approximation of functional of Poisson measures is studied by combining two probabilistic techniques, namely the Stein's method and the Malliavin calculus of variations.

We shall focus on conditions implying that a given sequence of random variables satisfies a central limit theorem (CLT), where the convergence in distribution takes place in the sense of the Wasserstein distance (see Section 1.1 for definitions). Our main concern is to provide analytic conditions for asymptotic normality, that is, conditions only involving expressions related to the kernels in the chaotic expansion of a given random variable. In particular, our approach does not involve computations based on the method of moments and cumulants (with the exception of Theorem 4.14, where we deal with Poisson approximations).

The main contributions of our paper are the following:

-In Theorem 3.5, we shall prove that conditions for asymptotic normality can be expressed in terms of norms of contraction operators (see Section 2.2). These analytic objects already appear in CLTs living inside a fixed Wiener chaos (see [START_REF] Peccati | Stein's method and normal approximation of Poisson functionals[END_REF][START_REF] Peccati | Multi-dimensional Gaussian fluctuations on the Poisson space[END_REF]), and are a crucial tool in order to effectively assess bounds based on Malliavin operators. One further important point is that the use of contraction operators allows one to neatly distinguish the contribution of each chaotic projection to the CLT, as well as to deduce joint CLTs for these projections starting from the asymptotic normality of their sum (see Proposition 3.14).

-In Theorem 3.12 we shall prove that, when specialized to random variables such that each kernel in the Wiener-Itô representation has a constant sign, our results yield necessary and sufficient conditions for asymptotic normality. The main tools in order to show such a result are two new analytic bounds, stated in Proposition 3.8 and Proposition 3.9. These findings extend to the Poisson framework the 'fourth moment theorem' proved by Nualart and Peccati (in a Gaussian setting) in [START_REF] Nualart | Central limit theorems for sequences of multiple stochastic integrals[END_REF], a result that has been the starting point of a new line of research in stochastic analysis -see the book [START_REF] Nourdin | Normal approximations using Malliavin calculus: from Stein's method to universality[END_REF], as well as the constantly updated webpage http : //www.iecn.unancy.fr/ nourdin/steinmalliavin.htm.

-As discussed below, random variables having Wiener-Itô kernels with constant sign appear quite naturally in problems arising in stochastic geometry. In particular, we shall use our results in order to provide an exhaustive characterization of stationary geometric random graphs whose edge counting statistics exhibit asymptotic Gaussian fluctuations (see Theorem 4.11). This family of geometric graphs contains e.g. interval graphs and disk graphs -see e.g. [START_REF] Clark | Unit disk graphs[END_REF][START_REF] Decreusefond | Simplicial Homology of Random Configurations[END_REF][START_REF] Ferraz | Statistics of geometric random simplicial complexes[END_REF][START_REF] Mcdiarmid | Random channel assignment in the plane[END_REF][START_REF] Müller | Two-point concentration in random geometric graphs[END_REF][START_REF] Penrose | Random Geometric Graphs[END_REF]. Our characterization of geometric random graphs involves 'diagonal subsets' of Cartesian products, that are reminiscent of the combinatorial conditions for CLTs used by Blei and Janson in [START_REF] Blei | Rademacher chaos: tail estimates versus limit theorems[END_REF], in the framework of CLTs for finite Rademacher sums (see also [START_REF] Nourdin | Stein's method and stochastic analysis of Rademacher sequences[END_REF]Section 6]). As a by-product of our analysis (see Theorem 4.14), we shall illustrate a new form of Poisson convergence for random graphs with sparse connections.

We stress that one of our main motivations comes from a remarkable paper by Reitzner and Schulte [START_REF] Reitzner | Central Limit Theorems for U-Statistics of Poisson Point Processes[END_REF], laying the foundations of a general theory for CLTs involving U -statistics based on Poisson point processes. In particular, one of the crucial insights of [START_REF] Reitzner | Central Limit Theorems for U-Statistics of Poisson Point Processes[END_REF] concerns the use of a formula by Last and Penrose (see [START_REF] Last | Poisson process Fock space representation, chaos expansion and covariance inequalities[END_REF]), providing explicit expressions for Wiener-Itô chaotic decompositions in terms of difference operators (see Theorem 2.9). It is interesting to note that Last and Penrose's formula is the Poisson analogous of the so-called 'Stroock formula' of Malliavin calculus, which is in turn an important tool for proving CLTs involving non-linear functionals of Gaussian measures (see e.g. [START_REF] Nourdin | Normal approximations using Malliavin calculus: from Stein's method to universality[END_REF]Corollary 2.7.8] for a discussion of this point). We shall see that our findings complement and extend the results proved in [START_REF] Reitzner | Central Limit Theorems for U-Statistics of Poisson Point Processes[END_REF] in several directions. See also Decreusefond et al. [START_REF] Decreusefond | Simplicial Homology of Random Configurations[END_REF], Ferraz and Vergne [START_REF] Ferraz | Statistics of geometric random simplicial complexes[END_REF], Last et al. [START_REF] Last | Moments and central limit theorems for some multivariate Poisson functionals[END_REF], Minh [START_REF] Minh | Malliavin-Stein method for multi-dimensional U-statistics of Poisson point processes[END_REF], Schulte [START_REF] Schulte | A Central Limit Theorem for the Poisson-Voronoi Approximation[END_REF], Schulte and Thaele [START_REF] Schulte | Exact and asymptotic results for intrinsic volumes of Poisson k-flat processes[END_REF][START_REF] Schulte | The scaling limit of Poisson-driven order statistics with applications in geometric probability[END_REF], for several new findings pertaining to this line of research.

In order to keep the length of this paper within bounds, in Section 4 we will present applications that are related to a very specific setting, namely edge-counting in random geometric graphs with possibly large connections. The power and flexibility of the results proved in the present work are further illustrated in the companion paper [START_REF] Lachièze-Rey | Fine Gaussian fluctuations on the Poisson space II: rescaled kernels, marked processes and geometric U-statistics[END_REF], where the following applications are developed in full detail:

(i) analytic bounds for the normal approximation of U -statistics based on marked point processes, in particular U -statistics with rescaled kernels;

(ii) bounds for general subgraph counting in the disk graph model under any regime;

(iii) an exhaustive characterization of the asymptotic behavior of geometric U -statistics;

(iv) applications to the boolean model, and to subgraph counting in disk graph models with random radius.

The rest of this section is devoted to the formal presentation of the main problems that are addressed in this paper.

Poisson measures

Throughout the paper (Z, Z , µ) is a measure space such that Z is a Borel space, Z is the associated Borel σ-field, and µ is a σ-finite Borel measure with no atoms. We write Z µ = {B ∈ Z : µ(B) < ∞} to denote the subclass of Z composed of sets with finite measure. Also, we shall write η = {η(B) : B ∈ Z µ } to indicate a Poisson measure on (Z, Z) with control µ. In other words, η is a collection of random variables defined on some probability space (Ω, F , P ), indexed by the elements of Z µ and such that: (i) for every B, C ∈ Z µ such that B ∩ C = ∅, the random variables η(B) and η(C) are independent; (ii) for every B ∈ Z µ , η(B) has a Poisson distribution with mean µ(B). We shall also write η(B) = η(B) -µ(B), B ∈ Z µ , and η = {η(B) : B ∈ Z µ }. A random measure verifying property (i) is usually called "completely random" or "independently scattered" (see e.g. [START_REF] Peccati | Wiener chaos: moments, cumulants and diagrams[END_REF] for a general introduction to these concepts).

Remark 1.1 As it is customary, by a slight abuse of notation, we shall often write x ∈ η in order to indicate that the point x ∈ Z is charged by the random measure η(•).

In this paper, we shall focus on sequences of random variables {F n : n 1} having a finite Wiener-Itô chaotic decomposition, that is, such that

F n = k i=1 I q i (f (n) i ), n 1, (1.1)
where the symbol I q i indicates a multiple Wiener-Iô integral of order q i with respect to η, the integer k does not depend on n, and each f

(n) i
is a non-zero symmetric kernel from Z q i to R (see Section 2.1 below for details). We will be specifically concerned with the forthcoming Problem 1.2. Recall that, given random variables U, Y ∈ L 1 (P ), the Wasserstein distance between the law of U and the law of Y is defined as the quantity

d W (U, Y ) = sup f ∈Lip(1) E[f (U )] -E[f (Y )] ,
where Lip(1) indicates the class of Lipschitz real-valued function with Lipschitz constant 1. It is well-known that the topology induced by d W , on the class of probability measures on the real line, is strictly stronger than the one induced by the convergence in distribution.

Problem 1.2 Find analytic conditions on the kernels {f (n) i } ensuring that the sequence

Fn := F n Var(F n ) , n 1,
converges in distribution, as n → ∞, to a standard Gaussian random variable N ∼ N (0, 1), in the sense of the Wasserstein distance. Determine under which assumptions these conditions are also necessary, and find explicit upper bounds for the sequence

d W ( Fn , N ), n 1.
We will deal with Problem 1.2 in Section 3, where it is shown that a convenient solution can be deduced by using contraction operators. Among other features, these operators provide a neat way to deal with the product of multiple stochastic integral, and virtually replace the use of diagram formulae -see e.g. [START_REF] Peccati | Wiener chaos: moments, cumulants and diagrams[END_REF]. As anticipated, we will see that, in the specific case of random variables as in (1.1) such that f (n) i 0, our results lead to necessary and sufficient conditions that are analogous to the so-called 'fourth moment theorems' for sequences of multiple integrals in a Gaussian setting -see [START_REF] Nualart | Central limit theorems for sequences of multiple stochastic integrals[END_REF].

Remark 1.3 Problem 1.2 is also explicitly studied in [START_REF] Reitzner | Central Limit Theorems for U-Statistics of Poisson Point Processes[END_REF]Section 4]. In particular, Theorem 4.1 in [START_REF] Reitzner | Central Limit Theorems for U-Statistics of Poisson Point Processes[END_REF] provides bounds in the Wasserstein distance for random variables having a finite chaotic decomposition, where the bounds are expressed in terms of expectations of inner products of multiple integral stochastic processes. On the other hand, Theorem 4.7 in [START_REF] Reitzner | Central Limit Theorems for U-Statistics of Poisson Point Processes[END_REF] provides an analytic bound, involving sums over partitions, for the normal approximation of absolutely convergent U -statistics. Here, we call 'analytic bound' any upper bound only involving deterministic transformations of the kernel determining the U -statistic, without any additional probabilistic component.

Random graphs

As anticipated, we shall now apply our main theoretical results to the study of geometric random graphs whose edge-counting statistics satisfy a CLT. The class of geometric random graphs considered below allow for long connections, in the sense that the geometric rule used to define edges is based on the use of arbitrarily large sets and therefore is not local. It is worth noting by now that our setting represents a natural generalization of the so called Gilbert graphs -see Example 1.5 below. Also, as explained in Remark 1.8 below, part of the models we consider cannot be dealt with by directly using the powerful theory of stabilization (see e.g. [START_REF] Kendall | New perspectives in stochastic geometry[END_REF]). Now let the notation introduced in the previous section prevail. In what follows, we shall denote by W (as in 'window') a measurable subset of Z such that µ(W ) < ∞. We first introduce the notion of a geometric random graph based on the restriction of the Poisson measure η to W , and on some symmetric set H ⊂ Z × Z.

Definition 1.4 (Random geometric graphs) Let H ⊂ Z × Z be such that µ 2 (H) < ∞, H
is symmetric (that is, for every (x, y) ∈ H, one also has (y, x) ∈ H) and H is non-diagonal (that is, H does not contain any pair of the type (x, x)).

(a) The random geometric graph based on η, W and H is the undirected random graph

G = G(η, W, H) = (V, E),
such that: (i) the vertices of G are given by the class V = η ∩ W = {x ∈ η : x ∈ W }, and (ii) a pair {x, y} belongs to the set E of the edges of G if and only if (x, y) ∈ H. We observe that, since H is non-diagonal, G has no loops, that is: G does not contain any edge of the type {x, x}.

(b) Assume in addition that Z is a vector space. The random geometric graph at Point (a) is said to be stationary if there exists a set H ⊂ Z such that

H = (x, y) ∈ Z 2 : x -y ∈ H .
Note that, since H is symmetric, one has necessarily that H = -H; moreover, since H has no diagonal components, 0 / ∈ H.

Example 1.5 (i)

The class of random geometric graphs introduced above generalizes the notion of a Gilbert graph, obtained by taking Z equal to some metric space (endowed with a distance d) and

H = (x 1 , x 2 ) ∈ Z 2 : 0 < d(x 1 , x 2 ) < δ , δ > 0. In this case, the random geometric graph G is obtained by connecting two vertices v 1 , v 2 ∈ η ∩ W if and only if d(v 1 , v 2 ) < δ. See e.g. [29]. (ii) If Z = R d and H = (x 1 , x 2 ) ∈ Z 2 : 0 < x 1 -x 2 R d < δ ,
then the corresponding geometric random graph is stationary with H = B(0, δ)\{0}, where B(0, δ) ⊂ Z stands for the open ball of radius δ centered at the origin. Graphs of this type are customarily called interval graphs when Z = R, and disk graphs when Z = R 2 -see e.g. [START_REF] Clark | Unit disk graphs[END_REF][START_REF] Decreusefond | Simplicial Homology of Random Configurations[END_REF][START_REF] Ferraz | Statistics of geometric random simplicial complexes[END_REF][START_REF] Mcdiarmid | Random channel assignment in the plane[END_REF][START_REF] Müller | Two-point concentration in random geometric graphs[END_REF] for recent developments on the subject.

In Section 4, we shall use our general results in order to deal with the following problem.

Problem 1.6 Fix a set W ⊂ Z, as well as a symmetric function g : W × W → R. Consider the following objects: (i) a collection of Poisson measures η λ , λ > 0, with σ-finite and non atomic control measures µ λ such that µ λ (W ) < ∞ and µ λ (W ) ↑ ∞, as λ → ∞, and (ii) a collection of non-diagonal non-negligible symmetric sets H λ ⊂ Z × Z, λ > 0. Characterize those classes {µ λ , H λ : λ > 0} such that the random variables

F (g, W ; η λ , H λ ) = {x,y}∈E λ g(x, y), λ > 0, (1.2)
(where G λ = (V λ , E λ ) is the geometric random graph based on η λ , W and H λ ) verify the limit relation

F (g, W ; η λ , H λ ) := F (g, W ; η λ , H λ ) -E[F (g, W ; η λ , H λ )] Var(F (g, W ; η λ , H λ )) Law -→ N ∼ N (0, 1), (1.3)
as λ → ∞.

Remark 1.7 (i) At this stage, the role of the window W might seem immaterial, and indeed the substance of Problem 1.6 does not change if one takes W = Z. However, the above formulation allows for the more general case of a window W = W λ possibly depending on λ. Moving windows of this type appear in Section 4, as well as in the paper [START_REF] Lachièze-Rey | Fine Gaussian fluctuations on the Poisson space II: rescaled kernels, marked processes and geometric U-statistics[END_REF].

(ii) In many examples and applications, one considers sets H λ such that α(H λ ∩(W ×W )) ↓ 0, as λ → ∞, for some fixed measure α on W × W . Heuristically, the fact that µ λ (W ) ↑ ∞ and α(H λ ∩ (W × W )) ↓ 0 ensures that the following phenomenon takes place: as λ grows, more and more vertices and edges are added to the geometric graph, whereas old edges are deleted as a consequence of the asymptotic negligibility of H λ ∩(W ×W ). Solving Problem 1.6 in this framework is equivalent to characterizing all sequences of random geometric graphs such that the addition of vertices and the cancellation of edges compensate, thus generating asymptotic Gaussian fluctuations.

When specialized to the case of Gilbert graphs on Z = R d , Problem 1.6 is tackled in the classic reference [START_REF] Penrose | Random Geometric Graphs[END_REF]Chapter 3] as a special case of general subgraph counting. A comparison with the results of [START_REF] Penrose | Random Geometric Graphs[END_REF]Chapter 3] is provided in Section 4.3.1 below. A complete solution of Problem 1.6 for general subgraph counting in Gilbert graphs, based on the techniques developed in this paper, is presented in [START_REF] Lachièze-Rey | Fine Gaussian fluctuations on the Poisson space II: rescaled kernels, marked processes and geometric U-statistics[END_REF]Section 3]. See also [START_REF] Reitzner | Central Limit Theorems for U-Statistics of Poisson Point Processes[END_REF]Section 6.2].

Remark 1.8 Assume that, for every x ∈ η, there exists a random radius R x such that all the y connected to x in the random graph lie in the ball with center x and radius R x . Then, the variable F = F (1, W ; η λ , H λ ) in (1.2) is stabilizing, meaning that F can be written in the form

F = x∈η ξ(x, η),
where ξ is such that ξ(x, η) is not modified by adding or removing a finite number of points to η outside the ball with center x and radius R x (see [START_REF] Kendall | New perspectives in stochastic geometry[END_REF] for more details on this topic). In our case, to fit the framework of formula (1.2) in the case g = 1, ξ(x, η) should be defined as

ξ(x, η) = 1 2 #({y = x : {x, y} ∈ E λ }),
where #A indicates the cardinality of A. The CLTs presented for instance in [START_REF] Barishnikov | Gaussian limits for random measures in geometric probability[END_REF][START_REF] Penrose | Normal approximation in geometric probability[END_REF] cover well this case. Remark that in this particular framework of a deterministic connection rule, stabilization theory only allows for a bounded length, while we consider here models where points can have arbitrarily long connections.

The rest of the paper is organized as follows. In Section 2, we discuss several background results concerning Poisson measures, Wiener chaos and U -statistics. Section 3 contains our main abstract results concerning the normal approximation of random variables having a finite chaotic decomposition. Section 4 focuses on random graphs and on several analytical characterizations of associated CLTs. An Appendix (see Section 5) provides some basic definitions and results of Malliavin calculus.

Preparation

Multiple integrals and chaos

As before, (Z, Z , µ) is a non-atomic Borel measure space, and η is a Poisson measure on Z with control µ.

Remark 2.1 By virtue of the assumptions on the space (Z, Z , µ), and to simplify the discussion, we will assume throughout the paper that (Ω, F , P ) and η are such that

Ω =    ω = n j=1 δ z j , n ∈ N ∪ {∞}, z j ∈ Z    ,
where δ z denotes the Dirac mass at z, and η is defined as the canonical mapping

(ω, B) → η(B)(ω) = ω(B), B ∈ Z µ , ω ∈ Ω.
Also, the σ-field F will be always supposed to be the P -completion of the σ-field generated by η.

Throughout the paper, for p ∈ [1, ∞), the symbol L p (µ) is shorthand for L p (Z, Z , µ). For an integer q 2, we shall write L p (µ q ) := L p (Z q , Z ⊗q , µ q ), whereas L p s (µ q ) stands for the subspace of L p (µ q ) composed of functions that are µ q -almost everywhere symmetric. Also, we adopt the convention L p (µ) = L p s (µ) = L p (µ 1 ) = L p s (µ 1 ) and use the following standard notation: for every q 1 and every f, g ∈ L 2 (µ q ), f, g L 2 (µ q ) = Z q f (z 1 , ..., z q )g(z 1 , ..., z q )µ q (dz 1 , ..., dz q ), f L 2 (µ q ) = f, f

1/2 L 2 (µ q ) .
For every f ∈ L 2 (µ q ), we denote by f the canonical symmetrization of f , that is,

f (x 1 , . . . , x q ) = 1 q! σ f (x σ(1) , . . . , x σ(q) ),
where σ runs over the q! permutations of the set {1, . . . , q}. Note that f L 2 (µ q ) f L 2 (µ q ) (to see this, use for instance the triangular inequality) . Definition 2.2 For every deterministic function h ∈ L 2 (µ), we write

I 1 (h) = η(h) = Z h(z)η(dz)
to indicate the Wiener-Itô integral of h with respect to η. For every q 2 and every f ∈ L 2 s (µ q ), we denote by I q (f ) the multiple Wiener-Itô integral, of order q, of f with respect to η. We also set I q (f ) = I q ( f ), for every f ∈ L 2 (µ q ) (not necessarily symmetric), and I 0 (b) = b for every real constant b.

The reader is referred for instance to the monograph [START_REF] Peccati | Wiener chaos: moments, cumulants and diagrams[END_REF], by Peccati and Taqqu, for a complete discussion of multiple Wiener-Itô integrals and their properties (including the forthcoming Proposition 2.3 and Proposition 2.4).

Proposition 2.3

The following equalities hold for every q, m 1, every f ∈ L 2 s (µ q ) and every g ∈ L 2

s (µ m ):

1. E[I q (f )] = 0, 2. E[I q (f )I m (g)] = q! f, g L 2 (µ q ) 1 (q=m) (isometric property).
The Hilbert space composed of the random variables with the form I q (f ), where q 1 and f ∈ L 2 s (µ q ), is called the qth Wiener chaos associated with the Poisson measure η. The following well-known chaotic representation property is an essential feature of Poisson random measures. Recall that F is assumed to be generated by η.

F = E[F ] + ∞ i=1 I i (f i ), (2.4)
where the series converges in L 2 (P ) and, for each i 1, the kernel f i is an element of L 2 s (µ i ).

Star contractions and multiplication formulae

We shall now introduce contraction operators, and succinctly discuss some of their properties.

As anticipated in the Introduction, these objects are at the core of our main results.

The kernel f l r g on Z p+q-r-l , associated with functions f ∈ L 2 s (µ p ) and g ∈ L 2 s (µ q ), where p, q 1, r = 1, . . . , p ∧ q and l = 1, . . . , r, is defined as follows:

f l r g(γ 1 , . . . , γ r-l , t 1 , , . . . , t p-r , s 1 , , . . . , s q-r ) (2.5) = Z l µ l (dz 1 , ..., dz l )f (z 1 , , . . . , z l , γ 1 , . . . , γ r-l , t 1 , , . . . , t p-r )
×g(z 1 , , . . . , z l , γ 1 , . . . , γ r-l , s 1 , , . . . , s q-r ).

Roughly speaking, the star operator ' l r ' reduces the number of variables in the tensor product of f and g from p + q to p + q -r -l: this operation is realized by first identifying r variables in f and g, and then by integrating out l among them. To deal with the case l = 0 for r = 0, . . . , p∧q, we set f 0 r g(γ 1 , . . . , γ r , t 1 , , . . . , t p-r , s 1 , , . . . , s q-r ) = f (γ 1 , . . . , γ r , t 1 , , . . . , t p-r )g(γ 1 , . . . , γ r , s 1 , , . . . , s q-r ), and f 0 0 g(t 1 , , . . . , t p , s 1 , , . . . , s q ) = f ⊗ g(t 1 , , . . . , t p , s 1 , , . . . , s q ) = f (t 1 , , . . . , t p )g(s 1 , , . . . , s q ). By using the Cauchy-Schwarz inequality, one sees immediately that f r r g is square-integrable for any choice of r = 0, . . . , p ∧ q , and every

f ∈ L 2 s (µ p ), g ∈ L 2 s (µ q ).
Remark 2.5 For every 1 p q and every r = 1, ..., p,

Z p+q-r (f 0 r g) 2 dµ p+q-r = Z r (f p-r p f )(g q-r q g)dµ r , (2.6)
for every f ∈ L 2 s (µ p ) and every g ∈ L 2 s (µ q ) The next statement contains an important product formula for Poisson multiple integrals (see e.g. [START_REF] Peccati | Wiener chaos: moments, cumulants and diagrams[END_REF] for a proof).

Proposition 2.6 (Product formula) Let f ∈ L 2 s (µ p ) and g ∈ L 2
s (µ q ), p, q 1, and suppose moreover that f l r g ∈ L 2 (µ p+q-r-l ) for every r = 1, . . . , p ∧ q and l = 1, . . . , r such that l = r. Then,

I p (f )I q (g) = p∧q r=0 r! p r q r r l=0 r l I p+q-r-l f l r g , (2.7)
with the tilde ∼ indicating a symmetrization, that is,

f l r g(x 1 , . . . , x p+q-r-l ) = 1 (p + q -r -l)! σ f l r g(x σ(1) , . . . , x σ(p+q-r-l) ),
where σ runs over all (p + q -r -l)! permutations of the set {1, . . . , p + q -r -l}.

About the Malliavin formalism

For the rest of the paper, we shall use definitions and results related to Malliavin-type operators defined on the space of functionals of the Poisson measure η. Our formalism coincides with the one introduced by Nualart and Vives in [START_REF] Nualart | Anticipative calculus for the Poisson process based on the Fock space[END_REF]. In particular, we shall denote by D, δ, L and L -1 , respectively, the Malliavin derivative, the divergence operator, the Ornstein-Uhlenbeck generator and its pseudo-inverse. The domains of D, δ and L are written domD, domδ and domL. The domain of L -1 is given by the subclass of L 2 (P ) composed of centered random variables. For the convenience of the reader we have collected some crucial definitions and results in the Appendix (see Section 5). Here, we just recall that, since the underlying probability space Ω is assumed to be the collection of discrete measures described in Remark 2.1, then one can meaningfully define the random variable ω → F z (ω) = F (ω + δ z ), ω ∈ Ω, for every given random variable F and every z ∈ Z, where δ z is the Dirac mass at z. One can therefore prove that the following neat representation of D as a difference operator is in order.

Lemma 2.7 For each F ∈ domD,

D z F = F z -F, a.e.

-µ(dz).

A complete proof of Lemma 2.7 can be found in [START_REF] Nualart | Anticipative calculus for the Poisson process based on the Fock space[END_REF].

U -statistics

Following [31, Section 3.1], we now introduce the concept of a U -statistic associated with the Poisson measure η.

Definition 2.8 (U -statistics) Fix k 1. A random variable F is called a U -statistic of order k, based on the Poisson measure η, if there exists a kernel f ∈ L 1 s (µ k ) such that F = (x 1 ,...,x k )∈η k = f (x 1 , ..., x k ), (2.8)
where the symbol η k = indicates the class of all k-dimensional vectors (x 1 , ..., x k ) such that x i ∈ η and x i = x j for every 1 i = j k. As made clear in [31, Definition 3.1], the possibly infinite sum appearing in (2.8) must be regarded as the L 1 (P ) limit of objects of the type

(x 1 ,...,x k )∈η k = ∩An f (x 1 , ..., x k ), n 1, where the sets A n ∈ Z k are such that µ k (A n ) < ∞ and A n ↑ Z k , as n → ∞.
Plainly, a U -statistic of order one is just a linear functional of η, with the form

x∈η f (x) = Z f (x)η(dx),
for some f ∈ L 1 (µ). The following statement, based on the results proved by Reitzner and Schulte in [START_REF] Reitzner | Central Limit Theorems for U-Statistics of Poisson Point Processes[END_REF], collects two crucial properties of U -statistics. Theorem 2.9 (See [START_REF] Reitzner | Central Limit Theorems for U-Statistics of Poisson Point Processes[END_REF]) Let F ∈ L 1 (P ) be a U -statistic as in (2.8). Then, the following two properties hold.

(a) The expectation of F is given by

E[F ] = Z k f (z 1 , ..., z k )µ k (dz 1 , ..., dz k ).
(2.9) (b) If F is also square-integrable, then necessarily f ∈ L 2 s (µ k ), and the Wiener-Itô representation (2.4) of F is such that f i = 0, for i k + 1, and

f i (x 1 , .., x i ) = k i Z k-i f (x 1 , ..., x i , z 1 , ..., z k-i ) µ k-i (dz 1 , ..., dz k-i ) (2.10
)

for every i = 1, ..., k. In particular, f k = f . For each i = 1, . . . , k, one has that f i ∈ L s (µ i ) ∩ L 2 s (µ i ).
One should note that formula (2.10) follows from an application of the results proved by Last and Penrose in [START_REF] Last | Poisson process Fock space representation, chaos expansion and covariance inequalities[END_REF].

U -statistics and random graphs

In this paper, we will be interested in characterizing the Gaussian fluctuations of U -statistics having a specific support. In particular this allows one to deal with the set of 'local U -statistics" introduced by Reitzner and Schulte in [31, Section 6]. Recall that a set H ∈ Z k is called symmetric if the following implication holds: if (x 1 , ..., x k ) ∈ H, then (x σ(1) , ..., x σ(k) ) ∈ H for every permutation σ of {1, ..., k}. Definition 2.10 (Support of a U -statistic) Let k 2, and let H ⊂ Z k be a measurable symmetric set. A U -statistic F as in (2.8) is said to have support in H if the function f is such that

f (x 1 , ..., x k ) = 0, ∀(x 1 , ..., x k ) / ∈ H.
Example 2.11 (Local U -statistics) Let Z be a metric space. Then, the class of local Ustatistics, as defined in [31, Section 6], coincides with the family of U -statistics having support in a set of the type H = (x 1 , ..., x k ) : diam({x 1 , ..., x k }) < δ for some δ > 0. Here, the symbol diam(B) is shorthand for the diameter of B.

We shall now point out a well-known connection between U -statistics and hypergraphs. Recall that a hypergraph of order k 2 is a pair (V, E), where V = (v 1 , ..., v m ) is a set of vertices, and E = (E 1 , ..., E s ) is a collection of (possibly non-disjoint) subsets of V (called edges), such that each E i contains exactly k elements; in particular a hypergraph of order 2 is an undirected graph.

Remark 2.12 (U -statistics as graph statistics) (i) Let k 2, let F be a U -statistic as in (2.8), and assume that f = 1 W k × 1 H , where W ⊂ Z is some set (usually called a 'window') such that µ(W ) < ∞. Then, the random variable 1 k! F counts the number of edges in the random hypergraph (V, E), obtained as follows: V = η ∩ W , and the class of edges E is composed of all subsets {x 1 , ...,

x k } ⊂ V such that (x 1 , ..., x k ) ∈ H. (ii) If k = 2, Z is some metric space (endowed with a distance d) and H = (x 1 , x 2 ) ∈ Z 2 : d(x 1 , x 2 ) < δ and f = 1 W × 1 H , then the random variable 1 2
F counts the number of edges in the undirected graph whose vertices V are given by the points of W charged by η and such that two vertices v 1 , v 2 are connected by an edge if and only if 0 < d(v 1 , v 2 ) < δ. These are the 'Gilbert random graphs' discussed in Example 1.5(i).

To conclude, we present the notion of a stationary U -statistic. It will play an important role in Section 4. Definition 2.13 (Stationary U -statistics) Fix k 2, assume that Z is a vector space, and let F be a U -statistic of the type (2.8), having support in a symmetric set H). We shall say that F is stationary if there exists H ⊂ Z k-1 such that

H = {(x 1 , ..., x k ) : (x 2 -x 1 , x 3 -x 1 , ..., x k -x 1 ) ∈ H}.
(2.11)

Example 2.14 Consider the case k = 2, Z = R d and H = (x 1 , x 2 ) ∈ Z 2 : x 1 -x 2 R d < δ .
Then, the corresponding U -statistic F is stationary, with H = B(0, δ), where B(0, δ) ⊂ Z stands for the open ball of radius δ centered at the origin. See Example 1.5(ii).

3 Normal approximations for finite chaotic expansions

Framework

We shall tackle Problem 1.2, by focussing on the normal approximation of random variables F having the form

F = E[F ] + k i=1 I q i (f i ), (3.12)
where:

k 1 is an integer;

-the integers q i , i = 1, ..., k, are such that 1 q 1 < q 2 < • • • < q k ; -the symbol I q indicates a multiple Wiener-Itô integral of order q, with respect to a centered Poisson measure η = η -µ, where η is a Poisson measure on the Borel measurable space (Z, Z ), with deterministic and σ-finite control measure µ;

-each kernel f i is a nonzero element of L 2 s (µ q i ), and the class {f i : i = 1, ..., k} verifies in addition the forthcoming Assumption 3.1. Assumption 3.1 (Technical assumptions on integrands) Let the notation of Section 2.2 prevail. Every random variable of the type (3.12) considered in the sequel of this paper is such that the following properties (i)-(iii) are verified.

(i) For every i = 1, ..., d and every r = 1, ...q i , the kernel

f i q i -r q i f i is an element of L 2 (µ r ).
(ii) For every i such that q i 2, every contraction of the type (z 1 , ...,

z 2q i -r-l ) → |f i | l r |f i |(z 1 , ..., z 2q i -r-l
) is well-defined and finite for every r = 1, ..., q i , every l = 1, ..., r and every (z 1 , ..., z 2q i -r-l ) ∈ Z 2q i -r-l .

(iii) For every i, j = 1, ..., d such that max(q i , q j ) > 1, for every k = |q i -q j | ∨ 1, ..., q i + q j -2 and every (r, l)

verifying k = q i + q j -2 -r -l, Z Z k (f i (z, •) l r f j (z, •)) 2 dµ k µ(dz) < ∞,
where, for every fixed z ∈ Z, the symbol f i (z, •) denotes the mapping (z 1 , ..., z q-1 ) → f i (z, z 1 , ..., z q-1 ). (a) for every 1 i < j k, for every r = 1, ..., q i ∧ q j and every l = 1, ..., r, the contraction f i l r f j is a well-defined element of L 2 (µ q i +q j -r-l );

(b) for every 1 i j k and every r = 1, ..., q i , f i 0 r f j is an element of L 2 (µ q i +q j -r );

(c) for every i = 1, ..., k, for every r = 1, ..., q i , and every l = 1, ..., r ∧ (q i -1), the kernel

f i l r f i is a well-defined element of L 2 (µ 2q i -r-l ).
In particular, the multiplication formula (2.7) implies that every random variable F verifying Assumption 3.1 is such that

I q i (f i ) 2 ∈ L 2 (P ) for every i = 1, ..., k, yielding in turn that E[F 4 ] < ∞.
Following a similar route, one can also show that, under Assumption 3.1, the random variable DF, -DL -1 F L 2 (µ) is square-integrable (and not merely an element of L 1 (P )).

Remark 3.3 Assumption 3.1 imply that Assumptions A-B-C in [START_REF] Peccati | Multi-dimensional Gaussian fluctuations on the Poisson space[END_REF] are verified, so that the computations therein can be directly applied in our framework.

A general bound

Let F be a random variable as in (3.12) such that E[F 2 ] = σ 2 > 0 (σ > 0) and E[F ] = m ∈ R, and consider a Gaussian random variable N ∼ N (m, σ 2 ) with the same mean and variance. Then, a slight modification of [26, Theorem 3.1] (the modification resides in the fact that we consider an arbitrary variance σ 2 ) yields the following estimates:

d W (F, N ) B 1 (F ; σ) B 2 (F ; σ), (3.13)
where

B 1 (F ; σ) = 1 σ E |σ 2 -DF, -DL -1 F L 2 (µ) | (3.14) + 1 σ 2 Z E[(D z F ) 2 |D z L -1 F |]µ(dz), B 2 (F ; σ) = 1 σ E (σ 2 -DF, -DL -1 F L 2 (µ) ) 2 (3.15) + 1 σ 2 Z E[(D z F ) 2 |D z L -1 F |]µ(dz).
The next statement shows that B 2 (F ; σ 2 ) can be further bounded in terms of the contractions introduced in Section 2.2. Theorem 3.5 Let F and N be the random variables appearing in (3.13)- (3.15). Then, there exists a universal constant C 0 = C 0 (q 1 , ..., q k ) ∈ (0, ∞), depending uniquely on q 1 , ..., q k , such that

B 2 (F ; σ) C 0 × B 3 (F ; σ), (3.16)
where

B 3 (F ; σ) (3.17) = 1 σ max 1 f i l r f i L 2 (µ 2q i -r-l ) + max 2 f i l r f j L 2 (µ q i +q j -r-l ) + max i=1,...,k f i 2 L 4 (µ q i ) .
In the previous expression, max 1 ranges over all 1 i k such that q i > 1, and all pairs (r, l) such that r ∈ {1, ..., q i } and 1 l r ∧ (q i -1), whereas max 2 ranges over all 1 i < j d and all pairs (r, l) such that r ∈ {1, ..., q i } and l ∈ {1, ..., r}. When

q 1 = 1, one can replace f 1 2 L 4 (µ)
in the previous bound by the smaller quantity

f 1 3 L 3 (µ) f 1 L 2 (µ) . ( 3

.18)

Proof of Theorem 3.5. Without loss of generality, we can assume that m = 0. Also, throughout this proof, we write

F i = I q i (f i ) and σ 2 i = E[I q i (f i ) 2 ] = q i ! f i 2 L 2 (µ q i ) , i = 1, ..., k, in such a way that σ 2 = E[F 2 ] = k i=1 E[F 2 i ] = k i=1 σ 2 i . Now write E (σ 2 -DF, -DL -1 F L 2 (µ) ) 2 k i=1 1 q i >1 E (σ 2 i -DF i , -DL -1 F i L 2 (µ) ) 2 + 1 i =j k E ( DF i , -DL -1 F j L 2 (µ) ) 2 ,
so that one can directly apply [27, Proposition 5.5] and deduce that there exists a constant a = a(q 1 , ..., q k ) such that

E (σ 2 -DF, -DL -1 F L 2 (µ) ) 2 a max 1 f i l r f i L 2 (µ 2q i -r-l ) + max 2 f i l r f j L 2 (µ q i +q j -r-l ) .
To conclude, observe that

Z E[(D z F ) 2 |D z L -1 F |]µ(dz) Z E   k i=1 |D z F i | 2 k i=1 |D z L -1 F i |   µ(dz),
so that [27, Proposition 5.6] implies that there exists a constant b = b(q 1 , ..., q k ) such that

Z E[(D z F ) 2 |D z L -1 F |]µ(dz) bσ max 1 f i l r f i L 2 (µ 2q i -r-l ) + max i=1,...,k f i 2 L 4 (µ q i ) .
Taking C 0 = a + b yields the desired conclusion. The last assertion in the statement comes from the fact that, when

q 1 = 1, Z E[(D z F ) 2 |D z L -1 F |]µ(dz) = f 1 3 L 3 (µ) .
Remark 3.6 According to [27, Lemma 2.9], for every quadruple (i, j, r, l) entering the expression of max 2 in (3.17), the following estimate holds:

f i l r f j 2 L 2 (µ q i +q j -r-l ) f i l r f i L 2 (µ 2q i -r-l ) × f j l r f j L 2 (µ 2q j -r-l ) . (3.19)

Estimates for positive kernels

We shall now specialize Theorem 3.5 to the case on random variables having the form (3.12) and such that f i 0. In particular, we shall unveil some useful connections between the quantity B 3 (F ; σ) and the fourth cumulant of F . Remark 3.7 Random variables admitting a Wiener-Itô chaotic expansion with positive kernels appear rather naturally in stochastic geometry. For instance, an application of (2.10) shows that any U -statistic with a positive kernel admits a Wiener-Itô chaotic expansion of this type. Note that many counting statistics have the form of U -statistics with an integer-valued (and therefore nonnegative) kernel -such as for instance the subgraph-counting statistics in random geometric graphs (see e.g. [START_REF] Penrose | Random Geometric Graphs[END_REF]Chapter 3] and the references therein), or the statistics associated with hyperplane tessellations considered in [START_REF] Heinrich | Central limit theorems for Poisson hyperplane tessellations[END_REF].

The following statement concerns random variables of the form (3.12), in the special case where E[F ] = 0, k = 1 and the multiple stochastic integral has a nonnegative kernel. Proposition 3.8 (Fourth moment bound, I) Consider a random variable F as in (3.12), with the special form F = I q (f ), q 1, where f 0 and

E[F 2 ] = q! f 2 L 2 (µ q ) = σ 2 > 0. Then, B 3 (F ; σ) = 1 σ max 1 f l r f L 2 (µ 2q-r-l ) + f 2 L 4 (µ q ) ,
and there exist universal constants c 1 = c 1 (q) < C 1 = C 1 (q), depending uniquely on q, such that

c 1 × B 3 (F ; σ) E[F 4 ] -3σ 4 C 1 × B 3 (F ; σ). (3.20)
Proof. Using the multiplication formula (2.7), together with (2.6) and the positivity assumptions on f , one sees that F 2 can be written in the following form

F 2 = σ 2 + I 2q (f 0 0 f ) + R,
where R is a random variable orthogonal to the constants and to I 2q (f 0 0 f ) and such that

J max 1 f l r f 2 L 2 (µ 2q-r-l ) + f 4 L 4 (µ q ) E[R 2 ] K max 1 f l r f 2 L 2 (µ 2q-r-l ) + f 4 L 4 (µ q ) ,
for some universal positive constants J, K depending uniquely on q. The conclusion is obtained by using the relation

E[I 2q (f 0 0 f ) 2 ] = (2q)! f 0 0 f 2 L 2 (µ 2q ) = 2σ 4 + q-1 p=1 q! 4 p! 2 (q -p)! 2 ! f p p f 2 L 2 (µ 2q-2p ) ,
where we have used [24, formula (11.6.30)].

The following general bound deals with random variables of the form (3.12) and with positive kernels. Proposition 3.9 (Fourth moment bound, II) Let F be as in (3.12), with k 1, and assume moreover that E[F ] = 0, and E[F 2 ] = σ 2 > 0, and f i 0 for every i. Then, there exists a universal constant C 2 = C 2 (q 1 , ..., q k ), depending uniquely on q 1 , ..., q k , such that max

1 f i l r f i L 2 (µ 2q i -r-l ) + max i=1,...,k f i 2 L 4 (µ q i ) C 2 E[F 4 ] -3σ 4 . (3.21)
Proof. Write as before F i = I q i (f i ), and

σ 2 i = E[F 2 i ], i = 1, ..., k.
We can now write

E[F 4 ] -3σ 4 = k i=1 {E[F 4 i ] -3σ 4 i } + 6 1 i<j k {E[F 2 i F 2 j ] -σ 2 i σ 2 j } + (i 1 ,i 2 ,i 3 ,i 4 )∈V d E[F i 1 F i 2 F i 3 F i 4 ] := W + Y + Z,
where V d stands for the collection of those (i 1 , i 2 , i 3 , i 4 ) ∈ {1, ..., k} 4 , such that one of the following conditions is satisfied: (a)

i 1 = i 2 = i 3 = i 4 , (b) i 1 = i 2 = i 3 = i 4 and i 4 = i 1 , (c)
the elements of (i 1 , i 2 , i 3 , i 4 ) are all distinct. Applying the multiplication formula (2.7) and exploiting the fact that each f i is nonnegative, we immediately deduce that Y 0 and Z 0, so that the desired conclusion follows from Proposition 3.8.

Conditions for asymptotic Gaussianity

This section contains a general statement (Theorem 3.12) about the normal approximation of random variables admitting a finite chaotic decomposition. The first part of such a result provides sufficient conditions for Central Limit Theorems, that are directly based on Theorem 3.5. As indicated in the subsequent parts, these conditions become necessary whenever the involved kernels are nonnegative. Theorem 3.12 is one of the main results of the paper, and is the main tool used to deduce the CLTs appearing in Section 4 and in [START_REF] Lachièze-Rey | Fine Gaussian fluctuations on the Poisson space II: rescaled kernels, marked processes and geometric U-statistics[END_REF].

More precisely, in what follows we shall fix integers k 1 and 1 q 1 < q 2 < ... < q k (not depending on n), and consider a sequence {F (n) : n 1} of random variables with the form

F (n) = k i=1 I q i (f (n) i ), n 1 (3.22)
each verifying the same assumptions as the random variable F appearing in (3.12) (in particular, Assumption 3.1 is satisfied for each n). We also use the following additional notation: (i)

σ 2 (n) = E[(F (n) ) 2 ], (ii) F (n) i = I q i (f (n) i ), i = 1, ..., d, and (iii) σ 2 i (n) = E[(F (n) i ) 2 ].
Remark 3.10 One of the main achievements of the forthcoming Theorem 3.12 is the 'fourth moment theorem' appearing at Point 3 in the statement, which only holds for random variables such that the kernels in the chaotic decomposition are nonnegative. As first proved in [START_REF] Nualart | Central limit theorems for sequences of multiple stochastic integrals[END_REF] (see also [START_REF] Nourdin | Normal approximations using Malliavin calculus: from Stein's method to universality[END_REF]Chapter 5]) an analogous result holds for general sequences of multiple Wiener-Itô integrals with respect to a Gaussian process. In particular, in the Gaussian framework one does not need to assume that the integrands have a constant sign. Proving analogous statements in a Poisson setting is quite a demanding task, one of main reasons being the rather intricate multiplication formula (2.7). Some previous partial findings in the Poisson case can be found in Peccati and Taqqu [START_REF] Peccati | Central limit theorems for double Poisson integrals[END_REF] (for sequences of double integrals) and in Peccati and Zheng [START_REF] Peccati | Universal Gaussian fluctuations on the discrete Poisson chaos[END_REF] (for sequences of multiple integrals having the form of homogeneous sums).

Remark 3.11

In the statement of Theorem 3.12, we implicitly allow that the underlying Poisson measure η also changes with n. In particular, one can assume that the associated control measure µ = µ n explicitly depends on n. This general framework is needed for the geometric applications developed in Section 4.

Theorem 3.12 Let {F (n) } be a sequence of random variables as in (3.22), and assume that there exists σ 2 > 0 such that lim n→∞ σ 2 (n) = σ 2 . Let N ∼ N (0, σ 2 ).

1.

For every n, one has the estimate

d W (F (n) , N ) C 0 × B 3 (F (n) ; σ(n)) + 2/π σ(n) ∨ σ |σ 2 (n) -σ 2 |. (3.23)
In particular, if B 3 (F (n) ; σ(n)) → 0, as n → ∞, then d W (F (n) , N ) → 0 and therefore

F (n) Law → N .

Assume that f

(n) i 0 for every i, n. Then, a sufficient condition in order to have that

B 3 (F (n) ; σ(n)) → 0 is that E[(F (n) ) 4 ] -3σ 4 (n) → 0.

Assume that f

(n) i 0 for every i, n, and also that the sequence (F (n) ) 4 , n 1, is uniformly integrable. Then, the following conditions (a)-(c) are equivalent, as n → ∞: (a)

d W (F (n) , N ) → 0, (b) B 3 (F (n) ; σ(n)) → 0, and (c) E[(F (n) ) 4 ] -3σ 4 (n) → 0. Proof. 1. Let N n ∼ N (0, σ 2 (n)), n 1.
Then, one has that (see e.g. [19, Proposition 3.6.1])

d W (N n , N ) 2/π σ(n) ∨ σ |σ 2 (n) -σ 2 |,
so that the desired conclusion follows from Theorem 3.5 as well as the inequality

d W (F (n) , N ) d W (F (n) , N n ) + d W (N n , N ). 2. If E[(F (n) ) 4 ] -3σ 4 (n) → 0, then relation (3.21) implies that max 1 f (n) i l r f (n) i L 2 (µ 2q i -r-l ) + max i=1,...,k f (n) i 2 L 4 (µ q i ) → 0.
Using (3. [START_REF] Nourdin | Normal approximations using Malliavin calculus: from Stein's method to universality[END_REF], we see that the last relation implies that B 3 (F (n) ; σ(n)) → 0, so that the desired conclusion follows from Point 1 in the statement.

3. In view of Point 1 and Point 2 in the statement, we shall only prove that (a) ⇒ (c). To prove this implication, just observe that 4 , so that the conclusion follows from the fact that σ 2 (n) → σ 2 . Remark 3.13 A sufficient condition in order to have that the sequence {(F (n) ) 4 } is uniformly integrable is the following: there exists some > 0 such that

F (n) Law → N and {(F (n) ) 4 } is uniformly integrable, then necessarily E[(F (n) ) 4 ] → E[N 4 ] = 3σ
sup n 1 E|F (n) | 4+ < ∞.
We shall use some estimates taken from [START_REF] Peccati | Multi-dimensional Gaussian fluctuations on the Poisson space[END_REF] (see, in particular, Table 2, p. 1505, therein). Given a thrice differentiable function ϕ : R k → R, we set

ϕ ∞ = max 1 i 1 i 2 k sup x∈R k ∂ 2 ∂x i 1 ∂x i 2 ϕ(x) . ϕ ∞ = max 1 i 1 i 2 i 3 k sup x∈R k ∂ 3 ∂x i 1 ∂x i 2 ∂x i 3 ϕ(x) .
Proposition 3.14 Let the assumptions and notation of Theorem 3.12 prevail, and suppose that B 3 (F (n) ; σ) → 0, as n → ∞. Let N n,i ∼ N (0, σ 2 i (n)), i = 1, ..., k, Then, for every thrice differentiable function ϕ : R k → R, such that ϕ ∞ , ϕ ∞ < ∞, one has that

E[ϕ(F (n) 1 , ..., F (n) k )] -E[ϕ(N n,1 , ..., N n,k )] -→ 0, n → ∞.
Proof. According to [START_REF] Peccati | Multi-dimensional Gaussian fluctuations on the Poisson space[END_REF], the following estimate takes place:

|E[ϕ(F (n) 1 , ..., F (n) k )] -E[ϕ(N n,1 , ..., N n,k )]| k 2 ϕ ∞ k i,j=1 E[(σ 2 i (n)1 i=j -DF i , -DL -1 F j L 2 (µ) ) 2 ] + 1 4 ϕ ∞ Z E   k i=1 |D z F i | 2 k i=1 |D z L -1 F i |   µ(dz),
so that the conclusion follows from (3.16).

4 Edge-counting in random geometric graphs: from Gaussian fluctuations to clustering

Framework

Our aim is now to tackle Problem 1.6. Throughout this section we shall work under the following slightly more restrictive setting (we use the notation of Problem 1.6).

-For every λ > 0, the control measure of η λ is µ λ (dx) = λ × θ(dx), where θ is a σ-finite non-atomic measure on (Z, Z ).

-The symmetric function g : W × W → R is bounded (this assumption can be relaxedsee the discussion below).

In the forthcoming Section 4.2, we will show that the normal approximation of the random variables F (g, W ; η λ , H λ ) (as defined in (1.2)) can be completely characterized in terms of some diagonal restrictions of Cartesian products of the sets H λ . Among several consequences, this remarkable phenomenon implicitly provides a new geometric interpretation of contraction operators.

Definition 4.1 (Sets with diagonal restrictions) Given the sets H λ , λ > 0, defining the random variables F (g, W ; η λ , H λ ) and F (g, W ; η λ , H λ ), respectively in (1.2) and (1.3), we define the following four sets -H

(1)

λ := {(x 1 , x 2 , x 3 ) ∈ Z 3 : (x 1 , x 2 ) ∈ H λ , (x 1 , x 3 ) ∈ H λ } ⊂ Z 3 ; -H (2) λ := {(x 1 , x 2 , x 3 , x 4 , x 5 ) ∈ Z 5 : (x 1 , x i ) ∈ H λ , ∀i = 2, ..., 5} ⊂ Z 5 ; -H (3) λ = {(x 1 , x 2 , x 3 , x 4 ) ∈ Z 4 : (x 1 , x 2 ) ∈ H λ , (x 2 , x 3 ) ∈ H λ , (x 3 , x 4 ) ∈ H λ , (x 4 , x 1 ) ∈ H λ } ⊂ Z 4 ; -H (4) λ := {(x 1 , x 2 , x 3 , x 4 , x 5 ) ∈ Z 5 : (x 1 , x 2 ) ∈ H λ , (x 2 , x 3 ) ∈ H λ , (x 3 , x 4 ) ∈ H λ , (x 4 , x 5 ) ∈ H λ } ⊂ Z 5 .
We shall also use the following quantities, defined for every λ > 0:

(i) V 2 λ (g) = V 2 1,λ (g) + V 2 2,λ (g) := 4λ 3 W 3 ∩H (1) λ g 0 1 g(x 1 , x 2 , x 3 )θ 3 (dx 1 , dx 2 , dx 3 ) + 2λ 2 W 2 ∩H λ g 2 (x 1 , x 2 )θ 2 (dx 1 , dx 2 ); (ii) A λ (g) = λ 5/2 W 5 ∩H (2) λ 5 i=2 g(x 1 , x i )θ 5 (dx 1 , ..., dx 5 ); (iii) B λ (g) = λ 2 W 4 ∩H (3) λ g(x 1 , x 2 )g(x 3 , x 4 )g(x 1 , x 4 )g(x 2 , x 3 )θ 4 (dx 1 , ..., dx 4 ); (iv) C λ (g) = λ 3/2 W 3 ∩H (1) λ g 2 (x 1 , x 2 )g 2 (x 1 , x 3 )θ 3 (dx 1 , dx 2 , dx 3 ); (v) D λ (g) = λ W 2 ∩H λ g 4 (x 1 , x 2 )θ 2 (dx 1 , dx 2 ); (vi) E λ (g) = λ 5/2 W 5 ∩H (4) λ g(x 1 , x 2 )g(x 1 ,
x 3 )g(x 2 , x 4 )g(x 3 , x 5 )θ 5 (dx 1 , ..., dx 5 ).

The following expressions are obtained by setting g = 1:

(i') V 2 λ (1) = V 2 1,λ (1) + V 2 2,λ (1) = 4λ 3 θ(W 3 ∩ H (1) λ ) + 2λ 2 θ 2 (W 2 ∩ H λ ); (ii') A λ (1) = λ 5/2 θ 5 (W 5 ∩ H (2) λ ); (iii') B λ (1) = λ 2 θ 4 (W 4 ∩ H (3) λ ); (iv') C λ (1) = λ 3/2 θ 3 (W 3 ∩ H (1)
λ );

(v') D λ (1) = λ θ 2 (W 2 ∩ H λ ); (vi') E λ (1) = λ 5/2 θ 5 (W 5 ∩ H (4) λ ).

General conditions and bounds

We start with a general estimate.

Theorem 4.2 (General bound for geometric graphs) Let the previous assumptions and notation prevail, and let N ∼ N (0, 1). Then, there exists a universal constant C, not depending on λ, such that, for every λ > 0,

d W ( F (g, W ; η λ , H λ ), N ) C 0 V 2 λ (g) × max{A λ (g), B λ (g), C λ (g), D λ (g), E λ (g)}. (4.24)
If the class { F (g, W ; η λ , H λ ) 4 : λ > 0} is uniformly integrable, then the RHS of (4.24) converges to zero, as λ → ∞, if and only if the CLT (1.3) takes place.

Proof. In what follows, we write F λ = F (g, W ; η λ , H λ ) and F λ = F (g, W ; η λ , H λ ) to simplify the notation. Last and Penrose's formula (2.10) implies that the random variable F λ admits the following chaotic decomposition

F λ = E[F λ ] + I 1 (f 1,λ ) + I 2 (f 2,λ ) := E[F λ ] + F 1,λ + F 2,λ , (4.25)
where

f 1,λ (x) = 2λ Z 1 {H λ ∩W ×W } (x, y)g(x, y)θ(dy) and f 2,λ (x 1 , x 2 ) = 1 H λ ∩(W ×W ) (x 1 , x 2 )g(x 1 , x 2 ).
Routine computations imply then that

V 2 i,λ (g) = Var(F i,λ ), i = 1, 2. (4.26)
It follows that

F λ = I 1 (f 1 /V λ (g)) + I 2 (f 2 /V λ (g)).
The upper bound (4.24) is now obtained by using (3.17), as well as the following relations, that can be proved by a standard use of the Fubini Theorem:

4A λ (g) = f 1,λ 2 L 4 (µ λ ) , B λ (g) = f 2,λ 1 1 f 2,λ L 2 (µ 2 λ ) , C λ (g) = f 2,λ 1 2 f 2,λ L 2 (µ λ ) , D λ (g) = f 2,λ 2 L 4 (µ 2 λ ) , 2E λ (g) = f 1,λ 1 1 f 2,λ L 2 (µ λ ) .
The last assertion in the statement follows from a direct application of Theorem 3.12.

2

The next two statements provide simplified bounds in case one of the two elements of the chaotic decomposition of F (g, W ; η λ , H λ ) converges to zero, as λ → ∞. The proof (which is standard and left to the reader) uses (4.26) as well as the following basic estimate: if Q, R, S are three random variables in L 1 (P ), then

d W (Q + R, S) d W (R, S) + E[|Q|]. Proposition 4.3 (Dominating first chaos) If V 2,λ (g) V 1,λ (g) → 0, as λ → ∞, (4.27)
then there exists a constant C 1 , independent of λ, such that, for λ large enough,

d W ( F (g, W ; η λ , H λ ), N ) C 1 V 2,λ (g) V 1,λ (g) + 1 V 2 1,λ (g)
× max{A λ (g)} .

(4.28)

If the class { F (g, W ; η λ , H λ ) 4 : λ > 0} is uniformly integrable, then the RHS of (4.28) converges to zero, as λ → ∞, if and only if the CLT (1.3) takes place.

Proposition 4.4 (Dominating second chaos)

If V 1,λ (g) V 2,λ (g) → 0, as λ → ∞, (4.29)
then there exists a constant C 2 , independent of λ, such that, for λ large enough,

d W ( F (g, W ; η λ , H λ ), N ) C 2 V 1,λ (g) V 2,λ (g) + 1 V 2 2,λ (g) × max{B λ (g), C λ (g), D λ (g))} . (4.30)
If the class { F (g, W ; η λ , H λ ) 4 : λ > 0} is uniformly integrable, then the RHS of (4.30) converges to zero, as λ → ∞, if and only if the CLT (1.3) takes place.

Edge counting in stationary graphs

For the rest of the section, we fix an integer d 1. For every λ > 0, we define the set

Q λ = [-1 2 λ 1/d , 1 2 λ 1/d ] d
. We now specialize the framework of the previous two sections to the following setting

Z = R d , W = Q 1 , g = 1, µ λ = λ , (4.31)
where is the Lebesgue measure on R d . We shall assume that, for every λ > 0, the symmetric non-diagonal set H λ has the form

H λ = {(x, y) : x -y ∈ H λ },
for some set H λ verifying

(H λ ∩ Q 1 ) > 0. (4.32)
Remark 4.5 We insist that the novelty here (with respect to the usual setting of disk graphs -see e.g. [29, Chapter 3] and the references therein) is that H λ need not be bounded, allowing for arbitrarily distant points to be connected. This is especially relevant whenever

H λ = α λ H 1 ,
where α λ is a scaling factor and H 1 is a fixed unbounded geometric connection rule. Unlike in the classical literature of stochastic geometry, e.g. in stabilization theory, this allows for models with unbounded interactions, such as between distant particles. As already recalled, our approach is further applied in [START_REF] Lachièze-Rey | Fine Gaussian fluctuations on the Poisson space II: rescaled kernels, marked processes and geometric U-statistics[END_REF], where U -statistics with general stationary kernels (not only taking values 0 or 1), and general order k 2, are considered.

For every λ > 0, we shall write

F λ = F (1, Q 1 ; η λ , H λ ) and F λ = F (1, Q 1 ; η λ , H λ ), (4.33)
where we used the notation introduced in (1.2)- (1.3). With this notation, each 1 2 F λ is a stationary U -statistic (see Definition 2.13), counting the number of edges in the stationary random graph based on H λ (see Definition 1.4). The chaotic decomposition of F λ is written

F λ = E[F λ ] + F 1,λ + F 2,λ ,
where we have adopted the same notation as in (4.25). Since g = 1, Problem 1.6 becomes the following: characterize all collections of sets {H λ } such that the CLT (1.3) takes place, and assess the rate of convergence in the Wasserstein distance.

Remark 4.6 For every λ > 0, one has the equality in law

F λ Law = x,y∈η∩Q λ ,x =y 1 x-y∈G λ , λ > 0, (4.34)
where η is a random Poisson measure with Lebesgue intensity, and G λ is a measurable subset of R d defined by the relation

H λ = λ -1/d G λ , (4.35)
so that

(G λ ∩ Q λ ) > 0. (4.36)
Remark 4.7 (Asymptotic equivalence notation) Given two mappings λ → γ λ , λ → δ λ , we write γ λ δ λ if there are two positive constants C, C > 0 such that Cγ λ δ λ C γ λ for λ sufficiently large. We write γ λ ∼ δ λ if δ λ > 0 for λ sufficiently large and α λ /δ λ → 1.

One of the main points developed in the present section is that the asymptotic Gaussianity of the class { F λ } results can be effectively studied by using the occupation coefficient of H λ , defined as

ψ(λ) := (H λ ∩ Q 1 ) = (G λ ∩ Q λ ) (Q λ ) , λ > 0. (4.37)
We also write

Ŵ = W -W = Q 2 d and W = Q 1/2 d (this is the largest set such that W -W ⊆ W ) and define, for λ > 0, ψ(λ) := (H λ ∩ W ) = (G λ ∩ Q λ/2 d ) (Q λ ) , λ > 0, (4.38)
ψ(λ) := (H λ ∩ Ŵ ) = (G λ ∩ Q 2 d λ ) (Q λ ) , λ > 0. (4.39)
In order to obtain necessary and sufficient conditions for asymptotic normality, we will often work under the additional assumption that

ψ(λ) ψ(λ). (4.40)
In this case, one has trivially that ψ(λ) ψ(λ) ψ(λ), and the value of ψ is only relevant up to a fixed multiplicative constant. Remark 4.8 (O-regularity) Assume that the geometric rule defined by G λ does not depend on λ, i.e.: G λ = G for some fixed measurable set G, in such a way that each set H λ is obtained by rescaling G by a factor λ -1/d . Then, condition (4.40) is implied by the following stronger assumption: ψ(aλ) ψ(λ) for every a > 0. In the terminology of [3, Section 2.2], this is equivalent to saying that ψ is O-regular.

In view of using the bounds appearing in Theorem 4.2, we have the following crucial estimates: Theorem 4.9 Let the previous notation and assumption prevail, set

V i,λ (1) = V i,λ , i = 1, 2, as well as A λ = A λ (1), B λ = B λ (1), . . . , E λ = E λ (1) -see Section 4.1.
The following estimates are in order for every fixed λ > 0:

2 -d ψ(λ) λ -2 V 2 2,λ = 2λ -2 D 2 λ 2 d ψ(λ), 2 -d ψ(λ) 2 λ -3 V 2 1,λ = λ -3 C 2 λ 2 d ψ(λ) 2 , 2 -d ψ(λ) 4 λ -5 A 2 λ 2 d ψ(λ) 4 , λ -4 B 2 λ 2 d ψ(λ) 3 , 2 -d ψ(λ) 4 λ -5 E 2 λ 2 d ψ(λ) 4 .
Proof. We introduce the changes of variables denoted by ϕ (i) , i = 0, 1, 2, 3, 4, where

ϕ (0) (x 1 , x 2 ) = (x 1 , u = x 1 -x 2 ), ϕ (1) (x 1 , x 2 , x 3 ) = (x 1 , u = x 1 -x 2 , v = x 1 -x 3 ), ϕ (2) (x 1 , x 2 , x 3 , x 4 , x 5 ) = (x 1 , u = x 1 -x 2 , v = x 1 -x 3 , w = x 1 -x 4 , z = x 1 -x 5 ), ϕ (3) (x 1 , x 2 , x 3 , x 4 ) = (x 1 , u = x 1 -x 2 , v = x 2 -x 3 , w = x 3 -x 4 ), ϕ (4) (x 1 , x 2 , x 3 , x 4 , x 5 ) = (x 1 , u = x 1 -x 2 , v = x 2 -x 3 , w = x 3 -x 4 , z = x 4 -x 5 ).
Using the notation introduced in Definition 4.1 we have

(W 2 ∩ H λ ) = W 2 1 x 1 -x 2 ∈H λ dx 1 dx 2 = ϕ (0) (W 2 )
1 u∈H λ dx 1 du,

(W 3 ∩ H (1) λ ) = W 3 1 x 1 -x 2 ∈H λ 1 x 1 -x 3 ∈H λ dx 1 dx 2 dx 3 = ϕ (1) (W 3 ) 1 u∈H λ 1 v∈H λ dx 1 dudv, (W 5 ∩ H (2) λ ) = W 5 1 x 1 -x 2 ∈H λ 1 1 x 1 -x 3 ∈H λ 1 x 1 -x 4 ∈H λ 1 x 1 -x 5 ∈H λ dx 1 dx 2 dx 3 dx 4 dx 5 = ϕ (2) (W 5 ) 1 u∈H λ 1 v∈H λ 1 w∈H λ 1 z∈H λ dx 1 dudvdwdz, (W 4 ∩ H (3) λ ) = W 4 1 x 1 -x 2 ∈H λ 1 x 2 -x 3 ∈H λ 1 x 3 -x 4 ∈H λ 1 x 4 -x 1 ∈H λ dx 1 dx 2 dx 3 dx 4 = ϕ (3) (W 4 ) 1 u∈H λ 1 v∈H λ 1 w∈H λ 1 u+v+w∈H λ dx 1 dudvdw, (W 5 ∩ H (4)
λ ) = W 5 1 x 1 -x 2 ∈H λ 1 x 2 -x 3 ∈H λ 1 x 3 -x 4 ∈H λ 1 x 4 -x 5 ∈H λ dx 1 dx 2 dx 3 dx 4 dx 5 = ϕ (4) (W 5 ) 1 u∈H λ 1 v∈H λ 1 w∈H λ 1 z∈H λ dx 1 dudv.
Using the inclusions 4 and the result follows.

W 2 ⊆ ϕ (0) (W 2 ) ⊆ Ŵ 2 , W 3 ⊆ ϕ (1) (W 3 ) ⊆ Ŵ 3 , W 5 ⊆ ϕ (2) (W 5 ) ⊆ Ŵ 5 , ϕ (3) (W 4 ) ⊆ Ŵ 4 , W 5 ⊆ ϕ (4) (W 5 ) ⊆ Ŵ 5 , and
1 u∈H λ 1 v∈H λ 1 w∈H λ 1 u+v+w∈H λ 1 u∈H λ 1 v∈H λ 1 w∈H λ , u, v, w ∈ R d , we have 2 ( W × (H λ ∩ W )) = 2 -d ψ(λ) λ -2 V 2 2,λ 2 ( Ŵ × (H λ ∩ Ŵ )) = 2 d ψ(λ) 3 ( W × (H λ ∩ W ) 2 ) = 2 -d ψ(λ) 2 λ -3 C 2 λ 3 ( Ŵ × (H λ ∩ Ŵ ) 2 ) = 2 d ψ(λ) 2 5 ( W × (H λ ∩ W ) 4 ) = 2 -d ψ(λ) 4 λ -5 A 2 λ 5 ( Ŵ × (H λ ∩ Ŵ ) 4 ) = 2 d ψ(λ) 4 λ -4 B 2 λ 4 ( Ŵ × (H λ ∩ Ŵ ) 3 ) = 2 d ψ(λ) 3 5 ( W × (H λ ∩ W ) 4 ) = 2 -d ψ(λ) 4 λ -5 E 2 λ 5 ( Ŵ × (H λ ∩ Ŵ ) 4 ) = 2 d ψ(λ)
The next statement provides one of the main results of this section: it gives an exhaustive characterization of the asymptotic behavior of F λ , whenever (4.40) is in order. In order to allow for a comparison with the existing literature, we classify the asymptotic behavior of F λ according to four regimes, denoted by (R1)-(R4). Such a classification is based on the proportion ψ(λ) of space occupied by H λ in the observation window, determining the influence area of a given point of the Poisson measure. This coefficient has to be compared with λ -1 , which corresponds to the total window measure divided by the mean number of points. The four regimes are the following:

(R1) λψ(λ) → 0 and λ ψ(λ) → ∞; (R2) λψ(λ) → ∞; (R3) (Thermodynamic regime) λψ(λ) 1;
(R4) The mapping λ → λ ψ(λ) is bounded.

The thermodynamic regime corresponds (after rescaling) to the usual models where the geometry of the interactions does not change as the window of observation grows to the whole space (see Remark 4.6). We will see in Section 4.3.1 that, when specialized to Poissonized disk graphs, our asymptotic approximations and variance estimates concur with those obtained in [START_REF] Penrose | Random Geometric Graphs[END_REF]Chapter 3]. Under regimes (R2) and (R3), there is asymptotic normality with convergence at speed λ -1/2 in the Wasserstein distance. Under (R1) the convergence to the normal law is slower, and under (R4) the asymptotic normality is lost: for any converging subsequence the limit is either Poisson or zero. Remark 4.10 One interesting contribution of Theorem 4.11 appears at the end of Point (ii), where it is stated that, under the thermodynamic regime, both chaotic projections of the random variable Fλ contributee to the limit and satisfy a joint CLT. This kind of phenomenon is an example of the "fine Gaussian fluctuations" appearing in the title of the paper. Theorem 4.11 Let {H λ : λ > 0} be a family of subsets of R d satisfying (4.32) and let ψ, ψ be defined according to (4.38)-(4.39). Assume in addition that (4.40) is satisfied, and consider a random variable N ∼ N (0, 1). The quantities introduced in Section 4.1 satisfy the following relations: there exist constants 0 < k < K < ∞, independent of λ, such that

V 2 1,λ V 2 2,λ λψ(λ), 1 V 2 1,λ
A λ λ -1/2 , and

k max(λ -1/2 , (λ 2 ψ(λ)) -1/2 , λ 1/2 ψ(λ)) 1 V 2 2,λ max(B λ , C λ , D λ , E λ ) K max( ψ(λ), λ -1/2 , (λ 2 ψ(λ)) -1/2 , λ 1/2 ψ(λ))).
Furthermore, one can choose K in such a way that the following properties (i)-(iii) are verified.

(i) (Regime (R2)) If λψ(λ) → ∞, the first chaos projection F 1,λ dominates and

Var(F 1,λ ) ∼ Var(F λ ) λ 3 ψ(λ) 2 → ∞, and
d W ( Fλ , N ) K λ -1/2 . (ii) (Regime (R3)) If λψ(λ) 1, Var(F λ ) Var(F 1,λ ) Var(F 2,λ ) λ, and
d W ( Fλ , N ) K λ -1/2 .
In this case one has also that, as λ → ∞, the pair

F 1,λ Var(F 1,λ ) 1/2 , F 2,λ Var(F 2,λ ) 1/2 ,
converges in distribution to a two-dimensional Gaussian vector (N 1 , N 2 ), such that N i ∼ N (0, 1) and N 1 , N 2 are independent.

(iii) (Regimes (R1) and (R4)) If λψ(λ) → 0, then the second chaos projection F 2,λ dominates,

Var(F λ ) ∼ Var(F 2,λ ) λ 2 ψ(λ), and
d W ( Fλ , N ) K λ ψ(λ) .
Moreover, one has that Fλ converges in distribution to N if and only if λ 2 ψ(λ) → ∞ (or, equivalently, Var(F λ ) → ∞).

Proof of Theorem 4.11. Theorem 4.2 and assumption (4.40) yield

V 2 2,λ = 2D 2 λ λ 2 ψ(λ) V 2 1,λ = C 2 λ λ 3 ψ(λ) 2 A 2 λ λ 5 ψ(λ) 4 B 2 λ 2 d λ 4 ψ(λ) 3 E 2 λ λ 5 ψ(λ) 4 .
(i) We assume λψ(λ) → ∞. Applying (4.24), one deduces that

d W ( F , N ) 1 V 2 1,λ max(A λ , B λ , C λ , D λ , E λ ) K √ λ λ 3 ψ(λ) 2 max(λ 2 ψ(λ) 2 , λ 3/2 ψ(λ) 3/2 , λψ(λ), λ 1/2 ψ(λ) 1/2 ) K √ λ
for λ large enough. Notice that (4.28) does not yield a better bound because ψ(λ) 1.

(ii) Applying again (4.24), the conclusion is deduced from Point (i), because λψ(λ) c for some constant c > 0 and for λ large enough. The last statement at Point (ii) follows from an application of Proposition 3.14.

(iii) Using (4.24) again yields

d W ( F , N ) 1 λ 2 ψ(λ) max(λ 5/2 ψ(λ) 2 , λ 2 ψ(λ) 3/2 , λ 3/2 ψ, λψ(λ) 1/2 ) K λ ψ(λ)
for λ large enough, because λψ(λ) → 0. To conclude the proof, we have to show that, if λ 2 ψ(λ) does not diverge to infinity, then Fλ does not converge in distribution to N .

To prove this negative result, one could apply the product formula (2.7) to prove that, whenever λ 2 ψ(λ) is not diverging to infinity and is bounded away from zero, there exists a sequence λ n , n 1, such that λ n → ∞ and sup n E[ F 6 λn ] < ∞, so that the desired conclusion is deduced from the last part of Theorem 4.2 (the case when λ 2 ψ(λ) is not bounded away from zero can be dealt with by a direct argument). However, the statement of the forthcoming Theorem 4.14 is much stronger, and it is therefore not necessary to spell out the details of these computations. Corollary 4.12 Assume that the geometric rule defined by G λ (see (4.35)) does not depend on λ, in such a way that G λ = G for some fixed measurable set G. Assuming (4.40) (see Remark 4.8), one has that Fλ converges in distribution to N ∼ N (0, 1), with a rate at most of the order λ -1/2 with respect to d W .

Proof. We are in one of the following situations:

1. If G has finite positive Lebesgue measure, ψ(λ) ψ(λ) (G)/ (Q λ ) λ -1
. It corresponds to the case (ii) in Theorem 4.11, meaning the two chaoses codominate. It follows that Fλ converges to the normal law with a rate at most of the order of λ -1/2 with respect to d W .

2. If G does not have finite measure, λψ(λ) (G ∩ Q λ ) → ∞ and we are in the situation of Point (i) of Theorem 4.11, that is: the first chaos dominates. We therefore deduce that d W ( Fλ , N ) Kλ -1/2 , for some K > 0, and the conclusion follows.

As announced, we shall now deal more thoroughly with the case where λ 2 ψ(λ) does not diverge to infinity. In the proof of the next statement we shall use the following notation: if X is a random variable with finite moments of every order, then we write {χ m (X) : m 1} to indicate the sequence of its cumulants (see [START_REF] Peccati | Wiener chaos: moments, cumulants and diagrams[END_REF]Chapter 3] for an introduction to this concept). For instance, χ 1 (X) = E[X], χ 2 (X) = Var(X), and so on.

Remark 4. [START_REF] Last | Moments and central limit theorems for some multivariate Poisson functionals[END_REF] The proof of Theorem 4.14 provided below is based on diagram formulae and the method of moments and cumulants. An alternate proof could be deduced from the classic results by Silverman and Brown [START_REF] Silverman | Short Distances, Flat Triangles and Poisson Limits[END_REF], combined with a Poissonization argument. Another proof of this result, complete with explicit bounds in the total variation distance, appears in [START_REF] Peccati | The Chen-Stein method for Poisson functionals[END_REF]. The proof provided below has the merit of illustrating an application of diagram formulae (that are typically used to deduce CLTs) to a non-central result. In particular, the family { F λ } does not verify a CLT as λ → ∞.

Proof. Since Var(F λ ) ∼ Var(F 2,λ ) λ 2 ψ(λ), Point (i) is immediately deduced from the Bolzano-Weierstrass theorem. Point (ii) follows from a direct application of Campbell's Theorem (see [START_REF] Schneider | Stochastic and integral geometry[END_REF]Theorem 3.1.3]), yielding that, as n → ∞,

E[F λn ] Var(F λn ) 1/2 λ n ψ(λ n ) → 0.
We shall prove Point (iii) by using the method of cumulants. First of all, we observe that since λ 2 n ψ(λ n ) is bounded and bounded away from zero, one has that V 2 1,λn λ 3 n ψ(λ n ) 2 → 0, that is: as n → ∞, the limits of F 2,λn and F λn -E[F λn ] coincide. We recall that the law of the random variable X = 2P (c/2) is determined by its moments or, equivalently, by its cumulants (see e.g. [24, pp. 42-43]). Standard computations imply that χ 1 (X) = 0 and, for every m 2, χ m (X) = 2 m-1 c. We are therefore left to show that, for every m 3,

χ m (I 2 (f 2,λn )) -→ 2 m-1 c, ( 4
Φ(x 1 , ...., x 2m ) = f 2,λ (x 1 , x 2 ) × f 2,λ (x 3 , x 4 ) × • • • × f 2,λ (x 2m-1 , x 2m ),
given by the juxtaposition of m copies of f 2,λ , and (2) identify two variables x i , x j in the argument of Φ if and only if i and j are in the same block of π. According to [START_REF] Peccati | Wiener chaos: moments, cumulants and diagrams[END_REF]Corollary 7.4.1], one has therefore that

χ m (I 2 (f 2,λn )) = π∈Mm λ |π| n (R d ) |π| (f 2,λn ) π d |π| ,
where the symbol M m stands for the class of those partitions π of

λ |π| n (R d ) |π| (f 2,λn ) π d |π| = f 2,λn 2 L 2 ((λn ) 2 ) -→ c.
On the other hand, if π ∈ M m and |π| 3, a change of variables analogous to the ones defined in the proof of Theorem 4.9 yields that, for some constant C independent of n,

0 λ |π| n (R d ) |π| (f 2,λn ) π d |π| C λ |π| n ψ(λ n ) |π|-1 = C λ 2 n ψ(λ n ) × (λ n ψ(λ n )) |π|-2 → 0,
thus concluding the proof.

Two examples

We now present some explicit examples. The notation of Section 4.3 will prevail throughout this section. for some r λ > 0, meaning that two points of η in Q λ are connected whenever their distance is smaller than r λ . It yields ψ(λ) r d λ /λ (it is easy to verify that (4.40) is satisfied). Then Fλ is asymptotically normal iff λr d λ → ∞, and

d W ( Fλ , N ) Cλ -1/2 max(1, r -d/2 λ
).

According to the classification based on the four regimes (R1)-(R4), the above result yields the following exhaustive description of the asymptotic behavior of F λ (note how we are able to distinguish the contribution of each chaotic projection) :

(R1) If r λ → 0 and λr d λ → ∞, then Var(F λ ) λr d λ , Fλ satisfies a CLT with an upper bound of the order of (λr d λ ) -1/2 on the Wasserstein distance, and the projection of Fλ on the second Wiener chaos dominates in the limit.

(R2) If r λ → ∞ , then Var(F λ ) λ(r d λ ) 2
, Fλ satisfies a CLT with an upper bound of the order of λ -1/2 on the Wasserstein distance, and the projection of Fλ on the first Wiener chaos dominates.

(R3) If r λ 1, then Var(F λ ) λ, Fλ satisfies a CLT with an upper bound of the order of λ -1/2 on the Wasserstein distance, and the projections of Fλ on the first and second Wiener chaos both contribute to the limit and satisfy a joint CLT.

(R4) If λr d λ converges to a finite constant c 0, then F λ converges either to zero (if c = 0) or to a multiple of a Poisson random variable (if c > 0). Remark 4.16 Explicit estimates on the variances and on the rates of convergence to normal in the Wasserstein distance for edge counting statistics are also provided in [START_REF] Reitzner | Central Limit Theorems for U-Statistics of Poisson Point Processes[END_REF]Theorem 6.3]. Their variance estimates are of the order

max(λ 3 δ 2d λ , λ 2 δ d ) = max(λ 3 ψ(λ) 2 , λ 2 ψ(λ)),
corresponding exactly to our findings (δ λ = λ -1/d r λ = ψ(λ) 1/d in their notation). They obtained convergence to the normal law if δ λ → 0 and λ 4/3 δ d λ → ∞, whereas Example 4.15 yields a CLT whenever λ 2 ψ(λ) → ∞, dealing with the cases lim sup λ δ λ > 0 and λ -2/d = o(δ λ ), δ λ λ -4/(3d) , and gives a negative answer if δ λ Cλ -2/d for some C > 0.

Remark 4.17 For every fixed λ, the U -statistic 1 2 F λ has the same law as the random variable counting the number of edges in a disk graph, with radius δ λ = λ -1/d r λ , based on random points of the form {Y 1 , ..., Y N (λ) }, where {Y i } indicates a collection of i.i.d. random variables uniformly distributed on Q 1 = [-1 2 , 1 2 ] d , and N (λ) is an independent Poisson random variable with parameter λ. As such, each 1 2 F λ is just a subgraph counting statistic based on a Poissonized random geometric graph, and enters the general framework of [START_REF] Penrose | Random Geometric Graphs[END_REF]Section 3.4], where general m-dimensional CLTs are obtained for these objects. It is immediately checked that our variance estimates coincide with those stated in [29, p. 56] (for the case k = 2), whereas our estimates in the Wasserstein distance refine the findings of [29, Theorems 3.9 and 3.10] (in the case k = 2 and m = 1), where no information on the rate of convergence is given. Previous references for CLTs for Poissonized disk graphs are [START_REF] Bhattacharya | A class of U -statistics and asymptotic normality of the number of k-clusters[END_REF][START_REF] Jammalamadaka | Limit theorems for a triangular scheme of U -statistics with applications to inter-point distances[END_REF], where no explicit rates of convergence are provided either. A generalization of the previously described findings to general subgraph counting in a disk graph model can be found in [START_REF] Lachièze-Rey | Fine Gaussian fluctuations on the Poisson space II: rescaled kernels, marked processes and geometric U-statistics[END_REF]Section 3]. (c) If f (x) = 1/x 2 , α λ = λ -1/4 , then λψ(λ) λ -1/2 , whence there is a CLT with an upper bound of the order of λ -1/4 (Situation (iii) of Theorem 4.11), see Fig. 2c.

(d) If f (x) = 1/x, α λ = λ -1/2 , then λψ(λ) log(λ)λ -1 , whence there is a CLT with an upper bound of the order of log(λ) -1 (Situation (iii) of Theorem 4.11), see Fig. 2d.

(e) f (x) = 1/x 2 , α λ = λ -1/2 . According to Theorem 4.14, Fλ converges in distribution to a multiple of a Poisson random variable, see Fig. 2e.

In all cases, the convergence to a normal law goes hand in hand with the almost sure convergence of the number of connections to infinity, and with the convergence of the variance to infinity. In the case (d), the convergence is very slow, the number of connections behaves asymptotically like a Poisson law with parameter log(λ), due to the long-range connections within the point process. In the case (e), the asymptotic properties of G λ do not yield long range connections and the number of connections converges towards a Poisson-type limit. We now define some Malliavin-type operators associated with a Poisson measure η, on the Borel space (Z, Z ), with non-atomic control measure µ. We follow the work by Nualart and Vives [START_REF] Nualart | Anticipative calculus for the Poisson process based on the Fock space[END_REF].

The derivative operator D.

For every F ∈ L 2 (P ), the derivative of F , DF is defined as an element of L 2 (P ; L 2 (µ)), that is, of the space of the jointly measurable random functions u : Ω × Z → R such that E Z u 2 z µ(dz) < ∞.

Definition 5.1 1. The domain of the derivative operator D, written domD, is the set of all random variables F ∈ L 2 (P ) admitting a chaotic decomposition (2.4) such that

k 1 kk! f k 2 L 2 (µ k ) < ∞,
2. For any F ∈ domD, the random function z → D z F is defined by

D z F = ∞ k 1 kI k-1 (f k (z, •)).
The divergence operator δ.

Thanks to the chaotic representation property of η, every random function u ∈ L 2 (P, L 2 (µ)) admits a unique representation of the type

u z = ∞ k 0 I k (f k (z, •)), z ∈ Z, (5.42)
where the kernel f k is a function of k+1 variables, and f k (z, •) is an element of L 2 s (µ k ). The divergence operator δ(u) maps a random function u in its domain to an element of L 2 (P ). Definition 5.2

1. The domain of the divergence operator, denoted by domδ, is the collection of all u ∈ L 2 (P, L 2 (µ)) having the above chaotic expansion (5.42) satisfied the condition:

k 0 (k + 1)! f k 2 L 2 (µ ( k+1)) < ∞.
2. For u ∈ domδ, the random variable δ(u) is given by

δ(u) = k 0 I k+1 ( fk ),
where fk is the canonical symmetrization of the k + 1 variables function f k .

As made clear in the following statement, the operator δ is indeed the adjoint operator of D. The proof of Lemma 5.3 is detailed e.g. in [START_REF] Nualart | Anticipative calculus for the Poisson process based on the Fock space[END_REF].

The Ornstein-Uhlenbeck generator L.

Definition 5.4

1. The domain of the Ornstein-Uhlenbeck generator, denoted by domL, is the collection of all F ∈ L 2 (P ) whose chaotic representation verifies the condition:

k 1 k 2 k! f k 2 L 2 (µ k ) < ∞
2. The Ornstein-Uhlenbeck generator L acts on random variable F ∈ domL as follows:

LF = - k 1 kI k (f k ).
The pseudo-inverse of L. Definition 5.5

1. The domain of the pseudo-inverse of the Ornstein-Uhlenbeck generator, denoted by L -1 , is the space L 2 0 (P ) of centered random variables in L 2 (P ). I k (f k ) ∈ L 2 0 (P ) , we set

For F =

L -1 F = - k 1 1 k I k (f k ).

Proposition 2 . 4 (

 24 Wiener-Itô chaotic decomposition) Every random variable F ∈ L 2 (Ω, F , P ) := L 2 (P ) admits a (unique) chaotic decomposition of the type

Remark 3 . 2

 32 According to [27, Lemma 2.9 and Remark 2.10], Point (i) in Assumption 3.1 implies that the following properties (a)-(c) are verified:

Remark 3 . 4

 34 For instance, Assumption 3.1 is verified whenever each f i is a bounded function with support in a rectangle of the type B × • • • × B, where µ(B) < ∞.

Theorem 4 . 14 (

 414 Poisson approximations) Let the assumptions and notation of Theorem 4.11 prevail, and assume in addition that λψ(λ) → 0 and the mapping λ → λ 2 ψ(λ) does not diverge to infinity, as λ → ∞. Then, there exists a sequence {λ n } such that lim n→∞ λ n = ∞ and the following properties (i)-(iii) hold. (i) lim n→∞ Var(F λn ) = lim n→∞ Var(F 2,λn ) = 2c, where c is a nonnegative constant possibly depending on the sequence {λ n }, and we have used the notation (4.25). (ii) If c = 0, then E[| Fλn |] → 0, as n → ∞. (iii) If c > 0, then F 2,λn , and therefore F λn -E[F λn ], converges in distribution to X = 2P (c/2), as n → ∞, where P (c/2) indicates a centered Poisson random variable with parameter c/2.

  [2m] satisfying the following properties: (a) every block of π contains at least two elements, (b) given any two blocks b 0 ∈ π 0 and b 1 ∈ π, the intersection b 0 ∩ b 1 contains at most one element, and (c) the diagram Γ(π 0 , π), as defined in [24, Section 4.1], is connected in the sense of [24, p. 47]. There are exactly 2 m-1 partitions π ∈ M m such that |π| = 2, and for any such partition one has that

Example 4 . 15 (

 415 Disk graph) Assume G λ = B(0, r λ )

Example 4 . 18

 418 We present here examples of geometric stationary graphs with arbitrarily long connections and behaviors spanning the whole spectrum of possibilities indicated in Theorem 4.11. In all cases, condition (4.40) is easily checked. We define G ⊆ R 2 as in Fig.1, symmetric with respect to all axes, and consider different choices for f , a monotone function R * + → R * + . We set G λ = α λ G with different values for α λ > 0. We refer the reader to Fig.2for results of simulations, where different values for λ have been used.(a) If f (x) = 1/x, α λ = 1, then λψ(λ) log(λ), whence there is a CLT with an upper bound of the order of λ -1/2 (Situation (i) of Theorem 4.11), see Fig.2a.(b) If f (x) = 1/x 2 , α λ = 1, then λψ(λ) 1,whence there is a CLT with an upper bound of the order of λ -1/2 (Situation (ii) of Theorem 4.11), see Fig.2b.

Figure 1 :

 1 Figure 1: General form of G λ = {(x, y) : |y| < |f (x)| and |x| < |f (y)|}.

Figure 2a :

 2a Figure 2a: λ = 25, λ = 150

Lemma 5 . 3 (

 53 Integration by parts) For every G ∈ domD and u ∈ domδ, one has that E[Gδ(u)] = E[ DG, u L 2 (µ) ].

k 1

 1

  .41) where f 2,λ is the kernel appearing in formula(4.25). Our proof of (4.41) is based on the use of the so-called 'diagram formulae' for multiple Poisson integrals as stated in[START_REF] Peccati | Wiener chaos: moments, cumulants and diagrams[END_REF] Corollary 7.4.1] (observe that this statement only deals with simple kernels: however, one can immediately extend this result to our framework by using e.g. Surgailis[37, Theorem 3.1]). Fix m 3, and introduce the following notation and definitions. We shall write [2m] = {1, 2, ..., 2m} and indicate by π 0 the partition of [2m] given by π 0 = {{1, 2}, {3, 4}, ..., {2m -3, 2m -2}, {2m -1, 2m}}. Given a partition π of [2m], we write |π| to indicate the number of blocks of π. The function (f 2,λ ) π , in |π| variables, is obtained as follows: (1) consider the function


Jónathan Heras
email: jonathan.heras@unirioja.es

Maxime Dénès
email: maxime.denes@inria.fr

Gadea Mata
email: gadea.mata@unirioja.es

Anders Mörtberg
email: mortberg@chalmers.se

María Poza
email: maria.poza@unirioja.es

Vincent Siles
email: siles@chalmers.se

Towards a certified computation of homology groups for digital images *

In this paper we report on a project to obtain a verified computation of homology groups of digital images. The methodology is based on programming and executing inside the COQ proof assistant. Though more research is needed to integrate and make efficient more processing tools, we present some examples partially computed in COQ from real biomedical images.

Introduction

The discipline of Algebraic Digital Topology, or more specifically, the computation of homology groups from digital images is mature enough (see, for instance, [START_REF] Ziou | Generating Cubical Complexes from Image Data and Computation of the Euler number[END_REF], one among many good references) to go one step further and investigate the possibility of a certified computation (i.e., formally verified by proving correctness using an interactive proof assistant) in digital topology, as it happens in other areas of computer mathematics (see [START_REF] Gonthier | Formal proof -The Four-Color Theorem[END_REF]).

In a very rough manner, the process to be verified is reflected in Figure 1. Putting it into words, from the black pixels of a monochromatic image a simplicial complex is obtained (by means of a triangulation procedure); subsequently, from the simplicial complex, its boundary (or incidence) matrices are constructed, and finally, homology can be computed. If we work with coefficients over a field (and it is well-known that it is enough to take as coefficients the field /2 , when we work with 2D and 3D digital images) and if only the dimensions of the homology groups (as vector spaces) are looked for, then having a program able to compute the rank of a matrix is sufficient to accomplish the whole task. This architecture is particularized in this paper with a real problem that appeared in an industrial application and with the COQ proof assistant as programming and verifying tool.

The rest of this paper is organized as follows. Section 2 is devoted to present an example, coming from the biomedical context, as a test-case for our formal development. The formalization process is explained in Section 3, focusing on the link between boundary matrices and homology groups. Section 4 explains how the certified programs can be used to effectively compute homology of images. A way to deal with the management of the huge matrices produced by biomedical images is presented in Section 5. The paper ends with a section of Conclusions and Further work, and the bibliography.

Motivation

When developing formal proofs, a major issue is ensuring that concepts are defined in a way that will be applicable to concrete use. In our case, we are developing a general theory of effective simplicial homology as part of the Formath project [START_REF]ForMath: formalisation of mathematics[END_REF]. We decided to validate our design choices on biomedical digital images obtained from synaptical structures.

Synapses are the points of connection between neurons. The relevance of synapses comes from the fact that they are related to the computational capabilities of the brain.

The possibility of changing the number of synapses may be an important asset in the treatment of neurological diseases, such as Alzheimer, see [START_REF] Selkoe | Alzheimer's disease is a synaptic failure[END_REF]. Therefore, we can claim that an efficient, reliable and automatic method for counting synapses is instrumental in the study of the evolution of synapses in scientific experiments.

Up to now, the method to count synapses was manual, see [START_REF] Cuesto | Phosphoinositide-3-Kinase Activation Controls Synaptogenesis and Spinogenesis in Hippocampal Neurons[END_REF]. This was impractical since it implies a considerable time investment. In order to improve this process, a plug-in called SynapCountJ [START_REF] Mata | SynapsCountJ. University of La Rioja[END_REF] for the ImageJ environment [START_REF] Rasband | ImageJ: Image Processing and Analysis in Java[END_REF] has been developed.

The procedure implemented in this software to handle neuron images can be split into two steps. First, taking as input three images of a neuron, namely the neu- Then the second step consists in counting the connected components of the bitmap. A detailed explanation of the procedure was given in [START_REF] Heras | Homological processing of biomedical digital images: automation and certification[END_REF].

To test the suitability of this program, biologists consider, on the one hand, control cultures and, on the other hand, cultures under the effect of some drugs; in this way, the evolution of the density of the occurrence of synapses under the effect of those drugs can be determined. For instance, using the chemical inhibitor GSK3, the evolution percentage manually obtained is 36% and the one obtained with SynapCountJ is 36.6%. Thus, the experimental results obtained with SynapCountJ were considered (by the biologists) very satisfactory.

The former step of the procedure implemented in SynapCountJ, the extraction of a bitmap with the synapses from three images of the neurons, is carried out based on solid previous experience of experimental scientists; therefore, they consider it as a safe process. The latter step, the computation of connected components, can be solved with many algorithms and is an interesting test case for our framework where we can compute the homology in dimension 0 of such images. This is a well known procedure to measure the amount of connected components of an image, even if more elementary methods are also applicable. tion of the third point, the computation of homology groups from the boundary matrices.

In our formalization, we have used the COQ proof assistant [START_REF]The COQ Proof Assistant Reference Manual[END_REF]. This system provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. In addition, we take advantage of the features included in SSREFLECT [START_REF] Gonthier | A Small Scale Reflection Extension for the Coq system[END_REF], an extension for COQ whose development was started by G. Gonthier during the formal proof of the Four Color Theorem [START_REF] Gonthier | Formal proof -The Four-Color Theorem[END_REF]. The SSRE-FLECT libraries include enough ingredients to undertake the task of defining and computing homology from matrices. Some details of the proofs will be omitted; the interested reader can consult the original and complete source code at http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ProofExamples.

First of all, we define the notion of homology in COQ. Let K be a field, V 1, V 2, V 3 vector spaces on K, and f : V 1 → V 2, g : V 2 → V 3 linear applications; then, the Homology of f , g is the quotient between the kernel of g and the image of f . This is translated into COQ in the following way.

Variable (K : fieldType) (V1 V2 V3 : vectType K) (f : linearApp V1 V2) (g : linearApp V2 V3). Definition Homology := ((lker g) :\: (limg f)).

Nevertheless, we do not usually work with linear applications when trying to compute homology but with the matrices representing those linear applications. In particular, as we are working on a field K, given two matrices with coefficients in this field, let us called them, mx f and mx g of sizes v1×v2 and v2×v3 respectively and such that their product is the null matrix, the dimension of the corresponding homology vector space is given by the formula: v2 -r ank(mx g) -r ank(mx f ). This definition is introduced in COQ as follows.

Definition dim_homology (mxf:'M

[K]_(v1,v2)) (mxg:'M[K]_(v2,v3)) := v2 -\rank mxg -\rank mxf.
Now, the correctness of dim_homology can be shown by proving that given two matrices mxf and mxg whose product is the null matrix (mxf *m mxg = ), then the result obtained using dim_homology is the dimension of the homology group associated with the linear applications defined from mxf and mxg ((LinearApp mxf ) and (LinearApp mxg)).

Lemma dimHomologyrankE: mxf *m mxg = -> \dim Homology (LinearApp mxf) (LinearApp mxg) = dim_homology mxf mxg.

However the use of SSREFLECT libraries may trigger heavy computations during deduction steps, that would not terminate within a reasonable amount of time. To handle this issue, some definitions like matrices are locked in a way that do not allow direct computations.

To overcome this pitfall, we use the matrix representation and the rank algorithm developed in [START_REF] Cohen | Smith Normal form and executable rank for matrices[END_REF] to define ex_homology which takes as argument two such Finally, we prove the correctness of ex_homology by showing its equivalence to dim_homology up to a change of representation (this domain transformation is given by seqmx_of_mx).

0 1 2 3 5 4         (0, 1) (0, 2) (1, 2) (1, 3) (4, 5) (0) 1 1 0 0 0 (1) 1 0 1 1 0 (2) 0 1 1 0 0 (3) 0 0 0 1 0 (4) 0 0 0 0 1 (5) 0 0 0 0 1        

Lemma ex_homology_rankE (mxf: 'M[K]_(w1,w2)) (mxg : 'M[K]_(w2,w3)) :

ex_homology (seqmx_of_mx mxf) (seqmx_of_mx mxg) = dim_homology mxf mxg.

Then, we have an executable program to compute homology, for any dimension, whose correctness has been verified in COQ; therefore, we can claim that its results will always be correct.

Computing homology with COQ

An example is presented in this section in order to clarify how we can compute homology groups in COQ. Let us consider the simplicial complex of the left side of Figure 3. If we impose a lexicographical order on the simplices of the same dimension of this simplicial complex, its boundary matrix in dimension 1 is the one presented in the right side of Figure 3; it is worth noting that the rest of boundary matrices are empty, in particular we do not consider the empty set as an element of dimension -1.

The procedure to compute the homology (note that it only makes sense to compute homology in dimensions 0 and 1) of the simplicial complex of Figure 3 Eventually, we can compute the homology using the following instructions.

Eval vm_compute in (ex_homology 6 5 d _ex1 d1_ex1). Eval vm_compute in (ex_homology 6 5 d1_ex1 d2_ex1).

obtaining 2 and 1 respectively. In the same way, we could compute homology from the boundary matrices associated with the simplicial complex generated from a digital image. However, if we try to compute the homology from the images produced by SynapCountJ (see Figure 2), COQ is not able to handle those images yet, due to the size of data involved.

It is worth noting that COQ is a Proof Assistant and not a Computer Algebra system. Efficient implementations of mathematical algorithms running inside COQ is an ongoing effort, as shown by recent works on efficient real numbers [START_REF] Krebbers | Computer certified efficient exact reals in coq[END_REF], machine integers and arrays [START_REF] Armand | Extending coq with imperative features and its application to SAT verification[END_REF] or a previous approach to compiled execution of internal computations [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF].

We devise a couple of ways to achieve better efficiency:

• Improve the runtime system using the extraction mechanism which translates COQ code to a functional programming language like OCAML or Haskell. However, this would not allow us to reuse the result of our homological computations for further proofs. Indeed, output of external programs are untrusted so they cannot be imported. Instead, we are using a recent intermediate approach consisting in internally compiling COQ terms to OCAML with performance comparable to extracted code [START_REF] Boespflug | Full reduction at full throttle[END_REF].

• Optimize algorithms and representations using sparse matrices, which is well suited to simplicial complexes obtained from digital images. We have developed an Haskell implementation of such an algorithm but we still need to formally verify its correctness.

In the next section we describe another method to overcome the efficiency drawback, based on reducing the size of matrices while keeping the same homological information.

Computing discrete vector fields

The method that we are using for the reduction process is based on Discrete Morse Theory [START_REF] Forman | Morse theory for cell complexes[END_REF]; namely, we work in the algebraic setting of this theory which was described in [START_REF] Romero | Discrete Vector Fields and Fundamental Algebraic Topology[END_REF]. Roughly speaking, the aim of Discrete Morse Theory consists of finding simplicial collapses which transform a simplicial complex into a smaller one but keeping its homological properties. In this context, the instrumental tool are admissible discrete vector fields which allows one to reduce the amount of information removing "useless" information but keeping the homological properties of the original object.

The use of these techniques from Discrete Morse Theory has been welcomed in the study of homological properties of digital images, see [START_REF] Cazals | Molecular shape analysis based upon Morse-Smale complex and the Connolly function[END_REF][START_REF] Gyulassy | A practical approach to Morse-Smale complex computation: Scalability and generality[END_REF][START_REF] Jerse | Tracking features in image sequences using discrete Morse functions[END_REF], for instance. This is due to the fact that the size of the cellular object associated with an image can be huge, but the choice of an appropriate vector field can produce a much smaller object.

So, the question now is given a cellular complex how we can produce a vector field as large as possible (the larger the vector field, the smaller the reduced object). Several approaches to solve this problem have been studied as can be seen in [START_REF] Robins | Theory and algorithms for constructing discrete Morse complexes from grayscale digital images[END_REF][START_REF] Harker | The Efficiency of a Homology Algorithm based on Discrete Morse Theory and Coreductions[END_REF][START_REF] Real | Towards Optimality in Discrete Morse Theory through Chain Homotopies[END_REF][START_REF] Molina-Abril | A homological-based description of subdivided nD objects[END_REF], the strategy that we have chosen was explained in [START_REF] Romero | Discrete Vector Fields and Fundamental Algebraic Topology[END_REF]. It is not the aim of this paper to describe that algorithm (from now on, called RS's algorithm; RS stands for Romero-Sergeraert); but, we just introduce some ideas. This algorithm takes as input one of the boundary matrices associated with the cellular complex and provides an admissible discrete vector field (subsequently, from the matrix and the vector field a reduced matrix can be obtained).

The algorithm has been implemented in Haskell; and, some remarkable results have been obtained in the reduction process. As benchmark to test our programs, we have considered matrices coming from, on the one hand, 500 randomly generated images; and, on the other hand, biomedical images. In the former case, the size of the matrices was initially around 100 × 300, and after the reduction process the average size was 5 × 50. Using the original matrices COQ takes around 12 seconds to compute their rank; on the contrary, using the reduced matrices COQ only needs milliseconds. In the latter case, the matrices coming from biomedical images, the size of matrices is reduced from around 690 × 1400 to 97 × 500. In this case, COQ cannot deal with the original matrices; on the contrary, it is able to handle matrices as the ones obtained after applying the reduction programs and compute the results in, approximately, 25 seconds.

As a final remark, let us explain the main reason for using Haskell to implement the RS algorithm. The use of this language is due to the fact that Haskell is quite close to COQ; and, therefore, algorithms implemented in Haskell can be verified using COQ, a question which is, as we have seen, instrumental in our developments. In particular, the formalization of the correctness of the algorithm in charge of constructing an admissible discrete vector field given a matrix is on-going work; and, up to now, we have certified that our programs build a discrete vector field. The proof of the admissibility property remains as further work.

Conclusions and further work

In this paper, we have presented how we can use Algebraic Topology techniques to study biomedical images in a reliable manner. The first step consists in processing the biomedical images to obtain an image where homological information is as explicit as possible. Subsequently, using programs whose correctness has been verified in the COQ/SSREFLECT proof assistant, homological properties from the pre-processed image are obtained, which in turn are interpreted as features of the original image.

This methodology has been applied in this paper to the problem of determining the number of synapses of a neuron. In this case, the problem is reduced to measure the number of connected components of a monochromatic image. An issue which can be solved, even if it is not the straightforward manner, thanks to the computation of the homology group in dimension 0 of the image. The use of certified tools able to compute homology groups will be important in the future; for instance, to recognize the structure of a neuron; a problem which seems to involve the homology group in dimension 1, see [START_REF] Mrozek | Homological methods for extraction and analysis of linear features in multidimensional images[END_REF]. Other techniques, like the ones of persistent homology, could be applied in stacks of neurons to remove the noise of the images and help to the detection of the dendrites (the branches of the neuron).

Some formalization aspects also remain as future work. We have already mentioned the on-going work around proving the correctness of the admissible discrete vector fields programs. Moreover, certifying the correctness of integer homology computation is also further work (some results about the formalization of the Smith Normal Form are already encoded in COQ, see [START_REF] Cohen | Smith Normal form and executable rank for matrices[END_REF]).

As we previously mentioned, we are still working on efficiency issues but switching to better representations and more efficient algorithms will not require to redo the proofs related to homology.

Figure 1 :

 1 Figure 1: Computing homology from a digital image

Figure 2 :

 2 Figure 2: Example of the results produced by SynapCountJ

Figure 3 :

 3 Figure 3: Simplicial complex and its boundary matrix

  is as follows. Firstly, we define the boundary matrices. Definition d _ex1 := [::]. Definition d1_ex1 := [::[::1;1; ;

Verification in COQ/SSREFLECTIn the introduction we have explained a method, based on simplicial homology, to study the homology of a digital image which consists of: (1) building a simplicial complex from the image, (2) generating the boundary matrices associated with the simplicial complex, and (3) computing the homology from the boundary matrices.The correctness of the programs in charge of both the construction of a simplicial complex from an image and the generation of the boundary matrices associated with a simplicial complex have been formally proved using proof assistant tools as can be seen in[START_REF] Node | From Digital Images to Simplicial Complexes: A report[END_REF] and[START_REF] Heras | Incidence simplicial matrices formalized in Coq/SSReflect[END_REF] respectively. Then, there only remains the verifica-

* Partially supported by Ministerio de Educación y Ciencia, project MTM2009-13842-C02-01, and by the European Union's 7th Framework Programme under grant agreement nr. 243847 (ForMath).