proposition: Lemma derivable_pt_recip_interv : forall f g lb ub x, lb < ub -> open_interval (f lb) (f ub) x -> reciprocal_interval (f lb) (f ub) f g -> (forall x : R, interval (f lb) (f ub) x -> interval lb ub (g x)) -> strictly_increasing_interval lb ub f -> derivable_interval lb ub f -> forall (pr : derivable_pt_in (interval lb ub) f (g x)), derive_pt_in _ f (g x) pr <> 0 -> derivable_pt_in (open_interval (f lb) (f ub)) g x.
proof: Proof. intros f g lb ub x lbltub x_in Hfg g_ok Hf Df Dfgx Df_neq ; assert (gfub: g (f ub) = ub). erewrite strictly_increasing_reciprocal_interval_comm ; try eassumption ; [reflexivity | apply interval_r ; left ; assumption]. assert (gflb: g (f lb) = lb). erewrite strictly_increasing_reciprocal_interval_comm ; try eassumption ; [reflexivity | apply interval_l ; left ; assumption]. assert (Df_gx' : derivable_pt_in (interval (g (f lb)) (g (f ub))) f (g x)) by (rewrite gflb, gfub ; assumption). apply derivable_pt_in_reciprocal_interval with f Df_gx' ; try eassumption. rewrite gflb, gfub ; apply interval_open_interval. apply g_ok, open_interval_interval, x_in. intro Hfalse ; destruct (Rlt_irrefl (f lb)). apply Rlt_le_trans with x ; [apply x_in | right]. rewrite Hfalse, Hfg ; [reflexivity |]. apply open_interval_interval, x_in. intro Hfalse ; destruct (Rlt_irrefl (f ub)). apply Rle_lt_trans with x ; [right | apply x_in]. rewrite Hfalse, Hfg ; [reflexivity |]. apply open_interval_interval, x_in. apply continuity_reciprocal_strictly_increasing_open_interval. left ; assumption. assumption. apply strictly_increasing_reciprocal_interval_comm ; try eassumption. apply derivable_in_continuity_in ; assumption. intro Hfalse ; apply Df_neq. apply derivable_pt_lim_derive_pt_interval ; [| apply g_ok, open_interval_interval |] ; try assumption. apply derivable_pt_lim_in_contravariant with (interval (g (f lb)) (g (f ub))). intros y y_in ; rewrite gflb, gfub ; assumption. eapply derive_pt_derivable_pt_lim_interval ; try eassumption ; rewrite gflb, gfub ; [| apply g_ok, open_interval_interval] ; 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