------------------------------ MODULE Calculus ------------------------------
EXTENDS Reals
OpenInterval(a, b) == {r \in Real : (a < r) /\ (r < b)}
ClosedInterval(a, b) == {r \in Real : (a \leq r) /\ (r \leq b)}
SetOfIntervals == {S \in SUBSET Real : \A x, y \in S : OpenInterval(x, y) \subseteq S}
RealFunction == UNION {[S -> Real] : S \in SUBSET Real}
AbsoluteValue(a) == IF a > 0 THEN a ELSE -a
OpenBall(a, e) == {x \in Real : e > AbsoluteValue(x-a)}
PositiveReal == {r \in Real : r > 0}
IsLimitAt(f, a, b) == (b \in Real) /\
\A e \in PositiveReal : \E d \in PositiveReal :
\A x \in OpenBall(a, d) \ {a} : f[x] \in OpenBall(b, e)
IsContinuousAt(f, a) == IsLimitAt(f, a, f[a])
IsContinuousOn(f, S) == \A x \in S : IsContinuousAt(f, x)
IsDerivativeAt(f, a, b) ==
\E e \in PositiveReal :
(OpenBall(a, e) \subseteq DOMAIN f) /\
IsLimitAt([x \in OpenBall(a,e) \ {a} |-> (f[x] - f[a]) / (x - a)], a, b)
IsDifferentiableAt(f, a) == \E b \in Real : IsDerivativeAt(f, a, b)
IsDifferentiableOn(f, S) == \A x \in S : IsDifferentiableAt(f, x)
Derivative(f) == [x \in DOMAIN f |-> CHOOSE y : IsDerivativeAt(f, x, y)]
THEOREM Theorem1 == \A f \in RealFunction : \A a \in Real :
IsDifferentiableAt(f, a) => IsContinuousAt(f, a)
IsIncreasingOn(f, I) == \A x, y \in I : (x < y) => (f[x] < f[y])
THEOREM MeanValueTheorem ==
\A f \in RealFunction : \A a, b \in Real :
( (a < b)
/\ IsContinuousOn(f, ClosedInterval(a, b))
/\ IsDifferentiableOn(f, OpenInterval(a, b)))
=> (\E x \in OpenInterval(a,b) :
Derivative(f)[x] = (f[b]-f[a])/(b-a))
PROPOSITION Fact1 == \A x \in Real : x - x = 0
PROPOSITION Fact2 == \A x, y \in Real : (x \leq y) <=> (x < y) \/ (x = y)
PROPOSITION Fact3 == \A x, y \in Real : x - y \in Real
PROPOSITION Fact4 == \A x, y \in Real : (x < y) <=> (y - x > 0)
PROPOSITION Fact5 == \A x, y \in Real : (y > 0) /\ (x / y > 0) => (x > 0)
COROLLARY Spivak == ASSUME NEW f \in RealFunction,
NEW I \in SetOfIntervals,
IsDifferentiableOn(f, I),
\A x \in I : Derivative(f)[x] > 0
PROVE IsIncreasingOn(f, I)
<1>1. SUFFICES ASSUME NEW a \in I, NEW b \in I, a < b
PROVE f[a] < f[b]
BY DEF IsIncreasingOn
<1>1a. (OpenInterval(a, b) \subseteq I)
/\ (ClosedInterval(a, b) \subseteq I)
/\ (OpenInterval(a, b) \subseteq ClosedInterval(a, b))
<2>1. OpenInterval(a, b) \subseteq I
BY DEF SetOfIntervals
<2>2. ClosedInterval(a, b) = OpenInterval(a, b) \cup {a, b}
BY <1>1, Fact2 DEF ClosedInterval, OpenInterval, SetOfIntervals
<2>3. QED
BY <2>1, <2>2
<1>2. \E x \in OpenInterval(a, b) : Derivative(f)[x] = (f[b] - f[a]) / (b-a)
<2>1. IsDifferentiableOn(f, ClosedInterval(a, b))
BY <1>1a, <1>1 DEF IsDifferentiableOn
<2>2. IsContinuousOn(f, ClosedInterval(a, b))
<3>1. SUFFICES ASSUME NEW x \in ClosedInterval(a, b)
PROVE IsContinuousAt(f, x)
BY DEF IsContinuousOn
<3>2. IsDifferentiableAt(f, x)
BY <2>1 DEF IsDifferentiableOn
<3>3. QED
BY <3>2, Theorem1 DEF ClosedInterval
<2>3. QED
BY <1>1, <1>1a, <2>1, <2>2, MeanValueTheorem
DEF SetOfIntervals, IsDifferentiableOn
<1>3. \A x \in OpenInterval(a, b) : Derivative(f)[x] > 0
BY <1>1a
<1>4. (f[b] - f[a]) / (b-a) > 0
<2>1. PICK x \in OpenInterval(a, b) :
Derivative(f)[x] = (f[b] - f[a]) / (b-a)
BY <1>2
<2>2. Derivative(f)[x] > 0
BY <2>1 DEF SetOfIntervals
<2>3. QED
BY <2>1, <2>2
<1>5. QED
<2>1. (a \in Real) /\ (b \in Real)
BY DEF SetOfIntervals
<2>2. (f[a] \in Real) /\ (f[b] \in Real)
<3>1. SUFFICES ASSUME NEW x \in Real,
IsDifferentiableAt(f, x)
PROVE f[x] \in Real
BY <2>1 DEF IsDifferentiableOn
<3>2. \A e \in PositiveReal : x \in OpenBall(x, e)
BY Fact1 DEF OpenBall, PositiveReal, AbsoluteValue
<3>3. x \in DOMAIN f
BY <3>1, <3>2 DEF IsDifferentiableAt, IsDerivativeAt
<3>4. QED
BY <3>3 DEF IsDifferentiableAt, IsDerivativeAt, RealFunction
<2>3. (f[b] - f[a] \in Real) /\ (b - a \in Real)
BY <2>1, <2>2, Fact3
<2>4. f[b] - f[a] > 0
BY <1>1, <1>4, <2>1, <2>3, Fact4, Fact5
<2>5. QED
BY <2>2, <2>4, Fact4
=============================================================================
\* Modification History
\* Last modified Tue Sep 27 23:29:24 PDT 2011 by lamport
\* Created Sat Aug 13 11:38:21 PDT 2011 by lamport