Impressum cross_metric_cont.pvs

%---------------------------------------------------------------------------------------------------------
%
%       Continuity of functions on product (metric) spaces
%
%       Author: Anthony Narkawicz, NASA Langley
%
%       
%       Version 1.0                     August 19, 2009
%
%---------------------------------------------------------------------------------------------------------


cross_metric_cont[T1:Type+,d1:[T1,T1->nnreal],
                  T2:Type+,d2:[T2,T2->nnreal],T3:TYPE+,d3:[T3,T3->nnreal]]: THEORY

BEGIN

    ASSUMING IMPORTING metric_spaces

        fullset_metric_space1: ASSUMPTION metric_space?[T1,d1](fullset[T1])
        fullset_metric_space2: ASSUMPTION metric_space?[T2,d2](fullset[T2])
        fullset_metric_space3: ASSUMPTION metric_space?[T3,d3](fullset[T3])

    ENDASSUMING

  IMPORTING cross_metric_spaces[T1,d1,T2,d2], continuity_ms_def[[T1,T2],d[T1,d1,T2,d2],T3,d3],
       uniform_continuity[T1,d1,T3,d3]

  S: VAR set[[T1,T2]]
  X: VAR set[T1]
  Y: VAR set[T2]
  f: VAR [[T1,T2] -> T3]

  product_cont_equiv: LEMMA 
    continuous?(f,S) IFF 
       (FORALL (x: (S), epsilon: posreal):  EXISTS (delta: posreal): 
            FORALL (y: (S)): (d1(x`1,y`1) <= delta AND d2(x`2,y`2) <= delta) 
               IMPLIES d3(f(x),f(y))<epsilon)

  product_cont_product_subset: COROLLARY 
     continuous?(f,fullset[[(X),(Y)]]) IFF 
        (FORALL (x: (X), y: (Y), epsilon: posreal): EXISTS (delta: posreal): 
            FORALL (z: (X), w: (Y)): (d1(x,z) <= delta AND d2(y,w) <= delta) 
                IMPLIES d3(f(x,y),f(z,w))<epsilon)



  % -----------    Uniform Continuity In One Variable  ---------------

  
  uniformly_continuous_in_first?(f,X,Y): bool = 
     FORALL (y1: (Y), epsilon: posreal): EXISTS (delta: posreal):
        FORALL (x1,x2: (X), y2: (Y)): (d1(x1,x2) <= delta AND d2(y1,y2) <= delta) 
            IMPLIES d3(f(x1,y1),f(x2,y2))<epsilon

  uniformly_continuous_in_second?(f,X,Y): bool = 
     FORALL (x1: (X), epsilon: posreal): EXISTS (delta: posreal):
        FORALL (x2: (X), y1,y2: (Y)): (d1(x1,x2) <= delta AND d2(y1,y2) <= delta) 
            IMPLIES d3(f(x1,y1),f(x2,y2))<epsilon


  % ---------     An Equivalent, Sequence Definition Of Uniform Continuity In One Variable ----

  one_variable_unif_cont_sequence: LEMMA NOT uniformly_continuous_in_first?(f,X,Y) IFF
    EXISTS (epsilon: posreal): EXISTS (y: (Y)): EXISTS (seq: [posint -> [T1,T1,T2]]):
  FORALL (n: posint): 
         (X(seq(n)`1) AND X(seq(n)`2) AND Y(seq(n)`3) 
         AND d1(seq(n)`1,seq(n)`2) < 1/n AND d2(y,seq(n)`3) < 1/n
         AND d3(f(seq(n)`1,y),f(seq(n)`2,seq(n)`3)) > epsilon)

  %---------     This implies that the associated curried function is uniformly continuous ----

  curried_is_uniform: LEMMA uniformly_continuous_in_first?(f,X,Y) IMPLIES (FORALL (y: (Y)):
               uniformly_continuous?((LAMBDA (t: T1): f(t,y)),X))
           


  

END cross_metric_cont