Step
*
of Lemma
sine-small_wf
No Annotations
∀[x:{x:ℝ| |x| ≤ (r1/r(2))} ]. (sine-small(x) ∈ {y:ℝ| y = sine(x)} )
BY
{ (Auto
THEN Unfold `sine-small` 0
THEN (Subst' λN.sine-approx(x;genfact-inv(N;48;k.4 * ((2 * k) + 3) * ((2 * k) + 2));N)
~ λN.(TERMOF{sine-approx-for-small-ext:o, \\v:l} 2 N x) 0
THENA ((RW (AddrC [2;1] (TagC (mk_tag_term 2))) 0 THEN Reduce 0) THEN RepeatFor 3 (EqCD) THEN Auto)
)
THEN BLemma `accelerate-rational-approx`
THEN Auto
THEN (GenConclTerm ⌜TERMOF{sine-approx-for-small-ext:o, \\v:l} 2⌝⋅ THENA Auto)) }
1
1. x : {x:ℝ| |x| ≤ (r1/r(2))}
2. n : ℕ+
3. v : ∀N:ℕ+. ∀x:{x:ℝ| |x| ≤ (r1/r(2))} . (∃z:ℤ [(|sine(x) - (r(z)/r(2 * N))| ≤ (r(2)/r(N)))])
4. (TERMOF{sine-approx-for-small-ext:o, \\v:l} 2)
= v
∈ (∀N:ℕ+. ∀x:{x:ℝ| |x| ≤ (r1/r(2))} . (∃z:ℤ [(|sine(x) - (r(z)/r(2 * N))| ≤ (r(2)/r(N)))]))
⊢ |sine(x) - (r((λN.(v N x)) n)/r(2 * n))| ≤ (r(2)/r(n))
Latex:
Latex:
No Annotations
\mforall{}[x:\{x:\mBbbR{}| |x| \mleq{} (r1/r(2))\} ]. (sine-small(x) \mmember{} \{y:\mBbbR{}| y = sine(x)\} )
By
Latex:
(Auto
THEN Unfold `sine-small` 0
THEN (Subst' \mlambda{}N.sine-approx(x;genfact-inv(N;48;k.4 * ((2 * k) + 3) * ((2 * k) + 2));N)
\msim{} \mlambda{}N.(TERMOF\{sine-approx-for-small-ext:o, \mbackslash{}\mbackslash{}v:l\} 2 N x) 0
THENA ((RW (AddrC [2;1] (TagC (mk\_tag\_term 2))) 0 THEN Reduce 0)
THEN RepeatFor 3 (EqCD)
THEN Auto)
)
THEN BLemma `accelerate-rational-approx`
THEN Auto
THEN (GenConclTerm \mkleeneopen{}TERMOF\{sine-approx-for-small-ext:o, \mbackslash{}\mbackslash{}v:l\} 2\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index