Nuprl Definition : derivative

The bound ⌜(r1/r(k))⌝ is a positive ⌜∈⌝.
The interval J = ⌜i-approx(I;n)⌝ is "any" compact subinterval of I.
(It is really one of a countable nested family of finite, closed intervals
that "fill up" the interval I.)
Given this, the "modulus of differentiabilty" computes a positive "delta" such
that for x and y in J,
if ⌜|y - x| ≤ del⌝ then
|f[y] - f[x] - f'[x] * (y - x)| ≤ (∈ * |y - x|)

The interval J is restricted to being a proper interval [a,b], where a < b,
because it doesn't make sense for a function defined on only one point to
have a derivative.
One might think that if J is not proper then (x ∈ J) ∧ (y ∈ J) would imply
x = y so ⌜(f[y] - f[x]) = r0⌝ and also (y - x) = r0
so any value for ⌜f'[x]⌝ would satisfy the inequality,
for any del (say del = r1).
But, in general,
if ⌜a ≤ b⌝ we can not decide whether or not ⌜a < b⌝, so this does not work.
In the proof of the fundamental theorem of calculus, we can only show that
(g x) = a_∫^-x f t dt is differentiable (with derivative f) when we can restrict
to proper, compact intervals J..⋅

d(f[x])/dx = λz.g[z] on I ==
  ∀k:ℕ⁺. ∀n:{n:ℕ⁺| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} .
    (∃del:{ℝ| ((r0 < del)
              ∧ (∀x,y:ℝ.
                   ((x ∈ i-approx(I;n))
                   ⇒ (y ∈ i-approx(I;n))
                   ⇒ (|y - x| ≤ del)
                   ⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))})

Definitions occuring in Statement : icompact: icompact(I), i-approx: i-approx(I;n), i-member: r ∈ I, iproper: iproper(I), rdiv: (x/y), rleq: x ≤ y, rless: x < y, rabs: |x|, rsub: x - y, rmul: a * b, int-to-real: r(n), real: ℝ, nat_plus: ℕ⁺, all: ∀x:A. B[x], sq_exists: ∃x:{A| B[x]}, implies: P ⇒ Q, and: P ∧ Q, set: {x:A| B[x]} , natural_number: $n
Definitions occuring in definition : rsub: x - y, rabs: |x|, int-to-real: r(n), natural_number: $n, rdiv: (x/y), rmul: a * b, rleq: x ≤ y, implies: P ⇒ Q, i-approx: i-approx(I;n), i-member: r ∈ I, real: ℝ, all: ∀x:A. B[x], rless: x < y, and: P ∧ Q, sq_exists: ∃x:{A| B[x]}, iproper: iproper(I), icompact: icompact(I), nat_plus: ℕ⁺, set: {x:A| B[x]}
FDL editor aliases : deriv

Latex:
d(f[x])/dx = \mlambda{}z.g[z] on I == \mforall{}k:\mBbbN{}\msupplus{}. \mforall{}n:\{n:\mBbbN{}\msupplus{}| icompact(i-approx(I;n)) \mwedge{} iproper(i-approx(I;n))\} . (\mexists{}del:\{\mBbbR{}| ((r0 < del) \mwedge{} (\mforall{}x,y:\mBbbR{}. ((x \mmember{} i-approx(I;n)) {}\mRightarrow{} (y \mmember{} i-approx(I;n)) {}\mRightarrow{} (|y - x| \mleq{} del) {}\mRightarrow{} (|f[y] - f[x] - g[x] * (y - x)| \mleq{} ((r1/r(k)) * |y - x|)))))\}) Date html generated: 2016_10_26-AM-11_18_53 Last ObjectModification: 2016_08_22-PM-08_21_43 Theory : reals Home Index