---

Step * of Lemma near-log_wf

∀[a:{a:ℝ| r0 < a} ]. ∀[N:ℕ+].  (near-log(a;N) ∈ {r:ℕ+ × ℤ| let j,c = r in |(r(c))/j - rlog(a)| ≤ (r1/r(N))} )
BY
{ (Fold `sq_exists` 0
   THEN ProveWfLemma
   THEN (DoSubsume THENL [Auto; ((D 0 THENA Auto) THEN RepeatFor 2 (D -1) THEN MemTypeCD THEN Reduce 0 THEN Auto)])) }

---

Latex:

---

Latex:
\mforall{}[a:\{a:\mBbbR{}|  r0  <  a\}  ].  \mforall{}[N:\mBbbN{}\msupplus{}].
    (near-log(a;N)  \mmember{}  \{r:\mBbbN{}\msupplus{}  \mtimes{}  \mBbbZ{}|  let  j,c  =  r  in  |(r(c))/j  -  rlog(a)|  \mleq{}  (r1/r(N))\}  )


By

---

Latex:
(Fold  `sq\_exists`  0
  THEN  ProveWfLemma
  THEN  (DoSubsume
              THENL  [Auto
                          ;  ((D  0  THENA  Auto)  THEN  RepeatFor  2  (D  -1)  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)]
  ))

---

Home Index