%------------------------------------------------------------------------------
% nth roots of nnreals
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            19/08/08   Initial version (DRL)
%
% (Note that we have the essentials of continuity proved, without
%  using of defining these concepts. This means that the definition can
%  be used stand-alone.)
%------------------------------------------------------------------------------

nn_root: THEORY

BEGIN

  IMPORTING exponentiation_aux

  x,x1,x2,y: VAR nnreal
  epsilon, px,py,
    delta: VAR posreal
  pm,pn:   VAR posnat
  lt1x:    VAR {r:posreal | r < 1}
  gt1x:    VAR {r:posreal | r > 1}

  continuous_alt_hat: LEMMA EXISTS delta: FORALL x2: abs(x1-x2) < delta
                 => abs(x1^pn-x2^pn) < epsilon

  hat_bijective: LEMMA bijective?[nnreal,nnreal](lambda x: x^pn)

  nn_root(x,pn):nnreal = inverse[nnreal,nnreal](lambda x: x^pn)(x)

  nn_root_0n: LEMMA nn_root(0,pn) = 0
  nn_root_1n: LEMMA nn_root(1,pn) = 1
  nn_root_x1: LEMMA nn_root(x,1)  = x

  nn_root_strict_increasing: LEMMA x < y => nn_root(x,pn) < nn_root(y,pn)

  nn_root_expt: LEMMA nn_root(x^pn,pn) = x
  expt_nn_root: LEMMA nn_root(x,pn)^pn = x

  nn_root_is_0: LEMMA nn_root(x,pn) = 0 IFF x = 0
  nn_root_pos:  LEMMA nn_root(px,pn) > 0
  nn_root_gt1:  LEMMA nn_root(x,pn) > 1 IFF x > 1
  nn_root_lt1:  LEMMA nn_root(x,pn) < 1 IFF x < 1

  mult_nn_root: LEMMA nn_root(x*y,pn)  = nn_root(x,pn)*nn_root(y,pn)
  inv_nn_root:  LEMMA nn_root(1/px,pn) = 1/nn_root(px,pn)
  div_nn_root:  LEMMA nn_root(x/py,pn) = nn_root(x,pn)/nn_root(py,pn)

  nn_root_mult: LEMMA nn_root(x,pn*pm)  = nn_root(nn_root(x,pn),pm)

  nn_root_increasing: LEMMA pn < pm AND 0 < x AND x < 1 =>
                             nn_root(x,pn) < nn_root(x,pm)

  nn_root_decreasing: LEMMA pn < pm AND 1 < x =>
                             nn_root(x,pn) > nn_root(x,pm)

  nn_root_upper_bound: LEMMA nn_root(1+px,pn) <= 1+px/pn

  nn_root_bijective: LEMMA bijective?[nnreal,nnreal](lambda x: nn_root(x,pn))

  continuous_alt_nn_root: LEMMA EXISTS delta: FORALL x2: abs(x1-x2) < delta
                 => abs(nn_root(x1,pn)-nn_root(x2,pn)) < epsilon

  both_sides_nn_root_lt: LEMMA nn_root(x,pn) <  nn_root(y,pn) IFF x <  y
  both_sides_nn_root_le: LEMMA nn_root(x,pn) <= nn_root(y,pn) IFF x <= y
  both_sides_nn_root_gt: LEMMA nn_root(x,pn) >  nn_root(y,pn) IFF x >  y
  both_sides_nn_root_ge: LEMMA nn_root(x,pn) >= nn_root(y,pn) IFF x >= y
  both_sides_nn_root:    LEMMA nn_root(x,pn) =  nn_root(y,pn) IFF x =  y

  both_sides_nn_root_lt1_lt: LEMMA
    nn_root(lt1x,pn) <  nn_root(lt1x,pm) IFF pn <  pm
  both_sides_nn_root_lt1_le: LEMMA
    nn_root(lt1x,pn) <= nn_root(lt1x,pm) IFF pn <= pm
  both_sides_nn_root_lt1_gt: LEMMA
    nn_root(lt1x,pn) >  nn_root(lt1x,pm) IFF pn >  pm
  both_sides_nn_root_lt1_ge: LEMMA
    nn_root(lt1x,pn) >= nn_root(lt1x,pm) IFF pn >= pm

  both_sides_nn_root_gt1_lt: LEMMA
    nn_root(gt1x,pn) <  nn_root(gt1x,pm) IFF pm <  pn
  both_sides_nn_root_gt1_le: LEMMA
    nn_root(gt1x,pn) <= nn_root(gt1x,pm) IFF pm <= pn
  both_sides_nn_root_gt1_gt: LEMMA
    nn_root(gt1x,pn) >  nn_root(gt1x,pm) IFF pm >  pn
  both_sides_nn_root_gt1_ge: LEMMA
    nn_root(gt1x,pn) >= nn_root(gt1x,pm) IFF pm >= pn

  both_sides_nn_root_eq: LEMMA nn_root(x,pn) = nn_root(x,pm) IFF
                               x = 0 OR x = 1 OR pn = pm

END nn_root