cont_vect3_real: THEORY
%------------------------------------------------------------------------------
%  Continuous functions [ Vect3 -> real]   
%
%  Author: Rick Butler     NASA Langley Research Center  2/1/2009
%
%------------------------------------------------------------------------------
BEGIN

  IMPORTING limit_vect3_real

  f, f1, f2      : VAR [Vect3 -> real]
  g              : VAR [Vect3 -> nzreal]
  u              : VAR real
  x, x0          : VAR Vect3
  epsilon, delta : VAR posreal
  n              : VAR nat
 
  %--------------------
  %  Continuity at x0    
  %--------------------

  continuous_vr?(f, x0) : bool = 
      FORALL epsilon : EXISTS delta : FORALL x :
         norm(x - x0) < delta IMPLIES abs(f(x) - f(x0)) < epsilon

  continuity_def : LEMMA
        continuous_vr?(f, x0) IFF convergence(f, x0, f(x0))

  continuity_def2 : LEMMA
        continuous_vr?(f, x0) IFF convergent?(f, x0)


  %------------------------------------------
  %  Operations preserving continuity at x0 
  %------------------------------------------

  sum_continuous_vr  : LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)
                           IMPLIES continuous_vr?(f1 + f2, x0)

  diff_continuous_vr : LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)
                           IMPLIES continuous_vr?(f1 - f2, x0)

  prod_continuous_vr : LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)
                           IMPLIES continuous_vr?(f1 * f2, x0)

  const_continuous_vr: LEMMA continuous_vr?(const_fun(u), x0)

  scal_continuous_vr : LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(u * f, x0)
                
  neg_continuous_vr  : LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(- f, x0)

  div_continuous_vr  : LEMMA continuous_vr?(f, x0) AND continuous_vr?(g, x0) 
                            IMPLIES continuous_vr?(f/g, x0)

  inv_continuous_vr  : LEMMA continuous_vr?(g, x0) IMPLIES continuous_vr?(1/g, x0)
  
  expt_continuous_vr : LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(f^n, x0)


  %---------------------------------
  %  Continuity of f in its domain
  %---------------------------------

  continuous_vr?(f): bool = FORALL x0: continuous_vr?(f, x0)

% ------------ Alternate forms and names for convenience ---------------

  sum_cont_vr_fun  : LEMMA continuous_vr?(f1) AND continuous_vr?(f2)
                           IMPLIES continuous_vr?(f1 + f2)

  diff_cont_vr_fun : LEMMA continuous_vr?(f1) AND continuous_vr?(f2)
                           IMPLIES continuous_vr?(f1 - f2)

  prod_cont_vr_fun : LEMMA continuous_vr?(f1) AND continuous_vr?(f2)
                           IMPLIES continuous_vr?(f1 * f2)

  const_cont_vr_fun: LEMMA continuous_vr?(const_fun(u))

  scal_cont_vr_fun : LEMMA continuous_vr?(f) IMPLIES continuous_vr?(u * f)
                
  neg_cont_vr_fun  : LEMMA continuous_vr?(f) IMPLIES continuous_vr?(-f)

  div_cont_vr_fun  : LEMMA continuous_vr?(f) AND continuous_vr?(g) 
                            IMPLIES continuous_vr?(f/g)

  inv_cont_vr_fun  : LEMMA continuous_vr?(g) IMPLIES continuous_vr?(1/g)
  
  expt_cont_vr_fun : LEMMA continuous_vr?(f) IMPLIES continuous_vr?(f^n)



  %--- Properties ---%

  continuous_vr_fun: TYPE+ = { f | continuous_vr?(f) }

  nz_continuous_vr_fun: TYPE = { g | continuous_vr?(g) }

  h, h1, h2: VAR continuous_vr_fun
  h3: VAR nz_continuous_vr_fun

  sum_fun_continuous_vr : JUDGEMENT  +(h1, h2) HAS_TYPE continuous_vr_fun

  diff_fun_continuous_vr: JUDGEMENT  -(h1, h2) HAS_TYPE continuous_vr_fun

  prod_fun_continuous_vr: JUDGEMENT  *(h1, h2) HAS_TYPE continuous_vr_fun

  const_fun_continuous_vr: JUDGEMENT const_fun(u) HAS_TYPE continuous_vr_fun

  scal_fun_continuous_vr: JUDGEMENT  *(u, h) HAS_TYPE continuous_vr_fun

  neg_fun_continuous_vr : JUDGEMENT -(h) HAS_TYPE continuous_vr_fun

  div_fun_continuous_vr : JUDGEMENT /(h, h3) HAS_TYPE continuous_vr_fun

  inv_fun_continuous_vr : LEMMA continuous_vr?(1/h3)

  expt_fun_continuous_vr: LEMMA continuous_vr?(f) IMPLIES continuous_vr?(f^n)



END cont_vect3_real