proposition: Lemma MVP_apply_modulus_correct : forall n (p:MultivariatePolynomial Q_as_CRing (S n)) x y e, (0 <= x) -> (x <= 1) -> (0 <= y) -> (y <= 1) -> @ball_ex Q_as_MetricSpace (MVP_apply_modulus p e) x y -> forall (v:Vector.t Q n), UnitHyperInterval v -> @ball Q_as_MetricSpace (proj1_sig e) (MVP_apply _ p (Vector.cons _ x _ v):Q) (MVP_apply _ p (Vector.cons _ y _ v)).
proof: Proof. intros n p x y e Hx0 Hx1 Hy0 Hy1 Hxy v Hv. assert (Hx : (Qmax 0 (Qmin 1 x))==x). rewrite -> Qle_min_r in Hx1. rewrite -> Hx1. rewrite -> Qle_max_r in Hx0. rewrite -> Hx0. reflexivity. assert (Hy : (Qmax 0 (Qmin 1 y))==y). rewrite -> Qle_min_r in Hy1. rewrite -> Hy1. rewrite -> Qle_max_r in Hy0. rewrite -> Hy0. reflexivity. simpl. rewrite <- Hx. rewrite <- Hy. unfold MVP_apply_modulus in Hxy. set (c:=(Qmax (MVP_upperBound (S n) (_D_ p)) (- MVP_lowerBound (S n) (_D_ p)))) in *. set (fp:=cpoly_map (RHcompose _ _ _ (inj_Q_hom IR) (MVP_apply_hom _ v)) p). apply (fun A B e => is_UniformlyContinuousD_Q (Some 0) (Some 1) refl_equal (FPoly _ fp) (FPoly _ (_D_ fp)) (Derivative_poly _ _ _) (fun x => (MVP_apply _ p (Vector.cons _ x _ v))) A c B e x y); try assumption. unfold fp. simpl. intros q _ _. clear - p. change (inj_Q_hom IR (MVP_apply_hom Q_as_CRing v p ! (MVP_C_ Q_as_CRing n q))[=] (cpoly_map (RHcompose (MultivariatePolynomial Q_as_CRing n) Q_as_CRing IR (inj_Q_hom IR) (MVP_apply_hom Q_as_CRing v)) p) ! (inj_Q_hom IR q)). rewrite -> cpoly_map_compose. rewrite <- cpoly_map_apply. apply inj_Q_wd. rewrite -> cpoly_map_apply. apply csbf_wd; try reflexivity. apply: C_MVP_apply. simpl. clear - c Hv. intros x _ [H0x Hx1]. change (AbsIR (_D_ (cpoly_map (RHcompose (MultivariatePolynomial Q_as_CRing n) Q_as_CRing IR (inj_Q_hom IR) (MVP_apply_hom Q_as_CRing v)) p)) ! (inj_Q_hom IR x)[<=] inj_Q IR c). rewrite <- cpoly_map_diff. rewrite -> cpoly_map_compose. rewrite <- cpoly_map_apply. change (AbsIR (inj_Q IR (cpoly_map (MVP_apply_hom Q_as_CRing v) (_D_ p)) ! x)[<=]inj_Q IR c). rewrite -> AbsIR_Qabs. apply inj_Q_leEq. assert (Hx: 0 <= x <= 1). split; apply (leEq_inj_Q IR). rewrite -> inj_Q_Zero. rstepl ([0][/][0][+][1][//]den_is_nonzero IR 0); auto. rewrite -> inj_Q_One. rstepr ([1][/][0][+][1][//]den_is_nonzero IR 1); auto. setoid_replace ((cpoly_map (MVP_apply_hom Q_as_CRing v) (_D_ p)) ! x) with (@MVP_apply Q_as_CRing (S n) (_D_ p) (Vector.cons _ x _ v)). apply Qabs_case; intros H. eapply Qle_trans;[|apply Qmax_ub_l]. apply MVP_upperBound_correct. split; auto. eapply Qle_trans;[|apply Qmax_ub_r]. apply Qopp_le_compat. apply MVP_lowerBound_correct. split; auto. generalize (_D_ p). intros s; clear -s. simpl. change ((cpoly_map_fun (MultivariatePolynomial Q_as_CRing n) Q_as_CRing (MVP_apply_hom Q_as_CRing v) s) ! x == MVP_apply_hom Q_as_CRing v (s ! (MVP_C_ Q_as_CRing n x))). rewrite -> cpoly_map_apply. simpl. rewrite -> C_MVP_apply. reflexivity. 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