Nuprl Definition : rat-sign-change-list
L is a list of rational numbers a < L[0] < L[1] < ... < L[||L||-1] < b,
and f(b) is positive. Working backward down the list,
f(L[n-1]) is negative, f(L[n-2]) is positive, etc, and f(a) has the opposite
sign from f(L[0]).
If L =[], this just says a < b and f(a) negative and f(b) positive.⋅
rat-sign-change-list(f;a;b;
L) ==
(∀i:ℕ||L||. ratless(if (i =z 0) then a else L[i - 1] fi ;L[i]))
∧ ratless(if (||L|| =z 0) then a else L[||L|| - 1] fi ;b)
∧ (∀i:ℕ||L||. (ratsign(f L[i]) = (-1)^(||L|| - i) ∈ ℤ))
∧ (ratsign(f b) = 1 ∈ ℤ)
∧ (ratsign(f a) = (-1)^(||L|| + 1) ∈ ℤ)
Definitions occuring in Statement :
ratless: ratless(x;y),
ratsign: ratsign(x),
exp: i^n,
select: L[n],
length: ||as||,
int_seg: {i..j-},
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
all: ∀x:A. B[x],
and: P ∧ Q,
apply: f a,
subtract: n - m,
add: n + m,
minus: -n,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
ratless: ratless(x;y),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
all: ∀x:A. B[x],
int_seg: {i..j-},
select: L[n],
subtract: n - m,
and: P ∧ Q,
equal: s = t ∈ T,
int: ℤ,
ratsign: ratsign(x),
apply: f a,
exp: i^n,
minus: -n,
add: n + m,
length: ||as||,
natural_number: $n
FDL editor aliases :
rat-sign-change-list
Latex:
rat-sign-change-list(f;a;b;
L) ==
(\mforall{}i:\mBbbN{}||L||. ratless(if (i =\msubz{} 0) then a else L[i - 1] fi ;L[i]))
\mwedge{} ratless(if (||L|| =\msubz{} 0) then a else L[||L|| - 1] fi ;b)
\mwedge{} (\mforall{}i:\mBbbN{}||L||. (ratsign(f L[i]) = (-1)\^{}(||L|| - i)))
\mwedge{} (ratsign(f b) = 1)
\mwedge{} (ratsign(f a) = (-1)\^{}(||L|| + 1))
Date html generated:
2019_10_30-AM-09_55_08
Last ObjectModification:
2019_01_17-AM-10_48_07
Theory : reals
Home
Index