Definition 3.0🔗

Definition 3.0. A handle family for the data (P, \mathcal U, \{r_\alpha\}, k) is a subdivision K of P together with continuous self-maps g_\alpha : P \to P (one per index \alpha) such that:

(a) (face preservation) for every \alpha, either r_\alpha \equiv 0, or g_\alpha maps every boundary subpolyhedron of P into itself;

(b) (general position, \le k per cell) for every facet D of K there is a set A of at most k indices such that for every \alpha \notin A, the map g_\alpha is constant on the closed cell \operatorname{conv}(D).

(There is no separate Lean definition: the handle family's data and properties are carried as hypotheses of Proposition 3.2 and conclusions of Theorem 3.4 below.)

Proposition 3.2🔗

Proposition 3.2. Given a handle family (K, \{g_\alpha\}), the map u(t,p,x) \;:=\; (1-t)\,p \;+\; t \sum_\alpha r_\alpha(x)\, g_\alpha(p) is a well-defined continuous map [0,1]\times P\times X \to P satisfying (i)–(iii) of Proposition 2.1 (with the same K in (ii)).

Proof. The inner sum \sigma(p,x) := \sum_\alpha r_\alpha(x)\,g_\alpha(p) is a convex combination — the weights r_\alpha(x) are nonnegative and sum to 1, and only finitely many are nonzero — of the points g_\alpha(p) \in P; since P is convex (a convex hull), \sigma(p,x) \in P, and then u(t,p,x) = (1-t)p + t\,\sigma(p,x) \in P likewise. Continuity of \sigma jointly in (p,x) follows from local finiteness of the partition of unity (locally, the sum is a finite sum of continuous functions), and then u is continuous.

(i) is clear: u(0,p,x) = p.

(ii): Fix a facet D of K and take the exceptional index set A, |A| \le k, from (b). We claim the family (p,x) \mapsto f(u(1,p,x),x) on \operatorname{conv}(D) \times X is supported on \bigcup_{\alpha\in A} U_\alpha. So let x \notin \bigcup_{\alpha \in A} U_\alpha and p, p' \in \operatorname{conv}(D); it suffices to show u(1,p,x) = u(1,p',x), i.e. \sum_\alpha r_\alpha(x) g_\alpha(p) = \sum_\alpha r_\alpha(x) g_\alpha(p'). Compare termwise: for \alpha \in A we have x \notin U_\alpha, and subordination (\overline{\operatorname{supp}\, r_\alpha} \subseteq U_\alpha) gives r_\alpha(x)=0, so the terms vanish; for \alpha \notin A, g_\alpha is constant on \operatorname{conv}(D), so g_\alpha(p) = g_\alpha(p'). Thus the restricted family is adapted with constant k.

(iii): Let Q be a boundary subpolyhedron and p \in Q. Being the convex hull of a finite set, Q is convex. In the sum \sigma(p,x), only indices with r_\alpha(x) \ne 0 contribute; such \alpha have r_\alpha \not\equiv 0, so by (a) g_\alpha preserves Q, giving g_\alpha(p) \in Q. Hence \sigma(p,x), a convex combination of points of Q, lies in Q, and so does u(t,p,x) = (1-t)p + t\,\sigma(p,x). \blacksquare

In Lean, the reparametrization, its membership in P, and its continuity are built in stages:

and the three properties (i)–(iii) are verified in: