# Zulip Chat Archive

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