Bump functions

Stream: Is there code for X?

[Patrick Massot]

@Yury G. Kudryashov and @Sebastien Gouezel what is the status of smooth bump function in vector spaces? I can find a lot of topological stuff and some manifold stuff, but not the intermediate vector space notion. Specifically I have a compact set $K$ in a finite dimensional real vector space and a neighborhood $U$ of $K$, do we have a smooth $[0, 1]$-value function which equals $1$ near $K$ and has compact support inside $U$?

[Yury G. Kudryashov]

You can use docs#exists_smooth_zero_one_of_closed

[Yury G. Kudryashov]

And use the fact that a vector space is a manifold.

[Patrick Massot]

Do you mean we actually have this for manifolds but not for vector spaces?

[Patrick Massot]

This doesn't seem reasonable to import manifold theory for this

[Yury G. Kudryashov]

We have bump function supported on a ball for a vector space.

[Patrick Massot]

I don't see how to prove this lemma for manifolds without having a simpler proof for vector spaces.

[Yury G. Kudryashov]

The proof for vector spaces (and closed sets, not closed balls) is the same as for manifolds.

[Yury G. Kudryashov]

The main lemma is docs#smooth_bump_covering.exists_is_subordinate.

[Yury G. Kudryashov]

Why importing manifolds is so bad?

[Heather Macbeth]

@Yury G. Kudryashov There's also https://leanprover-community.github.io/mathlib_docs/analysis/calculus/specific_functions.html right?

[Yury G. Kudryashov]

Yes but this is about bump functions supported on closed balls.

[Yury G. Kudryashov]

(more precisely, on closed balls in an unspecified Euclidean metric on your space)

[Yury G. Kudryashov]

@Patrick Massot You can repeat the proof for vector spaces using docs#times_cont_diff_bump if you want to avoid importing manifolds.

[Yury G. Kudryashov]

It will be a bit easier because you won't need to care about the manifold boundary.

[Patrick Massot]

Usually I don't mind crushing easy things with super general tools, but that one seems a bit too much

[Yury G. Kudryashov]

I would prefer not to have 2 theories of smooth partitions of unity in mathlib, one for vector spaces and one for manifolds.

[Yury G. Kudryashov]

Because it will be hard to maintain feature parity.

[Patrick Massot]

We'll have to restate things anyway

[Patrick Massot]

I'm not even really convince you could derive the statement I asked about from the manifold stuff we have.

[Yury G. Kudryashov]

Let me do it.

[Yury G. Kudryashov]

import geometry.manifold.partition_of_unity

open set
open_locale manifold

lemma exists_times_cont_diff_zero_one {E : Type*} [normed_group E]
  [normed_space ℝ E] [finite_dimensional ℝ E] {s t : set E} (hs : is_closed s)
  (ht : is_closed t) (hd : disjoint s t) :
  ∃ f : E → ℝ, times_cont_diff ℝ ⊤ f ∧ eq_on f 0 s ∧ eq_on f 1 t ∧
    ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
let ⟨f, hfs, hft, hf01⟩ := exists_smooth_zero_one_of_closed 𝓘(ℝ, E) hs ht hd
in ⟨f, f.smooth.times_cont_diff, hfs, hft, hf01⟩

[Yury G. Kudryashov]

If you want the function to be 1 in a neighborhood of K, then you need to use some separation property first.

[Yury G. Kudryashov]

IMHO, this should be done for manifolds.

[Yury G. Kudryashov]

(I don't remember what are the minimal assumptions for existence of intermediate compact sets)

[Patrick Massot]

This is indeed easier than what I thought. The neighborhood question is independent from the question of going from manifolds to vector spaces.

[Yury G. Kudryashov]

Thanks @Sebastien Gouezel for writing such a good manifolds library.

[Patrick Massot]

I just tried to use this idea of pulling the whole manifold library to get bump functions in vector spaces. Unfortunately if also brings smooth_at in the root namespace. @Sebastien Gouezel do you think we could move this docs#smooth_at to some manifold specific namespace?

[Sebastien Gouezel]

Yes, sure!

[Patrick Massot]

Do you have a namespace to suggest?

[Yury G. Kudryashov]

We can just call it msmooth_at.

[Yury G. Kudryashov]

This will agree with mdifferentiable etc