Library Coqtail.Reals.Ranalysis.Ranalysis_continuity

Require Import Rbase Ranalysis.
Require Import Rinterval Rfunctions Rfunction_def.
Require Import Ranalysis_def Ranalysis_def_simpl Rfunction_facts.
Require Import MyRIneq MyR_dist Fourier.

Require Import Ass_handling.

Local Open Scope R_scope.

Extensionality of continuity_pt_in


Lemma continuity_pt_in_ext : D (f g : RR) x,
  (f == g)%Fcontinuity_pt_in D f xcontinuity_pt_in D g x.
Proof.
intros D f g x Heq Hf Dx ; eapply limit1_in_ext.
 intros ; apply Heq.
 rewrite <- (Heq x) ; apply Hf ; assumption.
Qed.

Lemma continuity_pt_in_ext_strong : (D : RProp) (f g : RR) x,
  ( x, D xf x = g x)%F
  continuity_pt_in D f xcontinuity_pt_in D g x.
Proof.
intros D f g x Heq Hf Dx ; eapply limit1_in_ext.
 eexact Heq.
 rewrite <- (Heq x) ; [apply Hf |] ; assumption.
Qed.

Lemma continuity_in_ext : D (f g : RR),
  (f == g)%Fcontinuity_in D fcontinuity_in D g.
Proof.
intros D f g Heq Hf x ; eapply continuity_pt_in_ext, Hf ; eassumption.
Qed.

Lemma continuity_in_ext_strong : (D : RProp) f g,
  ( x, D xf x = g x)%F
  continuity_in D fcontinuity_in D g.
Proof.
intros D f g Heq Hf x ; eapply continuity_pt_in_ext_strong, Hf ; eassumption.
Qed.

How to relate the different notions of continuity.


Lemma continuity_pt_continuity_pt_in: f (D : RProp) x,
  continuity_pt f xcontinuity_pt_in D f x.
Proof.
intros f D x Hf Dx eps eps_pos ;
 destruct (Hf _ eps_pos) as [alp [alp_pos Halp]] ;
  alp ; split ; [assumption | intros y [Dy y_bd]].
 destruct (Req_dec x y) as [Heq | Hneq].
 subst ; rewrite R_dist_eq ; assumption.
 apply Halp ; repeat split ; assumption.
Qed.

Lemma continuity_continuity_in: D f,
  continuity fcontinuity_in D f.
Proof.
intros D f f_cont x x_in ; apply continuity_pt_continuity_pt_in ;
 [apply f_cont |] ; assumption.
Qed.

Lemma continuity_interval_continuity_pt: f lb ub x, lb < ub
  continuity_interval lb ub fopen_interval lb ub x
  continuity_pt f x.
Proof.
intros f lb ub x lb_lt_ub Hf x_in eps eps_pos ;
 assert (x_in' := open_interval_interval _ _ _ x_in) ;
 destruct (Hf _ x_in' _ eps_pos) as [alpha [alpha_pos Halpha]].
  (Rmin alpha (interval_dist lb ub x)) ; split.
  apply Rmin_pos_lt, open_interval_dist_pos ; assumption.
  intros y [[_ x_neq_y] y_bd] ; apply Halpha ; split.
   replace y with (x + (y -x)) by ring ; apply interval_dist_bound.
    assumption.
    left ; eapply Rlt_le_trans ; [eassumption | apply Rmin_r].
    eapply Rlt_le_trans ; [eassumption | apply Rmin_l].
Qed.

Lemma continuity_open_interval_continuity : f,
  ( lb ub, continuity_open_interval lb ub f) →
  continuity f.
Proof.
intros f Hf x eps eps_pos ;
 destruct (Hf _ _ _ (center_in_open_interval x 1 Rlt_0_1) _ eps_pos) as [delta [delta_pos Hdelta]] ;
  (Rmin delta 1) ; split.
  apply Rmin_pos_lt ; fourier.
  simpl ; intros y [[_ y_neq] y_b] ; apply Hdelta ; split.
   rewrite <- Rball_rewrite ; eapply Rlt_le_trans ; [eassumption | apply Rmin_r].
   eapply Rlt_le_trans ; [eassumption | apply Rmin_l].
Qed.

Simple compatibility results on continuity_in


Lemma continuity_in_const : D c, continuity_in D (fun _c).
Proof.
intros ; 1 ; split ; [fourier |] ;
 intros ; rewrite R_dist_eq ; assumption.
Qed.

Lemma continuity_in_opp : D f,
  continuity_in D fcontinuity_in D (- f)%F.
Proof.
intros D f Hf x x_in ; apply limit_Ropp ; ass_apply ; assumption.
Qed.

Lemma continuity_pt_in_opp_rev : f D x,
  continuity_pt_in D (- f)%F xcontinuity_pt_in D f x.
Proof.
intros f D x Hf x_in ; apply limit1_in_ext with (- - f)%F.
 intros y y_in ; apply Ropp_involutive.
 rewrite <- (Ropp_involutive (f x)) ;
 apply limit_Ropp, Hf ; assumption.
Qed.

Lemma continuity_in_plus : D f g,
  continuity_in D fcontinuity_in D g
  continuity_in D (f + g)%F.
Proof.
intros f g a b Hf Hg x x_in ; apply limit_plus ; ass_apply ;
 assumption.
Qed.

Lemma continuity_in_minus : D f g,
  continuity_in D fcontinuity_in D g
  continuity_in D (f - g)%F.
Proof.
intros f g a b Hf Hg x x_in ; apply limit_minus ; ass_apply ;
 assumption.
Qed.

Lemma continuity_in_mult : D f g,
  continuity_in D fcontinuity_in D g
  continuity_in D (f × g)%F.
Proof.
intros f g a b Hf Hg x x_in ; apply limit_mul ; ass_apply ;
 assumption.
Qed.

Special case: (open) interval

Lemma continuity_open_interval_Ropp_compat : f lb ub,
  continuity_open_interval lb ub f
  continuity_open_interval (- ub) (- lb) (fun xf (- x)).
Proof.
intros f lb ub Hf b b_in eps eps_pos.
 assert (mb_in : open_interval lb ub (- b)).
  destruct b_in ; split ; fourier.
 destruct (Hf _ mb_in _ eps_pos) as [alpha [alpha_pos Halpha]] ;
  alpha ; split ; [assumption | intros x [x_in x_bd]].
 apply Halpha ; split ; simpl.
  destruct x_in ; split ; fourier.
  rewrite R_dist_opp_compat ; assumption.
Qed.

Lemma continuity_open_interval_Ropp_compat_rev : f lb ub,
  continuity_open_interval (- ub) (- lb) (fun xf (- x)) →
  continuity_open_interval lb ub f.
Proof.
intros f lb ub Hf ; pose (F := fun xf (- x)) ;
 apply continuity_in_ext with (fun xF (- x)).
 intro x ; unfold F ; f_equal ; apply Ropp_involutive.
  rewrite <- (Ropp_involutive lb), <- (Ropp_involutive ub) ;
  apply continuity_open_interval_Ropp_compat, Hf.
Qed.

Lemma continuity_interval_Ropp_compat : f lb ub,
  continuity_interval lb ub f
  continuity_interval (- ub) (- lb) (fun xf (- x)).
Proof.
intros f lb ub Hf b b_in eps eps_pos.
 assert (mb_in : interval lb ub (- b)).
  destruct b_in ; split ; fourier.
 destruct (Hf _ mb_in _ eps_pos) as [alpha [alpha_pos Halpha]] ;
  alpha ; split ; [assumption | intros x [x_in x_bd]].
 apply Halpha ; split ; simpl.
  destruct x_in ; split ; fourier.
  rewrite R_dist_opp_compat ; assumption.
Qed.

Lemma continuity_interval_Ropp_compat_rev : f lb ub,
  continuity_interval (- ub) (- lb) (fun xf (- x)) →
  continuity_interval lb ub f.
Proof.
intros f lb ub Hf ; pose (F := fun xf (- x)) ;
 apply continuity_in_ext with (fun xF (- x)).
 intro x ; unfold F ; f_equal ; apply Ropp_involutive.
  rewrite <- (Ropp_involutive lb), <- (Ropp_involutive ub) ;
  apply continuity_interval_Ropp_compat, Hf.
Qed.

If f x <> y and f continue then there is a ball B around x such that y is not in f B.


Lemma continuity_not_eq_Rball : f (D : RProp) x y,
  D xcontinuity_pt_in D f xf x y
   alp, 0 < alp a, D aRball x alp af a y.
Proof.
intros f D x y Dx f_cont Hneq ; pose (eps := R_dist (f x) y / 2).
 assert (eps_pos: 0 < eps).
  unfold eps, Rdiv ; apply Rlt_mult_inv_pos.
   apply Rabs_pos_lt ; intro Hf ; apply Hneq, Rminus_diag_uniq ; assumption.
   fourier.
 destruct (f_cont Dx eps eps_pos) as [alp [alp_pos Halp]] ; alp ; split.
  assumption.
  intros a Da a_in ; apply Rminus_not_eq, Rabs_pos_lt_contravar.
  transitivity (Rabs (f x - y) - eps).
   apply Rlt_le_trans with eps ; [assumption | right ; unfold eps, R_dist ; field].
   apply Rlt_minus_swap ; apply Rle_lt_trans with (dist R_met (f x - y) (f a - y)) ;
   [apply Rabs_triang_inv | rewrite R_dist_sym, R_dist_minus_compat].
 apply Halp ; split ; [| unfold R_dist] ; assumption.
Qed.