:: The First Mean Value Theorem for Integrals :: by Keiko Narita , Noboru Endou and Yasunari Shidama :: :: Received October 30, 2007 :: Copyright (c) 2007-2016 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, XBOOLE_0, PROB_1, MEASURE1, PARTFUN1, SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, ARYTM_1, SUPINF_2, SUPINF_1, CARD_1, REAL_1, VALUED_1, INTEGRA5, MESFUNC5, ARYTM_3, MESFUNC1, COMPLEX1, TARSKI, MESFUNC2, VALUED_0, FINSEQ_1, BINOP_1, SETWISEO, CARD_3, FINSEQ_2, NEWTON, ORDINAL4, NAT_1, POWER, SQUARE_1, XXREAL_2, ORDINAL2, RFUNCT_3, FUNCT_3, MESFUNC7, XCMPLX_0; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, VALUED_0, XXREAL_3, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, XXREAL_2, MEASURE1, NAT_1, SUPINF_1, RELAT_1, RELSET_1, SETWISEO, PARTFUN1, FUNCT_1, FINSEQ_1, FINSEQ_2, SETWOP_2, BINOP_1, FUNCT_2, NEWTON, SQUARE_1, PROB_1, SUPINF_2, EXTREAL1, POWER, MESFUNC5, MESFUNC1, MESFUNC2, MEASURE6; constructors REAL_1, FINSOP_1, EXTREAL1, BINOP_1, NEWTON, POWER, MESFUNC1, MEASURE6, MESFUNC2, MEASURE3, SETWISEO, SQUARE_1, MESFUNC5, SUPINF_1, RELSET_1, BINOP_2, FINSEQ_2; registrations SUBSET_1, NAT_1, RELSET_1, XREAL_0, MEMBERED, ORDINAL1, FINSEQ_1, MEASURE1, NUMBERS, XXREAL_0, XBOOLE_0, VALUED_0, POWER, XXREAL_3, SQUARE_1, NEWTON, CARD_1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Lemmas for extended real valued functions reserve X for non empty set, S for SigmaField of X, M for sigma_Measure of S, f,g for PartFunc of X,ExtREAL, E for Element of S; theorem :: MESFUNC7:1 (for x be Element of X st x in dom f holds f.x <= g.x) implies g- f is nonnegative; theorem :: MESFUNC7:2 for Y be set, f be PartFunc of X,ExtREAL, r be Real holds (r(#)f) |Y = r(#)(f|Y); theorem :: MESFUNC7:3 f is_integrable_on M & g is_integrable_on M & g-f is nonnegative implies ex E be Element of S st E = dom f /\ dom g & Integral(M,f|E) <= Integral(M,g|E); begin :: Sigma finite set registration let X; cluster nonnegative for PartFunc of X,ExtREAL; end; registration let X,f; cluster |.f.| -> nonnegative for PartFunc of X,ExtREAL; end; theorem :: MESFUNC7:4 f is_integrable_on M implies ex F be sequence of S st ( for n be Element of NAT holds F.n = dom f /\ great_eq_dom(|.f.|, (1/(n+1))) ) & dom f \ eq_dom(f, 0.) = union rng F & for n be Element of NAT holds F.n in S & M.(F .n) <+infty; begin :: The first mean value theorem for integrals notation let F be Relation; synonym F is extreal-yielding for F is ext-real-valued; end; registration cluster extreal-yielding for FinSequence; end; definition func multextreal -> BinOp of ExtREAL means :: MESFUNC7:def 1 for x,y be Element of ExtREAL holds it.(x,y) = x*y; end; registration cluster multextreal -> commutative associative; end; theorem :: MESFUNC7:5 the_unity_wrt multextreal = 1; registration cluster multextreal -> having_a_unity; end; definition let F be extreal-yielding FinSequence; func Product F -> Element of ExtREAL means :: MESFUNC7:def 2 ex f being FinSequence of ExtREAL st f = F & it = multextreal \$\$ f; end; registration let x be Element of ExtREAL, n be Nat; cluster n |-> x -> extreal-yielding; end; definition let x be Element of ExtREAL; let k be Nat; func x |^ k -> set equals :: MESFUNC7:def 3 Product (k |-> x); end; definition let x be Element of ExtREAL, k be Nat; redefine func x |^ k -> R_eal; end; registration cluster <*>ExtREAL -> extreal-yielding; end; registration let r be Element of ExtREAL; cluster <*r*> -> extreal-yielding; end; theorem :: MESFUNC7:6 Product (<*>ExtREAL) = 1; theorem :: MESFUNC7:7 for r be Element of ExtREAL holds Product (<*r*>) = r; registration let f,g be extreal-yielding FinSequence; cluster f^g -> extreal-yielding; end; theorem :: MESFUNC7:8 for F being extreal-yielding FinSequence, r be Element of ExtREAL holds Product (F^<*r*>) = Product F * r; theorem :: MESFUNC7:9 for x be Element of ExtREAL holds x|^1 = x; theorem :: MESFUNC7:10 for x be Element of ExtREAL, k be Nat holds x|^(k+1) = x|^k*x; definition let k be Nat, X,f; func f|^k -> PartFunc of X,ExtREAL means :: MESFUNC7:def 4 dom it = dom f & for x be Element of X st x in dom it holds it.x = (f.x)|^k; end; theorem :: MESFUNC7:11 for x be Element of ExtREAL, y be Real, k be Nat st x=y holds x|^k = y|^k; theorem :: MESFUNC7:12 for x be Element of ExtREAL, k be Nat st 0 <=x holds 0 <= x|^k; theorem :: MESFUNC7:13 for k be Nat st 1<=k holds +infty|^k =+infty; theorem :: MESFUNC7:14 for k be Nat, X,S,f,E st E c= dom f & f is_measurable_on E holds (|.f.|) |^ k is_measurable_on E; theorem :: MESFUNC7:15 dom f /\ dom g = E & f is real-valued & g is real-valued & f is_measurable_on E & g is_measurable_on E implies f(#)g is_measurable_on E; theorem :: MESFUNC7:16 rng f is real-bounded implies f is real-valued; ::\$N Mean value theorem for integrals (first) theorem :: MESFUNC7:17 for M be sigma_Measure of S, f,g be PartFunc of X, ExtREAL, E be Element of S, F be non empty Subset of ExtREAL st dom f /\ dom g = E & rng f = F & g is real-valued & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds (f(#)g)|E is_integrable_on M & ex c be Element of REAL st c >= inf F & c <= sup F & Integral(M, (f(#)|.g.|)|E) = c * Integral(M, (|.g.|)|E); begin :: Selected properties of integrals reserve E1,E2 for Element of S; reserve x,A for set; reserve a,b for Real; theorem :: MESFUNC7:18 (|.f.|)|A = |.(f|A).|; theorem :: MESFUNC7:19 dom(|.f.|+|.g.|) = dom f /\ dom g & dom |.f+g.| c= dom |.f.|; theorem :: MESFUNC7:20 (|.f.|)|(dom |.f+g.|) + (|.g.|)|(dom |.f+g.|) = (|.f.|+|.g.|)|( dom |.f+g.|); theorem :: MESFUNC7:21 x in dom |.f+g.| implies (|.f+g.|).x <= (|.f.|+|.g.|).x; theorem :: MESFUNC7:22 f is_integrable_on M & g is_integrable_on M implies ex E be Element of S st E = dom(f+g) & Integral(M,(|.f+g.|)|E) <= Integral(M,(|.f.|)|E) + Integral (M,(|.g.|)|E); theorem :: MESFUNC7:23 max+(chi(A,X)) = chi(A,X); theorem :: MESFUNC7:24 M.E < +infty implies chi(E,X) is_integrable_on M & Integral(M, chi(E,X)) = M.E & Integral(M,(chi(E,X))|E) = M.E; theorem :: MESFUNC7:25 M.(E1/\E2) < +infty implies Integral(M,(chi(E1,X))|E2) = M.(E1/\ E2); theorem :: MESFUNC7:26 f is_integrable_on M & E c= dom f & M.E < +infty & (for x be Element of X st x in E holds a <= f.x & f.x <= b) implies ( a)*M.E <= Integral(M,f |E) & Integral(M,f|E) <= (b)*M.E;