proposition: Lemma continuity_reciprocal_strictly_increasing_open_interval : forall (f g:R->R) (lb ub:R), lb <= ub -> strictly_increasing_interval lb ub f -> reciprocal_interval lb ub g f -> continuity_interval lb ub f -> continuity_open_interval (f lb) (f ub) g.
proof: Proof. intros f g lb ub lb_le_ub f_incr Hfg Hf b b_in. destruct (IVT_interval f lb ub b) as [a [Ia Ha]] ; try assumption. apply open_interval_interval ; assumption. assert (a_in : open_interval lb ub a). apply interval_open_interval ; [assumption | |]. intro Hfalse ; rewrite Hfalse, Ha in b_in ; apply (Rlt_irrefl b), b_in. intro Hfalse ; rewrite Hfalse, Ha in b_in ; apply (Rlt_irrefl b), b_in. clear Ia. intros eps eps_pos ; pose (xlb := Rmax (a - eps) lb) ; pose (xub := Rmin (a + eps) ub). assert (xlb_in : interval lb ub xlb). split ; [apply RmaxLess2 |]. unfold xlb ; apply Rmax_le_le_le ; split. transitivity a ; [lra | left ; apply a_in]. assumption. assert (xub_in : interval lb ub xub). split ; [| apply Rmin_r]. unfold xub ; apply Rmin_le_le_le ; split. transitivity a ; [left ; apply a_in | lra]. assumption. assert (inc : included (interval xlb xub) (interval lb ub)). apply interval_restriction ; assumption. assert (a_in' : open_interval xlb xub a). split ; [apply Rmax_lt_lt_lt | apply Rmin_lt_lt_lt] ; split ; (lra || apply a_in). exists (interval_dist (f xlb) (f xub) (f a)) ; split. apply open_interval_dist_pos, strictly_increasing_interval_image. eapply strictly_increasing_in_contravariant ; eassumption. assumption. intros x [x_in x_bd] ; rewrite <- Ha in x_bd. destruct (IVT_interval f xlb xub x) as [a' [a'_in Ha']]. eapply continuity_in_contravariant ; eassumption. left ; eapply open_interval_inhabited ; eassumption. replace x with (f a + (x - f a)) by ring ; apply interval_dist_bound. apply open_interval_interval, strictly_increasing_interval_image ; [eapply strictly_increasing_in_contravariant|] ; eassumption. left ; apply x_bd. rewrite <- Ha, <- Ha'. assert (Hrew := Hfg a (open_interval_interval _ _ _ a_in)) ; unfold comp, id in Hrew ; rewrite Hrew ; clear Hrew. assert (Hrew := Hfg a') ; unfold comp, id in Hrew ; rewrite Hrew ; clear Hrew. simpl ; apply Rabs_def1. apply Rlt_minus_sort, Rlt_le_trans with xub ; [| apply Rmin_l]. apply Rle_neq_lt ; [apply a'_in |]. intro Hfalse ; rewrite <- Hfalse, <- Ha' in x_bd ; apply (Rlt_irrefl (f a' - f a)), Rlt_le_trans with (interval_dist (f xlb) (f a') (f a)) ; [| apply Rmin_r]. eapply Rle_lt_trans, x_bd ; right ; symmetry ; simpl ; apply Rabs_right ; left ; apply Rgt_minus, f_incr. eapply open_interval_interval, open_interval_restriction with lb ub ; try (apply interval_l || apply interval_r || rewrite Hfalse) ; eassumption. rewrite Hfalse ; assumption. rewrite Hfalse ; apply a_in'. apply Rlt_minus_sort2, Rle_lt_trans with xlb ; [apply RmaxLess1 |]. apply Rle_neq_lt ; [apply a'_in |]. intro Hfalse ; rewrite Hfalse, <- Ha' in x_bd ; apply (Rlt_irrefl (f a - f a')), Rlt_le_trans with (interval_dist (f a') (f xub) (f a)) ; [| apply Rmin_l]. eapply Rle_lt_trans, x_bd ; right ; symmetry ; simpl. rewrite R_dist_sym ; apply Rabs_right ; left ; apply Rgt_minus, f_incr. rewrite <- Hfalse ; assumption. eapply open_interval_interval, open_interval_restriction with lb ub ; try (apply interval_l || apply interval_r || rewrite <- Hfalse) ; eassumption. rewrite <- Hfalse ; apply a_in'. apply inc ; assumption. Qed.
imports: Rbase Ranalysis Rfunctions Rfunction_def Rseries_def Lra RiemannInt SeqProp PeanoNat RIneq MyRIneq Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rinterval RIVT