Sylvain Heraud

David Nowak

A Formalization of Polytime Functions ⋆

Keywords:

We present a deep embedding of Bellantoni and Cook's syntactic characterization of polytime functions. We prove formally that it is correct and complete with respect to the original characterization by Cobham that required a bound to be proved manually. Compared to the paper proof by Bellantoni and Cook, we have been careful in making our proof fully contructive so that we obtain more precise bounding polynomials and more efficient translations between the two characterizations. Another difference is that we consider functions on bitstrings instead of functions on positive integers. This latter change is motivated by the application of our formalization in the context of formal security proofs in cryptography. Based on our core formalization, we have started developing a library of polytime functions that can be reused to build more complex ones.

Introduction

When formally verifying algorithms, one often proves their correctness and termination, but complexity is rarely considered. However proving correctness or termination of an algorithm that is not executable in polynomial time is of little practical use. Even at a theoretical level, it might not make much sense. For instance, in the context of security proofs one has to restrict the computational power of the adversary in the model. Indeed, an adversary with unlimited computational power could break most cryptographic schemes without actually making them insecure.

One way to take into account complexity in formal verification would be to formalize a precise execution model (e.g., Turing machines) and to explicitly count the number of steps necessary for the execution of the algorithm. Such approach would be for the least tedious and would give results depending on the particular execution model that is used whereas one is mainly interested in the complexity class independently of a particular execution model. A more convenient approach is implicit computational complexity that relates programming languages with complexity classes without relying on a particular execution model nor counting explicitly execution steps.

The main motivation behind our work presented in this paper is its application in the context of security proofs in cryptography for restricting the computational power of the adversary so that it is feasible. Cobham's thesis asserts that being feasible is the same as being computable in polynomial time [START_REF] Cobham | The intrinsic computational difficulty of functions[END_REF]. Cryptographers follow Cobham's thesis in their security proofs by assuming that the adversary is computable in probabilistic polynomial time (PPT), i.e., executable on a Turing machine extended with a read-only random tape that has been filled with random bits, and working in (worst-case) polynomial time. Moreover the class of functions computable in polynomial time (a.k.a. polytime functions) has several natural closure properties that are convenient for programming. It is in particular closed under composition and a limited kind of recursion. Cobham uses those closure properties to characterize the polytime functions independently of any particular execution model. Indeed, although in his proof he uses a particular model of Turing machine, he claims that it is quite incidental, i.e., the particularities such as the number of tapes or the chosen instruction set have no significant effect on the proof. Even adding an instruction to erase a tape or put back the head in its initial position in a single step would not break the proof [START_REF] Cobham | The intrinsic computational difficulty of functions[END_REF].

Unfortunately, the characterization of Cobham is not fully syntactic: a size bound has to be proved on the semantics of recursive functions. This thus does not allow for an automatic procedure to check whether a program satisfies or not the conditions to be in Cobham's class. About 30 years later, Bellantoni and Cook have proposed a syntactic mechanism to control the growth rate of functions and thus eliminate the need for an explicit size bound [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF]. Being a fully syntactic characterization, membership in the Bellantoni-Cook's class can be checked automatically. They show that the existence of an algorithm in Cobham's class is equivalent to the existence of an algorithm in Bellantoni-Cook's class that computes the same function. This makes their class a sound and complete characterization of polytime functions: any function definable in Bellantoni-Cook's (or Cobham's) class is computable in polynomial time, and any function computable in polynomial time is definable in Bellantoni-Cook's (and Cobham's) class.

Related work. It is not uncommon that a few months or a few years after a so-called security proof for a cryptographic scheme is published (e.g., in a top-level conference in cryptography), an attack on this same scheme is published. This shows that there is a need for formal verification in cryptography. This need is well-known among and acknowledged by cryptographers [START_REF] Halevi | A plausible approach to computer-aided cryptographic proofs[END_REF]. As a matter of fact, these last few years, several frameworks for machine-checking security proofs in cryptography have been proposed [START_REF] Backes | A formal language for cryptographic pseudocode[END_REF][START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF][START_REF] Nowak | A framework for game-based security proofs[END_REF]. However, these frameworks either ignore complexity-theoretic issues or postulate the complexity of the involved functions.

Zhang has proposed a probabilistic programming language with a type system to ensure computation in probabilistic polynomial time and an equational logic to reason about those programs [START_REF] Zhang | The computational SLR: a logic for reasoning about computational indistinguishability[END_REF]. In [START_REF] Nowak | A calculus for game-based security proofs[END_REF], it has been applied to security proofs in cryptography. Zhang rely on Hofmann's SLR [START_REF] Hofmann | Safe recursion with higher types and BCK-algebra[END_REF] and its extension to the probabilistic case by Mitchell et al. [START_REF] Mitchell | A linguistic characterization of bounded oracle computation and probabilistic polynomial time[END_REF]. Those latter work are about functions on positive integers. Like us in this paper, Zhang made the move to bitstrings in order to be applicable in the context of cryptography where, for example, the bitstrings 0 and 00 are considered different although they would be identified if they were interpreted as positive integers.

In [START_REF] Schürmann | Representing reductions of NP-complete problems in logical frameworks: A case study[END_REF], it is acknowledged the need for a "polytime checker", possibly based on Bellantoni and Cook's work, and to be used to check automatically that a reduction between two NP-complete problems is computable in polynomial time. In this paper, we provide such polytime checker.

There are many other criteria to ensure that functions, defined using various programming paradigms, are in particular complexity classes. To cite only a few, some propose logical characterizations of polytime functions [START_REF] Leivant | A foundational delineation of computational feasibility[END_REF][START_REF] Schürmann | Identifying Polynomial-Time Recursive Functions[END_REF] or characterizations in terms of rewrite system [START_REF] Avanzini | Complexity Analysis by Rewriting[END_REF]. Others deal with different complexity classes [START_REF] Arai | A new function algebra of EXPTIME functions by safe nested recursion[END_REF]. To the best of our knowledge, none of those criteria have been applied to cryptography.

Contributions. In the proof assistant Coq, we have deep embedded the bitstring versions of Cobham and Bellantoni-Cook's classes and their relation. Initially, those classes were about functions on positive integers. But in the context of cryptography we must deal with bitstrings. The reformulation of Cobham's class with bitstrings and the proof that it contains exactly the function computable in polynomial time was done in [START_REF] Tourlakis | Computability[END_REF]. In a similar way, we have reformulated the definition of Bellantoni-Cook's class.

We have also extended Bellantoni and Cook's proof that their class is equivalent to Cobham's one by making it fully constructive, i.e., we provide explicit algorithms to perform translations between the two classes. Those algorithms can be executed in Coq and extracted automatically into a certified translator in an ML dialect supported by Coq. We also make more precise the bounding polynomials thus obtaining better bounds and a more efficient translation, whereas Bellantoni and Cook overapproximate them since they are only interested in their existence and do not try to optimize the translations.

We have started to implement libraries of functions in Cobham's and Bellantoni-Cook's classes that can be used to build more complex functions.

In the context of security proofs in cryptography, we have shown how to apply our work with the second author's toolbox for certifying cryptographic primitives [START_REF] Nowak | A framework for game-based security proofs[END_REF][START_REF] Nowak | On formal verification of arithmetic-based cryptographic primitives[END_REF][START_REF] Nowak | A Certification Toolbox for Cryptographic Algorithms[END_REF]. We have also extended Certicrypt [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF] with support to define in Bellantoni-Cook's class the mathematical functions used by adversaries: The benefit is that one gets for free polynomials that had to be postulated before our extension, thus bringing more confidence in the security proof.

We have proved a new result on Bellantoni-Cook's class: we give explicitly a polynomial that bounds the running time of a function in Bellantoni-Cook's class. Such explicit polynomial was necessary to interface our library with Certicrypt.

Outline. We start by some preliminaries in Section 2. In Section 3, we formalize Cobham's and Bellantoni-Cook's classes that characterize polytime functions. Then in Sections 4 and 5 we respectively formalize the translation from Bellantoni-Cook's class to Cobham's class and vice versa. Finally in Section 6 we show how our formalization can be used for the purpose of formalizing security proofs in cryptography.

Preliminaries

In this section, we introduce our formalization of multivariate polynomials and various notations that will be used in the rest of this paper.

Multivariate polynomials

We have implemented a library of positive multivariate polynomials. A shallow embedding of polynomials might consist in representing them as a particular class of functions on positive integers. However, since we need in Section 4 to translate polynomials into expressions in Cobham's class, we have opted for a deep embedding. A polynomial is represented as a pair of the number of distinct variables and a list of monomials. A monomial is represented as a pair of a constant positive integer and a list of variables and their powers. A variable is represented as an integer. For example, the polynomial 3y 3 + 5x 2 y + 16 is represented by

(2, [(3, [(1, 3)]); (5, [(0, 2); (1, 1)]); (16, [])])
where the leftmost 2 is the number of variables, and variables x and y are respectively represented by 0 and 1. We chose to put the number of variables in the representation of a polynomial so as to easily inject a polynomial using m variables into the class of polynomials with n variables when n > m. Otherwise we would have to add artificial occurrences of variables with coefficient 0. In the library we provide utility functions in Coq to create and combine polynomials (constant, variables, addition, multiplication, composition. . . ). We use those functions when building a polynomial. Those functions are parameterized by the number of variables, but we will omit this parameter in the rest of the paper since it will be clear from context. We write x 0 , . . . , x n-1 for the variables of a polynomial with n variables. If P is a polynomial with m variables and Q = Q 0 , . . . , Q m-1 is a vector of polynomials with n variables, we write P (Q) for the polynomial with n variables defined by substituting each variable x i in P by the polynomial Q i and by applying distributivity of multiplication over addition and associativity of addition.

In [START_REF] Grégoire | Proving Equalities in a Commutative Ring Done Right in Coq[END_REF], multivariate polynomials are represented in sparse Horner form and thus allow for a more efficient numerical evaluation of polynomials. Since we do not intend to numerically evaluate polynomials, we have opted for a more direct approach. This will moreover facilitate the connection with univariate polynomials in Certicrypt (cf. Section 6.2).

Notations

We list some notations that will be useful to present the results and their proofs in a concise manner. However, the meaning of those notations should be clear from the context. We write:

xb for the concatenation of the bitstring x with a bit b in the least significant position; -x for a vector x 0 , . . . , x n-1 (for some n); -x, y for the concatenation of vectors x and y;

-|x| for the length of a vector x;

-|x| for the size of a bitstring x; -|x| for the vector of sizes of the components of the vector x, i.e., if x = x 0 , . . . , x n-1 then |x| = |x 0 |, . . . , |x n-1 | ;

f (x) for the vector of applications of f to each component of the vector x, i.e., if x = x 0 , . . . , x n-1 then f (x) = f (x 0 ), . . . , f (x n-1 ) ;

f (x) for the vector of applications of each component of the vector f to x, i.e., if

f = f 0 , . . . , f n-1 then f (x) = f 0 (x), . . . , f n-1 (x) .

Characterizing polytime functions

In this section, we explain our deep embedding of the bitstring versions of Cobham's and Bellantoni-Cook's classes, and state some of their bounding properties.

Cobham's class

In a seminal paper [START_REF] Cobham | The intrinsic computational difficulty of functions[END_REF], Cobham characterized polytime functions as the least class of functions containing certain initial functions and closed under composition and a certain kind of recursion. However this characterization is not fully syntactic as it requires a size bound to be proved on the semantics of recursive functions.

We use the reformulation of Cobham's class taken from [START_REF] Tourlakis | Computability[END_REF] and that deals with bitstrings instead of positive integers as it was the case in [START_REF] Cobham | The intrinsic computational difficulty of functions[END_REF].

The syntax of Cobham's class C is given by:

C ::= O constant zero | Π n i projection (i < n) | S b successor | # smash | Comp n h g composition | Rec g h 0 h 1 j recursion
where i and n are positive integers, b is a bit, g, h, h 0 , h 1 and j are expressions in C, and g is a vector of expressions in C. Well-formed expressions e in C have a well defined arity A(e) given by:

A(O) = 0 A(Π n i ) = n A(S b ) = 1 A(#) = 2 A(h) = a h |g| = a h ∀g ∈ g, A(g) = n A(Comp n h g) = n A(g) = a g A(h 0 ) = A(h 1 ) = a h A(j) = a j a h = a g + 2 = a j + 1 A(Rec g h 0 h 1 j) = a j
In our implementation, A is a Coq function that computes the arity of a Cobham's expression if it is well formed, or returns an error message otherwise. It is helpful when programming and debugging polytime functions in Cobham's class. The semantics is given by:

-O denotes the constant function that always returns the empty bitstring ǫ.

- -Comp n h g is equal to the function f such that:

Π n i (x 0 , . . . , x n-1 ) is equal to x i . -S b (x) is equal to xb. -#(x,
f (x) = h(g(x))
-Rec g h 0 h 1 j is equal to the function f such that:

f (ǫ, x) = g(x) f (yi, x) = h i (y, f (y, x), x) |f (y, x)| ≤ |j(y, x)| (RecBounded )
We illustrate Cobham's class by implementing the binary successor function:

Rec Succ(ǫ) = 1 (Comp 0 S 1 O) Succ(x0) = x1 (Comp 0 S 1 Π 2 0 ) Succ(x1) = Succ(x)0 (Comp 0 S 0 Π 2 1 ) Succ(x) ≤ x1 (Comp 0 S 1 Π 1 0 )
We prove in the following proposition that the output of a Cobham's function is bounded by a polynomial in the lengths of its inputs.

Proposition 1. For all f in C with a well-defined arity A(f ) and semantics (i.e., satisfying the condition RecBounded ), there exists a length-bounding monotone polynomial Pol C (f ) such that:

|f (x)| ≤ (Pol C (f ))(|x|)
Proof. By induction on the syntax of f . Our proof is fully constructive in the sense that we define explicitly Pol C . For any f in C with arity A(f ) = n, Pol C (f ) is the monotone polynomial with n variables x 0 , . . . , x n-1 defined by:

Pol C (O) = 0 Pol C (Π n i ) = x i Pol C (S b ) = x 0 + 1 Pol C (#) = x 0 .x 1 + 1 Pol C (Comp n h g) = (Pol C (h))(Pol C (g)) Pol C (Rec g h 0 h 1 j) = Pol C (j) ⊓ ⊔
We define a translation Poly → C from polynomials into Cobham's expressions. It is such that, for any polynomial P , Poly → C(P ) is a unary encoding of P in Cobham's class, i.e., |Poly → C(P )(x)| = P (|x|)

Bellantoni-Cook's class

Bellantoni and Cook have given a fully syntactic characterization of polytime functions that does not require any explicit mechanism to count the number of computation steps [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF]. The control of the growth rate of functions is achieved by distinguishing two kinds of variables: the "normal" and "safe" ones written respectively on the left and right side of a semicolon such as:

f (x 0 , . . . , x n-1 normal ; x n , . . . , x n+s-1 safe )
The syntax of Bellantoni-Cook's class B is given by:

B ::= 0 constant zero | π n,s i projection (i < n + s) | s b successor | pred predecessor | cond conditional | comp n,s h g N g S composition | rec g h 0 h 1 recursion
where i, n and s are positive integers, b is a bit, g, h, h 0 and h 1 are expressions in B, and g N and g S are vectors of expressions in B. Note that, contrary to Cobham's class, a bounding function j is not needed for recursion. Well-formed expressions e in B have well defined arities A(e) (counting separately the numbers of normal and safe variables) given by:

A(0) = (0, 0) A(π n,s i ) = (n, s) A(s b ) = (0, 1) A(pred) = (0, 1)
A(cond) = (0, 4)

A(h) = (n h , s h ) |g N | = n h |g S | = s h ∀g ∈ g N , A(g) = (n, 0) ∀g ∈ g S , A(g) = (n, s) A(comp n,s h g N g S ) = (n, s) A(g) = (n g , s g ) A(h 0 ) = A(h 1 ) = (n h , s h ) n h = n g + 1 s h = s g + 1 A(rec g h 0 h 1 ) = (n h , s g )
This function A is implemented like the one for Cobham's class. The semantics is given by:

-0 denotes the constant function that always returns the empty bitstring ǫ.

π n,s i (x 0 , . . . , x n-1 ; x n , . . . , x n+s-1 ) is equal to

x i . -s b (; x) is equal to xb.
pred(; ǫ) = ǫ and pred(; xi) = x.

cond(; ǫ, x, y, z) = x, cond(; w0, x, y, z) = y and cond(; w1, x, y, z) = z.

comp n,s h g N g S is equal to the function f such that: f (x; y) = h(g N (x; ); g S (x; y))

Note here that the functions in g N only have access to normal variables.

rec g h 0 h 1 is equal to the function f such that:

f (ǫ, x; y) = g(x; y) f (zi, x; y) = h i (z, x; f (z, x; y), y)
Note here that the result of the recursive call f (z, x; y) is passed at a safe position. This prevents it to be used as the recursion argument in a nested recursion.

One can see that, contrary to Cobham's class C, there is no size bound to be proved on recursive functions: Bellantoni-Cook's class B is syntactically defined.

Reader may have noticed that our definition of Bellantoni-Cook's class is slightly different from the one in [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF]. First, here the conditional cond distinguishes between three cases (empty, even or odd bitstrings), whereas in [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF] the empty bitstring is treated as an even one. Second, here the base case for recursion is the empty bitstring, whereas in [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF] it is any bitstring whose interpretation as a positive integer is 0, i.e., the empty bitstring or any bitstring made of any number of bits 0 only. We made those changes because in cryptography one wants to distinguish, for example, bitstrings 0 and 00 although they would have the same interpretation in terms of positive integers. These changes are validated by the results we proved in the rest of the paper where we translate our Bellantoni-Cook's expressions to/from the bitstring version of Cobham's expressions [START_REF] Tourlakis | Computability[END_REF].

The following examples illustrate how one can program addition and multiplication in Bellantoni-Cook's class and their respective arity:

plus := rec (π 0,1 0 ) (comp 1,2 S 1 π 1,2 1 ) (comp 1,2 S 1 π 1, 2 1 )
A(plus) = (1, 1)

mult := rec (comp 1,0 O ) (comp 1,2 plus π 2,0 1 π 2,1 2 ) (comp 1,2 plus π 2,0 1 π 2,1 2 ) A(mult) = (2, 0)
We prove in the following proposition that the output of a Bellantoni-Cook's function is bounded by the sum of a polynomial in the lengths of its normal inputs and the size of its longest safe input. This is so because syntactic restrictions ensure that we cannot increase the lengths of safe inputs by more than an additive constant that will be taken into account in the polynomial part.

Proposition 2 (Polymax Bounding). For all f in B with well-defined arities A(f ), there exists a lengthbounding monotone polynomial Pol B (f ) such that, for all x and y:

|f (x; y)| ≤ (Pol B (f ))(|x|) + max i |y i |
Proof. By induction on the syntax of f . Our proof is fully constructive in the sense that we define explicitly Pol B . For any f in B with arity A(f ) = (n, s), Pol B (f ) is the monotone polynomial with n variables x 0 , . . . , x n-1 defined by:

Pol B (0) = 0 Pol B (π n,s i ) = x i if i < n 0 otherwise Pol B (s b ) = 1 Pol B (pred) = 0 Pol B (cond) = 0 Pol B (comp n,s h g N g S ) = Pol B (h)(Pol B (g N )) + (Pol B (g S )) Pol B (rec g h 0 h 1 ) = shift(Pol B (g)) + x 0 .(Pol B (h 0 ) + Pol B (h 1 ))
where shift(P ) is the polynomial P with each variable x i replaced by x i+1 .

⊓ ⊔

We define a translation Poly → B from polynomials into Bellantoni-Cook's expressions. It is such that, for any polynomial P , Poly → B(P ) is a unary encoding of P in Bellantoni-Cook's class, i.e.,

|Poly → B(P )(x)| = P (|x|)

In order to ease further development of functions in Bellantoni-Cook's class, we provide a mechanism to infer automatically the optimal values for the parameters n and s appearing in π n,s i and comp n,s thus obtaining more elegant code. This is implemented with a new syntax B inf for Bellantoni-Cook's class where arities do not appear in the syntax:

B inf ::= 0 constant zero | π normal i projection (normal) (i < n) | π safe i projection (safe) (i < s) | s b successor | pred predecessor | cond conditional | comp h g N g S composition | rec g h 0 h 1 recursion
We have validated this new syntax by providing certified translations between B inf and B. When translating from B inf to B, we can force arities to be larger that the minimal ones that are inferred.

Compiling Bellantoni-Cook into Cobham

In this section, we provide our formalization of the translation of expressions in Bellantoni-Cook's class into expressions in Cobham's class. The main result is stated in the following theorem.

Theorem 1. For all f in B with well defined arities A(f ), there exists f ′ in C such that for all vectors of bitstrings x and y, f (x; y) = f ′ (x, y).

Proof. The proof is split into two inductions on the syntax of f : The first one to prove the equality and the second one to prove that the condition RecBounded is satisfied. Our proof is fully constructive in the sense that we define explicitly the translation B → C from B to C and define f ′ as B → C(f ). The difficulty of the proof is in the generation of a Cobham expression that satisfies the condition RecBounded , and to build the polynomial j that bounds the recursive calls.

-The first cases are immediate:

B → C(0) = O B → C(π n,s i ) = Π n+s i B → C(s b ) = S b
pred and cond are translated by using Rec:

B → C(pred) = Rec O Π 2 0 Π 2 0 Π 1 0 B → C(cond) = Rec Π 3 0 Π 5 4 Π 5 3 Comp 4 # Comp 4 S 1 Π 4 1 ; Comp 4 # Comp 4 S 1 Π 4 2 ; Comp 4 S 1 Π 4 3
-For comp n,s h g N g S we need to add dummy variables, since the functions in g N do not take the safe arguments as parameters. We need to transform these functions in g N into functions with arity n + s. dummies s (written in C) add s dummy variables that are ignored:

B → C(comp n,s h g N g S ) = Comp n+s B → C(h) dummies s (B → C(g N )), B → C(g S )
-For rec g h 0 h 1 we need to change the order of the arguments passed to the translations of h 0 and h 1 . Indeed, while in B the recursive argument is put after the normal ones, in C it should be the second argument. This reordering is done by the function move arg 2,n (written in C). Moreover, we need to derive a suitable bound for the fourth argument of Rec. By Proposition 2 and the fact that the sum

|x n | + • • • + |x n+s-1
| of the sizes of the safe arguments is greater than or equal to the maximum size of the safe arguments, we can take the polynomial Pol B (rec g h 0 h 1 ) + x n + • • • + x n+s-1 for the bound. We then use Poly → C to encode it in C:

B → C(rec g h 0 h 1 ) = Rec B → C(g) move arg 2,n (B → C(h 0 )) move arg 2,n (B → C(h 1 )) Poly → C Pol B (rec g h 0 h 1 ) + x n + • • • + x n+s-1 ⊓ ⊔

Compiling Cobham into Bellantoni-Cook

Contrary to Bellantoni-Cook's class B, one does not distinguish between normal and safe variables in Cobham's class C. In C it is possible to recur on any argument, whereas in B one can only recur on normal arguments. Thus, when translating from C to B, we must introduce a distinction and deal appropriately with recursion. In our formalization, we follow Bellantoni and Cook's translation scheme by assuming that all the arguments are safe and adding an artificial normal argument w whose length is large enough to ensure enough recursion steps. This gives us the lemma below. After that, we will get rid of w thus obtaining Theorem 2.

Lemma 1 (Recursion Simulation). For all function f in C with well-defined arity A(f ) = n and semantics (i.e., satisfying the condition RecBounded ), there exists an f ′ in B and a monotone polynomial Pol C→B (f ) such that for all vector of bitstrings x and bistring w such that

Pol C→B (f )(|x|) ≤ |w|, f (x) = f ′ (w; x).
Proof. By induction on the syntax of f . Our proof is fully constructive in the sense that we define explicitly the polynomial Pol C→B (f ) and the translation C → B, and define

f ′ as C → B(f ). Our translation is such that if A(f ) = n then A(f ′ ) = (1, n), i.e.
, f ′ takes one normal argument and n safe arguments.

-The first cases for C → B(f ) are immediate. We just have to make sure that the arities are right:

C → B(O) = comp 1,n O C → B(Π n i ) = π 1,n i+1 C → B(S b ) = comp 1,n s b π 1,n 1 C → B(Comp n h g) = comp 1,n (C → B(h)) π 1,0 1 C → B(g)
Pol C→B (f )(|x|) is also immediate for these first cases:

Pol C→B (O) = 0 Pol C→B (Π n i ) = 0 Pol C→B (S b ) = 0 Pol C→B (Comp n h g) = Pol C→B (h)(Pol C (g)) + g∈g Pol C→B (g)
The rightness of the case for Comp follows by induction hypothesis and Proposition 1.

-For the case of Rec g h 0 h 1 j, we follow [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF]

f (ǫ, w; y, x) = g(w; x) f (zj, w; y, x) =    g ′ (w; x) if Y (S 1 z, w; y) is ǫ h ′ 0 (w, Y (z, w; y), f (z, w; y, x), x) if Y (S 1 z, w; y) is even h ′ 1 (w; Y (z, w; y), f (z, w; y, x), x) if Y (S 1 z, w; y) is odd where g ′ , h ′ 0 and h ′ 1 are respectively C → B(g), C → B(h 0 ) and C → B(h 1 )
. Our definition of f is simpler than in [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF] because we do not need, like in [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF], an additional intermediate function to check whether y is an encoding of the positive integer 0. In our case, we stop the recursion when y is equal to ǫ, since the cond can check whether the first safe argument is ǫ. We then define f ′ (w; y, x) in B such that it is equal to f (w, w; y, x), and finally:

C → B(Rec g h 0 h 1 j) = f ′ (C → B(g)) (C → B(h 0 )) (C → B(h 1 ))
For the polynomial, we have:

Pol C→B (Rec g h 0 h 1 j)(|y|, |x|) =(Pol C→B (h 0 )+Pol C→B (h 1 ))(|y|, Pol C (f ), |x|)+ shift(Pol C→B (g)(|x|)) + |y| + 2
-We can define the smash function # from C in B by a double recursion:

# ′ (ǫ, y) = y # ′ (xi, y) = # ′ (x, y) 0 (concatenation with a bit 0) #(ǫ, y) = 1 #(xi, y) = # ′ (y, #(x, y))
In order to implement in B those two recursive functions we apply the same technique as in the case of Rec above. We first obtain a # ′ in B by constructing f ′ with g = π 1,1

1 and h 0 = h 1 = comp 1,3 S 0 π 1,3 2 .
We then obtain # in B by applying the same construction of f ′ with g = one 1,1 and h

0 = h 1 = dummies 0,1 (comp 1,2 # ′ π 1,0 0 π 1,2 2 ; π 1,2 1
). For the polynomial, we obtain (after simplification):

Pol C→B (#) = x 0 + 2x 1 + 18 ⊓ ⊔
Finally, the main result of this section is stated in the following theorem.

Theorem 2. For all f in C with well-defined arity A(f ) and semantics (i.e., satisfying the condition RecBounded ), there exists f ′ in B such that, for all vectors of bitstrings x, f (x) = f ′ (x; ).

Proof. We define the expression b f in B by:

Poly → B(Pol C→B (f ))
By definition of Poly → B, for all vector of bistrings x, |b f (x; )| = Pol C→B (f )(|x|). We can thus apply Lemma 1 which gives:

f ′ (x; ) = (C → B(f ))(b f (x; ); x) ⊓ ⊔
Our translation gives a more efficient code than the one in [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF] since our definition of b f is more precise: the number of recursive calls will be no more than what is strictly necessary. Indeed, authors of [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF] use general properties of multivariate polynomials to first prove the existence of positive integers a and c such that

Pol C→B (f )(|x|) ≤ ( j |x j |) a + c
and then use a and c to build a b f that satisfies the condition of Lemma 1, i.e., Pol C→B (f )(|x|) ≤ |b(x; )|. Their b f is an overapproximation of Pol C→B (f ) while our b f is an exact encoding.

Applications

Security properties in cryptography are often modeled as games, and then security proofs consist in showing that no adversary can win the game [START_REF] Bellare | The security of triple encryption and a framework for code-based game-playing proofs[END_REF][START_REF] Shoup | Sequences of games: A tool for taming complexity in security proofs[END_REF]. Most of those proofs are based on computational assumptions that state that an effective adversary cannot solve a particular mathematical problem, e.g., Diffie-Hellman problems [START_REF] Diffie | New directions in cryptography[END_REF]. Effective adversaries are modeled as strict probabilistic polynomial-time functions, i.e., independently of the random choices, the execution time is bounded by a polynomial in a security parameter (typically the length of the inputs). This means that an adversary can be modeled as a polytime function with, as an additional parameter, a long enough bitstring that will be used by the adversary as its source of random bits.

Application to the second author's toolbox

The second author's toolbox is a collection of definitions and lemmas to be used for verifying game transformations in security proofs [START_REF] Nowak | A framework for game-based security proofs[END_REF][START_REF] Nowak | On formal verification of arithmetic-based cryptographic primitives[END_REF][START_REF] Nowak | A Certification Toolbox for Cryptographic Algorithms[END_REF]. With this toolbox, our library can be used as such when applying a computational hypothesis. The computational hypotheses can indeed be restricted to adversaries defined in Cobham's or Bellantoni-Cook's class (it is not too restrictive since those classes are complete) and adversaries appearing in proofs must then be defined in one of those classes. For example, when applying the Decisional Diffie-Hellman assumption (DDH) in the security proof for Hashed ElGamal in [START_REF] Nowak | A framework for game-based security proofs[END_REF], a new adversary ϕ is built from two adversaries A 1 and A 2 :

ϕ(X, Y, Z) = def A 2 (r, (X, k), (Y, H k (Z) ⊕ π b (A 1 (r, (X, k))))) ? = b
where b, k and r are fixed, ⊕ is a the bitwise exclusive or (xor), π b is the b th projection (b is equal to 1 or 2), and ? = is the equality test. That A 1 and A 2 are polytime is given by hypothesis. We can also assume that the hash function H k is polytime. Being polytime, they are definable in Bellantoni-Cook's class. Moreover, projections, exclusive or and equality test are easily defined in Bellantoni-Cook's class. Therefore ϕ is easily definable in Bellantoni-Cook's class and thus it is polytime.

Application to Certicrypt

The application of our library to Certicrypt requires more work but brings noticeable benefits.

In Certicrypt, a game is a probabilistic imperative program that transforms a distribution of input states into a distribution of output states. A state includes a time index. A distribution of states is polynomially bounded if there are two (univariate) polynomials p and q respectively bounding the size of the data and the time index of each state in the distribution. A program is strict probabilistic polynomial time (PPT) iff: it always terminates; and, there exists two (univariate) polynomial transformers F and G such that, for every polynomially bounded (by p and q) distribution of input states, the distribution of output states is bounded by F (p) (bounding the output size) and q + G(p) (bounding the execution time). Interested reader should refer to [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF] for further explanation about this way to formalize PPT.

We have built an interface with Certicrypt made of the following components:

-The core language of Certicrypt can be extended with user-defined types and functions. But the time cost of each function has to be axiomatized in the current implementation of Certicrypt. We have added the possibility to include functions that have been defined in our implementation of Bellantoni-Cook's class and that are thus automatically proved executable in polynomial time, thus removing the need for postulates. -We have added a conversion from any multivariate polynomial P given by our library into a univariate one ⌈P ⌉ in Certicrypt that overapproximates P when applied to the maximal argument: This is easily done by substituting all variables x 0 , . . . , x n-1 in P by a single variable x:

⌈P ⌉ = def P [x 0 → x; . . . ; x n-1 → x]
-In the case of a program c defined in Bellantoni-Cook's class, we can take F (p) to be equal to:

1 + 2 ⌈Pol B (c)⌉(p)
This is justified by Proposition 2. The multiplication by 2 and and addition of 1 are here because of technical reasons coming from Certicrypt. For example, the multiplication by 2 comes from the fact that the size of a boolean in Certicrypt is 2. -In order to obtain G(p), we need to consider the obvious implementation of Bellantoni-Cook's class on a stack machine as described in Section 3.4.2 of [START_REF] Bellantoni | Predicative Recursion and Computational Complexity[END_REF]. We have equipped the semantics of Bellantoni-Cook's class with a time index that keeps track of the running time. We can then prove that the multivariate polynomial Pol time below is an upper bound of the running time, and use it to define G(p). where shift(P ) is the polynomial P with each variable x i replaced by x i+1 . An interesting thing about Pol time is that, in the case of comp n,s h g N g S , it is necessary to consider the size Pol B (g N ) of the outputs of the functions in g N for the running time of h, but not the size of the outputs of the functions in g S . This is so because syntactic restrictions ensure that we cannot increase the lengths of safe inputs by more than an additive constant. Finally, for a program c defined in Bellantoni-Cook's class, we take G(p) to be equal to:

⌈Pol time (c)⌉(p)
The reader might be surprised that in this section we consider a particular implementation of Bellantoni-Cook's class while in introduction we said that we are interested in complexity independently of any execution model. The reason is that, although being in Cobham's or Bellantoni-Cook's class guarantees that there exists a polynomial bounding the execution time, it does not give any clue on the actual value of this polynomial. However Certicrypt requires that we explicitly give such a polynomial. This is why we consider here a particular execution model: to be able to compute a polynomial.

Conclusions and future work

We have formalized Cobham's and Bellantoni-Cook's classes and their relations in the proof assistant Coq. Usage of proof assistant led us to formalize parts of the proofs that were only informal in Bellantoni and Cook's paper. Our formalization allows to use those classes as programming languages to define any function that is computable in polynomial time. We have shown in particular that it can be used to build adversaries in security proofs in cryptography.

Future Work. In order to facilitate the use of our formalization, an important future work is to carry on developing a convenient library of polytime functions on bitstrings that can be reused in the construction of more advanced polytime functions. It is easy to implement bitwise operations such as bitwise XOR, NOT, AND, etc. However, when implementing numerical operations such as bitwise addition, dealing with the carry bit does not fit immediately in Bellantoni-Cook's recursion scheme. One possible solution is to implement binary addition, multiplication and other numerical functions in Cobham's class such as in [START_REF] Rose | Subrecursion: functions and hierarchies[END_REF], and use our automatic translation C → B (defined in Section 5) to derive their implementations in Bellantoni-Cook's class. Also, our approach can be extended with higher order so as to formalize a more powerful programming language such as CSLR [START_REF] Zhang | The computational SLR: a logic for reasoning about computational indistinguishability[END_REF].

  y) is equal to 10 . . . . . . 0 |x|.|y| times .

  in defining intermediate functions in B. However we need less of them since our definition of f below is simpler. We define P in B such that P (a; b) removes the |a| least significant bits of b, i.e., P (ǫ; b) = b and P (ai; b) = pred(; P (a; b)). We define Y in B such that Y (z, w; y) removes the |w| -|z| least significant bits of y, i.e., Y (z, w; y) = P (P ′ (z, w); y) where P ′ (a, b; ) = P (a; b). P and Y are then used to define f in B:

  Pol time (0) = Pol time (π n,s i ) = Pol time (s b ) = Pol time (pred) = Pol time (cond) = 1 Pol time (comp n,s h g N g S ) = Pol time (h)(Pol B (g N ))+ (Pol time (g N )) + (Pol time (g S )) Pol time (rec g h 0 h 1 )= shift(Pol time (g))+ x 0 .(Pol time (h 0 ) + Pol time (h 1 ))

Acknowledgments. We are grateful to Benjamin Grégoire and Santiago Zanella Béguelin for replying so quickly to every question we have had on Certicrypt, and for their comments on an earlier draft of this paper. We thank anonymous reviewers for their helpful suggestions, all of which improved the paper.

⋆ Partially supported by JST-CNRS Japanese-French cooperation project on computational and symbolic proofs of security. A short version of this paper will appear in the proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP Supported by Kakenhi 21500046. The work presented in this paper was carried out while this author was affiliated to Research Center for Information Security, AIST.


Ilaria Fragalà

Filippo Gazzola

Jimmy Lamboley

Ilaria Fragal

À -Filippo Gazzola -

Sharp bounds for the p-torsion of convex planar domains

Keywords: 49K30, 52A10, 49Q10 isoperimetric inequalities, shape optimization, web functions, convex shapes

come

Introduction

Let Ω ⊂ IR 2 be an open bounded domain and let p ∈ (1, +∞). Consider the boundary value problem

       -∆ p u = 1 in Ω u = 0 on ∂Ω , (1)
where ∆ p u = div(|∇u| p-2 ∇u) denotes the p-Laplacian. The p-torsion of Ω is defined by

τ p (Ω) := Ω |∇u p | p = Ω u p , (2)
being u p the unique solution to (1) in W 1,p 0 (Ω). Notice that the second equality in (2) is obtained by testing (1) by u p and integrating by parts. Since [START_REF] Bonnesen | Theory of convex bodies[END_REF] is the Euler-Lagrange equation of the variational problem min u∈W 1,p 0 (Ω)

J p (u) , where J p (u) =

Ω 1 p |∇u| p -u , (3)
there holds τ p (Ω) = p 1p min u∈W 1,p 0 (Ω)

J p (u) .

A further characterization of the p-torsion is provided by the equality τ p (Ω) = S(Ω) 1/(p- 1) , where S(Ω) is the best constant for the Sobolev inequality u p L 1 (Ω) ≤ S(Ω) ∇u p L p (Ω) on W 1,p 0 (Ω). The purpose of this paper is to provide some sharp bounds for τ p (Ω), holding for a convex planar domain Ω, in terms of its area, perimeter, and inradius (in the sequel denoted respectively by |Ω|, |∂Ω|, and R Ω ). The 1 original motivation for studying this kind of shape optimization problem draws its origins in the following long-standing conjecture by Pólya and Szegö:

Among polygons with a given area and N vertices, the regular N -gon maximizes τ p .

(4)

A similar conjecture is stated by the same Authors also for the principal frequency and for the logarithmic capacity, see [START_REF] Pólya | Isoperimetric Inequalities in Mathematical Physics[END_REF]. For N = 3 and N = 4 these conjectures were proved by Pólya and Szegö themselves [13, p. 158]. For N ≥ 5, to the best of our knowledge, the unique solved case is the one of logarithmic capacity, see the beautiful paper [START_REF] Solynin | An isoperimetric inequality for logarithmic capacity of polygons[END_REF] by Solynin and Zalgaller; the cases of torsion and principal frequency are currently open. In fact let us remind that, for N ≥ 5, the classical tool of Steiner symmetrization fails because it may increase the number of sides, see [START_REF] Henrot | Extremum problems for eigenvalues of elliptic operators[END_REF]Section 3.3].

The approach we adopt in order to provide upper and lower bounds for the p-torsion in terms of geometric quantities, is based on the idea of considering a proper subspace W p (Ω) of W 1,p 0 (Ω) and to address the minimization problem for the functional J p on W p (Ω). More precisely, we consider the subspace of functions depending only on the distance d(x) = dist(x, ∂Ω) from the boundary:

W p (Ω) = {u ∈ W 1,p 0 (Ω) : u(x) = u(d(x))} .
Functions in W p (Ω) have the same level lines as d, namely the boundaries of the so-called inner parallel sets, Ω t := {x ∈ Ω : d(x) > t}, which were first used in variational problems by Pólya and Szegö [13, Section 1.29]. Later, in [START_REF] Gazzola | Existence of minima for nonconvex functionals in spaces of functions depending on the distance from the boundary[END_REF], the elements of W p (Ω) were called web functions, because in case of planar polygons the level lines of d recall the pattern of a spider web. We refer to [START_REF] Crasta | Some estimates of the minimizing properties of web functions[END_REF][START_REF] Crasta | Web functions: survey of results and perspectives[END_REF] for some estimates on the minimizing properties of these functions, and to the subsequent papers [START_REF] Crasta | A sharp upper bound for the torsional rigidity of rods by means of web functions[END_REF][START_REF] Crasta | On the role of energy convexity in the web function approximation[END_REF] for their application in the study of the generalized torsion problem. Actually, the papers [START_REF] Crasta | A sharp upper bound for the torsional rigidity of rods by means of web functions[END_REF][START_REF] Crasta | On the role of energy convexity in the web function approximation[END_REF] deal with the problem of estimating how efficiently τ p (Ω) can be approximated by the web p-torsion, defined as

w p (Ω) := p 1 -p min u∈Wp(Ω) J p (u) .
While the value of τ p (Ω) is in general not known (because the solution to problem (1) cannot be determined except for some special geometries of Ω), the value of w p (Ω) admits the following explicit expression in terms of the parallel sets Ω t :

w p (Ω) = R Ω 0 |Ω t | q |∂Ω t | q-1 dt , (5)
where q = p p-1 is the conjugate exponent of p, and R Ω is the inradius of Ω (see [START_REF] Crasta | On the role of energy convexity in the web function approximation[END_REF]). Clearly, since W p (Ω) ⊂ W 1,p 0 (Ω), w p (Ω) bounds τ p (Ω) from below. On the other hand, when Ω is convex, τ p (Ω) can be bounded from above by a constant multiple of w p (Ω), for some constant which tends to 1 as p → +∞. In fact, in [START_REF] Crasta | On the role of energy convexity in the web function approximation[END_REF] it is proved that, for any p ∈ (1, +∞), the following estimates hold and are sharp:

∀ Ω ∈ C, q + 1 2 q < w p (Ω) τ p (Ω) ≤ 1 (6)
where C denotes the class of planar bounded convex domains; moreover the right inequality holds as an equality if and only if Ω is a disk. Note that, if p → +∞, then q → 1 and the constant in the left hand side of (6) tends to 1.

In this paper, we prove some geometric estimates for τ p (Ω) in the class C, which have some implications in the conjecture (4). More precisely, we consider the following shape functionals:

Ω → τ p (Ω)|∂Ω| q |Ω| q+1 and Ω → τ p (Ω) R q Ω |Ω| . ( 7
)
Let us remark that the above quotients are invariant under dilations and that convex sets which agree up to rigid motions (translations and rotations) are systematically identified throughout the paper.

Our main results are Theorems 1 and 6, which give sharp bounds for the functionals [START_REF] Freitas | A sharp upper bound for the first Dirichlet eigenvalue and the growth of the Isoperimetric Constant of convex domains[END_REF] when Ω varies in C. We also exhibit minimizing and maximizing sequences. These bounds are obtained by combining sharp bounds for the web p-torsion (see Theorem 2 and the second part of Theorem 6) with [START_REF] Crasta | Web functions: survey of results and perspectives[END_REF]. As a consequence of our results we obtain the validity of some weak forms of Pólya-Szegö conjecture (4). On the class P of convex polygons we introduce a sort of "asymmetry measure" such as

∀Ω ∈ P, γ(Ω) := |∂Ω| |∂Ω ⊛ | ∈ [1, +∞) ,
where Ω ⊛ denotes the regular polygon with the same area and the same number of vertices as Ω. Then, if the p-torsion τ p (Ω) is replaced by the web p-torsion w p (Ω), (4) holds in the following refined form:

∀ Ω ∈ P , w p (Ω) ≤ γ(Ω) -q w p (Ω ⊛ ) . (8)
Consequently, on the class P N of convex polygons with N vertices, conjecture (4) holds true for those Ω which are sufficiently "far" from Ω ⊛ , meaning that γ(Ω) exceeds a threshold depending on N and p:

∀ Ω ∈ P N : γ(Ω) ≥ Γ N,p , τ p (Ω) < τ p (Ω ⊛ ) . (9)
The value of the threshold Γ N,p can be explicitly characterized (see Corollary 4) and tends to 1 as p → +∞.

The paper is organized as follows. Section 2 contains the statement of our results, which are proved in Section 4 after giving in Section 3 some preliminary material of geometric nature. Section 5 is devoted to some related open questions and perspectives.

Results

We introduce the following classes of convex planar domains: C = the class of bounded convex domains in IR 2 ;

C o = the subclass of C given by tangential bodies to a disk; P = the class of convex polygons;

P N = the class of convex polygons having N vertices (N ≥ 3).

Tangential bodies to a disk are domains Ω ∈ C such that, for some disk D, through each point of ∂Ω there exists a tangent line to Ω which is also tangent to D. Domains in P ∩ C o are circumscribed polygons, whereas domains in C o \ P can be obtained by removing from a circumscribed polygon some connected components of the complement (in the polygon itself) of the inscribed disk. In particular, the disk itself belongs to C o . Our first results are the following sharp bounds for the p-torsion of convex planar domains. We recall that, for any given p ∈ (1, +∞), q := p p-1 denotes its conjugate exponent.

Theorem 1. For any p ∈ (1, +∞), it holds

∀Ω ∈ C, 1 q + 1 < τ p (Ω)|∂Ω| q |Ω| q+1 < 2 q+1 (q + 2)(q + 1) . ( 10
)
Moreover,

• the left inequality holds asymptotically with equality sign for any sequence of thinning rectangles;

• the right inequality holds asymptotically with equality sign for any sequence of thinning isosceles triangles.

By sequence of thinning rectangles or triangles, we mean that the ratio between their minimal width and diameter tends to 0. We point out that, in the particular case when p = 2, the statement of Theorem 1 is already known. Indeed, the left inequality in [START_REF] Hersch | Sur la fréquence fondamentale d'une membrane vibrante: évaluations par défaut et principe de maximum[END_REF] holds true for any simply connected set in IR 2 as discovered by Pólya [START_REF] Pólya | Two more inequalities between physical and geometrical quantities[END_REF]; the right inequality in [START_REF] Hersch | Sur la fréquence fondamentale d'une membrane vibrante: évaluations par défaut et principe de maximum[END_REF] for convex sets is due to Makai [START_REF] Makai | On the principal frequency of a membrane and the torsional rigidity of a beam[END_REF], though its method of proof, which is different from ours, does not allow to obtain the strict inequality.

Our approach to prove Theorem 1 employs as a major ingredient the following sharp estimates for the web p-torsion of convex domains, which may have their own interest.

Theorem 2. For any p ∈ (1, +∞), it holds

∀Ω ∈ C, 1 q + 1 < w p (Ω)|∂Ω| q |Ω| q+1 ≤ 2 q + 2 . ( 11
)
Moreover,

• the left inequality holds asymptotically with equality sign for any sequence of thinning rectangles;

• the right inequality holds with equality sign for Ω ∈ C o .

Let us now discuss the implications of the above results in the shape optimization problem which consists in maximizing τ p in the class of convex polygons with a given area and a given number of vertices:

max τ p (Ω) : Ω ∈ P N , |Ω| = m . ( 12
)
We recall that, for any Ω ∈ P, Ω ⊛ denotes the regular polygon with the same area and the same number of vertices as Ω. Moreover, we set

∀Ω ∈ P, γ(Ω) := |∂Ω| |∂Ω ⊛ | ;
notice that by the isoperimetric inequality for polygons (see Proposition 7),

γ(Ω) ∈ [1, +∞) and γ(Ω) > 1 if Ω = Ω ⊛ .
With this notation, it is straightforward to deduce from Theorem 2 the following Corollary 3. The regular polygon is the unique maximizer of w p over polygons in P with a given area and a given number of vertices. More precisely, the following refined isoperimetric inequality holds:

∀ Ω ∈ P , w p (Ω) ≤ γ(Ω) -q w p (Ω ⊛ ) . ( 13
)
As a consequence, using [START_REF] Crasta | Web functions: survey of results and perspectives[END_REF], we obtain some information on the shape optimization problem [START_REF] Pólya | Two more inequalities between physical and geometrical quantities[END_REF]:

Corollary 4. Let Γ N,p := w p (Ω ⊛ ) τ p (Ω ⊛ ) 1/q 2 (q + 1) 1/q . Then, ∀ Ω ∈ P N , τ p (Ω) < Γ q N,p γ(Ω) -q τ p (Ω ⊛ ) .
In particular, the p-torsion of the regular N -gon is larger than the p-torsion of any polygon in P N having the same area and an asymmetry measure larger than the threshold Γ N,p :

∀ Ω ∈ P N , γ(Ω) ≥ Γ N,p ⇒ τ p (Ω) < τ p (Ω ⊛ ) . (14)
Some comments on Corollary 4 are gathered in the next remark.

Remark 5. (i) Using again (6) we infer

1 < Γ N,p < 2 (q + 1) 1/q < 2 ∀N, p , lim p→+∞ Γ N,p = 1 .
Hence, asymptotically with respect to p, the condition γ(Ω) ≥ Γ N,p appearing in [START_REF] Solynin | An isoperimetric inequality for logarithmic capacity of polygons[END_REF] becomes not restrictive. Moreover, if p = 2, we have Γ N,2 ≤ 2/ √ 3 ≈ 1.15 and the dependence on N of Γ N,2 can be enlightened by using the numerical values given in [START_REF] Crasta | Web functions: survey of results and perspectives[END_REF]: (ii) Though the validity of ( 4) is known for triangles, in order to give an idea of the efficiency of Corollary 4, consider the case N = 3 and p = 2. The equilateral triangle

T ⊛ := (x, y) ∈ IR 2 ; y > 0 , - 1 2 + y √ 3 < x < 1 2 - y √ 3 satisfies |T ⊛ | = √ 3 4 and |∂T ⊛ | = 3. The solution to (1) is explicitly given by u(x, y) = √ 3 8 y - 4 √ 3 y 2 + 4 3 y 3 -4x 2 y so that τ 2 (T ⊛ ) = √ 3/
ℓ k = 3 4k 2 + k 2 4 so that |∂T k | = k + 3 k 2 + k 2 and |T k | = √ 3 4 = |T ⊛ | , (notice that T 1 = T ⊛ ). Therefore, γ(T k ) = k + 3 k 2 + k 2 3 and γ(T k ) ≥ Γ 3,2 if and only if 2 √ 10 k 3 -10 k 2 + 3 ≥ 0, which approximatively corresponds to k ∈ (0.760, 1.301).
We conclude this section with a variant of Theorems 1 and 2. Theorem 6. For every p ∈ (1, +∞), it holds

∀Ω ∈ C, 1 (q + 2)2 q-1 ≤ τ p (Ω) R q Ω |Ω| < 2 q (q + 1) 2 (15) ∀Ω ∈ C, 1 (q + 2)2 q-1 ≤ w p (Ω) R q Ω |Ω| < 1 q + 1 . ( 16
)
Moreover,

• the left inequality in (15) holds with equality sign for balls;

• the left inequality in (16) holds with equality sign for Ω ∈ C o ;

• the right inequality in (16) holds asymptotically with equality sign for a sequence of thinning rectangles.

The right inequality in (15) is not sharp. In fact, for p = 2, one has the sharp inequalities

∀Ω ∈ C, 1 8 ≤ τ 2 (Ω) R 2 Ω |Ω| ≤ 1 3 ,
see [13, p. 100] for the left one, and [START_REF] Makai | On the principal frequency of a membrane and the torsional rigidity of a beam[END_REF] for the right one.

Using the isoperimetric inequalities (15) and ( 16), one can also derive statements similar to Corollaries 3 and 4, where γ(Ω) is replaced by another "asymmetry measure" given by

γ(Ω) = R Ω ⊛ R Ω .

Geometric preliminaries

In this section we present some useful geometric properties of convex polygons, which will be exploited to prove Theorem 2. First, we recall an improved form of the isoperimetric inequality in the class P, whose proof can be found for instance in [3, Theorem 2]. For any Ω ∈ P, we set

C Ω := i cotan θ i 2 , being θ i the inner angles of Ω . ( 17
)
Proposition 7. For every Ω ∈ P, it holds

|Ω| ≤ |∂Ω| 2 4C Ω , ( 18
)
with equality sign if and only if Ω ∈ P ∩ C o , namely when Ω is a circumscribed polygon.

Next, we recall that, denoting by R Ω the inradius of any Ω ∈ P, for every t ∈ [0, R Ω ], the inner parallel sets of Ω are defined by

Ω t := {x ∈ Ω : dist(x, ∂Ω) > t} (notice in particular that Ω R Ω = ∅).
Then we focus our attention on the behaviour of the map t → C Ωt on the interval [0, R Ω ], and on the related expression of Steiner formulae. For every Ω ∈ P, we set

r Ω := sup t ∈ [0, R Ω ]
: Ω t has the same number of vertices as Ω .

Clearly, if r Ω < R Ω , the number of vertices of Ω t is strictly less than the number of vertices of Ω for every t ∈ [r Ω , R Ω ).

Proposition 8. For every Ω ∈ P and t ≥ 0, Ω t ∈ P and the map t

→ C Ωt is piecewise constant on [0, R Ω ).
Moreover, for every t ∈ [0, r Ω ], it holds

|Ω t | = |Ω| -|∂Ω|t + C Ω t 2 and |∂Ω t | = |∂Ω| -2C Ω t. ( 19
)
Finally, for every t ∈ [0, R Ω ], it holds

|∂Ω t | ≤ |∂Ω| -2πt. ( 20
)
Proof. For t small enough, the sides of Ω t are parallel and at distance t from the sides of Ω, and the corners of Ω t are located on the bisectors of the angles of Ω. r Ω is actually the first time when two of these bisectors intersect at a point having distance t from at least two sides, see Figure 1.

Ω r Ω ∂Ω t θ i θ i+1
r Ω

Figure 1: Intersection of bisectors

Therefore, for t < r Ω , Ω t has the same angles as Ω (so C Ωt = C Ω by ( 17)), and we notice that the perimeter of grey areas in Figure 2 is 2t cotan(θ i /2), and their areas are t 2 cotan(θ i /2), which gives (19) (still valid for t = r Ω by continuity). Let us now show that the map t → C Ωt is piecewise constant on [0, R Ω ), assuming that r Ω < R Ω . Once t = r Ω , Ω t still has sides parallel to the ones of Ω but loses at least one of them. Again, C Ωt is constant for t ≥ r Ω until the next value of t such that another intersection of bisectors appears (we now consider bisectors of Ω r Ω ). The number of discontinuities of t → C Ωt is finite since Ω has a finite number of sides, and therefore iterating the previous argument, we get that t → C Ωt is piecewise constant. Finally, from (17) we infer that C Ω ≥ π for any Ω ∈ P, so that (20) follows from the concavity of the map

θ i θ i+1 t
t → |∂Ω t | on [0, R Ω ] (see [1,

Sections 24 and 55]).

A special role is played by polygons Ω ∈ P such that r Ω = R Ω , namely polygons Ω whose inner parallel sets all have the same number of vertices as Ω itself. These are polygonal stadiums, characterized by the following Definition 9. We call S the class of polygonal stadiums, namely polygons P ℓ ∈ P such that there exist a circumscribed polygon P ∈ P ∩ C o having two parallel sides, and a nonnegative number ℓ such that, by choosing a coordinate system with origin in the center of the disk inscribed in P and the x-axis directed as two parallel sides of P , P ℓ can be written as

P ℓ := P -- ℓ 2 , 0 - ℓ 2 , ℓ 2 × -R P , R P P + + ℓ 2 , 0 , (21)
where P -(resp. P + ) denotes the set of points (x, y) ∈ P with x < 0 (resp. x > 0), and R P is the inradius of P , see Figure 3. Proof. We use the same notation as in Definition 9. Assume that Ω = P ℓ ∈ S. Then the bisectors of the angles of Ω intersect either at (-ℓ 2 , 0) or at ( ℓ 2 , 0), which are at distance R Ω from the boundary, see Figure 4. In particular, if Ω is circumscribed to a disk, namely if ℓ = 0, then the bisectors of the angles of Ω all intersect at the center of the disk. Therefore, Ω t has the same number of sides as Conversely, assume that R Ω = r Ω . The set {x ∈ Ω : d(x) = R Ω } is convex with empty interior, so either it is a point, or a segment. If it is a point, then its distance to each side is the same, and therefore the disk having this point as a center and radius R Ω is tangent to every side of Ω, so that Ω is circumscribed to a disk. If it is a segment, we choose coordinates such that this segment is -ℓ 2 , 0 ; ℓ 2 , 0 for some positive number ℓ. Every point of this segment is at distance R Ω from the boundary, so Ω the rectangle -ℓ 2 , ℓ 2 × (-R Ω , R Ω ). Considering

R P P × O R P ℓ P ℓ × O
Ω if t < R Ω . R Ω ℓ Ω t
P := Ω ∩ x ≤ - ℓ 2 + ℓ 2 , 0 Ω ∩ x ≥ ℓ 2 + - ℓ 2 ,
|P ℓ | = |P | + 2ℓR P , |∂P ℓ | = |∂P | + 2ℓ , C P ℓ = C P , R P ℓ = R P ,
and the following identities holding for every P ∈ P ∩ C o

C P = |P | R 2 P , |∂P | = 2|P | R P . (22)
Finally, we show that the parallel sets of any convex polygon Ω are polygonal stadiums for t sufficiently close to R Ω :

Proposition 12. For every Ω ∈ P, there exists t ∈ [0, R Ω ) such that the parallel sets Ω t belong to S for every t ∈ t, R Ω .

Proof. We define t as the last time t < R Ω such that Ω loses a side (we may have t = 0). Therefore ∀t ∈ t, R Ω , Ω t has a constant number of sides, and so is in the class S by Proposition 10.

Proofs

Proof of Theorem 2

We first prove Theorem 2 for Ω ∈ P, then we prove it for all Ω ∈ C.

•

Step 1: comparison with inner parallel sets. For a given Ω ∈ P, we wish to compare the value of the energy

wp(Ω)|∂Ω| q |Ω| q+1
with the one of its parallel set Ω ε for small ε. To that aim, we use the representation formula (5) for w p (Ω), and Steiner's formulae (19). In applying them we recall that, by Proposition 8 the map t → C Ωt is piecewise constant for t ∈ [0, R Ω ), and in particular it equals C Ω on [0, r Ω ]. Taking also into account that (Ω ε ) t = Ω ε+t , as ε → 0 we have

w p (Ω ε )|∂Ω ε | q |Ω ε | q+1 = R Ω -ε 0 |(Ωε)t| q |∂(Ωε)t| q-1 dt |∂Ω ε | q |Ω ε | q+1 (23) = w p (Ω) - ε 0 |Ωt| q |∂Ωt| q-1 dt [|∂Ω| -2C Ω ε] q [|Ω| -|∂Ω| ε] q+1 + o(ε), = |∂Ω| q |Ω| q+1 w p (Ω) - |Ω| q |∂Ω| q-1 ε 1 -2q C Ω |∂Ω| ε 1 + (q + 1) |∂Ω| |Ω| ε + o(ε), = w p (Ω)|∂Ω| q |Ω| q+1 + (q + 1) |∂Ω| q+1 |Ω| q+2 w p (Ω) - |∂Ω| |Ω| -2q C Ω w p (Ω)|∂Ω| q-1 |Ω| q+1 ε + o(ε), so that w p (Ω ε )|∂Ω ε | q |Ω ε | q+1 - w p (Ω)|∂Ω| q |Ω| q+1 = (q + 1) |∂Ω| q+1 |Ω| q+2 w p (Ω) - |∂Ω| |Ω| -2q C Ω w p (Ω)|∂Ω| q-1 |Ω| q+1 ε + o(ε) . ( 24
)
As we shall see in the next steps, formula (24) will enable us to reach a contradiction if (11) fails.

• Step 2: if [START_REF] Makai | On the principal frequency of a membrane and the torsional rigidity of a beam[END_REF] fails for some convex polygon then it also fails for a polygonal stadium. Let Ω ∈ P \ S, and assume that ( 11) fails. We have to distinguish two cases.

First case: Assume that

w p (Ω)|∂Ω| q |Ω| q+1 > 2 q + 2 . ( 25
)
Using the isoperimetric inequality ( 18) and (25), one gets

(q + 1) |∂Ω| q+1 |Ω| q+2 w p (Ω) - |∂Ω| |Ω| -2q C Ω w p (Ω)|∂Ω| q-1 |Ω| q+1 ≥ q + 2 2 |∂Ω| |Ω| w p (Ω)|∂Ω| q |Ω| q+1 - 2 q + 2 > 0 .
Inserting this information into (24) shows that

w p (Ω ε )|∂Ω ε | q |Ω ε | q+1 - w p (Ω)|∂Ω| q |Ω| q+1 > 0
for sufficiently small ε. In fact, more can be said. By Proposition 8 we know that C Ωt = C Ω for all t ∈ [0, r Ω ). By extending the above argument to all such t, we obtain that, if (25) holds, then the map t → wp(Ωt)|∂Ωt| q |Ωt| q+1 is strictly increasing for t ∈ [0, r Ω ). In particular, by (25),

w p (Ω ε )|∂Ω ε | q |Ω ε | q+1 > w p (Ω)|∂Ω| q |Ω| q+1 > 2 q + 2 ∀ε ∈ (0, r Ω ].
So, if Ω r Ω ∈ S , we are done since it violates [START_REF] Makai | On the principal frequency of a membrane and the torsional rigidity of a beam[END_REF]. At t = r Ω the number of sides of Ω t varies. If Ω r Ω / ∈ S, we repeat the previous argument to the next interval where C Ωt remains constant. Again, the map t → wp(Ωt)|∂Ωt| q |Ωt| q+1 is strictly increasing on such interval. In view of Proposition 12, this procedure enables us to obtain some polygonal stadium such that (25) holds. Second case: Assume that

w p (Ω)|∂Ω| q |Ω| q+1 ≤ 1 q + 1 . (26)
Hence,

(q + 1) |∂Ω| q+1 |Ω| q+2 w p (Ω) - |∂Ω| |Ω| -2q C Ω w p (Ω)|∂Ω| q-1 |Ω| q+1 = (q + 1) |∂Ω| |Ω| |∂Ω| q |Ω| q+1 w p (Ω) - 1 q + 1 - 2q q + 1 C Ω w p (Ω)|∂Ω| q-2 |Ω| q < 0 .
Inserting this into (24) and arguing as in the previous case, we see that the map t → wp(Ωt)|∂Ωt| q |Ωt| q+1 is strictly decreasing for t ∈ [0, R Ω ). In view of Proposition 12, this proves that there exists some polygonal stadium such that (26) holds.

• Step 3: explicit computation for a polygonal stadium. Let Ω = P ℓ ∈ S be a polygonal stadium. We are going to derive an explicit expression for the function

F (ℓ) := w p (P ℓ )|∂P ℓ | q |P ℓ | q+1 ∀ ℓ ≥ 0 .
We point out that, in the special case ℓ = 0, Ω ∈ P ∩ C o (namely Ω is a circumscribed polygon), and it is proven in [4, Proposition 2] that

∀Ω ∈ C o , w p (Ω)|∂Ω| q |Ω| q+1 = 2 q + 2 . ( 27
)
In particular, formula (27) shows that the upper bound in ( 11) is achieved when Ω ∈ C o . We now show that the above formula can be suitably extended also to the case ℓ > 0. Our starting point is the representation formula [START_REF] Crasta | Some estimates of the minimizing properties of web functions[END_REF]. Therein, we use the Steiner formulae (19); in particular, by Propositions 8 and 10, we know that C Ωt ≡ C Ω for every t ∈ [0, R Ω ). Moreover, since P ∈ P ∩ C o , we can exploit identities (22). Setting for brevity

A := |P | , R := R P , x := 2Rℓ A ,
we obtain

F (ℓ) = 2 A R + 2ℓ q (A + 2Rℓ) q+1 R 0 A + 2Rℓ -2ℓt -2 A R t + A R 2 t 2 q 2ℓ + 2 A R -2 A R 2 t q-1 dt = (x + 2) q (x + 1) q+1 1 0 (1 + x -xt -2t + t 2 ) q (x + 2 -2t) q-1 dt = (x + 2) q (x + 1) q+1 1 0 t q (x + t) q (x + 2t) q-1 dt . (28)
Of course, taking x = 0 in (28) gives again (27); on the other hand, taking x → ∞ gives the asymptotic behaviour for thinning polygonal stadiums.

• Step 4: In view of equality (28) obtained in Step 3, the estimate (11) will be proved for any polygonal stadium, provided we show that for all q ∈ (1, +∞) one has

1 q + 1 < (x + 2) q (x + 1) q+1 1 0 t q (x + t) q (x + 2t) q-1 dt < 2 q + 2 ∀x ∈ (0, +∞). (29)
With the change of variables t = xs, the inequalities in (29) become

1 q + 1 (x + 1) q+1 x q+2 (x + 2) q < 1/x 0 s q (1 + s) q (1 + 2s) q-1 ds < 2 q + 2 (x + 1) q+1 x q+2 (x + 2) q ∀x ∈ (0, +∞).
In turn, by putting y = 1/x, the latter inequalities become

1 q + 1 y q+1 (1 + y) q+1 (1 + 2y) q < y 0 s q (1 + s) q (1 + 2s) q-1 ds < 2 q + 2 y q+1 (1 + y) q+1
(1 + 2y) q ∀y ∈ (0, +∞).

In order to prove the right inequality in (30), consider the function Φ(y) := y 0 s q (1 + s) q (1 + 2s) q-1 ds -2 q + 2 y q+1 (1 + y) q+1

(1 + 2y) q y ∈ (0, +∞)

and we need to prove that Φ(y) < 0 for all y > 0. This is a consequence of the two following facts:

Φ(0) = 0 , Φ ′ (y) = - q q + 2 y q (1 + y) q (1 + 2y) q+1 < 0 .
In order to prove the left inequality in (30), consider the function Ψ(y) := y 0 s q (1 + s) q (1 + 2s) q-1 ds -

1 q + 1 y q+1 (1 + y) q+1
(1 + 2y) q y ∈ (0, +∞)

and we need to prove that Ψ(y) > 0 for all y > 0. This is a consequence of the two following facts:

Ψ(0) = 0 , Ψ ′ (y) = 2q q + 1 y q+1 (1 + y) q+1
(1 + 2y) q+1 > 0 .

Both inequalities in (30) are proved and (29) follows.

We point out that, in the case q = 2, some explicit computations give the stronger result that the map

x → (x + 2) q (x + 1) q+1 1 0 t q (x + t) q (x + 2t) q-1 dt is decreasing. We believe that this is true for any q, but we do not have a simple proof of this property.

• Step 5: conclusion. Let Ω ∈ P and assume for contradiction that Ω violates [START_REF] Makai | On the principal frequency of a membrane and the torsional rigidity of a beam[END_REF]. Then by Step 2 we know that there exists a polygonal stadium which also violates [START_REF] Makai | On the principal frequency of a membrane and the torsional rigidity of a beam[END_REF]. This contradicts Step 4, see (29). We have so far proved that [START_REF] Makai | On the principal frequency of a membrane and the torsional rigidity of a beam[END_REF] holds for all Ω ∈ P. By a density argument we then infer that

∀Ω ∈ C, 1 q + 1 ≤ w p (Ω)|∂Ω| q |Ω| q+1 ≤ 2 q + 2 . (31)
Therefore, in order to complete the proof we need to show that the left inequality in (31) is strict. Assume for contradiction that there exists Ω ∈ C such that

w p (Ω)|∂Ω| q |Ω| q+1 = 1 q + 1 . ( 32
)
Take any sequence Ω k ∈ P such that Ω k ⊃ Ω and Ω k → Ω in the Hausdorff topology. Similar computations as in (23), combined with (20), enable us to obtain

w p (Ω k ε )|∂Ω k ε | q |Ω k ε | q+1 ≤ w p (Ω k ) - ε 0 |Ω k t | q |∂Ω k t | q-1 dt |∂Ω k | -2π ε q [|Ω k | -|∂Ω k | ε] q+1 ≤ w p (Ω k )|∂Ω k | q |Ω k | q+1 + (q + 1) |∂Ω k | q+1 |Ω k | q+2 w p (Ω k ) - |∂Ω k | |Ω k | -2q πw p (Ω k )|∂Ω k | q-1 |Ω k | q+1 ε + αε 2 ,
where α is some positive constant, depending on Ω but not on k. Therefore, since Ω k t → Ω t for all t ∈ [0, R Ω ], we have

w p (Ω ε )|∂Ω ε | q |Ω ε | q+1 - w p (Ω)|∂Ω| q |Ω| q+1 = w p (Ω k ε )|∂Ω k ε | q |Ω k ε | q+1 - w p (Ω k )|∂Ω k | q |Ω k | q+1 + o(1) ≤ o(1) -2q πw p (Ω k )|∂Ω k | q-1 |Ω k | q+1 ε + αε 2 + o(1)
where o(1) are infinitesimals (independent of ε) as k → ∞. Hence, by letting k → ∞ and taking ε sufficiently small, we obtain wp(Ωε)|∂Ωε| q |Ωε| q+1 < 1 q+1 , which contradicts (31).

Proof of Theorem 1

The inequalities [START_REF] Hersch | Sur la fréquence fondamentale d'une membrane vibrante: évaluations par défaut et principe de maximum[END_REF] follow directly from ( 11) and ( 6) so we just need to show that they are sharp.

For the right inequality, take a sequence of thinning isosceles triangles T k . Then, by Theorem 2 we have

w p (T k )|∂T k | q |T k | q+1 = 2 q + 2
for all k .

On the other hand, by [4, Proposition 3] and ( 6) we know that

lim k→∞ w p (T k ) τ p (T k ) = q + 1 2 q
and therefore

lim k→∞ τ p (T k )|∂T k | q |T k | q+1 = 2 q+1 (q + 2)(q + 1)
.

For the left inequality, we seek an upper bound for τ p (Ω) by using the maximum principle. For all ℓ ∈ (0, +∞) let Ω ℓ = (-ℓ 2 , ℓ 2 ) × (-1, 1) and let u ℓ be the unique solution to

-∆ p u ℓ = 1 in Ω ℓ , u ℓ = 0 on ∂Ω ℓ . Let u ∞ (x, y) = p-1 p (1 -|y| p/(p-1) ) so that -∆ p u ∞ = 1 in Ω ℓ , u ∞ ≥ 0 on ∂Ω ℓ .
By the maximum principle, we infer that u ∞ ≥ u ℓ in Ω ℓ so that

τ p (Ω ℓ ) = Ω ℓ u ℓ ≤ Ω ℓ u ∞ = 2(p -1) p ℓ 1 0 (1 -y p/(p-1) ) dy = 2(p -1) 2p -1 ℓ = 2ℓ q + 1 .
Hence,

1 ≥ lim inf ℓ→∞ w p (Ω ℓ ) τ p (Ω ℓ ) ≥ lim inf ℓ→∞ (q + 1)w p (Ω ℓ ) 2ℓ = 1
where the last equality follows from Theorem 2. Combined with Theorem 2, this proves that

lim ℓ→∞ τ p (Ω ℓ )|∂Ω ℓ | q |Ω ℓ | q+1 = 1 q + 1 .

Proof of Theorem 6

Since it follows closely the proof of Theorem 1, we just sketch it. We first prove the counterpart of Theorem 2 and we follow the same steps.

• Step 1. Given Ω ∈ P and using R Ωε = R Ωε + o(ε) we prove:

w p (Ω ε ) R Ωε |Ω ε | - w p (Ω) R Ω |Ω| = ε R q Ω |Ω| w p (Ω) q R Ω + |∂Ω| |Ω| - |Ω| q |∂Ω| q-1 + o(ε) . (33)
• Step 2. We prove that, if (16) fails for some Ω ∈ P, then it also fails for a polygonal stadium. To that end, we estimate the sign in (33) with the help of the following classical geometric inequalities (see [START_REF] Bonnesen | Theory of convex bodies[END_REF])

∀Ω ∈ C, |Ω| R Ω < |∂Ω| ≤ 2|Ω| R Ω .
• Step 3. Again, explicit computations can be done for a polygonal stadium, and with the same notation as in the proof of Theorem 2, we get:

w p (P ℓ ) R q P ℓ |P ℓ | = 1 x + 1 1 0 t q (x + t) q (x + 2t) q-1 dt ∀P ℓ ∈ S .
• Step 4. In view of Step 3, estimate (15) is proved for any polygonal stadium, provided for all q ∈ (1, +∞) one has 1 (q + 2)2 q-1 <

1 x + 1 1 0 t q (x + t) q (x + 2t) q-1 dt < 1 q + 1 ∀x ∈ (0, +∞). (34)
With the change of variables t = xs and putting y = 1/x, the inequalities in (34) become

y q+2 + y q+1 (q + 2)2 q-1 < y 0 s q (1 + s) q (1 + 2s) q-1 ds < y q+2 + y q+1 q + 1 ∀y ∈ (0, +∞). (35)
Some tedious but straightforward computations show that y q+1 2 q-1 + q + 1 (q + 2)2 q-1 y q < y q (1 + y) q (1 + 2y) q-1 < q + 2 q + 1 y q+1 + y q ∀y ∈ (0, +∞) and (35) follows after integration over (0, y).

• Step 5. The previous steps leads to (16) for polygons and by density for convex domains. The strict right inequality in (16) can be obtained by reproducing carefully the computations in Step 1, similarly as done in

Step 5 of Section 4.1. Now the counterpart of Theorem 2 is proved, and we may use [START_REF] Crasta | Web functions: survey of results and perspectives[END_REF] in order to get (15) from (16). Balls realize equality in the left inequality of (15) because the are at the same time circumscribed and maximal for the quotient w p /τ p .

Some open problems

We briefly suggest here some perspectives which might be considered, in the light of our results.

Sharp bounds for the p-torsion in higher dimensions. In higher dimensions the shape functionals τ p and w p can be defined in the analogous way as for n = 2. In [START_REF] Crasta | Estimates for the energy of the solutions to elliptic Dirichlet problems on convex domains[END_REF], Crasta proved the following sharp bounds:

∀ Ω bounded convex set ⊂ IR n , n + 1 2n < w 2 (Ω) τ 2 (Ω) ≤ 1 .
Therefore it seems natural to ask: what kind of isoperimetric inequality can be proved for w p and τ p among convex sets in IR n ? In this direction, let us quote an inequality proven in [START_REF] Freitas | A sharp upper bound for the first Dirichlet eigenvalue and the growth of the Isoperimetric Constant of convex domains[END_REF], obtained by a strategy similar to our approach, that is by looking at the level sets of the support function:

∀ Ω bounded convex set ⊂ IR n , τ 2 (Ω)|∂Ω| R Ω |Ω| 2 ≥ τ 2 (B)|∂B| R B |B| 2 (B is a ball of IR n ).
Sharp bounds for the principal frequency. A notion of "web principal frequency" can be defined (in any space dimension) similarly as done for the web torsion, that is

λ + 1 (Ω) := inf Ω |∇u| 2 Ω u 2 : u ∈ W 2 (Ω) .
Writing the optimality condition in the space W 2 (Ω), one can express λ + 1 (Ω) as

λ + 1 (Ω) = inf R Ω 0 αρ ′2 R Ω 0 αρ 2 : ρ ∈ H 1 (0, R Ω ) , ρ(0) = 0 , where α(t) = |∂Ω t |.
It is clear that λ + 1 (Ω) ≥ λ 1 (Ω), with equality sign when Ω is a ball. On the other hand, the following questions can be addressed: • Find a sharp bound from above for the ratio λ + 1 (Ω)/λ 1 (Ω) among bounded convex subsets of IR n . • Is it possible to apply successfully the same strategy of this paper, that is find sharp bounds for λ + 1 (Ω) and then use the estimates on the ratio λ + 1 (Ω)/λ 1 (Ω), to deduce sharp bounds for λ 1 (Ω)? In particular, this approach might allow to retrieve the following known inequalities holding for any bounded convex domain Ω ⊂ IR 2 (see [START_REF] Hersch | Sur la fréquence fondamentale d'une membrane vibrante: évaluations par défaut et principe de maximum[END_REF][START_REF] Makai | On the principal frequency of a membrane and the torsional rigidity of a beam[END_REF][START_REF] Pólya | Two more inequalities between physical and geometrical quantities[END_REF]):

π 2 16 ≤ λ 1 (Ω) |Ω| 2 |∂Ω| 2 ≤ π 2 4 and π 2 4 ≤ λ 1 (Ω)R 2 Ω ≤ j 2 0 .

Figure 2 :

 2 Figure 2: How to derive Steiner formulae

Figure 3 :Proposition 10 .

 310 Figure 3: A circumscribed polygon P and a polygonal stadium P ℓ Proposition 10. Let Ω ∈ P. There holds r Ω = R Ω if and only if Ω ∈ S.

Figure 4 :

 4 Figure 4: Parallel sets of a polygonal stadium P ℓ

  640. Moreover, by (27) below we find w 2 (T ⊛ ) = √ 3/768 and, in turn, that Γ 3,2 = √ 10/3 ≈ 1.054. Consider now the isosceles triangles T k having the basis of length k > 0 and the two equal sides of length

Acknowledgments. This work was realized thanks to the financial support of the Italian Gruppo Nazionale per l'Analisi Matematica, la Probabilità e le loro Applicazioni, as part of the project "Problemi di ottimizzazione e disuguaglianze geometrico-funzionali", and by the French Agence Nationale de la Recherche, as part of the project ANR-09-BLAN-0037 "Geometric analysis of optimal shapes".