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:cont_convex_hull)
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 continuous 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 it 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:cont_convex_hull)
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 continuous 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$.