CoRN.metrics.ContFunctions

Require Export CPseudoMSpaces.

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 :=
  ∀ (x : A) (n : nat) (H : Two [#][0]),
  {m : nat |
  ∀ y : A,
  x [-d ]y [<]([1][/] Two [//]H )[^]m → f x [-d ]f y [<]([1][/] Two [//]H )[^]n }.

Definition continuous' (f : CSetoid_fun A B) : CProp :=
  ∀ (x : A) (n : nat),
  {m : nat |
  ∀ 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 :=
  ∀ (n : nat) (H : Two [#][0]),
  {m : nat |
  ∀ x y : A,
  x [-d ]y [<]([1][/] Two:IR [//]H )[^]m → f x [-d ]f y [<]([1][/] Two:IR [//]H )[^]n }.

Definition uni_continuous' (f : CSetoid_fun A B) : CProp :=
  ∀ n : nat,
  {m : nat |
  ∀ 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 : nat → nat |
  ∀ (n : nat) (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 : nat | ∀ x y : A, f x [-d ]f y [<=]Two [^]n[*](x [-d ]y )}.

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

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

End Continuous_functions.
Implicit Arguments continuous [A B].
Implicit Arguments uni_continuous [A B].
Implicit Arguments lipschitz [A B].
Implicit Arguments continuous' [A B].
Implicit Arguments uni_continuous' [A B].
Implicit Arguments uni_continuous'' [A B].
Implicit Arguments lipschitz' [A B].
Implicit Arguments lipschitz_c [A B].

Section Lemmas.

Lemma continuous_imp_continuous' :
∀ (A B : CPsMetricSpace) (f : CSetoid_fun A B),
continuous f → continuous' f.
Proof.
intros A B f.
unfold continuous in |- ×.
intro H.
unfold continuous' in |- ×.
intros x n.
set (H1 := two_ap_zero IR) in ×.
elim H with x (S n) H1.
intros p H2.
∃ (power p 2).
intro y.
intro H3.
apply leEq_transitive with ((OneR [/] Two:IR [//]H1)[^]S n).
  apply less_leEq.
  apply H2.
  apply leEq_less_trans with (one_div_succ (R:=IR) (power p 2)).
   exact H3.
  unfold one_div_succ in |- ×.
  astepr (OneR [^]p[/] (Two:IR )[^]p[//]nexp_resp_ap_zero p H1).
  astepr (OneR [/] (Two:IR )[^]p[//]nexp_resp_ap_zero p H1).
  apply recip_resp_less.
   apply nexp_resp_pos.
   apply pos_two.
  unfold Snring in |- ×.
  apply less_wdr with (nexp IR p Two [+][1]).
   apply shift_less_plus.
   apply minusOne_less.
  astepl (OneR [+]nexp IR p Two).
  astepr (OneR [+]nring (power p 2)).
   apply plus_resp_eq.
   apply nexp_power.
  simpl in |- ×.
  algebra.
apply less_leEq.
astepl (OneR [^]S n[/] (Two:IR )[^]S n[//]nexp_resp_ap_zero (S n) H1).
astepl (OneR [/] (Two:IR )[^]S n[//]nexp_resp_ap_zero (S n) H1).
unfold one_div_succ in |- ×.
unfold Snring in |- ×.
apply bin_less_un.
Qed.

Lemma continuous'_imp_continuous :
∀ (A B : CPsMetricSpace) (f : CSetoid_fun A B),
continuous' f → continuous f.
Proof.
intros A B f.
unfold continuous' in |- ×.
intro H.
unfold continuous in |- ×.
intros x n H0.
elim H with x (power n 2).
intros p H1.
∃ (S p).
intros y H2.
apply leEq_less_trans with (one_div_succ (R:=IR) (power n 2)).
  apply H1.
  apply less_leEq.
  apply less_transitive_unfolded with (([1][/] Two:IR [//]H0)[^]S p).
   exact H2.
  unfold one_div_succ in |- ×.
  astepl (OneR [^]S p[/] (Two:IR )[^]S p[//]nexp_resp_ap_zero (S p) H0).
  astepl (OneR [/] (Two:IR )[^]S p[//]nexp_resp_ap_zero (S p) H0).
  apply recip_resp_less.
   unfold Snring in |- ×.
   apply nring_pos.
   intuition.
  apply nat_less_bin_nexp.
unfold one_div_succ in |- ×.
unfold Snring in |- ×.
astepr (OneR [^]n[/] (Two:IR )[^]n[//]nexp_resp_ap_zero n H0).
astepr (OneR [/] (Two:IR )[^]n[//]nexp_resp_ap_zero n H0).
apply recip_resp_less.
  apply nexp_resp_pos.
  apply pos_two.
astepr (nring (R:=IR) (power n 2)[+][1]).
astepl (nexp IR n Two [+][0]).
apply plus_resp_leEq_less.
  apply eq_imp_leEq.
  apply nexp_power.
apply pos_one.
Qed.

Lemma uni_continuous_imp_uni_continuous' :
∀ (A B : CPsMetricSpace) (f : CSetoid_fun A B),
uni_continuous f → uni_continuous' f.
Proof.
intros A B f.
unfold uni_continuous in |- ×.
intro H.
unfold uni_continuous' in |- ×.
intro n.
set (H0 := two_ap_zero IR) in ×.
elim H with (S n) H0.
intros p H1.
∃ (power p 2).
intros x y H2.
apply less_leEq.
apply less_transitive_unfolded with ((OneR [/] Two:IR [//]H0)[^]S n).
  apply H1.
  apply leEq_less_trans with (one_div_succ (R:=IR) (power p 2)).
   exact H2.
  unfold one_div_succ in |- ×.
  unfold Snring in |- ×.
  astepr (OneR [^]p[/] (Two:IR )[^]p[//]nexp_resp_ap_zero p H0).
  astepr (OneR [/] (Two:IR )[^]p[//]nexp_resp_ap_zero p H0).
  apply recip_resp_less.
   apply nexp_resp_pos.
   apply pos_two.
  astepr (nring (R:=IR) (power p 2)[+][1]).
  astepl (nexp IR p Two [+][0]).
  apply plus_resp_leEq_less.
   apply eq_imp_leEq.
   apply nexp_power.
  apply pos_one.
unfold one_div_succ in |- ×.
unfold Snring in |- ×.
astepl (OneR [^]S n[/] (Two:IR )[^]S n[//]nexp_resp_ap_zero (S n) H0).
astepl (OneR [/] (Two:IR )[^]S n[//]nexp_resp_ap_zero (S n) H0).
apply bin_less_un.
Qed.

Lemma uni_continuous'_imp_uni_continuous :
∀ (A B : CPsMetricSpace) (f : CSetoid_fun A B),
uni_continuous' f → uni_continuous f.
Proof.
intros A B f.
unfold uni_continuous' in |- ×.
intro H.
unfold uni_continuous in |- ×.
intros n H0.
elim H with (power n 2).
intros p H1.
∃ (S p).
intros x y H2.
apply leEq_less_trans with (one_div_succ (R:=IR) (power n 2)).
  apply H1.
  apply less_leEq.
  apply less_transitive_unfolded with ((OneR [/] Two:IR [//]H0)[^]S p).
   exact H2.
  unfold one_div_succ in |- ×.
  unfold Snring in |- ×.
  astepl (OneR [^]S p[/] (Two:IR )[^]S p[//]nexp_resp_ap_zero (S p) H0).
  astepl (OneR [/] (Two:IR )[^]S p[//]nexp_resp_ap_zero (S p) H0).
  apply bin_less_un.
unfold one_div_succ in |- ×.
astepr (OneR [^]n[/] (Two:IR )[^]n[//]nexp_resp_ap_zero n H0).
astepr (OneR [/] (Two:IR )[^]n[//]nexp_resp_ap_zero n H0).
apply recip_resp_less.
  apply nexp_resp_pos.
  apply pos_two.
unfold Snring in |- ×.
astepr (nring (R:=IR) (power n 2)[+][1]).
astepl (nexp IR n Two [+][0]).
apply plus_resp_leEq_less.
  apply eq_imp_leEq.
  apply nexp_power.
apply pos_one.
Qed.

Lemma uni_continuous'_imp_uni_continuous'' :
∀ (A B : CPsMetricSpace) (f : CSetoid_fun A B),
uni_continuous' f → uni_continuous'' f.
Proof.
intros A B f.
unfold uni_continuous' in |- ×.
unfold uni_continuous'' in |- ×.
apply choice with (P := fun n m : nat ⇒ ∀ x y : A,
   x [-d ]y [<=]one_div_succ m → f x [-d ]f y [<=]one_div_succ n).
Qed.

Lemma lipschitz_imp_lipschitz' :
∀ (A B : CPsMetricSpace) (f : CSetoid_fun A B),
lipschitz f → lipschitz' f.
Proof.
intros A B f.
unfold lipschitz in |- ×.
intro H.
unfold lipschitz' in |- ×.
elim H.
intros n H0.
elim Archimedes with ((Two:IR )[^]n).
intros m H1.
∃ m.
intros x y.
apply leEq_transitive with ((Two:IR )[^]n[*](x[-d ]y)).
  apply H0.
apply mult_resp_leEq_rht.
  exact H1.
apply ax_d_nneg.
apply CPsMetricSpace_is_CPsMetricSpace.
Qed.

Lemma lipschitz'_imp_lipschitz :
∀ (A B : CPsMetricSpace) (f : CSetoid_fun A B),
lipschitz' f → lipschitz f.
Proof.
intros A B f.
unfold lipschitz' in |- ×.
intro H.
unfold lipschitz in |- ×.
elim H.
intros m H1.
∃ m.
intros x y.
apply leEq_transitive with (nring m[*](x[-d ]y)).
  apply H1.
apply mult_resp_leEq_rht.
  case m.
   simpl in |- ×.
   apply less_leEq.
   apply pos_one.
  intro n.
  astepl (Snring IR n).
  apply less_leEq.
  apply nat_less_bin_nexp.
apply ax_d_nneg.
apply CPsMetricSpace_is_CPsMetricSpace.
Qed.

Lemma lip_c_imp_lip : ∀ (A B : CPsMetricSpace) (f : CSetoid_fun A B) (C : IR),
lipschitz_c f C → lipschitz' f.
Proof.
unfold lipschitz_c.
unfold lipschitz'.
intros.
assert ({n : nat | C [<=] nring n}).
  apply Archimedes.
destruct X as [n H1].
∃ n.
intros.
assert (f x[-d ]f y [<=] C[*](x[-d ]y)).
  apply H.
apply leEq_transitive with (C[*](x[-d ]y)); auto.
apply mult_resp_leEq_rht; auto.
apply ax_d_nneg.
apply CPsMetricSpace_is_CPsMetricSpace.
Qed.

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

Lemma uni_continuous_imp_continuous :
∀ (C D : CPsMetricSpace) (f : CSetoid_fun C D),
uni_continuous f → continuous f.
Proof.
intros C D F.
red in |- ×.
unfold uni_continuous in |- ×.
intros H0 n u H3.
elim H0 with u H3.
intros.
∃ x.
intro y.
apply p.

Qed.

Lemma lipschitz_imp_uni_continuous :
∀ (C D : CPsMetricSpace) (f : CSetoid_fun C D),
lipschitz f → uni_continuous f.
Proof.
red in |- ×.
unfold lipschitz in |- ×.
intros C D f H n H0.
elim H.
intros.
∃ (n + x).
intros x0 y H1.
apply leEq_less_trans with (Two [^]x[*](x0[-d ]y)).
  apply p.
apply mult_cancel_less with (([1][/] Two:IR [//]H0)[^]x).
  apply nexp_resp_pos.
  apply div_resp_pos.
   apply pos_two.
  apply pos_one.
apply less_wdr with (([1][/] Two:IR [//]H0)[^](n + x)).
  apply less_wdl with (x0[-d ]y).
   exact H1.
  astepr (Two [^]x[*](x0[-d ]y)[*]([1][^]x[/] Two [^]x[//]nexp_resp_ap_zero x H0)).
  astepr (Two [^]x[*](x0[-d ]y)[*]([1][/] Two [^]x[//]nexp_resp_ap_zero x H0)).
  rational.
apply eq_symmetric_unfolded.
astepr (([1][/] Two:IR [//]H0)[^](n + x)).
apply nexp_plus.

Qed.

End Lemmas.

Section Identity.

Identity

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

Lemma id_is_lipschitz : ∀ X : CPsMetricSpace, lipschitz (id_un_op X).
Proof.
intro X.
red in |- ×.
simpl in |- ×.
∃ 0.
intros x y.
astepr (OneR [*](x[-d ]y)).
astepr (x[-d ]y).
apply leEq_reflexive.
Qed.

Lemma id_is_uni_continuous :
∀ X : CPsMetricSpace, uni_continuous (id_un_op X).
Proof.
intro X.
apply lipschitz_imp_uni_continuous.
apply id_is_lipschitz.
Qed.

Lemma id_is_continuous : ∀ X : CPsMetricSpace, continuous (id_un_op X).
Proof.
intro X.
apply uni_continuous_imp_continuous.
apply id_is_uni_continuous.
Qed.

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 :
∀ b : B, lipschitz (Const_CSetoid_fun X B b).
Proof.
intro b.
red in |- ×.
∃ 1.
intros.
astepr (Two [^]1[*](x[-d ]y)).
astepr (Two [*](x[-d ]y)).
unfold Const_CSetoid_fun in |- ×.
rewrite → leEq_def in |- ×.
red in |- ×.
simpl in |- ×.
intros H.
apply (ap_irreflexive_unfolded B b).
apply (ax_d_pos_imp_ap B (cms_d (c:=B)) (CPsMetricSpace_is_CPsMetricSpace B)).
apply leEq_less_trans with (([0][+][1][+][1])[*](x[-d ]y)).
  astepr ((Two:IR )[*](x[-d ]y)).
  apply shift_leEq_mult' with (two_ap_zero IR).
   apply pos_two.
  astepl ZeroR.
  apply ax_d_nneg.
  apply CPsMetricSpace_is_CPsMetricSpace.
exact H.
Qed.

Lemma const_fun_is_uni_continuous :
∀ b : B, uni_continuous (Const_CSetoid_fun X B b).
Proof.
intro b.
apply lipschitz_imp_uni_continuous.
apply const_fun_is_lipschitz.
Qed.

Lemma const_fun_is_continuous :
∀ b : B, continuous (Const_CSetoid_fun X B b).
Proof.
intro b.
apply uni_continuous_imp_continuous.
apply const_fun_is_uni_continuous.
Qed.

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).
Proof.
unfold lipschitz in |- ×.
intros H H0.
elim H.
intros x H1.
elim H0.
intros x0 H2.
∃ (x + x0).
simpl in |- ×.
intros x1 y.
apply leEq_transitive with ((Two:IR )[^]x0[*](f x1[-d ]f y)).
apply H2.
astepr (Two [^](x + x0)[*](x1[-d ]y)).
astepr (Two [^]x[*]Two [^]x0[*](x1[-d ]y)).
astepr (Two [^]x0[*]Two [^]x[*](x1[-d ]y)).
rstepr (Two [^]x0[*](Two [^]x[*](x1[-d ]y))).
apply mult_resp_leEq_lft.
apply H1.
apply nexp_resp_nonneg.
apply less_leEq.
apply pos_two.

Qed.

Lemma comp_resp_uni_continuous :
uni_continuous f →
uni_continuous g → uni_continuous (compose_CSetoid_fun X B C f g).
Proof.
unfold uni_continuous in |- ×.
intros H H0.
simpl in |- ×.
intros n H1.
elim H0 with n H1.
intro x.
intro H3.
elim H with x H1.
intro x0.
intro H4.
∃ x0.
intros x1 y H5.
apply H3.
apply H4.
exact H5.
Qed.

Lemma comp_resp_continuous :
continuous f → continuous g → continuous (compose_CSetoid_fun X B C f g).
Proof.
unfold continuous in |- ×.
intros H H0 x n H1.
simpl in |- ×.
elim H0 with (f x) n H1.
intros.
elim H with x x0 H1.
intros.
∃ x1.
intros y H2.
apply p.
apply p0.
exact H2.

Qed.

End Composition.

Section Limit.

Limit

Definition MSseqLimit (X : CPsMetricSpace) (seq : nat → X)
  (lim : X) : CProp :=
  ∀ (n : nat) (H : Two [#][0]),
  {N : nat |
  ∀ m : nat, N ≤ m → seq m [-d ]lim [<]([1][/] Two:IR [//]H )[^]n }.

Implicit Arguments MSseqLimit [X].

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

Implicit Arguments MSseqLimit' [X].

Lemma MSseqLimit_imp_MSseqLimit' :
∀ (X : CPsMetricSpace) (seq : nat → X) (lim : X),
MSseqLimit seq lim → MSseqLimit' seq lim.
Proof.
intros X seq lim.
unfold MSseqLimit in |- ×.
intro H.
unfold MSseqLimit' in |- ×.
intro n.
set (H2 := two_ap_zero IR) in ×.
elim H with (S n) H2.
intros p H3.
∃ p.
intros m H4.
apply less_leEq.
apply less_transitive_unfolded with ((OneR [/] Two:IR [//]H2)[^]S n).
  apply H3.
  exact H4.
unfold one_div_succ in |- ×.
unfold Snring in |- ×.
astepl (OneR [^]S n[/] (Two:IR )[^]S n[//]nexp_resp_ap_zero (S n) H2).
astepl (OneR [/] (Two:IR )[^]S n[//]nexp_resp_ap_zero (S n) H2).
apply bin_less_un.
Qed.

Lemma MSseqLimit'_imp_MSseqLimit :
∀ (X : CPsMetricSpace) (seq : nat → X) (lim : X),
MSseqLimit' seq lim → MSseqLimit seq lim.
Proof.
intros X seq lim.
unfold MSseqLimit' in |- ×.
intro H.
unfold MSseqLimit in |- ×.
intros n H0.
elim H with (power n 2).
intros p H1.
∃ p.
intros m H2.
apply leEq_less_trans with (one_div_succ (R:=IR) (power n 2)).
  apply H1.
  exact H2.
unfold one_div_succ in |- ×.
astepr (OneR [^]n[/] (Two:IR )[^]n[//]nexp_resp_ap_zero n H0).
astepr (OneR [/] (Two:IR )[^]n[//]nexp_resp_ap_zero n H0).
apply recip_resp_less.
  apply nexp_resp_pos.
  apply pos_two.
unfold Snring in |- ×.
simpl in |- ×.
apply less_wdr with (nexp IR n Two [+][1]).
  apply shift_less_plus.
  astepl (nexp IR n Two [-][1]).
  apply minusOne_less.
astepl (OneR [+]nexp IR n Two).
astepr (OneR [+]nring (power n 2)).
apply plus_resp_eq.
apply nexp_power.
Qed.

Definition seqcontinuous' (A B : CPsMetricSpace) (f : CSetoid_fun A B) :
  CProp :=
  ∀ (seq : nat → A) (lim : A),
  MSseqLimit' seq lim → MSseqLimit' (fun m : nat ⇒ f (seq m)) (f lim).

Implicit Arguments seqcontinuous' [A B].

Lemma continuous'_imp_seqcontinuous' :
∀ (A B : CPsMetricSpace) (f : CSetoid_fun A B),
continuous' f → seqcontinuous' f.
Proof.
intros A B f.
unfold continuous' in |- ×.
intro H.
unfold seqcontinuous' in |- ×.
intros seq lim.
unfold MSseqLimit' in |- ×.
intro H0.
intro n.
elim H with lim n.
intros p H1.
elim H0 with p.
intros q H2.
∃ q.
intro m.
intro H3.
astepl (f lim[-d ]f (seq m)).
  apply H1.
  astepl (seq m[-d ]lim).
   apply H2.
   exact H3.
  apply ax_d_com.
  apply CPsMetricSpace_is_CPsMetricSpace.
apply ax_d_com.
apply CPsMetricSpace_is_CPsMetricSpace.
Qed.

End Limit.