- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the
*statement*of this result is ready to be formalized; all prerequisites are done - Orange border
- the
*statement*of this result is not ready to be formalized; the blueprint needs more work - Blue background
- the
*proof*of this result is ready to be formalized; all prerequisites are done - Green border
- the
*statement*of this result is formalized - Green background
- the
*proof*of this result is formalized - Dark green background
- the
*proof*of this result and all its ancestors are formalized

Let \(U_0\) and \(U_1\) be open sets in \(E\). Let \(K_0 ⊂ U_0\) and \(K_1 ⊂ U_1\) be compact subsets. For any \(γ_0 ∈ \operatorname{\mathcal{L}}(U_0, g, β, Ω)\) and \(γ_1 ∈ \operatorname{\mathcal{L}}(U_1, g, β, Ω)\), there exists a neighborhood \(U\) of \(K_0 ∪ K_1\) and there exists \(γ ∈ \operatorname{\mathcal{L}}(U, g, β, Ω)\) which coincides with \(γ_0\) near \(K_0\cup U_1^c\).

A continuous family of loops \(γ \! :E × [0, 1] × 𝕊^1 → F, (x, t, s) ↦ γ^t_x(s)\) surrounds a map \(g \! :E → F\) with base \(β \! :E → F\) on \(U ⊂ E\) in \(Ω ⊂ E × F\) if, for every \(x\) in \(U\), every \(t ∈ [0, 1]\) and every \(s ∈ 𝕊^1\),

\(γ^t_x\) is based at \(β(x)\)

\(γ^0_x(s) = β(x)\)

\(γ^1_x\) surrounds \(g(x)\)

\((x,γ^t_x(s)) ∈ Ω\).

The space of such families will be denoted by \(\operatorname{\mathcal{L}}(g, β, U, Ω)\).

Let \(X\) be a topological space, \(x\) a point in \(X\) and \(Y\) a set. A germ of function from \(X\) to \(Y\) at \(x\) is an element of the quotient \((X → Y)_x\) of the set of functions from \(X\) to \(Y\) by the relation \(f ∼ g\) if \(f\) and \(g\) coincide near \(x\). The image of a function \(f\) in this quotient will be denoted by \([f]_x\).

A local predicate on functions from \(X\) to \(Y\) is a family \(P\) of predicates on the germ set \((X → Y)_x\) for every \(x\) in \(X\). We say that a function \(f\) satisfies \(P\) at \(x\) if \(P [f]_x\) holds, and \(f\) satisfies \(P\) if it satisfies \(P\) at every point.

A first order differential relation \(\mathcal{R}⊂ J^1(M, N)\) satisfies the \(h\)-principle if every formal solution of \(\mathcal{R}\) is homotopic to a holonomic one. It satisfies the parametric \(h\)-principle if, for every manifold \(P\) and every closed set \(C\) in \(P × M\), every family \(\mathcal{F}: P × M → J^1(M, N)\) of formal solutions which are holonomic for \((p, m)\) near \(C\) is homotopic to a family of holonomic ones relative to \(C\).

A section \(\mathcal{F}\) of \(J^1(M, N) → M\) is called holonomic if it is the \(1\)–jet of its base map. Equivalently, \(\mathcal{F}\) is holonomic if there exists \(f \! :M → N\) such that \(\mathcal{F}= j^1f\), since such a map is necessarily \(\operatorname{bs}\mathcal{F}\).

Let \(f : M → N\) be a continuous map between manifolds. A localisation data for \(f\) is a tuple \((E, F, N, ι, φ, ψ, j)\) where \(E\) and \(F\) are normed vector spaces, \(N\) is a natural number, \(ι\) is a set, \(φ : \mathcal{I}_{N} × E → M\) and \(ψ : ι × F → N\) are families of smooth open embeddings, and \(j : \mathcal{I}_{N} → ι\) such that:

\(⋃_i φ_i(B_E) = M\) where \(B_E\) is the open unit ball in \(E\),

\(⋃_i ψ_i(B_F) = N\) where \(B_F\) is the open unit ball in \(F\),

\(∀ i, f(φ_i(E)) ⊂ ψ_{j(i)}(B_F)\) where \(B_F\) is the open unit ball in \(F\),

\(i \mapsto ψ_i(F)\) is locally finite.

Such a tuple will be denoted by \((φ, ψ, j)\) for brevity.

A loop is a map defined on the circle \(𝕊^1 = ℝ/ℤ\) with values in a finite-dimensional vector space. It can also freely be seen as \(1\)-periodic maps defined on \(ℝ\).

The average of a loop \(γ\) is \(\barγ := \int _{𝕊^1} γ(s)\, ds\).

The *support* of a family \(γ\) of loops in \(F\) parametrized by \(E\) is the closure of the set of \(x\) in \(E\) such that \(γ_x\) is not a constant loop.

Let \(X\) be a topological space, \(A\) a subset of \(X\), \(Y\) a set and \(P\) a local predicate on functions from \(X\) to \(Y\). The restriction of \(P\) to \(A\) is the local predicate \(P_{|A}\) defined by the constraint that a function \(f\) satisfies \(P_{|A}\) at \(x\) if \(x ∈ A\) implies that \(f\) satisfies \(P\) near \(x\).

Given manifolds \(M\), \(X\), \(N\) and \(Y\) and smooth open embeddings \(g : Y → N\) and \(h : X → M\) we get a transfer map \(ψ_{g, h} : J^1(X, Y) → J^1(M, N)\) defined by

and an operator on sections which sends \(\mathcal{F}: M → J^1(M, N)\) to \(Ψ_{g, h}\mathcal{F}: X → J^1(X, Y)\) defined when \(\operatorname{bs}\mathcal{F}(h(X)) ⊂ g(Y)\) by

Given a relation \(\mathcal{R}⊂ J^1(M, N)\), the induced relation in \(J^1(X, Y)\) is \(ψ_{g, h}⁻¹\mathcal{R}\).

Given manifolds \(W\), \(X\), \(Y\) and \(Z\) and smooth open embeddings \(g : Z → Y\) and \(h : W → X\), the relation induced (in the sense of Definition 3.18) in \(J^1(W, Z)\) by an ample relation in \(J^1(X, Y)\) is ample.

Let \(φ : X → M\) and \(ψ : Y → N\) be smooth open embeddings. Let \(K_X\) and \(K_P\) be compact sets in \(X\) and \(P\). Let \(f : P × M → N\) be a continuous family of maps such that, for each \(p\), \(f_p(φ(X)) ⊂ ψ(Y)\). For every continuous function \(ε : M → ℝ_{{\gt} 0}\), there is some positive number \(η\) such that, for every map \(g : P × X → Y\) and every \((p, p', x)\) in \(K_P × K_P × K_X\), \(d(g_{p'}(x), ψ⁻¹∘f_p∘φ(x)) {\lt} η\) implies \(d(f'_{p'}(φ(x)), f_p(φ(x))) {\lt} ε(φ(x))\) where \(f'\) is obtained by updating \(f\) using \(g\).

Let \(E\) and \(F\) be real normed vector spaces. Assume that \(E\) is finite dimensional. Let \(P\) be a predicate on \(E \times F\) such that for all \(x\) in \(E\), \(\{ y ~ |~ P (x, y) \} \) is convex. Let \(n\) be a natural number or \(+\infty \). Assume that every \(x\) has a neighbourhood \(U\) on which there exists a \(C^n\) function \(f\) such that \(\forall x ∈ U, P(x, f(x))\). Then there is a global \(C^n\) function \(f\) such that \(\forall x, P(x, f(x))\).

Let \(E₁\), \(E₂\) and \(F\) be real vector spaces. Assume \(E₁\) and \(E₂\) are finite dimensional. Let \(n\) be a natural number or \(+\infty \). Let \(P\) be a property of pairs \((x, f)\) with \(x ∈ E₁\) and \(f : E₂ → F\). Assume that, for every \(x\), the space of functions \(f\) such that \(P(x, f)\) holds is convex. Assume that for every \(x₀\) in \(E₁\) there is a neighborhood \(U\) of \(x₀\) and a function \(φ : E₁ × E₂ → F\) which is \(C^n\) on \(U × E₂\) and such that \(P(x, φ(x, \cdot ))\) holds for every \(x\) in \(U\). There there is a global \(C^n\) function \(φ \! :E₁ × E₂ → F\) such that \(P(x, φ(x, \cdot ))\) holds for every \(x\).

Let \(X\) be a topological space and let \(Y\) be any set. Let \(f\) be a sequence of functions from \(X\) to \(Y\) indexed by \(\mathcal{I}_{N}\) for some \(N\). Let \(V\) be a family of subsets of \(X\) indexed by \(\mathcal{I}_{N}\) such that, for every non-maximal \(n\), \(f_{S(n)}\) coincides with \(f_n\) outside \(V_{S(n)}\). If \(V\) is locally finite then there exists \(F \! :X → Y\) such that, for every \(x\) and every sufficiently large \(n\), \(F\) coincides with \(f_n\) near \(x\).

Let \(X\) be a metrizable locally compact second countable topological space. Let \(C\) be a closed subset in \(X\). Let \(P\) be a non-decreasing predicate on subsets of \(X\) (meaning that if \(U ⊂ V\) and \(V\) satisfies \(P\) then so does \(U\)). Assume the empty set satisfies \(P\) and every point in \(C\) has a neighborhood in \(X\) satisfying \(P\). Then there exist sequences of subsets \(K\) and \(W\) indexed by natural numbers such that \(K\) covers \(C\), \(W\) is locally finite and, for every \(n\) :

\(K_n\) is compact

\(W_n\) is open

\(K_n ⊂ W_n\)

\(W_n\) satisfies \(P\).

Let \(\mathcal{F}\) be a formal solution of \(\mathcal{R}\). Let \(K_1 ⊂ E\) be a compact subset, and let \(K_0\) be a compact subset of the interior of \(K_1\). Assume \(\mathcal{F}\) is holonomic near a closed subset \(C\) of \(E\). Let \(ε\) be a positive real number.

If \(\mathcal{R}\) is open and ample then there is a homotopy \(\mathcal{F}_t\) such that:

\(\mathcal{F}_0 = \mathcal{F}\)

\(\mathcal{F}_t\) is a formal solution of \(\mathcal{R}\) for all \(t\) ;

\(\mathcal{F}_t(x) = \mathcal{F}(x)\) for all \(t\) when \(x\) is near \(C\) or outside \(K_1\).

\(d(\operatorname{bs}\mathcal{F}_t(x), \operatorname{bs}\mathcal{F}(x)) ≤ ε\) for all \(t\) and all \(x\) ;

\(\mathcal{F}_1\) is holonomic near \(K_0\) ;

\(t ↦ F_t\) is constant near \(0\) and \(1\).

Let \(X\) be a topological space and \(Y\) be any set. Let \(U\) be a locally finite family of subsets of \(X\) indexed by some \(\mathcal{I}_{N}\). Let \(P₀\) be a local predicate on functions from \(X\) to \(Y\), let \(i ↦ P₁^i\) be a family of such predicates, and let \(i ↦ P₂^i\) be a family of predicates on functions from \(X\) to \(Y\), all families being indexed by \(\mathcal{I}_{N}\). Assume that

there exists \(f₀ \! :X → Y\) satisfying \(P₀\) and \(P₂^0\) ;

for every \(i\) in \(\mathcal{I}_{N}\) and every \(f \! :X → Y\) satisfying \(P₀\), \(P₂^i\) and every \(P₁^j\) for \(j {\lt} i\), there exists a function \(f' \! :X → Y\) which coincides with \(f\) outside \(U_i\) and satisfies \(P₀\) and every \(P₁^j\) for \(j ≤ i\) as well as \(P₂^{S(i)}\) unless \(i\) is maximal.

Then there exists \(f \! :X → Y\) which satisfies \(P₀\) and all \(P₁^i\)’s.

Let \(X\) a second countable locally compact metrizable topological space. Let \(P₀\), \(P₀'\) and \(P₁\) be local predicates on function from \(X\) to a set \(Y\). Let \(f₀ \! :X → Y\) be a function satisfying \(P₀\) and \(P₀'\). Assume that

For every \(x\) in \(X\), there exists a function \(f \! :X → Y\) which satisfies \(P₀\) and satisfies \(P₁\) near \(x\).

For every closed subsets \(K₁\) and \(K₂\) of \(X\) and every open subsets \(U₁\) and \(U₂\) containing \(K₁\) and \(K₂\), for every function \(f₁\) and \(f₂\) satisfying \(P₀\), if \(f₁\) satisfies \(P₀'\) and satisfies \(P₁\) on \(U₁\) and if \(f₂\) satisfies \(P₁\) on \(U₂\) then there exists \(f\) which satisfies \(P₀\) and \(P₀'\), and satisfies \(P₁\) near \(K₁ ∪ K₂\) and coincides with \(f₁\) near \(K₁ ∪ U₂^c\).

Then there exists \(f\) which satisfies \(P₀\), \(P₀'\) and \(P₁\).

Let \(X\) be a topological space and \(Y\) be any set. Let \(P₀\) and \(P₁\) be local predicates on maps from \(X\) to \(Y\). Let \(P₀'\) be a local predicate on maps from \(ℝ × X → Y\). Assume that for every \(a\), \(b\) and \(t\) in \(ℝ\), every \(x\) in \(X\) and every \(f \! :ℝ × X → Y\), if \(f\) satisfies \(P₂\) at \((at + b, x)\) then \((t, x) ↦ f(at+b, x)\) satisfies \(P₀'\) at \((t, x)\). Let \(f₀ \! :X → Y\) be a function satisfying \(P₀\) and such that \((t, x) ↦ f₀(x)\) satisfies \(P₀'\).

Let \(K\) and \(U\) be families of subsets of \(X\) indexed by some \(\mathcal{I}_{N}\). Assume that \(U\) is locally finite and \(K\) covers \(X\).

Assume that, for every \(i\) in \(\mathcal{I}_{N}\) and every \(f \! :X → Y\) satisfying \(P₀\) and satisfying \(P₁\) on \(\bigcup _{j {\lt} i} K_j\), there exists \(F \! :ℝ × X → Y\) such that

for all \(t\), \(F(t, \cdot )\) satisfies \(P₀\)

\(F\) satisfies \(P₀'\)

\(F(1, \cdot )\) satisfies \(P₁\) on \(\bigcup _{j ≤ i} K_j\)

\(F(t, x) = f(x)\) whenever \(x\) is not in \(U_i\) or \(t\) is near \((-∞, 0]\)

\(F(t, x) = F(1, x)\) whenever \(t\) is near \([1, +∞)\).

Then there exists \(F \! :ℝ × X → Y\) such that

for all \(t\), \(F(t, \cdot )\) satisfies \(P₀\)

\(F\) satisfies \(P₀'\)

\(F(0, \cdot ) = f₀\)

\(F(1, \cdot )\) satisfies \(P₁\).

Given a point \(c\) of \(E\) and a real number \(t\), let:

be the homothety which dilates about \(c\) by a scale of \(t\).

Suppose \(c\) belongs to the interior of a convex subset \(C\) of \(E\) and \(t {\gt} 1\), then

Let \(\mathcal{F}\) be a formal solution of \(\mathcal{R}\). Let \(K_1 ⊂ E\) be a compact subset, and let \(K_0\) be a compact subset of the interior of \(K_1\). Let \(C\) be a closed subset of \(E\). Let \(E'\) be a linear subspace of \(E\) contained in \(\ker π\). Let \(ε\) be a positive real number.

Assume \(\mathcal{R}\) is open. Assume that \(\mathcal{F}\) is \(E'\)–holonomic near \(K_0\), \((π, v)\)–short, and holonomic near \(C\). Then there is a homotopy \(\mathcal{F}_t\) such that:

\(\mathcal{F}_0 = \mathcal{F}\) ;

\(\mathcal{F}_t\) is a formal solution of \(\mathcal{R}\) for all \(t\) ;

\(\mathcal{F}_t(x) = \mathcal{F}(x)\) for all \(t\) when \(x\) is near \(C\) or outside \(K_1\) ;

\(d(\operatorname{bs}\mathcal{F}_t(x), \operatorname{bs}\mathcal{F}(x)) ≤ ε\) for all \(t\) and all \(x\) ;

\(\mathcal{F}_1\) is \(E' ⊕ ℝv\)–holonomic near \(K_0\).

Let \(f : M → N\) be a continuous map between manifolds, and let \((φ, ψ, i)\) be some localisation data for \(f\). There exists a continuous positive function \(ε : M → ℝ_{{\gt}0}\) such that:

If a vector \(v\) is in the convex hull of a connected open subset \(O\) then, for every base point \(b ∈ O\), there is a continuous family of loops \(γ \! :[0, 1] × 𝕊^1 → E, (t, s) ↦ γ^t(s)\) such that, for all \(t\) and \(s\):

\(γ^t\) is based at \(b\)

\(γ^0(s) = b\)

\(γ^t(s) ∈ O\)

\(γ^1\) surrounds \(v\)

Let \(M\) be a manifold modelled on the normed space \(E\) and \((V_j)_{j ∈ J}\) a cover of \(M\) by open sets. There exists some natural number \(N\) and a family of smooth open embeddings \(φ : \mathcal{I}_{N} × E → M\) such that

for each \(i\) there is some \(j\) such that \(φ_i(E) \subseteq V_j\),

\(i ↦ φ_i(E)\) is a locally-finite collection of sets in \(M\),

\(⋃_i φ_i(B_E(0, 1)) = M\) where \(B_E(0, 1)\) is the open unit ball in \(E\).

Let \(\mathcal{R}\) be a first order differential relation for maps from \(M\) to \(N\). If, for every manifold with boundary \(P\), \(\mathcal{R}^P\) satisfies the \(h\)-principle then \(\mathcal{R}\) satisfies the parametric \(h\)-principle. Likewise, the \(C^0\)-dense and relative \(h\)-principle for all \(\mathcal{R}^P\) imply the parametric \(C^0\)-dense and relative \(h\)-principle for \(\mathcal{R}\).

In the above setup, we have:

\(\bar F\) is holonomic at \((x, p)\) if and only if \(F_p\) is holonomic at \(x\).

\(F\) is a family of formal solutions of some \(\mathcal{R}⊂ J^1(X, Y)\) if and only if \(\bar F\) is a formal solution of \(\mathcal{R}^P := Ψ^{-1}(\mathcal{R})\).

Let \(X\) a second countable locally compact metrizable topological space. Let \(P₀\) and \(P₁\) be local predicates on functions from \(X\) to a set \(Y\). Let \(K\) be a closed subset of \(X\). Let \(f₀ \! :X → Y\) be a function satisfying \(P₀\) and satisfying \(P₁\) near \(K\). Assume that

For every \(x\) in \(X\), there exists a function \(f \! :X → Y\) which satisfies \(P₀\) and satisfies \(P₁\) near \(x\).

For every closed subsets \(K₁\) and \(K₂\) of \(X\) and every open subsets \(U₁\) and \(U₂\) containing \(K₁\) and \(K₂\), for every function \(f₁\) and \(f₂\) satisfying \(P₀\), if \(f₁\) satisfies \(P₁\) on \(U₁\) and if \(f₂\) satisfies \(P₁\) on \(U₁\) then there exists \(f\) which satisfies \(P₀\), and satisfies \(P₁\) near \(K₁ ∪ K₂\) and coincides with \(f₁\) near \(K₁ ∪ U₂^c\).

Then there exists \(f\) which satisfies \(P₀\) and \(P₁\) and coincides with \(f₀\) near \(K\).

For every set \(U ⊂ E\), \(\operatorname{\mathcal{L}}(g, β, U, Ω)\) is “path connected”: for every \(γ_0\) and \(γ_1\) in \(\operatorname{\mathcal{L}}(g, β, U, Ω)\), there is a continuous map \(δ \! :[0, 1] × E × [0, 1] × 𝕊^1 → F, (τ, x, t, s) ↦ δ^t_{τ, x}(s)\) which interpolates between \(γ_0\) and \(γ_1\) in \(\operatorname{\mathcal{L}}(g, β, U, Ω)\).

For every \(x\) in \(E\) and every collection of points \(p ∈ E^{d+1}\) surrounding \(x\), there is a function \(w \! :E × E^{d+1} → ℝ^{d+1}\) such that, for every \((y, q)\) in a neighborhood of \((x, p)\),

\(w\) is smooth at \((y, q)\)

\(w(y, q) {\gt} 0\)

\(\sum _{i=0}^d w_i(y, q) = 1\)

\(y = \sum _{i=0}^d w_i(y, q)q_i\).

Let \(φ : P × X → M\) and \(ψ : P × Y → N\) be families of smooth open embeddings. Let \(K\) be a set in \(X\) whose image in \(M\) is closed. Let \(f : P × M → N\) and \(g : P × X → Y\) be smooth families of maps. If for each \(p\) and for every \(x\) not in \(K\), \(f_p(φ(x)) = ψ(g_p(x))\) then the family of maps \(f_p\) updated using \(g_p\) is smooth from \(P × M\) to \(N\).

In a metric space \(X\), let \(U : ι → \operatorname{\mathcal{P}}{X}\) be a family of open subsets of \(X\) and let \(K : ι → \operatorname{\mathcal{P}}{X}\) be a locally-finite family of closed subsets such that \(K_i ⊂ U_i\) for all \(i\). There exists a continuous function \(δ : X → ℝ_{{\gt} 0}\) such that:

In the situation of the previous definition, given a section \(\mathcal{F}: M → J^1(M, N)\):

\(Ψ_{g, h}(\mathcal{F})\) is a smooth section of \(J^1(X, Y)\).

\(\mathcal{F}\) is holonomic on \(s ⊂ h(X) ∩ \operatorname{bs}\mathcal{F}⁻¹(g(Y))\) if and only if \(Ψ_{g, h}(\mathcal{F})\) is holonomic on \(h⁻¹(s)\).

\(\mathcal{F}\) is a formal solution of \(\mathcal{R}\) on \(h(X) ∩ \operatorname{bs}\mathcal{F}⁻¹(g(Y)\) if and only if \(Ψ_{g, h}(\mathcal{F})\) is a formal solution of the induced relation \(Ψ_{g, h}⁻¹\mathcal{R}\).

The linear map \(φ + (w - φ(v)) ⊗ π)\) coincides with \(φ\) on \(\ker π\) and sends \(v\) to \(w\). If \(\sigma \) belongs to \(\mathcal{R}\) then \(φ(v)\) belongs to \(\{ w ∈ F, (x, y, φ + (w - φ(v)) ⊗ π) ∈ \mathcal{R}\} \).

In the setup of Proposition 1.2, assume we have a continuous family \(γ\) of loops defined near \(K\) which is based at \(β\), surrounds \(g\) and such that each \(γ_x^t\) takes values in \(Ω_x\). Then there such a family which is defined on all of \(E\) and agrees with \(γ\) near \(K\).

Let \(f\) be a \(\mathcal{C}^1\) function from \(E\) to \(F\). Let \((π, v)\) be a dual pair on \(E\). Let \(γ \! :E × 𝕊^1 → F\) be a \(\mathcal{C}^1\) family of loops such that \(\overline{γ_x} = Df(x)v\) for all \(x\).

For any compact set \(K ⊂ E\) and any positive \(ε\), the function \(f'\) obtained by corrugation of \(f\) in direction \((π, v)\) using \(γ\) with large enough oscillation number \(N\) satisfies:

\(∀ x ∈ K, ‖f'(x) - f(x)‖ ≤ ε\)

\(∀ x ∈ K, ‖(Df'(x) - Df(x))_{|\ker π}‖ ≤ ε\).

\(∀ x ∈ K, ‖Df'(x)v - γ(x, Nπ(x))‖ ≤ ε\)

In addition, all the differences estimated above vanish if \(x\) is outside the support of \(γ\).

Let \(K\) a compact set in \(E\). Let \(Ω\) be an open set in \(E × F\).

Let \(β\) and \(g\) be smooth maps from \(E\) to \(F\). Write \(Ω_x := \{ y ∈ F \mid (x, y) ∈ Ω\} \), assume that \(β(x) ∈ Ω_x\) for all \(x\), and that \(g(x) = β(x)\) near \(K\).

If, for every \(x\), \(g(x)\) is in the convex hull of the connected component of \(Ω_x\) containing \(β(x)\), then there exists a smooth family of loops

such that, for all \(x ∈ E\), all \(t ∈ ℝ\) and all \(s ∈ 𝕊^1\),

\(γ^t_x(s) ∈ Ω_x\)

\(γ^0_x(s) = γ^t_x(1) = β(x)\)

\(\barγ^1_x = g(x)\)

\(γ^t_x(s) = β(x)\) if \(x\) is near \(K\).