proposition: Lemma derivable_pt_lim_recip_interv : forall (f g:R->R) (lb ub x:R) (Prf:forall a : R, g lb <= a <= g ub -> derivable_pt f a) (Prg : continuity_pt g x), lb < ub -> lb < x < ub -> forall (Prg_incr:g lb <= g x <= g ub), (forall x, lb <= x <= ub -> (comp f g) x = id x) -> derive_pt f (g x) (Prf (g x) Prg_incr) <> 0 -> derivable_pt_lim g x (1 / derive_pt f (g x) (Prf (g x) Prg_incr)).
proof: Proof. intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq. assert (x_encad2 : lb <= x <= ub). { split ; apply Rlt_le ; intuition. } elim (Prf (g x)); simpl; intros l Hl. unfold derivable_pt_lim. intros eps eps_pos. pose (y := g x). assert (Hlinv := limit_inv). assert (Hf_deriv : forall eps:R, 0 < eps -> exists delta : posreal, (forall h:R, h <> 0 -> Rabs h < delta -> Rabs ((f (g x + h) - f (g x)) / h - l) < eps)). { intros eps0 eps0_pos. red in Hl ; red in Hl. elim (Hl eps0 eps0_pos). intros deltatemp Htemp. exists deltatemp ; exact Htemp. } elim (Hf_deriv eps eps_pos). intros deltatemp Htemp. red in Hlinv ; red in Hlinv ; unfold dist in Hlinv ; unfold Rdist in Hlinv. assert (Hlinv' := Hlinv (fun h => (f (y+h) - f y)/h) (fun h => h <>0) l 0). unfold limit1_in, limit_in, dist in Hlinv' ; simpl in Hlinv'. unfold Rdist in Hlinv'. assert (Premisse : forall eps : R, eps > 0 -> exists alp : R, alp > 0 /\ (forall x : R, (fun h => h <>0) x /\ Rabs (x - 0) < alp -> Rabs ((f (y + x) - f y) / x - l) < eps)). { intros eps0 eps0_pos. elim (Hf_deriv eps0 eps0_pos). intros deltatemp' Htemp'. exists deltatemp'. split. { exact (cond_pos deltatemp'). } intros htemp cond. apply (Htemp' htemp). { exact (proj1 cond). } replace (htemp) with (htemp - 0). { exact (proj2 cond). } intuition. } assert (Premisse2 : l <> 0). { intro l_null. rewrite l_null in Hl. apply df_neq. rewrite derive_pt_eq. exact Hl. } elim (Hlinv' Premisse Premisse2 eps eps_pos). intros alpha cond. assert (alpha_pos := proj1 cond) ; assert (inv_cont := proj2 cond) ; clear cond. unfold derivable, derivable_pt, derivable_pt_abs, derivable_pt_lim in Prf. elim (Hl eps eps_pos). intros delta f_deriv. assert (g_cont := g_cont_pur). unfold continuity_pt, continue_in, limit1_in, limit_in in g_cont. pose (mydelta := Rmin delta alpha). assert (mydelta_pos : mydelta > 0). { unfold mydelta, Rmin. case (Rle_dec delta alpha). { intro ; exact ((cond_pos delta)). } intro ; exact alpha_pos. } elim (g_cont mydelta mydelta_pos). intros delta' new_g_cont. assert(delta'_pos := proj1 (new_g_cont)). clear g_cont ; assert (g_cont := proj2 (new_g_cont)) ; clear new_g_cont. pose (mydelta'' := Rmin delta' (Rmin (x - lb) (ub - x))). assert(mydelta''_pos : mydelta'' > 0). { unfold mydelta''. apply Rmin_pos ; [intuition | apply Rmin_pos] ; apply Rgt_minus ; intuition. } pose (delta'' := mkposreal mydelta'' mydelta''_pos: posreal). exists delta''. intros h h_neq h_le_delta'. assert (lb <= x +h <= ub). { assert (Sublemma2 : forall x y, Rabs x < Rabs y -> y > 0 -> x < y). { intros m n Hyp_abs y_pos. apply Rlt_le_trans with (r2:=Rabs n). { apply Rle_lt_trans with (r2:=Rabs m) ; [ | assumption] ; apply RRle_abs. } apply Req_le ; apply Rabs_right ; apply Rgt_ge ; assumption. } split. { assert (Sublemma : forall x y z, -z <= y - x -> x <= y + z). { intros ; lra. } apply Sublemma. apply Rlt_le ; apply Sublemma2. { rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=x-lb) ; [| apply RRle_abs] ; apply Rlt_le_trans with (r2:=Rmin (x - lb) (ub - x)) ; [| apply Rmin_l] ; apply Rlt_le_trans with (r2:=Rmin delta' (Rmin (x - lb) (ub - x))). { apply Rlt_le_trans with (r2:=delta''). { assumption. } intuition. } apply Rmin_r. } apply Rgt_minus. intuition. } assert (Sublemma : forall x y z, y <= z - x -> x + y <= z). { intros ; lra. } apply Sublemma. apply Rlt_le ; apply Sublemma2. { apply Rlt_le_trans with (r2:=ub-x) ; [| apply RRle_abs] ; apply Rlt_le_trans with (r2:=Rmin (x - lb) (ub - x)) ; [| apply Rmin_r] ; apply Rlt_le_trans with (r2:=Rmin delta' (Rmin (x - lb) (ub - x))) ; [| apply Rmin_r] ; assumption. } apply Rlt_le_trans with (r2:=delta''). { assumption. } apply Rle_trans with (r2:=Rmin delta' (Rmin (x - lb) (ub - x))). { intuition. } apply Rle_trans with (r2:=Rmin (x - lb) (ub - x)). { apply Rmin_r. } apply Rmin_r. } replace ((g (x + h) - g x) / h) with (1/ (h / (g (x + h) - g x))). 2:{ field ; split. { assumption. } intro Hfalse ; apply h_neq. apply (Rplus_0_r_uniq x). assert (Hfin : (comp f g) (x+h) = (comp f g) x). { apply Rminus_diag_uniq in Hfalse. unfold comp. rewrite Hfalse ; reflexivity. } rewrite f_eq_g in Hfin. { rewrite f_eq_g in Hfin. { unfold id in Hfin. exact Hfin. } assumption. } assumption. } assert (Hrewr : h = (comp f g ) (x+h) - (comp f g) x). { rewrite f_eq_g. { rewrite f_eq_g. { unfold id ; rewrite Rplus_comm ; unfold Rminus ; rewrite Rplus_assoc ; rewrite Rplus_opp_r ; intuition. } assumption. } assumption. } rewrite Hrewr at 1. unfold comp. replace (g(x+h)) with (g x + (g (x+h) - g(x))) by field. pose (h':=g (x+h) - g x). replace (g (x+h) - g x) with h' by intuition. replace (g x + h' - g x) with h' by field. assert (h'_neq : h' <> 0). { unfold h'. intro Hfalse. unfold Rminus in Hfalse ; apply Rminus_diag_uniq in Hfalse. assert (Hfalse' : (comp f g) (x+h) = (comp f g) x). { intros ; unfold comp ; rewrite Hfalse ; trivial. } rewrite f_eq_g in Hfalse' ; rewrite f_eq_g in Hfalse'. - unfold id in Hfalse'. apply Rplus_0_r_uniq in Hfalse'. apply h_neq ; exact Hfalse'. - assumption. - assumption. - assumption. } unfold Rdiv at 1 3; rewrite Rmult_1_l ; rewrite Rmult_1_l. apply inv_cont. split. { exact h'_neq. } rewrite Rminus_0_r. unfold continuity_pt, continue_in, limit1_in, limit_in in g_cont_pur. elim (g_cont_pur mydelta mydelta_pos). intros delta3 cond3. unfold dist in cond3 ; simpl in cond3 ; unfold Rdist in cond3. unfold h'. assert (mydelta_le_alpha : mydelta <= alpha). { unfold mydelta, Rmin ; case (Rle_dec delta alpha). { trivial. } intro ; intuition. } apply Rlt_le_trans with (r2:=mydelta). 2:assumption. unfold dist in g_cont ; simpl in g_cont ; unfold Rdist in g_cont ; apply g_cont. split. { unfold D_x ; simpl. split. { unfold no_cond ; trivial. } intro Hfalse ; apply h_neq. apply (Rplus_0_r_uniq x). symmetry ; assumption. } replace (x + h - x) with h by field. apply Rlt_le_trans with (r2:=delta''). { assumption ; unfold delta''. } intuition. apply Rle_trans with (r2:=mydelta''). { apply Req_le. unfold delta''. intuition. } apply Rmin_l. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra