Duplicate approximation of continuous by smooth

Stream: mathlib4

[Anatole Dedecker]

I realize just as the new docs#Continuous.exists_contDiff_approx got merged that we already had docs#Continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le and friends :man_facepalming:

I'm not quite sure how I missed it: either I forgot to search, or I was strongly expecting the result to be proven using partitions of unity.

I believe the results I added are better, because they apply to manifolds (see docs#Continuous.exists_contMDiff_approx) where (global) convolution wouldn't work, give a more precise control of the support, and allow the required precision to be any continuous positive function of the point. They also do not require completeness of the target space because there's no vector-valued integration involved. I don't have an analog of the estimate in docs#Continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le, but I think I can do it.

So, I would vote for removing the pre-existing results (but of course keep their preliminaries, convolution by bump functions is still a natural operations!), after making sure that APIs match up. How does that sound?

@Yury G. Kudryashov @Michael Rothgang @Sébastien Gouëzel @Moritz Doll

[Ruben Van de Velde]

As long as "removing" means "deprecating" :)

[Yury G. Kudryashov]

Should we allow a manifold as the codomain?

[Yury G. Kudryashov]

Also, I want to have these versions for complex analysis (I was thinking about rewriting the proof using Weierstrass/Bernstein approximation, but your approach may be better):

• if x and y are joined in an open set, then one can choose the path to be smooth;
• if two smooth paths from x to y are homotopic in an open set, then one can choose a smooth homotopy.

#xy: I want to use these two results together with #24019 to show that a complex differentiable function on a simply connected open subset of Complex admits a primitive.

[Yury G. Kudryashov]

I don't know if it's OK for this result to depend on parts of the manifolds library.

[Yury G. Kudryashov]

In fact, I may decide to write the other approach anyway, because it gives an approximation by multivariate polynomials.