:: 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; begin :: Preliminaries theorem :: RVSUM_3:1 for x, y, z, w being Real st |. x - y .| < |. z - w .| holds (x - y) ^2 < (z - w) ^2; 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; 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 :: RVSUM_3:def 1 for n being Nat st n in dom f holds f.n > 0; end; registration cluster non empty constant positive for real-valued FinSequence; cluster non empty non constant positive for real-valued FinSequence; end; registration let f be non empty real-valued FinSequence; let n be Nat; cluster f | Seg n -> real-valued; end; registration let f be positive non empty real-valued FinSequence; let n be Nat; cluster f | Seg n -> positive; 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 :: RVSUM_3:3 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; theorem :: RVSUM_3:4 ::: 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; begin :: Arithmetic Mean and Geometric Mean definition let f be real-valued FinSequence; func Mean f -> real number equals :: RVSUM_3:def 2 (Sum f) / len f; end; definition let f be positive real-valued FinSequence; func GMean f -> real number equals :: RVSUM_3:def 3 (len f)-root (Product f); end; theorem :: RVSUM_3:5 for f being real-valued FinSequence holds Sum f = (len f) * (Mean f); theorem :: RVSUM_3:6 for f being real-valued FinSequence holds Mean (f ^ <*Mean f*>) = Mean f; registration let f be non empty constant real-valued FinSequence; cluster the_value_of f -> real; end; theorem :: RVSUM_3:7 for f being non empty constant real-valued FinSequence holds Sum f = (the_value_of f) * (len f); theorem :: RVSUM_3:8 for f being non empty constant real-valued FinSequence holds Product f = (the_value_of f) |^ (len f); theorem :: RVSUM_3:9 for f being non empty constant real-valued FinSequence holds Mean f = the_value_of f; theorem :: RVSUM_3:10 for f being non empty constant positive real-valued FinSequence holds the_value_of f > 0; theorem :: RVSUM_3:11 for f being non empty constant positive real-valued FinSequence holds GMean f = the_value_of f; registration let f be non empty positive real-valued FinSequence; cluster Mean f -> positive; end; registration let f be non empty positive real-valued FinSequence; cluster Product f -> positive; end; registration let f be positive non empty real-valued FinSequence; cluster GMean f -> positive; end; begin :: Heterogeneity of a Finite Sequence 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 }; end; registration let f be real-valued FinSequence; cluster HetSet f -> finite; end; registration let f be positive non empty real-valued FinSequence; cluster HetSet f -> bounded_above bounded_below real-membered; end; definition let f be real-valued FinSequence; func Het f -> Nat equals :: RVSUM_3:def 5 card HetSet f; end; theorem :: RVSUM_3:12 for f being real-valued FinSequence st Het f = 0 holds f is homogeneous; theorem :: RVSUM_3:13 for f being non empty real-valued FinSequence st Het f <> 0 holds f is heterogeneous; registration let f be heterogeneous positive non empty real-valued FinSequence; cluster HetSet f -> non empty; end; theorem :: RVSUM_3:14 for f being non empty homogeneous positive real-valued FinSequence holds Mean f = GMean f; 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; symmetry; end; 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; :: 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 }; func MeanMore f -> Subset of NAT equals :: RVSUM_3:def 8 { n where n is Nat : n in dom f & f.n > Mean f }; end; theorem :: RVSUM_3:16 for f being real-valued FinSequence holds HetSet f c= dom f; theorem :: RVSUM_3:17 for f being real-valued FinSequence holds MeanLess f c= dom f; theorem :: RVSUM_3:18 for f being real-valued FinSequence holds MeanMore f c= dom f; theorem :: RVSUM_3:19 for f being real-valued FinSequence holds HetSet f = MeanLess f \/ MeanMore f; registration let f be heterogeneous real-valued FinSequence; cluster MeanLess f -> non empty; cluster MeanMore f -> non empty; end; registration let f be homogeneous real-valued FinSequence; cluster MeanLess f -> empty; cluster MeanMore f -> empty; end; theorem :: RVSUM_3:20 for f be heterogeneous non empty real-valued FinSequence holds MeanLess f misses MeanMore f; theorem :: RVSUM_3:21 for f be heterogeneous non empty real-valued FinSequence holds Het f >= 2; 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 :: RVSUM_3:def 9 (f+*(i,a))+*(j,b); end; theorem :: RVSUM_3:22 for f being FinSequence, i,j being Nat, a,b being object holds dom Replace (f,i,j,a,b) = dom f; 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; end; theorem :: RVSUM_3:23 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); theorem :: RVSUM_3:24 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; theorem :: RVSUM_3:25 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); theorem :: RVSUM_3:26 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; theorem :: RVSUM_3:27 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)); theorem :: RVSUM_3:28 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; theorem :: RVSUM_3:29 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; theorem :: RVSUM_3:30 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; theorem :: RVSUM_3:31 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; theorem :: RVSUM_3:32 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); theorem :: RVSUM_3:33 for f,g being positive non empty real-valued FinSequence st len f = len g & Product f < Product g holds GMean f < GMean g; theorem :: RVSUM_3:34 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; theorem :: RVSUM_3:35 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; theorem :: RVSUM_3:36 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; theorem :: RVSUM_3:37 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; theorem :: RVSUM_3:38 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; theorem :: RVSUM_3:39 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; theorem :: RVSUM_3:40 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; theorem :: RVSUM_3:41 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; begin :: Homogenization of a Finite Sequence definition let f be heterogeneous positive non empty real-valued FinSequence; func Homogen f -> real-valued FinSequence means :: 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); end; theorem :: RVSUM_3:42 for f being heterogeneous positive non empty real-valued FinSequence holds dom Homogen f = dom f; registration let f be heterogeneous positive non empty real-valued FinSequence; cluster Homogen f -> non empty; end; registration let f be heterogeneous positive non empty real-valued FinSequence; cluster Homogen f -> positive; end; theorem :: RVSUM_3:43 for f be heterogeneous positive non empty real-valued FinSequence holds Het Homogen f < Het f; theorem :: RVSUM_3:44 for f be heterogeneous positive non empty real-valued FinSequence holds Homogen f, f are_gamma-equivalent; theorem :: RVSUM_3:45 for f be heterogeneous positive non empty real-valued FinSequence holds GMean Homogen f > GMean f; begin :: Cauchy Mean Theorem theorem :: RVSUM_3:46 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; theorem :: RVSUM_3:47 ::\$N Inequality of arithmetic and geometric means for f being non empty positive real-valued FinSequence holds GMean f <= Mean f;