MOMENTM1

MOMENTM1: On n-dimensional Real Spaces and n-dimensional Complex Spaces I. by Yatsuka Nakamura :: On n-dimensional Real Spaces and n-dimensional Complex Spaces I
:: by Yatsuka Nakamura
::

environ

vocabularies HIDDEN, TARSKI, NUMBERS, NAT_1, FINSEQ_2, FINSEQ_1, SUBSET_1, SQUARE_1, VALUED_0, CARD_1, XXREAL_0, XCMPLX_0, FUNCT_1, FUNCT_2, FUNCT_7, XBOOLE_0, RVSUM_1, COMPLEX1, RELAT_1, REAL_1, ARYTM_1, MOMENTM1;
notations HIDDEN, TARSKI, XBOOLE_0, VALUED_0, FUNCT_1, FUNCT_2, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, FINSEQ_1, FINSEQ_2, DOMAIN_1, RELAT_1, XXREAL_0, SUBSET_1, EUCLID;
definitions TARSKI;
theorems FINSEQ_1, FINSEQ_2, FUNCT_1, FUNCT_2, TARSKI, COMPLEX1, FUNCOP_1, ORDINAL1, NUMBERS, XBOOLE_1;
schemes ;
registrations RELSET_1, NUMBERS, XREAL_0, FINSEQ_2, RVSUM_1, ORDINAL1, COMPLEX1, XCMPLX_0;
constructors HIDDEN, COMPLEX1, FINSEQOP, TOPMETR, EUCLID;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities EUCLID, FINSEQ_1, FINSEQ_2;
expansions TARSKI, XBOOLE_0;

theorem Th1: :: MOMENTM1:1

REAL c= COMPLEX by NUMBERS:11;

theorem :: MOMENTM1:2

<i> in COMPLEX ;

theorem :: MOMENTM1:3

<i> * <i> = - 1r by COMPLEX1:18;

theorem Th4: :: MOMENTM1:4

not <i> in REAL by COMPLEX1:7;

theorem :: MOMENTM1:5

REAL c< COMPLEX by Th4, Th1;

theorem :: MOMENTM1:6

REAL * is FinSequenceSet of REAL ;

theorem :: MOMENTM1:7

COMPLEX * is FinSequenceSet of COMPLEX ;

theorem Th8: :: MOMENTM1:8

REAL * is FinSequenceSet of COMPLEX by FINSEQ_2:91, Th1;

theorem :: MOMENTM1:9

REAL * c= COMPLEX * by FINSEQ_2:90, Th8;

definition

let n be Nat;

func COMPLEX n -> FinSequenceSet of COMPLEX equals :: MOMENTM1:def 1
n -tuples_on COMPLEX;

end;

:: deftheorem defines COMPLEX MOMENTM1:def 1 :

registration

let n be Nat;

cluster COMPLEX n -> non empty ;

end;

registration

let n be Nat;

cluster -> n -element for Element of COMPLEX n;

end;

theorem :: MOMENTM1:10

for n being Nat holds REAL n = n -tuples_on REAL ;

theorem :: MOMENTM1:11

for n being Nat holds COMPLEX n = n -tuples_on COMPLEX ;

registration

let n be Nat;

cluster -> n -element for Element of COMPLEX n;

end;

theorem :: MOMENTM1:12

for n being Nat holds REAL n = n -tuples_on REAL ;

theorem :: MOMENTM1:13

for n being Nat holds COMPLEX n = n -tuples_on COMPLEX ;

theorem :: MOMENTM1:14

for n being Nat holds REAL n is FinSequenceSet of REAL ;

theorem :: MOMENTM1:15

for n being Nat holds COMPLEX n is FinSequenceSet of COMPLEX ;

registration

let n be Nat;

cluster COMPLEX n -> non empty ;

end;

registration

let n be Nat;

cluster -> n -element for Element of COMPLEX n;

end;

theorem :: MOMENTM1:16

for n being Nat holds COMPLEX n = n -tuples_on COMPLEX ;

theorem Th17: :: MOMENTM1:17

for n being Nat holds n -tuples_on REAL = Funcs ((Seg n),REAL) by FINSEQ_2:93;

theorem Th18: :: MOMENTM1:18

for n being Nat holds n -tuples_on COMPLEX = Funcs ((Seg n),COMPLEX) by FINSEQ_2:93;

theorem Th19: :: MOMENTM1:19

for x being object
for n being Nat holds
( x in Funcs ((Seg n),REAL) iff ex f being Function st
( x = f & dom f = Seg n & rng f c= REAL ) ) by FUNCT_2:def 2;

theorem Th20: :: MOMENTM1:20

for x being object
for n being Nat holds
( x in Funcs ((Seg n),COMPLEX) iff ex f being Function st
( x = f & dom f = Seg n & rng f c= COMPLEX ) ) by FUNCT_2:def 2;

theorem Th21: :: MOMENTM1:21

for n being Nat holds n -tuples_on COMPLEX = Funcs ((Seg n),COMPLEX) by FINSEQ_2:93;

theorem Th22: :: MOMENTM1:22

for n being Nat holds Funcs ((Seg n),REAL) c= Funcs ((Seg n),COMPLEX)

let n be Nat; :: thesis:
thus Funcs ((Seg n),REAL) c= Funcs ((Seg n),COMPLEX) :: thesis:

let x3 be object ; :: according to TARSKI:def 3 :: thesis:
assume x3 in Funcs ((Seg n),REAL) ; :: thesis:
then consider f being Function such that
A1: ( x3 = f & dom f = Seg n & rng f c= REAL ) by Th19;
thus x3 in Funcs ((Seg n),COMPLEX) by Th1, Th20, XBOOLE_1:1, A1; :: thesis:

end;

end;

theorem Th23: :: MOMENTM1:23

for n being Nat holds n -tuples_on REAL c= n -tuples_on COMPLEX

let n be Nat; :: thesis:

let x3 be object ; :: thesis:
assume A1: x3 in n -tuples_on REAL ; :: thesis:
A2: Funcs ((Seg n),REAL) c= Funcs ((Seg n),COMPLEX) by Th22;
x3 in Funcs ((Seg n),REAL) by Th17, A1;
then x3 in Funcs ((Seg n),COMPLEX) by A2;
hence x3 in n -tuples_on COMPLEX by Th21; :: thesis:

end;

hence n -tuples_on REAL c= n -tuples_on COMPLEX ; :: thesis:

end;

theorem :: MOMENTM1:24

for n being Nat holds REAL n c= COMPLEX n by Th23;

definition

let n be Nat;

func I* n -> FinSequence equals :: MOMENTM1:def 2
n |-> (In (1,REAL));

end;

:: deftheorem defines I* MOMENTM1:def 2 :

definition

let n be Nat;

func i* n -> complex-valued FinSequence equals :: MOMENTM1:def 3
n |-> (In (<i>,COMPLEX));

end;

:: deftheorem defines i* MOMENTM1:def 3 :

theorem :: MOMENTM1:25

for n being Nat holds i* n is Element of COMPLEX n ;

theorem :: MOMENTM1:26

for n being Nat st 1 <= n holds
i* n in COMPLEX n ;

registration

let n be Nat;

cluster -> n -element for Element of COMPLEX n;

end;

theorem Th27: :: MOMENTM1:27

for n being Nat st 1 <= n holds
( rng (i* n) = {<i>} & ex f2 being Function st
( dom f2 = Seg n & rng f2 c= COMPLEX ) )

let n be Nat; :: thesis:
assume A1: 1 <= n ; :: thesis:
A2: 1 in Seg n by A1;
A3: n is Element of NAT by ORDINAL1:def 12;
for A being set
for p being FinSequence of A holds
( p in n -tuples_on A iff len p = n ) by FINSEQ_2:133, A3;
then A4: for p being FinSequence of COMPLEX holds
( p in n -tuples_on COMPLEX iff len p = n ) ;
A5: ( i* n in n -tuples_on COMPLEX iff len (i* n) = n ) by A4;
A6: len (i* n) = n by A5;
A7: Seg (len (i* n)) = dom (i* n) by FINSEQ_1:def 3;
A8: len (i* n) = n by A6;
then A9: dom (i* n) = Seg n by A7;
1 in { k where k is Nat : ( 1 <= k & k <= n ) } by A2;
then A10: 1 in Seg n ;
then A11: 1 in dom (i* n) by A9;
A12: (n |-> (In (<i>,COMPLEX))) . 1 = In (<i>,COMPLEX) by A10, FUNCOP_1:7;
reconsider p = n |-> (In (<i>,COMPLEX)) as FinSequence ;
A13: Seg (len p) = dom p by FINSEQ_1:def 3;
p . 1 = In (<i>,COMPLEX) by A12;
then A14: (n |-> <i>) . 1 = In (<i>,COMPLEX)
.= <i> ;
A15: (n |-> (In (<i>,COMPLEX))) . 1 = <i> by A14;
rng (n |-> (In (<i>,COMPLEX))) = {<i>}

A16: rng (n |-> (In (<i>,COMPLEX))) c= {<i>}

let y3 be object ; :: according to TARSKI:def 3 :: thesis:
assume y3 in rng (n |-> (In (<i>,COMPLEX))) ; :: thesis:
then consider x3 being object such that
A17: ( x3 in dom (n |-> (In (<i>,COMPLEX))) & (n |-> (In (<i>,COMPLEX))) . x3 = y3 ) by FUNCT_1:def 3;
x3 in dom (n |-> (In (<i>,COMPLEX))) by A17;
then x3 in Seg n by A13, A8;
then x3 in Seg n ;
then A18: (n |-> (In (<i>,COMPLEX))) . x3 = In (<i>,COMPLEX) by FUNCOP_1:7;
(n |-> <i>) . x3 = In (<i>,COMPLEX) by A18
.= <i> ;
then A19: (n |-> (In (<i>,COMPLEX))) . x3 = <i> ;
A20: ( x3 in dom (n |-> (In (<i>,COMPLEX))) & (n |-> (In (<i>,COMPLEX))) . x3 = y3 ) by A17;
y3 = <i> by A20, A19;
hence y3 in {<i>} by TARSKI:def 1; :: thesis:

end;

{<i>} c= rng (n |-> (In (<i>,COMPLEX)))

let y3 be object ; :: according to TARSKI:def 3 :: thesis:
assume y3 in {<i>} ; :: thesis:
then A21: y3 = <i> by TARSKI:def 1;
A22: 1 in dom (n |-> (In (<i>,COMPLEX))) by A11;
( 1 in dom (n |-> (In (<i>,COMPLEX))) & (n |-> (In (<i>,COMPLEX))) . 1 = y3 ) by A21, A22, A15;
hence y3 in rng (n |-> (In (<i>,COMPLEX))) by FUNCT_1:def 3; :: thesis:

end;

hence rng (n |-> (In (<i>,COMPLEX))) = {<i>} by A16; :: thesis:

end;

hence ( rng (i* n) = {<i>} & ex f2 being Function st
( dom f2 = Seg n & rng f2 c= COMPLEX ) ) by A9; :: thesis:

end;

theorem Th28: :: MOMENTM1:28

for n being Nat holds Funcs ((Seg n),REAL) c= Funcs ((Seg n),COMPLEX) by Th22;

theorem Th29: :: MOMENTM1:29

for n being Nat st 1 <= n holds
( i* n in Funcs ((Seg n),COMPLEX) & not i* n in Funcs ((Seg n),REAL) )

let n be Nat; :: thesis:
assume A1: 1 <= n ; :: thesis:
n -tuples_on COMPLEX = Funcs ((Seg n),COMPLEX) by FINSEQ_2:93;
then A2: i* n in Funcs ((Seg n),COMPLEX) ;
1 in { k where k is Nat : ( 1 <= k & k <= n ) } by A1;
then A3: 1 in Seg n ;
A4: not <i> in REAL by Th4;

assume A5: i* n in Funcs ((Seg n),REAL) ; :: thesis:
consider f being Function such that
A6: ( i* n = f & dom f = Seg n & rng f c= REAL ) by A5, FUNCT_2:def 2;
1 in Seg n by A3;
then A7: (i* n) . 1 in rng (i* n) by A6, FUNCT_1:def 3;
(i* n) . 1 in {<i>} by A7, A1, Th27;
then A8: (i* n) . 1 = <i> by TARSKI:def 1;
<i> in REAL by A8, A7, A6;
hence contradiction by A4; :: thesis:

end;

then not i* n in Funcs ((Seg n),REAL) ;
hence ( i* n in Funcs ((Seg n),COMPLEX) & not i* n in Funcs ((Seg n),REAL) ) by A2; :: thesis:

end;

theorem Th30: :: MOMENTM1:30

for n being Nat st 1 <= n holds
Funcs ((Seg n),REAL) c< Funcs ((Seg n),COMPLEX)

let n be Nat; :: thesis:
assume A1: 1 <= n ; :: thesis:
A2: Funcs ((Seg n),REAL) c= Funcs ((Seg n),COMPLEX) by Th28;

assume A3: Funcs ((Seg n),REAL) = Funcs ((Seg n),COMPLEX) ; :: thesis:
i* n in Funcs ((Seg n),COMPLEX) by Th29, A1;
hence contradiction by A3, Th29, A1; :: thesis:

end;

hence Funcs ((Seg n),REAL) c< Funcs ((Seg n),COMPLEX) by A2; :: thesis:

end;

theorem Th31: :: MOMENTM1:31

for n being Nat st n >= 1 holds
n -tuples_on REAL c< n -tuples_on COMPLEX

let n be Nat; :: thesis:
assume A1: n >= 1 ; :: thesis:
A2: Funcs ((Seg n),REAL) = n -tuples_on REAL by Th17;
Funcs ((Seg n),COMPLEX) = n -tuples_on COMPLEX by Th18;
hence n -tuples_on REAL c< n -tuples_on COMPLEX by A1, A2, Th30; :: thesis:

end;

theorem :: MOMENTM1:32

for n being Nat st n >= 1 holds
REAL n c< COMPLEX n by Th31;