proposition: Lemma MVP_CR_apply_cont : forall n (e : Qpos) (p:MultivariatePolynomial Q_as_CRing (S n)), {d | forall x y, (0 <= x)%CR -> (x <= 1)%CR -> (0 <= 'y)%CR -> ('y <= 1)%CR -> ball_ex d x ('y)%CR -> n_Function_ball01 n (proj1_sig e) (MVP_CR_apply _ (MVP_map inject_Q_hom _ p) x) (MVP_CR_apply _ (MVP_map inject_Q_hom _ p) ('y)%CR)}.
proof: Proof. intros n e p. revert e. induction p; intros e. exists QposInfinity. intros x y _ _ _ _ _. change (n_Function_ball01 n (proj1_sig e) (MVP_CR_apply n [0]) (MVP_CR_apply n [0])). generalize (MVP_CR_apply n [0]). induction n. intros. apply ball_refl, Qpos_nonneg. intros s a _ _. apply IHn. simpl. destruct (IHp ((1#2)*e)%Qpos) as [d0 Hd0]. set (b:=MVP_poor_Bound01 (S n) p). set (d1:=(Qscale_modulus b ((1 # 2) * e))). exists (QposInf_min d0 d1). intros x y Hx0 Hx1 Hy0 Hy1 Hxy. change (n_Function_ball01 n (proj1_sig e) (MVP_CR_apply n ((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))) (MVP_CR_apply n ((MVP_map inject_Q_hom n s)[+](MVP_C_ CRasCRing n ('y)%CR)[*]((cpoly_map (MVP_map inject_Q_hom n) p)) ! (MVP_C_ CRasCRing n (inject_Q_hom y)%CR)))). apply n_Function_ball01_plus. setoid_replace (proj1_sig e) with (proj1_sig ((1#2)*e + (1#2)*e)%Qpos) by (simpl; ring). apply n_Function_ball01_triangle with (MVP_CR_apply n (MVP_C_ CRasCRing n x[*] (cpoly_map (MVP_map inject_Q_hom n) p) ! (MVP_C_ CRasCRing n (inject_Q_hom y)%CR))). apply n_Function_ball01_mult_C; auto. change (n_Function_ball01 n ((1 # 2) * proj1_sig e) (MVP_CR_apply (S n) (MVP_map inject_Q_hom (S n) p) x) (MVP_CR_apply (S n) (MVP_map inject_Q_hom (S n) p) ('y)%CR)). apply Hd0; auto with *. eapply ball_ex_weak_le;[|apply Hxy]. apply QposInf_min_lb_l. eapply n_Function_ball01_wd. reflexivity. apply Morphism_prf. apply mult_wdr. eapply eq_transitive. apply csbf_wd;[apply eq_reflexive|]. symmetry. apply MVP_map_C_. symmetry. apply cpoly_map_apply. apply Morphism_prf. apply mult_wdr. eapply eq_transitive. apply csbf_wd;[apply eq_reflexive|]. symmetry. apply MVP_map_C_. symmetry. apply cpoly_map_apply. apply n_Function_ball01_mult with b. assert (Z:=MVP_poor_is_Bound01 (S n) p _ Hy0 Hy1). unfold b. change (MVP_is_Bound01 n (' MVP_poor_Bound01 (S n) p)%CR (MVP_map inject_Q_hom (S n) p) ! (MVP_C_ CRasCRing n (' y)%CR)) in Z. eapply MVP_is_Bound01_wd;[| |apply Z]. reflexivity. simpl. change (MVP_map inject_Q_hom n p ! (MVP_C_ Q_as_CRing n y)[=] (cpoly_map (MVP_map inject_Q_hom n) p) ! (MVP_C_ CRasCRing n (inject_Q_hom y)%CR)). rewrite <- MVP_map_C_. apply cpoly_map_apply. eapply ball_ex_weak_le;[|apply Hxy]. apply QposInf_min_lb_r. 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