proposition: Lemma extend_continuously_continuous : forall a b f, a <= b -> Ranalysis_def.continuity_interval a b f -> Ranalysis1.continuity (extend_continuously f a b).
proof: Proof. intros a b f aleb f_cont x ; destruct (Rlt_le_dec x a) as [xlta | alex]. { exists ((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 ; [lra |]. rewrite <- Rabs_right at 1 ; [assumption | lra]. } 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]]. exists 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. } } } { exists ((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 ; [lra |]. 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 ; [lra |]. rewrite <- Rabs_right at 1 ; [| lra]. rewrite Rabs_minus_sym, Rplus_comm. 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 ; [lra |]. 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 ; [lra |]. rewrite <- Rabs_right at 1 ; [| lra]. rewrite Rabs_minus_sym, Rplus_comm ; assumption. - unfold Rminus ; rewrite Rplus_opp_r, Rabs_R0 ; assumption. } } Qed.
imports: Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_usual Ranalysis_facts Rbase MyRIneq MyR_dist Rfunctions Lra