Gromov's theorem

Stream: sphere eversion

[Floris van Doorn]

I modified the statement of the h-principle so that it is relative and C^0-dense. Does this seem right?
In particular: do we want to be relative to a specified closed set in the domain M and a specified closed set in the parameter space P?

/-- An arbitrary distance on `J¹(M, M')`. -/
@[reducible] def some_dist : has_dist (one_jet_bundle I M I' M') :=
-- some garbage; obtained from metrizability

/-- A relation `R` satisfies the parametric relative C⁰-dense h-principle w.r.t. manifold `P`,
`C₁ ⊆ P`, `C₂ ⊆ M` and `ε : M → ℝ` if for every family of
formal solutions `𝓕₀` indexed by a manifold with boundary `P` that is holonomic near `C₁` and `C₂`,
there is a homotopy `𝓕` between `𝓕₀` and a holonomic solution,
in such a way that `𝓕` is constant near `C₁` and `C₂` and `ε`-close to `𝓕₀`.
Note: `ε`-closeness is measured using an arbitrary distance function obtained from the metrizability
of `J¹(M, M')`. Potentially we prefer to have this w.r.t. an arbitrary compatible metric.
-/
def rel_mfld.satisfies_h_principle_with (R : rel_mfld I M I' M') (C₁ : set P) (C₂ : set M)
  (ε : M → ℝ) : Prop :=
∀ 𝓕₀ : family_formal_sol IP P R, -- given a family of formal solutions with parameters in `P`
(∀ᶠ s in 𝓝ˢ C₁, (𝓕₀ s).to_one_jet_sec.is_holonomic) → -- holonomic near `C₁` of parameter space
(∀ᶠ x in 𝓝ˢ C₂, ∀ s, (𝓕₀ s).to_one_jet_sec.is_holonomic_at x) → -- and near set `C₂` of the domain
∃ 𝓕 : family_formal_sol (𝓘(ℝ, ℝ).prod IP) (ℝ × P) R, -- then there is a homotopy of such families
  (∀ s, 𝓕 (0, s) = 𝓕₀ s) ∧ -- that agrees on `t = 0`
  (∀ᶠ s in 𝓝ˢ C₁, ∀ t : ℝ, 𝓕 (t, s) = 𝓕₀ s) ∧ -- and agrees near `C₁`
  (∀ᶠ x in 𝓝ˢ C₂, ∀ (t : ℝ) (s : P), 𝓕 (t, s) x = 𝓕₀ s x) ∧ -- and agrees near `C₂`
  (∀ s, (𝓕 (1, s)).to_one_jet_sec.is_holonomic) ∧ -- is holonomic everywhere for `t = 1`.
  (∀ (t : ℝ) (s : P) (x : M), @dist _ some_dist (𝓕 (t, s) x) (𝓕₀ s x) ≤ ε x) -- and close to `𝓕₀`

/-- **Gromov's Theorem** -/
theorem rel_mfld.ample.satisfies_h_principle_with (hC₁ : is_closed C₁) (hC₂ : is_closed C₂)
  (hε_pos : ∀ x, 0 < ε x) (hε_cont : continuous ε)
  (h1 : R.ample) (h2 : is_open R) :
  R.satisfies_h_principle_with IP C₁ C₂ ε :=
sorry

[Oliver Nash]

I think for our application we would require the parametric version to be relative only to a closed subset of the parameter space but this is really a question for Patrick. Also, isn't it just the base map of the section of the jet bundle that has to be $C^0$ close?

[Patrick Massot]

In the sphere eversion application of this theorem the homotopy is not relative to a subset in M. But there is a parameter space. And the way we get rid of parameters turns parameters into elements of M somehow, so we need need to have a result relative to a subset of M in the non-parametric case. So I don't think we can gain any simplification from removing C₂

[Patrick Massot]

Much more importantly, Oliver is right that only the base map stays $C^0$-close.

[Patrick Massot]

You need to keep in mind the important example of the Bullock-Reeves theorem. This states that given any map $f : \R \to \R^2$, there is a map $g$ which is as close as you want to $f$ in $C^0$ topology and whose derivative satisfies $\forall t, \|g'(t) \| > 50 \text{ mph}$. That's because the complement of the $50 \text{ mph}$ ball around the origin in ample in $\R^2$. But there is no hope you can guarantee $g'$ stays close to $f'$ if $\|f'\|$ was very small. Note that our proof also doesn't yield any control on the acceleration of $g$, which is presumably why Bullock and Reeves don't use convex integration (but they actually also give up on $C^0$ control).

[Patrick Massot]

Floris, I also don't understand why you want to define the has_dist (one_jet_bundle I M I' M') instead of simply defining the dist function. I guess you want to be able to start the proof with a letI and then access all metric spaces lemmas but you could do both.

[Patrick Massot]

In order to make the statement readable, it would also be nice to define abbreviation getting rid of all .to_one_jet_sec (unless Kyle's new dot notation tweaks allows it without doing anything, which would be awesome).

[Floris van Doorn]

Oh yes, of course we only get the $C^0$-closeness on the base map. I'll correct it tomorrow.
In that case I could just make M' a metric space, to have it for an arbitrary compatible metric.
Patrick, I'm not sure what you mean by "instead of simply defining the dist function".

[Patrick Massot]

I mean replacing @dist _ some_dist (𝓕 (t, s) x) (𝓕₀ s x) with a def. That's not very important and indeed it is probably better to think of a better way of talking about a distance function on a metrizable space.

[Floris van Doorn]

With the corrected version, I made the change that the target space is a metric space, so we can talk about the distance, instead of having to define (and write API for) the distance on a metrizable space.

[Oliver Nash]

Thanks for the updated statements, they look good to me now. We can drop the hypothesis (hC₁ : is_closed C₁) from rel_mfld.ample.satisfies_h_principle though since C₁ is irrelevant, right?

[Patrick Massot]

Yes, this is a copy-paste mistake, there is no parameter in that lemma.

[Patrick Massot]

We have a much more serious issue. The metrizable stuff is backfiring, as I feared. When applying all this to sphere eversion the target manifold is a normed space that get two metric spaces instances: one from the norm and one imposed by the statement and coming from its manifold structure.

[Patrick Massot]

This isn't blocking since with a have a statement for Gromov's theorem assuming a distinguished metric has been fixed. But at some point we'll need a better way to handle this.

[Floris van Doorn]

I was expecting something like this, so I stated the main Gromov's theorem to use an arbitrary metric space instance