proposition: Lemma exp_bound_bound : forall (z:Z) x, closer (inj_Q IR (z:Q)) x -> AbsIR (Exp x)[<=]inj_Q IR (proj1_sig (exp_bound z)).
proof: Proof. intros [|z|z]; simpl; intros x Hx; apply AbsSmall_imp_AbsIR; (apply leEq_imp_AbsSmall;[apply less_leEq; apply Exp_pos|]). rewrite inj_Q_One. apply Exp_leEq_One. rewrite inj_Q_Zero in Hx. exact Hx. apply leEq_transitive with (Exp (Max x [0])). apply Exp_resp_leEq. apply lft_leEq_Max. stepr (Three[!](inj_Q IR (inject_Z z))[//](pos_three IR)). astepl (E[!](Max x [0])[//]pos_E). apply real_power_resp_leEq_both; try solve [IR_solve_ineq (1#1)%Qpos]. apply rht_leEq_Max. apply Max_leEq; auto. stepl (inj_Q IR 0). apply inj_Q_leEq. simpl; auto with *. apply (inj_Q_nring IR 0). stepl (Three[!]nring (nat_of_P z)[//]pos_three IR). astepl (@nring IR 3 [^](nat_of_P z)). stepl ((inj_Q IR (3%mc:Q))[^](nat_of_P z)). stepl (inj_Q IR (3%mc^z)). apply inj_Q_wd. apply eq_symmetric. reflexivity. rewrite <- convert_is_POS. apply inj_Q_power. apply nexp_wd. apply (inj_Q_nring IR 3). apply power_wd. apply eq_reflexive. apply eq_symmetric. rewrite <- convert_is_POS. stepl (inj_Q IR (nring (nat_of_P z))). apply (inj_Q_nring). apply inj_Q_wd; apply nring_Q. stepr (Half[!](inj_Q IR (inject_Z z))[//](pos_half IR)). astepl (Exp [--][--]x). astepl ([1][/]_[//](Exp_ap_zero [--]x)). unfold Half. astepr (([1][!]inj_Q IR (z:Q)[//]pos_one _)[/]((Two[!]inj_Q IR (z:Q)[//]pos_two _))[//]power_ap_zero _ _ _). astepr ([1][/]((Two[!]inj_Q IR (z:Q)[//]pos_two _))[//]power_ap_zero _ _ _). apply recip_resp_leEq. apply power_pos. astepr (E[!][--]x[//]pos_E). apply real_power_resp_leEq_both; try solve [IR_solve_ineq (1#1)%Qpos]. stepl (inj_Q IR 0). apply inj_Q_leEq. simpl; auto with *. apply (inj_Q_nring IR 0). rewrite <- cg_inv_inv. apply inv_resp_leEq. stepr (inj_Q IR ((Zneg z):Q)). assumption. astepr (inj_Q IR (-(z:Q))). apply inj_Q_wd. simpl; reflexivity. stepl (Half[!]nring (nat_of_P z)[//]pos_half IR). astepl (@Half IR [^](nat_of_P z)). stepl ((inj_Q IR ((1#2):Q))[^](nat_of_P z)). stepl (inj_Q IR ((1#2)^z)). apply inj_Q_wd. apply eq_symmetric. reflexivity. rewrite <- (convert_is_POS z). apply inj_Q_power. apply nexp_wd. assert (X:(inj_Q IR (2:Q))[#][0]). stepr (inj_Q IR 0). apply inj_Q_ap; discriminate. apply (inj_Q_nring IR 0). stepr ((inj_Q IR 1)[/]_[//]X). stepl (inj_Q IR (1/2)). apply inj_Q_div. apply inj_Q_wd. apply eq_symmetric; apply Qmake_Qdiv. apply div_wd. apply inj_Q_One. apply (inj_Q_nring IR 2). apply power_wd. apply eq_reflexive. apply eq_symmetric. rewrite <- convert_is_POS. stepl (inj_Q IR (nring (nat_of_P z))). apply (inj_Q_nring). apply inj_Q_wd; apply nring_Q. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRAlternatingSum_alg CoRN.reals.fast.CRstreams CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.iso_CReals Coq.QArith.Qpower CoRN.algebra.COrdFields2 CoRN.model.ordfields.Qordfield CoRN.transc.PowerSeries CoRN.reals.fast.CRpower CoRN.transc.Exponential CoRN.transc.RealPowers CoRN.reals.fast.Compress Coq.NArith.Ndigits CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.reals.fast.CRsign CoRN.reals.Q_in_CReals Coq.QArith.Qabs Coq.QArith.Qround CoRN.tactics.CornTac MathClasses.theory.int_pow MathClasses.interfaces.abstract_algebra