:: Cauchy Mean Theorem
:: by Adam Grabowski
::
:: Received June 13, 2014
:: Copyright (c) 2014-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, FINSEQ_1, VALUED_0, FINSEQ_2, CARD_1, RELAT_1,
SUBSET_1, XBOOLE_0, FUNCT_1, TARSKI, XREAL_0, ORDINAL4, ARYTM_1, ARYTM_3,
SQUARE_1, FUNCOP_1, REAL_1, XXREAL_0, CARD_3, COMPLEX1, PREPOWER,
ORDINAL1, RVSUM_3, POWER, UNIALG_1, FINSET_1, NEWTON, AFINSQ_1, FUNCT_4,
CLASSES1, PARTFUN3, RFINSEQ, XXREAL_2, MEMBERED;
notations TARSKI, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_2, VALUED_0,
XBOOLE_0, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, SQUARE_1, NAT_D, NAT_1,
RELAT_1, FUNCT_1, PARTFUN1, SETWISEO, FUNCT_2, MEMBERED, BINOP_1,
FINSET_1, CLASSES1, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, VALUED_1,
FINSOP_1, PBOOLE, PREPOWER, FUNCT_4, SERIES_1, FINSEQ_7, SEQ_4, NEWTON,
POWER, RVSUM_1, FUNCT_7, RFINSEQ, COMPLEX1, PARTFUN3;
constructors PARTFUN1, BINOP_1, SETWISEO, SQUARE_1, NAT_1, BINOP_2, MEMBERED,
XXREAL_2, VALUED_1, FINSEQOP, FINSEQ_4, FINSOP_1, SETWOP_2, RELSET_1,
XXREAL_1, REAL_1, FINSEQ_2, RVSUM_1, POWER, FINSET_1, NEWTON, ABIAN,
RFINSEQ, PBOOLE, NAT_D, XREAL_0, CARD_1, CARD_2, SEQ_4, FUNCT_4, FUNCT_7,
CLASSES1, SERIES_1, SERIES_3, SEQ_1, PREPOWER, FINSEQ_7, PARTFUN3;
registrations XBOOLE_0, FUNCT_1, NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, NAT_1,
FINSEQ_1, FINSEQ_2, VALUED_0, RELAT_1, CARD_1, RVSUM_1, FUNCT_7,
FINSET_1, XXREAL_2, XXREAL_0, MEMBERED, COMPLEX1, FINSEQ_6, PDIFF_7;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
definitions TARSKI, XBOOLE_0;
equalities FINSEQ_1, SQUARE_1, FINSEQ_2, ORDINAL1, RELAT_1;
expansions FINSEQ_1, TARSKI, CLASSES1, XBOOLE_0, SEQM_3, PARTFUN3;
theorems SQUARE_1, FUNCT_1, FINSEQ_1, FUNCOP_1, FINSEQ_2, RELAT_1, XREAL_0,
ZFMISC_1, XREAL_1, XBOOLE_1, FINSEQ_3, CARD_1, TARSKI, RVSUM_1, XCMPLX_1,
FINSEQ_5, POWER, NAT_1, NEWTON, FUNCT_7, RFINSEQ, CLASSES1, XXREAL_0,
COMPLEX1, NAT_4, CARD_2, XBOOLE_0, PREPOWER;
schemes NAT_1;
begin :: Preliminaries
theorem ProdMon:
for x, y, z, w being Real st
|. x - y .| < |. z - w .| holds
(x - y) ^2 < (z - w) ^2
proof
let x, y, z, w be Real;
A2: |. x - y .| ^2 = (x - y) ^2 by COMPLEX1:75;
assume |. x - y .| < |. z - w .|; then
|. x - y .| ^2 < |. z - w .| ^2 by SQUARE_1:16;
hence thesis by COMPLEX1:75,A2;
end;
theorem
for x, y, z, w being Real st
|. x - y .| < |. z - w .| & x + y = z + w holds
x * y > z * w
proof
let x, y, z, w be Real;
assume
A1: |. x - y .| < |. z - w .| & x + y = z + w;
(x - y) ^2 < (z - w) ^2 by A1,ProdMon; then
(x + y) ^2 - (x - y) ^2 > (z + w) ^2 - (z - w) ^2
by A1,XREAL_1:15; then
4 * (x * y) > 4 * (z * w);
hence thesis by XREAL_1:64;
end;
notation let f be real-valued FinSequence;
synonym f is positive for f is positive-yielding;
end;
definition let f be real-valued FinSequence;
redefine attr f is positive means :PosDef: :: redefines positive (RVSUM_3, synonym) → positive-yielding (PARTFUN3, definition)
for n being Nat st n in dom f holds f.n > 0;
compatibility
proof
thus f is positive implies
for n being Nat st n in dom f holds f.n > 0 by FUNCT_1:3;
assume
A3: for n being Nat st n in dom f holds f.n > 0;
for r being Real st r in rng f holds 0 < r
proof
let r be Real;
assume r in rng f; then
consider x being object such that
A2: x in dom f & r = f.x by FUNCT_1:def 3;
reconsider n = x as Nat by A2;
thus thesis by A2,A3;
end;
hence thesis;
end;
end;
registration
cluster non empty constant positive for real-valued FinSequence;
existence
proof
set f = <*1*>;
for n being Nat st n in dom f holds f.n > 0
proof
let n be Nat;
assume n in dom f; then
n in {1} by FINSEQ_1:2,FINSEQ_1:38; then
n = 1 by TARSKI:def 1;
hence thesis;
end; then
f is non empty positive;
hence thesis;
end;
cluster non empty non constant positive for real-valued FinSequence;
existence
proof
set f = <*1,2*>;
for n being Nat st n in dom f holds f.n > 0
proof
let n be Nat;
assume n in dom f; then
n in Seg len f by FINSEQ_1:def 3; then
n in {1,2} by FINSEQ_1:2,FINSEQ_1:44; then
n = 1 or n = 2 by TARSKI:def 2;
hence thesis;
end; then
A1: f is non empty positive;
dom f = {1,2} by FINSEQ_1:92; then
A2: 1 in dom f & 2 in dom f by TARSKI:def 2;
f.1 = 1 & f.2 = 2; then
f is non constant by A2;
hence thesis by A1;
end;
end;
registration
let f be real-valued FinSequence;
let n be Nat;
cluster f | Seg n -> real-valued;
coherence;
end;
registration
let f be positive real-valued FinSequence;
let n be Nat;
cluster f | Seg n -> positive;
coherence
proof
set g = f | Seg n;
let k be Nat;
A1: dom g c= dom f by RELAT_1:60;
assume
A2: k in dom g; then
f.k > 0 by PosDef,A1;
hence thesis by FUNCT_1:47,A2;
end;
end;
notation let f be FinSequence;
synonym f is homogeneous for f is constant;
end;
notation let f be FinSequence;
antonym f is heterogeneous↑ for f is homogeneous;
end;
theorem Th83:
for R1, R2 being real-valued FinSequence st
len R1 = len R2 &
(for j be Nat st j in Seg len R1 holds R1.j <= R2.j) &
(ex j be Nat st j in Seg len R1 & R1.j < R2.j) holds
Sum R1 < Sum R2
proof
let R1, R2 be real-valued FinSequence;
set i = len R1;
assume
A1: len R1 = len R2 &
(for j be Nat st j in Seg i holds R1.j <= R2.j) &
(ex j be Nat st j in Seg i & R1.j < R2.j);
reconsider w = len R1 as natural Number;
R1 is FinSequence of REAL & R2 is FinSequence of REAL by RVSUM_1:145; then
reconsider r1 = R1, r2 = R2 as Element of w-tuples_on REAL
by A1,FINSEQ_2:92;
Sum r1 < Sum r2 by A1,RVSUM_1:83;
hence thesis;
end;
theorem ::: An analogue of RFINSEQ for Products - EULER_2 change for Functions
for R1,R2 being real-valued FinSequence st R1,R2 are_fiberwise_equipotent
holds Product R1 = Product R2
proof
let R1,R2 be real-valued FinSequence;
defpred P[Nat] means for f,g be FinSequence of REAL st f,g
are_fiberwise_equipotent & len f = $1 holds Product f = Product g;
assume
A1: R1,R2 are_fiberwise_equipotent;
A2: len R1 = len R1;
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A4: P[n];
let f,g be FinSequence of REAL;
assume that
A5: f,g are_fiberwise_equipotent and
A6: len f = n+1;
set a = f.(n+1);
A7: rng f = rng g by A5,CLASSES1:75;
0 qua Nat + 1 <= n + 1 by NAT_1:13;
then n+1 in dom f by A6,FINSEQ_3:25;
then a in rng g by A7,FUNCT_1:def 3;
then consider m being Nat such that
A8: m in dom g and
A9: g.m = a by FINSEQ_2:10;
set gg = g/^m, gm = g|m;
A11: 1 <= m by A8,FINSEQ_3:25;
max(0,m-1) = m-1 by FINSEQ_2:4,A8,FINSEQ_3:25;
then reconsider m1 = m-1 as Element of NAT by FINSEQ_2:5;
m = m1+1; then
A13: Seg m1 c= Seg m by FINSEQ_1:5,NAT_1:11;
m in Seg m by A11; then
WW: a = gm.(m1+1) by A8,A9,RFINSEQ:6;
m <= len g by A8,FINSEQ_3:25; then
len gm = m by FINSEQ_1:59; then
A14:gm = (gm|m1)^<*a*> by WW,RFINSEQ:7;
set fn = f|n;
A15: g = (g|m)^(g/^m) by RFINSEQ:8;
A16: gm|m1 = g | ((Seg m)/\(Seg m1)) by RELAT_1:71
.= g|m1 by A13,XBOOLE_1:28;
A17: f = fn ^ <*a*> by A6,RFINSEQ:7;
now
let x be object;
card Coim(f,x) = card Coim(g,x) by A5; then
card(fn"{x}) +
card(<*a*>"{x}) = card(((g|m1)^<*a*>^(g/^m))"{x})
by A15,A14,A16,A17,FINSEQ_3:57
.= card(((g|m1)^<*a*>)"{x}) + card((g/^m)"{x}) by FINSEQ_3:57
.= card((g|m1)"{x})+ card(<*a*>"{x}) + card((g/^m)"{x}) by FINSEQ_3:57
.= card((g|m1)"{x}) + card((g/^m)"{x})+ card(<*a*>"{x})
.= card(((g|m1)^(g/^m))"{x})+ card(<*a*>"{x}) by FINSEQ_3:57;
hence card Coim(fn,x) = card Coim((g|m1)^(g/^m),x);
end; then
A18: fn, (g|m1)^(g/^m) are_fiberwise_equipotent;
len fn = n by A6,FINSEQ_1:59,NAT_1:11;
then Product fn = Product ((g|m1)^gg) by A4,A18;
hence Product f = Product((g|m1)^gg) * Product <*a*> by A17,RVSUM_1:97
.= Product(g|m1) * Product gg* Product <*a*> by RVSUM_1:97
.= Product(g|m1) * Product <*a*> * Product gg
.= Product gm * Product gg by A14,A16,RVSUM_1:97
.= Product g by A15,RVSUM_1:97;
end;
A19: P[0]
proof
let f,g be FinSequence of REAL;
assume
a: f,g are_fiberwise_equipotent & len f = 0; then
A20: len g = 0 & f = <*>REAL by RFINSEQ:3;
g = <*>REAL by RFINSEQ:3,a;
hence thesis by A20;
end;
A4: for n being Nat holds P[n] from NAT_1:sch 2(A19,A3);
R1 is FinSequence of REAL & R2 is FinSequence of REAL by RVSUM_1:145;
hence thesis by A1,A2,A4;
end;
begin :: Arithmetic Mean and Geometric Mean
definition let f be real-valued FinSequence;
func Mean f -> real number equals
(Sum f) / len f;
coherence;
end;
definition let f be positive real-valued FinSequence;
func GMean f -> real number equals
(len f)-root (Product f);
coherence by TARSKI:1;
end;
theorem Huk1:
for f being real-valued FinSequence holds
Sum f = (len f) * (Mean f)
proof
let f be real-valued FinSequence;
per cases;
suppose
len f <> 0;
hence thesis by XCMPLX_1:87;
end;
suppose len f = 0; then
f = <*>REAL;
hence thesis by RVSUM_1:72;
end;
end;
theorem
for f being real-valued FinSequence holds
Mean (f ^ <*Mean f*>) = Mean f
proof
let f be real-valued FinSequence;
Mean (f ^ <*Mean f*>)
= (Sum f + Mean f) / len (f ^ <*Mean f*>) by RVSUM_1:74
.= (Sum f + Mean f) / (len f + len <*Mean f*>) by FINSEQ_1:22
.= (Sum f + Mean f) / (len f + 1) by FINSEQ_1:39
.= ((len f) * (Mean f) + Mean f) / (len f + 1) by Huk1
.= (Mean f) * (len f + 1) / (len f + 1)
.= Mean f by XCMPLX_1:89;
hence thesis;
end;
registration let f be non empty constant real-valued FinSequence;
cluster the_value_of f -> real;
coherence
proof
consider x being set such that
A1: x in dom f & the_value_of f = f.x by FUNCT_1:def 12;
thus thesis by A1;
end;
end;
theorem ConstantSum:
for f being non empty constant real-valued FinSequence holds
Sum f = (the_value_of f) * (len f)
proof
let f be non empty constant real-valued FinSequence;
set r = the_value_of f, i = len f;
f = (dom f) --> r by FUNCOP_1:80
.= i |-> r by FINSEQ_1:def 3;
hence thesis by RVSUM_1:80;
end;
theorem ConstantProduct:
for f being non empty constant real-valued FinSequence holds
Product f = (the_value_of f) |^ (len f)
proof
let f be non empty constant real-valued FinSequence;
set r = the_value_of f, i = len f;
f = (dom f) --> r by FUNCOP_1:80
.= i |-> r by FINSEQ_1:def 3;
hence thesis by NEWTON:def 1;
end;
theorem ConstantMean:
for f being non empty constant real-valued FinSequence holds
Mean f = the_value_of f
proof
let f be non empty constant real-valued FinSequence;
reconsider v = the_value_of f as Real;
Mean f = ((len f) * v) / len f by ConstantSum
.= v * ((len f) / len f) by XCMPLX_1:74
.= v * 1 by XCMPLX_1:60;
hence thesis;
end;
theorem PosLeq:
for f being non empty constant positive real-valued FinSequence holds
the_value_of f > 0
proof
let f be non empty constant positive real-valued FinSequence;
consider x being set such that
A1: x in dom f & the_value_of f = f.x by FUNCT_1:def 12;
thus thesis by A1,PosDef;
end;
theorem ConstantGMean:
for f being non empty constant positive real-valued FinSequence holds
GMean f = the_value_of f
proof
let f be non empty constant positive real-valued FinSequence;
reconsider v = the_value_of f as Real;
A3: len f >= 1 by NAT_1:14;
A4: v >= 0 by PosLeq;
Product f = v |^ (len f) by ConstantProduct;
hence thesis by A4,A3,POWER:4;
end;
registration let f be non empty positive real-valued FinSequence;
cluster Mean f -> positive;
coherence
proof
B1: for i be Nat st i in dom f holds 0 <= f.i by PosDef;
ex i be Nat st i in dom f & 0 < f.i
proof
take i = 1;
1 in dom f by FINSEQ_5:6;
hence thesis by PosDef;
end; then
Sum f > 0 by B1,RVSUM_1:85;
hence thesis;
end;
end;
registration let f be non empty positive real-valued FinSequence;
cluster Product f -> positive;
coherence
proof
reconsider F = f as FinSequence of REAL by RVSUM_1:145;
for k being Element of NAT st k in dom F holds F.k > 0 by PosDef;
hence thesis by NAT_4:42;
end;
end;
registration
let f be positive non empty real-valued FinSequence;
cluster GMean f -> positive;
coherence
proof
A2: len f >= 1 by NAT_1:14;
(len f)-root Product f = (len f) -Root Product f by POWER:def 1,NAT_1:14;
hence thesis by A2,PREPOWER:def 2;
end;
end;
begin :: Heterogeneity of a Finite Sequence
definition let f be real-valued FinSequence;
func HetSet f -> Subset of NAT equals
{ n where n is Nat : n in dom f & f.n <> Mean f };
coherence
proof
A3: { n where n is Nat : n in dom f & f.n <> Mean f } c= dom f
proof
let x be object;
assume x in { n where n is Nat : n in dom f & f.n <> Mean f }; then
consider n being Nat such that
A2: x = n & n in dom f & f.n <> Mean f;
thus thesis by A2;
end;
dom f c= NAT; then
{ n where n is Nat : n in dom f & f.n <> Mean f } c= NAT by A3;
hence thesis;
end;
end;
registration let f be real-valued FinSequence;
cluster HetSet f -> finite;
coherence
proof
{ n where n is Nat : n in dom f & f.n <> Mean f } c= dom f
proof
let x be object;
assume x in { n where n is Nat : n in dom f & f.n <> Mean f }; then
ex n being Nat st x = n & n in dom f & f.n <> Mean f;
hence thesis;
end;
hence thesis;
end;
end;
registration let f be positive non empty real-valued FinSequence;
cluster HetSet f -> bounded_above bounded_below real-membered;
coherence;
end;
definition let f be real-valued FinSequence;
func Het f -> Nat equals
card HetSet f;
coherence;
end;
theorem HetHomo:
for f being real-valued FinSequence st
Het f = 0 holds f is homogeneous
proof
let f be real-valued FinSequence;
assume
A1: Het f = 0;
set X = { n where n is Nat : n in dom f & f.n <> Mean f };
assume
a4: f is heterogeneous;
A5: for n being Nat st n in dom f holds f.n = Mean f
proof
let n be Nat;
assume
A2: n in dom f;
f.n = Mean f
proof
assume f.n <> Mean f; then
n in X by A2;
hence thesis by A1;
end;
hence thesis;
end;
for x, y being object st x in dom f & y in dom f holds f.x = f.y
proof
let x,y be object;
assume
B1: x in dom f & y in dom f; then
reconsider xx = x, yy = y as Nat;
f.xx = Mean f by A5,B1;
hence thesis by A5,B1;
end;
hence thesis by a4;
end;
theorem HetHetero:
for f being non empty real-valued FinSequence st
Het f <> 0 holds f is heterogeneous
proof
let f be non empty real-valued FinSequence;
assume
A1: Het f <> 0;
assume
A3: f is homogeneous; then
the_value_of f = Mean f by ConstantMean; then
consider x being set such that
A2: x in dom f & Mean f = f.x by FUNCT_1:def 12,A3;
HetSet f <> {} by A1; then
consider y being object such that
A5: y in HetSet f by XBOOLE_0:def 1;
consider z being Nat such that
A6: z = y & z in dom f & f.z <> Mean f by A5;
thus thesis by A3,A2,A6;
end;
registration let f be heterogeneous positive non empty
real-valued FinSequence;
cluster HetSet f -> non empty;
coherence
proof
Het f <> 0 by HetHomo;
hence thesis;
end;
end;
theorem HetBase:
for f being non empty homogeneous positive real-valued FinSequence holds
Mean f = GMean f
proof
let f be non empty homogeneous positive real-valued FinSequence;
the_value_of f = Mean f by ConstantMean;
hence thesis by ConstantGMean;
end;
definition let f1, f2 be real-valued FinSequence;
pred f1,f2 are_gamma-equivalent means
len f1 = len f2 & Mean f1 = Mean f2;
reflexivity;
symmetry;
end;
theorem
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
{ n where n is Nat : n in dom f & f.n < Mean f };
coherence
proof
A3: { n where n is Nat : n in dom f & f.n < Mean f } c= dom f
proof
let x be object;
assume x in { n where n is Nat : n in dom f & f.n < Mean f }; then
consider n being Nat such that
A2: x = n & n in dom f & f.n < Mean f;
thus thesis by A2;
end;
dom f c= NAT; then
{ n where n is Nat : n in dom f & f.n < Mean f } c= NAT by A3;
hence thesis;
end;
func MeanMore f -> Subset of NAT equals
{ n where n is Nat : n in dom f & f.n > Mean f };
coherence
proof
A3: { n where n is Nat : n in dom f & f.n > Mean f } c= dom f
proof
let x be object;
assume x in { n where n is Nat : n in dom f & f.n > Mean f }; then
ex n being Nat st x = n & n in dom f & f.n > Mean f;
hence thesis;
end;
dom f c= NAT; then
{ n where n is Nat : n in dom f & f.n > Mean f } c= NAT by A3;
hence thesis;
end;
end;
theorem
for f being real-valued FinSequence holds
HetSet f c= dom f
proof
let f be real-valued FinSequence;
let x be object;
assume x in HetSet f; then
ex n being Nat st x = n & n in dom f & f.n <> Mean f;
hence thesis;
end;
theorem LessDom:
for f being real-valued FinSequence holds
MeanLess f c= dom f
proof
let f be real-valued FinSequence;
let x be object;
assume x in MeanLess f; then
ex n being Nat st x = n & n in dom f & f.n < Mean f;
hence thesis;
end;
theorem MoreDom:
for f being real-valued FinSequence holds
MeanMore f c= dom f
proof
let f be real-valued FinSequence;
let x be object;
assume x in MeanMore f; then
ex n being Nat st x = n & n in dom f & f.n > Mean f;
hence thesis;
end;
theorem MeanSum:
for f being real-valued FinSequence holds
HetSet f = MeanLess f \/ MeanMore f
proof
let f be real-valued FinSequence;
thus HetSet f c= MeanLess f \/ MeanMore f
proof
let x be object;
assume x in HetSet f; then
consider i being Nat such that
A1: i = x & i in dom f & f.i <> Mean f;
f.i < Mean f or f.i > Mean f by A1,XXREAL_0:1; then
i in MeanLess f or i in MeanMore f by A1;
hence thesis by A1,XBOOLE_0:def 3;
end;
let x be object;
assume x in MeanLess f \/ MeanMore f; then
per cases by XBOOLE_0:def 3;
suppose x in MeanLess f; then
ex i being Nat st i = x & i in dom f & f.i < Mean f;
hence thesis;
end;
suppose x in MeanMore f; then
ex i being Nat st i = x & i in dom f & f.i > Mean f;
hence thesis;
end;
end;
MeanL:
for f being heterogeneous real-valued FinSequence holds
MeanLess f <> {}
proof
let f be heterogeneous real-valued FinSequence;
Het f <> {} by HetHomo; then
HetSet f <> {}; then
consider x being object such that
A1: x in HetSet f by XBOOLE_0:7;
x in MeanLess f \/ MeanMore f by A1,MeanSum; then
per cases by XBOOLE_0:def 3;
suppose x in MeanLess f;
hence thesis;
end;
suppose x in MeanMore f; then
consider n being Nat such that
A2: x = n & n in dom f & f.n > Mean f;
reconsider R1 = (len f) |-> Mean f as real-valued FinSequence;
set ff = f;
reconsider w = len R1 as Nat;
ex i being Nat st i in dom f & ff.i < Mean f
proof
assume
TT: for i being Nat st i in dom f holds ff.i >= Mean f;
G1: for j be Nat st j in Seg w holds R1.j <= ff.j
proof
let j be Nat;
assume
g0: j in Seg w; then
G2: j in Seg len f by CARD_1:def 7;
G3: j in dom f by FINSEQ_1:def 3,CARD_1:def 7,g0;
R1.j = Mean f by G2,FINSEQ_2:57;
hence thesis by TT,G3;
end;
ex j be Nat st j in Seg w & R1.j < ff.j
proof
take n;
n in Seg len f by A2,FINSEQ_1:def 3;
hence thesis by CARD_1:def 7,A2,FINSEQ_2:57;
end; then
Sum R1 < Sum ff by Th83,G1,CARD_1:def 7; then
Sum ff > (len f) * Mean f by RVSUM_1:80;
hence thesis by Huk1;
end; then
consider m being Nat such that
B1: m in dom f & f.m < Mean f;
m in MeanLess f by B1;
hence thesis;
end;
end;
MeanM:
for f being heterogeneous real-valued FinSequence holds
MeanMore f <> {}
proof
let f be heterogeneous real-valued FinSequence;
Het f <> {} by HetHomo; then
HetSet f <> {}; then
consider x being object such that
A1: x in HetSet f by XBOOLE_0:7;
x in MeanLess f \/ MeanMore f by A1,MeanSum; then
per cases by XBOOLE_0:def 3;
suppose x in MeanMore f;
hence thesis;
end;
suppose x in MeanLess f; then
consider n being Nat such that
A2: x = n & n in dom f & f.n < Mean f;
reconsider R1 = (len f) |-> Mean f as real-valued FinSequence;
set ff = f;
reconsider w = len R1 as Nat;
ex i being Nat st i in dom f & ff.i > Mean f
proof
assume
TT: for i being Nat st i in dom f holds ff.i <= Mean f;
G0: len R1 = len f by CARD_1:def 7;
G1: for j be Nat st j in Seg w holds R1.j >= ff.j
proof
let j be Nat;
assume
g0: j in Seg w; then
G2: j in Seg len f by CARD_1:def 7;
G3: j in dom f by FINSEQ_1:def 3,g0,CARD_1:def 7;
R1.j = Mean f by G2,FINSEQ_2:57;
hence thesis by TT,G3;
end;
ex j be Nat st j in Seg w & R1.j > ff.j
proof
take n;
n in Seg len f by A2,FINSEQ_1:def 3;
hence thesis by A2,FINSEQ_2:57,CARD_1:def 7;
end; then
Sum R1 > Sum ff by Th83,G1,G0; then
Sum ff < (len f) * Mean f by RVSUM_1:80;
hence thesis by Huk1;
end; then
consider m being Nat such that
B1: m in dom f & f.m > Mean f;
m in MeanMore f by B1;
hence thesis;
end;
end;
registration let f be heterogeneous real-valued FinSequence;
cluster MeanLess f -> non empty;
coherence by MeanL;
cluster MeanMore f -> non empty;
coherence by MeanM;
end;
registration let f be homogeneous real-valued FinSequence;
cluster MeanLess f -> empty;
coherence
proof
per cases;
suppose f is empty; then
dom f = {}; then
MeanLess f c= {} by LessDom;
hence thesis;
end;
suppose
AA: f is non empty;
A0: HetSet f = MeanLess f \/ MeanMore f by MeanSum;
MeanLess f = {}
proof
assume MeanLess f <> {}; then
consider x being object such that
A1: x in MeanLess f by XBOOLE_0:7;
Het f <> 0 by A0,A1;
hence thesis by HetHetero,AA;
end;
hence thesis;
end;
end;
cluster MeanMore f -> empty;
coherence
proof
per cases;
suppose f is empty; then
dom f = {}; then
MeanMore f c= {} by MoreDom;
hence thesis;
end;
suppose
AA: f is non empty;
A0: HetSet f = MeanLess f \/ MeanMore f by MeanSum;
MeanMore f = {}
proof
assume MeanMore f <> {}; then
consider x being object such that
A1: x in MeanMore f by XBOOLE_0:7;
Het f <> 0 by A0,A1;
hence thesis by HetHetero,AA;
end;
hence thesis;
end;
end;
end;
theorem MeanMiss:
for f be heterogeneous non empty real-valued FinSequence holds
MeanLess f misses MeanMore f
proof
let f be heterogeneous non empty real-valued FinSequence;
assume MeanLess f meets MeanMore f; then
consider x being object such that
A1: x in MeanLess f & x in MeanMore f by XBOOLE_0:3;
consider i being Nat such that
A2: i = x & i in dom f & f.i < Mean f by A1;
consider j being Nat such that
A3: j = x & j in dom f & f.j > Mean f by A1;
thus thesis by A2,A3;
end;
theorem
for f be heterogeneous non empty real-valued FinSequence holds
Het f >= 2
proof
let f be heterogeneous non empty real-valued FinSequence;
set x = the Element of MeanLess f;
set y = the Element of MeanMore f;
HetSet f = MeanLess f \/ MeanMore f by MeanSum; then
A0: x in HetSet f & y in HetSet f by XBOOLE_0:def 3;
A4: x <> y by XBOOLE_0:3,MeanMiss;
A5: card {x,y} = 2 by CARD_2:57,A4;
card Segm 2 c= card Segm Het f by A5,ZFMISC_1:32,A0,CARD_1:11;
hence thesis by NAT_1:40;
end;
begin :: Auxiliary Replacement Function
definition let f be Function,
i,j be Nat,
a, b be object;
func Replace (f,i,j,a,b) -> Function equals
(f+*(i,a))+*(j,b);
coherence;
end;
theorem DinoDom:
for f being FinSequence,
i,j being Nat,
a,b being object holds
dom Replace (f,i,j,a,b) = dom f
proof
let f be FinSequence,
i,j be Nat,
a,b be object;
dom (f+*(i,a)) = dom f by FUNCT_7:30;
hence thesis by FUNCT_7:30;
end;
registration let f be real-valued FinSequence,
i,j be Nat,
a, b be Real;
cluster Replace (f,i,j,a,b) -> real-valued FinSequence-like;
coherence;
end;
theorem CopyForValued:
for w being real-valued FinSequence,
r being Real,
i being Nat st
i in dom w holds w+*(i,r) = (w | (i-'1)) ^ <*r*> ^ (w/^i)
proof
let w be real-valued FinSequence, r be Real, i be Nat;
reconsider ww = w as FinSequence of REAL by RVSUM_1:145;
reconsider rr = r as Element of REAL by XREAL_0:def 1;
assume i in dom w; then
ww +* (i,rr) = (ww | (i-'1)) ^ <*rr*> ^ (ww/^i) by FUNCT_7:98;
hence thesis;
end;
theorem SumA:
for f be real-valued FinSequence,
i be Nat,
a be Real st i in dom f holds
Sum (f+*(i,a)) = Sum f - f.i + a
proof
let f be real-valued FinSequence,
i be Nat,
a be Real;
reconsider w = f as FinSequence of REAL by RVSUM_1:145;
reconsider aa = a as Element of REAL by XREAL_0:def 1;
assume
A1: i in dom f; then
Z1: Sum (w+*(i,a)) = Sum ((w | (i-'1)) ^ <*aa*> ^ (w/^i)) by CopyForValued
.= Sum ((w | (i-'1)) ^ <*aa*>) + Sum (w/^i) by RVSUM_1:75
.= Sum (w | (i-'1)) + Sum <*aa*> + Sum (w/^i) by RVSUM_1:75
.= Sum (w | (i-'1)) + aa + Sum (w/^i) by RVSUM_1:73
.= aa + (Sum (w | (i-'1)) + Sum (w/^i))
.= aa + Sum ((w | (i-'1)) ^ (w/^i)) by RVSUM_1:75;
reconsider fi = f.i as Real;
1 <= i & i <= len w by A1,FINSEQ_3:25; then
Sum w = Sum ((w | (i-'1)) ^ <*f.i*> ^ (w/^i)) by FINSEQ_5:84
.= Sum ((w | (i-'1)) ^ <*f.i*>) + Sum (w/^i) by RVSUM_1:75
.= Sum (w | (i-'1)) + Sum <*f.i*> + Sum (w/^i) by RVSUM_1:75
.= Sum (w | (i-'1)) + fi + Sum (w/^i) by RVSUM_1:73
.= fi + (Sum (w | (i-'1)) + Sum (w/^i))
.= fi + Sum ((w | (i-'1)) ^ (w/^i)) by RVSUM_1:75;
hence thesis by Z1;
end;
theorem ProductA:
for f be positive real-valued FinSequence,
i be Nat,
a be Real st i in dom f holds
Product (f+*(i,a)) = (Product f) * a / (f.i)
proof
let f be positive real-valued FinSequence,
i be Nat,
a be Real;
reconsider w = f as FinSequence of REAL by RVSUM_1:145;
reconsider aa = a as Element of REAL by XREAL_0:def 1;
assume
A1: i in dom f; then
Z1: Product (w+*(i,a)) = Product ((w | (i-'1)) ^ <*aa*> ^ (w/^i))
by CopyForValued
.= Product ((w | (i-'1)) ^ <*aa*>) * Product (w/^i) by RVSUM_1:97
.= Product (w | (i-'1)) * Product <*aa*> * Product (w/^i) by RVSUM_1:97
.= aa * (Product (w | (i-'1)) * Product (w/^i))
.= aa * Product ((w | (i-'1)) ^ (w/^i)) by RVSUM_1:97;
reconsider fi = f.i as Real;
ZZ: fi <> 0 by A1,PosDef;
1 <= i & i <= len w by A1,FINSEQ_3:25; then
zz: Product w = Product ((w | (i-'1)) ^ <*f.i*> ^ (w/^i)) by FINSEQ_5:84
.= Product ((w | (i-'1)) ^ <*f.i*>) * Product (w/^i) by RVSUM_1:97
.= Product (w | (i-'1)) * Product <*f.i*> * Product (w/^i) by RVSUM_1:97
.= fi * (Product (w | (i-'1)) * Product (w/^i))
.= fi * Product ((w | (i-'1)) ^ (w/^i)) by RVSUM_1:97;
Product (w+*(i,a)) = aa * (Product w / fi) by ZZ,XCMPLX_1:89,zz,Z1
.= aa * (Product w * (1 / fi)) by XCMPLX_1:99
.= Product w * aa * (1 / fi)
.= (Product f) * a / (f.i) by XCMPLX_1:99;
hence thesis;
end;
theorem SumReplace:
for f be real-valued FinSequence,
i,j be Nat,
a, b be 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
let f be real-valued FinSequence,
i,j be Nat,
a, b be Real;
assume
A0: i in dom f & j in dom f & i <> j;
A1: j in dom (f +* (i,a)) by A0,FUNCT_7:30;
Sum Replace (f,i,j,a,b) =
Sum (f +* (i,a)) - (f +* (i,a)).j + b by A1,SumA
.= Sum (f +* (i,a)) - f.j + b by FUNCT_7:32,A0
.= Sum f - f.i + a - f.j + b by A0,SumA
.= Sum f - f.i + (a - f.j) + b;
hence thesis;
end;
theorem ProdReplace:
for f be positive real-valued FinSequence,
i,j be Nat,
a, b be 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
let f be positive real-valued FinSequence,
i,j be Nat,
a, b be positive Real;
for n being Nat st n in dom (f+*(i,a)) holds (f+*(i,a)).n > 0
proof
let n be Nat;
assume n in dom (f+*(i,a)); then
A2: n in dom f by FUNCT_7:30;
per cases;
suppose n = i;
hence thesis by A2,FUNCT_7:31;
end;
suppose n <> i; then
(f+*(i,a)).n = f.n by FUNCT_7:32;
hence thesis by PosDef,A2;
end;
end; then
S1: f+*(i,a) is positive;
assume
A0: i in dom f & j in dom f & i <> j;
A1: j in dom (f +* (i,a)) by A0,FUNCT_7:30;
Product Replace (f,i,j,a,b)
= Product (f +* (i,a)) * b / ((f +* (i,a)).j) by A1,ProductA,S1
.= Product (f +* (i,a)) * b / (f.j) by FUNCT_7:32,A0
.= (Product f * a / (f.i)) * b / (f.j) by A0,ProductA
.= (Product f * a * (1 / (f.i))) * b / (f.j) by XCMPLX_1:99
.= Product f * a * b * (1 / (f.i)) * (1 / (f.j)) by XCMPLX_1:99
.= Product f * a * b / (f.i) * (1 / (f.j)) by XCMPLX_1:99
.= Product f * a * b / (f.i) / (f.j) by XCMPLX_1:99
.= (Product f) * a * b / ((f.i) * (f.j)) by XCMPLX_1:78;
hence thesis;
end;
theorem ReplaceGamma:
for f be real-valued FinSequence,
i,j be 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
let f be real-valued FinSequence,
i,j be Nat;
set a = Mean f;
set b = f.i + f.j - Mean f;
assume
A1: i in dom f & j in dom f & i <> j;
A2: dom f = dom Replace (f,i,j,a,b) by DinoDom;
Sum Replace (f,i,j,a,b) = Sum f - f.i - f.j + a + b by SumReplace,A1
.= Sum f;
hence thesis by FINSEQ_3:29,A2;
end;
theorem ReplaceValue:
for f be real-valued FinSequence,
i,j,k be Nat,
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
let f be real-valued FinSequence,
i,j,k be Nat,
a,b be Real;
assume
A1: i in dom f & j in dom f & k in dom f & i <> j & (k <> i & k <> j);
(Replace (f,i,j,a,b)).k = (f +* (i,a)).k by A1,FUNCT_7:32
.= f.k by A1,FUNCT_7:32;
hence thesis;
end;
theorem ReplaceValue2:
for f be FinSequence,
i,j be Nat,
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
let f be FinSequence,
i,j be Nat,
a,b be object;
set g = Replace (f,i,j,a,b);
assume i in dom f & j in dom f & i <> j; then
j in dom (f +* (i,a)) by FUNCT_7:30;
hence thesis by FUNCT_7:31;
end;
theorem ReplaceValue3:
for f be FinSequence,
i,j be Nat,
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
let f be FinSequence,
i,j be Nat,
a,b be object;
set g = Replace (f,i,j,a,b);
assume
A1: i in dom f & j in dom f & i <> j; then
g.i = (f +* (i,a)).i by FUNCT_7:32
.= a by A1,FUNCT_7:31;
hence thesis;
end;
theorem HetMono:
for f be real-valued FinSequence,
i,j be 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
let f be real-valued FinSequence,
i,j be Nat;
assume
A0: i in dom f & j in dom f & i <> j;
assume
FF: f.i <> Mean f & f.j <> Mean f;
set g = Replace (f,i,j,Mean f,f.i + f.j - Mean f);
zz: f,g are_gamma-equivalent by ReplaceGamma,A0;
set a = Mean f;
set b = f.i + f.j - Mean f;
FX: HetSet g <> HetSet f
proof
assume
h2: HetSet g = HetSet f;
not i in { n1 where n1 is Nat : n1 in dom g & g.n1 <> Mean g }
proof
assume i in { n1 where n1 is Nat : n1 in dom g & g.n1 <> Mean g };
then consider n2 being Nat such that
G1: n2 = i & n2 in dom g & g.n2 <> Mean g;
thus thesis by zz,ReplaceValue3,A0,G1;
end;
hence thesis by h2,FF,A0;
end;
HetSet g c= HetSet f
proof
let x be object;
assume x in HetSet g; then
consider n1 being Nat such that
A1: n1 = x & n1 in dom g & g.n1 <> Mean g;
A2: n1 in dom f by A1,DinoDom;
f.n1 <> Mean f
proof
per cases;
suppose n1 = i;
hence thesis by A1,zz,ReplaceValue3,A0;
end;
suppose
n1 = j;
hence thesis by FF;
end;
suppose
B1: n1 <> i & n1 <> j;
f, g are_gamma-equivalent by ReplaceGamma,A0;
hence thesis by B1,ReplaceValue,A0,A2,A1;
end;
end;
hence thesis by A1,A2;
end; then
HetSet g c< HetSet f by FX;
hence thesis by CARD_2:48;
end;
theorem ProdGMean:
for f,g being positive non empty real-valued FinSequence st
len f = len g & Product f < Product g holds
GMean f < GMean g
proof
let f,g be positive non empty real-valued FinSequence;
A1: Product f >= 0 & len f >= 1 by NAT_1:14;
assume len f = len g & Product f < Product g;
hence thesis by POWER:17,A1;
end;
theorem ExDiff:
for f be positive heterogeneous non empty real-valued FinSequence
ex i,j be Nat st
i in dom f & j in dom f & i <> j & f.i < Mean f & Mean f < f.j
proof
let f be positive heterogeneous non empty real-valued FinSequence;
take i = the Element of MeanLess f;
take j = the Element of MeanMore f;
i in MeanLess f; then
consider ii being Nat such that
A1: ii = i & ii in dom f & f.ii < Mean f;
j in MeanMore f; then
consider jj being Nat such that
A2: jj = j & jj in dom f & f.jj > Mean f;
thus thesis by A1,A2;
end;
theorem ReplacePositive:
for f be positive heterogeneous non empty real-valued FinSequence
for i,j be 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
let f be positive heterogeneous non empty real-valued FinSequence;
let i,j be Nat such that
A1: i in dom f & j in dom f & i <> j & f.i > Mean f;
set a = Mean f;
set b = f.i + f.j - Mean f;
h2: Mean f - Mean f < f.i - Mean f by A1,XREAL_1:14;
f.j > 0 by A1,PosDef; then
f.i - Mean f + f.j > 0 by h2; then
reconsider b as positive Real;
set g = Replace (f,i,j,a,b);
for n being Nat st n in dom g holds g.n > 0
proof
let n be Nat;
assume n in dom g; then
A2: n in dom f by DinoDom;
per cases;
suppose n = i;
hence thesis by ReplaceValue3,A1;
end;
suppose n = j;
hence thesis by ReplaceValue2,A1;
end;
suppose n <> i & n <> j; then
g.n = f.n by A2,ReplaceValue,A1;
hence thesis by PosDef,A2;
end;
end;
hence thesis;
end;
theorem ReplacePositive2:
for f be positive heterogeneous non empty real-valued FinSequence
for i,j be 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
let f be positive heterogeneous non empty real-valued FinSequence;
let i,j be Nat such that
A1: i in dom f & j in dom f & i <> j & f.j > Mean f;
set a = Mean f;
set b = f.i + f.j - Mean f;
h2: Mean f - Mean f < f.j - Mean f by XREAL_1:14,A1;
f.i > 0 by A1,PosDef; then
f.j - Mean f + f.i > 0 by h2; then
reconsider b as positive Real;
set g = Replace (f,i,j,a,b);
for n being Nat st n in dom g holds g.n > 0
proof
let n be Nat;
assume n in dom g; then
A2: n in dom f by DinoDom;
per cases;
suppose n = i;
hence thesis by ReplaceValue3,A1;
end;
suppose n = j;
hence thesis by ReplaceValue2,A1;
end;
suppose n <> i & n <> j; then
g.n = f.n by A2,ReplaceValue,A1;
hence thesis by PosDef,A2;
end;
end;
hence thesis;
end;
theorem
for f be positive heterogeneous non empty real-valued FinSequence
ex i,j be Nat st
i in dom f & j in dom f & i <> j &
ex g being positive non empty real-valued FinSequence st
g = Replace (f,i,j,Mean f,f.i + f.j - Mean f) &
GMean f < GMean g
proof
let f be positive heterogeneous non empty real-valued FinSequence;
consider j,i be Nat such that
A1: j in dom f & i in dom f & j <> i & f.j < Mean f & Mean f < f.i
by ExDiff;
take i,j;
thus i in dom f & j in dom f & i <> j by A1;
reconsider a = Mean f as positive Real;
b1: f.i > 0 & f.j > 0 by A1,PosDef;
h2: Mean f - Mean f < f.i - Mean f by A1,XREAL_1:14;
f.j > 0 by A1,PosDef; then
f.i - Mean f + f.j > 0 by h2; then
reconsider b = f.i + f.j - Mean f as positive Real;
set g = Replace (f,i,j,a,b);
jj: dom f = dom g by DinoDom;
reconsider g as positive non empty real-valued FinSequence
by ReplacePositive,A1;
take g;
f.i > Mean f + 0 & Mean f > f.j + 0 by A1; then
f.i - Mean f > 0 & Mean f - f.j > 0 by XREAL_1:20; then
(f.i - Mean f) * (Mean f - f.j) > 0; then
a * b - (f.i) * (f.j) + (f.i) * (f.j) > 0 + (f.i) * (f.j)
by XREAL_1:8; then
a * b / ((f.i) * (f.j)) > 1 by XREAL_1:187,b1; then
(Product f) * (a * b / ((f.i) * (f.j))) > (Product f) * 1
by XREAL_1:68; then
(Product f) * (a * b) / ((f.i) * (f.j)) > Product f by XCMPLX_1:74; then
(Product f) * a * b / ((f.i) * (f.j)) > Product f; then
Product g > Product f by A1,ProdReplace;
hence thesis by ProdGMean,jj,FINSEQ_3:29;
end;
theorem BlaBla:
for f be heterogeneous non empty real-valued FinSequence,
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
let f be heterogeneous non empty real-valued FinSequence;
let i,j be Nat;
assume
A1: i = the Element of MeanLess f &
j = the Element of MeanMore f;
i in MeanLess f by A1; then
consider ii being Nat such that
A2: ii = i & ii in dom f & f.ii < Mean f;
j in MeanMore f by A1; then
consider jj being Nat such that
A3: jj = j & jj in dom f & f.jj > Mean f;
thus thesis by A2,A3;
end;
theorem BlaBla2:
for f be heterogeneous positive non empty real-valued FinSequence,
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
let f be heterogeneous positive non empty real-valued FinSequence;
let i,j be object;
assume
A1: i in MeanLess f & j in MeanMore f; then
consider ii being Nat such that
A2: ii = i & ii in dom f & f.ii < Mean f;
consider jj being Nat such that
A3: jj = j & jj in dom f & f.jj > Mean f by A1;
thus thesis by A2,A3;
end;
theorem
for f be positive heterogeneous non empty real-valued FinSequence
for i,j be Nat st
i in dom f & j in dom f & i <> j & i in MeanMore f & j in MeanLess f
holds
ex g being positive non empty real-valued FinSequence st
g = Replace (f,i,j,Mean f,f.i + f.j - Mean f) &
GMean f < GMean g
proof
let f be positive heterogeneous non empty real-valued FinSequence;
let i, j be Nat such that
A1: i in dom f & j in dom f & i <> j & i in MeanMore f & j in MeanLess f;
reconsider a = Mean f as positive Real;
b1: f.i > 0 & f.j > 0 by A1,PosDef;
h1: Mean f < f.i by A1,BlaBla2; then
h2: Mean f - Mean f < f.i - Mean f by XREAL_1:14;
f.j > 0 by A1,PosDef; then
f.i - Mean f + f.j > 0 by h2; then
reconsider b = f.i + f.j - Mean f as positive Real;
set g = Replace (f,i,j,a,b);
jj: dom f = dom g by DinoDom;
reconsider g as positive non empty real-valued FinSequence
by ReplacePositive,A1,h1;
take g;
f.i > Mean f + 0 & Mean f > f.j + 0 by A1,BlaBla2; then
f.i - Mean f > 0 & Mean f - f.j > 0 by XREAL_1:20; then
(f.i - Mean f) * (Mean f - f.j) > 0; then
a * b - (f.i) * (f.j) + (f.i) * (f.j) > 0 + (f.i) * (f.j)
by XREAL_1:6; then
a * b / ((f.i) * (f.j)) > 1 by XREAL_1:187,b1; then
(Product f) * (a * b / ((f.i) * (f.j))) > (Product f) * 1
by XREAL_1:68; then
(Product f) * (a * b) / ((f.i) * (f.j)) > Product f by XCMPLX_1:74; then
(Product f) * a * b / ((f.i) * (f.j)) > Product f; then
Product g > Product f by A1,ProdReplace;
hence thesis by ProdGMean,jj,FINSEQ_3:29;
end;
theorem ReplaceGMean3:
for f be positive heterogeneous non empty real-valued FinSequence
for i,j be Nat st
i in dom f & j in dom f & i <> j & j in MeanMore f & i in MeanLess f
holds
ex g being positive non empty real-valued FinSequence st
g = Replace (f,i,j,Mean f,f.i + f.j - Mean f) &
GMean f < GMean g
proof
let f be positive heterogeneous non empty real-valued FinSequence;
let i, j be Nat such that
A1: i in dom f & j in dom f & i <> j & j in MeanMore f & i in MeanLess f;
reconsider a = Mean f as positive Real;
b1: f.i > 0 & f.j > 0 by A1,PosDef;
h1: Mean f < f.j by A1,BlaBla2; then
h2: Mean f - Mean f < f.j - Mean f by XREAL_1:14;
f.i > 0 by A1,PosDef; then
f.j - Mean f + f.i > 0 by h2; then
reconsider b = f.i + f.j - Mean f as positive Real;
set g = Replace (f,i,j,a,b);
jj: dom f = dom g by DinoDom;
reconsider g as positive non empty real-valued FinSequence
by ReplacePositive2,A1,h1;
take g;
f.j > Mean f + 0 & Mean f > f.i + 0 by A1,BlaBla2; then
f.j - Mean f > 0 & Mean f - f.i > 0 by XREAL_1:20; then
(f.j - Mean f) * (Mean f - f.i) > 0; then
k2: a * b - (f.i) * (f.j) + (f.i) * (f.j) > 0 + (f.i) * (f.j)
by XREAL_1:8;
a * b / ((f.i) * (f.j)) > 1 by k2,XREAL_1:187,b1; then
(Product f) * (a * b / ((f.i) * (f.j))) > (Product f) * 1
by XREAL_1:68; then
(Product f) * (a * b) / ((f.i) * (f.j)) > Product f by XCMPLX_1:74; then
(Product f) * a * b / ((f.i) * (f.j)) > Product f; then
Product g > Product f by A1,ProdReplace;
hence thesis by ProdGMean,jj,FINSEQ_3:29;
end;
begin :: Homogenization of a Finite Sequence
definition let f be heterogeneous positive non empty real-valued FinSequence;
func Homogen f -> real-valued FinSequence means :HomDef:
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
proof
set i = the Element of MeanLess f,
j = the Element of MeanMore f;
reconsider i, j as Nat;
Replace (f, i, j, Mean f, f.i + f.j - Mean f) is real-valued FinSequence;
hence thesis;
end;
uniqueness;
end;
theorem DomHomogen:
for f being heterogeneous positive non empty real-valued FinSequence holds
dom Homogen f = dom f
proof
let f be heterogeneous positive non empty real-valued FinSequence;
consider i,j being Nat such that
A1: i = the Element of MeanLess f &
j = the Element of MeanMore f &
Homogen f = Replace (f, i, j, Mean f, f.i + f.j - Mean f) by HomDef;
thus thesis by DinoDom,A1;
end;
registration let f be heterogeneous positive non empty real-valued FinSequence;
cluster Homogen f -> non empty;
coherence
proof
dom Homogen f = dom f by DomHomogen;
hence thesis;
end;
end;
registration let f be heterogeneous positive non empty real-valued FinSequence;
cluster Homogen f -> positive;
coherence
proof
consider i,j being Nat such that
A1: i = the Element of MeanLess f &
j = the Element of MeanMore f &
Homogen f = Replace (f, i, j, Mean f, f.i + f.j - Mean f) by HomDef;
i in MeanLess f by A1; then
consider ii being Nat such that
A2: ii = i & ii in dom f & f.ii < Mean f;
j in MeanMore f by A1; then
consider jj being Nat such that
A3: jj = j & jj in dom f & f.jj > Mean f;
thus thesis by A1,ReplacePositive2,A2,A3;
end;
end;
theorem HomogenHet:
for f be heterogeneous positive non empty real-valued FinSequence holds
Het Homogen f < Het f
proof
let f be heterogeneous positive non empty real-valued FinSequence;
consider i,j being Nat such that
A1: i = the Element of MeanLess f &
j = the Element of MeanMore f &
Homogen f = Replace (f, i, j, Mean f, f.i + f.j - Mean f) by HomDef;
A2: i in dom f & j in dom f & i <> j by A1,BlaBla;
f.i <> Mean f & f.j <> Mean f by A1,BlaBla;
hence thesis by HetMono,A1,A2;
end;
theorem HomEqui:
for f be heterogeneous positive non empty real-valued FinSequence holds
Homogen f, f are_gamma-equivalent
proof
let f be heterogeneous positive non empty real-valued FinSequence;
consider i,j being Nat such that
A1: i = the Element of MeanLess f &
j = the Element of MeanMore f &
Homogen f = Replace (f, i, j, Mean f, f.i + f.j - Mean f) by HomDef;
i in dom f & j in dom f & i <> j by A1,BlaBla;
hence thesis by A1,ReplaceGamma;
end;
theorem HomGMean:
for f be heterogeneous positive non empty real-valued FinSequence holds
GMean Homogen f > GMean f
proof
let f be heterogeneous positive non empty real-valued FinSequence;
consider i,j being Nat such that
A1: i = the Element of MeanLess f &
j = the Element of MeanMore f &
Homogen f = Replace (f, i, j, Mean f, f.i + f.j - Mean f) by HomDef;
i in dom f & j in dom f & i <> j by A1,BlaBla2; then
consider g being positive non empty real-valued FinSequence such that
J1: g = Replace (f,i,j,Mean f,f.i + f.j - Mean f) &
GMean f < GMean g by A1,ReplaceGMean3;
thus thesis by J1,A1;
end;
begin :: Cauchy Mean Theorem
theorem WOWTheo:
for f be heterogeneous positive non empty real-valued FinSequence holds
ex g being non empty homogeneous positive real-valued FinSequence st
GMean g > GMean f & Mean g = Mean f
proof
let f be heterogeneous positive non empty real-valued FinSequence;
defpred P[Nat] means
ex g being positive non empty real-valued FinSequence st
Het g = $1 &
Mean f = Mean g &
GMean g > GMean f &
Het g < Het f;
B1: ex k being Nat st P[k]
proof
reconsider g = Homogen f as positive non empty real-valued FinSequence;
take k = Het g;
take g;
g, f are_gamma-equivalent by HomEqui;
hence thesis by HomogenHet,HomGMean;
end;
B2: for k being Nat st k <> 0 & P[k] ex n being Nat st n < k & P[n]
proof
let k be Nat;
assume
Y1: k <> 0 & P[k]; then
consider g being positive non empty real-valued FinSequence such that
Y2: Het g = k &
Mean f = Mean g &
GMean g > GMean f &
Het g < Het f;
reconsider g as heterogeneous
positive non empty real-valued FinSequence by Y1,Y2,HetHetero;
reconsider h = Homogen g as positive non empty real-valued FinSequence;
take n = Het h;
thus n < k by Y2,HomogenHet;
thus P[n]
proof
ex g1 being positive non empty real-valued FinSequence st
Het g1 = n &
Mean f = Mean g1 &
GMean g1 > GMean f &
Het g1 < Het f
proof
take h;
h, g are_gamma-equivalent by HomEqui;
hence thesis by Y2,HomogenHet,XXREAL_0:2,HomGMean;
end;
hence thesis;
end;
end;
P[0] from NAT_1:sch 7(B1,B2); then
consider g being positive non empty real-valued FinSequence such that
WW: Het g = 0 &
Mean f = Mean g &
GMean g > GMean f &
Het g < Het f;
g is homogeneous by WW;
hence thesis by WW;
end;
::$N Inequality of arithmetic and geometric means
::$L https://en.wikipedia.org/wiki/Inequality_of_arithmetic_and_geometric_means Inequality of arithmetic and geometric means
theorem
for f being non empty positive real-valued FinSequence holds
GMean f <= Mean f
proof
let f be non empty positive real-valued FinSequence;
per cases;
suppose Het f = 0; then
reconsider ff = f as
non empty homogeneous positive real-valued FinSequence;
GMean ff = Mean ff by HetBase;
hence thesis;
end;
suppose Het f <> 0; then
reconsider ff = f as
non empty heterogeneous positive real-valued FinSequence
by HetHetero;
ex g being non empty homogeneous positive real-valued FinSequence st
GMean g > GMean ff & Mean g = Mean ff by WOWTheo;
hence thesis by HetBase;
end;
end;
theorem
for f being positive real-valued FinSequence st
GMean f = Mean f holds
f is constant
proof
let f be positive real-valued FinSequence;
assume
A1: GMean f = Mean f;
assume f is heterogeneous; then
reconsider ff = f as
non empty heterogeneous positive real-valued FinSequence;
ex g being non empty homogeneous positive real-valued FinSequence st
GMean g > GMean ff & Mean g = Mean ff by WOWTheo;
hence thesis by A1,HetBase;
end;