Smooth endpoint-preserving approximation of continuous complex curves

Every continuous map from the unit interval to ℂ is uniformly approximated, to any positive tolerance, by a smooth curve on ℝ taking the same values at 0 and 1. The approximants are Mathlib's Bernstein approximations, read as polynomial functions on all of ℝ, which is what makes their smoothness and their endpoint values immediate.

Main results

• TauCeti.Contour.exists_contDiff_eq_endpoints_dist_lt — the endpoint-preserving smooth approximation.
• JoinedIn.exists_contDiff_mapsTo — two points joined by a path in an open set are joined by a smooth curve that stays in the set.

This is the regularization step that lets the merely continuous intermediate paths of a path homotopy be compared with the piecewise-C¹ winding number.

Provenance

The construction and its uniform convergence are Mathlib's bernsteinApproximation and bernsteinApproximation_uniform; the polynomials themselves are Mathlib's bernsteinPolynomial. No formal source is vendored.

theorem TauCeti.Contour.exists_contDiff_eq_endpoints_dist_lt (f : C(↑unitInterval, ℂ)) {ε : ℝ} (hε : 0 < ε) : ∃ (γ : ℝ → ℂ), ContDiff ℝ ⊤ γ ∧ γ 0 = f 0 ∧ γ 1 = f 1 ∧ ∀ (t : ↑unitInterval), dist (γ ↑t) (f t) < ε

Endpoint-preserving smooth approximation of a continuous complex path. Every continuous map from the unit interval to ℂ is uniformly approximated, to any positive tolerance, by a smooth curve on ℝ with the same values at 0 and 1.

The approximants are Mathlib's Bernstein approximations, read as polynomial functions on ℝ; a consumer needing only piecewise-C¹ regularity gets it from IsPiecewiseC1On.of_contDiffOn.

theorem JoinedIn.exists_contDiff_mapsTo {U : Set ℂ} {z w : ℂ} (h : JoinedIn U z w) (hU : IsOpen U) : ∃ (γ : ℝ → ℂ), ContDiff ℝ ⊤ γ ∧ γ 0 = z ∧ γ 1 = w ∧ Set.MapsTo γ (Set.Icc 0 1) U

Smoothing a path inside an open set. Two points joined by a path in an open set U ⊆ ℂ are joined by a smooth curve on ℝ that maps the unit interval into U.