description/proof of that for affine simplex and ascending sequence of faces, set of barycenters of faces is affine-independent
Topics
About: vectors space
The table of contents of this article
- Starting Context
- Target Context
- Orientation
- Main Body
- 1: Structured Description
- 2: Natural Language Description
- 3: Proof
Starting Context
- The reader knows a definition of affine simplex.
- The reader knows a definition of ascending sequence of faces of affine simplex.
- The reader knows a definition of barycenter of affine simplex.
- The reader admits the proposition that for any linearly independent finite subset of any module, the induced subset of the module with some linear combinations is linearly independent.
Target Context
- The reader will have a description and a proof of the proposition that for any affine simplex and its any ascending sequence of faces, the set of the barycenters of the faces is affine-independent.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(V\): \(\in \{\text{ the real vectors spaces }\}\)
\(\{p_0, ..., p_n\}\): \(\subseteq V\), \(\in \{\text{ the affine-independent sets of base points on } V\}\)
\([p_0, ..., p_n]\): \(= \text{ the affine simplex }\)
\((p'_0, ..., p'_n)\): \(\in \text{ the sequences whose elements are } \{p_0, ..., p_n\}\)
\(S\): \(= ([p'_0], [p'_0, p'_1], ..., [p'_0, ..., p'_n])\)
\(S'\): \(= \{bary ([p'_0]), bary ([p'_0, p'_1]), ..., bary ([p'_0, ..., p'_n])\}\)
//
Statements:
\(S' \in \{\text{ the affine-independent sets of points on } V\}\).
//
2: Natural Language Description
For any real vectors space, \(V\), any affine-independent set of base points on \(V\), \(\{p_0, ..., p_n\}\), the affine simplex, \([p_0, ..., p_n]\), and any ascending sequence of faces of \([p_0, ..., p_n]\), \(S = ([p'_0], [p'_0, p'_1], ..., [p'_0, ..., p'_n])\), the set of the barycenters of the faces, \(S' = \{bary ([p'_0]), bary ([p'_0, p'_1]), ..., bary ([p'_0, ..., p'_n])\}\), is affine-independent. \(\)
3: Proof
\(bary ([p'_0, ..., p'_m]) = 1 / (m + 1) (p'_0 + ... + p'_m)\). Especially, \(bary ([p'_0]) = p'_0\).
\(bary ([p'_0, ..., p'_m]) - bary ([p'_0]) = 1 / (m + 1) (p'_0 + ... + p'_m) - p'_0 = 1 / (m + 1) (p'_0 + (p'_1 - p'_0) + p'_0 + ... + (p'_m - p'_0) + p'_0) - p'_0 = 1 / (m + 1) ((p'_1 - p'_0) + ... + (p'_m - p'_0) + (m + 1) p'_0) - p'_0 = 1 / (m + 1) ((p'_1 - p'_0) + ... + (p'_m - p'_0)) + p'_0 - p'_0 = 1 / (m + 1) ((p'_1 - p'_0) + ... + (p'_m - p'_0))\).
\(\{bary ([p'_0, p'_1]) - bary ([p'_0]), ..., bary ([p'_0, ..., p'_n]) - bary ([p'_0])\} = \{1 / 2 ((p'_1 - p'_0)), 1 / 3 ((p'_1 - p'_0) + (p'_2 - p'_0)), .., 1 / (n + 1) ((p'_1 - p'_0) + ... + (p'_n - p'_0))\}\).
As \(\{p'_1 - p'_0, p'_2 - p'_0, ..., p'_n - p'_0\}\) is linearly independent, \(\{1 / 2 ((p'_1 - p'_0)), 1 / 3 ((p'_1 - p'_0) + (p'_2 - p'_0)), ..., 1 / (n + 1) ((p'_1 - p'_0) + ... + (p'_n - p'_0))\}\) is linearly independent, by the proposition that for any linearly independent finite subset of any module, the induced subset of the module with some linear combinations is linearly independent.
