## Stream: sphere eversion

### Topic: Gromov's theorem

#### Floris van Doorn (Aug 25 2022 at 15:55):

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 (Aug 25 2022 at 16:49):

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 (Aug 25 2022 at 17:27):

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 (Aug 25 2022 at 17:30):

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

#### Patrick Massot (Aug 25 2022 at 17:37):

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 (Aug 25 2022 at 17:40):

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 (Aug 25 2022 at 17:41):

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 (Aug 25 2022 at 18:34):

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 (Aug 25 2022 at 19:26):

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 (Aug 26 2022 at 12:20):

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 (Aug 26 2022 at 14:24):

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 (Aug 26 2022 at 14:30):

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

#### Patrick Massot (Aug 26 2022 at 14:32):

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 (Aug 26 2022 at 14:40):

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 (Aug 26 2022 at 14:41):

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

Last updated: Dec 20 2023 at 11:08 UTC