Nuprl Lemma : sine-poly-approx-1

[x:{x:ℝ(r0 ≤ x) ∧ (x ≤ r1)} ]. ∀[k:ℕ].
  (|sine(x) - Σ{-1^i (x^(2 i) 1)/((2 i) 1)! 0≤i≤k}| ≤ (x^(2 k) 3/r(((2 k) 3)!)))


Proof




Definitions occuring in Statement :  sine: sine(x) rsum: Σ{x[k] n≤k≤m} rdiv: (x/y) rleq: x ≤ y rabs: |x| rnexp: x^k1 int-rdiv: (a)/k1 int-rmul: k1 a rsub: y int-to-real: r(n) real: fastexp: i^n fact: (n)! nat: uall: [x:A]. B[x] and: P ∧ Q set: {x:A| B[x]}  multiply: m add: m minus: -n natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: so_lambda: λ2x.t[x] int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q le: A ≤ B less_than: a < b squash: T ge: i ≥  all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False prop: subtype_rel: A ⊆B so_apply: x[s] rneq: x ≠ y guard: {T} iff: ⇐⇒ Q rev_implies:  Q nat_plus: + uiff: uiff(P;Q) series-sum: Σn.x[n] a converges-to: lim n→∞.x[n] y sq_exists: x:A [B[x]] less_than': less_than'(a;b) rless: x < y sq_stable: SqStable(P) rleq: x ≤ y rnonneg: rnonneg(x) real: rev_uimplies: rev_uimplies(P;Q) rge: x ≥ y top: Top rdiv: (x/y) req_int_terms: t1 ≡ t2 cand: c∧ B subtract: m true: True int_upper: {i...} sq_type: SQType(T) nequal: a ≠ b ∈  int_nzero: -o

Latex:
\mforall{}[x:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  ].  \mforall{}[k:\mBbbN{}].
    (|sine(x)  -  \mSigma{}\{-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}k\}|  \mleq{}  (x\^{}(2  *  k)  +  3/r(((2  *  k)  +  3)!)))



Date html generated: 2020_05_20-AM-11_25_09
Last ObjectModification: 2020_01_06-PM-01_15_24

Theory : reals


Home Index