search

leanprover-community / sphere-eversion

Formalization of the existence of sphere eversions
https://leanprover-community.github.io/sphere-eversion/
Apache License 2.0
36 stars 10 forks source link

reparametrization: simplify proof #81

Closed fpvandoorn closed 2 years ago

fpvandoorn commented 2 years ago

I proved a stronger convergence result for convolutions in leanprover-community/mathlib#16704. With this result, we can significantly simplify loop.tendsto_mollify_apply.

This PR introduces a sorry (that is proven in the aforementioned PR), so we can decide to only merge this PR after that PR is merged and we bumped mathlib.

PatrickMassot commented 2 years ago

Great! Can you update this now?

fpvandoorn commented 2 years ago

I rebased and pushed this.