Section Continuous_functions.

Continuous functions, uniformly continuous functions and Lipschitz functions

Let A and B be pseudo metric spaces.

Variable A : CPsMetricSpace.
Variable B : CPsMetricSpace.

We will look at some notions of continuous functions.

Definition continuous (f : CSetoid_fun A B) : CProp :=
  forall (x : A) (n : N) (H : 2[#]0),
  {m : N |
  forall y : A,
  x[-d]y[<](1[/] 2[//]H)[^]m -> f x[-d]f y[<](1[/] 2[//]H)[^]n}.

Definition continuous' (f : CSetoid_fun A B) : CProp :=
  forall (x : A) (n : N),
  {m : N |
  forall y : A, x[-d]y[<=]one_div_succ m -> f x[-d]f y[<=]one_div_succ n}.

Definition uni_continuous (f : CSetoid_fun A B) : CProp :=
  forall (n : N) (H : 2[#]0),
  {m : N |
  forall x y : A,
  x[-d]y[<](1[/] 2:IR[//]H)[^]m -> f x[-d]f y[<](1[/] 2:IR[//]H)[^]n}.

Definition uni_continuous' (f : CSetoid_fun A B) : CProp :=
  forall n : N,
  {m : N |
  forall x y : A, x[-d]y[<=]one_div_succ m -> f x[-d]f y[<=]one_div_succ n}.

Definition uni_continuous'' (f : CSetoid_fun A B) : CProp :=
  {mds : N -> N |
  forall (n : N) (x y : A),
  x[-d]y[<=]one_div_succ (mds n) -> f x[-d]f y[<=]one_div_succ n}.

Definition lipschitz (f : CSetoid_fun A B) : CProp :=
  {n : N | forall x y : A, f x[-d]f y[<=]2[^]n[*](x[-d]y)}.

Definition lipschitz' (f : CSetoid_fun A B) : CProp :=
  {n : N | forall x y : A, f x[-d]f y[<=]nring n[*](x[-d]y)}.

Definition lipschitz_c (f : CSetoid_fun A B) (C : IR) : CProp :=
    forall x1 x2 : A, f x1 [-d] f x2 [<=] C [*] (x1 [-d] x2).

End Continuous_functions.

Section Lemmas.


Lemma continuous_imp_continuous' :
 forall (A B : CPsMetricSpace) (f : CSetoid_fun A B),
 continuous f -> continuous' f.

Lemma continuous'_imp_continuous :
 forall (A B : CPsMetricSpace) (f : CSetoid_fun A B),
 continuous' f -> continuous f.

Lemma uni_continuous_imp_uni_continuous' :
 forall (A B : CPsMetricSpace) (f : CSetoid_fun A B),
 uni_continuous f -> uni_continuous' f.

Lemma uni_continuous'_imp_uni_continuous :
 forall (A B : CPsMetricSpace) (f : CSetoid_fun A B),
 uni_continuous' f -> uni_continuous f.

Lemma uni_continuous'_imp_uni_continuous'' :
 forall (A B : CPsMetricSpace) (f : CSetoid_fun A B),
 uni_continuous' f -> uni_continuous'' f.

Lemma lipschitz_imp_lipschitz' :
 forall (A B : CPsMetricSpace) (f : CSetoid_fun A B),
 lipschitz f -> lipschitz' f.

Lemma lipschitz'_imp_lipschitz :
 forall (A B : CPsMetricSpace) (f : CSetoid_fun A B),
 lipschitz' f -> lipschitz f.

Lemma lip_c_imp_lip : forall (A B : CPsMetricSpace) (f : CSetoid_fun A B) (C : IR),
lipschitz_c f C -> lipschitz' f.

Every uniformly continuous function is continuous and every Lipschitz function is uniformly continuous.

Lemma uni_continuous_imp_continuous :
 forall (C D : CPsMetricSpace) (f : CSetoid_fun C D),
 uni_continuous f -> continuous f.

Lemma lipschitz_imp_uni_continuous :
 forall (C D : CPsMetricSpace) (f : CSetoid_fun C D),
 lipschitz f -> uni_continuous f.

End Lemmas.

Section Identity.

Identity

The identity function is Lipschitz. Hence it is uniformly continuous and continuous.

Lemma id_is_lipschitz : forall X : CPsMetricSpace, lipschitz (id_un_op X).

Lemma id_is_uni_continuous :
 forall X : CPsMetricSpace, uni_continuous (id_un_op X).

Lemma id_is_continuous : forall X : CPsMetricSpace, continuous (id_un_op X).

End Identity.

Section Constant.

Constant functions

Let B and X be pseudo metric spaces.
Any constant function is Lipschitz. Hence it is uniformly continuous and continuous.
Variable B : CPsMetricSpace.
Variable X : CPsMetricSpace.

Lemma const_fun_is_lipschitz :
 forall b : B, lipschitz (Const_CSetoid_fun X B b).

Lemma const_fun_is_uni_continuous :
 forall b : B, uni_continuous (Const_CSetoid_fun X B b).

Lemma const_fun_is_continuous :
 forall b : B, continuous (Const_CSetoid_fun X B b).

End Constant.

Section Composition.

Composition

Let B,C and X be pseudo metric spaces. Let f : (CSetoid_fun X B) and g : (CSetoid_fun B C).
The composition of two Lipschitz/uniformly continous/continuous functions is again Lipschitz/uniformly continuous/continuous.
Variable X : CPsMetricSpace.
Variable B : CPsMetricSpace.
Variable f : CSetoid_fun X B.
Variable C : CPsMetricSpace.
Variable g : CSetoid_fun B C.

Lemma comp_resp_lipschitz :
 lipschitz f -> lipschitz g -> lipschitz (compose_CSetoid_fun X B C f g).

Lemma comp_resp_uni_continuous :
 uni_continuous f ->
 uni_continuous g -> uni_continuous (compose_CSetoid_fun X B C f g).

Lemma comp_resp_continuous :
 continuous f -> continuous g -> continuous (compose_CSetoid_fun X B C f g).

End Composition.

Section Limit.

Limit


Definition MSseqLimit (X : CPsMetricSpace) (seq : N -> X)
  (lim : X) : CProp :=
  forall (n : N) (H : 2[#]0),
  {N : N |
  forall m : N, N <= m -> seq m[-d]lim[<](1[/] 2:IR[//]H)[^]n}.


Definition MSseqLimit' (X : CPsMetricSpace) (seq : N -> X)
  (lim : X) : CProp :=
  forall n : N,
  {N : N | forall m : N, N <= m -> seq m[-d]lim[<=]one_div_succ n}.


Lemma MSseqLimit_imp_MSseqLimit' :
 forall (X : CPsMetricSpace) (seq : N -> X) (lim : X),
 MSseqLimit seq lim -> MSseqLimit' seq lim.

Lemma MSseqLimit'_imp_MSseqLimit :
 forall (X : CPsMetricSpace) (seq : N -> X) (lim : X),
 MSseqLimit' seq lim -> MSseqLimit seq lim.

Definition seqcontinuous' (A B : CPsMetricSpace) (f : CSetoid_fun A B) :
  CProp :=
  forall (seq : N -> A) (lim : A),
  MSseqLimit' seq lim -> MSseqLimit' (fun m : N => f (seq m)) (f lim).


Lemma continuous'_imp_seqcontinuous' :
 forall (A B : CPsMetricSpace) (f : CSetoid_fun A B),
 continuous' f -> seqcontinuous' f.

End Limit.