Home

Formalization status

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:

    1. $\mathcal{F}_0 = \mathcal{F}$ ;

    2. $\mathcal{F}_t$ is a formal solution of $\mathcal{R}$ over $U$ for all $t$ ;

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

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

    5. $\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:

    1. $\mathcal{F}_0 = \mathcal{F}$

    2. $\mathcal{F}_t$ is a formal solution of $\mathcal{R}$ over $U$ for all $t$ ;

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

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

    5. $\mathcal{F}_1$ is holonomic near $K_0$.

  • Lemma 2.3 (prop:theilliere)

    The corrugated function $f’$ satisfies, uniformly in $x$:

    1. $Df’(x)v = γ(x, Nπ(x)) + O\left(\frac1N\right)$, and the error vanishes whenever $γ_x$ is constant.

    2. $Df’(x)w = Df(x)w + O\left(\frac1N\right)$ for $w ∈ \ker π$

    3. $f’(x) = f(x) + O\left(\frac1N\right)$

    4. $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 pull-back 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:h-princ)

    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$,

    1. $j^1f$ is smooth

    2. $j^1f$ is a section of $J^1(M, N) → M$

    3. $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 pull-back 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$:

    1. $Df’(x)v = γ(x, Nπ(x)) + O\left(\frac1N\right)$, and the error vanishes whenever $γ_x$ is constant.

    2. $Df’(x)w = Df(x)w + O\left(\frac1N\right)$ for $w ∈ \ker π$

    3. $f’(x) = f(x) + O\left(\frac1N\right)$

    4. $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$.