environ
vocabularies HIDDEN, NUMBERS, ORDINAL1, SUBSET_1, CARD_1, ARYTM_3, TARSKI, RELAT_1, XXREAL_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1, ZFMISC_1, FINSEQ_1, VALUED_0, VALUED_1, CARD_3, RFINSEQ2, NEWTON, EQREL_1, FIB_NUM2, ORDINAL4, ORDINAL2, GOBRD13, ABIAN, FINSEQ_2, CLASSES1, MCART_1, FINSOP_1, POWER, RFUNCT_3, MONOID_0, FLEXARY1, EULRPART;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1, MONOID_0, FUNCT_2, XXREAL_0, NAT_1, FINSEQ_2, FINSEQ_1, VALUED_0, VALUED_1, FINSET_1, RVSUM_1, CLASSES1, XXREAL_2, ABIAN, RFINSEQ2, FIB_NUM2, FUNCT_3, NAT_D, MATRIX_0, NEWTON, POWER, FINSOP_1, RFUNCT_3, JORDAN1H, FLEXARY1;
definitions TARSKI, FUNCT_1, FLEXARY1;
theorems ABIAN, CARD_1, CARD_2, CARD_4, CLASSES1, FIB_NUM2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FOMODEL2, FUNCOP_1, FUNCT_1, FUNCT_2, INTEGRA3, MATRPROB, NAGATA_2, NAT_1, NAT_D, NEWTON, NUMBERS, ORDINAL1, RELAT_1, RFINSEQ, RFINSEQ2, RFUNCT_3, RVSUM_1, STIRL2_1, SUBSET_1, TARSKI, VALUED_0, VALUED_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, XXREAL_2, ZFMISC_1, FLEXARY1;
schemes FINSEQ_1, FINSEQ_2, FUNCT_2, NAT_1, FLEXARY1;
registrations ORDINAL1, XREAL_0, FUNCT_1, FINSEQ_1, FINSEQ_2, VALUED_0, VALUED_1, PRE_POLY, NAT_1, INT_6, RVSUM_1, XCMPLX_0, MEMBERED, VALUED_2, FOMODEL0, XBOOLE_0, RELAT_1, FUNCT_2, CARD_1, RELSET_1, XXREAL_2, EUCLID_9, FINSET_1, XXREAL_0, NUMBERS, INT_1, AOFA_A00, XTUPLE_0, NEWTON, ABIAN, POWER, RFINSEQ, AFINSQ_2, FLEXARY1;
constructors HIDDEN, XXREAL_2, ABIAN, RFINSEQ2, CLASSES1, MONOID_0, NAT_D, FOMODEL2, RELSET_1, FIB_NUM2, FINSOP_1, NEWTON, POWER, JORDAN1H, FLEXARY1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities FINSEQ_1, FINSEQ_2, XCMPLX_0, FLEXARY1;
expansions FINSEQ_1, TARSKI, XBOOLE_0, FUNCT_1;
Lm1:
for f1, f2, g1, g2 being complex-valued FinSequence st len f1 = len g1 & len f2 <= len g2 holds
(f1 ^ f2) (#) (g1 ^ g2) = (f1 (#) g1) ^ (f2 (#) g2)
Lm2:
for i being Nat
for f being complex-valued FinSequence holds ((id (dom f)) (#) f) . i = i * (f . i)
Lm3:
for mu being natural-valued FinSequence st ( for j being Nat holds mu . (2 * j) = 0 ) holds
ex h being odd-valued FinSequence st
( h is non-decreasing & ( for j being Nat holds card (Coim (h,j)) = mu . j ) )
theorem Th11:
for
n being
Nat for
d being
one-to-one a_partition of
n ex
e being
odd-valued a_partition of
n st
for
j being
Nat for
O1 being
odd-valued FinSequence for
a1 being
natural-valued FinSequence st
len O1 = len d &
len d = len a1 &
d = O1 (#) (2 |^ a1) holds
for
sort being
DoubleReorganization of
dom d st 1
= O1 . (sort _ (1,1)) & ... & 1
= O1 . (sort _ (1,(len (sort . 1)))) & 3
= O1 . (sort _ (2,1)) & ... & 3
= O1 . (sort _ (2,(len (sort . 2)))) & 5
= O1 . (sort _ (3,1)) & ... & 5
= O1 . (sort _ (3,(len (sort . 3)))) & ( for
i being
Nat holds
(2 * i) - 1
= O1 . (sort _ (i,1)) & ... &
(2 * i) - 1
= O1 . (sort _ (i,(len (sort . i)))) ) holds
(
card (Coim (e,1)) = ((2 |^ a1) . (sort _ (1,1))) + (((((2 |^ a1) *. sort) . 1),2) +...) &
card (Coim (e,3)) = ((2 |^ a1) . (sort _ (2,1))) + (((((2 |^ a1) *. sort) . 2),2) +...) &
card (Coim (e,5)) = ((2 |^ a1) . (sort _ (3,1))) + (((((2 |^ a1) *. sort) . 3),2) +...) &
card (Coim (e,((j * 2) - 1))) = ((2 |^ a1) . (sort _ (j,1))) + (((((2 |^ a1) *. sort) . j),2) +...) )
definition
let n be
Nat;
let p be
one-to-one a_partition of
n;
func Euler_transformation p -> odd-valued a_partition of
n means :
Def5:
for
j being
Nat for
O being
odd-valued FinSequence for
a being
natural-valued FinSequence st
len O = len p &
len p = len a &
p = O (#) (2 |^ a) holds
for
sort being
DoubleReorganization of
dom p st 1
= O . (sort _ (1,1)) & ... & 1
= O . (sort _ (1,(len (sort . 1)))) & 3
= O . (sort _ (2,1)) & ... & 3
= O . (sort _ (2,(len (sort . 2)))) & 5
= O . (sort _ (3,1)) & ... & 5
= O . (sort _ (3,(len (sort . 3)))) & ( for
i being
Nat holds
(2 * i) - 1
= O . (sort _ (i,1)) & ... &
(2 * i) - 1
= O . (sort _ (i,(len (sort . i)))) ) holds
(
card (Coim (it,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) &
card (Coim (it,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) &
card (Coim (it,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) &
card (Coim (it,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) );
existence
ex b1 being odd-valued a_partition of n st
for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (b1,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (b1,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (b1,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (b1,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )
by Th11;
uniqueness
for b1, b2 being odd-valued a_partition of n st ( for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (b1,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (b1,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (b1,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (b1,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) ) & ( for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (b2,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (b2,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (b2,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (b2,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) ) holds
b1 = b2
end;
::
deftheorem Def5 defines
Euler_transformation EULRPART:def 5 :
for n being Nat
for p being one-to-one a_partition of n
for b3 being odd-valued a_partition of n holds
( b3 = Euler_transformation p iff for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (b3,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (b3,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (b3,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (b3,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) );
Lm4:
for n being Nat
for p1, p2 being one-to-one a_partition of n st Euler_transformation p1 = Euler_transformation p2 holds
rng p1 c= rng p2