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: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:

    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 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:

    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: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\):

    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\).