proposition: Lemma continuity_pt_recip_prelim : forall (f g:R->R) (lb ub : R) (Pr1:lb < ub), (forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) -> (forall x, lb <= x <= ub -> (comp g f) x = id x) -> (forall a, lb <= a <= ub -> continuity_pt f a) -> forall b, f lb < b < f ub -> continuity_pt g b.
proof: Proof. assert (Sublemma : forall x y z, Rmax x y < z <-> x < z /\ y < z). { intros x y z. split. { unfold Rmax. case (Rle_dec x y) ; intros Hyp Hyp2. { split. { apply Rle_lt_trans with (r2:=y) ; assumption. } assumption. } split. { assumption. } apply Rlt_trans with (r2:=x). { assert (Temp : forall x y, ~ x <= y -> x > y). { intros m n Hypmn. intuition. } apply Temp ; clear Temp ; assumption. } assumption. } intros Hyp. unfold Rmax. case (Rle_dec x y). { intro ; exact (proj2 Hyp). } intro ; exact (proj1 Hyp). } assert (Sublemma2 : forall x y z, Rmin x y > z <-> x > z /\ y > z). { intros x y z. split. { unfold Rmin. case (Rle_dec x y) ; intros Hyp Hyp2. { split. { assumption. } apply Rlt_le_trans with (r2:=x) ; intuition. } split. { apply Rlt_trans with (r2:=y). { intuition. } assert (Temp : forall x y, ~ x <= y -> x > y). { intros m n Hypmn. intuition. } apply Temp ; clear Temp ; assumption. } assumption. } intros Hyp. unfold Rmin. case (Rle_dec x y). { intro ; exact (proj1 Hyp). } intro ; exact (proj2 Hyp). } assert (Sublemma3 : forall x y, x <= y /\ x <> y -> x < y). { intros m n Hyp. unfold Rle in Hyp. destruct Hyp as (Hyp1,Hyp2). case Hyp1. { intuition. } intro Hfalse ; apply False_ind ; apply Hyp2 ; exact Hfalse. } intros f g lb ub lb_lt_ub f_incr_interv f_eq_g f_cont_interv b b_encad. assert (f_incr_interv2 : forall x y, lb <= x -> x <= y -> y <= ub -> f x <= f y). { intros m n cond1 cond2 cond3. case cond2. { intro cond. apply Rlt_le ; apply f_incr_interv ; assumption. } intro cond ; right ; rewrite cond ; reflexivity. } unfold continuity_pt, continue_in, limit1_in, limit_in ; intros eps eps_pos. unfold dist ; simpl ; unfold Rdist. assert (b_encad_e : f lb <= b <= f ub) by intuition. elim (f_interv_is_interv f lb ub b lb_lt_ub b_encad_e f_cont_interv) ; intros x Temp. destruct Temp as (x_encad,f_x_b). assert (lb_lt_x : lb < x). { assert (Temp : x <> lb). { intro Hfalse. assert (Temp' : b = f lb). { rewrite <- f_x_b ; rewrite Hfalse ; reflexivity. } assert (Temp'' : b <> f lb). { apply Rgt_not_eq ; exact (proj1 b_encad). } apply Temp'' ; exact Temp'. } apply Sublemma3. split. { exact (proj1 x_encad). } assert (Temp2 : forall x y:R, x <> y <-> y <> x). { intros m n. split ; intuition. } rewrite Temp2 ; assumption. } assert (x_lt_ub : x < ub). { assert (Temp : x <> ub). { intro Hfalse. assert (Temp' : b = f ub). { rewrite <- f_x_b ; rewrite Hfalse ; reflexivity. } assert (Temp'' : b <> f ub). { apply Rlt_not_eq ; exact (proj2 b_encad). } apply Temp'' ; exact Temp'. } apply Sublemma3. split ; [exact (proj2 x_encad) | assumption]. } pose (x1 := Rmax (x - eps) lb). pose (x2 := Rmin (x + eps) ub). assert (Hx1 : x1 = Rmax (x - eps) lb) by intuition. assert (Hx2 : x2 = Rmin (x + eps) ub) by intuition. assert (x1_encad : lb <= x1 <= ub). { split. { apply RmaxLess2. } apply Rlt_le. rewrite Hx1. rewrite Sublemma. split. { apply Rlt_trans with (r2:=x) ; lra. } assumption. } assert (x2_encad : lb <= x2 <= ub). { split. { apply Rlt_le ; rewrite Hx2 ; apply Rgt_lt ; rewrite Sublemma2. split. { apply Rgt_trans with (r2:=x) ; lra. } assumption. } apply Rmin_r. } assert (x_lt_x2 : x < x2). { rewrite Hx2. apply Rgt_lt. rewrite Sublemma2. split ; lra. } assert (x1_lt_x : x1 < x). { rewrite Hx1. rewrite Sublemma. split ; lra. } exists (Rmin (f x - f x1) (f x2 - f x)). split. { apply Rmin_pos ; apply Rgt_minus. { apply f_incr_interv ; [apply RmaxLess2 | | ] ; lra. } apply f_incr_interv ; intuition. } intros y Temp. destruct Temp as (_,y_cond). rewrite <- f_x_b in y_cond. assert (Temp : forall x y d1 d2, d1 > 0 -> d2 > 0 -> Rabs (y - x) < Rmin d1 d2 -> x - d1 <= y <= x + d2). { intros. split. { assert (H10 : forall x y z, x - y <= z -> x - z <= y). { intuition. lra. } apply H10. apply Rle_trans with (r2:=Rabs (y0 - x0)). { replace (Rabs (y0 - x0)) with (Rabs (x0 - y0)). { apply RRle_abs. } rewrite <- Rabs_Ropp. unfold Rminus ; rewrite Ropp_plus_distr. rewrite Ropp_involutive. intuition. } apply Rle_trans with (r2:= Rmin d1 d2). { apply Rlt_le ; assumption. } apply Rmin_l. } assert (H10 : forall x y z, x - y <= z -> x <= y + z). { intuition. lra. } apply H10. apply Rle_trans with (r2:=Rabs (y0 - x0)). { apply RRle_abs. } apply Rle_trans with (r2:= Rmin d1 d2). { apply Rlt_le ; assumption. } apply Rmin_r. } assert (Temp' := Temp (f x) y (f x - f x1) (f x2 - f x)). replace (f x - (f x - f x1)) with (f x1) in Temp' by field. replace (f x + (f x2 - f x)) with (f x2) in Temp' by field. assert (T : f x - f x1 > 0). { apply Rgt_minus. apply f_incr_interv ; intuition. } assert (T' : f x2 - f x > 0). { apply Rgt_minus. apply f_incr_interv ; intuition. } assert (Main := Temp' T T' y_cond). clear Temp Temp' T T'. assert (x1_lt_x2 : x1 < x2). { apply Rlt_trans with (r2:=x) ; assumption. } assert (f_cont_myinterv : forall a : R, x1 <= a <= x2 -> continuity_pt f a). { intros ; apply f_cont_interv ; split. { apply Rle_trans with (r2 := x1) ; intuition. } apply Rle_trans with (r2 := x2) ; intuition. } elim (f_interv_is_interv f x1 x2 y x1_lt_x2 Main f_cont_myinterv) ; intros x' Temp. destruct Temp as (x'_encad,f_x'_y). rewrite <- f_x_b ; rewrite <- f_x'_y. unfold comp in f_eq_g. rewrite f_eq_g. 2:{ split. { apply Rle_trans with (r2:=x1) ; intuition. } apply Rle_trans with (r2:=x2) ; intuition. } rewrite f_eq_g. 2:assumption. unfold id. assert (x'_encad2 : x - eps <= x' <= x + eps). { split. { apply Rle_trans with (r2:=x1) ; [ apply RmaxLess1|] ; intuition. } apply Rle_trans with (r2:=x2) ; [ | apply Rmin_l] ; intuition. } assert (x1_lt_x' : x1 < x'). { apply Sublemma3. assert (x1_neq_x' : x1 <> x'). { intro Hfalse. rewrite Hfalse, f_x'_y in y_cond. assert (Hf : Rabs (y - f x) < f x - y). { apply Rlt_le_trans with (r2:=Rmin (f x - y) (f x2 - f x)). { lra. } apply Rmin_l. } assert(Hfin : f x - y < f x - y). { apply Rle_lt_trans with (r2:=Rabs (y - f x)). { replace (Rabs (y - f x)) with (Rabs (f x - y)). { apply RRle_abs. } rewrite <- Rabs_Ropp. replace (- (f x - y)) with (y - f x) by field ; reflexivity. } lra. } apply (Rlt_irrefl (f x - y)) ; assumption. } split ; intuition. } assert (x'_lb : x - eps < x'). { apply Sublemma3. split. { intuition. } apply Rlt_not_eq. apply Rle_lt_trans with (r2:=x1) ; [ apply RmaxLess1|] ; intuition. } assert (x'_lt_x2 : x' < x2). { apply Sublemma3. assert (x1_neq_x' : x' <> x2). { intro Hfalse. rewrite <- Hfalse, f_x'_y in y_cond. assert (Hf : Rabs (y - f x) < y - f x). { apply Rlt_le_trans with (r2:=Rmin (f x - f x1) (y - f x)). { lra. } apply Rmin_r. } assert(Hfin : y - f x < y - f x). { apply Rle_lt_trans with (r2:=Rabs (y - f x)). { apply RRle_abs. } lra. } apply (Rlt_irrefl (y - f x)) ; assumption. } split ; intuition. } assert (x'_ub : x' < x + eps). { apply Sublemma3. split. { intuition. } apply Rlt_not_eq. apply Rlt_le_trans with (r2:=x2) ; [ |rewrite Hx2 ; apply Rmin_l] ; intuition. } apply Rabs_def1 ; lra. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra