:: Cauchy Mean Theorem
:: by Adam Grabowski
::
:: Received June 13, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users

theorem ProdMon: :: RVSUM_3:1

for x, y, z, w being Real st |.(x - y).| < |.(z - w).| holds
(x - y) ^2 < (z - w) ^2

proof end;

theorem :: RVSUM_3:2

for x, y, z, w being Real st |.(x - y).| < |.(z - w).| & x + y = z + w holds
x * y > z * w

proof end;

notation

let f be real-valued FinSequence;
synonym positive f for positive-yielding ;

end;

definition

let f be real-valued FinSequence;

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
( f is positive iff for n being Nat st n in dom f holds
f . n > 0 )

proof end;

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 );

registration

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₁ being real-valued FinSequence st
( not b₁ is empty & b₁ is constant & b₁ is positive )

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₁ being real-valued FinSequence st
( not b₁ is empty & not b₁ is constant & b₁ is positive )

proof end;

end;

registration

let f be non empty real-valued FinSequence;
let n be Nat;

cluster f | (Seg n) -> real-valued ;

coherence
f | (Seg n) is real-valued ;

end;

registration

let f be non empty real-valued positive FinSequence;
let n be Nat;

cluster f | (Seg n) -> positive ;

coherence
f | (Seg n) is positive

proof end;

end;

notation

let f be FinSequence;
synonym homogeneous f for constant ;

end;

notation

let f be FinSequence;
antonym heterogeneous f for homogeneous ;

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

proof end;

theorem :: RVSUM_3:4

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

proof end;

definition

let f be real-valued FinSequence;

func Mean f -> real number equals :: RVSUM_3:def 2
(Sum f) / (len f);

coherence
(Sum f) / (len f) is real number ;

end;

:: deftheorem defines Mean RVSUM_3:def 2 :
for f being real-valued FinSequence holds Mean f = (Sum f) / (len f);

definition

let f be real-valued positive FinSequence;

func GMean f -> real number equals :: RVSUM_3:def 3
(len f) -root (Product f);

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

end;

:: deftheorem defines GMean RVSUM_3:def 3 :
for f being real-valued positive FinSequence holds GMean f = (len f) -root (Product f);

theorem Huk1: :: RVSUM_3:5

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

proof end;

theorem :: RVSUM_3:6

for f being real-valued FinSequence holds Mean (f ^ <*(Mean f)*>) = Mean f

proof end;

registration

let f be constant non empty real-valued FinSequence;

cluster the_value_of f -> real ;

coherence
the_value_of f is real

proof end;

end;

theorem ConstantSum: :: RVSUM_3:7

for f being constant non empty real-valued FinSequence holds Sum f = (the_value_of f) * (len f)

proof 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;

theorem ConstantMean: :: RVSUM_3:9

for f being constant non empty real-valued FinSequence holds Mean f = the_value_of f

proof end;

theorem PosLeq: :: RVSUM_3:10

for f being constant non empty real-valued positive FinSequence holds the_value_of f > 0

proof end;

theorem ConstantGMean: :: RVSUM_3:11

for f being constant non empty real-valued positive FinSequence holds GMean f = the_value_of f

proof end;

registration

let f be non empty real-valued positive FinSequence;

cluster Mean f -> real positive ;

coherence
Mean f is positive

proof end;

end;

registration

let f be non empty real-valued positive FinSequence;

cluster Product f -> positive ;

coherence
Product f is positive

proof end;

end;

registration

let f be non empty real-valued positive FinSequence;

cluster GMean f -> real positive ;

coherence
GMean f is positive

proof end;

end;

definition

let f be real-valued FinSequence;

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 ) } is Subset of NAT

proof end;

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 ) } ;

registration

let f be real-valued FinSequence;

cluster HetSet f -> finite ;

coherence
HetSet f is finite

proof end;

end;

registration

let f be non empty real-valued positive FinSequence;

cluster HetSet f -> real-membered bounded_below bounded_above ;

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

end;

definition

let f be real-valued FinSequence;

func Het f -> Nat equals :: RVSUM_3:def 5
card (HetSet f);

coherence
card (HetSet f) is Nat ;

end;

:: deftheorem defines Het RVSUM_3:def 5 :
for f being real-valued FinSequence holds Het f = card (HetSet f);

theorem HetHomo: :: RVSUM_3:12

for f being real-valued FinSequence st Het f = 0 holds
f is homogeneous

proof end;

theorem HetHetero: :: RVSUM_3:13

for f being non empty real-valued FinSequence st Het f <> 0 holds
f is heterogeneous

proof end;

registration

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

cluster HetSet f -> non empty ;

coherence
not HetSet f is empty

proof end;

end;

theorem HetBase: :: RVSUM_3:14

for f being homogeneous non empty real-valued positive FinSequence holds Mean f = GMean f

proof end;

definition

let f1, f2 be real-valued FinSequence;

pred f1,f2 are_gamma-equivalent means :: RVSUM_3:def 6
( len f1 = len f2 & Mean f1 = Mean f2 );

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;

:: 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 ) );

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;

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

definition

let f be real-valued FinSequence;

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 ) } 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 ) } is Subset of NAT

proof end;

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 ) } ;

:: 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 ) } ;

theorem :: RVSUM_3:16

for f being real-valued FinSequence holds HetSet f c= dom f

proof end;

theorem LessDom: :: RVSUM_3:17

for f being real-valued FinSequence holds MeanLess f c= dom f

proof end;

theorem MoreDom: :: RVSUM_3:18

for f being real-valued FinSequence holds MeanMore f c= dom f

proof end;

theorem MeanSum: :: RVSUM_3:19

for f being real-valued FinSequence holds HetSet f = (MeanLess f) \/ (MeanMore f)

proof end;

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;

cluster MeanLess f -> non empty ;

coherence
not MeanLess f is empty by MeanL;

cluster MeanMore f -> non empty ;

coherence
not MeanMore f is empty by MeanM;

end;

registration

let f be homogeneous real-valued FinSequence;

cluster MeanLess f -> empty ;

coherence
MeanLess f is empty

proof end;

cluster MeanMore f -> empty ;

coherence
MeanMore f is empty

proof end;

end;

theorem MeanMiss: :: RVSUM_3:20

for f being heterogeneous non empty real-valued FinSequence holds MeanLess f misses MeanMore f

proof end;

theorem :: RVSUM_3:21

for f being heterogeneous non empty real-valued FinSequence holds Het f >= 2

proof end;

definition

let f be Function;
let i, j be Nat;
let a, b be object ;

func Replace (f,i,j,a,b) -> Function equals :: RVSUM_3:def 9
(f +* (i,a)) +* (j,b);

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

end;

:: 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);

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

proof end;

registration

let f be real-valued FinSequence;
let i, j be Nat;
let a, b be Real;

cluster Replace (f,i,j,a,b) -> real-valued FinSequence-like ;

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

end;

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)

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

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)

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

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))

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

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

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

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

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))))

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

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 )

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

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

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 ) )

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 )

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 )

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 )

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 )

proof end;

definition

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

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 b₁ being real-valued FinSequence ex i, j being Nat st
( i = the Element of MeanLess f & j = the Element of MeanMore f & b₁ = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) )

proof end;

uniqueness
for b₁, b₂ being real-valued FinSequence st ex i, j being Nat st
( i = the Element of MeanLess f & j = the Element of MeanMore f & b₁ = 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₂ = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) ) holds
b₁ = b₂ ;

end;

:: deftheorem HomDef defines Homogen RVSUM_3:def 10 :
for f being heterogeneous non empty real-valued positive FinSequence
for b₂ being real-valued FinSequence holds
( b₂ = Homogen f iff ex i, j being Nat st
( i = the Element of MeanLess f & j = the Element of MeanMore f & b₂ = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) ) );

theorem DomHomogen: :: RVSUM_3:42

for f being heterogeneous non empty real-valued positive FinSequence holds dom (Homogen f) = dom f

proof end;

registration

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

cluster Homogen f -> non empty real-valued ;

coherence
not Homogen f is empty

proof end;

end;

registration

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

cluster Homogen f -> real-valued positive ;

coherence
Homogen f is positive

proof end;

end;

theorem HomogenHet: :: RVSUM_3:43

for f being heterogeneous non empty real-valued positive FinSequence holds Het (Homogen f) < Het f

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 )

proof end;

theorem :: RVSUM_3:47

for f being non empty real-valued positive FinSequence holds GMean f <= Mean f

proof end;