:: Cauchy Mean Theorem
::
:: 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 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
existence
ex b1 being real-valued FinSequence st
( not b1 is empty & b1 is constant & b1 is positive )
proof end;
existence
ex b1 being real-valued FinSequence st
( not b1 is empty & not b1 is constant & b1 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 ();
coherence
(len f) -root () 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 ();

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

theorem ConstantSum: :: RVSUM_3:7
for f being constant non empty real-valued FinSequence holds Sum f = () * (len f)
proof end;

theorem ConstantProduct: :: RVSUM_3:8
for f being constant non empty real-valued FinSequence holds Product 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;
coherence
Mean f is positive
proof end;
end;

registration
let f be non empty real-valued positive FinSequence;
coherence
proof end;
end;

registration
let f be non empty real-valued positive FinSequence;
coherence
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;
coherence
HetSet f is finite
proof end;
end;

registration
let f be non empty real-valued positive FinSequence;
coherence ;
end;

definition
let f be real-valued FinSequence;
func Het f -> Nat equals :: RVSUM_3:def 5
card ();
coherence
card () is Nat
;
end;

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

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 = () \/ ()
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;
coherence
proof end;
coherence
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)) = (() * 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)) = ((() * 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 b1 being real-valued FinSequence ex i, j being Nat st
( i = the Element of MeanLess f & j = the Element of MeanMore f & b1 = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) )
proof end;
uniqueness
for b1, b2 being real-valued FinSequence st ex i, j being Nat st
( i = the Element of MeanLess f & j = the Element of MeanMore f & b1 = 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 & b2 = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) ) holds
b1 = b2
;
end;

:: deftheorem HomDef defines Homogen RVSUM_3:def 10 :
for f being heterogeneous non empty real-valued positive FinSequence
for b2 being real-valued FinSequence holds
( b2 = Homogen f iff ex i, j being Nat st
( i = the Element of MeanLess f & j = the Element of MeanMore f & b2 = 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 () = dom f
proof end;

registration
let f be heterogeneous non empty real-valued positive FinSequence;
coherence
not Homogen f is empty
proof end;
end;

registration
let f be heterogeneous non empty real-valued positive FinSequence;
coherence
proof end;
end;

theorem HomogenHet: :: RVSUM_3:43
for f being heterogeneous non empty real-valued positive FinSequence holds Het () < 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 () > 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;