proposition: Lemma n_Function_ball01_mult : forall n e x y p M, MVP_is_Bound01 n ('M)%CR p -> ball_ex (Qscale_modulus M e) x y -> n_Function_ball01 n (proj1_sig e) (MVP_CR_apply n (MVP_C_ CRasCRing n x[*]p)) (MVP_CR_apply n (MVP_C_ CRasCRing n y[*]p)).
proof: Proof. induction n; intros e x y p b Hb Hxy. change (ball (proj1_sig e) (x*p) (y*p))%CR. rewrite <- CRAbsSmall_ball. change (@cg_minus CRasCOrdField (x * p)%CR (y * p)%CR) with (x*p-y*p)%CR. setoid_replace (x*p-y*p)%CR with (p*(x-y))%CR by ring. simpl in Hb. case_eq (Qscale_modulus b e). intros q Hq. apply AbsSmall_leEq_trans with (CRabs p * 'proj1_sig q)%CR. destruct b as [[|nb|nb] db]. discriminate Hq. simpl in Hq. injection Hq; clear Hq; intros Hq; rewrite <- Hq. assert (' proj1_sig ((db # nb) * e)%Qpos >< 0)%CR as Z. { apply Qap_CRap, Qpos_nonzero. } apply shift_mult_leEq with Z. apply: CRlt_Qlt; auto with *. unfold AbsSmall in Hb. rewrite <- CRabs_AbsSmall in Hb. stepr ('(nb#db))%CR; auto. change ((' (nb # db)) == (' proj1_sig e)%CR * CRinvT (' proj1_sig ((db # nb) * e)%Qpos) Z)%CR. rewrite -> CRinv_Qinv. rewrite -> CRmult_Qmult. rewrite -> CReq_Qeq. simpl. rewrite -> Qinv_mult_distr. replace RHS with ((/(db#nb) * proj1_sig e) * /proj1_sig e) by simpl; ring. change (nb#db == ((nb#db)*proj1_sig e/proj1_sig e)). rewrite -> Qdiv_mult_l. reflexivity. apply Qpos_nonzero. elim (Qle_not_lt 0 (Zneg nb # db)); auto with *. rewrite <- CRle_Qle. eapply AbsSmall_nonneg. apply Hb. cut (Not (Not (@AbsSmall CRasCOrdField (CRabs p * (' proj1_sig q))%CR (p * (x - y))%CR))). { unfold Not, AbsSmall. repeat rewrite -> leEq_def. unfold Not; tauto. } generalize (leEq_or_leEq CRasCOrdField [0] p). unfold Not. intros H abs. contradict H; intro H. contradict abs. destruct H as [Hp|Hp]. - rewrite -> CRabs_pos; auto. apply mult_resp_AbsSmall;auto. rewrite Hq in Hxy. apply (CRAbsSmall_ball x y). auto. - rewrite -> CRabs_neg; auto. setoid_replace (p * (x - y))%CR with (-p * (y - x))%CR by ring. apply mult_resp_AbsSmall. rewrite <- CRopp_0. apply inv_resp_leEq. auto. rewrite Hq in Hxy. apply (CRAbsSmall_ball y x). apply ball_sym. apply Hxy. - intros Hq. destruct b as [[|nb|nb] db]; try discriminate Hq. setoid_replace p with 0%CR. rewrite CRmult_comm, CRmult_0_r. apply zero_AbsSmall. simpl. rewrite -> CRle_Qle; auto with *. destruct Hb as [Hb0 Hb1]. apply CRle_antisym. split. stepr ((' (0 # db)))%CR; auto. change ('(0#db)==0)%CR. rewrite -> CReq_Qeq. unfold Qeq; reflexivity. stepl (-(' (0 # db)))%CR; auto. rewrite -> CRopp_Qopp. change ('(0#db)==0)%CR. rewrite -> CReq_Qeq. unfold Qeq; reflexivity. - simpl. intros a Ha0 Ha1. eapply n_Function_ball01_wd. reflexivity. apply Morphism_prf. eapply eq_transitive. apply mult_apply. apply csbf_wd. apply c_apply. reflexivity. apply Morphism_prf. eapply eq_transitive. apply mult_apply. apply csbf_wd. apply c_apply. reflexivity. apply: IHn; auto. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.algebra.Bernstein CoRN.algebra.CRing_Homomorphisms CoRN.algebra.COrdFields2 CoRN.model.ordfields.Qordfield CoRN.model.totalorder.QMinMax CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.reals.fast.CRabs CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.CRArith CoRN.reals.fast.CRArith_alg CoRN.algebra.RSetoid