Nuprl Definition : Legendre_zero
Legendre_zero(n;i) ==
eval L = Legendre_changes(n) in
rational-fun-zero(λx.int-rat-mul(-1^n - i - 1;ratLegendre(n;x));if i=0 then <-1, 1> else L[i - 1];if i=n - 1
then <1, 1>
else L[i])
Definitions occuring in Statement :
Legendre_changes: Legendre_changes(n),
ratLegendre: ratLegendre(n;x),
rational-fun-zero: rational-fun-zero(f;a;b),
int-rat-mul: int-rat-mul(n;x),
fastexp: i^n,
select: L[n],
callbyvalue: callbyvalue,
int_eq: if a=b then c else d,
lambda: λx.A[x],
pair: <a, b>,
subtract: n - m,
minus: -n,
natural_number: $n
Definitions occuring in definition :
callbyvalue: callbyvalue,
Legendre_changes: Legendre_changes(n),
rational-fun-zero: rational-fun-zero(f;a;b),
lambda: λx.A[x],
int-rat-mul: int-rat-mul(n;x),
fastexp: i^n,
ratLegendre: ratLegendre(n;x),
minus: -n,
int_eq: if a=b then c else d,
subtract: n - m,
pair: <a, b>,
natural_number: $n,
select: L[n]
FDL editor aliases :
Legendre_zero
Latex:
Legendre\_zero(n;i) ==
eval L = Legendre\_changes(n) in
rational-fun-zero(\mlambda{}x.int-rat-mul(-1\^{}n - i - 1;ratLegendre(n;x));if i=0
then <-1, 1>
else L[i - 1];if i=n - 1
then ə, 1>
else L[i])
Date html generated:
2019_10_31-AM-06_22_59
Last ObjectModification:
2019_01_19-PM-11_05_49
Theory : reals_2
Home
Index