Lemma 7.1.1, 7.1.2 and most of 7.1.5

[Parcly-Taxel]

There is an error in the blueprint proof of 7.1.5: it is possible that the minimum $s_1$ of $\sigma(\mathfrak u,x)$ is equal to $S$, and in that case the equation to be shown reduces to

∑ x_1 ∈ t.σ u x, ∫ (y : X), Ks x_1 x y * approxOnCube (𝓙 (t.𝔗 u)) f y = 0

which is clearly false in general. (In fact it can be easily reduced further to ∫ (y : X), Ks S x y * approxOnCube (𝓙 (t.𝔗 u)) f y = 0, but this is not in the PR code.)