proposition: Lemma Hopital_gninf_Lfin_left : forall (f g : R -> R) (a b L : R), a < b -> forall (Df : forall x : R, open_interval a b x -> derivable_pt f x) (Dg : forall x : R, open_interval a b x -> derivable_pt g x), (forall x : R, a <= x <= b -> continuity_pt f x) -> (forall x : R, a <= x <= b -> continuity_pt g x) -> limit_div_neg g (open_interval a b) b -> (forall (x : R) (Hopen : open_interval a b x), derive_pt g x (Dg x Hopen) <> 0) -> (forall eps : R, eps > 0 -> exists alp : R, alp > 0 /\ (forall (x : R) (Hopen : open_interval a b x), R_dist x b < alp -> R_dist (derive_pt f x (Df x Hopen) / derive_pt g x (Dg x Hopen)) L < eps)) -> limit1_in (fun x : R => f x / g x) (open_interval a b) L b.
proof: Proof. intros f g a b L Hab Df Dg Cf Cg Hdiv_neg g'_not_0 Hlimder. apply limit1_ext with (comp (fun x => f (-x) / g (-x)) (fun x => -x)). intros. unfold comp. ring_simplify (--x). now reflexivity. apply limit1_imp with (Dgf (open_interval a b) (open_interval (-b) (-a)) (fun x => - x)). intros. unfold Dgf. split. now apply H. now destruct H; split; lra. apply (limit_comp (fun x => - x) (fun x : R => f (- x) / g (- x)) _ _ (-b)). unfold limit1_in, limit_in. intros. exists eps. split. now assumption. intros. destruct H0. unfold dist in *. simpl in *. destruct H0. unfold R_dist in *. replace (- x -- b) with (- (x - b)) by ring. rewrite Rabs_Ropp. now apply H1. assert (Df': forall x, open_interval (-b) (-a) x -> derivable_pt (fun x => f (- x)) x). intros. reg. apply Df. now destruct H; split; lra. assert (Dg': forall x, open_interval (-b) (-a) x -> derivable_pt (fun x => g (- x)) x). intros. reg. apply Dg. now destruct H; split; lra. apply Hopital_gninf_Lfin_right with Df' Dg'. now intuition. intros. reg. apply Cf. now destruct H; split; lra. intros. reg. apply Cg. now destruct H; split; lra. apply limit_div_neg_opp. apply Hdiv_neg. intros. intros. assert (Hopen2: open_interval a b (-x)). now destruct Hopen; split; lra. intro. destruct (g'_not_0 (-x) Hopen2). assert (derive_pt (fun x0 : R => g (- x0)) x (Dg' x Hopen) = - derive_pt g (- x) (Dg (- x) Hopen2)). reg. apply Ropp_eq_compat. now apply pr_nu. apply Dg. now apply Hopen2. rewrite <- Ropp_involutive. symmetry. rewrite <- Ropp_involutive. replace 0 with (- 0) in H by ring. apply Ropp_eq_compat. rewrite <- H. rewrite H0. reflexivity. intros eps Heps. specialize (Hlimder eps Heps). destruct Hlimder as [alp [Halp Hsolve]]. exists alp. split. apply Halp. intros. assert (Hopenx : open_interval a b (-x)). split; destruct Hopen; lra. assert (R_dist (-x) b < alp). unfold R_dist in *. replace (- x - b) with (- (x + b)) by ring. ring_simplify (x--b) in H. rewrite Rabs_Ropp. apply H. specialize (Hsolve (-x) Hopenx H0). replace (derive_pt (fun x0 : R => f (- x0)) x (Df' x Hopen)) with (- derive_pt f (- x) (Df (- x) Hopenx)). replace (derive_pt (fun x0 : R => g (- x0)) x (Dg' x Hopen)) with (- derive_pt g (- x) (Dg (- x) Hopenx)). replace ((- derive_pt f (- x) (Df (- x) Hopenx) / - derive_pt g (- x) (Dg (- x) Hopenx))) with ((derive_pt f (- x) (Df (- x) Hopenx) / derive_pt g (- x) (Dg (- x) Hopenx))). apply Hsolve. field. apply g'_not_0. apply derive_pt_comp_Ropp. apply derive_pt_comp_Ropp. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality