TheoremBase

Proof

Let x∈Rnx\in\mathbb{R}^{n} satisfy the stated inequality, write yi=xi−(x0)iy_{i}=x_{i}-(x_{0})_{i} for i∈[n]i\in[n] and put s=∑i=1n∣yi∣s=\sum_{i=1}^{n}|y_{i}|, so that s≤rs\le r. Let SS be the successor map of Natural Numbers and put N=S(n)N=S(n); by claim 3 of Basic Properties of Initial Segments of the Natural Numbers we have [N]=[n]∪{N}[N]=[n]\cup\{N\} with N∉[n]N\notin[n], so a family indexed by [N][N] may be prescribed separately on [n][n] and at NN.

Since 0<r0<r, claim 7 of Elementary Order Arithmetic in an Ordered Field gives 0<r−10<r^{-1} for the multiplicative inverse r−1r^{-1} of rr.

The family of points. For i∈[n]i\in[n] set σi=1\sigma_{i}=1 if 0≤yi0\le y_{i} and σi=−1\sigma_{i}=-1 otherwise, so that σi∣yi∣=yi\sigma_{i}|y_{i}|=y_{i} in either case, by Absolute Value in an Ordered Field. Define v:[N]→Rnv:[N]\to\mathbb{R}^{n} by

vk=x0+(rσk) e(k)  (k∈[n]),vN=x0.v_{k}=x_{0}+(r\sigma_{k})\,e^{(k)}\ \ (k\in[n]),\qquad v_{N}=x_{0}.

Each vkv_{k} with k∈[n]k\in[n] is x0+r e(k)x_{0}+r\,e^{(k)} or x0−r e(k)x_{0}-r\,e^{(k)}, so every value of vv lies in CC and satisfies u(vk)≤Mu(v_{k})\le M, by hypothesis.

The weights. Define t:[N]→Rt:[N]\to\mathbb{R} by

tk=∣yk∣ r−1  (k∈[n]),tN=1−s r−1.t_{k}=|y_{k}|\,r^{-1}\ \ (k\in[n]),\qquad t_{N}=1-s\,r^{-1}.

For k∈[n]k\in[n] we have 0≤∣yk∣0\le|y_{k}| by claim 1 of Properties of the Absolute Value in an Ordered Field, so 0≤tk0\le t_{k} by claim 5 of Elementary Arithmetic in an Ordered Field. Multiplying s≤rs\le r by the nonnegative number r−1r^{-1}, again by claim 5 of Elementary Arithmetic in an Ordered Field, gives s r−1≤r r−1=1s\,r^{-1}\le r\,r^{-1}=1, so 0≤tN0\le t_{N} by claim 3 of Elementary Order Arithmetic in an Ordered Field.

By the recursion in claim 1 and by claim 3 of Properties of Finite Sums,

∑k=1Ntk=(∑k=1n∣yk∣ r−1)+tN=s r−1+(1−s r−1)=1,\sum_{k=1}^{N}t_{k}=\Bigl(\sum_{k=1}^{n}|y_{k}|\,r^{-1}\Bigr)+t_{N}=s\,r^{-1}+\bigl(1-s\,r^{-1}\bigr)=1,

so tt is a system of convex weights of length NN.

The combination is xx. Fix j∈[n]j\in[n]. For k∈[n]k\in[n] the jjth coordinate of vkv_{k} is (x0)j+rσk(x_{0})_{j}+r\sigma_{k} if k=jk=j and (x0)j(x_{0})_{j} otherwise, while the jjth coordinate of vNv_{N} is (x0)j(x_{0})_{j}. Hence, writing w:[N]→Rw:[N]\to\mathbb{R} for the family with wj=rσjw_{j}=r\sigma_{j} and wk=0w_{k}=0 for every k∈[N]k\in[N] with k≠jk\ne j, we have (vk)j=(x0)j+wk(v_{k})_{j}=(x_{0})_{j}+w_{k} for every k∈[N]k\in[N]. By claims 2 and 3 of Properties of Finite Sums, by the value of ∑k=1Ntk\sum_{k=1}^{N}t_{k} computed above, and by claim 7 of Properties of Finite Sums applied to the family k↦tkwkk\mapsto t_{k}w_{k}, which vanishes off jj,

(∑k=1Ntkvk)j=∑k=1Ntk((x0)j+wk)=(x0)j∑k=1Ntk+∑k=1Ntkwk=(x0)j+tj rσj,\Bigl(\sum_{k=1}^{N}t_{k}v_{k}\Bigr)_{j}=\sum_{k=1}^{N}t_{k}\bigl((x_{0})_{j}+w_{k}\bigr)=(x_{0})_{j}\sum_{k=1}^{N}t_{k}+\sum_{k=1}^{N}t_{k}w_{k}=(x_{0})_{j}+t_{j}\,r\sigma_{j},

the convex combination being that of Convex Combination of Finitely Many Points of Rn\mathbb{R}^n. Finally

tj rσj=∣yj∣ r−1r σj=σj∣yj∣=yj,t_{j}\,r\sigma_{j}=|y_{j}|\,r^{-1}r\,\sigma_{j}=\sigma_{j}|y_{j}|=y_{j},

so the jjth coordinate of the combination is (x0)j+yj=xj(x_{0})_{j}+y_{j}=x_{j}. As j∈[n]j\in[n] was arbitrary, x=∑k=1Ntkvkx=\sum_{k=1}^{N}t_{k}v_{k}.

Conclusion. All values of vv lie in the convex set CC, so xx lies in CC by claim 3 of Small Cases, Reduction, and Membership for Convex Combinations. By Jensen's Inequality for Finite Convex Combinations,

u(x)≤∑k=1Ntk u(vk).u(x)\le\sum_{k=1}^{N}t_{k}\,u(v_{k}).

For every k∈[N]k\in[N] we have u(vk)≤Mu(v_{k})\le M and 0≤tk0\le t_{k}, so tku(vk)≤tkMt_{k}u(v_{k})\le t_{k}M by claim 5 of Elementary Arithmetic in an Ordered Field. Comparing the two sums termwise by Comparison and Absolute Value Bounds for Finite Sums of Real Numbers and then using claim 3 of Properties of Finite Sums,

∑k=1Ntk u(vk)≤∑k=1NtkM=M∑k=1Ntk=M,\sum_{k=1}^{N}t_{k}\,u(v_{k})\le\sum_{k=1}^{N}t_{k}M=M\sum_{k=1}^{N}t_{k}=M,

whence u(x)≤Mu(x)\le M by claim 1 of Elementary Order Arithmetic in an Ordered Field.

Citations

Loading…

Dependencies

Uses0

Loading…

Comments

Log in to comment.

Loading…