---

Step * of Lemma near-log-exists-ext

∀a:{a:ℝ| r0 < a} . ∀N:ℕ+.  ∃m:ℕ+. (∃z:ℤ [(|(r(z))/m - rlog(a)| ≤ (r1/r(N)))])
BY
{ Extract of Obid: near-log-exists
  not unfolding  rdiv canonical-bound recdefs int-to-real int-rdiv rexp real_exp
  finishing with (Reduce 0 THEN RepUR ``so_lambda`` 0 THEN Try (Trivial))
  normalizes to:
  
  λa,N. eval x = 4 * (N + 1) in
        eval x1 = r1 x in
        eval x2 = a x in
          if (x1 + 4) < (x2)
             then eval b = canonical-bound(a) in
                  eval c = canonical-bound(real_exp(r(b))) in
                  eval M = N * c in
                    if ((M * (b - 0)) - 1) < (0)
                       then <1, b>
                       else let c1,j = letrec g(a@0)=λb,k. if (k) < (M * (b - a@0))
                                                              then eval m = a@0 + b in
                                                                   eval j = 2 * k in
                                                                   eval n4 = 4 * N in
                                                                   eval a1 = real_exp((r(m))/j) n4 in
                                                                   eval b1 = a n4 in
                                                                     if (a1 + 4) < (b1)
                                                                        then eval bb = 2 * b in
                                                                             let c,N = g m bb j 
                                                                             in <c, N>
                                                                        else if (b1 + 4) < (a1)
                                                                                then eval aa = 2 * a@0 in
                                                                                     let c,N = g aa m j 
                                                                                     in <c, N>
                                                                                else <m, j>
                                                              else <b, k> in
                                        g(0) 
                                       b 
                                       1 
                            in <j, c1>
             else if (x2 + 4) < (x1)
                     then eval b = canonical-bound((r1/a)) in
                          eval c = canonical-bound(real_exp(r(b))) in
                          eval M = N * c in
                            if ((M * (b - 0)) - 1) < (0)
                               then <1, -b>
                               else let c1,j = letrec g(a@0)=λb,k. if (k) < (M * (b - a@0))
                                                                      then eval m = a@0 + b in
                                                                           eval j = 2 * k in
                                                                           eval n4 = 4 * N in
                                                                           eval a1 = real_exp((r(m))/j) n4 in
                                                                           eval b1 = (r1/a) n4 in
                                                                             if (a1 + 4) < (b1)
                                                                                then eval bb = 2 * b in
                                                                                     let c,N = g m bb j 
                                                                                     in <c, N>
                                                                                else if (b1 + 4) < (a1)
                                                                                        then eval aa = 2 * a@0 in
                                                                                             let c,N = g aa m j 
                                                                                             in <c, N>
                                                                                        else <m, j>
                                                                      else <b, k> in
                                                g(0) 
                                               b 
                                               1 
                                    in <j, -c1>
                     else <1, 0> }

---

Latex:

---

Latex:
\mforall{}a:\{a:\mBbbR{}|  r0  <  a\}  .  \mforall{}N:\mBbbN{}\msupplus{}.    \mexists{}m:\mBbbN{}\msupplus{}.  (\mexists{}z:\mBbbZ{}  [(|(r(z))/m  -  rlog(a)|  \mleq{}  (r1/r(N)))])


By

---

Latex:
Extract  of  Obid:  near-log-exists
not  unfolding    rdiv  canonical-bound  recdefs  int-to-real  int-rdiv  rexp  real\_exp
finishing  with  (Reduce  0  THEN  RepUR  ``so\_lambda``  0  THEN  Try  (Trivial))
normalizes  to:

\mlambda{}a,N.  eval  x  =  4  *  (N  +  1)  in
            eval  x1  =  r1  x  in
            eval  x2  =  a  x  in
                if  (x1  +  4)  <  (x2)
                      then  eval  b  =  canonical-bound(a)  in
                                eval  c  =  canonical-bound(real\_exp(r(b)))  in
                                eval  M  =  N  *  c  in
                                    if  ((M  *  (b  -  0))  -  1)  <  (0)
                                          then  ə,  b>
                                          else  let  c1,j  =  letrec  g(a@0)=\mlambda{}b,k.  if  (k)  <  (M  *  (b  -  a@0))
                                                                                                                        then  eval  m  =  a@0  +  b  in
                                                                                                                                  eval  j  =  2  *  k  in
                                                                                                                                  eval  n4  =  4  *  N  in
                                                                                                                                  eval  a1  =  real\_exp((r(m))/j)  n4  in
                                                                                                                                  eval  b1  =  a  n4  in
                                                                                                                                      if  (a1  +  4)  <  (b1)
                                                                                                                                            then  eval  bb  =  2  *  b  in
                                                                                                                                                      let  c,N  =  g  m  bb  j 
                                                                                                                                                      in  <c,  N>
                                                                                                                                            else  if  (b1  +  4)  <  (a1)
                                                                                                                                                            then  eval  aa  =  2
                                                                                                                                                                      *  a@0  in
                                                                                                                                                                      let  c,N  =  g  aa  m 
                                                                                                                                                                                          j 
                                                                                                                                                                      in  <c,  N>
                                                                                                                                                            else  <m,  j>
                                                                                                                        else  <b,  k>  in
                                                                            g(0) 
                                                                          b 
                                                                          1 
                                                    in  <j,  c1>
                      else  if  (x2  +  4)  <  (x1)
                                      then  eval  b  =  canonical-bound((r1/a))  in
                                                eval  c  =  canonical-bound(real\_exp(r(b)))  in
                                                eval  M  =  N  *  c  in
                                                    if  ((M  *  (b  -  0))  -  1)  <  (0)
                                                          then  ə,  -b>
                                                          else  let  c1,j  =
                                                                      letrec  g(a@0)=\mlambda{}b,k.  if  (k)  <  (M  *  (b  -  a@0))
                                                                                                                    then  eval  m  =  a@0  +  b  in
                                                                                                                              eval  j  =  2  *  k  in
                                                                                                                              eval  n4  =  4  *  N  in
                                                                                                                              eval  a1  =  real\_exp((r(m))/j)  n4  in
                                                                                                                              eval  b1  =  (r1/a)  n4  in
                                                                                                                                  if  (a1  +  4)  <  (b1)
                                                                                                                                        then  eval  bb  =  2  *  b  in
                                                                                                                                                  let  c,N  =  g  m  bb  j 
                                                                                                                                                  in  <c,  N>
                                                                                                                                        else  if  (b1  +  4)  <  (a1)
                                                                                                                                                        then  eval  aa  =  2
                                                                                                                                                                  *  a@0  in
                                                                                                                                                                  let  c,N  =  g  aa  m  j 
                                                                                                                                                                  in  <c,  N>
                                                                                                                                                        else  <m,  j>
                                                                                                                    else  <b,  k>  in
                                                                        g(0) 
                                                                      b 
                                                                      1 
                                                                    in  <j,  -c1>
                                      else  ə,  0>

---

Home Index