# Library Coqtail.Reals.Ranalysis.Ranalysis_extend

Require Import Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity.
Require Import Ranalysis_derivability Ranalysis_usual Ranalysis_facts.
Require Import Rbase MyRIneq MyR_dist Rfunctions Fourier.

Open Scope R_scope.

Definition extend_continuously (f : RR) (a b : R) (x : R) : R.
destruct (Rlt_le_dec x a).
+ exact (f a).
+ destruct (Rle_lt_dec x b).
- exact (f x).
- exact (f b).
Defined.

Lemma extend_continuously_continuous : a b f,
a b
Ranalysis_def.continuity_interval a b f
Ranalysis1.continuity (extend_continuously f a b).
Proof.
intros a b f aleb f_cont x ; destruct (Rlt_le_dec x a) as [xlta | alex].
{ ((a - x) / 2)%R ; split.
+ eapply dist_2_pos ; assumption.
+ intros h [_ h_bd] ; simpl ; unfold R_dist, extend_continuously.
destruct (Rlt_le_dec x a) as [_ | hf].
{
destruct (Rlt_le_dec h a) as [_ | hf].
+ unfold Rminus ; rewrite Rplus_opp_r, Rabs_R0 ; assumption.
+ simpl in h_bd ; unfold R_dist in h_bd.
destruct (Rlt_irrefl x) ; apply (Rlt_le_trans x a) ; [assumption |].
transitivity (h + h - a)%R.
- apply Rminus_le_compat_r, Rplus_le_compat ; assumption.
- left. apply Rlt_minus_swap, Rminus_lt_compat_rev with (c := x).
apply Rle_lt_trans with (2 × (h - x))%R ; [right ; ring |].
apply Rmult_Rdiv_lt_compat_l_rev ; [fourier |].
rewrite <- Rabs_right at 1 ; [assumption | fourier].
}
destruct (Rlt_irrefl x) ; apply Rlt_le_trans with a ; assumption.
}
destruct (Rle_lt_dec x b) as [xleb | bltx].
assert (x_in : interval a b x).
{
unfold interval ; split ; assumption.
}
{
intros eps eps_pos ; destruct (f_cont x x_in _ eps_pos) as [delta [delta_pos Hdelta]].
delta ; split.
+ assumption.
+ intros h [_ h_bd] ; simpl ; unfold R_dist, extend_continuously.
destruct (Rlt_le_dec h a) as [hlta | aleh].
{
destruct (Rlt_le_dec x a) as [_ | _].
+ unfold Rminus ; rewrite Rplus_opp_r, Rabs_R0 ; assumption.
+ destruct (Rle_lt_dec x b) as [_ | hf].
{
apply Hdelta ; split.
+ split ; [reflexivity | transitivity x ; assumption].
+ simpl ; rewrite R_dist_sym ; transitivity (R_dist x h).
- apply Rlt_le_Rdist_compat ; assumption.
- rewrite R_dist_sym ; assumption.
}
destruct (Rlt_irrefl x) ; apply Rle_lt_trans with b ; assumption.
}
{
destruct (Rle_lt_dec h b) as [hleb | blth].
{
destruct (Rlt_le_dec x a) as [hf | _].
+ destruct (Rlt_irrefl x) ; apply Rlt_le_trans with a ; assumption.
+ destruct (Rle_lt_dec x b) as [_ | hf].
- apply Hdelta ; repeat split ; assumption.
- destruct (Rlt_irrefl b) ; apply Rlt_le_trans with x ; assumption.
}
{
destruct (Rlt_le_dec x a) as [hf | _].
+ destruct (Rlt_irrefl x) ; apply Rlt_le_trans with a ; assumption.
+ destruct (Rle_lt_dec x b) as [_ | hf].
{
apply Hdelta ; split.
+ split ; [transitivity x ; assumption | reflexivity].
+ simpl ; transitivity (R_dist h x).
- apply Rle_lt_Rdist_compat ; assumption.
- assumption.
}
destruct (Rlt_irrefl x) ; apply Rle_lt_trans with b ; assumption.
}
}
}
{ ((x - b) / 2)%R ; split.
+ eapply dist_2_pos ; assumption.
+ intros h [_ h_bd] ; simpl ; unfold R_dist, extend_continuously.
destruct (Rlt_le_dec x a) as [hf | _].
- destruct (Rlt_irrefl a) ; apply Rle_lt_trans with x ; assumption.
- destruct (Rle_lt_dec x b) as [hf |_].
destruct (Rlt_irrefl b) ; apply Rlt_le_trans with x ; assumption.
{
destruct (Rlt_le_dec h a) as [hlta | aleh].
+ simpl in h_bd ; unfold R_dist in h_bd.
destruct (Rlt_irrefl a) ; apply (Rle_lt_trans a h) ; [| assumption].
transitivity b ; [assumption |].
left ; apply Rmult_lt_reg_l with 2 ; [fourier |].
transitivity (x + b)%R.
- replace (2 × b)%R with (b + b)%R by ring ; apply Rplus_lt_compat_r.
assumption.
- apply Rlt_minus_sort3, Rplus_lt_reg_r with x.
apply Rle_lt_trans with (2 × (x - h))%R ; [right ; ring |].
apply Rmult_Rdiv_lt_compat_l_rev ; [fourier |].
rewrite <- Rabs_right at 1 ; [| fourier].
rewrite Rabs_minus_sym ; assumption.
+ destruct (Rle_lt_dec h b) as [hleb | blth].
- destruct (Rlt_irrefl b) ; apply Rlt_le_trans with h ; [| assumption].
apply Rmult_lt_reg_l with 2 ; [fourier |].
transitivity (x + b)%R.
× replace (2 × b)%R with (b + b)%R by ring ; apply Rplus_lt_compat_r.
assumption.
× apply Rlt_minus_sort3, Rplus_lt_reg_r with x.
apply Rle_lt_trans with (2 × (x - h))%R ; [right ; ring |].
apply Rmult_Rdiv_lt_compat_l_rev ; [fourier |].
rewrite <- Rabs_right at 1 ; [| fourier].
rewrite Rabs_minus_sym ; assumption.
- unfold Rminus ; rewrite Rplus_opp_r, Rabs_R0 ; assumption.
}
}
Qed.

Lemma extend_continuously_extends_open_interval : a b f x,
Rinterval.open_interval a b xf x = extend_continuously f a b x.
Proof.
intros a b f x [alex xleb] ; unfold extend_continuously.
destruct (Rlt_le_dec x a).
+ destruct (Rlt_irrefl x) ; transitivity a ; assumption.
+ destruct (Rle_lt_dec x b).
- reflexivity.
- destruct (Rlt_irrefl x) ; transitivity b ; assumption.
Qed.

Lemma extend_continuously_extends_interval : a b f x,
Rinterval.interval a b xf x = extend_continuously f a b x.
Proof.
intros a b f x [alex xleb] ; unfold extend_continuously.
destruct (Rlt_le_dec x a).
+ destruct (Rlt_irrefl x) ; apply Rlt_le_trans with a ; assumption.
+ destruct (Rle_lt_dec x b).
- reflexivity.
- destruct (Rlt_irrefl x) ; apply Rle_lt_trans with b ; assumption.
Qed.

Lemma extend_continuously_derivable_open_interval : a b f,
Ranalysis_def.derivable_open_interval a b f
Ranalysis_def.derivable_open_interval a b (extend_continuously f a b).
Proof.
intros a b f f_deriv x x_in ;
eapply derivable_pt_in_ext_strong, f_deriv ; try assumption.
apply extend_continuously_extends_open_interval.
Qed.

Lemma extend_continuously_derive_open_interval :
a b f fext_deriv f_deriv c,
(derive_open_interval a b (extend_continuously f a b) fext_deriv c =
derive_open_interval a b f f_deriv c)%R.
Proof.
intros a b f fext_deriv f_deriv c ; unfold derive_open_interval ;
destruct (in_open_interval_dec a b c) as [c_in | c_out].
+ apply derive_pt_in_ext_strong.
- apply dense_open_interval.
× transitivity c ; apply c_in.
× apply open_interval_interval ; assumption.
- assumption.
- intros ; symmetry ; eapply extend_continuously_extends_open_interval ; assumption.
+ reflexivity.
Qed.