:: by Adam Grabowski

::

:: Received June 13, 2014

:: Copyright (c) 2014-2021 Association of Mizar Users

definition

let f be real-valued FinSequence;

( f is positive iff for n being Nat st n in dom f holds

f . n > 0 )

end;
redefine attr f is positive-yielding means :PosDef: :: RVSUM_3:def 1

for n being Nat st n in dom f holds

f . n > 0 ;

compatibility for n being Nat st n in dom f holds

f . n > 0 ;

( f is positive iff for n being Nat st n in dom f holds

f . n > 0 )

proof end;

:: deftheorem PosDef defines positive RVSUM_3:def 1 :

for f being real-valued FinSequence holds

( f is positive iff for n being Nat st n in dom f holds

f . n > 0 );

for f being real-valued FinSequence holds

( f is positive iff for n being Nat st n in dom f holds

f . n > 0 );

registration

ex b_{1} being real-valued FinSequence st

( not b_{1} is empty & b_{1} is constant & b_{1} is positive )

ex b_{1} being real-valued FinSequence st

( not b_{1} is empty & not b_{1} is constant & b_{1} is positive )
end;

cluster Relation-like omega -defined Function-like constant non empty complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like positive for set ;

existence ex b

( not b

proof end;

cluster Relation-like omega -defined Function-like non constant non empty complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like positive for set ;

existence ex b

( not b

proof end;

registration
end;

registration

let f be non empty real-valued positive FinSequence;

let n be Nat;

coherence

f | (Seg n) is positive

end;
let n be Nat;

coherence

f | (Seg n) is positive

proof end;

theorem Th83: :: RVSUM_3:3

for R1, R2 being real-valued FinSequence st len R1 = len R2 & ( for j being Nat st j in Seg (len R1) holds

R1 . j <= R2 . j ) & ex j being Nat st

( j in Seg (len R1) & R1 . j < R2 . j ) holds

Sum R1 < Sum R2

R1 . j <= R2 . j ) & ex j being Nat st

( j in Seg (len R1) & R1 . j < R2 . j ) holds

Sum R1 < Sum R2

proof end;

theorem :: RVSUM_3:4

for R1, R2 being real-valued FinSequence st R1,R2 are_fiberwise_equipotent holds

Product R1 = Product R2

Product R1 = Product R2

proof end;

:: deftheorem defines Mean RVSUM_3:def 2 :

for f being real-valued FinSequence holds Mean f = (Sum f) / (len f);

for f being real-valued FinSequence holds Mean f = (Sum f) / (len f);

definition

let f be real-valued positive FinSequence;

coherence

(len f) -root (Product f) is real number by TARSKI:1;

end;
coherence

(len f) -root (Product f) is real number by TARSKI:1;

:: deftheorem defines GMean RVSUM_3:def 3 :

for f being real-valued positive FinSequence holds GMean f = (len f) -root (Product f);

for f being real-valued positive FinSequence holds GMean f = (len f) -root (Product f);

registration
end;

theorem ConstantProduct: :: RVSUM_3:8

for f being constant non empty real-valued FinSequence holds Product f = (the_value_of f) |^ (len f)

proof end;

registration
end;

registration
end;

registration
end;

definition

let f be real-valued FinSequence;

{ n where n is Nat : ( n in dom f & f . n <> Mean f ) } is Subset of NAT

end;
func HetSet f -> Subset of NAT equals :: RVSUM_3:def 4

{ n where n is Nat : ( n in dom f & f . n <> Mean f ) } ;

coherence { n where n is Nat : ( n in dom f & f . n <> Mean f ) } ;

{ n where n is Nat : ( n in dom f & f . n <> Mean f ) } is Subset of NAT

proof end;

:: deftheorem defines HetSet RVSUM_3:def 4 :

for f being real-valued FinSequence holds HetSet f = { n where n is Nat : ( n in dom f & f . n <> Mean f ) } ;

for f being real-valued FinSequence holds HetSet f = { n where n is Nat : ( n in dom f & f . n <> Mean f ) } ;

registration

let f be non empty real-valued positive FinSequence;

coherence

( HetSet f is bounded_above & HetSet f is bounded_below & HetSet f is real-membered ) ;

end;
coherence

( HetSet f is bounded_above & HetSet f is bounded_below & HetSet f is real-membered ) ;

:: deftheorem defines Het RVSUM_3:def 5 :

for f being real-valued FinSequence holds Het f = card (HetSet f);

for f being real-valued FinSequence holds Het f = card (HetSet f);

registration

let f be heterogeneous non empty real-valued positive FinSequence;

coherence

not HetSet f is empty

end;
coherence

not HetSet f is empty

proof end;

definition

let f1, f2 be real-valued FinSequence;

reflexivity

for f1 being real-valued FinSequence holds

( len f1 = len f1 & Mean f1 = Mean f1 ) ;

symmetry

for f1, f2 being real-valued FinSequence st len f1 = len f2 & Mean f1 = Mean f2 holds

( len f2 = len f1 & Mean f2 = Mean f1 ) ;

end;
reflexivity

for f1 being real-valued FinSequence holds

( len f1 = len f1 & Mean f1 = Mean f1 ) ;

symmetry

for f1, f2 being real-valued FinSequence st len f1 = len f2 & Mean f1 = Mean f2 holds

( len f2 = len f1 & Mean f2 = Mean f1 ) ;

:: deftheorem defines are_gamma-equivalent RVSUM_3:def 6 :

for f1, f2 being real-valued FinSequence holds

( f1,f2 are_gamma-equivalent iff ( len f1 = len f2 & Mean f1 = Mean f2 ) );

for f1, f2 being real-valued FinSequence holds

( f1,f2 are_gamma-equivalent iff ( len f1 = len f2 & Mean f1 = Mean f2 ) );

theorem :: RVSUM_3:15

for f1, f2 being real-valued FinSequence st dom f1 = dom f2 & Sum f1 = Sum f2 holds

f1,f2 are_gamma-equivalent by FINSEQ_3:29;

f1,f2 are_gamma-equivalent by FINSEQ_3:29;

:: Transitivity of gamma-equivalence is obvious for the Mizar checker

definition

let f be real-valued FinSequence;

{ n where n is Nat : ( n in dom f & f . n < Mean f ) } is Subset of NAT

{ n where n is Nat : ( n in dom f & f . n > Mean f ) } is Subset of NAT

end;
func MeanLess f -> Subset of NAT equals :: RVSUM_3:def 7

{ n where n is Nat : ( n in dom f & f . n < Mean f ) } ;

coherence { n where n is Nat : ( n in dom f & f . n < Mean f ) } ;

{ n where n is Nat : ( n in dom f & f . n < Mean f ) } is Subset of NAT

proof end;

func MeanMore f -> Subset of NAT equals :: RVSUM_3:def 8

{ n where n is Nat : ( n in dom f & f . n > Mean f ) } ;

coherence { n where n is Nat : ( n in dom f & f . n > Mean f ) } ;

{ n where n is Nat : ( n in dom f & f . n > Mean f ) } is Subset of NAT

proof end;

:: deftheorem defines MeanLess RVSUM_3:def 7 :

for f being real-valued FinSequence holds MeanLess f = { n where n is Nat : ( n in dom f & f . n < Mean f ) } ;

for f being real-valued FinSequence holds MeanLess f = { n where n is Nat : ( n in dom f & f . n < Mean f ) } ;

:: deftheorem defines MeanMore RVSUM_3:def 8 :

for f being real-valued FinSequence holds MeanMore f = { n where n is Nat : ( n in dom f & f . n > Mean f ) } ;

for f being real-valued FinSequence holds MeanMore f = { n where n is Nat : ( n in dom f & f . n > Mean f ) } ;

MeanL: for f being heterogeneous real-valued FinSequence holds MeanLess f <> {}

proof end;

MeanM: for f being heterogeneous real-valued FinSequence holds MeanMore f <> {}

proof end;

registration

let f be heterogeneous real-valued FinSequence;

coherence

not MeanLess f is empty by MeanL;

coherence

not MeanMore f is empty by MeanM;

end;
coherence

not MeanLess f is empty by MeanL;

coherence

not MeanMore f is empty by MeanM;

registration

let f be homogeneous real-valued FinSequence;

coherence

MeanLess f is empty

MeanMore f is empty

end;
coherence

MeanLess f is empty

proof end;

coherence MeanMore f is empty

proof end;

definition

let f be Function;

let i, j be Nat;

let a, b be object ;

coherence

(f +* (i,a)) +* (j,b) is Function ;

end;
let i, j be Nat;

let a, b be object ;

coherence

(f +* (i,a)) +* (j,b) is Function ;

:: deftheorem defines Replace RVSUM_3:def 9 :

for f being Function

for i, j being Nat

for a, b being object holds Replace (f,i,j,a,b) = (f +* (i,a)) +* (j,b);

for f being Function

for i, j being Nat

for a, b being object holds Replace (f,i,j,a,b) = (f +* (i,a)) +* (j,b);

theorem DinoDom: :: RVSUM_3:22

for f being FinSequence

for i, j being Nat

for a, b being object holds dom (Replace (f,i,j,a,b)) = dom f

for i, j being Nat

for a, b being object holds dom (Replace (f,i,j,a,b)) = dom f

proof end;

registration

let f be real-valued FinSequence;

let i, j be Nat;

let a, b be Real;

coherence

( Replace (f,i,j,a,b) is real-valued & Replace (f,i,j,a,b) is FinSequence-like ) ;

end;
let i, j be Nat;

let a, b be Real;

coherence

( Replace (f,i,j,a,b) is real-valued & Replace (f,i,j,a,b) is FinSequence-like ) ;

theorem CopyForValued: :: RVSUM_3:23

for w being real-valued FinSequence

for r being Real

for i being Nat st i in dom w holds

w +* (i,r) = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)

for r being Real

for i being Nat st i in dom w holds

w +* (i,r) = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)

proof end;

theorem SumA: :: RVSUM_3:24

for f being real-valued FinSequence

for i being Nat

for a being Real st i in dom f holds

Sum (f +* (i,a)) = ((Sum f) - (f . i)) + a

for i being Nat

for a being Real st i in dom f holds

Sum (f +* (i,a)) = ((Sum f) - (f . i)) + a

proof end;

theorem ProductA: :: RVSUM_3:25

for f being real-valued positive FinSequence

for i being Nat

for a being Real st i in dom f holds

Product (f +* (i,a)) = ((Product f) * a) / (f . i)

for i being Nat

for a being Real st i in dom f holds

Product (f +* (i,a)) = ((Product f) * a) / (f . i)

proof end;

theorem SumReplace: :: RVSUM_3:26

for f being real-valued FinSequence

for i, j being Nat

for a, b being Real st i in dom f & j in dom f & i <> j holds

Sum (Replace (f,i,j,a,b)) = ((((Sum f) - (f . i)) - (f . j)) + a) + b

for i, j being Nat

for a, b being Real st i in dom f & j in dom f & i <> j holds

Sum (Replace (f,i,j,a,b)) = ((((Sum f) - (f . i)) - (f . j)) + a) + b

proof end;

theorem ProdReplace: :: RVSUM_3:27

for f being real-valued positive FinSequence

for i, j being Nat

for a, b being positive Real st i in dom f & j in dom f & i <> j holds

Product (Replace (f,i,j,a,b)) = (((Product f) * a) * b) / ((f . i) * (f . j))

for i, j being Nat

for a, b being positive Real st i in dom f & j in dom f & i <> j holds

Product (Replace (f,i,j,a,b)) = (((Product f) * a) * b) / ((f . i) * (f . j))

proof end;

theorem ReplaceGamma: :: RVSUM_3:28

for f being real-valued FinSequence

for i, j being Nat st i in dom f & j in dom f & i <> j holds

f, Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) are_gamma-equivalent

for i, j being Nat st i in dom f & j in dom f & i <> j holds

f, Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) are_gamma-equivalent

proof end;

theorem ReplaceValue: :: RVSUM_3:29

for f being real-valued FinSequence

for i, j, k being Nat

for a, b being Real st i in dom f & j in dom f & k in dom f & i <> j & k <> i & k <> j holds

(Replace (f,i,j,a,b)) . k = f . k

for i, j, k being Nat

for a, b being Real st i in dom f & j in dom f & k in dom f & i <> j & k <> i & k <> j holds

(Replace (f,i,j,a,b)) . k = f . k

proof end;

theorem ReplaceValue2: :: RVSUM_3:30

for f being FinSequence

for i, j being Nat

for a, b being object st i in dom f & j in dom f & i <> j holds

(Replace (f,i,j,a,b)) . j = b

for i, j being Nat

for a, b being object st i in dom f & j in dom f & i <> j holds

(Replace (f,i,j,a,b)) . j = b

proof end;

theorem ReplaceValue3: :: RVSUM_3:31

for f being FinSequence

for i, j being Nat

for a, b being object st i in dom f & j in dom f & i <> j holds

(Replace (f,i,j,a,b)) . i = a

for i, j being Nat

for a, b being object st i in dom f & j in dom f & i <> j holds

(Replace (f,i,j,a,b)) . i = a

proof end;

theorem HetMono: :: RVSUM_3:32

for f being real-valued FinSequence

for i, j being Nat st i in dom f & j in dom f & i <> j & f . i <> Mean f & f . j <> Mean f holds

Het f > Het (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))))

for i, j being Nat st i in dom f & j in dom f & i <> j & f . i <> Mean f & f . j <> Mean f holds

Het f > Het (Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))))

proof end;

theorem ProdGMean: :: RVSUM_3:33

for f, g being non empty real-valued positive FinSequence st len f = len g & Product f < Product g holds

GMean f < GMean g

GMean f < GMean g

proof end;

theorem ExDiff: :: RVSUM_3:34

for f being heterogeneous non empty real-valued positive FinSequence ex i, j being Nat st

( i in dom f & j in dom f & i <> j & f . i < Mean f & Mean f < f . j )

( i in dom f & j in dom f & i <> j & f . i < Mean f & Mean f < f . j )

proof end;

theorem ReplacePositive: :: RVSUM_3:35

for f being heterogeneous non empty real-valued positive FinSequence

for i, j being Nat st i in dom f & j in dom f & i <> j & f . i > Mean f holds

Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) is positive

for i, j being Nat st i in dom f & j in dom f & i <> j & f . i > Mean f holds

Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) is positive

proof end;

theorem ReplacePositive2: :: RVSUM_3:36

for f being heterogeneous non empty real-valued positive FinSequence

for i, j being Nat st i in dom f & j in dom f & i <> j & f . j > Mean f holds

Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) is positive

for i, j being Nat st i in dom f & j in dom f & i <> j & f . j > Mean f holds

Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) is positive

proof end;

theorem :: RVSUM_3:37

for f being heterogeneous non empty real-valued positive FinSequence ex i, j being Nat st

( i in dom f & j in dom f & i <> j & ex g being non empty real-valued positive FinSequence st

( g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) & GMean f < GMean g ) )

( i in dom f & j in dom f & i <> j & ex g being non empty real-valued positive FinSequence st

( g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) & GMean f < GMean g ) )

proof end;

theorem BlaBla: :: RVSUM_3:38

for f being heterogeneous non empty real-valued FinSequence

for i, j being Nat st i = the Element of MeanLess f & j = the Element of MeanMore f holds

( i in dom f & j in dom f & i <> j & f . i < Mean f & f . j > Mean f )

for i, j being Nat st i = the Element of MeanLess f & j = the Element of MeanMore f holds

( i in dom f & j in dom f & i <> j & f . i < Mean f & f . j > Mean f )

proof end;

theorem BlaBla2: :: RVSUM_3:39

for f being heterogeneous non empty real-valued positive FinSequence

for i, j being object st i in MeanLess f & j in MeanMore f holds

( i in dom f & j in dom f & i <> j & f . i < Mean f & f . j > Mean f )

for i, j being object st i in MeanLess f & j in MeanMore f holds

( i in dom f & j in dom f & i <> j & f . i < Mean f & f . j > Mean f )

proof end;

theorem :: RVSUM_3:40

for f being heterogeneous non empty real-valued positive FinSequence

for i, j being Nat st i in dom f & j in dom f & i <> j & i in MeanMore f & j in MeanLess f holds

ex g being non empty real-valued positive FinSequence st

( g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) & GMean f < GMean g )

for i, j being Nat st i in dom f & j in dom f & i <> j & i in MeanMore f & j in MeanLess f holds

ex g being non empty real-valued positive FinSequence st

( g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) & GMean f < GMean g )

proof end;

theorem ReplaceGMean3: :: RVSUM_3:41

for f being heterogeneous non empty real-valued positive FinSequence

for i, j being Nat st i in dom f & j in dom f & i <> j & j in MeanMore f & i in MeanLess f holds

ex g being non empty real-valued positive FinSequence st

( g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) & GMean f < GMean g )

for i, j being Nat st i in dom f & j in dom f & i <> j & j in MeanMore f & i in MeanLess f holds

ex g being non empty real-valued positive FinSequence st

( g = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) & GMean f < GMean g )

proof end;

definition

let f be heterogeneous non empty real-valued positive FinSequence;

ex b_{1} being real-valued FinSequence ex i, j being Nat st

( i = the Element of MeanLess f & j = the Element of MeanMore f & b_{1} = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) )

for b_{1}, b_{2} being real-valued FinSequence st ex i, j being Nat st

( i = the Element of MeanLess f & j = the Element of MeanMore f & b_{1} = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) ) & ex i, j being Nat st

( i = the Element of MeanLess f & j = the Element of MeanMore f & b_{2} = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) ) holds

b_{1} = b_{2}
;

end;
func Homogen f -> real-valued FinSequence means :HomDef: :: RVSUM_3:def 10

ex i, j being Nat st

( i = the Element of MeanLess f & j = the Element of MeanMore f & it = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) );

existence ex i, j being Nat st

( i = the Element of MeanLess f & j = the Element of MeanMore f & it = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) );

ex b

( i = the Element of MeanLess f & j = the Element of MeanMore f & b

proof end;

uniqueness for b

( i = the Element of MeanLess f & j = the Element of MeanMore f & b

( i = the Element of MeanLess f & j = the Element of MeanMore f & b

b

:: deftheorem HomDef defines Homogen RVSUM_3:def 10 :

for f being heterogeneous non empty real-valued positive FinSequence

for b_{2} being real-valued FinSequence holds

( b_{2} = Homogen f iff ex i, j being Nat st

( i = the Element of MeanLess f & j = the Element of MeanMore f & b_{2} = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) ) );

for f being heterogeneous non empty real-valued positive FinSequence

for b

( b

( i = the Element of MeanLess f & j = the Element of MeanMore f & b

registration

let f be heterogeneous non empty real-valued positive FinSequence;

coherence

not Homogen f is empty

end;
coherence

not Homogen f is empty

proof end;

registration

let f be heterogeneous non empty real-valued positive FinSequence;

coherence

Homogen f is positive

end;
coherence

Homogen f is positive

proof end;

theorem HomEqui: :: RVSUM_3:44

for f being heterogeneous non empty real-valued positive FinSequence holds Homogen f,f are_gamma-equivalent

proof end;

theorem HomGMean: :: RVSUM_3:45

for f being heterogeneous non empty real-valued positive FinSequence holds GMean (Homogen f) > GMean f

proof end;

theorem WOWTheo: :: RVSUM_3:46

for f being heterogeneous non empty real-valued positive FinSequence ex g being homogeneous non empty real-valued positive FinSequence st

( GMean g > GMean f & Mean g = Mean f )

( GMean g > GMean f & Mean g = Mean f )

proof end;