Partition of unity

Stream: maths

[Yury G. Kudryashov]

Hi, I'm trying to formalize smooth partition of unity. Is there anyone else interested in this? Current progress:

• paracompact spaces : done, polishing for a PR, see #6395
• shrinking lemma: WIP;
• smooth bump function: done, needs refactoring;
• general partition of unity: not started.

[Yury G. Kudryashov]

First, #8281 formalizes continuous and smooth partitions of unity. Second, I'm trying to write something about it. A very rough draft is here: paper1.pdf
This is my first attempt to write a text about formalization, so it may be very bad. Comments are welcome.

[Sebastien Gouezel]

Lean is not the only proof assistant with manifolds https://dl.acm.org/doi/10.1145/3293880.3294093

[Kevin Buzzard]

My impression from papers in this area is that if it has been formalised before, you have to clearly explain what new things your work brings to the table.

[Yury G. Kudryashov]

I didn't know that Isabelle has partitions of unity. Then probably this is not publishable.

[Yury G. Kudryashov]

@Sebastien Gouezel Thanks for the reference.

[Yury G. Kudryashov]

Do you know if someone has formalized the weak Whitney embedding thm?

[Johan Commelin]

If anywhere, I guess it would be in Isabelle.

[Yury G. Kudryashov]

Google doesn't find it but I've managed to miss the Isabelle manifolds library...

[Eric Wieser]

I assume the paper is for FMM 2021, based on the weird footnote in the LaTeX style?

[Yury G. Kudryashov]

Not anymore, because I assume that it is not publishable without the Whitney embedding thm.

[Yury G. Kudryashov]

Now I'm trying to revive an older draft about rotation numbers. It seems that I have either 1h35 or 2h35 till deadline.

[Yury G. Kudryashov]

And this as a draft.

[Patrick Massot]

(deleted)

[Yury G. Kudryashov]

[answering to the deleted post] The abstract of the paper linked by Sebastien says that they have partitions of unity too. I'm going to formalize the weak Whitney embedding thm soon, then revive this paper with this thm as a selling point (unless the actual Isabelle library has it; I'll look into this tomorrow).

[Patrick Massot]

Sorry, I wrote my message and then checked the Isabelle formalization and saw it has partitions of unity, that's why I deleted it.

[Patrick Massot]

We really need to do something with our manifolds to go further than in Isabelle. I really thought my sphere eversion project would do the trick, but nobody helped and then LTE came and took all forces (including me).

[Sebastien Gouezel]

We are already further than Isabelle in the sense that the tangent bundle is a manifold, so you can take the tangent bundle of a tangent bundle, or see the derivative of a smooth map as a smooth map between tangent bundles.

[Patrick Massot]

This is still very much foundational, I don't count this as "doing something with manifolds".

[Sebastien Gouezel]

Sure!

[Heather Macbeth]

@Yury G. Kudryashov I wonder if the following other application of partitions of unity is within reach: if $\omega_1$ and $\omega_2$ are two volume forms on the same manifold $M$ (or, given the current state of tensors, let's say two nice measures which are smooth-function-multiples of each other) with the same total mass, then there exists a self-diffeomorphism of $M$ which takes $\omega_1$ to $\omega_2$.

[Heather Macbeth]

https://www.jstor.org/stable/1994022

[Heather Macbeth]

I just glanced through the proof and it doesn't even use existence and uniqueness for ODEs (although that might be doable too), instead it has some trick using integration.

[Yury G. Kudryashov]

/me is going to read the proof.

[Yury G. Kudryashov]

About the statement: we can talk about smooth functions and multiplication by the Jacobian. We can leave the "measure" or "differential form" interpretation to comments.

[Yury G. Kudryashov]

(ignore, I'm too sleepy now)