Hugues Cassé

Florian Birée

Pascal Sainrat

Multi-architecture Value Analysis for Machine Code *

Keywords: machine code, static analysis, value analysis, semantics Digital Object Identifier 10.4230/OASIcs.WCET.2013.42 1

Safety verification of critical real-time embedded systems requires Worst Case Execution Time information (WCET). Among the existing approaches to estimate the WCET, static analysis at the machine code level has proven to get safe results. A lot of different architectures are used in real-time systems but no generic solution provides the ability to perform static analysis of values handled by machine instructions. Nonetheless, results of such analyses are worth to improve the precision of other analyzes like data cache, indirect branches, etc.

This paper proposes a semantic language aimed at expressing semantics of machine instructions whatever the underlying instruction set is. This ensures abstraction and portability of the value analysis or any analysis based on the semantic expression of the instructions.

As a proof of concept, we adapted and refined an existing analysis representing values as Circular-Linear Progression (CLP), that is, as a sparse integer interval effective to model pointers. In addition, we show how our semantic instructions allow to build back conditions of loop in order to refine the CLP values and improve the precision of the analysis.

Both contributions have been implemented in our framework, OTAWA, and experimented on the Malärdalen benchmark to demonstrate the effectiveness of the approach.

Introduction

Safety of critical embedded real-time applications needs to be verified in order to avoid catastrophic issues. This verification concerns not only functional features but also nonfunctional ones like temporal properties. The Worst Case Execution Time (WCET) is an important element of time properties. Its computation by static analysis is required at the machine level to get confident results. Some tools, like OTAWA [3], provide a generic framework to perform these kinds of analyses whatever the underlying architecture is, including programming and execution models. In this article, we show how to adapt static analysis of data flow analysis to the machine code. More precisely, we have adapted and improved the circular-linear representation of integer values of [START_REF] Rathijit | Wcet estimation for executables in the presence of data caches[END_REF] [START_REF] Rathijit | Executable analysis using abstract interpretation with circular linear progressions[END_REF] to any machine code using an architecture-independent language while maintaining fast convergence for the fixpoint computation. Such an analysis is utterly important as its results can be used in the implementation of a lot of other analyses concerning control or data flow. For example, it can be used to compute the targets of indirect branches (pointer call or optimized switch implementations using indirection tables) or to identify statically code that is dynamically dead (typically in library functions where some conditions are always false because of the call context). Data flow uses include the analysis of data caches, of array accesses (bounding of the array range in memory), of the stack size (very important in embedded applications with small memory sizes) and infeasible paths by providing information on the program conditions.

This article is divided in 5 sections. In the first one, we present the abstraction of the machine language and its application to Abstract Interpretation (AI). The second section presents the clp representation of values and a proposed refinement based on the decoding of branch conditions. Then, Section 3 gives the results of the experimentations and we provide in Section 4 a comparison with existing value analyses. The last section concludes the paper.

Value Analysis at Machine Code Level

In this section, we first present the abstraction of the machine instructions and how to use it to build an AI.

Independent Machine Language

As critical embedded real-time systems are running on very different architectures, OTAWA provides an abstraction of the machine instruction semantics. This avoids (a) to tie the analysis to a particular instruction set and (b) to focus only on the more useful part of the instruction behaviour to analyze the computation of integer values and addresses. Unlikely to an RTL (Register Transfer Language) language, it is designed to make the static analyses easier and faster. Especially, it avoids actions internal to the microprocessor that are neither relevant, nor supported by the value analysis. This language, presented in Table 1, is composed of very simple a-la RISC instructions working either on machine registers, or on temporaries. As some instructions may be very complex, one machine instruction may match a block of semantic instructions.

add d, a, b d ← a + b sub d, a, b d ← a -b shl d, a, b d ← a b shr d, a, b d ← a b asr d, a, b d ← a + b set d, a d ← a seti d, i d ← i scratch d d ← cmp d, a, b d ← a ∼ b store d, a, t Mt[a] ← d load d, a, t d ← Mt[a] if c, a, i if a = c then ic ← ic + i branch d pc ← d cont stop interpretation d,
The semantic instructions set have been designed to be minimal and canonical and, therefore, to make their support in analysis easier: there is only one instruction performing a semantic function. Consequently, there are only addition, subtraction, shift and move operations. As our goal is only to support arithmetics on integer and particularly on address computation, we have included neither multiplication, nor division. These operations, often on powers of 2, are implemented more efficiently as shifts. In the same way, we have no equivalent of bit-to-bit operations like NOT, AND or OR as they do not produce precise results on interval analysis. The special instruction scratch(r) is needed to cope with these limitations: it means that the variable r is modified in a way that cannot be described by the semantic language. Indeed, there are always machine operations too atypical to be supported but a sound static analysis requires to mark r as modified even if the exact value cannot be expressed.

As a machine instruction is usually translated into a semantic instruction block, temporary variables are needed to pass computation intermediate results all along the block. They may take place of machine register in the semantic instructions but their life is bounded to the machine instruction block.

Another important concept to support is the conditional execution of some semantic instructions. In a machine instruction set, this is performed by using a comparison instruction followed by a branch instruction to modify the control flow accordingly. This scheme is currently supported by the semantic instructions but with some limitations.

First, there is a comparison instruction cmp that compares two values and stores the result in a target register (usually the status register of the underlying architecture). Then the comparison result is used by an if instruction. If the comparison from register a is equal to the c condition argument, the semantic instruction execution continues. Otherwise, the i following instructions are skipped and the execution continues just after them. An important outcome of such a structure is that the instruction block can exhibit several execution paths but no loop. This is an important property because the fixpoint computation induced by loops needs expensive computation time: several analyses are performed on the loop body. cont is the second and last instruction handling the semantics control flow: it stops the execution of the current path. It must be noticed that a cont is implicitely assumed at the end of a block. The if and cont handle the control flow of the semantic instructions but there are also an instruction to represent control at the machine instruction level. The branch instruction informs that the machine control will change according to the address found in its arguments An important point to keep in mind is that this instruction does not modify the execution flow of the semantic instructions in the block: this one continues until the end of the block. It just denotes control flow changes in the machine instructions, i.e. modification of the PC.

Finally, load and store allow to load from, or store to, the memory. The first argument is the handled value while the second contains the address. The last one is the size of handled data in bytes.

This language makes easy and straight-forward the translation of most machine instructions but it may require more work when processing instructions as complex as multiple load-store to memory. An intermediate special computation phase is required but benefits from the instruction arguments, constant in the instruction code at the generation time. For example, a particular multiple-load instruction in memory gives the precise list of loaded registers and we can generate as many load semantic instructions as required. This genera- [START_REF] Ferdinand | Static Memory and Timing Analysis of Embedded Systems Code[END_REF]; add(t 1 , t 1 , t 2 )] end for seti ( t1 , 0) add ( t1 , r1 , t1 ) seti ( t2 , 4) load ( r29 , t1 , 4); add ( t1 , t1 , t2 ) load ( r30 , t1 , 4); add ( t1 , t1 , t2 ) load ( r31 , t1 , 4); add ( t1 , t1 , t2 )

Algorithm 1 lmw r d , k(r a ) b ← [seti(t 1 , k); add(t 1 , t a , t 1 ); seti(t2, 4)] for i ← d to 31 do b ← b :: [load(r i , t 1 ,
Listing 1 lmw r29, 0(r1).
tion is performed only once per instruction and makes the static analysis faster: semantic instruction blocks are simpler than the full translation inducing loops. This is illustrated by Algorithm 1 that shows the generation of semantics instructions list (between '[' and ']') for the PowerPC lmw instructions: starting from address r a + k, it loads registers from r d to r 31 . As d, a and k are constant at the translation time, a particular instantiation, as shown at the right, just gives a sequence of loads.

AI with Semantic Instructions

The semantic instructions have been designed to promote static analyses and more particularly AI. AI [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] analyzes a program by abstracting the state S along the different execution paths. With machine code, AI is often performed on the Control Flow Graph (CFG), G = V × E, where the vertices V represent Basic Blocks (BB), a block of consecutive instructions executed together, and edges, E = V × V , the control flow between BB.

Algorithm 2 CFG Interpretation

wl

← {v 0 } while wl = [] do v i , wl ← wl s ← update(v i , join({s j /(v j , v i ) ∈ E})) if s = s i then s i ← s wl = wl ∪ {v j /(v i , v j ) ∈ E} end if end while Algorithm 3 update([I 0 , I 1 , ..., I n-1 ], s 0 ) s r ← ⊥; wl ← {(0, s 0 )} while wl = [] do (i, s), wl ← wl if i ≥ n then s r ← s r ∪ s else if I i = if (c, a, d) then wl ← wl ∪ {(i + 1, s), (i + d, s)} else wl ← wl ∪ {(i + 1, update I (I i ))} end if end while
Algorithm 2 is a common implementation of the AI on the CFG. v 0 ∈ V is the entry vertex of the CFG and the s i ∈ S # are the abstractions of the real state at the different program points. S # is often a lattice with a smallest element, ⊥, and greatest element, . ⊥ is the initial value of s i except for v 0 whose initial value is , that is, the more inaccurate value taking into account any possible state before the program execution. Algorithm 2 just ensures that the computation converges to a fixpoint, that is, the maximum of all possible values. This property is ensured by the existence of the lattice and the monotonicity property of any function handling the state.

This computation requires two analysis-specific functions. update(v, s) emulates the effect of a basic block v on a state s while join(s 1 , s 2 , ...) allows to combine different states coming from different paths. The semantic instructions are only used in the update(v, s 0 ) function. For each machine instruction, the block of semantic instructions B is interpreted according to Algorithm 3. The different execution paths are supported with a working list wl containing pairs composed of the index of the current instruction and the current state. update I implements the computation effect on a state as shown in Table 1. Different execution paths are created when a if instruction is found: two pairs are pushed in wl for each possibility. When all execution paths have been computed, the resulting states are joined in s r . As one may observe from Algorithm 3, the semantic instruction analysis is simple and straight-forward and re-uses directly the operators defined by the AI.

Proof of Concept: CLP analysis

For experimentation purpose, the semantic language has been used to implement a Circular-Linear Progression (clp) analysis [START_REF] Rathijit | Wcet estimation for executables in the presence of data caches[END_REF]. To push our semantics model even further, an analysis of conditions has been 0developed and applied to the clp to tighten the precision.

Circular-Linear Progression Analysis

The clp is an abstraction of integer values represented by a tuple (l, δ, m) denoting the set

{n ∈ Z s.t. n = l + δi ∧ 0 ≤ i ≤ m}, where l ∈ Z(n), (δ, m) ∈ N(n) 2
. l is the base of the set, δ the increment, and m the count of increments on l to get the last point l

+ n δ × m.
The addition is performed on n bits (modulo 2 n ), inducing a circularity on clp and mimics the integer behaviour on the real hardware. The abstraction of a value k is easily obtained by the singleton (k, 0, 0). while the top element (a clp that contains all possible values) is (l, 1, 2 n -1).

Performing clp analysis on the machine code requires to abstract the semantics instructions on the clp domain. For sake of brievity, only the add is given below but details on other operations can be found in [START_REF] Rathijit | Wcet estimation for executables in the presence of data caches[END_REF]:

{l 1 } + {l 2 } = (l 1 + n l 2 , 0, 0) (l 1 , δ 1 , m 1 ) + (l 2 , δ 2 , m 2 ) = (l 1 + n l 2 , g, m 1 δ1 g + m 2 δ2
g ) where g = gcd(δ 1 , δ 2 ). The clp allows to define the abstract states of the machine as a map from registers R and memory addresses A to clp values, that is, S : (R ∪ A) → clp. AI operators are now defined by U S : V × S → S (update) and J S : S × S → S (join). J S is naturally derived from the join function on the clp , applied on the values assigned to registers and addresses.

The update function, U S , is implemented as presented in the previous section. The abstract state S is applied to each machine instruction and, therefore, to each execution path of the semantics instructions. clp values of the registers and of the memory are read or written by getting or setting them in the machine abstract state S.

Widening Function

To converge faster to a fixpoint, a widening function, ∇ : S × S → S, is useful. The example in Listing 2, a simple loop computing the sum of the elements of an array, allows to illustrate this. Listing 3 shows the translation of machine code of the loop header into semantic instructions.

At the first iteration of the loop, p 0 = @t, @t being the actual address of array t in memory. At the second iteration of the loop, p 1 = p 0 + 4 = @t + 4. The widening ∇ is applied to these two clp: (@t, 0, 0)∇(@t + 4, 0, 0) = (@t, 4, 2 n /4 -1). The resulting clp is sound (it contains all possible values) and fast to obtain, but not very precise: next paragraph help to fix this. int t [10]; int *p , int * q ; int s = 0; q = t ; p = q ; while ( p -10 <= q ) { s += * p ; p ++; } Listing 2 Example of a simple C loop.

; r0 = 0 x7fc4 ( variable q ) seti t2 ,0 x10 add t1 , r31 , t2

; t1 = 0 x7fc0 load r9 , t1 ,0 x4 ; r9 is p seti t1 , -0 x28 add r9 , r9 , t1

; r9 <-r9 -40 cmp r71 , r9 , r0 if gt , r71 ,0 x1 cont seti t1 ,0 x9c branch t1

Listing 3 Translated Loop header.

Condition Filtering

In the example of Listing 2, we get the state p = (@t, 4, 2 n /4 -1), and a condition equivalent to p -40 > q (10 × sizeof (int) for a 32-bit machine). The edge remaining in the loop, taken if the condition is false, should provide as input state p = (@t, 4, 2 n-2 -1) filtered by p -40 ≤ q (inversed condition), i.e. p = (@t, 4, 10). This would give an accurate state for the values inside the loop if we are able to build such a filter.

Unlike a condition written in a high-level programming language, the machine code does not provide a well-identified single expression for the loop condition. Instead, we must rebuild the link between variables (either registers or values in the memory) involved in the condition. In addition, one may remark that the same variable can be stored in many places, as registers or memory locations at the same time during the execution. Therefore, building the condition only on the register used in the comparison would make our approach very ineffective because it would ignore the aliasing existing between registers and memory. This is illustrated in Listing 3: the variable p is stored at the memory address 0x7fc0, then loaded in r9. r9 is used again to carry out the result of p -40. So the condition analysis must return two filters: @0x7fc0 > q + 40 and r9 > q.

The algorithm proposed here tries to cope with both issues: the backward traversal of the semantics execution paths allows to collect the conditions of the if semantic instruction and to build back the aliases existing between registers and memories. Applied to the branch instruction of the loop header, the execution paths are sorted in two categories: the branching paths ending with a branch instruction and the continuing paths. The execution paths are then extended with other instructions of the loop header to completely form the computed condition. Each category applies a filter to the output state s of the loop header edge it matches (taken for the branch set, untaken for continuing set). As a category may contain several paths, the filters are applied on s separately and the result is joined by J S .

Taking a path p (either branching or not), the filters are built by recording the condition induced by the if instructions and by rewritting the conditions when a computation instruction is found. To represent a condition, we use a simple parenthesed tree-based language where nodes are either constants c, registers r, memory places @a or binary operators ω(e 1 , e 2 ) where ω ∈ {add, sub, ..., eq, ne, lt, ...}. As shown in Algorithm 4, the rewritting is performed backward (denoted by p -1 ) from an empty set of conditions. set and load instructions are considered as creating an alias with their destination register and the filter is duplicated to generate condition for both places. The expression f [x/y] means that the register x is replaced all over the filter f by y. Notice that, if a register computation is not involved in the condition building, the replacement have no effect on the filter f .

Algorithm 4 Building symbolic expressions

f ← {} for all sj ∈ p -1 do f ← f ilter[sj]f end for
With f ilter defined by:

f ilter[if(r, c, _)]f = f ∧ c(r, r) f ilter[cmp(c, a, b)]f = f [a/r][b/r] f ilter[set(c, a)]f = f ∧ f [a/c] f ilter[load(c, a, _)]f = f ∧ f [@a/c] f ilter[ω(c, a, b)]f = f [ω(a, b)/c] (1)
The application of the obtained filter f to an abstract state S is quite forward on a state s. For each clp value stored in s whose reference, register or memory, is i, each reference i ∈ f , i = i, is replaced by its values in s, f [s[i ]/i ] that allows, after simplification, to get a condition of the form ω(i, c) where ω ∈ {ne, eq, lt, le, gt, ge} and c ∈ clp. According to the actual operator ω, a clp c ω is obtained and intersected with the value of i: s[i] ∩ c ω . For example, in Listing 3, the continuing path gives the filter le(sub(r 9 , 0x28), r0). Replacing the values of r 31 and r0 by the matching clp in s and simplifying gets le(r 9 , 0x7F C4 + 0x28 and refines the value of r 9 by s[r 9 ] ∩ (-2 31 , 1, 2 31 + 0x7F C4 + 0x28) = (0x7F C4, 4, 10).

The application of the clp to our semantic instructions has shown that (1) it is feasible to support such type of static analysis, and (2) there are different ways to use the semantic instructions as in condition filtering. We can hope that the semantic instruction is a valuable abstraction of the machine code instructions. In the next section, we try to evaluate the performances of this representation.

Experimentation

The value analysis presented in this paper has been implemented in the OTAWA framework [3] using its own internal AI engine. The evaluation has been performed with a 3-GHz, 2GB memory Linux machine on the classic Mälardalen benchmark [1] that contains a collection of programs covering different embedded real-time domains .

Analysis Precision

This first evaluation criterium concerns the precision of the performed analysis. We are not able to estimate the actual precision of the obtained measurements in terms of difference between the real values and the analyzed ones: (a) we have no other analysis that can be taken as a reference and (b) it is impossible to have precise values as soon as a program is using external inputs. The more visible trace of imprecision is the apparition of values in the computation. Yet, it is hard to qualify the actual source of this imprecision as being naturally produced by the AI or an outcome of the intrinsic inefficiency of our analysis. In turn, the last issue may be decomposed in two causes: the lack of expressivity of semantics instructions or the limits of the abstraction of the clp analysis. Whatever, the last three columns of Figure 2 show the number of non-values obtained for different items: each column represents the ratio of non-values on the total of values of the measured items, the bigger is the better. The values column displays the number of set values generated by set and store semantic instructions with an average of 42.30% of nonvalues. In the absolute, the result is a bit disappointing but (1) to our knowledge, no such statistics have been published to compare with and (2) the large variation between benches (from 2.47% to 99.98%) shows that the effectiveness has a big dependency on the type of However, our analysis works better with address computation (74% on a mean, column addrs) and condition filtering (68% on a mean, column filters). The Addresses column evaluates the non-addresses used in load and store instructions while the filters column evaluates the number of non-filtered conditions. The obtained results are not perfect but they meet the needs of accuracy required by subsequent analyses like data cache, control flow analysis, infeasible path, etc. As for set values, the worst results are obtained on benchmarks using unsupported operations of the semantic language.

Computation Time

The six first columns of Table 2 show runtime performances of the analysis. We call static estimation the performance evaluation based on the count of instructions found as-is in the program once loaded in memory. On the opposite, dynamic instructions are counted during the AI. Both estimations are different because a single instruction may be interpreted several times before reaching a fixpoint: this is particularly the case of instructions contained in loops. The left column displays the experimented program, the next one the analysis time in µs (user time mean after 1000 iterations). The following two columns show the rate in machine and in semantic instructions, for dynamic estimation and the last two columns are the same for static.

The static estimation gives an insight of the capacity of the analysis to face to a raw program. For example, the average of about 139000 instructions / s states that we can process quickly (in less than 1 second) a program of nearly 512KB of code for a PowerPC architecture or any pure 32-bit RISC architecture.

On the other hand, the dynamic performances give a more straight-forward estimation of the real rate of the analysis, 242,594 machine instructions/s and 539,705 semantic instructions/s, taking into account the structure of the Hopefully, both measures are quite good although there is a lot of variability according to the benchmarks. Such performances let place for improving analysis without being blocked by intractable computation time.

Comparison with Existing Work

A lot of work on value analysis has been done for different purposes. The foundation of abstract AI was motivated by the interval analysis [l, u] of each variable on Pascal-like languages [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. In addition to the domain, the performed analysis is also different because of the widening operation. To speed up the convergence to the fixpoint, widening and narrowing operators are applied, that requires several passes of analysis and increases the computation time. To our knowledge, although there is very few documentation on this [START_REF] Ferdinand | Static Memory and Timing Analysis of Embedded Systems Code[END_REF], the tool ait [2] is also using such an analysis to exhibit register values at program points but is applied to machine language. Yet, the interval of values [l, u] does not fit well with address representation. They include too many false values while the addresses are usually aligned to a multiple of data sizes and cause the union of too many false data and reduce the precision. Ermedhal et al in [START_REF] Ermedahl | Loop Bound Analysis based on a Combination of Program Slicing, Abstract Interpretation and Invariant Analysis[END_REF] improve this using a modulo analysis to identify more precisely values inside an interval. Yet, their domain is more complex than ours, ([l,u],(i,c)) that identifies the set of values matching [l, u] ∩ {i + n × c, n ∈ Z}. Moreover, this domain makes the analysis more costly in computation time.

S. Rathijit [START_REF] Rathijit | Executable analysis using abstract interpretation with circular linear progressions[END_REF][9] simplifies a lot this representation using only three integers, (l, u, δ). i, the argument of Ermedhal's representation is easily replaced by finding the lowest value of the set to get a more precise l. Then, we have improved Rathijit's work to have canonical representation of these values. Indeed several representations for a same set exist because u -l is not required to be a multiple of δ. Our triplet (a, δ, n) ensures the uniqueness of the representation as it forces u = a + n × δ. This property makes easier some operations of the value arithmetics like equality tests. In addition, unlike Rathijit that seems to support only ARM, our machine code abstraction, avoids to tie our analysis to a specific machine instruction set and we are using the conditions to accelerate convergence of fixpoint of the analysis and improve the precision in presence of selections.

In the domain of semantics languages, ALF [START_REF] Gustafsson | ALF -A Language for WCET Flow Analysis[END_REF] is supported by several compilation and WCET tools. It allows to represent completely a program while our language is just an overlay on the CFG. More comprehensive and more expressive than our semantics instructions, it seems to be more memory-and time-consuming for analyses. Architecture Description Languages like SimNML, Lisa, etc are also good candidate to express semantics of machine code. But we think that their granularity would make the analyses too costly and some concepts are too hard to extract: for example, in a microprocessor, the comparison result is represented as a set of bits obtained by a combination of operand bits whose usage in analysis is not straight-forward.

Conclusion

The contribution of our paper is twofold. First, we propose a language to abstract usual machine code semantic and show how it may be involved in abstract AI. The overall outcome is that the analyses based on this language becomes portable on any microprocessor supported by our semantic language. For example, in the OTAWA framework, it has been already successfully used to describe several RISC instruction sets like PowerPC. We plan to quickly apply the semantics instructions to Sparc, TriCore and possibly to the x86 instruction set. Second, we have improved existing value analysis, based on clp domain, for speed of computation. The changes include a reformulation of the domain leading to canonical values and therefore simplification of operation abstraction. The second improvement concerns the use of conditions to speed up the convergence of fixpoint computation.

The resulting analysis rate is quite fast, which will be valuable in the future in order to fix medium precision results. We think that the precision problem is not inherent to the value analysis algorithm but, instead, to the limitation of the semantic language. So, we plan to extend it with bit-to-bit operations, integer multiplication and division as well as floating-point operations. The latter extension cannot be done in the frame of clp because the notion of modulo does not fit well with float value: we have to fall back to usual interval analysis. This means a state abstraction with heterogenous content.

Finally, we would like to exploit the results of this value analysis to extend the OTAWA framework. The semantic language has already been used in OTAWA to implement data cache analysis and stack analysis but we can exploit the value analysis results to improve control flow analyses like detection of infeasible paths, dynamically dead code, switch decoding, indirect pointer call analyzes. As the latter analysis does not fit well with clp, we have also to introduce set of addresses in our domain and it remains to identify which values should be clp and which ones should be sets. In a more generic way, we have to replace our naive implementation of state to improve our value representation to support heterogeneous data, to maintain fast computation and to waste as less memory as possible.

Table 1

 1 Semantic Instructions.

Instruction (I) Semantics (updateI )

Table 2

 2 Analysis Execution Time.

			Dynamic		Static		Value Precision
	Program	Time	mach	sem	mach	sem values	addrs	filters
		(µs)	(i/s)	(i/s)	(i/s)	(i/s)	(%)	(%)	(%)
	adpcm	31530	219600	495908	39861	204598	2.47	15.39	72.34
	bs	1190	103361	228571	97560	141176	53.85	89.09	33.33
	bsort100	2680	117537	269029	63492	110074	20.75	17.31	33.33
	cnt	2590	214285	462548	50450	188030	36.17	46.51 100.00
	compress	25610	85591	196134	48813	88481	8.68	27.42	49.30
	cover	50040	59492	159852	156533	81434	8.66	52.94 100.00
	crc	5160	230232	446511	47979	207751	10.04	79.25	86.52
	duff	1100	97272	233636	271028	441818	38.46	58.70	60.87
	expint	3290	115805	272644	70866	132218	47.37	71.43	80.00
	fac	30 1400000 3233333 1000000 4533333	77.78	95.00 100.00
	fdct	1330	958646 2051127	8627 1057142	20.98	99.42 100.00
	fft1	42220	247418	485243	17231	87162	24.77	61.90	16.03
	fibcall	910	98901	252747	100000	142857	74.19 100.00 100.00
	fir	3330	104504	268168	45977	97897	34.48	90.50	16.00
	insertsort	1070	241121	481308	34883	202803	47.37	72.22	33.33
	janne_c	2360	72457	188559	93567	74576	59.52	87.21	77.78
	jfdctint	1940	718556 1690721	10043	598453	6.72	91.57 100.00
	lcdnum	4040	73267	177970	162162	92574	30.99	50.45 100.00
	lms	14590	202604	385263	33491	125222	49.47	91.25	81.94
	ludcmp	12660	138151	280489	29731	77725	33.16	82.85	29.65
	matmult	4140	238647	503864	38461	145893	23.33	29.44 100.00
	minver	16320	145220	306250	32911	87438	13.49	67.93	29.00
	ndes	27550	167622	369546	33347	111724	52.28	74.46	74.39
	nsichneu	205180	98450	209182	37425	104664	11.98	89.68	29.80
	ns	8060	99503	206203	24937	29528	83.58	89.40	61.29
	prime	2500	162800	362000	100737	237200	70.75 100.00	50.00
	qsort-exam	5860	139761	289419	41514	150170	13.46	63.50	16.85
	qurt	6320	154113	305537	61601	233386	44.81 100.00 100.00
	recursion	30	800000 2033333 1714285 4066666	69.23 100.00 100.00
	select	5150	136893	283300	51063	149708	19.75	66.42	36.17
	sqrt	1610	91304	182608	74829	88198	50.00 100.00 100.00
	statemate	48770	157227	307709	40688	109883	3.81	90.85	89.02
	st	7680	213411	430989	58572	245833	10.12	19.33 100.00
	ud	7630	144429	300262	37205	114285	33.59	81.25	26.72
	average		242593	539705	139114	428232	34.88	72.14	67.17
	the program. Some benchmarks like crc or adpcm give particularly bad results because they
	are performing a lot of operations unsupported by our semantics instructions, respectively,
	bit-to-bit and floating-point operations.

The research leading to these results has received funding from ANR under grant ANR-12-INSE-0001.


Eugénie Poulon

ABOUT THE POSSIBILITY OF MINIMAL BLOW UP FOR NAVIER-STOKES SOLUTIONS WITH DATA IN Ḣs (IR 3 )

Keywords: incompressible Navier-Stokes equations, blow up, profile decomposition, critical solution. 1

About the possibility of minimal blow up for

Navier-Stokes solutions with data in Ḣs (R 3 ) Eugénie Poulon

Introduction and statement of main result

We consider the Navier-Stokes system for incompressible viscous fluids evolving in the whole space IR 3 . Denoting by u the velocity, a vector field in IR 3 , by p in IR the pressure function, the Cauchy problem for the homogeneous incompressible Navier-Stokes system is given by ( 1)

   ∂ t u + u • ∇u -∆u = -∇p div u = 0 u |t=0 = u 0 .
We recall a crucial property of the Navier-Stokes equation : the scaling invariance. Let us define the operator

∀α ∈ IR + , ∀λ ∈ IR + * , ∀x 0 ∈ IR 3 , Λ α λ,x 0 u(t, x) def = 1 λ α u t λ 2 , x -x 0 λ .
If α = 1, we note Λ 1 λ,x 0 = Λ λ,x 0 .

(2)

Clearly, if u is smooth solution of Navier-Stokes system on [0, T ] × IR 3 with pressure p associated with the initial data u 0 , then, for any positive λ, the vector field and the pressure u λ def = Λ λ,x 0 u and p λ def = Λ 2 λ,x 0 p is a solution of Navier-Stokes system on the interval [0, λ 2 T ] × IR 3 , associated with the initial data u 0,λ = Λ λ,x 0 u 0 . This leads to the definition of scaling invariant space. Definition 1.1. A Banach space X is said to be scaling invariant (or also critical), if its norm is invariant under the scaling transformation defined by u → u λ

||u λ || X = ||u|| X .
Let us give some exemples of critical spaces in dimension 3

Ḣ 1 2 (IR 3 ) ֒→ L 3 (IR 3 ) ֒→ Ḃ-1+ 3 p p,∞ (IR 3 ) p<∞ ֒→ BMO -1 (IR 3 ) ֒→ Ḃ-1 ∞,∞ (IR 3
). The framework of this work is functional spaces which are above the natural scaling of Navier-Stokes equations. More precisely, our statements will take place in some Sobolev and Besov spaces, with a regularity index s such that

1 2 < s < 3 2 •
Notations. We shall constantly be using the following simplified notations:

L ∞ T ( Ḣs ) def = L ∞ ([0, T ], Ḣs ) and L 2 T ( Ḣs+1 ) def = L 2 ([0, T ], Ḣs+1 ),
and the relevant function space we shall be working with in the sequel is

X s T def = L ∞ T ( Ḣs ) ∩ L 2
T ( Ḣs+1 ), endowed with the norm u 2

X s T def = u 2 L ∞ T ( Ḣs ) + u 2 L 2 T ( Ḣs+1 ) .
Let us start by recalling the local existence theorem for data in the Sobolev space Ḣs .

Theorem 1.1. Let u 0 be in Ḣs , with 1 2 < s < 3 2

• Then there exists a time T and there exists a unique solution N S(u 0 ) such that N S(u 0 ) belongs to L ∞ T ( Ḣs ) ∩ L 2 T ( Ḣs+1 ). Moreover, denoting by T * (u 0 ) the maximal time of existence of such a solution, there exists a positive constant c such that

(3) T * (u 0 ) u 0 σs Ḣs c, with σ s def = 1 1 2 (s -1 2 ) • Remark 1.1.
Throughout this paper, we will adopt the useful notation N S(u 0 ) to mean the maximal solution of the Navier-Stokes system, associated with the initial data u 0 . Notice that our whole work relies on the hypothesis there exists some blowing up N S-solutions, e.g some N S-solutions with a finite lifespan T * (u 0 ). This is still an open question.

Remark 1.2. We point out that the infimum of the quantity T * (u 0 ) u 0 σs Ḣs exists and is positive (because of the constant c). It has been proved in [START_REF] Poulon | About the behaviour of regular Navier-Stokes solutions near the blow up[END_REF] that there exists some intial data which reach this infimum and that the set of such data is compact, up to dilations and translations. N S(u 0 )(t) σs Ḣs = +∞.

Our motivation here is to wonder if there exist some Navier-Stokes solutions which stop living in finite time (e.g T * (u 0 ) < ∞) and which blows up at a minimal rate, namely: there exists a positive constant M such that (T * (u 0 )t) N S(u 0 ) σs Ḣs M . In others terms, Question: Does there exist some blowing up N S-solutions such that (T * (u 0 )t) N S(u 0 ) σs

Ḣs

M ? If yes, what do they look like ?

We assume an affirmative answer and we search to characterize such solutions.

Hypothesis H: There exist some blowing up N S-solutions such that (T * (u 0 )t) N S(u 0 ) σs

Ḣs

M .

Notice that a very close question to this one is to prove that If T * (u 0 ) < ∞, does lim sup t→T * (u 0 ) (T * (u 0 )t) N S(u 0 )(t) σs Ḣs = +∞ ?

We underline that this question about blowing-up Navier-Stokes solutions has been highly developed in the context of critical spaces, namely Ḣ 1 2 (IR 3 ) and L 3 (IR 3 ). Indeed, L. Escauriaza, G. Seregin and V. Sverák showed in the fundamental work [START_REF] Escauriaza | L3,∞-solutions of Navier-Stokes equations and backward uniqueness[END_REF] that any "Leray-Hopf" weak solution which remains bounded in L 3 (IR 3 ) can not develop a singularity in finite time. Alternatively, it means that [START_REF] Bahouri | Lack of compactness in the 2D critical Sobolev embedding, the general case[END_REF] If T * (u 0 ) < +∞, then lim sup t→T * (u 0 )

N S(u 0 )(t) L 3 = +∞.

I. Gallagher, G. Koch and F. Planchon revisited the above criteria in the context of mild Navier-Stokes solutions. They proved in [START_REF] Gallagher | A profile decomposition approach to the L ∞ t (L 3 x ) Navier-Stokes regularity criterion, to appear[END_REF] that strong solutions which remain bounded in L 3 (IR 3 ), do not become singular in finite time. To perform it, they develop an alternative viewpoint : the method of "critical elements" (or "concentration-compactness"), which was introduced by C. Kenig and F. Merle to treat critical dispersive equations. Recently, same authors extend the method in [START_REF] Gallagher | Blow-up of critical Besov norms at a Navier-Stokes singularity[END_REF] to prove the same result in the case of the critical Besov space Ḃ-1+ 3 p p,q (IR 3 ), with 3 < p, q < ∞. Notice the work of J.-Y.Chemin and F. Planchon in [START_REF] Chemin | Self-improving bounds for the Navier-Stokes equations[END_REF], who gives the same answer in the case of the Besov space Ḃ-1+ 3 p p,q (IR 3 ), with 3 < p < ∞, q < 3 and with an additional regularity assumption on the data. To conclude the nonexhaustive list of blow up results, we mention the work of C. Kenig and G. Koch who carried out in [START_REF] Kenig | An alternative approach to the Navier-Stokes equations in critical spaces[END_REF] such a program of critical elements for solutions in the simpler case Ḣ 1 2 (IR 3 ). More precisely, they proved for any data u 0 belonging to the smaller critical space

Ḣ 1 2 (IR 3 ), (6) If T * (u 0 ) < +∞, then lim t→T * (u 0 ) N S(u 0 )(t) Ḣ 1 2 = +∞.
In our case (remind : we consider Sobolev spaces Ḣs (IR

M σs c = sup A > 0, sup t<T * (u 0 ) (T * (u 0 ) -t) N S(u 0 ) σs Ḣs A ⇒ T * (u 0 ) = +∞ .
But unfortunately, such a point of view makes no sense, owing to the meaning of (T * (u 0 )t) when T * (u 0 ) = +∞. We have to proceed in an other way and it may be removed by defining a new object

M σs c M σs c def = inf u 0 ∈ Ḣs T * (u 0 )<∞ lim sup t→T * (u 0 ) (T * (u 0 ) -t) N S(u 0 )(t) σs Ḣs .
Clearly, (4) implies that M σs c exists and is positive. As we have decided to work under hypothesis H, a fortiori, this implies that M σs c is finite. The definition below is the key notion of critical solution in this context.

Definition 1.2. (Sup-critical solution)

Let u 0 be an element in Ḣs . We say that u = N S(u 0 ) is a sup-critical solution if N S(u 0 ) satisfies the two following assumptions:

T * (u 0 ) < ∞ and lim sup t→T * (u 0 ) (T * (u 0 ) -t) N S(u 0 )(t) σs Ḣs = M σs c .
A natural question is to know if such elements exist. The statement given below gives an affirmative answer and provides a general procedure to build some sup-critical solutions. Our main result follows.

Theorem 1.2. (Key Theorem)

Let us assume that there exists u 0 in Ḣs and M in IR + * such that T * (u 0 ) < ∞ and (T * (u 0 )t) N S(u 0 )(t) σs

Ḣs

M.

Then, there exists

Φ 0 ∈ Ḣs ∩ Ḃ 1 2 2,∞ such that Φ def = N S(Φ 0 ) is a sup-critical solution, blowing up at time 1, such that (7) sup τ <1 (1 -τ ) N S(Φ 0 )(τ ) σs Ḣs = lim sup τ →1 (1 -τ ) N S(Φ 0 )(τ ) σs Ḣs = M σs c .
In addition, there exists a positive constant C such that [START_REF] Chemin | Remarques sur l'existence globale pour le systéme de Navier-Stokes incompressible[END_REF] and for any τ < 1, N S(Φ 0 )(τ )

Ḃ 1 2 2,∞ C,
where the Besov norm (for regularity index 0 < α < 1) is defined by

u Ḃα 2,∞ def = sup x∈IR d u(• -x) -u L 2 |x| α •
We postpone the proof of (7) of the Key Theorem 1.2 to the next section. The proof of (8) will be given in Section 5. We stress on the fact that ( 8) is somewhat close to a question raised by the paper of I. Gallagher, G. Koch and F. Planchon [START_REF] Gallagher | Blow-up of critical Besov norms at a Navier-Stokes singularity[END_REF], in which they prove that for any initial data in the critical Besov space Ḃ-1+ 3 p p,q , with 3 < p, q < ∞, the N S-solution, (the lifespan of which is assumed finite) becomes unbounded at the blow-up time. Let us say a few words about the limit case Ḃ-1+ 3 p p,∞ . We may wonder if the result holds in the limit case q = ∞. As far as the author is aware, the answer is still open. Actually, if it holds, a fortiori it holds in the smaller space

Ḃ 1 2 2,∞ , by vertue of the embedding Ḃ 1 2 2,∞ ֒→ Ḃ-1+ 3 p p,∞ .
In others terms, it would mean there is no blowing-up solution, bounded in the critical space Ḃ 1 2 2,∞ . This is related to the concern of our paper since we build some blowing-up solutions bounded in this critical space, under the assumption of blow up at minimal rate. We mention the very interesting work of H. Jia and V. Sverák [START_REF] Jia | Local-in-space estimates near initial time for weak solutions of the Navier-Stokes equations and forward self-similar solutions[END_REF], where they prove that -1-homogeneous initial data generate global -1-homogeneous solutions. Unfortunately, the uniqueness of such solutions is not guaranteed.

Existence of sup-critical solutions

The goal of this section is to give a partial proof of Key Theorem 1.2. It relies on the two Lemmas below.

Lemma 2.1. (Existence of sup-critical solutions in Ḣs ) Let (v 0,n ) n∈IN be a bounded sequence in Ḣs such that [START_REF] Chemin | Théorèmes d'unicité pour le système de Navier-Stokes tridimensionnel[END_REF] τ * (v 0,n ) = 1 and for any τ < 1, (1τ ) N S(v 0,n )(τ, • ) σs

Ḣs

M σs c + ε n , where ε n is a generic sequence which tends to 0 when n goes to +∞.

Then, there exists Ψ 0 in Ḣs such that Ψ def = N S(Ψ 0 ) is a sup-critical solution blowing up at time 1 and satisfies [START_REF] Chemin | Large, global solutions to the Navier-Stokes equations, slowly varying in one direction[END_REF] sup

τ <1 (1 -τ ) N S(Ψ 0 )(τ ) σs Ḣs = lim sup τ →1 (1 -τ ) N S(Ψ 0 )(τ ) σs Ḣs = M σs c .
Moreover, the initial data of such element is a weak limit of the sequence (v 0,n ) translated, e.g

(11) ∃ (x 0,n ) n 0 , v 0,n (• +x 0,n ) ⇀ n→+∞ Ψ 0 .
The proof of Lemma 2.1 will be the purpose of Section 4. It relies essentially on scaling argument and profile theory, which will be introduced in the next Section 3.

Lemma 2.2. (Fluctuation estimates)

Let u = N S(u 0 ) be a NS-solution associated with a data u 0 ∈ Ḣs , with

1 2 < s < 3 2 , such that (T * (u 0 ) -t) 1 σs N S(u 0 )(t) Ḣs M.
Then, the following estimates on the fluctuation part B(u, u)(t)

def = u -e t ∆ u 0 yield (12) for any s < s ′ < 2s - 1 2 , (T * (u 0 ) -t) 1 σ s ′ B(u, u)(t) Ḣs ′ F s ′ (M 2 )
Moreover, for the critical case = 1 2 , we have

(13) B(u, u)(t) Ḃ 1 2 2,∞ C M 2 .
The proof of this lemma is postpone to Section 8. It merely stems from product laws in Besov spaces, interpolation inequalities and from judicious splitting into low and high frequencies in the following sense (T *t)2 2j 1 and (T *t)2 2j 1.

Remark 2.1. Let us point out that estimates of Lemma 2.2 do not hold if 0 < α < 1 2 , owing to low frequencies. Indeed, arguments similar to the ones used in the proof of Lemma 2.2 lead only to the following estimate

B(u, u)(t) Ḃα 2,∞ C M 2 T * (u 0 ) 1 2 (α-1 2 ) .

Partial proof of Key Theorem 1.2

In all this text, we denote by (ε n ) a non increasing sequence, which tends to 0, when n tend to +∞.

• Step 1 : Existence of sup-critical elements in Ḣs , with

1 2 < s < 3 2 •
Let us consider the sequence (M c + ε n ) n 0 . By definition of M c , there exists a sequence (u 0,n ) belonging to Ḣs , with a finite lifespan T * (u 0,n ), such that for any t < T * (u 0,n ) :

lim sup t→T * (u 0 ) (T * (u 0,n ) -t) N S(u 0,n ) σs Ḣs M σs c + ε n .
By definition of lim sup, there exists a nondecreasing sequence of time t n , converging to T * (u 0 ), such that

(14) ∀t t n , (T * (u 0,n ) -t) N S(u 0,n )(t, x) σs Ḣs M σs c + ε n .
By rescaling, we consider the sequence

v 0,n (y) = T * (u 0,n ) -t n 1 2 N S(u 0,n ) t n , (T * (u 0,n ) -t n 1 2 y .
and we have

v 0,n σs Ḣs = T * (u 0,n ) -t n N S(u 0,n )(t n ) σs Ḣs . ( 15
)
By vertue of ( 14), the sequence (v 0,n ) n 1 is bounded by M σs c + ε 0 in the space Ḣs . Moreover, such a sequence generates a Navier-Stokes solution, which keeps on living until the time τ * = 1 and satisfies

N S(v 0,n )(τ, y) = T * (u 0,n ) -t n 1 2 N S(u 0,n ) t n + τ T * (u 0,n ) -t n , T * (u 0,n ) -t n 1 2 y . (16)
We introduce t n = t n + τ T * (u 0,n )t n . Notice that, because of scaling, an easy computation yields [START_REF] Gallagher | Blow-up of critical Besov norms at a Navier-Stokes singularity[END_REF] (

1 -τ ) N S(v 0,n )(τ ) σs Ḣs = T * (u 0,n ) -t n N S(u 0,n ) t n σs Ḣs .
As t n t n for any n (by definition of t n ) we combine [START_REF] Gallagher | Blow-up of critical Besov norms at a Navier-Stokes singularity[END_REF] with ( 14) and we get, for any τ

∈ [0, 1[, (1 -τ ) N S(v 0,n )(τ, x) σs Ḣs M σs c + ε n .
The sequence (v 0,n ) satisfies the hypothesis of Lemma 2.1. Applying it, we build a sup-critical solution Φ = N S(Ψ 0 ) in Ḣs which blows up at time 1, e.g

lim sup τ →1 (1 -τ ) N S(Ψ 0 )(τ ) σs Ḣs = M σs c .
This proves the first part of the statement of Theorem 1.2.

• 2,∞ and obviously we have

N S(Ψ 0 )(t) Ḃ 1 2 2,∞ N S(Ψ 0 )(t) -e t∆ Ψ 0 Ḃ 1 2 2,∞ + e t∆ Ψ 0 Ḃ 1 2 2,∞
.

The paper is structured as follows. In Section 3, we recall the main tools of this paper. Essentially, it deals with the profile theory of P. Gérard [START_REF] Gérard | Description du défaut de compacité de l'injection de Sobolev[END_REF] and a structure lemma concerning a N S-solution associated with a sequence which satisfies hypothesis of profile theory. We also recall some basics facts on Besov spaces.

In Section 4, we are going to establish the proof of crucial Lemma 2.1, which provides the proof of the first part of Theorem 1.2 : there exists some sup-critical elements in Ḣs . The second part of the proof is postponed in Section 6, where we build some sup-critical elements not only in Ḣs , but also in others spaces, such as

Ḃ 1 2 2,∞ and Ḃs ′ 2,∞ , with s < s ′ < 2s - 1 2
• To carry out this, we need some estimates on the fluctuation part of the solution, which will be provided in Section 5. Then in Section 7, we give an analogue sup-inf critical criteria. It turns out that among sup-critical solutions, there exists some of them which are sup-inf-critical in the sense of they reach the biggest infimum limit. Section 8 is devoted to the proof of Lemma 3.2, which gives the structure of a Navier-Stokes solution associated with a bounded sequence of data in Ḣs . We recall to the reader that such structure result has been partially proved in [START_REF] Poulon | About the behaviour of regular Navier-Stokes solutions near the blow up[END_REF], except for the orthogonality property of Navier-Stokes solution in Ḣs -norm. As a result, we give the proof of such a property, after reminding the ideas of the complete proof.

Profile theory and Tool Box

We recall the fundamental result due to P. Gérard : the profile decomposition of a bounded sequence in the Sobolev space Ḣs . The original motivation of this theory was the desciption, up to extractions, of the defect of compactness in Sobolev embeddings (see for instance the pionneering works of P.-L. Lions in [START_REF] Lions | The concentration-compactness principle in the calculus of variations. The limit case I[END_REF], [START_REF] Lions | The concentration-compactness principle in the calculus of variations. The limit case II[END_REF] and H. Brezis, J.-M. Coron in [START_REF] Brézis | Convergence of solutions of H-Systems or how to blow bubbles[END_REF]. Here, we will use the theorem of P. Gérard [START_REF] Gérard | Description du défaut de compacité de l'injection de Sobolev[END_REF], which gives, up to extractions, the structure of a bounded sequence of Ḣs , with s between 0 and 3 2 •

More precisely, the defect of compactness in the critical Sobolev embedding Ḣs ⊂ L p is described in terms of a sum of rescaled and translated orthogonal profiles, up to a small term in L p . For more details about the history of the profile theory, we refer the reader to the paper [START_REF] Poulon | About the behaviour of regular Navier-Stokes solutions near the blow up[END_REF].

Theorem 3.1. (Profile Theorem [START_REF] Gérard | Description du défaut de compacité de l'injection de Sobolev[END_REF])

Let (u 0,n ) n∈IN be a bounded sequence in Ḣs . Then,

up to an extraction:

-There exists a sequence vectors fields, called profiles (ϕ j ) j∈IN in Ḣs .

-There exists a sequence of scales and cores (λ n,j , x n,j ) n,j∈IN , such that, up to an extraction

∀J 0, u 0,n (x) = J j=0 Λ 3 p λ n,j ,x n,j ϕ j (x) + ψ J n (x) with lim J→+∞ lim sup n→+∞ ψ J n L p = 0, and p = 6 3 -2s •
Where, (λ n,j , x n,j ) n∈IN,j∈IN * are sequences of (IR * + × IR 3 ) IN with the following orthogonality property: for every integers (j, k) such that j = k, we have

either lim n→+∞ λ n,j λ n,k + λ n,k λ n,j = +∞ or λ n,j = λ n,k and lim n→+∞ |x n,j -x n,k | λ n,j = +∞.
Moreover, for any J ∈ IN, we have the following orthogonality property

(18) u 0,n 2 Ḣs = J j=0 ϕ j 2 Ḣs + ψ J n 2 Ḣs + •(1), when n → +∞.
Let us recall a structure Lemma, based on the crucial profils theorem of P. Gérard (see [START_REF] Gérard | Description du défaut de compacité de l'injection de Sobolev[END_REF]). Let (u 0,n ) be a bounded sequence in the Sobolev space Ḣs , which profile decomposition is given by

u 0,n (x) = j∈J Λ 3 p λ n,j ,x n,j ϕ j (x) + ψ J n (x),
with the appropriate properties on the error term ψ J n . By vertue of orthogonality of scales and cores given by Theorem 3.1, we sort profiles according to their scales

u 0,n (x) = j∈J 1 j J ϕ j (x -x n,j ) + j∈J c 1 j J Λ 3 p λ n,j ,x n,j ϕ j (x) + ψ J n (x) (19)
where for any j ∈ J 1 , for any n ∈ IN, λ n,j ≡ 1. Under these notations, we claim we have the following structure Lemma of the Navier-Stokes solutions, which proof will be provided in Section 8.

Lemma 3.2. (Profile decomposition of a sequence of Navier-Stokes solutions)

Let (u 0,n ) n 0 be a bounded sequence of initial data in Ḣs which profile decomposition is given by

u 0,n (x) = J j=0 Λ 3 p λ n,j ,x n,j ϕ j (x) + ψ J n (x).
Then, lim inf

n 0 T * (u 0,n ) T def = inf j∈J 1
T * (ϕ j ) and for any t < T * (u 0,n ), we have

N S(u 0,n )(t, x) = j∈J 1 N S(ϕ j )(t, x -x n,j ) + e t∆ j∈J c 1 j J Λ 3 p λ n,j ,x n,j ϕ j (x) + ψ J n (x) + R J n (t, x) (20)
where the remaining term R J n satisfies for any T < T , lim

J→+∞ lim n→+∞ R J n X s T = 0.

Moreover, we have the orthogonality property on the Ḣs -norm for any

t < T N S(u 0,n )(t) 2 Ḣs = j∈J 1 N S(ϕ j )(t) 2 Ḣs + e t∆ j∈J c 1 j J Λ 3 p λ n,j ,x n,j ϕ j + ψ J n 2 Ḣs + γ J n (t). (21) with lim J→+∞ lim sup n→+∞ sup t ′ <t |γ J n (t ′ )| = 0.
For the convenience of the reader, we recall the usual definition of Besov spaces. We refer the reader to [START_REF] Bahouri | Fourier Analysis and Nonlinear Partial Differential Equations[END_REF], from page 63, for a detailed presentation of the theory and analysis of homogeneous Besov spaces.

Definition 3.1. Let s be in IR, (p, r) in [1, +∞] 2 and u in S ′ . A tempered distribution u is an element of the Besov space Ḃs p,r if u satifies lim j→∞ || Ṡj u|| L ∞ = 0 and u Ḃs p,r def = j∈Z 2 jrs || ∆j u|| r L p 1 r < ∞,
where ∆j is a frequencies localization operator (called Littlewood-Paley operator), defined by

∆j u(ξ) def = F -1 ϕ(2 -j |ξ|) u(ξ) , with ϕ ∈ D([ 1 2 , 2]), such that j∈Z ϕ(2 -j t) = 1, for any t > 0.
Remark 3.1. Notice that the characterization of Besov spaces with positive indices in terms of finite differences is equivalent to the above definition (cf [START_REF] Bahouri | Fourier Analysis and Nonlinear Partial Differential Equations[END_REF]). In the case where the regularity index is between 0 and 1, one has the following property. Let s be in ]0,

u Ḃθ s 1 +(1-θ) s 2 p,1 C(s 1 , s 2 , θ) u θ Ḃs 1 p,∞ u 1-θ Ḃs 2 p,∞ .

Application of profile theory to sup-critical solutions

This section is devoted to the proof of Lemma 2.1. The statement given below is actually a bit stronger and clearly entails Lemma 2.1. We shall prove the following proposition.

Ḣs

M σs c + ε n , where ε n is a generic sequence which tends to 0 when n goes to +∞. Then, up to extractions, we get the statements below • the profile decomposition of such a sequence of data has a unique profile ϕ j 0 with constant scale such that N S(ϕ j 0 ) is a sup-critical solution which blows up at time 1, e.g [START_REF] Lemarié-Rieusset | Recent Developments in the Navier-Stokes Problem[END_REF] lim sup τ →1

(1τ ) N S(ϕ j 0 )(τ ) σs Ḣs = M σs c .

• "The limsup is actually a sup"

(24) sup τ <1 (1 -τ ) N S(ϕ j 0 )(τ ) σs Ḣs = M σs c .
Proof. Let (v 0,n ) n 1 be a bounded sequence in Ḣs , satisfiying the assumptions of Proposition 4.1. Therefore, (v 0,n ) n 1 has the profile decomposition below

v 0,n (x) = j∈J 1 j J ϕ j (x -x n,j ) + j∈J c 1 j J Λ 3 p λ n,j ,x n,j ϕ j (x) + ψ J n (x). (25)
We denote by τ *

j 0 def = inf j∈J 1 T * (ϕ j ).
• Step 1 : we start by proving by a contradiction argument that τ * j 0 = 1.

We have already known by vertue of Lemma 3.2, that τ * j 0

1. Assuming that τ * j 0 < 1, we expect a contradiction. Moreover, orthogonal Estimate ( 21) can be bounded from below by

N S(v 0,n )(τ ) 2 Ḣs N S(ϕ j 0 )(τ ) 2 Ḣs -|γ J n (τ )|. (26)
On the one hand, it seems clear by assumption that for any τ < τ * j 0 , we have

(1 -τ * j 0 ) 2 σs (1 -τ ) 2 σs .
On the other hand, hypothesis on N S(v 0,n ) yields

(1 -τ ) 2 σs N S(v 0,n )(τ ) 2 Ḣs M 2 c + ε n .
Therefore, from the above remarks, we get

(27) N S(v 0,n )(τ ) 2 Ḣs M 2 c + ε n (1 -τ * j 0 )
2 σs

•

Combining the above estimate with (26), we finally get, after multiplication by the factor (τ

* j 0 -τ ) 2 σs , M 2 c + ε n (1 -τ * j 0 ) 2 σs (τ * j 0 -τ ) 2 σs (τ * j 0 -τ ) 2 σs N S(ϕ j 0 )(τ ) 2 Ḣs -(τ * j 0 -τ ) 2 σs |γ J n (τ )|. (28) Notice that (τ * j 0 -τ ) 2
σs is always less than 1, which allows us to get rid of it in front of the remaining term |γ J n (τ )|. In addition, applying (4) and hypothesis on the sequence ε n , one has

M 2 c + ε 0 (1 -τ * j 0 ) 2 σs (τ * j 0 -τ ) 2 σs c -|γ J n (τ )|.
We first choose τ = τ c such that τ c < τ * j 0 and

M 2 c + ε 0 (1 -τ * j 0 ) 2 σs (τ * j 0 -τ c ) 2 σs = c 4
• Then, we take J and n

large enough such that |γ J n (τ c )| c 2
• Therefore, we get a contradiction, which proves that τ * j 0 = 1. • Step 2 : we prove here that N S(ϕ j 0 ) is a sup-critical solution in Ḣs .

Let us come back to Inequality [START_REF] Meyer | Wavelets, paraproducts, and Navier-Stokes equations, Current developments in mathematics[END_REF], which we multiply by the factor (1τ ) 2 σs . As we have shown that τ * j 0 = 1, hypothesis on N S(v 0,n ) implies that for any τ < 1,

(29) M 2 c + ε n (1 -τ ) 2 σs N S(ϕ j 0 )(τ ) 2 Ḣs -|γ J n (τ )|.
Our aim is to prove that the particular profile ϕ j 0 generates a sup-critical solution. If not, it means that

∃α 0 > 0, ∀ε > 0, ∃τ ε , such that 0 < (1 -τ ε ) 2 σs < ε and (1 -τ ε ) 2 σs N S(u 0,n )(τ ε ) 2 Ḣs M 2
c + α 0 . Taking the above inequality at time τ ε , one has

M 2 c + ε n M 2 c + α 0 -|γ J n (τ ε )|. Moreover, assumption on the remaining term γ J n implies that ∀η > 0, ∃ J(η) ∈ IN, ∃N η ∈ IN such that ∀J J(η), ∀n N η , |γ J n (τ ε )| η. Let η > 0.
For any J J (η) and for any n N η , we get at time τ ε ,

M 2 c M 2 c + α 0 -η. Now, choosing η small enough (namely η = α 0 2
) we get a contradiction which proves that N S(ϕ j 0 ) is a sup-critical solution. This concludes the proof of step 2 and thus the point ( 23) is proved.

• Step 3 : let us prove the point (24) of Proposition 4.1. The proof is a straightforward adaptation of the previous one. We shall use that N S(ϕ j 0 ) is a sup-critical solution:

lim sup τ →1 (1 -τ ) N S(ϕ j 0 )(τ ) σs Ḣs = M σs c .
As we always have sup τ <1

(1τ ) N S(ϕ j 0 )(τ ) σs Ḣs lim sup τ →1

(1τ ) N S(ϕ j 0 )(τ ) σs Ḣs , we get a first inequality : sup τ <1

(1τ ) N S(ϕ j 0 )(τ ) σs Ḣs M σs c . According to the previous computations, we have, for any τ < 1, (1τ ) N S(ϕ j 0 )(τ ) σs

M 2 c + ε n (1 -τ ) 2 σs N S(ϕ j 0 )(τ )

Ḣs

M σs c , which provides the second desired inequality. This ends up the proof of [START_REF] Lions | The concentration-compactness principle in the calculus of variations. The limit case I[END_REF].

Let us recall some notation and add a few words about profiles with constant scale. Thanks to Lemma 3.2 and obvious boundaries from below we get for any τ < τ *

j 0 def = inf j∈J 1 T * (ϕ j ) = 1 N S(v 0,n )(τ ) 2 Ḣs j∈J 1 N S(ϕ j )(τ ) 2 Ḣs -|γ J n (τ )|. ( 30
)
Among profiles with a scale equal to 1 (e.g j ∈ J 1 ), we distinguish profiles with a lifespan equal to τ * j 0 = 1 and profiles with a lifespan τ * j strictly greater than 1. In other words, we consider the set

J1 def = {j ∈ J 1 | τ * j = 1}. Therefore, for any τ < 1, N S(v 0,n )(τ ) 2 Ḣs N S(ϕ j 0 )(τ ) 2 Ḣs + j∈ J1 , j =j 0 N S(ϕ j )(τ ) 2 Ḣs + j∈J 1 \ J1 N S(ϕ j )(τ ) 2 Ḣs -|γ J n (τ )|,
which be bounded from below once again by

N S(v 0,n )(τ ) 2 Ḣs N S(ϕ j 0 )(τ ) 2 Ḣs + j∈ J1 , j =j 0 N S(ϕ j )(τ ) 2 Ḣs -|γ J n (τ )|, (31)
since obviously the term

j∈J 1 \ J1 N S(ϕ j )(τ ) 2
Ḣs is positive.

• Step 4 : in order to complete the proof of Lemma 2.1, we have to prove that there exists a unique profile with a lifespan τ *

j 0 = 1, namely | J1 | = 1.
Once again, we assume that there exists at least two profiles in J1 . We expect a contraction. Arguments of the proof are similar to the ones used in the step 2. We shall use the fact (1τ )

2 σs N S(ϕ j )(τ ) 2
Ḣs can not be small as we want, by vertue of (4). Indeed, let us come back to Inequality (31). We have already proved that ϕ j 0 generates a sup-critical solution, blowing up at time 1. It means that for any ε > 0, there exists a time τ ε such that

0 < (1 -τ ε ) 2 σs < ε and M 2 c -ε (1 -τ ε ) 2 σs N S(ϕ j 0 )(τ ε ) 2 Ḣs M 2 c + ε. Therefore, Inequality (31) becomes at time τ ε (32) M 2 c + ε n M 2 c -ε + j∈ J1 ,j =j 0 (1 -τ ε ) 2 σs N S(ϕ j )(τ ε ) 2 Ḣs -|γ J n (τ ε )|.
By vertue of ( 4), there exists a universal constant c > 0 such that for any j ∈ J1 and j = j 0

(33) (1 -τ ) 2 σs N S(ϕ j )(τ ) 2 Ḣs c 2 .
As a result, taking the limit for n and J large enough, we infer that (still under the hypothesis

| J1 | > 1) (34) M 2 c M 2 c -ε + (| J1 | -1) c 2 -η.
Choosing ε small enough, we get a contradiction and as a consequence, | J1 | = 1. It means there exists a unique profile generating a sub-critical solution, blowing up at time 1. This completes the proof of Proposition 4.1, and thus the proof of Lemma 2.1.

Fluctuation estimates in Besov spaces

This section is devoted to the proof of Lemma 2.2. We shall prove some estimates on the fluctuation part which is given by the bilinear form

B(u, u)(t) def = N S(u 0 )(t) -e t∆ u 0 = u -e t∆ u 0 .
We distinguish the case

Ḃ 1 2
2,∞ from the case Ḃs ′ 2,∞ , even if proves ideas are similar : we cut-off according low and high frequencies in the following sense :

(T * -t)2 2j 1 and (T * -t)2 2j 1.
Concerning high frequencies, we shall use the regularization effet of the Laplacian. Let us start by proving the critical part of Lemma 2.2.

Lemma 5.1. Let 1 2 < s < 3 2 and u 0 ∈ Ḣs . It exists a positive constant C s such that If T * (u 0 ) < ∞ and M u def = (T * (u 0 ) -t) N S(u 0 )(t) σs Ḣs < ∞, then, we have u -e t∆ u 0 Ḃ 1 2 2,∞ < C s M 2 u .
Proof. Duhamel formula gives

(35) u -e t∆ u 0 def = B(u, u) = - t 0 e (t-t ′ )∆ P(div(u ⊗ u) dt ′ .
By vertue of classsical estimates on the heat term (see for instance Lemma 2.4 in [START_REF] Bahouri | Fourier Analysis and Nonlinear Partial Differential Equations[END_REF]), we have

(36) ∆ j e t∆ a L 2 C e -ct 2 2j ∆ j a L 2 .
Therefore, the fluctuation part becomes

∆ j B(u, u)(t) L 2 t 0 e -c(t-t ′ ) 2 2j 2 j ∆ j (u ⊗ u)(t ′ ) L 2 dt ′ t 0 e -c(t-t ′ ) 2 2j 2 j 2 -j(2s-3 2 ) u ⊗ u(t ′ ) Ḃ2s-3 2 2,∞ dt ′ . ( 37
)
We infer thus, thanks to the product laws in Sobolev spaces

2 j 2 ∆ j B(u, u)(t) L 2 t 0 e -c(t-t ′ ) 2 2j 2 j(3-2s) u(t ′ ) 2 Ḣs dt ′ . ( 38
)
By hypothesis, we have supposed that

M 2 u def = (T * (u 0 ) -t) N S(u 0 )(t) σs Ḣs < ∞.
As a result,

2 j 2 ∆ j B(u, u)(t) L 2 C s t 0 e -c(t-t ′ ) 2 2j 2 j(3-2s) M 2 u (T * (u 0 ) -t ′ ) 2 σs = t 0 1 {(T * (u 0 )-t ′ )2 2j 1} e -c(t-t ′ ) 2 2j 2 j(3-2s) M 2 u (T * (u 0 ) -t ′ ) 2 σs dt ′ + t 0 1 {(T * (u 0 )-t ′ )2 2j 1} e -c(t-t ′ ) 2 2j 2 j(3-2s) M 2 u (T * (u 0 ) -t ′ ) 2 σs dt ′ • (39)
We apply Young inequality : in the first integral, we consider L ∞ ⋆ L 1 , whereas in the second one, we consider L 1 ⋆ L ∞ in order to use the regularization effect of the Laplacian.

2 j 2 ∆ j B(u, u)(t) L 2 C s M 2 u T * (u 0 ) T * (u 0 )-2 -2j 2 j(3-2s) dt ′ (T * (u 0 ) -t ′ ) 2 σs + C s M 2 u t 0 e -c(t-t ′ ) 2 2j 2 j(3-2s) 2 2j(s-1 2 ) dt ′ . ( 40
)
We recall that

2 σ s def = s - 1 2 and s - 1 2 < 1.
As a result,

2 j 2 ∆ j B(u, u)(t) L 2 C s M 2 u 2 j(2s-3) 2 j(3-2s) + 1 2 2j 2 j(3-2s) 2 2j(s-1 2 ) C s M 2 u . (41)
This concludes the proof on the fluctuation estimate in the critical case.

The statement given below is a bit more general than the one of Lemma 2.2, which we deduce immediately by an interpoaltion argument (the same as given at the end of the proof of Theorem 1.2). (T * (u 0 )t)

1 2 (s ′ -1 2 ) u(t) -e t∆ u 0 Ḃs ′ 2,∞ < ∞.
Proof. Same arguments as above yield

∆ j B(u, u)(t) L 2 t 0 e -c(t-t ′ ) 2 2j 2 j 2 -j(2s-3 2 ) u ⊗ u(t ′ ) Ḃ2s-3 2 2,∞ dt ′ . (42)
Product laws in Sobolev spaces and hypothesis on u imply

2 js ′ ∆ j B(u, u)(t) L 2 t 0 e -c(t-t ′ ) 2 2j 2 j( 5 2 -2s+s ′ ) u(t ′ ) 2 Ḣs dt ′ t 0 e -c(t-t ′ ) 2 2j 2 j( 5 2 -2s+s ′ ) C (T * (u 0 ) -t ′ ) s-1 2 • ( 43
)
We split (the same cut off as before) according low and high frequencies. Concerning high frequencies, since T * (u 0 )t T * (u 0 )t ′ , we get

2 js ′ ∆ j B(u, u)(t) 1 {(T * -t)2 2j 1} L 2 t 0 e -c(t-t ′ ) 2 2j 2 j( 5 2 -2s+s ′ ) C (T * (u 0 ) -t) s-1 2 dt ′ 2 j( 1 2 -2s+s ′ ) C (T * (u 0 ) -t) s-1 2 • (44)
Choosing s ′ such that 1 2 -2s + s ′ < 0, we get

2 js ′ ∆ j B(u, u)(t) 1 {(T * -t)2 2j 1} L 2 C (T * (u 0 ) -t) 1 2 (-1 2 +2s-s ′ ) (T * (u 0 ) -t) s-1 2 = C (T * (u 0 ) -t) -1 2 (s ′ -1 2 ) ,
which yields the desired estimate, as far as high frequencies are concerned. Concerning low frequencies, let us come back to the very beginning.

2 js ′ ∆ j B(u, u)(t) 1 {(T * (u 0 )-t)2 2j 1} L 2 2 j(s ′ -s) 2 js ∆ j B(u, u) L 2 2 j(s ′ -s) u(t) -e t∆ u 0 Ḃs 2,∞ . (45) As u(t) -e t∆ u 0 Ḃs 2,∞ C (T * (u 0 ) -t) 1 2 (s-1 2 )
, we infer that

2 js ′ ∆ j B(u, u)(t) 1 {(T * (u 0 )-t)2 2j 1} L 2 2 j(s ′ -s) C (T * (u 0 ) -t) 1 2 (s-1 2 )
• Hypothesis of low frequencies implies

2 js ′ ∆ j B(u, u)(t) 1 {(T * (u 0 )-t)2 2j 1} L 2 C (T * (u 0 ) -t) 1 2 (s-1 2 )+ 1 2 (s ′ -s) = C (T * (u 0 ) -t) 1 2 (s ′ -1 2 )
• which ends up the proof for low frequency part. The proof of Lemma 5.2 is thus complete.

Existence of sup-critical solutions bounded in

Ḃ 1 2 2,∞
This section is devoted to complete the proof of Theorem 1.2, namely the part concerning the Ḃ 1 2 2,∞norm of the sup-critical solutions. We have already built some sup-critical elements in the space Ḣs . It turns out that, starting from this statement, we shall prove that data generating a sup-critical element are not only in Ḣs , but also in some others spaces such as

Ḃ 1 2 2,∞ ∩ Ḃs ′ 2,∞
, with s ′ satisfiying the condition given below, which stems from the proof of Lemma 2.2. The statement given below is actually a bit stronger than the one we want to prove, since we are going to catch some sup-critical solutions not only in Ḃ 1 2 2,∞ (as claimed by Theorem 1.2) but also in Ḃs ′ 2,∞ . The main idea to get such information on the regularity is to focus on the fluctuation part which is more regular than the solution itself. Notice that, in all this section, we use regularity index s ′ satisfying

s < s ′ < 2s - 1 2 • Theorem 6.1. There exists a data Φ 0 ∈ Ḃ 1 2 2,∞ ∩ Ḣs ∩ Ḃs ′ 2,∞ , such that T * (Φ 0 ) < ∞ and sup t<T * (Φ 0 ) (T * (Φ 0 ) -t) N S(Φ 0 )(t) σs Ḣs = lim sup t→T * (Φ 0 ) (T * (Φ 0 ) -t) N S(Φ 0 ) σs Ḣs = M σs c ,
and for any t < T * (Φ 0 ), N S(Φ 0 )

Ḃ 1 2 2,∞ < ∞.
Proof. The idea of the proof is to start with the existence of sup-sup-critical elements in Ḣs . Indeed, we have proved previously that there exists a data Ψ 0 ∈ Ḣs , such that Ψ def = N S(Ψ 0 ) is sup-critical. Therefore, by definition of lim sup, there exists a sequence t n ր T * (Ψ 0 ) such that

lim n→+∞ (T * (Ψ 0 ) -t n ) N S(Ψ 0 )(t n ) σs Ḣs = M σs c .
Let us introduce as before the rescaled sequence

v 0,n (y) = T * (Ψ 0 ) -t n 1 2 N S(Ψ 0 )(t n , T * (Ψ 0 ) -t n 1 2 y).
Such a sequence generates a solution which keeps on living until the time 1 and satisfies

v 0,n σs Ḣs = T * (Ψ 0 ) -t n N S(Ψ 0,n )(t n ) σs Ḣs . (46)
In the sake of simplicity, we note

τ n def = T * (Ψ 0 ) -t n .
Previous computations imply that (v 0,n ) is a bounded sequence of Ḣs . Now, inspired by the idea of Y. Meyer (fluctuation-tendancy method, [START_REF] Meyer | Wavelets, paraproducts, and Navier-Stokes equations, Current developments in mathematics[END_REF]), we decomposed the sequence (v 0,n ) into (47) v 0,n (y)

def = v 0,n (y) -τ 1 2
n e tn∆ Ψ 0 (τ

1 2 n y) + τ 1 2
n e tn∆ Ψ 0 (τ

1 2
n y), where we have v 0,n (y)

def = τ 1 2 n N S(Ψ 0 )(t n , τ 1 2 n y) It follows (48) v 0,n (y) def = τ 1 2 n N S(Ψ 0 )(t n , • ) -e tn∆ Ψ 0 B(Ψ,Ψ)(tn)=fluctuation part (τ 1 2 n y) + τ 1 2 n e tn∆ Ψ 0 tendancy part (τ 1 2
n y).

Lemma 6.2. The rescaled fluctuation part

φ n def = τ 1 2 n B(Ψ, Ψ)(t n , τ 1 2 n • ) is bounded in Ḣs ∩ Ḃ 1 2 2,∞ ∩ Ḃs ′ 2,∞ .
Proof. Indeed, concerning the

Ḃ 1 2
2,∞ we use firstly the scaling invariance of this norm and then we apply Lemma 2.2, which gives ( 49)

sup n φ n Ḃ 1 2 2,∞ = sup n N S(Ψ 0 )(t n , • ) -e tn∆ Ψ 0 Ḃ 1 2 2,∞ < ∞.
Concerning the Ḣs -norm, we apply successively the following arguments : scaling, triangular inequality and the fact that N S(Ψ 0 ) is a sup-critical element in Ḣs .

φ n σs Ḣs = τ n N S(Ψ 0 )(t n , • ) -e tn∆ Ψ 0 σs Ḣs τ n N S(Ψ 0 )(t n , • ) σs Ḣs + τ n e tn∆ Ψ 0 σs Ḣs M c + 1 n σs + τ n Ψ 0 σs Ḣs < ∞.
φ n σ s ′ Ḃs ′ 2,∞ = τ n N S(Ψ 0 )(t n , • ) -e tn∆ Ψ 0 σ s ′ Ḃs ′ 2,∞ . (51)
This concludes the proof of this Lemma 6.2.

By vertue of profile theory, we perform a profile decomposition of the sequence φ n in the Sobolev space Ḣs . But in this decomposition, there is only left profiles with constant scale, as Lemma below will prove it. The idea is clear. As φ n is bounded in the Besov space Ḣs ∩ Ḃ 1 2 2,∞ , big scales vanish. Likewise, the fact that φ n is bounded in the Besov space Ḣs ∩ Ḃs ′ 2,∞ implies that small scales vanish. That is the point in the Lemma below.

Lemma 6.3. • If (f n ) is a bounded sequence in Ḃ 1 2 2,∞ ∩ Ḣs and if lim sup n→+∞ f n Ḃs 2,∞
= L > 0, then there is no big scales in the profile decomposition of the sequence f n in Ḣs .

• If (f n ) is a bounded sequence in Ḃs ′ 2,∞ ∩ Ḣs , with s ′ > s > 1 2 and if lim sup n→+∞ f n Ḃs 2,∞ = L > 0, then
there is no small scales in the profile decomposition of the sequence f n in Ḣs .

Proof. We only proof the first part of the Lemma. The other one is similar. If lim sup

n→+∞ f n Ḃs 2,∞ = L > 0, it means there exists an extraction ϕ(n) such that f ϕ(n) Ḃs 2,∞ L 2
• Otherwise, for any subsequence of (f n ), we would have

f ϕ(n) Ḃs 2,∞ < L 2 and thus, lim n→+∞ f ϕ(n) Ḃs 2,∞ L 2 •
As a result, we would have lim sup

n→+∞ f n Ḃs 2,∞ L 2 < L,
2 kns ∆ kn f ϕ(n) L 2 = f ϕ(n) Ḃs 2,∞ . Therefore, lim n→+∞ 2 kns ∆ kn f ϕ(n) L 2 L 2 .
Let us introduce the scale λ n def = 2 -kn . As (up to extraction)

2 kns ∆ kn f ϕ(n) L 2 L 2
, then one has

2 kn(s-1 2 ) f ϕ(n) Ḃ 1 2 2,∞ L 2 •
Hence, the infimum limit of the sequence k n is not -∞, otherwise, the term 2 kn(s-1 2 ) would tend to 0 and thus L = 0 (since the sequence

f ϕ(n) Ḃ 1 2 2,∞
is bounded by hypothesis), which is false by hypothesis.

Therefore, λ n +∞ : big scales are excluded from the profile decomposition of the sequence f n . This concludes the proof of Lemma 6.3.

Continuation of the proof of Theorem 6.1.

Let us come back to the proof of sup-critical element in the Besov space

Ḃ 1 2 2,∞ ∩ Ḃs ′ 2,∞
. Firstly, we check that φ n satisfies hypothesis of Lemma 6.3. As it was already checked previously,

φ n is bounded in Ḃ 1 2 2,∞ ∩ Ḣs ∩ Ḃs ′ 2,∞ . Concerning assumption lim sup n→+∞ φ n Ḃs 2,∞
> 0, by scaling argument, one has

φ n σs Ḃs 2,∞ = τ n N S(Ψ 0 )(t n , • ) -e tn∆ Ψ 0 σs Ḃs 2,∞ = (T * (Ψ 0 ) -t n ) N S(Ψ 0 )(t n , • ) -e tn∆ Ψ 0 σs Ḃs 2,∞ (T * (Ψ 0 ) -t n ) N S(Ψ 0 )(t n , • ) σs Ḃs 2,∞ -(T * (Ψ 0 ) -t n ) Ψ 0 σs Ḣs . (53)
Obviously, the term (T * (Ψ 0 )t n ) Ψ 0 σs Ḣs tends to 0 when n goes to +∞. By vertue of ( 4) and [START_REF] Lemarié-Rieusset | Recent Developments in the Navier-Stokes Problem[END_REF], there exists a constant c > 0 such that

(T * (Ψ 0 ) -t n ) N S(Ψ 0 )(t n , • ) σs Ḃs 2,∞ c. Therefore, lim sup n→+∞ φ n Ḃs 2,∞ > 0
and thus profile decomposition of φ n in the space Ḣs is reduced to (with notations of Theorem 3.1) (54)

φ n = J j 0 V j (• -x n,j ) + r J n .
Moreover, as the sequence φ n is bounded in

Ḃ 1 2 2,∞ ∩ Ḃs ′ 2,∞ , profiles V j belong also to Ḃ 1 2 2,∞ ∩ Ḃs ′ 2
,∞ . That's the crucial point in the proof. Indeed, each profile V j can be seen as a translated (by x n,j ) weak limit of the sequence φ n . As a result, we get immediately

V j Ḃ 1 2 2,∞ lim inf n→+∞ φ n Ḃ 1 2 2,∞ < ∞ and V j Ḃs ′ 2,∞ lim inf n→+∞ φ n Ḃs ′ 2,∞ < ∞.
Let us come back to the sequence (v 0,n ) defined by

v 0,n def = φ n + τ 1 2 n e tn∆ Ψ 0 (τ 1 2 n • ).
As it has been already underlined previously, the term γ n def = τ n e tn∆ Ψ 0 (τ

1 2 n • ) σs Ḣs = τ n e tn∆ Ψ 0 σs Ḣs τ n Ψ 0 σs Ḣs .
Combining the profile decomposition of (φ n ) with the definition of (v 0,n ), we finally get

v 0,n = J j 0 V j (• -x n,j ) + r J n + γ n ,
with lim J→+∞ lim sup n→+∞ r J n L p = 0 and lim n→+∞ γ n L p = 0. By vertue of Lemma 3.2, one has for any τ < 1

N S(v 0,n )(τ ) = J j 0 N S(V j )(τ, • -x n,j ) + e τ ∆ (r J n + γ n ) + R J n (τ ).
By definition of the sequence

(v 0,n ), N S(v 0,n ) is given by N S(v 0,n )(τ, • ) = T * (Ψ 0 ) -t n 1 2 N S(Ψ 0 ) t n + τ T * (Ψ 0 ) -t n , T * (Ψ 0 ) -t n 1 2 • .
Once again, we denote t n = t n + τ T * (Ψ 0 )t n and one has

(1 -τ ) N S(v 0,n )(τ, • ) σs Ḣs = T * (Ψ 0 ) -t n N S(Ψ 0 ) t n , • σs
Ḣs . As t n t n for any n, we get

(1 -τ ) N S(v 0,n )(τ ) σs Ḣs = (T * (Ψ 0 ) -t n ) N S(Ψ 0 )( t n ) σs Ḣs M σs c + 2 n •
Hence, Proposition 4.1 implies there exists some a unique profile

Φ 0 in Ḃ 1 2 2,∞ ∩ Ḣs ∩ Ḃs ′
2,∞ such that the N S-solution genrated by this profile is a sup-critical solution. As Φ 0 belongs to Ḃ 1 2 2,∞ , Lemma 2.2 implies that N S(Φ 0 ) is bounded in the same space. This ends up the proof of Theorem 6.1. Hence, we claim that the proof of Theorem 1.2 is over. Indeed, this stems from an interpolation argument. By vertue of Proposition 3.3, we have for any s < s

1 < s ′ Φ 0 Ḣs 1 Φ 0 Ḃs 1 2,1 Φ 0 θ Ḃs 2,∞ Φ 0 1-θ Ḃs ′ 2,∞ Φ 0 θ Ḣs Φ 0 1-θ Ḃs ′ 2,∞ . (56)
This concludes the proof of Theorem 1.2.

Another notion of critical solution

In this section, we wonder if among sup-critical solutions, we can find some of them which reach the biggest infimum limit of the quantity (T * (u 0 )t) N S(u 0 )(t) σs Ḣs . We define the following set E c by

E c def = u 0 ∈ Ḃ 1 2 2,∞ ∩ Ḣs ∩ Ḃs ′ 2,∞ such that T * (u 0 ) < ∞ ; sup t<T * (u 0 ) (T * (u 0 ) -t) N S(u 0 )(t) σs Ḣs = lim sup t→T * (u 0 ) (T * (u 0 ) -t) N S(u 0 )(t) σs Ḣs = M σs c ; for any t < T * (u 0 ), N S(u 0 )(t) Ḃ 1 2 2,∞ < ∞ and (T * (u 0 ) -t) N S(u 0 )(t) σ s ′ Ḃs ′ 2,∞ < ∞ .
Let us introduce the following quantity m σs c

m σs c def = sup u 0 ∈ Ec lim inf t→T * (u 0 ) (T * (u 0 ) -t) N S(u 0 )(t) σs Ḣs . Definition 7.1. (sup-inf-critical solution) A solution u = N S(u 0 ) is said to be a sup-inf-critical solution if u 0 belongs to E c and lim inf t→T * (u 0 ) (T * (u 0 ) -t) N S(u 0 )(t) σs Ḣs = m σs c . (57)
Notice we need to look for such elements among sup-critical solutions, otherwise the definition of m σs c would be meaningless. We claim that there exist such elements. Lemma 7.1. There exists some elements belonging to E c , which are sup-inf-critical.

Proof. By definition of m σs c , we can find a sequence (u 0,n ) ∈ Ḣs and a sequence t n ր T * (u 0,n ) ≡ T * (we can assume this, up to a rescaling) such that (58)

m c -ε n (T * -t n ) 1 σs N S(u 0,n )(t n ) Ḣs m c + ε n and (59) For any t t n , m c -ε n (T * -t) 1 σs N S(u 0,n )(t) Ḣs .
Assume in addition that the sequence (u 0,n ) belongs to the set E c . As a consequence, we have (60) For any t t n , m cε n (T *t)

1 σs N S(u 0,n )(t) Ḣs M c + ε n .
Considering the rescaled sequence

v 0,n (y) = T * -t n 1 2 N S(u 0,n ) t n , (T * -t n 1 2 y .
Hence, v 0,n satisfies properties below by scaling argument

v 0,n σs Ḣs = T * -t n N S(u 0,n )(t n ) σs Ḣs , v 0,n Ḃ 1 2 2,∞ = N S(u 0,n )(t n ) Ḃ 1 2 2,∞ and v 0,n σ s ′ Ḃs ′ 2,∞ = T * -t n N S(u 0,n )(t n ) σ s ′ Ḃs ′ 2,∞ . (61)
Combining (58) with the fact that (u 0,n ) belongs to E c , we infer that the sequence

(v 0,n ) n 1 is bounded in Ḃ 1 2 2,∞ ∩ Ḣs ∩ Ḃs ′ 2,∞ .
Moreover, concerning the Navier-Stokes solution generated by such a data N S(v 0,n ), we know that it keeps on living until the time τ * = 1 and satisfies once again (with

t n = t n + τ T * -t n ) (62) (1 -τ ) 1 σs N S(v 0,n )(τ ) Ḣs = (T * -t n ) 1 σs N S(u 0,n )( t n ) Ḣs .
As t n t n for any n, we infer that for any τ < 1

(1τ )

1 σs N S(v 0,n )(τ ) Ḣs m c -ε n .
Let us sum up information we have on the sequence v 0,n . Firstly, the lifespan of the Navier-Stokes associated with the sequence v 0,n is equal to 1. Then,

lim sup τ →1 (1 -τ ) 1 σs N S(v 0,n )(τ ) Ḣs = lim sup tn→T * (T * -t n ) 1 σs N S(u 0,n )( t n ) Ḣs ,
which implies, thanks to (60) and definition of M c , that for any τ < 1, lim sup τ →1

(1τ )

1 σs N S(v 0,n )(τ ) Ḣs = M c and N S(v 0,n )(τ ) Ḃ 1 2 2,∞ = N S(u 0,n )( t n ) Ḃ 1 2 2,∞ < ∞.
In addition,

(1 -τ ) 1 σ s ′ N S(v 0,n )(τ ) Ḃs ′ 2,∞ = (T * -t n ) 1 σ s ′ N S(u 0,n )( t n ) Ḃs ′ 2,∞ < ∞. ( 63
)
To summerize, from the minimizing sequence (u 0,n ) of the set E c , we build another sequence (v 0,n ) (the rescaled sequence of (u 0,n )) which also belongs to the set E c . Moreover, as the sequence

(v 0,n ) is bounded in the spaces Ḃ 1 2 2,∞ ∩ Ḣs ∩ Ḃs ′ 2,∞ and satisfies lim sup n→+∞ v 0,n Ḃs 2,∞
< ∞, Lemma 6.3 implies that profile decomposition in Ḣs of such a sequence is reduced, up to extractions, to a sum of translated profiles and a remaining term (under notations of Theorem 3.1)

v 0,n = j∈J 1 ϕ j (• -x n,j ) + ψ J n .
By vertue of Theorem 3.2, combining with Proposition 4.1, we infer there exists only one profile ϕ j 0 which blows up at time 1 and such that

(64) N S(v 0,n )(τ, • ) = N S(ϕ j 0 )(τ, • -x n,j 0 ) + j∈J 1 ,j =j 0 τ j * >1 N S(ϕ j )(• -x n,j ) + e τ ∆ ψ J n (• ) + R J n (τ, • ).
By orthogonality, we have

N S(v 0,n )(τ ) 2 Ḣs N S(ϕ j 0 )(τ ) 2 Ḣs + j∈J 1 ,j =j 0 τ j * >1 N S(ϕ j )(τ ) 2 Ḣs + + e τ ∆ ψ J n 2 Ḣs + |γ J n (τ )|. ( 65
)
We want to prove that lim inf τ →1

(1τ ) N S(ϕ j 0 )(τ ) Ḣs = m c . Let us assume that is not the case. Therefore,

∃α 0 > 0, ∀ε > 0, ∃τ ε , such that 0 < (1 -τ ε ) 2 σs < ε and (1 -τ ε ) 2 σs N S(u 0,n )(τ ε ) 2 Ḣs m 2
cα 0 . From (65), we deduce that

(1 -τ ε ) 2 σs N S(v 0,n )(τ ε ) 2 Ḣs = (1 -τ ε ) 2 σs N S(ϕ j 0 )(τ ε ) 2 Ḣs + (1 -τ ε ) 2 σs j∈J 1 ,j =j 0 τ j * >1 N S(ϕ j )(τ ε ) 2 Ḣs + e τε∆ ψ J n 2 Ḣs + |γ J n (τ ε )| .
By hypothesis, (1τ ε )

1 σs N S(v 0,n )(τ ε ) Ḣs m c -ε n , and 1 -τ ε 1. Hence, we get m c -ε n 2 m 2 c -α 0 + (1 -τ ε ) 2 σs j∈J 1 ,j =j 0 τ j * >1 sup τ ∈[0,1] N S(ϕ j )(τ ) 2 Ḣs + ψ J n 2 Ḣs + |γ J n (τ ε )|. (66)
On the one hand, as profiles ϕ j have a lifespan τ j * > 1, the quantity sup

τ ∈[0,1]
N S(ϕ j )(τ ) 2 Ḣs is finite.

On the other hand, by vertue of profile decomposition of the sequence (v 0,n ), we have obviously that

ψ J n 2 Ḣs v 0,n 2
Ḣs . As we have proved that (v 0,n ) is an element of the set E c , we get in particular that sup τ <1

(1τ ) 1 σs N S(v 0,n )(τ ) Ḣs = M c , which leads to (at τ = 0) v 0,n Ḣs M c . Finally, for all τ ε ,

(1 -τ ε ) 2 σs j∈J 1 ,j =j 0 τ j * >1 sup τ ∈[0,1] N S(ϕ j )(τ ) 2 Ḣs + ψ J n 2 Ḣs α 0 4 , we get m c -ε n 2 m 2 c -α 0 + α 0 4 + |γ J n (τ ε )|. (67)
Now, by assumption of γ J n , we take the limit for n and J large enough, and we get

(68) m 2 c m 2 c - 3 α 0 4 + α 0 4 ,
which is obviously absurd. Thus, we have proved that lim inf τ →1

(1τ )

1 σs N S(ϕ j 0 )(τ ) Ḣs = m c .
This concludes the proof of Lemma 7.1.

Structure Lemma for Navier-Stokes solutions with bounded data

The sequence (v 0,n ) n 0 be a bounded sequence of initial data in Ḣs . Thanks to Theorem 3.1, (v 0,n ) n 0 can be written as follows, up to an extraction

v 0,n (x) = J j=0 Λ 3 p
λ n,j ,x n,j ϕ j (x) + ψ J n (x), which can be written as follows

v 0,n (x) = j∈J 1 j J ϕ j (x -x n,j ) + j∈J c 1 j J Λ 3 p
λ n,j ,x n,j ϕ j (x) + ψ J n (x). (69) Let η > 0 be the parameter of rough cutting off frequencies. We define by w η (x) and wc η (x) the elements which Fourier transform is given by (70)

w η (ξ) = w(ξ)1 { 1 η |ξ| η} and wc η (ξ) = w(ξ) 1 -1 { 1 η |ξ| η} .
After rough cutting off frequencies with respect to the notations (70) and sorting profiles supported in the annulus 1 { 1 η |ξ| η} according to their scale (thanks to the orthogonality property of scales and cores, given by Theorem 3.1). We get the following profile decomposition

v 0,n (x) = j∈J 1 ϕ j (x -x n,j ) + j∈J 0 Λ 3 p λ n,j ,x n,j ϕ j η (x) + j∈J∞ Λ 3 p λ n,j ,x n,j ϕ j η (x) + ψ J n,η (x)
where ψ J n,η (x)

def = j∈J c 1 ≡J 0 ∪J∞ j J Λ 3 p λ n,j ,x n,j V j c η (x) + ψ J n (x), (71)
for any j in J 1 ⊂ J, λ n,j = 1, for any j in J 0 , lim n→+∞ λ n,j = 0 and for any j in J ∞ , lim n→+∞ λ n,j = +∞.

As mentionned in the introduction, the whole Lemma 3.2 has been already proved in [START_REF] Poulon | About the behaviour of regular Navier-Stokes solutions near the blow up[END_REF], except for the orthogonality property of the Navier-stokes solution associated with such a sequence of initial data. Therefore, we refer the reader to [START_REF] Poulon | About the behaviour of regular Navier-Stokes solutions near the blow up[END_REF] for details of the proof and here, we focus on the "Pythagore property". Let us recall the notations

U 0 n,η def = j∈J 0 Λ 3 p λ n,j ,x n,j ϕ j η and U ∞ n,η def = j∈J∞ Λ 3 p
λ n,j ,x n,j ϕ j η .

We recall some properties on profiles with small and large scale and remaining term. We refer the reader to [START_REF] Poulon | About the behaviour of regular Navier-Stokes solutions near the blow up[END_REF] to the proof of the two propositions below.

Proposition 8.1.

For any s 1 < s, for any η > 0, for any j ∈ J 0 , (e.g lim

n→+∞ λ n,j = 0), then lim n→+∞ U 0 n,η Ḣs 1 = 0.
For any s 2 > s, for any η > 0, for any j ∈ J ∞ , (e.g lim

n→+∞ λ n,j = +∞), then lim n→+∞ U ∞ n,η Ḣs 2 = 0.
Concerning the remaining term, we can show it tends to 0, thanks to Lebesgue Theorem.

N S(v 0,n )(t, •) 2 Ḣs = j∈J 1 N S(ϕ j )(t, • -x n,j ) 2 Ḣs + e t∆ j∈J c 1 j J Λ 3 p λ n,j ,x n,j ϕ j (x) + ψ J n 2 Ḣs + R J n (t, •) 2 Ḣs + 2 j∈J 1 N S(ϕ j )(t, • -x n,j ) | e t∆ j∈J c 1 j J Λ 3 p λ n,j ,x n,j ϕ j (x) + ψ J n Ḣs + 2 j∈J 1 N S(ϕ j )(t, • -x n,j ) | R J n Ḣs + 2 e t∆ j∈J c 1 j J Λ 3 p λ n,j ,x n,j ϕ j (x) + ψ J n | R J n Ḣs .
Therefore, proving ( 21) is equivalent to prove Propositions 8.3 and 8.4 below. Both of them essentially stem from the orthogonality of cores and a compactness argument.

Proposition 8.3. Let ε > 0. Then, for any t ∈ [0, T -ε], (72)
j∈J 1 N S(ϕ j )(t, • -x n,j ) 2 Ḣs = j∈J 1 N S(ϕ j )(t, • ) 2 Ḣs + γ n,ε (t), with lim n→+∞ sup t∈[0, T -ε] |γ n,ε (t)| = 0.
Proof. Once again, we developp the square of Ḣs -norm and we get for any t < T

j∈J 1 N S(ϕ j )(t, • -x n,j ) 2 Ḣs = j∈J 1 N S(ϕ j )(t, • -x n,j ) 2 Ḣs + 2 (j,k)∈J 1 ×J 1 j =k Λ s N S(ϕ j )(t, • -x n,j ) | Λ s N S(ϕ k )(t, • -x n,k ) L 2 ,
where Λ = √ -∆. Let ε > 0. Then, for any t in [0, Tε], we get

j∈J 1 N S(ϕ j )(t, • -x n,j ) 2 Ḣs = j∈J 1 N S(ϕ j )(t, • ) 2 Ḣs + 2 (j,k)∈J 1 ×J 1 j =k Γ s,j,k ε,n , where Γ s,j,k ε,n def = Λ s N S(ϕ j )(t, • -x n,j ) | Λ s N S(ϕ k )(t, • -x n,k ) L 2 . We denote by K J ε def = j∈J Λ s N S(ϕ j )([0, T -ε]).

By vertue of the continuity of the map

t ∈ [0, T -ε] → Λ s N S(ϕ j )(t, • ) ∈ L 2 , we deduce that K J
ε is compact (and thus precompact) in L 2 . It means that it can be covered by a finite open ball with an arbitrarily radius α > 0. Let α be a positive radius. There exists an integer N α , and there exists (θ ℓ ) 1 ℓ Nα some elements of D(IR 3 ), such that (73)

K J ε ⊂ Nα ℓ=1 B(θ ℓ , α).
Let us come back to the proof of 8.3. Thanks to the previous remark, we approach each profil Λ s N S(ϕ j )(t, • ) (resp. Λ s N S(ϕ k )(t, • )) by a smooth function: e.g there exists a integer ℓ ∈ {1, • • • N α } and there exists a function θ ℓ(j,t) (resp. θ ℓ(k,t) ) in D(IR 3 ) and we get

Γ s,j,k ε,n = Λ s N S(ϕ j )(t, • -x n,j ) -θ ℓ(j,t) (• -x n,j ) | Λ s N S(ϕ k )(t, • -x n,k ) -θ ℓ(k,t) (• -x n,k ) L 2 + Λ s N S(ϕ j )(t, • -x n,j ) -θ ℓ(j,t) (• -x n,j ) | θ ℓ(k,t) (• -x n,k ) L 2 + θ ℓ(j,t) (• -x n,j ) | Λ s N S(ϕ k )(t, • -x n,k ) -θ ℓ(k,t) (• -x n,k ) L 2 + θ ℓ(j,t) (• -x n,j ) | θ ℓ(k,t) (• -x n,k ) L 2 . (74)
The three first terms in the right-hand side of the above estimate tend uniformly (in time) to 0, by vertue of Cauchy-Schwarz and the translation-invariance of the Ḣs -norm (we just perform the estimate for the first term, the others are similar). For any t ∈ [0, Tε]

Λ s N S(ϕ j )(t, • -x n,j ) -θ ℓ(j,t) (• -x n,j ) | Λ s N S(ϕ k )(t, • -x n,k ) -θ ℓ(k,t) (• -x n,k ) L 2 Λ s N S(ϕ j )(t) -θ ℓ(j,t) L 2 Λ s N S(ϕ k )(t) -θ ℓ(k,t) L 2 α 2 . (75)
Therefore, for any α > 0, we have ( 76)

sup t∈[0, T -ε] Λ s N S(ϕ j )(t, • -x n,j ) -θ ℓ(j,t) (• -x n,j ) | Λ s N S(ϕ k )(t, • -x n,k ) -θ ℓ(k,t) (• -x n,k ) L 2 α 2 .
For the last term θ ℓ(j,t) (

• -x n,j ) | θ ℓ(k,t) (• -x n,k ) L 2 , we have θ ℓ(j,t) (• -x n,j ) | θ ℓ(k,t) (• -x n,k ) L 2 = IR 3 θ ℓ(j,t) (x) θ ℓ(k,t) (x + x n,j -x n,k ) dx.
It follows immediately that the above term tends to 0, when n tend to +∞, by vertue of Lebesgue theorem combining with the orthogonality property of cores(e.g. lim n→∞ |x n,jx n,k | = +∞). To sum up, we have proved that Γ s,j,k ε,n tends to 0 when n tends to +∞, uniformly in time. This concludes the proof of Proposition 8.3.

Concerning the crossed-terms in the profile decomposition, we have to prove they are also negligable, uniformly in time. That is the point in the following proposition. Proposition 8.4. Let ε > 0, We denote by By vertue of the continuity of the map t ∈ [0, Tε] → N S(ϕ j )(t, • ) ∈ Ḣs , we deduce that Λ J ε is compact (and thus precompact) in Ḣs . It means that it can be covered by a finite open ball with an arbitrarily radius β > 0. Let β be a positive radius. There exists an integer N β , and there exists (χ ℓ ) 1 ℓ N β some elements of D(IR 3 ), such that

I n (t, • ) def = j∈J 1 N S(ϕ j )(t, • -x n,j ) | e t∆ j∈J c 1 j J Λ 3 p λ n,j ,x n,j ϕ j (x) + ψ J n Ḣs , then, one has lim J→+∞ lim η→+∞ lim n→+∞ sup t∈[0, T -ε] I n (t, • ) = 0, (77) lim J→+∞ lim n→+∞ sup t∈[0, T -ε] j∈J 1 N S(ϕ j )(t, • -x n,j ) | R J n (t) Ḣs = 0, (78)
Concerning the second part of above inequality, we shall use the splitting with respect to the parameter of cut off η. We refer the reader to the beginning of this section for notations. λ n,j ,x n,j ϕ j + ψ J n Ḣs = I Obviously the term ψ J n,η Ḣs is bounded by profiles hypothesis and the term Λ 2s χχ ℓ(t,j) L p ′ is bounded too, since the function χ is as regular as we need. By vertue of Proposition 8.2, the term ψ J n,η L p is small in the sense of for any ε > 0, there exists an integer N 0 ∈ N , such that for any n N 0 , there exists η > 0 and J 0, such that for any η η and for any J J , we have ψ J n,η L p ε. As a result, we get for any lim This ends up the proof of estimate (77).

Concerning the proof of ( 78) and (79), the proof is very close in both cases and relies on the fact that the error term R J n tends to 0 in the L ∞ T ( Ḣs )-norm. For any t ∈ [0, Tε], we have λ n,j ,x n,j ϕ j (x)

+ ψ J n L ∞ T ( Ḣs ) R J n L ∞ T -ε ( Ḣs ) U 0 n,η + U ∞ n,η + ψ J n,η Ḣs R J n L ∞ T -ε ( Ḣs ) . (86)
Thanks to profile decomposition (71), we get We end up the proof as before, thanks to the hypothesis on R J n . This completes the proof of Proposition 8.4 and thus Lemma 3.2.

U 0 n,η + U ∞ n,η + ψ J n,η 2

Remark 1 . 3 .

 13 Theorem 1.1 implies there exists a constant c > 0, such that (4) (T * (u 0 )t) N S(u 0 )(t) σs Ḣs c, and thus we get in particular the blow up of the Ḣs -norm lim t→T * (u 0 )

Proposition 4 . 1 .

 41 Let (v 0,n ) n∈IN be a bounded sequence in Ḣs such that τ * (v 0,n ) = 1 and for any τ < 1, (1τ ) N S(v 0,n )(τ, ) σs

and u 0 ∈

 0 Ḣs . It exists a positive constant C s such that If T * (u 0 ) < ∞ and M u def = (T * (u 0 )t) N S(u 0 )(t) σs Ḣs < ∞, then, we have for any s < s ′ < 2s -1 2

  Concerning the Ḃs ′ 2,∞ -norm, scaling argument combinig with Lemma 2.2 yields

1 2 n 2 n

 122 e tn∆ Ψ 0 (τ 1 • ) tends to 0 in Ḣs -norm (and thus in L p -norm, by Sobolev embedding) since (55) τ 1 2

  ϕ j 0 )(τ ) Ḣs m c . By definition of m c , this will imply that lim inf τ →1 (1τ ) 1 σs

  j ,x n,j ϕ j (x) + ψ J n | R J n (t) Ḣs = 0. (79)Proof. Let us start by proving (77). We shall use once again an approximation argument. Let us defineΛ J ε def = j∈J N S(ϕ j )([0, Tε]).

j∈J 1 N 1 N 1 χ 1 χ

 1111 ℓ , β).Let us come back to the proof of (77). Same arguments as previously imply there exists an integer ℓ ∈ {1• • • N β } and a smooth function χ ℓ(t,j) in D(IR 3 ) such thatI n (t, • ) def = S(ϕ j )(t, •x n,j ) | e t∆ j ,x n,j ϕ j + ψ J n Ḣs = j∈J S(ϕ j )(t, •x n,j )χ ℓ(t,j) (• -x n,j ) | e t∆ j ,x n,j ϕ j + ψ J n Ḣs + j∈J ℓ(t,j) (• -x n,j ) | e t∆ j ,x n,j ϕ j + ψ J n Ḣs . j ,x n,j ϕ j + ψ J n Ḣs v 0,n Ḣs , we infer thatI n (t, • ) |J 1 | β v 0,n Ḣs + j∈J ℓ(t,j) (• -x n,j) | e t∆ j ,x n,j ϕ j + ψ J n Ḣs

j∈J 1 χ

 1 ℓ(t,j) (• -x n,j ) | e t∆

j∈J 1 N 1 N

 11 S(ϕ j )(t, •x n,j ) | R J n Ḣs j∈J 1 N S(ϕ j )(t, • ) | R J n (t, • +x n,j ) Ḣs |J 1 | N S(ϕ j )(t, • ) L ∞ T ( Ḣs ) R J n (t, • ) L ∞ T ( Ḣs ) .(85)Obviously, the term N S(ϕ j )(t,• ) L ∞ T ( Ḣs ) is bounded since t ∈ [0, Tε]. As a result, Lemma 3S(ϕ j )(t, •x n,j ) | R J n Ḣs |= 0.As far as estimate (79) is concerned, the idea is the same. For any t ∈ [0, Tj ,x n,j ϕ j (x) + ψ J n j ,x n,j ϕ j (x) + ψ J n

  j ,x n,j ϕ j (x) + ψ J n | R J n Ḣs | C v 0

  Step 2 : Existence of sup-critical elements in Ḣs ∩ Ḣs ′ , with s and s ′ such that s < s ′ < 2s -

	Ḃ 1 2 2,∞ ∩ 1 2 This will be proved in Section 6. Notice that proving that N S(Ψ 0 ) is bounded in the Besov space Ḃ 1 2 2,∞ • is equivalent to prove that Ψ 0 belongs to Ḃ 1 2 2,∞ , since, by vertue of Lemma 2.2, the fluctuation part is bounded in Ḃ 1 2

  1[ and (p, r) in [1, ∞] 2 . A constant C exists such that, for any u ∈ S ′ ,We recall an interpolation property in Besov spaces, which will be useful in the sequel.

	(22)	C -1 u Ḃs p,r	u(• -y) -u L p |y| s	L r (IR d ; dy |y| d )	C u Ḃs p,r	.
	Remark 3.2. Notice that Ḣs ⊂ Ḃs 2,2 and both spaces coincide if s <	3 2	•

Proposition 3.3. A constant C exists which satisifes the following property. If s 1 and s 2 are real numbers such that s 1 < s 2 and θ ∈]0, 1[, then we have for any p ∈ [1, +∞]

  which is wrong by hypothesis. Moreover, by definition of the Besov norm, we can find a sequence (k n ) n∈Z , such that

	(52)	lim n→+∞

  Continuation of Proof of Lemma 3.2. By vertue of (20) in Lemma 3.2, it seems clear that for any t < T

	Proposition 8.2.
	lim J→+∞	lim η→+∞	lim sup n→+∞	ψ J n,η L p = 0.

  ḢsandI 3 n (t, • ) = j∈J 1 χ ℓ(t,j) (• -x n,j ) | e t∆ ψ J n,η Ḣs .Let us start with I 1 n (t, • ). One has|I 1 n (t, • )| |J 1 | χ ℓ(t,j) Ḣ2s-s 1 e t∆ U 0 n,η Ḣs 1 |J 1 | χ ℓ(t,j) Ḣ2s-s 1 U 0 n,η Ḣs 1 .Proposition 8.1 (for η and j ∈ J 1 fixed) implies thus limConcerning profiles with large scale, the proof is similar and we get for any t ∈ [0, Tε]|I 2 n (t, • )| |J 1 | χ ℓ(t,j) Ḣ2s-s 2 U ∞ n,η (x) Ḣs 2 . (83)Once again, Proposition 8.1 implies the result : lim • )| Λ 2s χ ℓ(t,j) | e t∆ ψ J n,η (• +x n,j ) L 2 Λ 2s χ ℓ(t,j) L p ′ e t∆ ψ J n,η (• +x n,j ) L p . By translation invariance of the L p -norm and estimate on the heat equation, we get

			n→+∞	sup t∈[0, T -ε]	|I 2 n (t, • )| = 0.
	Concerning the last term I 3 n , Hölder inequality with	1 p	+	1 p ′ = 1 yields
	(84)	|I 3 n (t, |I 3 n (t, • )|	Λ 2s χ ℓ(t,j) L p ′ ψ J n,η L p .
				n→+∞	sup t∈[0, T -ε]	|I 1 n (t, • )| = 0.

1 n (t, • ) + I 2 n (t, • ) + I 3 n (t, • ),

where

I 1 n (t, • ) = j∈J 1 χ ℓ(t,j) (• -x n,j ) | e t∆ U 0 n,η Ḣs ; I 2 n (t, • ) = j∈J 1 χ ℓ(t,j) (• -x n,j ) | e t∆ U ∞ n,η