Proof.
We need to prove the characterisation in Prop. 3.19.
Without loss of generality is achieved by . We need to find , such that
For this we study the gradient of the function on the various -charts.
First, notice for on the face , namely the convex hull of , the vector is parallel to the face, and by convexity of the directional derivative is monotone along the path from to , so must be maximized at . In particular we consider such line segments on the face parallel to for . By the discrete symmetry, must be zero on the plane of reflection bisecting the face. Thus for , , the subset of the face
|
|
|
agrees exactly with the half of the face containing . Therefore the subset of face
|
|
|
is exactly the intersection of with the face. Without loss of generality lies in .
We follow the notation in the proof of Prop. 3.26. In the -chart, denote the gradient of as , so that for in the -chart,
|
|
|
A priori lives in . We lift to by demanding , so by the above discussion
for
Define , then for all .
We regard as the gradient of at , and write as a function of . This construction can be made on other faces as well, and on the intersection of two faces the definitions are compatible.
We claim : it suffices to show . Notice .
Consider the line segment in the face joining to the boundary of the face in the direction , which stays inside , and along which increases, or equivalently increases. But the boundary of the face lies also on a different face, and we can use the information from this new face to deduce there.
By construction for in the -chart,
|
|
|
We claim that in fact holds for all . We are left to check for on the face , namely the complement of the -chart. Consider the -chart for . We can write according to the decomposition , that
|
|
|
By local convexity, in the -chart is convex, so there is some , such that for any in the -chart
|
|
|
But a gradient vector of at is , so we may take . Thus
|
|
|
Now as in the proof of Prop. 3.26, and by . This implies as required.
We have verified the characterisation in Prop. 3.19, hence the extension property. ∎