Nuprl Lemma : cosine-approx-property

[x:ℝ]. ∀[k:ℕ]. ∀[N:ℕ+].  ((|x| ≤ (r1/r(2)))  1-approx(Σ{-1^i (x^2 i)/(2 i)! 0≤i≤k};N;cosine-approx(x;k;N)))


Proof




Definitions occuring in Statement :  cosine-approx: cosine-approx(x;k;N) ireal-approx: j-approx(x;M;z) 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 int-to-real: r(n) real: fastexp: i^n fact: (n)! nat_plus: + nat: uall: [x:A]. B[x] implies:  Q multiply: m minus: -n natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q nat: true: True nequal: a ≠ b ∈  not: ¬A uimplies: supposing a sq_type: SQType(T) all: x:A. B[x] guard: {T} false: False bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  nat_plus: + ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top prop: subtype_rel: A ⊆B bfalse: ff bnot: ¬bb assert: b so_lambda: λ2x.t[x] int_seg: {i..j-} lelt: i ≤ j < k less_than: a < b squash: T le: A ≤ B less_than': less_than'(a;b) so_apply: x[s] pointwise-req: x[k] y[k] for k ∈ [n,m] iff: ⇐⇒ Q rev_implies:  Q cosine-approx: cosine-approx(x;k;N) rneq: x ≠ y ireal-approx: j-approx(x;M;z) rleq: x ≤ y rnonneg: rnonneg(x) exp: i^n primrec: primrec(n;b;c) primtailrec: primtailrec(n;i;b;f) subtract: m int_nzero: -o rev_uimplies: rev_uimplies(P;Q) rge: x ≥ y req_int_terms: t1 ≡ t2 rdiv: (x/y)
Lemmas referenced :  poly-approx-property subtype_base_sq int_subtype_base istype-int eq_int_wf eqtt_to_assert assert_of_eq_int int-rdiv_wf fact_wf nat_properties nat_plus_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermMultiply_wf itermVar_wf int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_mul_lemma int_term_value_var_lemma int_formula_prop_wf istype-le eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot neg_assert_of_eq_int int-to-real_wf rnexp_wf rsum_functionality rmul_wf int_seg_properties int_seg_subtype_nat istype-false int_seg_wf int-rmul_wf fastexp_wf equal_wf squash_wf true_wf istype-universe exp-minusone subtype_rel_self iff_weakening_equal modulus-is-rem ireal-approx_functionality cosine-approx_wf rsum_wf rleq_wf rabs_wf rdiv_wf rless-int rless_wf le_witness_for_triv nat_plus_wf istype-nat real_wf exp_wf2 req-int-fractions nequal_wf exp_wf3 rleq_functionality_wrt_implies rnexp_functionality_wrt_rleq zero-rleq-rabs rleq_weakening_equal rleq_weakening itermSubtract_wf req-iff-rsub-is-0 nat_plus_inc_int_nzero rmul_preserves_req decidable__lt intformless_wf intformeq_wf int_formula_prop_less_lemma int_formula_prop_eq_lemma rinv_wf2 exp-fastexp req_weakening rleq_functionality rabs-rnexp req_functionality req_inversion rnexp-rdiv rneq_functionality rnexp-int rdiv_functionality real_polynomial_null real_term_value_sub_lemma real_term_value_var_lemma real_term_value_const_lemma rmul_functionality int-rdiv-req req_transitivity int-rmul-req rmul-rinv3 real_term_value_mul_lemma rnexp-mul
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut lambdaFormation_alt extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality_alt remainderEquality setElimination rename because_Cache hypothesis natural_numberEquality instantiate cumulativity intEquality independent_isectElimination dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination voidElimination equalityIstype baseClosed sqequalBase closedConclusion inhabitedIsType unionElimination equalityElimination productElimination sqequalRule dependent_set_memberEquality_alt multiplyEquality approximateComputation dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt independent_pairFormation universeIsType applyEquality promote_hyp imageElimination addEquality minusEquality universeEquality imageMemberEquality inrFormation_alt functionIsTypeImplies isectIsTypeImplies applyLambdaEquality

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[k:\mBbbN{}].  \mforall{}[N:\mBbbN{}\msupplus{}].
    ((|x|  \mleq{}  (r1/r(2)))  {}\mRightarrow{}  1-approx(\mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  |  0\mleq{}i\mleq{}k\};N;cosine-approx(x;k;N)))



Date html generated: 2019_10_29-AM-10_36_32
Last ObjectModification: 2019_02_02-AM-11_35_07

Theory : reals


Home Index