Completion report
Click chapter titles to see missing items.Introduction 100%
1 Loops 40%

Lemma 1.11 (lem:local_loops)
Assume \(Ω\) is open and connected over some neighborhood of \(x_0\). If \(g(x)\) is the convex hull of \(Ω_x\) for \(x\) near \(x_0\) then there is a continuous family of loops defined near \(x_0\), based at \(β\), taking value in \(Ω\) and surrounding \(g\).

Lemma 1.12 (lem:satisfied_or_refund)
Each \(\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)\).

Corollary 1.13 (cor:extend_loops)
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 \(U ∈ 𝓝(K_0 ∪ K_1)\) and there exists \(γ ∈ \operatorname{\mathcal{L}}(U, g, β)\) which coincides with \(γ_0\) near \(K_0\).

Lemma 1.14 (lem:∃_surrounding_loops)
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 \(U\) and agrees with \(γ\) near \(K\).

Lemma 1.15 (lem:reparametrization)
Let \(γ \! :E × 𝕊^1 → F\) be a smooth family of loops surrounding a map \(g\) with base \(β\) over some \(U ⊆ E\). There is a family of circle diffeomorphisms \(φ : U × 𝕊^1 → 𝕊^1\) such that each \(γ_x ∘ φ_x\) has average \(g(x)\) and \(φ_x(0) = 0\).

Proposition 1.2 (prop:loops)
Let \(U\) be an open set in \(E\) and \(K ⊆ U\) a compact subset. Let \(Ω\) be a set in \(E × F\) such that, for each \(x\) in \(U\), \(Ω_x := Ω ∩ (\{ x\} × F)\) is open and connected.
Let \(β\) and \(g\) be maps from \(E\) to \(F\) that are smooth on \(U\). Assume that \(β(x) ∈ Ω_x\) for all \(x\) in \(U\), and \(g(x) = β(x)\) near \(K\).
If, for every \(x\) in \(U\), \(g(x)\) is in the convex hull of \(Ω_x\), then there exists a smooth family of loops
\[ γ \! :E × [0, 1] × 𝕊^1 → F, (x, t, s) ↦ γ^t_x(s) \]such that, for all \(x\) in \(U\), and all \((t, s) ∈ [0, 1] × 𝕊^1\)
\(γ^t_x(s) ∈ Ω_x\)
\(γ^0_x(s) = β(x)\)
\(\barγ^1_x = g(x)\)
\(γ^t_x(s) = β(x)\) if \(x\) is near \(K\).

Lemma 1.4 (lem:refined_caratheodory)
If a point \(x\) of \(E\) lies in the convex hull of a set \(P\), then \(x\) can be written as the convex combination of at most \(d + 1\) affinely independent points in \(P\) with positive coefficients.

Lemma 1.6 (lem:int_cvx)
If a point \(x\) of \(E\) lies in the convex hull of an open set \(P\), then it is surrounded by some collection of points belonging to \(P\).

Lemma 1.7 (lem:smooth_barycentric_coord)
For every \(x\) in \(E\) and every collection of points \(p ∈ E^{d+1}\) surrounding \(x\), there is a neighborhood \(U\) of \(\{ (x, p)\} \) and a function \(w : E × E^{d+1} → ℝ^{d+1}\) such that, for every \((y, q)\) in \(U\),
\(w\) is smooth at \((y, q)\)
\(w(y, q) ∈ (0, 1)\)
\(y = \sum _{i=0}^d w_i(y, q)q_i\)
2 Local theory of convex integration 37%

Definition 2.10 (def:short_formal_sol)
A formal solution \(\mathcal{F}\) of \(\mathcal{R}\) over \(U\) is \((π, v)\)–short if, for every \(x\) in \(U\), \(Df(x)v\) belonds to the interior of the convex hull of \(\mathcal{R}((x, f(x), φ(x)), π, v)\).

Lemma 2.11 (lem:integration_step)
Let \(\mathcal{F}\) be a formal solution of \(\mathcal{R}\) over an open set \(U\). Let \(K_1 ⊂ U\) be a compact subset, and let \(K_0\) be a compact subset of the interior of \(K_1\). Let \(C\) be a subset of \(U\). Let \(E'\) be a linear subspace of \(E\) contained in \(\ker π\). Let \(ε\) be a positive real number.
Assume \(\mathcal{R}\) is open over \(U\). Assume that \(\mathcal{F}\) is \(E'\)–holonomic near \(K_0\), \((π, v)\)–short over \(U\), 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}\) over \(U\) 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\).

Lemma 2.13 (lem:ample_codim_two)
The complement of a linear subspace of codimension at least 2 is ample.

Definition 2.14 (def:ample_relation_loc)
A first order differential relation \(\mathcal{R}\) is ample if all its slices are ample.

Lemma 2.15 (lem:open_ample_immersion_loc)
The relation of immersions in positive codimension is open and ample.

Lemma 2.16 (lem:h_principle_open_ample_loc)
Let \(\mathcal{F}\) be a formal solution of \(\mathcal{R}\) over an open set \(U\). Let \(K_1 ⊂ U\) 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 subset \(C\) of \(U\). Let \(ε\) be a positive real number.
If \(\mathcal{R}\) is open and ample over \(U\) 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}\) over \(U\) 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\).

Lemma 2.3 (prop:theilliere)
The corrugated function \(f'\) satisfies, uniformly in \(x\):
\(Df'(x)v = γ(x, Nπ(x)) + O\left(\frac1N\right)\), and the error vanishes whenever \(γ_x\) is constant.
\(Df'(x)w = Df(x)w + O\left(\frac1N\right)\) for \(w ∈ \ker π\)
\(f'(x) = f(x) + O\left(\frac1N\right)\)
\(f'(x) = f(x)\) whenever \(γ_x\) is constant.

Definition 2.7 (def:htpy_formal_sol_loc)
A homotopy of formal solutions over \(U\) is a map \(\mathcal{F}: ℝ × E → F × \operatorname{Hom}(E, F)\) which is smooth over \([0, 1] × U\) and such that each \(x ↦ \mathcal{F}(t, x)\) is a formal solution over \(U\) when \(t\) is in \([0, 1]\).

Definition 2.8 (def:rel_slice)
For every \(σ = (x, y, φ)\), the slice of \(\mathcal{R}\) at \(σ\) with respect to \((π, v)\) is:
\[ \mathcal{R}(σ, π, v) = \operatorname{Conn}_{φ(v)}\{ w ∈ F \; \; (x, y, φ + (w  φ(v)) ⊗ π) ∈ \mathcal{R}\} . \] 
Lemma 2.9 (lem:update_lin_map)
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}\} \).
3 Global theory of open and ample relations 0%

Definition 3.1 (def:pull_back_bundle)
For every bundle \(p : E → B\) and every map \(f \! :B' → B\), the pullback bundle \(f^*E → B'\) is defined by \(f^*E = \{ (b', e) ∈ B' × E \; \; p(e) = f(b')\} \) with the obvious projection to \(B'\).

Definition 3.10 (def:hprinc)
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 with boundary \(P\), every family \(\mathcal{F}: P × M → J^1(M, N)\) of formal solutions which are holonomic for \(p\) in \(𝓝(∂P)\) is homotopic to a family of holonomic ones relative to \(𝓝(∂P)\). It satisfies the parametric \(h\)principle if, for every manifold with boundary \(P\), every family \(\mathcal{F}: P × M → J^1(M, N)\) of formal solutions is homotopic to a family of holonomic ones.

Lemma 3.11 (lem:sol_chart)
The above definitions translate to the definitions of the previous chapter in local charts. (We’ll need more precise statements...)

Lemma 3.12 (lem:param_trick)
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})\).

Lemma 3.13 (lem:param_for_free)
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}\).

Definition 3.14 (def:ample_relation)
A relation \(\mathcal{R}\) is ample if, for every \(σ = (x, y, φ)\) in \(\mathcal{R}\) and every \((λ, v)\), the slice \(\mathcal{R}_{σ, λ, v}\) is ample in \(T_yY\).

Lemma 3.15 (lem:ample_iff_loc)
If a relation is ample then it is ample if the sense of Definition 2.14 when seen in local charts.

Lemma 3.16 (lem:open_ample_immersion)
The relation of immersions of \(M\) into \(N\) in positive codimension is open and ample.

Theorem 3.17 (thm:open_ample)
If \(\mathcal{R}\) is open and ample then it satisfies the relative and parametric \(C^0\)dense \(h\)principle.

Lemma 3.18 (lem:ample_parameter)
If \(\mathcal{R}\) is ample then, for any parameter space \(P\), \(\mathcal{R}^P\) is also ample.

Theorem 3.19 (thm:sphere_eversion)
There is a homotopy of immersions of \(𝕊^2\) into \(ℝ^3\) from the inclusion map to the antipodal map \(a : q ↦ q\).

Definition 3.2 (def:hom_bundle)
Let \(E → B\) and \(F → B\) be two vector bundles over some smooth manifold \(B\). The bundle \(\operatorname{Hom}(E, F) → B\) is the set of linear maps from \(E_b\) to \(F_b\) for some \(b\) in \(B\), with the obvious project map.

Definition 3.3 (def:one_jet_space)
Let \(M\) and \(N\) be smooth manifolds. Denote by \(p_1\) and \(p_2\) the projections of \(M × N\) to \(M\) and \(N\) respectively.
The space \(J^1(M, N)\) of \(1\)jets of maps from \(M\) to \(N\) is \(Hom(p_1^*TM, p_2^*TN)\)

Definition 3.4 (def:one_jet_extension)
The \(1\)jet of a smooth map \(f \! :M → N\) is the map from \(m\) to \(J^1(M, N)\) defined by \(j^1f(m) = (m, f(m), T_mf)\).

Lemma 3.5 (lem:one_jet_extension_prop)
For every smooth map \(f \! :M → N\),
\(j^1f\) is smooth
\(j^1f\) is a section of \(J^1(M, N) → M\)
\(j^1f\) composed with \(J^1(M, N) → N\) is \(f\).

Definition 3.6 (def:holonomic_section)
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}\).

Definition 3.7 (def:rel)
A first order differential relation for maps from \(M\) to \(N\) is a subset \(\mathcal{R}\) of \(J^1(M, N)\).

Definition 3.8 (def:formal_sol)
A formal solution of a differential relation \(\mathcal{R}⊆ J^1(M, N)\) is a section of \(J^1(M, N) → M\) taking values in \(\mathcal{R}\). A solution of \(\mathcal{R}\) is a map from \(M\) to \(N\) whose \(1\)–jet extension is a formal solution.

Definition 3.9 (def:htpy_formal_sol)
A homotopy of formal solutions of \(\mathcal{R}\) is a family of sections \(\mathcal{F}: ℝ × M → J^1(M, N)\) which is smooth over \([0, 1] × M\) and such that each \(m ↦ \mathcal{F}(t, m)\) is a formal solution when \(t\) is in \([0, 1]\).
What to define next?
2 Local theory of convex integration

Definition 2.10 (def:short_formal_sol)
A formal solution \(\mathcal{F}\) of \(\mathcal{R}\) over \(U\) is \((π, v)\)–short if, for every \(x\) in \(U\), \(Df(x)v\) belonds to the interior of the convex hull of \(\mathcal{R}((x, f(x), φ(x)), π, v)\).

Definition 2.7 (def:htpy_formal_sol_loc)
A homotopy of formal solutions over \(U\) is a map \(\mathcal{F}: ℝ × E → F × \operatorname{Hom}(E, F)\) which is smooth over \([0, 1] × U\) and such that each \(x ↦ \mathcal{F}(t, x)\) is a formal solution over \(U\) when \(t\) is in \([0, 1]\).

Definition 2.8 (def:rel_slice)
For every \(σ = (x, y, φ)\), the slice of \(\mathcal{R}\) at \(σ\) with respect to \((π, v)\) is:
\[ \mathcal{R}(σ, π, v) = \operatorname{Conn}_{φ(v)}\{ w ∈ F \; \; (x, y, φ + (w  φ(v)) ⊗ π) ∈ \mathcal{R}\} . \]
3 Global theory of open and ample relations

Definition 3.1 (def:pull_back_bundle)
For every bundle \(p : E → B\) and every map \(f \! :B' → B\), the pullback bundle \(f^*E → B'\) is defined by \(f^*E = \{ (b', e) ∈ B' × E \; \; p(e) = f(b')\} \) with the obvious projection to \(B'\).

Definition 3.14 (def:ample_relation)
A relation \(\mathcal{R}\) is ample if, for every \(σ = (x, y, φ)\) in \(\mathcal{R}\) and every \((λ, v)\), the slice \(\mathcal{R}_{σ, λ, v}\) is ample in \(T_yY\).

Definition 3.2 (def:hom_bundle)
Let \(E → B\) and \(F → B\) be two vector bundles over some smooth manifold \(B\). The bundle \(\operatorname{Hom}(E, F) → B\) is the set of linear maps from \(E_b\) to \(F_b\) for some \(b\) in \(B\), with the obvious project map.
What to state next?
1 Loops

Lemma 1.4 (lem:refined_caratheodory)
If a point \(x\) of \(E\) lies in the convex hull of a set \(P\), then \(x\) can be written as the convex combination of at most \(d + 1\) affinely independent points in \(P\) with positive coefficients.

Lemma 1.6 (lem:int_cvx)
If a point \(x\) of \(E\) lies in the convex hull of an open set \(P\), then it is surrounded by some collection of points belonging to \(P\).

Lemma 1.7 (lem:smooth_barycentric_coord)
For every \(x\) in \(E\) and every collection of points \(p ∈ E^{d+1}\) surrounding \(x\), there is a neighborhood \(U\) of \(\{ (x, p)\} \) and a function \(w : E × E^{d+1} → ℝ^{d+1}\) such that, for every \((y, q)\) in \(U\),
\(w\) is smooth at \((y, q)\)
\(w(y, q) ∈ (0, 1)\)
\(y = \sum _{i=0}^d w_i(y, q)q_i\)
2 Local theory of convex integration

Lemma 2.13 (lem:ample_codim_two)
The complement of a linear subspace of codimension at least 2 is ample.

Lemma 2.15 (lem:open_ample_immersion_loc)
The relation of immersions in positive codimension is open and ample.

Lemma 2.3 (prop:theilliere)
The corrugated function \(f'\) satisfies, uniformly in \(x\):
\(Df'(x)v = γ(x, Nπ(x)) + O\left(\frac1N\right)\), and the error vanishes whenever \(γ_x\) is constant.
\(Df'(x)w = Df(x)w + O\left(\frac1N\right)\) for \(w ∈ \ker π\)
\(f'(x) = f(x) + O\left(\frac1N\right)\)
\(f'(x) = f(x)\) whenever \(γ_x\) is constant.

Lemma 2.9 (lem:update_lin_map)
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}\} \).
3 Global theory of open and ample relations

Lemma 3.16 (lem:open_ample_immersion)
The relation of immersions of \(M\) into \(N\) in positive codimension is open and ample.

Theorem 3.19 (thm:sphere_eversion)
There is a homotopy of immersions of \(𝕊^2\) into \(ℝ^3\) from the inclusion map to the antipodal map \(a : q ↦ q\).
What to prove next?
1 Loops

Lemma 1.12 (lem:satisfied_or_refund)
Each \(\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)\).

Corollary 1.13 (cor:extend_loops)
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 \(U ∈ 𝓝(K_0 ∪ K_1)\) and there exists \(γ ∈ \operatorname{\mathcal{L}}(U, g, β)\) which coincides with \(γ_0\) near \(K_0\).

Lemma 1.14 (lem:∃_surrounding_loops)
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 \(U\) and agrees with \(γ\) near \(K\).

Proposition 1.2 (prop:loops)
Let \(U\) be an open set in \(E\) and \(K ⊆ U\) a compact subset. Let \(Ω\) be a set in \(E × F\) such that, for each \(x\) in \(U\), \(Ω_x := Ω ∩ (\{ x\} × F)\) is open and connected.
Let \(β\) and \(g\) be maps from \(E\) to \(F\) that are smooth on \(U\). Assume that \(β(x) ∈ Ω_x\) for all \(x\) in \(U\), and \(g(x) = β(x)\) near \(K\).
If, for every \(x\) in \(U\), \(g(x)\) is in the convex hull of \(Ω_x\), then there exists a smooth family of loops
\[ γ \! :E × [0, 1] × 𝕊^1 → F, (x, t, s) ↦ γ^t_x(s) \]such that, for all \(x\) in \(U\), and all \((t, s) ∈ [0, 1] × 𝕊^1\)
\(γ^t_x(s) ∈ Ω_x\)
\(γ^0_x(s) = β(x)\)
\(\barγ^1_x = g(x)\)
\(γ^t_x(s) = β(x)\) if \(x\) is near \(K\).