proposition: Lemma MVP_poor_is_Bound01 : forall n p, MVP_is_Bound01 n ('(MVP_poor_Bound01 n p))%CR (MVP_map inject_Q_hom n p).
proof: Proof. induction n. split. change (-('Qabs p)<='p)%CR. rewrite -> CRopp_Qopp. rewrite -> CRle_Qle. simpl in p. replace RHS with (- (- p)) by simpl; ring. apply Qopp_le_compat. rewrite <- Qabs_opp. apply Qle_Qabs. change ('p<=('Qabs p))%CR. rewrite -> CRle_Qle. apply Qle_Qabs. simpl. induction p; intros x Hx0 Hx1. change (MVP_is_Bound01 n 0%CR ([0])). clear - n. induction n. apply AbsSmall_reflexive. apply leEq_reflexive. intros y _ _. apply IHn. change (MVP_is_Bound01 n (' (MVP_poor_Bound01 n s + (fix MVP_poor_Bound01_H (p0 : cpoly (MultivariatePolynomial Q_as_CRing n)) : Q := match p0 with | cpoly_zero _ => 0 | cpoly_linear _ s0 p' => (MVP_poor_Bound01 n s0 + MVP_poor_Bound01_H p')%Q end) p)%Q)%CR (MVP_map inject_Q_hom n s[+]MVP_C_ CRasCRing n x[*](cpoly_map (MVP_map inject_Q_hom n) p) ! (MVP_C_ CRasCRing n x))). rewrite <- CRplus_Qplus. apply MVP_is_Bound01_plus. apply IHn. apply MVP_is_Bound01_mult01; 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