Prove2Me

A continuous retraction of the ball onto the sphere can be replaced by a smooth one

Proved
AGT.exists_contDiff_retraction_unitBall

by korbonits · Sep 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

algorithmic-game-theoryanalysisbrouwertopology

Smoothing a retraction (Milnor 1978, Section 2; also Rogers 1980). Let B‾n⊆Rn\overline{B}^n \subseteq \mathbb{R}^n be the closed unit ball and Sn−1S^{n-1} its boundary sphere. If there is a continuous map r:B‾n→Sn−1r : \overline{B}^n \to S^{n-1} with r(x)=xr(x) = x for all x∈Sn−1x \in S^{n-1}, then there is a C∞C^\infty map g:Rn→Rng : \mathbb{R}^n \to \mathbb{R}^n with

g(B‾n)⊆Sn−1andg(x)=xfor all x∈Sn−1.g(\overline{B}^n) \subseteq S^{n-1} \qquad\text{and}\qquad g(x) = x \quad \text{for all } x \in S^{n-1}.

This is the approximation step in Milnor's analytic proof of the no-retraction theorem (and hence of Brouwer's fixed-point theorem): it reduces the continuous statement to the smooth one, AGT.no_contDiff_retraction_unitBall, where calculus (the inverse function theorem and the change-of-variables formula) can be applied. The standard construction extends rr radially to Rn\mathbb{R}^n, approximates the extension uniformly by a polynomial map (Stone–Weierstrass), normalizes to unit length, and patches with a smooth cutoff so that the map is exactly the identity on a neighbourhood of the sphere.

A note on the hypotheses. For n=0n = 0 the hypotheses are contradictory (the ball is a point and the sphere is empty), so the statement holds vacuously; nothing else is assumed. Only continuity of rr on the ball is used.

Formalization Note. The ambient space is EuclideanSpace ℝ (Fin n). The input retraction is a total function with ContinuousOn r (closedBall 0 1), Set.MapsTo r (closedBall 0 1) (sphere 0 1) and the fixed-point condition; the output is a total function g with ContDiff ℝ ⊤ g (here ⊤ : ℕ∞, i.e. C∞C^\infty) and the same two conditions.

Preamble
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.Calculus.ContDiff.Basic
Formal statement
namespace AGT

/-- **Smoothing a retraction** (Milnor 1978, §2).  If the closed unit ball of
`ℝⁿ` admits a continuous retraction onto its boundary sphere, then it admits a
smooth one, defined on all of `ℝⁿ`. -/
theorem exists_contDiff_retraction_unitBall (n : ℕ)
    (r : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hr : ContinuousOn r (Metric.closedBall 0 1))
    (hrS : Set.MapsTo r (Metric.closedBall 0 1) (Metric.sphere 0 1))
    (hfix : ∀ x ∈ Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1, r x = x) :
    ∃ g : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n),
      ContDiff ℝ (⊤ : ℕ∞) g ∧ Set.MapsTo g (Metric.closedBall 0 1) (Metric.sphere 0 1) ∧
      ∀ x ∈ Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1, g x = x := by
  sorry

end AGT
Source
J. Milnor, Analytic proofs of the "hairy ball theorem" and the Brouwer fixed point theorem, Amer. Math. Monthly 85 (1978), 521-524, Section 2 (the reduction from continuous to smooth retractions by polynomial approximation, p. 523); C. A. Rogers, A less strange version of Milnor's proof of Brouwer's fixed-point theorem, Amer. Math. Monthly 87 (1980), 525-527. Supporting result for Theorem 1.8 of Nisan-Roughgarden-Tardos-Vazirani (eds.), Algorithmic Game Theory, Cambridge 2007, Ch. 1.

View graph