ln_approx: THEORY
%-----------------------------------------------------------------------------
%      ln_approx by David Lester  Manchester Univ
%                   Cesar Munoz   NIA
%      ---------
%      Defines upper and lower bounds on ln:
%           - ln_lb(a,n) <= ln(a) <= ln_ub(a,n)
%-----------------------------------------------------------------------------

BEGIN

  IMPORTING ln_series,reals@log_nat

  n:    VAR nat
  x:    VAR real
  px:   VAR posreal
  pn:   VAR posnat
  xgt1: VAR {x:posreal | x > 1}

  ln_le2_lb(n,x): real = if x = 0 then 0 else ln_estimate(x,2*n)   endif
  ln_le2_ub(n,x): real = if x = 0 then 0 else ln_estimate(x,2*n+1) endif

  ln_le2_bounds: LEMMA 0 < x AND x <= 1 IMPLIES
       (ln_le2_lb(n,x) < ln(x+1) AND ln(x+1) < ln_le2_ub(n,x))

  ln2_lb(n): MACRO real = ln_le2_lb(n,1)
  ln2_ub(n): MACRO real = ln_le2_ub(n,1)

  ln_gt1_lb(n,xgt1): real = 
    let (m,y) = log_nat(xgt1,2) in
      m*ln2_lb(n)+ln_le2_lb(n,y-1) 

  ln_gt1_ub(n,xgt1): real = 
    let (m,y) = log_nat(xgt1,2) in
       m*ln2_ub(n)+ln_le2_ub(n,y-1) 

  ln_gt1_bounds: LEMMA 1 < x IMPLIES
       (ln_gt1_lb(n,x) < ln(x) AND ln(x) < ln_gt1_ub(n,x))

  ln_lb(px,n): real = IF    px < 1 THEN -ln_gt1_ub(n,1/px)
                      ELSIF px = 1 THEN 0
                                   ELSE ln_gt1_lb(n,px)    ENDIF

  ln_ub(px,n): real = IF    px < 1 THEN -ln_gt1_lb(n,1/px)
                      ELSIF px = 1 THEN 0
                                   ELSE ln_gt1_ub(n,px)    ENDIF

  ln_bounds: LEMMA ln_lb(px,n) <= ln(px) AND ln(px) <= ln_ub(px,n)

END ln_approx