We set \(Γ_x(t) = ∫_0^t \left(γ_x(s) - \overline{γ}_x\right)ds\), so that \(f'(x) = f(x) + Γ_x(Nπ(x))/N\). Because each \(Γ_x\) is \(1\)-periodic, and everything has compact support in \(E\), all derivatives of \(Γ\) are uniformly bounded. Item 1 in the statement is then obvious. Item 2 also follows since \(∂_if'(x) = ∂_if(x) + ∂_iΓ(x, Nπ(x))/N\). In order to prove Item 3, we compute:

Outside the support of \(γ\), \(Γ_x\) and its derivative with respect to \(x\) vanish identically (for the derivative computation, it is important that the support of \(γ\) is the closure of the set of \(x\) where \(γ_x\) is not constant).

These are direct checks.

We denote the components of \(\mathcal{F}\) by \(f\) and \(φ\). Since \(\mathcal{F}\) is short, proposition 1.2 applied to \(g \! :x ↦ Df(x)v\), \(β \! :x ↦ φ(x)v\), \(Ω_x = \mathcal{R}(\mathcal{F}(x), π, v)\), and \(K = C ∩ K_1\) gives us a smooth family of loops \(γ \! :E × [0, 1] × 𝕊^1 → F\) such that, for all \(x\):

• \(∀ t\, s,\; γ^t_x(s) ∈ \mathcal{R}(\mathcal{F}(x), π, v)\)

• \(∀ s,\; γ^0_x(s) = φ(x)v\)

• \(\barγ^1_x = Df(x)v\)

• if \(x\) is near \(C\), \(∀t\, s,\; γ^t_x(s) = φ(x)v\)

Let \(ρ: E → ℝ\) be a smooth cut-off function which equals one on a neighborhood of \(K_0\) and whose support is contained in \(K_1\).

Let \(N\) be a positive real number. Let \(\bar f\) be the corrugated map constructed from \(f\), \(γ^1\) and \(N\). Proposition 2.3 ensures that, for all \(x\),

for some remainder term \(R\) which is \(ε\)-small and vanishes whenever \(γ_x\) is constant, hence vanishes near \(C\).

We set \(\mathcal{F}_t(x) = \big(f_t(x), φ_t(x)\big)\) where:

and

We now prove that \(\mathcal{F}_t\) has the announced properties, starting with he obvious ones. The fact that \(\mathcal{F}_0 = \mathcal{F}\) is obvious since \(γ^0_x(s) = φ(x)v\) for all \(s\).

When \(x\) is near \(C\), \(Df(x) = φ(x)\) since \(\mathcal{F}\) is holonomic near \(C\). In addition, \(γ^t_x(s) = φ(x)v\) for all \(s\) and \(t\), hence \(B_x\) vanishes. Hence \(\mathcal{F}_t(x) = \mathcal{F}(x)\) for all \(t\) when \(x\) is near \(C\).

Outside of \(K_1\), \(ρ\) vanishes. Hence \(f_t(x) = f(x)\) for all \(t\), and \(γ^{tρ(x)}_x(s) = φ(x)v\) for all \(s\) and \(t\), and \(φ_t(x) = φ(x)\).

The distance between \(f(x)\) and \(f_t(x)\) is zero outside of \(K_1\) and \(ε\)-small everywhere.

We now turn to the interesting parts. The first one is that each \(\mathcal{F}_t\) is a formal solution of \(\mathcal{R}\). We already now that \(\mathcal{F}_t\) coincides with \(\mathcal{F}\), which is a formal solution, outside of the compact set \(K_1\). We set

Since \(\mathcal{R}\) is open, and \(K_1 × [0, 1]\) is compact and \(\mathcal{F}_t\) is within \(O\left(1/N\right)\) of \(\mathcal{F}'_t\), it suffices to prove that \(\mathcal{F}'_t\) is a formal solution for all \(t\). This is guaranteed by the definition of the slice \(\mathcal{R}(\mathcal{F}(x), π, v)\) to which \(γ^{tρ(x)}_x(Nπ(x))\) belongs.

Finally, let’s prove that \(\mathcal{F}_1\) is \(E' ⊕ ℝv\)–holonomic near \(K_0\). Since \(ρ = 1\) near \(K_0\), we have, for \(x\) near \(K_0\),

and

Let \(p\) be the projection of \(E\) onto \(\ker π\) along \(v\), so that \(\operatorname{Id}_E = p + v ⊗ π\). We can rewrite the above formulas as

and

So we see the difference is \(Df(x) ∘ p - φ(x) ∘ p\) which vanishes on \(E'\) since \(\mathcal{F}\) is \(E'\)–holonomic near \(K_0\), and vanishes on \(v\) since \(p(v) = 0\).

Let \(F\) be subspace of \(E\) with codimension at least \(2\). Let \(F'\) be a complement subspace. Its dimension is at least \(2\) since it is isomorphic to \(E/F\) and \(\dim (E/F) = \operatorname{codim}(F) ≥ 2\). First note the complement of \(F\) is path-connected. Indeed let \(x\) and \(y\) be points outside \(F\). Decomposing on \(F ⊕ F'\), we get \(x = u + u'\) and \(y = v + v'\) with \(u' ≠ 0\) and \(v' ≠ 0\). The segments from \(x\) to \(u'\) and \(y\) to \(v'\) stay outside \(F\), so it suffices to connect \(u'\) and \(v'\) in \(F' ∖ \{ 0\} \). If the segment from \(u'\) to \(v'\) doesn’t contains the origin then we are done. Otherwise \(v' = μu'\) for some (negative) \(u'\). Since \(\dim (F') ≥ 2\) and \(u' ≠ 0\), there exists \(f ∈ F'\) which is linearly independent from \(u'\), hence from \(v'\). We can then connect both \(u'\) and \(v'\) to \(f\) by a segment away from zero.

We now turn to ampleness. The connectedness result reduces to prove that every \(e\) in \(E\) is in the convex hull of \(E ∖ F\). If \(e\) is not in \(F\) then it is the convex combination of itself with coefficient \(1\) and we are done. Now assume \(e\) is in \(F\). The codimension assumption guarantees the existence of a subspace \(G\) such that \(\dim (G) = 2\) and \(G ∩ F = \{ 0\} \). Let \((g_1, g_2)\) be a basis of \(G\). We set \(p_1 = e + g_1\), \(p_2 = e + g_2\), \(p_3 = e - g_1 - g_2\). All these points are in \(E ∖ F\) and \(e = p_1/3 + p_2/3 + p_3/3\).

This is a straightforward induction using lemma 2.11. Let \((e_1, \dots , e_n)\) be a basis of \(E\), and let \((π_1, \dots , π_n)\) be the dual basis. Let \(E'_i\) be the linear subspace of \(E\) spanned by \((e_1, \dots , e_i)\), for \(1 ≤ i ≤ n\), and let \(E'_0\) be the zero subspace of \(E\). Each \((π_i, e_i)\) is a dual pair and the kernel of \(π_i\) contains \(E'_{i - 1}\).

Lemma 2.11 allows to build a sequence of homotopies of formal solutions, each homotopy relating a formal solution which is \(E'_i\)–holonomic to one which is \(E'_{i+1}\)–holonomic (always near \(K_0\)). The shortness condition is always satisfies because \(\mathcal{R}\) is ample. Each homotopy starts where the previous one stopped, stay at \(C^0\) distance at most \(ε/n\), and is relative to \(C\) and the complement of \(K_1\).

It then suffices to do a smooth concatenation of theses homotopies. We first pre-compose with a smooth map from \([0, 1]\) to itself that fixes \(0\) and \(1\) and has vanishing derivative to all orders at \(0\) and \(1\). Then we precompose by affine isomorphisms from \([0, 1]\) to \([i/n, (i + 1)/n]\) before joining them.