:: Cauchy Mean Theorem :: by Adam Grabowski :: :: Received June 13, 2014 :: Copyright (c) 2014-2018 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, ORDINAL1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, NAT_1, BINOP_2, FINSEQ_1, FINSEQ_2, VALUED_0, VALUED_1, RELAT_1, FINSEQ_4, CARD_1, INT_1, RVSUM_1, FUNCT_7, SEQ_4, FINSET_1, XXREAL_2, RELSET_1, XXREAL_0, MEMBERED, COMPLEX1, NEWTON, FINSEQ_6, FINSEQ_7, PDIFF_7; requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL; definitions BINOP_1, FINSEQOP, FINSEQ_1, TARSKI, RFINSEQ, CLASSES1, XBOOLE_0, SEQM_3, PARTFUN3; equalities FINSEQ_1, SQUARE_1, FINSEQ_2, VALUED_1, FINSEQ_4, XREAL_0, ORDINAL1, FUNCT_7, FINSEQ_7, RVSUM_1, FUNCOP_1, RELAT_1; expansions BINOP_1, FINSEQOP, FINSEQ_1, TARSKI, RFINSEQ, CLASSES1, FUNCT_7, FINSEQ_7, 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: 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 by FINSEQ_1:def 8; 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 by FINSEQ_1:44; 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 by FINSEQ_1:44; then f is non constant by A2; hence thesis by A1; end; end; registration let f be non empty real-valued FinSequence; let n be Nat; cluster f | Seg n -> real-valued; coherence; end; registration let f be positive non empty real-valued FinSequence; let n be Nat; cluster f | Seg n -> positive; coherence proof set g = f | Seg n; for k being Nat st k in dom g holds g.k > 0 proof let k be Nat; A1: dom g c= dom f by RELAT_1:60; assume A3: k in dom g; then f.k > 0 by PosDef,A1; hence thesis by FUNCT_1:47,A3; end; hence thesis; 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; aa: m <= len g by A8,FINSEQ_3:25; 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; A12: m = m1+1; then A13: Seg m1 c= Seg m by FINSEQ_1:5,NAT_1:11; m in Seg m by A11; then gm.m = a by A8,A9,RFINSEQ:6; then A14: gm = (gm|m1)^<*a*> by aa,A12,RFINSEQ:7,FINSEQ_1:59; 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 .= Product (w | (i-'1)) * aa * Product (w/^i) by RVSUM_1:95 .= 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 .= Product (w | (i-'1)) * fi * Product (w/^i) by RVSUM_1:95 .= 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; theorem ::\$N Inequality of arithmetic and geometric means 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;