:: Average Value Theorems for Real Functions of One Variable :: by Jaros{\l}aw Kotowicz, Konrad Raczkowski and Pawe{\l} Sadowski :: :: Received June 18, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin theorem Th1: :: ROLLE:1 for p, g being Real st p < g holds for f being PartFunc of REAL,REAL st [.p,g.] c= dom f & f | [.p,g.] is continuous & f . p = f . g & f is_differentiable_on ].p,g.[ holds ex x0 being Real st ( x0 in ].p,g.[ & diff (f,x0) = 0 ) proofend; :: [WP: ] Rolle_Theorem theorem :: ROLLE:2 for x, t being Real st 0 < t holds for f being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f . x = f . (x + t) & f is_differentiable_on ].x,(x + t).[ holds ex s being Real st ( 0 < s & s < 1 & diff (f,(x + (s * t))) = 0 ) proofend; :: [WP: ] The_Mean_Value_Theorem theorem Th3: :: ROLLE:3 for p, g being Real st p < g holds for f being PartFunc of REAL,REAL st [.p,g.] c= dom f & f | [.p,g.] is continuous & f is_differentiable_on ].p,g.[ holds ex x0 being Real st ( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) ) proofend; :: [WP: ] Lagrange_Theorem theorem :: ROLLE:4 for x, t being Real st 0 < t holds for f being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f is_differentiable_on ].x,(x + t).[ holds ex s being Real st ( 0 < s & s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) ) proofend; theorem Th5: :: ROLLE:5 for p, g being Real st p < g holds for f1, f2 being PartFunc of REAL,REAL st [.p,g.] c= dom f1 & [.p,g.] c= dom f2 & f1 | [.p,g.] is continuous & f1 is_differentiable_on ].p,g.[ & f2 | [.p,g.] is continuous & f2 is_differentiable_on ].p,g.[ holds ex x0 being Real st ( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) ) proofend; :: [WP: ] Cauchy_Theorem theorem :: ROLLE:6 for x, t being Real st 0 < t holds for f1, f2 being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f1 & [.x,(x + t).] c= dom f2 & f1 | [.x,(x + t).] is continuous & f1 is_differentiable_on ].x,(x + t).[ & f2 | [.x,(x + t).] is continuous & f2 is_differentiable_on ].x,(x + t).[ & ( for x1 being Real st x1 in ].x,(x + t).[ holds diff (f2,x1) <> 0 ) holds ex s being Real st ( 0 < s & s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff (f1,(x + (s * t)))) / (diff (f2,(x + (s * t)))) ) proofend; theorem Th7: :: ROLLE:7 for p, g being Real for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds diff (f,x) = 0 ) holds f | ].p,g.[ is V8() proofend; theorem :: ROLLE:8 for p, g being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on ].p,g.[ & f2 is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds diff (f1,x) = diff (f2,x) ) holds ( (f1 - f2) | ].p,g.[ is V8() & ex r being Real st for x being Real st x in ].p,g.[ holds f1 . x = (f2 . x) + r ) proofend; theorem :: ROLLE:9 for p, g being Real for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds 0 < diff (f,x) ) holds f | ].p,g.[ is increasing proofend; theorem :: ROLLE:10 for p, g being Real for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds diff (f,x) < 0 ) holds f | ].p,g.[ is decreasing proofend; theorem :: ROLLE:11 for p, g being Real for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds 0 <= diff (f,x) ) holds f | ].p,g.[ is non-decreasing proofend; theorem :: ROLLE:12 for p, g being Real for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds diff (f,x) <= 0 ) holds f | ].p,g.[ is non-increasing proofend;