Quelle  vect3_Heine.pvs

%------------------------------------------------------------------------------------------------
%
%       A Special Result On Continuous Functions R x R^3 -> R
%
%       Author: Anthony Narkawicz, NASA Langley
%
%       
%       Version 1.0                     September 16, 2009
%
%------------------------------------------------------------------------------------------------


vect3_Heine: THEORY
BEGIN

   IMPORTING vect3_metric_space, 
             analysis@real_metric_space, 
             analysis@cross_metric_real_fun[real,real_dist,Vect3,dist], 
             analysis@continuity_ms[Vect3,dist,real,real_dist]

   f: VAR [[real,Vect3] -> real]

   curried_min_exists_3D: LEMMA FORALL (A: real, B: {x: real | A < x}):
    continuous?(f,fullset[[(closed_intv(A,B)),Vect3]])
     IMPLIES (FORALL (y: Vect3):  
        nonempty?[real]({r: real | EXISTS (t: (LAMBDA (x: real): A <= x AND x <= B)):r = f(t, y)})
    AND below_bounded[real]({r: real | EXISTS (t: (LAMBDA (x: real): A <= x AND x <= B)):r = f(t, y)})
    AND ext[real]({r: real | EXISTS (t: (LAMBDA (x: real): A <= x AND x <= B)): r = f(t, y)})
              (inf[real]({r: real | EXISTS (t: (LAMBDA (x: real): A <= x AND x <= B)): r = f(t, y)}))
    AND (EXISTS (tmin: (closed_intv(A,B))): FORALL (s: (closed_intv(A,B))): f(tmin,y) <= f(s,y)))

   curried_min_is_cont_3D: THEOREM FORALL (A: real, B: {x: real | A < x}): 
      continuous?(f,fullset[[(closed_intv(A,B)),Vect3]]) 
      IMPLIES
          LET unif_min_first(y: Vect3): real 
              = min({r: real | EXISTS (t: (closed_intv(A,B))): r = f(t,y)})
          IN continuous?(unif_min_first)

   curried_min_is_cont_3D_ed: THEOREM FORALL (A: real, B: {x: real | A < x}):
       (FORALL (x: (closed_intv(A,B)), y: Vect3, epsilon: posreal): 
          EXISTS (delta: posreal): 
             FORALL (z: (closed_intv(A,B)), w: Vect3): 
               (real_dist(x,z) <= delta AND dist(y,w) <= delta) IMPLIES real_dist(f(x,y),f(z,w))<epsilon)
       IMPLIES
           LET unif_min_first(y: Vect3): real 
               = min({r: real | EXISTS (t: (closed_intv(A,B))): r = f(t,y)})
           IN
              (FORALL (y: Vect3): FORALL (epsilon: posreal): 
                  EXISTS (delta: posreal): FORALL (q:Vect3):
                       dist(y,q) < delta IMPLIES real_dist(unif_min_first(y),unif_min_first(q)) < epsilon)


   % Uniform Continuity In The First Variable

   multiary_Heine_3D:   THEOREM FORALL (A: real, B: {x: real | A < x}):
      continuous?(f,fullset[[(closed_intv(A,B)),Vect3]]) 
      IMPLIES uniformly_continuous_in_first?(f,closed_intv(A,B),fullset[Vect3])


   multiary_Heine_3D_ed:   THEOREM FORALL (A: real, B: {x: real | A < x}):
     (FORALL (x: (closed_intv(A,B)), y: Vect3, epsilon: posreal): 
        EXISTS (delta: posreal): 
           FORALL (z: (closed_intv(A,B)), w: Vect3): (real_dist(x,z) <= delta AND dist(y,w) <= delta) 
                                                          IMPLIES real_dist(f(x,y),f(z,w))<epsilon)
     IMPLIES
        FORALL (y1: Vect3, epsilon: posreal): EXISTS (delta: posreal):
           FORALL (x1,x2: (closed_intv(A,B)), y2: Vect3): (real_dist(x1,x2) <= delta AND dist(y1,y2) <= delta) 
              IMPLIES real_dist(f(x1,y1),f(x2,y2))<epsilon

END vect3_Heine