let n, k be Nat; for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds
diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K)
let K be non void finite-degree bounded SimplicialComplex of (TOP-REAL n); ( |.K.| c= [#] K implies diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K) )
set dK = degree K;
set ddK = (degree K) / ((degree K) + 1);
defpred S1[ Nat] means ( diameter (BCS ($1,K)) <= (((degree K) / ((degree K) + 1)) |^ $1) * (diameter K) & BCS ($1,K) is finite-degree & degree (BCS ($1,K)) <= degree K );
assume A1:
|.K.| c= [#] K
; diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K)
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
set T =
TOP-REAL n;
set B =
BCS (
k,
K);
set cM =
center_of_mass (TOP-REAL n);
A3:
degree K >= - 1
by SIMPLEX0:23;
assume A4:
S1[
k]
;
S1[k + 1]
then reconsider B =
BCS (
k,
K) as non
void finite-degree bounded SimplicialComplex of
(TOP-REAL n) ;
set dB =
degree B;
A5:
degree B >= - 1
by SIMPLEX0:23;
A6:
0 <= diameter K
by Th7;
A7:
0 <= diameter B
by Th7;
A8:
(
|.B.| = |.K.| &
[#] B = [#] K )
by A1, SIMPLEX1:18, SIMPLEX1:19;
then A9:
BCS B = subdivision (
(center_of_mass (TOP-REAL n)),
B)
by A1, SIMPLEX1:def 5;
A10:
BCS (
(k + 1),
K)
= BCS B
by A1, SIMPLEX1:20;
then A11:
diameter (BCS ((k + 1),K)) <= ((degree B) / ((degree B) + 1)) * (diameter B)
by A1, A8, Th16;
not
{} in dom (center_of_mass (TOP-REAL n))
by ORDERS_1:1;
then
dom (center_of_mass (TOP-REAL n)) is
with_non-empty_elements
by SETFAM_1:def 8;
then A12:
degree (BCS ((k + 1),K)) <= degree B
by A9, A10, SIMPLEX0:52;
per cases
( degree B = - 1 or degree B = 0 or ( degree B <> - 1 & degree B <> 0 ) )
;
suppose
(
degree B = - 1 or
degree B = 0 )
;
S1[k + 1]then A13:
(degree B) / ((degree B) + 1) = 0
;
per cases
( degree K = 0 or degree K = - 1 or ( degree K <> 0 & degree K <> - 1 ) )
;
suppose A14:
(
degree K <> 0 &
degree K <> - 1 )
;
S1[k + 1]then
degree K > - 1
by A3, XXREAL_0:1;
then
degree K >= (- 1) + 1
by INT_1:7;
then
(degree K) / ((degree K) + 1) > 0
by A14, XREAL_1:139;
then
((degree K) / ((degree K) + 1)) |^ (k + 1) > 0
by NEWTON:83;
hence
S1[
k + 1]
by A1, A4, A6, A9, A11, A12, A13, SIMPLEX1:20, XXREAL_0:2;
verum end; end; suppose
(
degree B <> - 1 &
degree B <> 0 )
;
S1[k + 1]then
degree B > - 1
by A5, XXREAL_0:1;
then A15:
degree B >= (- 1) + 1
by INT_1:7;
A16:
(degree B) / ((degree B) + 1) =
(((degree B) + 1) / ((degree B) + 1)) - (1 / ((degree B) + 1))
.=
1
- (1 / ((degree B) + 1))
by A15, XCMPLX_1:60
;
A17:
(degree K) / ((degree K) + 1) =
(((degree K) + 1) / ((degree K) + 1)) - (1 / ((degree K) + 1))
.=
1
- (1 / ((degree K) + 1))
by A4, A15, XCMPLX_1:60
;
(degree B) + 1
<= (degree K) + 1
by A4, XREAL_1:6;
then
1
/ ((degree K) + 1) <= 1
/ ((degree B) + 1)
by A15, XREAL_1:85;
then
(degree B) / ((degree B) + 1) <= (degree K) / ((degree K) + 1)
by A16, A17, XREAL_1:10;
then A18:
((degree B) / ((degree B) + 1)) * (diameter B) <= ((degree K) / ((degree K) + 1)) * ((((degree K) / ((degree K) + 1)) |^ k) * (diameter K))
by A4, A7, A15, XREAL_1:66;
((degree K) / ((degree K) + 1)) * ((((degree K) / ((degree K) + 1)) |^ k) * (diameter K)) =
(((degree K) / ((degree K) + 1)) * (((degree K) / ((degree K) + 1)) |^ k)) * (diameter K)
.=
(((degree K) / ((degree K) + 1)) |^ (k + 1)) * (diameter K)
by NEWTON:6
;
hence
S1[
k + 1]
by A1, A4, A9, A11, A12, A18, SIMPLEX1:20, XXREAL_0:2;
verum end;
end;
((degree K) / ((degree K) + 1)) |^ 0 = 1
by NEWTON:4;
then A19:
S1[ 0 ]
by A1, SIMPLEX1:16;
for k being Nat holds S1[k]
from NAT_1:sch 2(A19, A2);
hence
diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K)
; verum