proposition: Lemma derivable_pt_recip_interv (f g:R->R) (lb ub x : R) (lb_lt_ub:lb < ub) (x_encad:f lb < x < f ub) (f_eq_g:forall x : R, f lb <= x -> x <= f ub -> comp f g x = id x) (g_wf:forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub) (f_incr:forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y) (f_derivable:forall a : R, lb <= a <= ub -> derivable_pt f a) : derive_pt f (g x) (derivable_pt_recip_interv_prelim1 f g lb ub x lb_lt_ub x_encad g_wf f_derivable) <> 0 -> derivable_pt g x.
proof: Proof. intros Df_neq. assert(g_incr : g (f lb) < g x < g (f ub)). { assert (Temp:= f_incr_implies_g_incr_interv f g lb ub lb_lt_ub f_incr f_eq_g g_wf). split ; apply Temp ; intuition. - exact (proj1 x_encad). - apply Rlt_le ; exact (proj2 x_encad). - apply Rlt_le ; exact (proj1 x_encad). - exact (proj2 x_encad). } assert(g_incr2 : g (f lb) <= g x <= g (f ub)). { split ; apply Rlt_le ; intuition. } assert (g_eq_f := leftinv_is_rightinv_interv f g lb ub f_incr f_eq_g g_wf). unfold comp, id in g_eq_f. assert (f_derivable2 : forall a : R, g (f lb) <= a <= g (f ub) -> derivable_pt f a). { intros a a_encad ; apply f_derivable. rewrite g_eq_f in a_encad ; rewrite g_eq_f in a_encad ; intuition. } apply derivable_pt_recip_interv_prelim0 with (f:=f) (lb:=f lb) (ub:=f ub) (Prf:=f_derivable2) (Prg_incr:=g_incr2). - apply continuity_pt_recip_interv with (f:=f) (lb:=lb) (ub:=ub) ; intuition. + apply derivable_continuous_pt ; apply f_derivable ; intuition. + exact (proj1 x_encad). + exact (proj2 x_encad). - apply f_incr ; intuition. - assumption. - intros x0 x0_encad ; apply f_eq_g ; intuition. - rewrite pr_nu_var2_interv with (g:=f) (lb:=lb) (ub:=ub) (pr2:=derivable_pt_recip_interv_prelim1 f g lb ub x lb_lt_ub x_encad g_wf f_derivable); [| |rewrite g_eq_f in g_incr ; rewrite g_eq_f in g_incr| ] ; intuition. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra