Sophie Tourret

Pascal Fontaine

Daniel El Ouraoui

Haniel Barbosa

Lifting congruence closure with free variables to λ-free higher-order logic via SAT encoding (work in progress)

Recent work in extending SMT solvers to higher-order logic (HOL) has not explored lifting quantifier instantiation algorithms to perform higher-order unification. As a consequence, widely used instantiation techniques, such as trigger-and particularly conflictbased, can only be applied in a limited manner. Congruence closure with free variables (CCFV) is a decision procedure for the E-ground (dis-)unification problem, which is at the heart of these instantiation techniques. Here, as a first step towards fully supporting trigger-and conflict-based instantiation in HOL, we define the E-ground (dis-)unification problem in λ-free higher-order logic (λfHOL), an extension of first-order logic where function symbols may be partially applied and functional variables may occur, and extend CCFV to solve it. To improve scalability in the context of handling higher-order variables, we rely on an encoding of the CCFV search as a propositional formula. We present a solution reconstruction procedure so that models for the propositional formula lead to solutions for the E-ground (dis-)unification problem. This is instrumental to port triggerand conflict-based instantiation to be fully applied in λfHOL.

Introduction

Higher-order (HO) logic is a pervasive setting for reasoning about numerous real-world applications. In particular, it is widely used in proof assistants to provide trustworthy, formal, and machine-checkable proofs of theorems. A major challenge in this setting is to automate proofs as much as possible, thereby making the proof assistants easier to use. A successful approach to this automation challenge is hammering [START_REF] Blanchette | Hammering towards QED[END_REF]. It consists in encoding proof obligations into first-order (FO) logic and use first-order provers to discharge them. A similar layered approach is also used by HO theorem provers such as Leo-III [START_REF] Steen | The higher-order prover Leo-III[END_REF] and Satallax [START_REF] Brown | Satallax: an automatic higher-order prover[END_REF], which regularly invoke FO provers to discharge intermediate goals that depend solely on FO reasoning.

Such approaches have well-known performance, soundness, or completeness issues due to the black-box integration between FO and HO reasoning [START_REF] Bhayat | Set of support for higher-order reasoning[END_REF][START_REF] Meng | Translating higher-order clauses to first-order clauses[END_REF][START_REF] Vukmirovic | Extending a brainiac prover to lambdafree higher-order logic[END_REF]. To mitigate these problems, recent work [START_REF] Barbosa | Extending SMT solvers to higher-order logic[END_REF][START_REF] Bentkamp | Superposition with lambdas[END_REF][START_REF] Bentkamp | Superposition for lambda-free higher-order logic[END_REF][START_REF] Bhayat | Restricted combinatory unification[END_REF][START_REF] Vukmirovic | Extending a brainiac prover to lambdafree higher-order logic[END_REF] has focused on extending FO provers, based on the superposition calculus [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF][START_REF] Nieuwenhuis | Paramodulation-based theorem proving[END_REF] or on SMT solving [START_REF] Barrett | Satisfiability modulo theories[END_REF], to natively support HOL, so that the integration between the highly efficient FO component and the new HO one is graceful, i.e. the prover behaves mostly as its first-order counterpart on FO problems and also handles HO problems natively. The HO extension of SMT solvers [START_REF] Barbosa | Extending SMT solvers to higher-order logic[END_REF] has not explored lifting quantifier instantiation algorithms to perform higher-order unification. As a consequence, widely used instantiation techniques, such as trigger-based [START_REF] De Moura | Efficient e-matching for SMT solvers[END_REF][START_REF] Detlefs | Simplify: a theorem prover for program checking[END_REF], conflict-based [START_REF] Barbosa | Congruence closure with free variables[END_REF][START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF], model-based [START_REF] Ge | Complete instantiation for quantified formulas in satisfiabiliby modulo theories[END_REF][START_REF] Reynolds | Quantifier instantiation techniques for finite model finding in SMT[END_REF], and enumerative [START_REF] Reynolds | Revisiting enumerative instantiation[END_REF] instantiation, can only be applied in a limited manner. Moreover, even in a limited application, the efficient implementation of these techniques depends on specific term indices that have to be adapted to handle equalities between functions and a curried representation of terms [START_REF] Barbosa | Extending SMT solvers to higher-order logic[END_REF]Section 3.4].

Congruence closure with free variables (CCFV) [START_REF] Barbosa | Congruence closure with free variables[END_REF] is a framework for casting instantiation techniques in SMT. It is based on solving the E-ground (dis)unification problem, i.e. given a conjunctive set of ground equality literals E and a conjunctive set of (possibly non-ground) equality literals L, it finds substitutions σ such that E |= Lσ holds. These substitutions lead to instantiations following the instantiation technique being used. By extending CCFV to perform HO unification effectively we can in one fell swoop remove the limitations for HOL of all the instantiation techniques supported by the framework. This can be specially helpful for techniques that heavily depend on unification (as opposed to matching), such as conflict-based instantiation, which has been shown to be particularly effective for proof obligations originating from proof assistants [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF].

Given the complexity of the task at hand, we follow previous approaches by proceeding in a stepwise manner [START_REF] Bentkamp | Superposition for lambda-free higher-order logic[END_REF][START_REF] Vukmirovic | Extending a brainiac prover to lambdafree higher-order logic[END_REF], first extending CCFV to λ-free HOL (λfHOL), a fragment of HOL with partial applications and functional variables. In this effort we quickly realized that extending CCFV as a tableaux-like calculus, as it was originally presented [START_REF] Barbosa | Congruence closure with free variables[END_REF], posed a strong limitation on our ability to add new features to the framework. Moreover, the added complications of handling functional variables and a curried representation of terms, let alone lambda terms in the future, indicated that to have a scalable implementation we should handle the combinatorial nature of the search more efficiently than via regular backtracking. We thus present a lifting of CCFV to λfHOL via an encoding into an equisatisfiable SAT problem (Section 4). The encoding is based on fully reducing the search for substitutions to SAT based on the entailment conditions of literals in L (Section 4.1), after they have been preprocessed (Section 3), while taking into account the dependencies between variables due to cycles (Section 4.2) and congruence (Section 4.3). We present a solution reconstruction procedure (Section 5) so that satisfiable assignments lead to substitutions solving the original problem.

Preliminaries and problem statement

We work in λ-free higher-order logic (λfHOL) with Henkin semantics, following Bentkamp et al. [START_REF] Bentkamp | Superposition for lambda-free higher-order logic[END_REF]. We introduce here the relevant notions of this logic.

We use a monomorphic type system equipped with a set of atomic types S and a binary function → such that given two types τ , ν, the type τ → ν is the type of functions from τ to ν. The sets Σ and V respectively contain the function symbols (a, b, f , g...) and variables (w, x, y, z) upon which terms are built. Each symbol and variable is annotated with a type, e.g. f : τ → τ , but the types will be omitted when irrelevant or obvious, i.e. almost all the time except in the following definition. Terms are defined as: u = a | x | (u 1 : τ → ν) (u 2 : τ ) where a ∈ Σ, x ∈ V and u 1 , u 2 are terms. Note that this entails a curried representation of terms. A term is ground if it does not contain variables. We always denote terms using u plus various sub-and superscripts and ground terms using t instead. Subterms of u are u, u 1 , u 2 and all subterms of u 1 and u 2 (if they occur). Strict subterms are all subterms excluding u itself. The notations u[u ] and u[u ] s respectively denote that u is a subterm or a strict subterm of u.

Literals are equalities (u 1 u 2 ) and disequalities (u 1 u 2 ) of terms, respectively denoted positive and negative literals. It is possible to handle predicate literals, e.g. Q and ¬Q, implicitly as equations and disequations, e.g. Q and Q , by defining a binary type for Booleans and an interpreted symbol of this type. This is used in practice to apply the techniques presented here to predicates but it does not impact the theory so we do not mention it further in this paper. Sets of literals are denoted by L, L , etc., and sets of ground literals by E. The set of all terms, subterms included, that occur in a set of literals L is denoted by T(L). The set of all ground terms in L is denoted by T g (L).

Substitutions, denoted σ, are functions that map variables to terms such that only finitely many of them are not mapped to themselves. They are extended as usual to apply on terms and sets of terms, written in postfix notation. The domain of σ is dom(σ) = {x | x ∈ V and xσ = x} and its range is ran(σ) = {xσ | x ∈ dom(σ)}. A substitution is ground if its range is a set of ground terms. It is acyclic if each variable x never occurs as a subterm of xσ n for any n > 0. The fixpoint of an acyclic substitution always exists and is denoted σ .

An interpretation I assigns: 1. to each atomic type τ a non-empty set I(τ ); 2. to each type τ → ν a subset I(τ → ν) of the function space from I(τ ) to I(ν); 3. to each function or variable u : τ in Σ ∪ V an element I(u) in I(τ ). I naturally extends to an interpretation I(u) for each term u. An equation u 1 u 2 is entailed by an interpretation I if and only if I(u 1 ) = I(u 2 ), and a disequation u 1 u 2 is entailed by I if and only if I(u 1 ) = I(u 2 ). An interpretation I is a model of a set of literals L if it entails all of them. This is denoted by I |= L. By extension, we write E |= L when every model of E is also a model of L. 1Given a set of ground literals E, the congruence closure of E is the partition into classes of all ground terms such that two ground terms t 1 and t 2 belong to the same class if and only if E |= t 1 t 2 . Given additionally a set of literals L, the restriction of the congruence closure to T g (E ∪ L) is denoted E cc . The notation [t] denotes the E-congruence class in which t occurs. 2The representative of [t] is a chosen element in the class. The notation [t] ∈ E cc denotes that E |= t t for some ground term t ∈ T g (E ∪ L). Notice that, if [t] ∈ E cc , then [t ] ∈ E cc for any subterm t of t. We abuse this notation by writing [u] ∈ E cc and u ∈ [t] for non-ground terms u to indicate that we want u, or rather uσ for some grounding substitution σ, to belong to an E-equivalence class that exists in E cc or to a particular class [t] ∈ E cc respectively. We denote by [[t]] the set of signatures in [t], that is, all the pairs of classes

[t 1 ][t 2 ] such that [t 1 t 2 ] = [t].
Example 1. Let E = {a f a, g f, g b h c} and L = {x y d}, then E cc = {{a, f a}, {f, g}, {g b, h c}, {b}, {c}, {d}, {h}}.

In the full congruence closure of E, the class [a] is infinite since it includes all terms of the form f n a and g n a for n ≥ 0, among others. Entailment also goes beyond E cc , e.g.

E |= f b h c and E |= a f (g a). Moreover [[a]] = {[f ][a]}, [[g b]] = {[f ][b], [h][c
]} and the other signatures are empty.

Following Barbosa et al. [START_REF] Barbosa | Congruence closure with free variables[END_REF], we present below the definition of the E-ground (dis)unification problem in λfHOL and the theorem characterizing its set of solutions. Although both statements coincide with their first-order logic (FOL) counterparts, in λfHOL the problem and its solutions, if they exist, may include functional variables, which are now part of the set of terms over which substitutions range. Nevertheless, the lifting to λfHOL is straightforward since it can be directly encoded into FOL (e.g. by means of an applicative encoding).

Definition 2 (E-ground (dis)unification). Given two finite sets of equational literals E and L, where E is ground, the E-ground (dis)unification problem is that of finding substitutions σ such that E |= Lσ.

Theorem 3. Given an E-ground (dis)unification problem, if a substitution σ exists such that E |= Lσ, then there is an acyclic substitution σ such that ran(σ ) ⊆ T(E ∪ L), σ is ground, and E |= Lσ .

Proof. Let app denote the encoding of terms from λfHOL to FOL. 3 Let us assume that there exists a σ such that E |= Lσ. Then app(E) |= app(Lσ) = app(L)app(σ). The theorem we want to prove holds in first-order logic (see Theorem 1 in [START_REF] Barbosa | Congruence closure with free variables[END_REF]) thus there exists an acyclic substitution σ such than ran(σ ) ⊆ T app (app(E) ∪ app(L)), σ is ground, and app(E) |= app(L)σ . Then the substitution σ , where app(σ ) = σ is also acyclic and such that ran(σ ) ⊆ T(E ∪ L) and E |= Lσ .

Preprocessing

To ease the SAT encoding (Section 4) we assume that a series of standard preprocessing techniques, shown below, have been applied to L so that it comprises only literals of the form x y, x t or u 0 u 1 u 2 , where at least one of u 1 and u 2 is a variable.

Normalizing. A set of literals is E-normalized, abbreviated as normalized because E is always clear from the context, if every ground term it contains is the representative of its congruence class modulo E. A set of literals can be normalized by replacing all occurrences of ground terms by their representative.

Example 4. Given the problem:

E = {(f a) b (f b) a, g b g c, h 1 h 2 , g f a} L = {h 1 x b, x (f a) y, h 1 ((f x) b) a, g b (f x) y, (f a) a g b}
The non-singleton classes in E cc are:

[g] = {g g g, f a} [(f a) b] = {g b, g c g c g c, (f a) b, (f b) a} [h 1 ] = {h 1 , h 2 h 2 h 2 }
where bold font t t t identifies the representative term in a class [t]. The normalized L is thus:

L norm = {h 2 h 2 h 2 x b, x g g g y, h 2 h 2 h 2 ((f x) b) a, g c g c g c (f x) y, g g g a g c g c g c}.
Removing ground literals. Eliminating ground literals from L amounts to replace them by if they are entailed by E and by ⊥ otherwise, followed by removing all occurrences of from L. If there is any occurrence of ⊥ then L itself becomes {⊥} since the E-ground (dis)unification problem is then unsatisfiable.

Example 5. Consider E and L as in the previous example. Removing ground literals from L norm produces L non-ground = {⊥} because its last equation is not entailed by E. If we consider instead L = L\{(f a) a g b} then L norm = L norm \{g a g c} and finally L non-ground = L norm .

Flattening. A set of literals is flattened if each of its literals is of the form x t, x y, x t, x y, or u 0 u 1 u 2 where x and y are variables, t is a ground term, and u 0 , u 1 , u 2 are either variables or ground terms with at least u 1 or u 2 being a variable. Any set of literals can be flattened by introducing new variables.

Example 6. Consider L as in the previous example. The flattened version of L non-ground is:

L flat = {b h 2 x, x g y, a h 2 z 1 , z 1 z 2 b, z 2 f x, g c z 2 y}.
Trivial assignments. A set of literals L has trivial assignments if it contains literals of the following form:

• x t, where x is a variable and t is ground; • x y, where x, y are variables; • x u, where variable x does not occur elsewhere in L including in u, and u is any term (not containing x).

As long as there is a trivial assignment x u in L it is possible to consider the equivalent problem where L is replaced by L = (L \ {x u })σ instead, where σ = {x → u }. In the third case, this simply amounts to removing the x u equation from L.

Since L may contain new ground literals and trivial assignments, as well as ground terms that are not in normal form, it is necessary to iterate on normalization, ground literals simplification and trivial assignments instantiation until all such literals have been removed. Eliminating trivial assignments might render a literal ground, but otherwise flattening is not impacted by this transformation. Indeed, none of the three cases of trivial assigments will ever lead to the replacement of a variable inside a literal by an applied non-ground term. This process terminates since each step eliminates one variable from L among finitely many. Sect. 5 provides a way to build a solution for L from a solution for L . x b, z y z}. Assume that L is already normalized for a given E. Note that L is also flattened and without ground literals. However, it contains the trivial assignment x f a since f a is ground. Applying the previously described procedure yields L = {y (f a) b, z y z}. This new set is still flattened and without ground literals but it contains a new trivial assignment, namely y (f a) b. Assume (f a) b is normalized. After another iteration of the procedure, the remaining problem is L = {z ((f a) b) z}.

Example 9. Let L = {y

x a, z x, z f x, g x c}. As in the previous example, L is flattened and without ground literals and we assume it is normalized for a given E. Both literals y x a and z x are trivial assignments and are to be eliminated. The preprocessing chain yields L = {x f x, g x c}.

A flattened normalized set of literals without trivial assignments and ground literals is called a preprocessed set of literals.

Encoding CCFV as a SAT problem

Every solution of the E-ground (dis)unification problem is a substitution: it maps variables to terms. Thanks to Theorem 3 we know that if a generic solution exists, then a ground one can always be found. Thus it is enough to search for ground solutions to answer the general problem. Such a ground solution associates each variable to a ground term belonging to a particular Econgruence class, in or out of E cc .

By considering all classes from E cc and merging all the classes outside of E cc together, the association between variables and classes turns into a combinatorial problem with finitely many possibilities. Barbosa et al. [START_REF] Barbosa | Congruence closure with free variables[END_REF] presented CCFV, a decision procedure for E-ground (dis)unification, as a tableaux-like procedure that decomposes L in a top-down manner so that the possibilities for mapping variables are increasingly reduced. The decompositions are based on the entailment conditions for the literals in L, according to their structure. However, considering the entailment conditions in the presence of functional variables and a curried representation of terms, particularly when we move beyond λfHOL and need to take higher-order unification into account, opens up more possibilities that cannot be handled in such a high-level procedure without a severe loss of efficiency or an extremely intricate design. As an alternative solution aiming for greater flexibility and better performance, here we tackle the combinatorial problem by, from the get-go, fully decomposing each literal in L as a propositional disjunction over all the conditions for its entailment, relying on a SAT solver to determine an assignment that respects all conditions (Section 4.1). Moreover, by reducing the problem to SAT we also need to encode properties that were handled silently at the firstorder level by term indexing and by the underlying ground congruence closure component, namely cyclic dependencies between variables (Section 4.2) and variables assigned by derived congruence reasoning (Section 4.3).

Encoding's core

We assume L is preprocessed. The set L thus only contains literals of the form x u and u 0 u 1 u 2 where x is a variable and u, u 0 , u 1 , u 2 are variables or ground terms, at least one of u 1 and u 2 being a variable. The problem is encoded into a set C of formulas, which is the union of all C for ∈ L.

C x u : [t1],[t2]∈E cc ,E|=t1 t2 (x ∈ [t 1 ] ∧ u ∈ [t 2 ]) C u0 u1u2 : [u 0 ] ∈ E cc ∨ [t0]∈E cc , [t1][t2]∈[[t0]] (u 0 ∈ [t 0 ] ∧ u 1 ∈ [t 1 ] ∧ u 2 ∈ [t 2 ])
The intuition behind this encoding is as follows. Assume there exists a solution σ to the Eground (dis)unification problem.

such that [t 1 ][t 2 ] ∈ [[u 0 σ]].
Thus in that case it is enough to consider all possible signatures of the class that u 0 is assigned to. 4All membership tests where u or u i is not a variable are simplified in the above formulas (to true or false). In the literals that remain, u and u i are always variables and literals are of the form x ∈ [t] or [x] / ∈ E cc for some variable x and some class [t] ∈ E cc . A new propositional variable P x,[t] is introduced for each literal x ∈ [t] occurring in any C . Another propositional variable Q x is introduced for each literal x / ∈ E cc occurring in any C . Note that since a variable cannot be mapped to two distinct classes at the same time, we also encode that the P x,[t] that occur in the encoding are mutually exclusive between themselves and with Q x , for each x ∈ V.

As illustrated by the following example, the above encoding is not enough to represent the problem in the general case.

C x y x = Q x ∨ (P x,[a] ∧ P y,[f ] ) C z g y = Q z C z v f = Q z ∨ (P z,[k] ∧ P v,[h] ) C y y = (P y,[f ] ∧ P y ,[f ] ) ∨ (P y,[f ] ∧ P y ,[f ] )
and the relevant mutual exclusion constraints are

¬P y,[f ] ∨ ¬P y,[f ] ¬P y ,[f ] ∨ ¬P y ,[f ] ¬Q x ∨ ¬P x,[a] ¬Q z ∨ ¬P z,[k]
Note that in C x y x the disjunct P x,[k] ∧ P y,[h] ∧ P x,[f ] does not occur, because it assigns x to two distinct classes. Since this trivially contradicts the mutual exclusion constraints, this disjunct can never be true. 5 Another noteworthy point is that C z v f is redundant to C z g y . This could also be detected during the encoding and simplified. It would prevent the addition of the useless mutual exclusion constraint on z-related literals.

Note that one model of the obtained formula is {Q x , Q z , P y,[f ] , P y ,[f ] }, which implies in particular that [x] ∈ E cc . However, all the solutions to the current problem must map x to [a] ∈ E cc because it is the only class that contain both a term and its image by f . In fact, this issue happens for a whole family of variables, that we denote as cyclic variables. An extra constraint is required to handle them separately.

Cycle-based constraints

Formally, a variable is cyclic in a set of terms

L if L |= x u[x]
. The cycle can be directly apparent in an equation in L as in the previous example, but it can also be less obvious, as in L = {x y a, y g x} where both x and y are cyclic. Cyclic variables in an Eground (dis)unification problem must all be mapped to terms in E cc . This is a consequence of Lemma 11. Its proof is available in Appendix B. Lemma 11. Let E be a set of ground equational terms. Let t and t [t] s be ground terms. If The dependency between variables can be encoded as a directed graph where a vertice represents a variable and an edge from the vertex x to the vertex y indicates the presence of an equation x u 1 u 2 in L where y is either of u 1 and u 2 . Thus it is possible to use any algorithm that enumerates the cycles in a graph to find all cyclic variables in L. For our prototype implementation, we used a naive algorithm described in Appendix C but linear algorithms are known, e.g. Tarjan's strongly connected components algorithm [START_REF] Tarjan | Depth-first search and linear graph algorithms[END_REF]. Once the cycles are detected, the additional constraints ¬Q i must be added to the encoding for each cyclic variable as well as for all variables reachable from cyclic variables in the dependency graph. 6 The later is required because all subterms of a term in E cc must also be in E cc .

E |= t t [t] s then [t] ∈ E cc .
The core encoding and the cycle-based constraints ensure that all the variables that must be mapped to terms in E cc indeed are. However, the variables that can be mapped outside of E cc may also have extra constraints that are not captured by what has been described so far.

Example 14. Consider Example 10, with the addition of ¬Q x to the encoding. A model of the resulting formula is {P x,[a] , P y,[f ] , P y ,[f ] , Q z }. This does not tell us anything about v, which means that this variable could be mapped to any (type-compatible) class. However, mapping v to [h] does not lead to a valid solution. This would force z to be equal both to g f and to h f , although [g f ] = [h f ], which is impossible.

Further constraints are required on the variables that can be mapped outside of E cc . We denote those variables as floaters.

Floater-based constraints

For a variable x, being a floater means it occurs on the left-hand side of an equation in L and that [x] ∈ E cc . It follows from the latter that any equation x u 1 u 2 ∈ L where x is a floater must either be a tautology or hold by congruence. In both cases, it means that if another equation of the same form x u 1 u 2 also occurs in

L, necessarily [u 1 ] = [u 1 ] and [u 2 ] = [u 2 ].
Of course, before running the SAT solver, we don't know exactly which variables are floaters, so we have to encode these constraints conditionally. If there are n equalities x u 1j u 2j in L where j ∈ {1..n}, x is not cyclic nor occurs in a disequation, and if n > 1, the previously described constraints can be expressed as:

Q x ⇒ (Q u11 ≡ • • • ≡ Q u1n ) and Q x ⇒ (Q u21 ≡ • • • ≡ Q u2n ); for [t] ∈ E cc , Q x ⇒ (P u11,[t] ≡ • • • ≡ P u1n,[t] ) and Q x ⇒ (P u21,[t] ≡ • • • ≡ P u2n,[t] ).
Note that as soon as one of the u ij is ground for i ∈ {1, 2} and j ∈ {1..n}, the corresponding Q uij is false and the truth values of the P uij ,[t] s are also known beforehand for all [t] ∈ E cc , which simplifies and significantly narrows the constraints.

Example 15. Consider again Example 10, the only floater-based constraints to add originate from the two equations involving z: z g y and z v f . In their simplified form, because f and g are ground, they are:

Q z ⇒ ¬Q v , Q z ⇒ P v,[g] , Q z ⇒ ¬P v,[h] , Q z ⇒ ¬Q y , Q z ⇒ P y,[f ] , Q z ⇒ ¬P y,[f ]
Thanks to the addition of these constraints, the only model of the encoding is now

M = {P x,[a] , P y,[f ] , P y ,[f ] , Q z , P v,[g] }. The substitution σ = {x → a, y → f, y → f , z → g f, v
→ g} is a solution of the problem. It satisfies all the constraints in M.

We conjecture that our encoding is sound and complete. The proof of this central result is still work in progress.

Conjecture 16. Given two sets of equational literals E and L such that E is ground, the E-ground (dis)unification problem has a solution if and only if the encoding of this problem is satisfiable.

Reconstruction of a solution from a SAT model

Let E and L form an E-ground (dis)unification problem. Let L pre be a preprocessed version of L and L triv be the set of trivial assignments that were removed from L during the preprocessing. Assume that the encoding of the problem is satisfiable and let M be a model of this encoding. Let t r denote the representative of [t].

To build a ground substitution σ such that E |= Lσ, we proceed iteratively, starting with the variables in E cc and those that do not depend on any other variables, then going backward through the variable dependency graph of L pre ∪ L triv , until all variables are mapped to ground terms.

In more details:

• σ 0 = {x → t r | M |= P x,[t]
}, where x occurs in L pre .

• σ 1 = σ 0 • σ such that, for any variable x not grounded by σ 0 and that only occurs on the right-hand side of equations in L pre ∪ L triv , σ maps x : τ to t τ r where t τ denotes a default term of the appropriate type.

• The mapping of all other variables must be built iteratively. For i > 1 let

I i = {(x, t) | x t ∈ (L pre ∪ L triv )σ i-1 } and let σ i = σ i-1 • {x → t r | (x, t) ∈ I i }.
The process terminates as soon as all variables have been assigned and the final result is σ.

Example 17. For the problem in Example 10, considering the model M given in Example 15, σ 0 = {x → a, y → f, y → f , v → g} is determined looking at all the P x,[t] in M. Then σ 1 = σ 0 because there are no variables matching the criterion. Finally, one iteration of the last step is enough to obtain σ = σ 0 • {z → f g} that is a ground substitution such that E |= Lσ.

Note that the solution obtained may not satisfy all the [x] ∈ E cc constraints. They will only be satisfied if the variables mapped in the second step are assigned default values outside E cc . In practice, in the context of SMT, we may want to do the exact inverse and map as many of these variables as possible inside of E cc .

Another noteworthy point concerning this second step is that there must be only one unique default value for each type, or at least one default class. To illustrate this, consider a problem where x f y, x f z ∈ L pre , but neither of the three variables occur anywhere else. If y and z are mapped to two terms that do not belong to the same E-congruence class, the resulting substitution will not be a solution of the problem. Conjecture 18. Let E and L form an E-ground (dis)unification problem that admits a solution. Then the substitution σ constructed following the reconstruction method described in this section is a ground solution of the problem.

Ongoing and future work

A first-order version of CCFV with support for λfHO terms encoded with the applicative encoding [START_REF] Barbosa | Extending SMT solvers to higher-order logic[END_REF] is already implemented in the λfHOL extension of the lightweight SMT solver veriT [START_REF] Bouton | veriT: an open, trustable and efficient SMT-solver[END_REF]. It has a term-indexing issue because terms are indexed by the symbol at their head and the applicative symbol occurs at the head of all functional symbols. Thus, contrarily to what happens in FOL where the head symbol significantly restricts the mapping possibilities, here only types can be exploited to retrieve suitable terms, which can lead to many more terms being retrieved at once in comparison with the first-order case. The present approach does not have this problem because it does not rely on the applicative encoding at all.

A prototype is under development in veriT. However, model reconstruction is not yet operational. As soon as it is, we will be able to compare our approach with the applicative version of CCFV. Given that the later, used by trigger-and conflict-based instantiation, currently takes around 40% of the overall SMT computation time in the benchmarks used by Barbosa et al. [START_REF] Barbosa | Extending SMT solvers to higher-order logic[END_REF], we expect that any improvement on the efficiency of CCFV will lead to an important speedup in the SMT process, but it remains to be observed in practice if this is the case for our approach.

Experiments notwithstanding, there is much that can be improved in our prototype regarding the data-structures as well as the algorithms for the preprocessing and the encoding phases. In particular, cycle detection is currently implemented with a naive algorithm in O(n 3 ). It will eventually be replaced by Tarjan's linear algorithm. Furthermore, the encoding itself could be improved. Each constraint C x u and C u0 u1u2 imposes that variables belong to some classes among all, and indirectly that they do not belong to the remaining classes. This information could be propagated to other constraints and lead to further narrowing of the set of possible classes for some variables. By starting with the most restrictive constraints, one might be able to significantly restrict the size of the constraints, the number of propositional variables, and also the number of necessary mutual exclusion constraints. An incremental encoding to SAT, as well as a heuristic to guide the SAT solver so that it starts its search on the most restricted variables are also on our list of ideas to be investigated.

A Applicative encoding

The applicative encoding turns every symbol in λfHOL of a non-atomic type τ 1 → τ 2 into a symbol of the atomic type τ τ1→τ2 in non-curried FOL. It also introduces a family of function symbols @ : τ τ1→τ2 ×τ 1 → τ 2 such that app(u 1 u 2 ) = @(u 1 , u 2 ). For example app(h 1 ((f x) b)) = @(h 1 , @(@(f, x), b)).

B Proof of the cycle-based narrowing lemma

Lemma. Let E be a set of ground equational terms. Let t and t [t] s be ground terms. If

E |= t t [t] then [t] ∈ E cc .
Proof. The congruence graph induced by E on a set of terms is the smallest undirected graph such that:

• for each equality u v in E, there is an edge between u and v.

• if there is a path from u 1 to v 1 and from u 2 to v 2 , there is an edge from u 1 u 2 to v 1 v 2 ; the edges are said to be congruence edges.

Consider all possible terms in a given language and their partition induced by E: two terms are in the same class if and only if there is a path in the congruence graph from one to the other. We now consider the interpretation I such that:

• the domain is the set of partitions;

• each constant is interpreted as the partition it belongs to;

• the application of two elements is interpreted as the partition containing the application of members in the respective partitions.

v] / ∈ E cc . Then u = u 1 u 2 , and v = v 1 v 2 , one v i containing t. Then E |= u i v i and [v i ] / ∈ E cc for i ∈ {1, 2}
. Similarly, we can continue decomposing u i , until we obtain a constant after finitely many decompositions (t being a finite term). We reach a contradiction, because this constant is equal to an application term, and both terms are equal through congruence.

C A naive cycle-detection algorithm

Given a preprocessed set of literals L, let us denote as defining equations the equations of the form x u 1 u 2 occurring in L, where x is a variable and u 1 , u 2 are any term. Variables occurring on the left-hand side of defining equation are called defined variables and variables occurring on the right-hand side of a defining equation are called the used variables.

Let D be the set of all variables occurring in L that are both defined and used. For example, for L 1 = {x y z, x f z, y g x} where x, y, z are variables, we obtain D 1 = {x, y}, and for L 2 = {x y z, y g x, z f y, g w c} where x, y, z, w are variables, we obtain D 2 = {x, y, z}. If D = 0 then there are no cyclic variables in L. Otherwise, the following procedure identifies the cyclic variables in L:

• Build an n × n matrix M 0 , where n = |D|. Each row i of this matrix and its successors represents a defined variable x i in D and each column j a used variable x j in D. Initialize the cells of M 0 as:

M 0 [i, j] =    1 if
x j occurs in a defining equation x i = u 1 u 2 , i.e. x j = u 1 or x j = u 2 ; 0 otherwise.

• Iterate the following operations until the matrix is stable, i.e. until M k = M k+1 . For all lines i of M k , let J i = {j | M k [i, j] = 1} and have:

M k+1 [i] = M k [i] ∨ j∈Ji M k [j]
where the disjunctions are bit-wise operators. • Let M be the stable result obtained in the previous step. The used variables that belong to cycles are all the i ∈ {0, ..n -1} such that M[i, i] = 1.

Example 19. Let us consider L 2 = {x y z, y g x, z f y, g w c} as before. Then D 2 = {x, y, z} and:

M 0 =   0 1 1 1 0 0 0 1 0   , M 1 =   1 1 1 1 1 1 1 1 0   , M 2 =   1 1 1 1 1 1 1 1 1   , M 3 = M 2 ,
thus x, y and z are cyclic but not w.

Note that if the matrix is completely filled with 1's, it is not necessary to perform an extra iteration of the procedure to conclude that it is stable.

M 0 =   0 1 1 0 0 0 1 0 0   , M 1 =   1 1 1 0 0 0 1 1 1   , M 2 = M 1 ,
showing that here only x and y are cyclic. Note that if a line of the matrix contains only zero's, it is possible to remove it completely from the problem, so here it is possible to compute only:

M 0 = 0 1 1 0 , M 1 = 1 1 1 1 , M 2 = M 1 .
Note that it is also possible to consider all variables when building M 0 , not only those in D. This will only create more lines filled with 0's that need to be discarded.

Moreover, Note that not all lines in the matrices end up filled with only 1's or only 0's, as illustrated in the following extension of the previous example.

M 0 =     0 1 1 0 0 0 0 1 1 0 0 0 0 0 0 1     , M 1 =     1 1 1 1 0 0 0 1 1 1 1 0 0 0 0 1     , M 2 =     1 1 1 1 0 0 0 1 1 1 1 1 0 0 0 1     , M 3 = M 2 .
It is not possible to use this algorithm to detect cycles before the flattening because it applies only on variables and it is possible to have a cycle on an applied term before flattening. For example in the non-flattened L = {g x (k w) (f x), f x h (g x)}, both g x and f x are involved in a cycle but they are terms, not variables. The only variables x and w are not involved in cycles, hence our algorithm will not find any cyclic variable. After flattening, L flat = {y 1 g x, z k w, y 2 f x, y 1 z y 2 y 2 h y 1 } and the variables y 1 and y 2 represent the terms involved in cycles. This can now be detected by the algorithm presented above.

Example 7 .

 7 L flat from the previous example contains no trivial assignments. Example 8. Let L = {x f a, y

Example 10 .

 10 Let E = {a f b, a b, f f , k h f } and L = {x y x, z g y, z v f, y y } where x, y, y , z, and v are variables. The only non-singleton classes in E cc are [a] = {a, b, f b} and [k] = {k, h f }. The non-empty signatures are [[a]] = {[f ][a]} and [[k]] = {[h][f ]} The set L is already preprocessed. Then:

Corollary 12 .Figure 1 : 10 Example 13 .

 1211013 Figure 1: Dependency graph of L from Example 10

Figure 4 .

 4 2 represents this graph for the set of literals L from Example 10.

Example 20 .

 20 Let us now consider L 3 = {x y z, y g w, z f x}, where x, y, z, w are variables. Then D = {x, y, z} and:

Example 21 .

 21 Let L 4 = {x y z, y f w, z f x, w f w}, where x, y, z, w are variables. Then D = {x, y, z, w} and:

  For negative literals, E |= (x u)σ holds only if there exist t 1 , t 2 such that E |= t 1 t 2 and xσ ∈ [t 1 ], uσ ∈ [t 2 ]. Moreover, for E |= t 1 t 2 to hold it must be the case that [t 1 ], [t 2 ] ∈ E cc . For positive literals, E |= (u 0 u 1 u 2 )σ holds if u 0 σ and (u 1 u 2 )σ are in the same congruence class. If [u 0 σ] ∈ E cc , we know exactly which kind of applied term can belong to this class: any term t 1 t 2

  This interpretation I is a model of E, and assigns two terms in different classes to different elements in the domain. Hence, E |= u v only if u and v belong to the same class.Within each class[u] = [v] such that [u] / ∈ E cc ,all edges between two distinct members u, v of the class are congruence edges (all other edges being between elements of E cc ), which imposes that u is of the form u 1 u 2 and v is of the form v 1 v 2 with u 1 in the same class as v 1 and u 2 in the same class as v 2 . In particular there exists a term t [t] s such that t occurs in t [t] s at a depth larger than the depth of t. Since [t] / ∈ E cc , no subterm of t [t] s that contains t belong to E cc either. Now let us consider for a start u = t and v = t [t] s . We have already shown that E |= u v and [

Notice that, if E |= t t [t] s , then E |= t t [t [t] s ] s . This can be used to build a term of arbitrary depth t [t] s equal to t according to E.

This is a simplification of the actual formalism by Bentkamp et al.[START_REF] Bentkamp | Superposition for lambda-free higher-order logic[END_REF].

Note that [t] alone refers to the class of t, while u[t] refers to a term u with a subterm t.

WiP note: The applicative encoding allows to encode λfHOL with Henkin semantics to FOL with standard semantics. In future work, we plan to replace this proof with one that does not rely on the applicative encoding, we only give a minimal description of it in Appendix A. It is also described, e.g., byBarbosa et al. [4].

WiP note: These informal statements will be formalized as a lifting to λfHOL of Theorem 4.4 in[START_REF] Barbosa | New techniques for instantiation and proof production in SMT solving[END_REF], which captures the conditions in FOL for solving the E-ground (dis)unification problem for a given literal in L based on its structure.

Even if this was not the case, there would still be a typing incompatibility in allowing x to be mapped to [a] and to [f ] in different disjuncts since a and f must have distinct types.

Alternatively, all occurrences of Q i for relevant is are set to false and the formula is simplified accordingly.

Acknowledgments

We are grateful to Jasmin Blanchette for many discussions throughout the development of this work, for providing funding for research visits and for suggesting many improvements. Experiments were carried out using the Grid'5000 testbed (https://www.grid5000.fr/), supported by a scientific interest group hosted by Inria and including CNRS, RENATER, and several universities as well as other organizations.

The order of authors is inverse alphabetic† The work has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka).


Mathieu Sart
email: mathieu.sart@univ-st-etienne.fr

MINIMAX BOUNDS FOR BESOV CLASSES IN DENSITY ESTIMATION

Keywords: Mathematics Subject Classification. 62G05, 62G07. Key words and phrases. density estimation, minimax risk, Besov spaces

come

Minimax bounds for Besov classes in density estimation

Introduction

We consider n independent and identically distributed random variables X 1 , . . . , X n defined on an abstract probability space (Ω, E , P ). We suppose that X i admits a density f with respect to the Lebesgue measure on [0, 1] and are interested in estimating f from the observations X 1 , . . . , X n .

We consider p ≥ 1, a subset F of the linear space (L p ([0, 1]), • p ), and define the celebrated minimax risk

R p (F) = inf f R p ( f ) where R p ( f ) = sup f ∈F E f d p p (f, f ) 1/p
, where d p denotes the distance in the above space, and where the infimum is taken over all estimators f with values in F. The minimax rate of convergence, that is the rate at which R p (F) converges to 0 (if it converges), is the best possible for procedures based solely on assumptions modelled by F. This rate can therefore be seen as a benchmark for statistical procedures.

In the present paper, our aim is to define a (near) minimax estimator under smoothness constraints. We will therefore pay special attention to bounded subsets F of Besov spaces B α π,∞ . The subscript π indicates here in which (quasi) norm the regularity α is measured. The smaller π is, the larger the class is, and the more difficult the estimation problem is. It is sometimes said that these Besov spaces allow taking into account spatially inhomogeneous smoothness. The minimax results rely heavily on π, p, α as described below.

The simplest case is π ≥ p. The minimax rate of convergence is then n -α/(1+2α) , and this rate can even be achieved by a linear estimator, see [START_REF] David L Donoho | Density estimation by wavelet thresholding[END_REF]. In the literature, the case π < p is often associated with the restriction α > 1/π. Despite this, linear estimators are no longer rate optimal and more sophisticated procedures need to be considered. We may cite for instance [START_REF] David L Donoho | Density estimation by wavelet thresholding[END_REF][START_REF] Delyon | On minimax wavelet estimators[END_REF] for wavelet thresholding estimators, [START_REF] Birgé | From model selection to adaptive estimation[END_REF] for penalized minimum contrast estimators and [START_REF] Birgé | Model selection via testing: an alternative to (penalized) maximum likelihood estimators[END_REF] for T -estimators. The results are as follows: the previous rate n -α/(1+2α) still applies when α > (p -π)/(2π), but becomes (log n/n) (α-1/π+1/p)/(1+2α-2/π) when α < (p -π)/(2π). At the boundary α = (p -π)/(2π), additional logarithmic factors may appear.

The situation appears to be more complicated to deal with when π < p and α ∈ (1/π -1/p, 1/π]. The condition α > 1/π -1/p ensures that B α π,∞ ⊂ L p ([0, 1]) and allows the use of a L p loss. However, B α π,∞ is not included in L ∞ ([0, 1]) as α ≤ 1/π. A key paper for understanding the importance of the condition f ∞ < +∞ in estimation procedures is that of [START_REF] Birgé | Model selection for density estimation with L2-loss[END_REF]. In this paper, [START_REF] Birgé | Model selection for density estimation with L2-loss[END_REF] showed a lower minimax bound. It reveals that the usual rate n -α/(1+2α) cannot be true over the whole range (1/π -1/p, 1/π] when p = 2. However, this rate is the right one when the density is bounded. This problem of determining the optimal rates when the target function is smooth but not bounded has already been studied in the literature in other statistical settings such as, for instance, the Gaussian white noise model and the regression model with random design. We refer here to [START_REF] Baraud | Model selection for regression on a random design[END_REF][START_REF] Birgé | Model selection for Gaussian regression with random design[END_REF][START_REF] Lepski | Adaptive estimation over anisotropic functional classes via oracle approach[END_REF] and the references therein. In the latter model, the minimax rate is known (up to log factors) for the L 2 loss and is n -min{α/(1+2α),α-1/π+1/2} when π ∈ [1, 2) and α ∈ (1/π -1/2, 1/π]. We observe therefore a possible deterioration of the rates when the target is not bounded. This is similar to density estimation but contrasts with the white noise model where the boundedness assumption can be removed without changing the exponent in the optimal rates: it is α/(1 + 2α) regardless of π ∈ [1, 2), α ∈ (1/π -1/2, 1/π] when p = 2.

Several procedures for unbounded densities have been proposed in the statistical literature. We may cite for instance the wavelet thresholding procedures of [START_REF] Bunea | Spades and mixture models[END_REF][START_REF] Reynaud-Bouret | Adaptive density estimation: a curse of support?[END_REF]. They lead to nice oracle inequalities for the L 2 loss without condition on the supremum norm of f . There are also the pointwise selection scheme of [START_REF] Lepski | Oracle inequalities and adaptive estimation in the convolution structure density model[END_REF] and the test procedures of [START_REF] Birgé | Model selection via testing: an alternative to (penalized) maximum likelihood estimators[END_REF][START_REF] Birgé | Model selection for density estimation with L2-loss[END_REF]. They give very general results but at the cost of a (very) high computational complexity. In the present paper, we define a new estimator and show that it achieves the rate (log n) β n -min{α/(1+2α),(α-1/π+1/p)/(1+α-1/π)} when α ∈ (1/π -1/p, 1/π], π < p for some β independent of n. Moreover, we show that this rate is optimal, up to logarithmic factors. In particular, when π < p -2, the minimax rate is never n -α/(1+2α) . When π > p -2, there is an elbow effect, the exponent being (α -1/π + 1/p)/(1 + α -1/π) for "small values of α" and α/(1 + 2α) for "large values".

We restrict our study to the estimation of the density on the unit interval [0, 1] but other estimation domains have also been considered in the literature. For results concerning the estimation on the real line under smooth constraints, we refer to [BH78, JLL04, Efr08, RBRTM11, GL11, GL14]. However, it should be noted that the minimax rates on Besov classes can be very different, depending on whether the estimation domain is compact or not. As far as we know, the rates on the real line are not fully known. In higher dimension, the whole point is to reduce the curse of dimensionality. A solution is to allow the smoothness of f to vary with the direction. For more informations on these issues of anisotropy, we refer to [Kle09, GL11, Aka12, GL14].

Our estimation strategy is based on projection estimators and on a new estimator selection rule. This procedure may be thought of as a mix between a Lespki-type procedure [START_REF] Lepski | Asymptotically minimax adaptive estimation. i: Upper bounds. optimally adaptive estimates[END_REF] and the one of [START_REF] Sart | Estimation of the transition density of a Markov chain[END_REF]. It leads to a piecewise polynomial estimator of degree r that is (near) minimax and adaptive over the full scale of Besov classes π ∈ (0, p) and α ∈ (1/π -1/p, r + 1). In other terms, it achieves the rates given above, up to logarithmic factors, without the prior knowledge of α and π. Our estimator has also computational properties. We may build it in polynomial time when p > 1, and more precisely in around O(n p/(p-1) log n) operations. It is also possible to make our estimator computable in (nearly) linear time when the classical condition α > 1/π is met.

The paper is organized as follows. We make explicit the minimax rates of convergence in the next section. Section 3 is devoted to the construction of our estimator and contains intermediate results such as an oracle inequality and a result on the approximation of the elements of B α π,∞ by piecewise polynomial functions. The proofs are postponed to Section 4.

Minimax results

2.1. Besov classes. We recall here the definition of Besov spaces to introduce our notations, and refer to [START_REF] Ronald | Constructive approximation[END_REF] for more details.

We consider α, π > 0, π ∈ (0, +∞] and the smallest integer r larger than α. For any map f on

[0, 1], h > 0 and t ∈ [0, 1 -rh], we set ∆ r h f (t) = r k=0 r k (-1) r-k f (t + kh).
Let then ω p (f, x) be the modulus of smoothness

ω π (f, x) = sup 0<h≤x [0,1-rh] |∆ r h f (t)| π dt 1/π , and
|f | B α π,π =    ∞ 0 [x -α ω π (f, x)] π dx x 1/π if π < +∞ sup x>0 x -α ω π (f, x) if π = +∞. When π, π ≥ 1, | • | B α π,
π is a semi-norm, and a quasi semi-norm otherwise. We define the Besov space B α π,π as the set of functions f on [0, 1] with finite (quasi) seminorm |f | B α π,π . We investigate in the next section the problem of minimax estimation over the class

B α π,π (R) = f ∈ B α π,π , |f | B α π,π ≤ R .

Minimax results.

We consider π ∈ (0, p),

ᾱ = 1/(2π) -1/p + 1/π -1/p + (1/(2π) -1/p) 2 , (1) and set for α ∈ (1/π -1/p, 1/π], ψ = min {(α -1/π + 1/p)/(1 + α -1/π), α/(1 + 2α)} , = (α -1/π + 1/p)/(1 + α -1/π) if α ∈ (1/π -1/p, ᾱ], α/(1 + 2α) if α ∈ (ᾱ, 1/π].
Note that ᾱ may be larger than 1/π, in which case (ᾱ, 1/π] = ∅. In Section 3, we carry out an (adaptive) estimation procedure leading to the following result:

Theorem 1. Let p ∈ [1, +∞), π ∈ (0, p), α ∈ (1/π -1/p, 1/π] and R > 0. Then, for n large enough, R p (B α π,∞ (R)) ≤ c 1 (log n) β n -ψ , (2)
where β only depends on p, π, α and where c 1 only depends on R, p, π, α.

Up to log factors, the rate that is achieved when α > ᾱ cannot be improved as it corresponds to the minimax rate for Hölder semi-balls. In the literature, [START_REF] Birgé | Model selection for density estimation with L2-loss[END_REF] obtained a lower bound that matches with this upper bound (to within logarithmic factors) when p = 2 and α ≤ ᾱ. Slight modifications of his proof lead to:

Proposition 2. Let p ∈ [1, +∞), π ∈ (0, p) and R > 0. Then, if α ∈ (1/π -1/p, 1/π], for n large enough, R p (B α π,∞ (R)) ≥ c 2 n -ψ . Moreover, if α ≤ 1/π -1/p and p > 1, for n large enough, R p f ∈ B α π,∞ (R), f p ≤ 1 + R ≥ c 2 .
In these inequalities, c 2 depends on R, p, π, α only.

Therefore, the optimal rate of convergence is n -ψ , up to possible logarithmic factors. When α is smaller than 1/π -1/p, B α π,∞ (R) is not included in L p ([0, 1]) and minimax results for B α π,∞ (R) are meaningless. The second point of the proposition says that the minimax rate does not tend to zero even under an additional condition on the L p norm when p > 1.

When p = 1, ᾱ = 1/π-1, and we recover that ψ = α/(1+2α) on the whole range (1/π-1, 1/π]. This rate is actually free of logarithmic factors, see [START_REF] Birgé | Model selection via testing: an alternative to (penalized) maximum likelihood estimators[END_REF]. The case p > 1, α < 1/π does not seem to have attracted much attention in the statistical literature. However, we suspect the estimators of [BTWB10, RBRTM11, LW19] are minimax to within logarithmic factors. This is unfortunately not the case for the estimator of [START_REF] Birgé | Model selection for density estimation with L2-loss[END_REF] (see his Section 4.4.3).

When α > 1/π, the minimax rate of convergence has been known for a long time. It is, up to logarithmic factors, n -ψ , where

ψ = α/(1 + 2α) if α > (p -π)/(2π) (α -1/π + 1/p)/(1 + 2α -2/π) if α ≤ (p -π)/(2π).
We present in Figure 1 below a graph to summarize these rates when p = 4.

There are therefore three possible formula for the rate on (1/π -1/p, +∞). The well-known elbow phenomenon refers in literature to the non-differentiability of ψ at (p -π)/(2π) when p > 2 + π, i.e. when moving from the orange zone to the green zone. Actually, ψ is not differentiable at min{ᾱ, 1/π} either. Therefore, there is always at least one elbow effect on (1/π -1/p, +∞) and sometimes two.

Estimation procedure

The remaining part of the paper is devoted to the construction of minimax, or near minimax, adaptive estimators. It will be convenient to use the following notation. To shorten the formulas, we may write I f in place of I f (x) dx and omit the subscript I when I = [0, 1]. For all subset F ⊂ L p ([0, 1]), and f ∈ L p ([0, 1]), we set d p (f, F) = inf g∈F d p (f, g). The notation |I| stands for both the cardinal of a finite set I, and the length of an interval I. We set N = N \ {0}. The letters c, c , C, C , . . . denote quantities that may change from line to line.

Collection of partitions.

We introduce here tree-structured partitions m of [0, 1] derived from the recursive algorithm of [START_REF] Ronald | Degree of adaptive approximation[END_REF] that are frequently encountered when estimating smooth functions by histograms or more generally by piecewise polynomial estimators (see [START_REF] Baraud | Estimating the intensity of a random measure by histogram type estimators[END_REF][START_REF] Akakpo | Adaptation to anisotropy and inhomogeneity via dyadic piecewise polynomial selection[END_REF][START_REF] Sart | Estimation of the transition density of a Markov chain[END_REF] among other references).

Consider a partition m of [0, 1]. We may refine m by dividing some intervals I of m into two equal parts. The collection of all partitions that can be constructed from m by this way is denoted by M(m). We then define collections M of partitions by induction by setting

M 0 = {{[0, 1]}} and M = M -1 ∪ m∈M -1 M(m).
The collection M is therefore composed of partitions of [0, 1] into intervals with endpoints of the form k/2 . It does not only contain the regular partitions of [0, 1] of size 2 k , k ≤ but also partitions that are very thin locally, and wider elsewhere.

We moreover define the collection M ∞ = ≥0 M of partitions m that can be constructed by this algorithm in a finite number of steps.

Projection estimators.

We estimate the density f by means of piecewise polynomial estimators. They are defined as projection estimators as described below.

Consider an integer r, a collection m of disjoint intervals, and the space P r (m) = I∈m P I 1 I , where P I is a polynomial function of degree at most r of piecewise polynomial functions. Let (ϕ I,j ) I∈m,j∈{0,...,r} be the orthonormal basis of P r (m) defined from the Legendre polynomials

Q j (x) = 1 2 j j k=0 j k 2 (x -1) j-k (x + 1) k ,
by the formula

ϕ I,j (x) = 2j + 1 b -a Q j 2 x -a b -a -1 1 I (x),
where a < b denote the extremities of I. We define the projection estimator fm = I∈m j∈{0,...,r} βI,j ϕ I,j with βI,j = 1

n n i=1 ϕ I,j (X i ),
and omit the dependency in r to lighten the notations.

Since their introduction by [START_REF] Cencov | Estimation of an unknown distribution density from observations[END_REF], projection estimators have received considerable interest in statistical estimation. They are at the heart of many model selection procedures, see [START_REF] Birgé | Minimum contrast estimators on sieves: exponential bounds and rates of convergence[END_REF][START_REF] Barron | Risk bounds for model selection via penalization[END_REF][START_REF] Massart | Concentration inequalities and model selection[END_REF] for key references. For pedagogical reasons, we present below a risk bound for this estimator when p = 2:

Proposition 3. Let m be a (finite) partition of [0, 1] into intervals of positive lengths. Then, if f ∈ L 2 ([0, 1]), E f d 2 2 (f, fm ) ≤ d 2 2 (f, P r (m)) + inf q>1 f q (r + 1) 2 I∈m |I| 1-q/(q-1) (q-1)/q n . (3)
The proof of this result is merely based on Hölder's inequality, see Section 4.2. It highlights what will allow us to estimate unbounded densities f of B α π,∞ . When m is a regular partition, that is when the intervals I ∈ m are of the same size, the term in the infimum is f q (r + 1) 2 |m|/n. In particular, by letting q tend to 1,

E f d 2 2 (f, fm ) ≤ d 2 2 (f, P r (m)) + (r + 1) 2 |m| n . (4)
For more general partitions m, and q → +∞,

E f d 2 2 (f, fm ) ≤ d 2 2 (f, P r (m)) + f ∞ (r + 1) 2 |m| n . (5)
These two inequalities apply either for regular partitions, without assumption on f ∞ , or for any partition when f ∞ is finite. More generally, the risk bounds of projection estimators sometimes involve the supremum norm of f , and sometimes not, depending on whether or not the model checks a condition linking the L 2 and L ∞ structure of the model (equation (7.16) in [START_REF] Massart | Concentration inequalities and model selection[END_REF]). For more details on this phenomenon, we refer to [START_REF] Birgé | Model selection for density estimation with L2-loss[END_REF].

It is worth mentioning that (4) and (5) are not suitable for estimating densities f in B α π,∞ (R) when α < 1/π and π < 2. Indeed, such densities may not be bounded and may be poorly approached by piecewise polynomial functions based on regular grids. Making the bias term d 2 2 (f, P r (m)) small requires working with partitions m adapted to the spatial inhomogeneity of f . In some sense, (3) fills the gap between (4) and (5). We can deal with irregular partitions and unbounded densities. The condition on the supremum norm is replaced by a condition on the L q norm. The larger q is, the smaller ( I∈m |I| 1-q/(q-1) ) (q-1)/q is and vice versa.

Two issues remain to be addressed. First, the risk of the estimator depends on the choice of m. We need to explain how to define a partition m realizing a good compromise between the two terms in (3). Second, we need to compute the risk of this estimator when the target f lies in a Besov class. In the section below, we start by answering the first point.

Selection rule.

For all partitions m, m and interval J, we set

m ∨ J = {I ∩ J, I ∈ m} m ∨ m = J∈m m ∨ J = I ∩ J, I ∈ m, J ∈ m .
For all interval I, we define

v p (I) = r j=0 |ϕ I,j | 1 n n i=1 ϕ 2 I,j (X i ) p p and w p (I) = 1 |I| p/2 r j=0 (2j + 1)|ϕ I,j | p p .
We set for any collection m of intervals and ξ > 0,

v p ξ (m) = I∈m ((ξ + log 2 (1/|I|))/n) p/2 v p (I) w p ξ (m) = I∈m ((ξ + log 2 (1/|I|))/n) p w p (I),
where log 2 denotes the logarithm base 2. We consider κ 1 , κ 2 , and

pen p ξ (m) = κ 1 v p ξ (m) + κ 2 w p ξ (m).
We consider some ∈ N ∪ {∞} and define for m ∈ M ,

γ(m) = J∈m sup m ∈M d p p ( fm 1 J , fm∨m 1 J ) -pen p ξ (m ∨ J) . (6)
We then define m as any partition of M satisfying

γ( m) + (1 + 2 1-p ) pen p ξ ( m) ≤ inf m∈M γ(m) + (1 + 2 1-p ) pen p ξ (m) + 1/n 2p , (7)
and shrink the resulting estimator

f = min{1, n f m -1 p } f m.
This criterion can be seen as a Lespki-type procedure [START_REF] Lepski | Asymptotically minimax adaptive estimation. i: Upper bounds. optimally adaptive estimates[END_REF] (see also [START_REF] Baraud | Estimating the intensity of a random measure by histogram type estimators[END_REF]) modified as in [START_REF] Sart | Estimation of the transition density of a Markov chain[END_REF] in order make possible the construction of the estimator by dynamic programming algorithms. We leave these computational aspects aside for the moment to focus on the theoretical properties of f . They will be discussed in Section 3.7.

Risk bound.

We prove in Section 4.3:

Theorem 4. Let r ∈ N, ∈ N ∪ {∞} and p ∈ [1, +∞).
Then, there exists κ depending only on p such that if κ 1 , κ 2 ≥ κ, if ξ = 2p log n + log(r + 1), and if f ∈ L p ([0, 1]), the preceding estimator satisfies for n ≥ f p ,

E f d p p (f, f ) 1/p ≤ C inf m∈M d p (f, P r (m)) + inf q∈[p,+∞] M q (m)v q (m) m + log n n (8) + w(m) m + log n n ,
where m is the smallest value of

N such that m ∈ M m , M q (m) = min{ f q , 1/q m f q/(1+q/(p m)) }, v q (m) = I∈m |I| 1-pq/(2q-p) (2q-p)/(pq) , w(m) = I∈m |I| 1-p 1/p .
Moreover, C only depends on r, p, κ 1 and κ 2 .

Thereby, the risk of the estimator is controlled by the best possible compromise between a bias term d p (f, P r (m)) and an estimation term inf q∈[p,+∞] M q (m)v q (m) ( m + log n)/n + w(m)( m + log n)/n (up to a multiplicative factor). The partitions m can vary freely in M , and can be very thin locally and thus well adapted to the target density f . Note that this result improves with (we can even set = +∞ in theory).

Our theorem applies for any density f ∈ L p ([0, 1]), and in particular for unbounded densities. We may always set q = p in the infimum but playing with larger values of q will be worthwhile as v q (m) is non-increasing with q. The value of q = +∞ is allowed using standard algebra in R ∪ {∞} to deal with bounded f . In that case

M q (m) = f p m ≤ f ∞ and v q (m) = I∈m |I| 1-p/2 2/p .
There are two main differences between the present estimation term and that of Proposition 3. We have here an additional term m + log n which will be of the order of log n for best partitions m and Besov-type regularity constraints. This implies that our results will be slightly sub-optimal in some cases. But this term cannot be avoided in general as (8) leads to the optimal rates in the sparse zone (orange zone of Figure 1), see Section 3.6. The second difference lies in the presence of the additional term w(m)( m + log n)/n. For adequate partitions m, and densities f ∈ B α π,∞ (R), this last term will be, in the worst case, of the same order of magnitude as M q (m)v q (m)( m + log n)/n. 3.5. Approximation. We need to bound (8) from above when f lies in a Besov class to get our maximal risk bound. This problem falls under the theory of approximation and is treated below.

We know from the literature that functions f ∈ B α π,∞ (R) can be well approximated by piecewise polynomial functions defined over a moderate number of intervals. We refer to [DY90, BM00, Aka12]. Let us observe that

v q (m) = I∈m |I| 1-δ 1/δ with δ = pq/(2q -p). (9)
When δ ≤ 1, a concavity argument entails v q (m) ≤ |m|. Moreover, if p = 1, w(m) = |m| and Corollary 3.3 of [START_REF] Ronald | Degree of adaptive approximation[END_REF] may be used to control the right-hand side of (8). In general, however, v q (m) and w(m) may be much larger than |m|: we do not only need to control the size of m but also the thinness of the intervals. The following result, to be proved in Section 4.4, is tailored to solve this problem.

Proposition 5. Let δ ≥ 1, p ∈ [1, +∞), π ∈ (0, p), α > 1/π -1/p, R > 0, f ∈ B α π,∞ (R), r > α -1 and k ≥ 1.
• Suppose that α > δ(1/π -1/p). Then, there exist and m ∈ M such that

d p (f, P r (m)) ≤ CR2 -kα , I∈m |I| 1-δ ≤ C2 kδ ,
and

I∈m |I| 1-p ≤      C2 kp if α > p/π -δ/p C 2 kp if α = p/π -δ/p C2 kπ(α+δ/p)+ π(p/π-δ/p-α) if α < p/π -δ/p. Moreover, ≤ α + δ/p δ/p + α -1/π k.
• Suppose that α < δ(1/π -1/p). Then, there exists a partition m ∈ M with ≤ k such that

d p (f, P r (m)) ≤ CR2 -k(α+1/p-1/π) , I∈m |I| 1-δ ≤ C2 k(δ-1) ,
and if p > δ,

I∈m |I| 1-p ≤ C2 k(p-1) .
• Suppose that α = δ(1/π -1/p). Then, there exists a partition m ∈ M with ≤ k such that

d p (f, P r (m)) ≤ CRk 1/p 2 -k(α+1/p-1/π) , I∈m |I| 1-δ ≤ Ck2 k(δ-1) ,
and if p > δ,

I∈m |I| 1-p ≤ C2 k(p-1) .
In the above inequalities, C depends on α, δ, p, r, π only.

3.6. Minimax bound. We may therefore define partitions m with moderate v q (m) and w(m) that are well adapted to the variations of f . This makes it possible to bound the infimum in (8) from above. We state:

Theorem 6. Let r ≥ 0, p ∈ [1, +∞), and f be the estimator defined in Section 3.3 with κ 1 = κ 2 = κ, = +∞ and ξ given by Theorem 4. For all π ∈ (0, p), α ∈ (1/π -1/p, r + 1) and R > 0, the estimator f satisfies for n large enough,

sup f ∈B α π,∞ (R) E f d p p (f, f ) 1/p ≤ C(log n) τ (log n/n) ψ , ( 10
)
where ψ is defined in Section 2.2 and where τ depends on p, π, α only. If α ∈ (ᾱ, 1/π], or if α > 1/π and α = (p -π)/(2π), then τ = 0. If α > 1/π and α = (p -π)/(2π), τ = 1/p. Moreover, C depends on R, p, π, α only.

Combined with Proposition 2, this theorem says that our estimator f is adaptive and nearminimax over a large scale of Besov classes. It implies Theorem 1. Note that the rate is optimal in the orange zone of Figure 1.

The precise value of ᾱ can be explained by the following reasoning. A function f ∈ B α π,∞ "almost belongs" to L q where 1/q = 1/π -α. Assuming that this is true, we see from Proposition 5 that the change of rates occurs at α = δ(1/π -1/p) with δ = pq/(2q -p). This leads to the equation

α = 1/π -1/p 2/p -1/π + α (11)
for which ᾱ is solution. By the way, slight modifications of the proof entail that τ = 0 when α < 1/π and α < ᾱ when the supremum is taken over all the densities of B α π,∞ (R) whose L q norm is uniformly bounded (with 1/q = 1/π -α).

When π ≥ p, the functions in B α π,∞ (R) can be approached by piecewise polynomial functions based on regular partitions, see Lemma 12 of [START_REF] Barron | Risk bounds for model selection via penalization[END_REF]. More precisely, for every α > 0 and k ≥ 1, there is a regular partition m of size 2 k such that d p (f, P r (m)) ≤ CR2 -kα . For such a partition, v q (m) = w(m) = |m|. By putting these results in (8), we deduce that our estimator achieves the rate (log n/n) α/(1+2α) over the Besov classes B α π,∞ (R) for all π ≥ p and α ∈ (0, r+1).

Computational statistics.

To compute our estimator, we have to minimize γ(m) + (1 + 2 1-p ) pen p ξ (m) on the set of partitions m of M . It is not advisable, in practice, to solve this optimization problem by an exhaustive search of m among all the partitions of M . This is due to the very large cardinal of M , even when is moderate. Actually, the calculation of γ(m) itself is an optimization problem that can hardly be solved by a naive approach.

Fortunately, dynamic programming allows here to build the estimator more efficiently. We refer to [Don97, BSR04, AL11, [START_REF] Akakpo | Adaptation to anisotropy and inhomogeneity via dyadic piecewise polynomial selection[END_REF][START_REF] Sart | Estimation of the transition density of a Markov chain[END_REF] for some examples of this technique in statistics. In particular, we may slightly adapt the algorithm of [START_REF] Sart | Estimation of the transition density of a Markov chain[END_REF] to perform the exact computation of m in at most C (2 + n) operations (see his Proposition A.1). The term C does not depend on , n and by operations we mean elementary operations such as additions, multiplications etc., computation of elementary functions or integrals. Naturally, the numerical complexity of the procedure increases with . Since the theoretical results improve with , the choice of is, at first sight, a sort of compromise between the theoretical and computational properties of the estimator.

One may, however, in practice, be interested only in linear (or polynomial) time estimators. This is equivalent to setting and looking for the classes of functions on which our estimator is (nearly) rate optimal. We show:

Proposition 7. Let p ∈ [1, +∞), π ∈ (0, p), r ≥ 0, α ∈ (1/π -1/p,
r + 1) and R > 0. Let c and be the largest integer such that 2 ≤ n c , κ 1 = κ 2 = κ and f be the estimator defined in Section 3.3.

Then, if p > 1 and c = p/(p -1), or if c = 1 and α > 1/π, the estimator satisfies (10) for n large enough.

The numerical complexity of our procedure is of the order of n c (log n). By setting c = 1, we get the preceding rates under the standard condition α > 1/π in nearly linear time. When p > 1, we may set c = p/(p -1) to get all the rates in polynomial time.

Remark: the minimum length of an interval of a partition m ∈ M is 2 -. In particular, it is not necessary to go below 1/n to be (near) optimal when α > 1/π. We need to cross this threshold to estimate unbounded densities corresponding to smaller values of α.

Proofs

R p B α π,∞ (R) ≥ c(1/n) (α+1/p-1/π)/(1+α-1/π)
. This inequality can be shown by slightly adapting the arguments of [START_REF] Birgé | Model selection for density estimation with L2-loss[END_REF] to the case p = 2. It is actually attained on a two-point problem {f 1 , f 2 }.

Consider α ∈ [1/π -1/p, 1/π], p > 1 and a density ϕ ∈ B α π,∞ with support included in (0, 1). We set ϕ(x) = 0 for |x| > 1, define ρ = min{R, R/ ϕ p }/ max{|ϕ| B α π,∞ , 1}, a such that a 1+α-1/π = ρ(4n) 1/π-α and g(x) = aϕ(4anx). We suppose from now on that n is large enough to ensure that g is compactly supported on

[0, 1/2]. Moreover, |g| B α π,∞ = ρ|ϕ| B α π,∞ and g p = ε where ε = ρ (1-1/p)/(1+α-1/π) (1/(4n)) (α+1/p-1/π)/(1+α-1/π) ϕ p . Define now f 1 for all x ∈ [0, 1] by f 1 (x) = g(x) + 1 -1/(4n), and set f 2 (x) = f 1 (1 -x).
Then, f 1 and f 2 are two densities such that

|f 1 | B α π,∞ = |f 2 | B α π,∞ = |g| B α π,∞ = ρ|ϕ| B α π,∞ and max{ f 1 p , f 2 p } ≤ 1 + g p ≤ 1 + ε.
Since g(x) and g(1 -x) cannot be simultaneously non-zero,

f 2 -f 1 p = 2 1/p g p = 2 1/p ε.
Let h be the Hellinger distance. Then,

h 2 (f 1 , f 2 ) = 1 2 R f 1 (x) -f 2 (x) 2 dx = 1/(4an) 0 g(x) + 1 -1/(4n) -1 -1/(4n) 2 dx ≤ 1/(4an) 0 g(x) dx ≤ 1/(4n).
Our lower bound when α ≥ 1/π -1/p then follows from standard results in minimax estimation. We refer, for instance, to Proposition 5 of [START_REF] Birgé | Model selection for density estimation with L2-loss[END_REF]. As to the case, α < 1/π -1/p, we use B

1/π-1/p π,∞ (R) ⊂ B α π,∞ (
R) and apply the previous result with α = 1/π -1/p.

Proof of Proposition 3.

Let f m be the L 2 projection of f on P r (m) defined by

f m = β I,j ϕ I,j with β I,j = ϕ I,j f = E[ βI,j ],
where the sum runs over the intervals I ∈ m and j ∈ {0, . . . , r}. Pythagoras' theorem implies

d 2 2 (f, fm ) = d 2 2 (f, f m ) + βI,j -β I,j 2 = d 2 2 (f, P r (m)) + βI,j -E[ βI,j ] 2 .
Therefore,

E d 2 2 (f, fm ) ≤ d 2 2 (f, P r (m)) + A/n with A = ϕ 2 I,j f.
We use ϕ I,j ∞ = (2j + 1)/|I| to get

A ≤ (r + 1) 2 I∈m 1 |I| I f,
and apply Hölder's inequality twice:

A ≤ (r + 1) 2 I∈m I f q 1/q |I| -1/q ≤ (r + 1) 2 f q I∈m |I| -1/(q-1)
(q-1)/q . 4.3. Proof of Theorem 4. We define the collection I ∞ gathering all the dyadic intervals that appear in the partitions m of M ∞ , that is, all the intervals with endpoints k2 -, (k + 1)2 - where k ∈ {0, . . . , 2 -1} and ≥ 0. Without loss of generality, we may assume that these intervals are of the form [a, b) when b < 1 and [a, b] when b = 1.

We set for I ∈ I ∞ , collection m of intervals and ξ > 0,

v p id (I) = r j=0 |ϕ I,j | E[ϕ 2 I,j (X)] p p , v p id,ξ (m) = I∈m ((ξ + log 2 (1/|I|))/n) p/2 v p id (I), pen p id,ξ (m) = v p id,ξ (m) + w p ξ (m).
We begin by proving a uniform risk bound in deviation for the projection estimators:

Lemma 1. For all r ∈ N, f ∈ L p ([0, 1]), ξ ≥ log 4 + log(r + 1) and probability larger than 1 -(1/2)e -ξ : for all J ∈ I ∞ , and m ∈ M ∞ ,

d p p (f 1 J , fm∨J 1 J ) ≤ c 1 d p p (f 1 J , P r (m ∨ J)) + c 2 pen p id,ξ (m ∨ J),
where c 1 only depends on p, r and where c 2 only depends on p.

Proof of Lemma 1. Let f m∨J be the L 2 projection of f on P r (m ∨ J) defined by

f m∨J = I∈m∨J j∈{0,...,r} β I,j ϕ I,j with β I,j = f ϕ I,j = E[ βI,j ].
By using the triangle inequality, and the elementary inequality (a + b) p ≤ 2 p-1 (a p + b p ),

d p p (f 1 J , fm∨J 1 J ) ≤ 2 p-1 d p p (f 1 J , f m∨J 1 J ) + d p p (f m∨J 1 J , fm∨J 1 J ) . (12)
It follows from standard results about the L p norm of the L 2 projection operator that

d p (f 1 J , f m∨J 1 J ) ≤ cd p (f 1 J , P r (m ∨ J)), (13)
where c only depends on r. We refer for instance to the argument below Lemma 3 of [START_REF] Birgé | An adaptive compression algorithm in Besov spaces[END_REF] for the proof of this inequality. We now tackle the second term in (12). Consider ≥ 0, and note that the intervals of I = {I ∈ I ∞ , |I| = 2 -} are of the form [k/2 , (k +1)/2 ) (the interval is closed when (k +1)/2 = 1). In particular, |I | = 2 . We deduce from Bernstein's inequality (Theorem 2.10 of [START_REF] Boucheron | Concentration inequalities: A nonasymptotic theory of independence[END_REF]) that there exists for each interval I ∈ I and j, an event Ω(I, j) of probability 1 -e -ξ with ξ = 2ξ + 2 log 2 on which

| βI,j -β I,j | ≤ 2(ξ /n)E f [ϕ 2 I,j (X)] + ξ /(3n) ϕ I,j ∞ . ( 14
)
We then set Ω ξ = I∈I ≥0 j∈{0,...,r} Ω(I, j), and deduce from a union bound

P Ω c ξ ≤ (r + 1) ≥0 |I |e -ξ ≤ (r + 1) ≥0 2 e -2ξ-2 log 2 ≤ 2(r + 1)e -2ξ ,
which is not larger than (1/2)e -ξ as ξ ≥ log 4 + log(r + 1).

On the event Ω ξ , (14) holds true simultaneously for all I ∈ I ∞ , j ∈ {0, . . . , r} with such that 2 -= |I|. Now, for m ∈ M ∞ , and J ∈ I ∞ ,

d p p (f m∨J 1 J , fm∨J 1 J ) = I∈m∨J j∈{0,...,r} βI,j -β I,j ϕ I,j p ≤ I∈m∨J   j∈{0,...,r} βI,j -β I,j |ϕ I,j |   p .
As m ∨ J ⊂ I ∞ , we may use (14), and then (a + b) p ≤ 2 p-1 (a p + b p ), ϕ I,j ∞ = (2j + 1)/|I| to conclude the proof.

Lemma 2. For all r ∈ N, ξ ≥ log 4 + log(r + 1) and f ∈ L p ([0, 1]), the following assertion holds true with probability larger than 1 -(1/2)e -ξ : for all m ∈ M ∞ , J ∈ I ∞ ,

pen p id,ξ (m ∨ J) ≤ pen p ξ (m ∨ J) ≤ c 3 pen p id,ξ (m ∨ J), (15)
provided that κ 1 , κ 2 ≥ κ for some κ depending only on p and where c 3 only depends on κ 1 , κ 2 , p.

Proof of Lemma 2. As in the previous proof, we may apply Bernstein's inequality to get with probability 1 -(1/2)e -ξ : for all j ∈ {0, . . . , r}, and

I ∈ I ∞ , 1 n n i=1 ϕ 2 I,j (X i ) -E f [ϕ 2 I,j (X)] ≤ 2(ξ /n)E f [ϕ 4 I,j (X)] + (ξ /(3n)) ϕ I,j 2 ∞ ≤ 2(ξ /n) ϕ I,j 2 ∞ E f [ϕ 2 I,j (X)] + (ξ /(3n)) ϕ I,j 2
∞ ,
where is such that 2 -= |I| and ξ = 2ξ + 2 log 2. By using the elementary inequality √ 2ab ≤ a/2 + b,

1 n n i=1 ϕ 2 I,j (X i ) -E f [ϕ 2 I,j (X)] ≤ 1 2 E f [ϕ 2 I,j (X)] + (4/3)(ξ /n) ϕ I,j 2 ∞ .
Therefore,

1 n n i=1 ϕ 2 I,j (X i ) ≤ (3/2)E f [ϕ 2 I,j (X)] + (4/3)(ξ /n) ϕ I,j 2 ∞ E f [ϕ 2 I,j (X)] ≤ 2 n n i=1 ϕ 2 I,j (X i ) + (8/3)(ξ /n) ϕ I,j 2 ∞ ,
which leads to the result after some computations.

Proposition 8. Let r ∈ N, ξ > 0, ∈ N ∪ {∞} and m be a partition satisfying (7). Then if κ 1 , κ 2 ≥ κ for some κ depending only on p, and if f ∈ L p ([0, 1]), the following assertion holds true: for all ξ ≥ log 4 + log(r + 1) with probability 1 -e -ξ :

d p p (f, f m) ≤ C inf m∈M d p p (f, P r (m)) + pen p id,ξ (m) + 1/n 2p . ( 16
)
In this inequality, C depends on p, r, κ 1 , κ 2 only.

Proof of Proposition 8. Up to an increase of κ, the two preceding lemmas assert: with probability 1 -e -ξ , for all m ∈ M , J ∈ I ∞ , κ 1 , κ 2 ≥ κ,

2 p-1 d p p (f 1 J , fm∨J 1 J ) ≤ cd p p (f 1 J , P r (m ∨ J)) + pen p ξ (m ∨ J), (17)
where c depends on p and r only. In the sequel, we repeatedly use the inequality (a + b) p ≤ 2 p-1 (a p + b p ) without mentioning it again. The triangle inequality implies

γ(m) ≤ 2 p-1 d p p (f, fm ) + J∈m sup m ∈M 2 p-1 d p p (f 1 J , fm ∨J 1 J ) -pen p ξ (m ∨ J) ,
and (17) ensures

γ(m) ≤ 2 p-1 d p p (f, fm ) + J∈m sup m ∈M cd p p (f 1 J , P r (m ∨ J)) ≤ 2 p-1 d p p (f, fm ) + cd p p (f, P r (m)) ≤ 2cd p p (f, P r (m)) + pen p ξ (m). ( 18
)
The triangle inequality entails for all m ∈ M ,

d p p (f, f m) ≤ 2 p-1 d p p (f, f m∨m ) + pen p ξ ( m ∨ m) + d p p ( f m, f m∨m ) -pen p ξ ( m ∨ m) ≤ 2 p-1 d p p (f, f m∨m ) + pen p ξ ( m ∨ m) + J∈ m d p p ( f m1 J , f m∨m 1 J ) -pen p ξ (m ∨ J) .
We apply (17) with the inequalities pen p ξ ( m ∨ m) ≤ pen p ξ ( m) + pen p ξ (m) (as m ∨ m ⊂ m ∪ m) and d p p (f, P r ( m ∨ m)) ≤ d p p (f, P r (m)) to deduce,

d p p (f, f m) ≤ 2 p-1 c d p p (f, P r (m)) + (1 + 2 1-p ) pen p ξ (m) + J∈ m d p p ( f m1 J , f m∨m 1 J ) -pen p ξ (m ∨ J) + (1 + 2 1-p ) pen p ξ ( m) .
By using (6), and taking the infimum over all the partitions m ∈ M ,

d p p (f, f m) ≤ 2 p-1 inf m∈M c d p p (f, P r (m)) + (1 + 2 1-p ) pen p ξ (m) + 2 p-1 γ( m) + (1 + 2 1-p ) pen p ξ ( m) ,
and (7) entails

d p p (f, f m) ≤ 2 p-1 inf m∈M c d p p (f, P r (m)) + 2(1 + 2 1-p ) pen p ξ (m) + γ(m) + 1/n 2p .
We then use (18) to get

d p p (f, f m) ≤ C inf m∈M d p p (f, P r (m)) + pen p ξ (m) + 1/n 2p ,
and apply (15).

Lemma 3. For all m ∈ M ∞ , ξ > 0 and q ∈ [p, +∞],

pen p id,ξ (m) ≤ C ((ξ + m )/n) p/2 M p/2 q (m)v p/2 q (m) + ((ξ + m )/n) p w p (m) ,
where C only depends on p and r.

Proof. Since |I| ≥ 2 -m for all I ∈ m, v p id,ξ (m) ≤ ((ξ + m )/n) p/2 I∈m I r j=0 |ϕ I,j | I f ϕ 2 I,j p .
We use ϕ I,j ∞ = (2j + 1)/|I| to get

v p id,ξ (m) ≤ ((ξ + m )/n) p/2 I∈m I r j=0 2j + 1 |I| I f p ≤ ((ξ + m )/n) p/2 (r + 1) 2p A with A = I∈m I f p/2 |I| 1-p . ( 19
)
We now bound above A by repeatedly using Hölder's inequality as in the proof of Proposition 3.

First, we use it twice to get for every q ≥ p, A ≤

I∈m I f q p/(2q)
|I| 1-p/2(1+1/q) ≤ f p/2 q v p/2 q (m). (20) Second, let q ≥ p/2 such that 1/q = 1/q + 1/(p m ) and for j ≥ 0, m j = {I ∈ m, |I| = 2 -j }, I j = ∪ I∈m j I. We deduce,

A ≤ m j=0 f 1 I j p/2 q |m j | 1-p/(2q ) 2 -j(1-p/2(1+1/q )) ≤ f p/2 q 2 1/2 m j=0 |m j | 1-p/(2q) 2 -j(1-p/2(1+1/q)) ≤ f p/2 q 2 1/2 ( m + 1) p/(2q)   m j=0 |m j |2 -j(1-p/2(1+1/q))2q/(2q-p)   1-p/(2q) ≤ f p/2 q 2 1/2 ( m + 1) p/(2q) v p/2 q (m).
By combining this result together with ( 20) and ( 19), we obtain

v p id,ξ (m) ≤ C ((ξ + m )/n) p/2 M p/2 q (m)v p/2 q (m).
We now turn to the term w p ξ (m). We have, Proof of Theorem 4. We denote by x + the positive part of a real number x. We have,

w p ξ (m) = I∈m ((ξ + log 2 (1/|I|))/n) p w(I) p ≤ ((ξ + m )/n) p I∈m 1 |I| p/2
d p ( f m, f ) = ( f m p -n) + ≤ ( f m p -f p ) + as f p ≤ n. Therefore, d p ( f m, f ) ≤ d p (f, f m) and d p (f, f ) ≤ 2d p (f, f m).
We apply Proposition 8 to define an event Ω ξ of probability 1 -e -ξ on which (16) holds true. By using moreover

d p (f, f ) ≤ f p + f p ≤ 2n, E f d p p (f, f ) ≤ E f d p p (f, f )1 Ω ξ + (2n) p e -ξ ≤ 2 p E f d p p (f, f m)1 Ω ξ + (2n) p e -ξ .
Since ξ ≥ 2p log n, and w(m) ≥ 1 for all m, (2n) p e -ξ ≤ 2 p (w(m)/n) p . We then bound d p p (f, f m) thanks to (16) and Lemma 3. 4.4. Proof of Proposition 5. We introduce for each interval I the space P r (I) = {P 1 I , where P is a polynomial function of degree at most r} composed of polynomial functions on I. We need the following claim: Claim 1. Let j ∈ N and mj be the regular partition of [0, 1] of size 2 j . Then, for all p ∈

[1, +∞], π ∈ (0, p), α > 1/π -1/p, r > α -1, R > 0 and f ∈ B α π,∞ (R),   I∈ mj d π p (f 1 I , P r (I))   1/π ≤ C (1 + 1/τ ) R2 -jτ ,
where τ = α + 1/p -1/π and where C depends on π, r only.

This claim is a slight revisit of Lemma 1 of [START_REF] Akakpo | Adaptation to anisotropy and inhomogeneity via dyadic piecewise polynomial selection[END_REF] in a unidimensional context. Note that it holds for all f ∈ B α π,∞ (R) whereas her result is restricted to functions f ∈ B α π,π (R) when π ∈ (1, p). The term in front of R2 -jτ is also made more explicit here (which will be of interest for the proof of Theorem 6).

Sketch of the proof of Claim 1. We make the following minor modification in the proof of [START_REF] Akakpo | Adaptation to anisotropy and inhomogeneity via dyadic piecewise polynomial selection[END_REF]. Instead of applying Hölder's inequality to her inequality (27), we apply Minkowski's integral inequality. By using her notations, this yields

2 jdτ σ/H(σ)   K∈D σ j E p r (s, K) q   1/p ≤ C(d, r, σ, p, q)2 jdτ σ/H(σ) k≥j    K∈D σ j 2 -kdτ σ/H(σ) 2 kσ e k (s, K) p    1/p
where the term C(d, r, σ, p, q) comes from her equation ( 19).

If we go back to her calculations, we can observe that C(d, r, σ, p, q) does not depend on σ in a unidimensional setting (as σ = H(σ)). Moreover, the dependency on q comes from her equation (20), and can be removed thanks to Theorem 2.6 in Chapter 4 of [START_REF] Ronald | Constructive approximation[END_REF]. We therefore write C(r, p) in place of C(d, r, σ, p, q) (as d = 1).

We thus have,

2 jdτ σ/H(σ)   K∈D σ j E p r (s, K) q   1/p ≤ C(r, p)2 jdτ σ/H(σ) k≥j 2 -kdτ σ/H(σ) 2 kσ e k (s, [0, 1] d ) ≤ C(r, p) 1 -2 -dτ σ/H(σ) -1 sup k≥j 2 kσ e k (s, [0, 1] d ) ,
which gives the result using 1 -

2 -dτ σ/H(σ) -1 = (1 -2 -τ ) -1 ≤ (1/ log(2))(1 + 1/τ ).
We now prove the following lemma.

Lemma 4. Let (η j ) j≥0 be a sequence of numbers that is bounded below by a positive constant.

Let p ≥ 1, π ∈ (0, p), α > 1/π -1/p, r > α -1, R > 0 and f ∈ B α π,∞ (R).
Then, there exists m ∈ M ∞ such that m j = I ∈ m, |I| = 2 -j satisfies for all j ≥ 1,

|m j | ≤ min C R 2 -(j-1)τ η j-1 π , 2 j , (21)
where τ = α + 1/p -1/π and where C depends on p, π, r, α only. Moreover,

d p p (f, P r (m)) ≤ ∞ j=0 |m j |η p j . (22)
Remark: the construction of the partition m is the same to that of [START_REF] Ronald | Degree of adaptive approximation[END_REF] when the sequence (η j ) j is constant.

Proof of Lemma 4. We begin by defining two preliminary collections mj , m j of disjoint intervals of [0, 1] by induction.

When d p (f 1 [0,1] , P r ([0, 1])) ≤ η 0 , we set ( m0 , m 0 ) = ( m0 , ∅) and when d p (f 1 [0,1] , P r ([0, 1])) > η 0 , we set ( m0 , m 0 ) = (∅, m0 ). We then define mj and m j from mj-1 , m j-1 by mj = {I ∈ mj , ∃I ∈ m j-1 such that I ⊂ I and d p (f 1 I , P r (I)) ≤ η j } m j = {I ∈ mj , ∃I ∈ m j-1 such that I ⊂ I and d p (f 1 I , P r (I)) > η j }.

Therefore, mj , m j are subsets of mj , mj ∪ m j is a partition of ∪ I ∈ m j-1 I and

d p (f 1 I , P r (I)) ≤ η j for all I ∈ mj d p (f 1 I , P r (I)) > η j for all I ∈ m j . For every k, m k = k j=0 mj ∪ m k is a partition of [0, 1]
. Moreover, we derive m k from m k-1 by dividing some of its intervals in two equal parts (more precisely, we divide the intervals of m k-1 ). Therefore, m k ∈ M( m k-1 ) and m k ∈ M for some , see Section 3.1.

Since (η j ) j is bounded below, we may define the smallest such that m = ∅. We then set m = m = j=0 mj . Note that mj = m j = I ∈ m, |I| = 2 -j and m ∈ M .

We now show the bound on |m j | = | mj | for j ≥ 1. For all I ∈ mj , there exists I ∈ m j-1 such that I ⊂ I . Therefore, (η j-1 ) π < d π p (f 1 I , P r (I )), and hence

(η j-1 ) π | mj | < I∈ mj d π p (f 1 I , P r (I )) < J∈ m j-1 I∈ mj I =J d π p (f 1 J , P r (J)) < 2 J∈ m j-1 d π p (f 1 J , P r (J)).
By using m j-1 ⊂ mj-1 and Claim 1,

(η j-1 ) π | mj | < 2 C R2 -(j-1)τ π ,
which shows the first bound in (21). As to the second one, we merely use that mj ⊂ mj and

| mj | = 2 j . Now, d p p (f, P r (m)) = I∈m d p p (f 1 I , P r (I)) ≤ ∞ j=0 I∈m j d p p (f 1 I , P r (I)) ≤ ∞ j=0 |m j |η p j ,
which shows (22).

Proof of Proposition 5. We apply Lemma 4 with

η j = C 1/π R2 (j+1)(δ-1)/p+τ -k(α+δ/p) if α > δ(1/π -1/p) C 1/π R2 (j+1)(δ-1)/p+τ -k(τ +(δ-1)/p) if α ≤ δ(1/π -1/p). ( 23
)
We deduce a partition m with |m j | such that

|m j | 1/π ≤ 2 k(α+δ/p) 2 -j(α+δ/p-1/π) if α > δ(1/π -1/p) 2 (k-j)(τ +(δ-1)/p) if α ≤ δ(1/π -1/p). (24)
In the first case, |m j | = 0 when j > (α + δ/p)/(α + δ/p -1/π)k, which shows that m ∈ M . As to the second case, we have |m j | = 0 when j > k and thus m ∈ M k .

Note now that

I∈m |I| 1-δ = ∞ j=0 |m j |2 j(δ-1) . ( 25
)
By using |m j | ≤ 2 j and (24), we get in the first case

I∈m |I| 1-δ ≤ k j=0 2 j 2 j(δ-1) + 2 kπ(α+δ/p) ∞ j=k+1 2 -j(α+δ/p-1/π)π 2 j(δ-1) ≤ 2 (k+1)δ 2 δ -1 + 2 kπ(α+δ/p) 2 -(k+1)(α-δ(1/π-1/p))π 1 -2 -(α-δ(1/π-1/p))π ≤ C 2 kδ , (26)
where C depends on α, δ, p, π.

As to the second case, we use that |m j | = 0 for j > k and (24) to get

I∈m |I| 1-δ ≤ k j=0
2 (k-j)(τ +(δ-1)/p)π 2 j(δ-1) ≤ 2 kπ(τ +(δ-1)/p) k j=0 2 j((1-π/p)(δ-1)-πτ ) . (27) When the condition on α is strict, (1 -π/p)(δ -1) -πτ > 0, and thus,

I∈m |I| 1-δ ≤ 2 kπ(τ +(δ-1)/p) × C 2 k((1-π/p)(δ-1)-πτ ) ≤ C 2 k(δ-1) , (28)
where C depends on p, π, α, δ only.

Suppose now that α = δ(1/π -1/p). Then, we put the inequalities (1 -π/p)(δ -1) -πτ = 0 and π(τ

+ (δ -1)/p) = δ -1 into (27) to derive I∈m |I| 1-δ ≤ C k2 k(δ-1) . ( 29
)
We now prove the bounds on d p p (f, P r (m)). We use ( 22) and ( 23) to get in the first case,

d p p (f, P r (m)) ≤ C p/π R p 2 -kp(α+δ/p)+pτ +δ-1 ∞ j=0 |m j |2 j(δ-1) ,
and in the second case

d p p (f, P r (m)) ≤ C p/π R p 2 -kp(τ +(δ-1)/p)+pτ +δ-1 ∞ j=0 |m j |2 j(δ-1) .
We then bound the sum by using (25) (26), ( 28) and (29).

We finally prove the bounds on

I∈m |I| 1-p = ∞ j=0 |m j |2 j(p-1) .
When α > δ(1/π -1/p), and α ≥ p/π -δ/p,

I∈m |I| 1-p ≤ k j=0 2 j 2 j(p-1) + 2 kπ(α+δ/p) j=k+1 2 -jπ(α+δ/p-1/π) 2 j(p-1) ≤ 2 (k+1)p 2 p -1 + 2 kπ(α+δ/p) j=k+1 2 -jπ[α-(p/π-δ/p)] (30) and j=k+1 2 -jπ[α-(p/π-δ/p)] ≤ C 2 -kπ[α-(p/π-δ/p)] if α > p/π -δ/p -k if α = p/π -δ/p.
We put this inequality in (30) to get the bound. When α > δ(1/π -1/p), and α < p/π -δ/p, we have

I∈m |I| 1-p ≤ 2 kπ(α+δ/p) j=0 2 -jπ(α+δ/p-1/π) 2 j(p-1) ≤ 2 kπ(α+δ/p) j=0 2 -jπ[α-(p/π-δ/p)] ≤ 2 kπ(α+δ/p) × C 2 -π[α-(p/π-δ/p)] ,
which implies the bound. When α ≤ δ(1/π -1/p),

I∈m |I| 1-p ≤ k j=0 2 (k-j)(τ +(δ-1)/p)π 2 j(p-1)
≤ 2 kπ(α-1/π+δ/p) k j=0 2 jπ(p/π-δ/p-α) .

Since δ < p, we have p/π -δ/p -α > 0 and

I∈m |I| 1-p ≤ C 2 kπ(α-1/π+δ/p) 2 kπ(p/π-δ/p-α) ≤ C 2 (p-1)k .
4.5. Proof of Theorem 6. It is well known that there is an embedding of Besov spaces into L q spaces, see [START_REF] Ronald | Interpolation of Besov spaces[END_REF][START_REF] Devore | Nonlinear approximation[END_REF]. We use here the following lemma. It will be proved after the present proof for the sake of completeness.

Lemma 5. Let f be a density belonging to B α π,∞ (R) for some π, α > 0. Then, for all q ∈ [1, +∞] such that 1/q > 1/π -α,

f q ≤ c q (1 + R), (31)
where c q depends on π, α, q only. Moreover c q ≤ c(1 + 1/(α -1/π + 1/q)) for some c depending only on π, α.

We recall that ᾱ is the unique positive solution of (11) that is α = (1/π -1/p)/(2/p -1/π + α). Define, when α ≤ 1/π, q α = π/(1 -πα), 1/δ α = 2/p -1/q α = 2/p -1/π + α. Every α ∈ ( ᾱ, 1/π] satisfies α > δ α (1/π -1/p) and every α ∈ (1/π -1/p, ᾱ] satisfies α ≤ δ α (1/π -1/p).

Suppose that α ∈ ( ᾱ, 1/π]. Let ε > 0 be small enough such that α > (1/π -1/p)/(2/p -(1/q α + ε)).

Let q α ≥ p such that 1/q α = 1/q α + ε and 1/δ α = 2/p -1/q α . We apply Proposition 5 with k defined as the smallest integer larger than

1 1 + 2α log 2 R 2 1 + R n log n , (32)
and δ = max{1, δ α }. We therefore get a partition m ∈ M such that d p (f, P r (m)) ≤ CR2 -kα ,

I∈m |I| 1-δ 1/δ ≤ C2 k , (33) and w(m) ≤      C2 k if α > p/π -δ/p C 2 k if α = p/π -δ/p C2 (π/p)[k(α+δ/p)+ (p/π-δ/p-α)] if α < p/π -δ/p. (34)
We use (33) with a concavity argument when δ α < 1 to get

v q α (m) = I∈m |I| 1-δ α 1/δ α ≤ C2 k .
Moreover, we have

≤ α + δ/p δ/p + α -1/π k. (35)
Lemma 5 implies that M q α (m) ≤ f q α ≤ c(1 + R) for some c. Due to our choice of k, we have for n large enough, using m ≤ c log n for some suitable c ,

d p (f, P r (m)) + M q α (m)v q (m) m + log n n ≤ C R 1/(1+2α) (1 + R) log n n 1/(1+2α)
.

We now claim that the term w(m)( m + log n)/n in (8) is negligible when n is large. This is indeed straightforward when α ≥ p/π -δ/p as our bounds for w(m) and v q α (m) are of the same order of magnitude (up to a logarithmic term in case of equality). When α < p/π -δ/p, we have, using (34) and (35), w(m) ≤ C 2 k(α+δ/p)(1-1/p)/(δ/p+α-1/π) .

We apply the claim below (proved after the present proof) to get w(m) ≤ C 2 kβ(1+α) for some β < 1.

Claim 2. The following inequality holds true: for all

α ∈ (1/π -1/p, 1/π], q ∈ [p, π/(1 -πα)], π ∈ (0, p), 1/δ = 2/p -1/q such that α > δ (1/π -1/p), (α + δ/p)(1 -1/p) < (1 + α)(δ/p + α -1/π),
where δ = max{1, δ }.

It follows from the definition of k that for n large enough,

w(m) m + log n n ≤ C R 2 /(1 + R) β(1+α)/(1+2α) log n n (1+2α-β(1+α))/(1+2α)
.

As β < 1, the exponent is always larger than α/(1 + 2α), and the term is negligible. Since f p ≤ f q α ≤ c(1 + R), we may apply Theorem 4 to get the result for n large enough.

Suppose now that α ∈ (1/π -1/p, ᾱ) and α ≤ 1/π. Then, α < δ α (1/π -1/p). Since α > 1/π -1/p, we may suppose that δ α > 1. Let k be the smallest integer larger than

1 2(α -1/π + 1/p) + 1 -1/δ α log 2 R 2 1 + R n log n . ( 36
)
We derive from the second point of Proposition 5 a partition m ∈ M k such that

v qα (m) ≤ C2 k(1-1/δα) , w(m) ≤ C2 k(1-1/p) , and d p (f, P r (m)) ≤ CR2 -k(α+1/p-1/π) .
Lemma 5 ensures that f qα/(1+qα/(pk)) ≤ ck(1 + R), for some c depending only on π, α and p. We may thus apply Theorem 4 to get when n is large enough,

E f d p p (f, f ) 1/p ≤ C R2 -k(α+1/p-1/π) + (1 + R)k 1/qα+1 2 k(1-1/δα) k + log n n +2 k(1-1/p) k + log n n .
By replacing k by (36), we observe that the first three terms are all of the same order of magnitude (up to log terms). We then use Lemma 5 to bound the L p norm of f in the remaining term.

In borderline case α = ᾱ, and α ≤ 1/π, we do as above. We simply apply the third point of Proposition 5 instead of the second one, which leads to additional logarithmic factors in the final result.

The proof when α > 1/π is quite similar. We set from now on q α = ∞, δ α = p/2. Suppose that α > δ α (1/π -1/p). We apply Proposition 5 with k defined as the smallest integer larger than (32) and δ = max{1, δ α }. We therefore get a partition m ∈ M such that d p (f, P r (m)) ≤ CR2 -kα , v ∞ (m) ≤ C2 k , and w(m) bounded from above by (34). Lemma 5 ensures that f ∞ ≤ c(1 + R), and we apply Theorem 4. We finally use (35) and the claim below to show that w(m)( m + log n)/n is negligible when α < p/π -δ/p. Claim 3. The following inequality holds true: for all α > 1/π, π ∈ (0, p), such that α > (p/2)(1/π -1/p),

(α + δ/p)(1 -1/p) < (1 + α)(δ/p + α -1/π),
where δ = max{1, p/2}. When α < δ α (1/π -1/p), we may suppose that δ α = p/2 ≥ 1 and define k as the smallest integer such that (36) holds true (with the present value of δ α ). We derive from the second point of Proposition 5 a partition m ∈ M k such that v ∞ (m) ≤ C2 k(1-1/δα) , w(m) ≤ C2 k(1-1/p) , and d p (f, P r (m)) ≤ CR2 -k(α+1/p-1/π) . By using f p ≤ f ∞ ≤ c(1 + R), Lemma 5 and Theorem 4, we have for n large enough

E f d p p (f, f ) 1/p ≤ C R2 -k(α+1/p-1/π) + (1 + R)2 k(1-1/δα) k + log n n +2 k(1-1/p) k + log n n .
By replacing k by (36), the first two terms are of the order of ((log n)/n) (α-1/π+1/p)/(2α-2/π+1) and the third one ((log n)/n) (2α-2/π+1/p)/(2α-2/π+1) . It is therefore negligible compared to the first two terms as α > 1/π.

Finally, when α = δ α (1/π -1/p), we do as above, but additional logarithmic factors appear as we apply the third point of Proposition 5.

Proof of Lemma 5. We apply Claim 1 in Section 4.4 with j = 0, p replaced by q, and with r defined as the smallest integer larger than α. Then, there is a polynomial function g of degree at most r such that

d q (f, g) ≤ C 1 + 1 α -1/π + 1/q R, (37)
where C depends on α and π only. Since g is a polynomial function, there exists C depending only on r such that g q ≤ C g 1 (see Theorem 2.6 in Chapter 4 of [START_REF] Ronald | Constructive approximation[END_REF]). Therefore, using the triangle inequality,

g q ≤ C [d 1 (f, g) + f 1 ] ≤ C [d q (f, g) + 1] . (38)
We finally put f q ≤ d q (f, g) + g q , (37) and (38) together.

Proof of Claim 2. We first suppose that δ ≥ 1. Then, Finding a root of the quadratic polynomial amounts to solving (11). The only positive root is therefore ᾱ. Since α > δ (1/π -1/p) ≥ (1/π -1/p)/(2/p -1/π + α), α is larger than ᾱ and the above quantity is always positive.

Suppose now that δ < 1. Then, α > 1 + 1/π -2/p ≥ 1/π -1/p, and

(1 + α)(δ/p + α -1/π) -(α + δ/p)(1 -1/p) = (α + 1/p) 2 -(1 + α)/π.

The right-hand side of this inequality is an increasing function of α on [1/(2π) -1/p, +∞) ⊃ [1/π -1/p, +∞). It is therefore larger than when α = 1 + 1/π -2/p. For such a value of α, it is equal to (1 -1/p) 2 and is non-negative.

Proof of Claim 3. We first suppose that p ≥ 2. Then, The right-hand side is a quadratic polynomial of the form α 2 + bα + c with b = 1/p -1/π + 1/2 ≥ 1/p -1/π. It it therefore increasing on [-b/2, +∞) ⊃ [1/(2π) -1/(2p), +∞). In particular, it is larger that when α = 1/π or when α = (p/2)(1/π -1/p). It is equal to (-p + π + 2)/(2πp) in the first case, and to p(p -π -2)/(4π 2 ) in the second case. At least one of the two terms is non-negative.

(
We now suppose that p < 2. Then,

(1 + α)(δ/p + α -1/π) -(α + δ/p)(1 -1/p) = (1/p + α) 2 -(1 + α)/π.

As in the proof of Claim 2, the right-hand side of this inequality is an increasing function of α on [1/(2π) -1/p, +∞). It is therefore larger that when α = 1/π, in which case it is equal to (π + (2 -p)p)/(p 2 π) > 0.

4.6. Proof of Proposition 7. We must show that the partitions m defined in the proof of Theorem 6 belong to M for some satisfying 2 ≤ n p/(p-1) for n large enough. Moreover, we must have 2 ≤ n when α > 1/π and n large enough.

When α ≤ ᾱ and α ≤ 1/π, or when α ≤ (p -π)/(2π) and α > 1/π, k is defined by (36) with 1/δ α = 2/p -1/π + α or 1/δ α = 2/p. As ≤ k, we have, 2 ≤ C n log n 1/(2(α-1/π+1/p)+1-1/δα) .

When 1/δ α is given by the first formula, the denominator in the exponent is 2(α -1/π + 1/p) + 1 -1/δ α = α -1/π + 1 ≥ 1 -1/p, and 2 ≤ n p/(p-1) for n large enough. When 1/δ α = p/2, we rather have 2(α -1/π + 1/p) + 1 -1/δ α = 2α -2/π + 1, and using α > 1/π, 2 ≤ n for n large enough. Suppose now that α ∈ (ᾱ, 1/π], or α > 1/π and α > (p -π)/(2π). Then, k is defined by (32) and is bounded above by (35). In the first case, we use Claim 2 to get ≤ (1 + α)/(1 -1/p) and thus 2 ≤ C n log n (1+α)/((1-1/p)(1+2α)) , which is smaller than n p/(p-1) for n large. In the second case, we use the claim below to get ≤ (1 + 2α)k and hence 2 ≤ C (n/log n).

Claim 4. The following inequality holds true: for all α > 1/π, π ∈ (0, p), such that α > (p/2)(1/π -1/p), α + δ/p < (1 + 2α)(δ/p + α -1/π), where δ = max{1, p/2}. Proof of Claim 4. We first suppose that p ≥ 2. Then, (1 + 2α)(δ/p + α -1/π) -(α + δ/p) = (1 + 2α)(1/2 + α -1/π) -(α + 1/2) = 2(α -1/π)(α + 1/2) > 0.

We now suppose that p < 2. Then, (1 + 2α)(δ/p + α -1/π) -(α + δ/p) = 2α(α + 1/p) -(1 + 2α)/π. This quadratic polynomial is increasing on [(1/π-1/p)/2, +∞). The right-hand side of the above equality is therefore larger that when α = 1/π, in which case it is equal to (2 -p)/(pπ) > 0.

Figure 1 .

 1 Figure 1. Minimax rates for Besov classes and compact estimation domains

4. 1 .

 1 Proof of Proposition 2. Due to the results on Hölder's classes, we only need to show

.

  We simply use |ϕ I,j | ≤ (2j + 1)/|I| to get w p ξ (m) ≤ C((ξ + m )/n) p w p (m), which ends the proof.

( 1 +

 1 α)(δ/p + α -1/π) -(α + δ/p)(1 -1/p) = (1 + α)(δ /p + α -1/π) -(α + δ /p)(1 -1/p) = (α + δ /p)(1/p + α) -(1 + α)/π.We have 1/δ ≤ 2/p -1/π + α, and hence,(1 + α)(δ/p + α -1/π) -(α + δ/p)(1 -1/p) ≥ α + 1 p(2/p -1/π + α) (1/p + α) -(1 + α)/π.The right-hand side of this inequality is of the same sign as[α(2/p -1/π + α) + 1/p] (1/p + α) -(1/π)(1 + α)(2/p -1/π + α) = (α -1/π + 1/p) α 2 + (2/p -1/π)α -(1/π -1/p) .

  1 + α)(δ/p + α -1/π) -(α + δ/p)(1 -1/p) = (1 + α)(1/2 + α -1/π) -(α + 1/2)(1 -1/p) = (α + 1/2)(1/p + α) -(1 + α)/π.