proposition: Lemma derivable_pt_lim_in_reciprocal_open_interval : forall f g lb ub, reciprocal_interval lb ub f g -> forall x Df_g, open_interval (g lb) (g ub) (g x) -> continuity_pt_in (open_interval lb ub) g x -> open_interval lb ub x -> derive_open_interval (g lb) (g ub) f Df_g (g x) <> 0 -> derivable_pt_lim_in (open_interval lb ub) g x (/ derive_open_interval (g lb) (g ub) f Df_g (g x)).
proof: Proof. intros f g lb ub Hfg x Df_g gx_in Hgx x_in df_neq ; assert (glbub := open_interval_inhabited _ _ _ gx_in). apply limit1_in_ext with (fun y => / ((f (g y) - f (g x)) / (g y - g x))). unfold reciprocal_interval, comp in Hfg ; intros y [y_in y_neq] ; unfold growth_rate ; rewrite Rinv_Rdiv. do 2 (rewrite Hfg ; [| apply open_interval_interval ; assumption]) ; reflexivity. do 2 (rewrite Hfg ; [| apply open_interval_interval ; assumption]). apply Rminus_eq_contra ; symmetry ; assumption. apply Rminus_eq_contra ; intro Hf ; apply y_neq. rewrite <- (Hfg x), <- (Hfg y) ; [rewrite Hf ; reflexivity | |] ; apply open_interval_interval ; assumption. apply limit_inv ; [| assumption]. unfold derive_open_interval ; destruct (in_open_interval_dec (g lb) (g ub) (g x)) as [x_in' |] ; [| contradiction] ; destruct (Df_g _ x_in') as [l Hl] ; intros eps eps_pos ; destruct (Hl _ eps_pos) as [alpha [alpha_pos Halpha]]. pose (beta := Rmin (interval_dist (g lb) (g ub) (g x)) alpha) ; assert (beta_pos : 0 < beta) by (apply Rmin_pos_lt ; [apply open_interval_dist_pos |] ; assumption) ; destruct (Hgx x_in _ beta_pos) as [delta [delta_pos Hdelta]] ; exists delta ; split ; [assumption |]. intros y [[y_in y_neq] y_bd] ; rewrite (derivable_pt_lim_derive_pt_open_interval _ _ _ _ _ _ gx_in Hl) ; apply Halpha ; split. split. replace (g y) with (g x + (g y - g x)) by ring ; apply open_interval_dist_bound. apply open_interval_interval ; assumption. apply Rlt_le_trans with beta ; [simpl in Hdelta ; apply Hdelta | apply Rmin_l] ; split ; assumption. intro Hf ; apply y_neq ; rewrite <- (Hfg x), <- (Hfg y) ; [rewrite Hf ; reflexivity | |] ; apply open_interval_interval ; assumption. apply Rlt_le_trans with beta ; [apply Hdelta | apply Rmin_r] ; split ; 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