proposition: Lemma MVP_uc_fun_close : forall n (e:Qpos) (p:MultivariatePolynomial Q_as_CRing n), MVP_uc_fun_close_sig n (proj1_sig e) (MVP_uc_fun n p) (MVP_CR_apply n (MVP_map inject_Q_hom n p)).
proof: Proof. induction n; intros e p. apply ball_refl, Qpos_nonneg. intros x Hx0 Hx1. change (MVP_uc_fun_close_sig n (proj1_sig e) (MVP_uc_fun (S n) p x) (MVP_CR_apply (S n) (MVP_map inject_Q_hom (S n) p) x)). setoid_replace (proj1_sig e) with (proj1_sig ((((1#3)*e)+(1#3)*e)+(1#3)*e)%Qpos) by (simpl; ring). set (e3:=((1#3)*e)%Qpos). destruct (MVP_CR_apply_cont e3 p) as [d0 Hd]. set (d1:=mu (MVP_uc_fun (S n) p) e3). set (d:=QposInf_min d0 d1). set (y:=Qclamp01 (approximate x d)). destruct (Qclamp01_clamped (approximate x d)) as [Hy0 Hy1]. rewrite <- CRle_Qle in Hy0. rewrite <- CRle_Qle in Hy1. pose proof (Hd _ _ Hx0 Hx1 Hy0 Hy1) as Hd0. assert (ball_ex d x (' Qclamp01 (approximate x d))%CR) as Z. { clear - Hx0 Hx1. destruct d as [d|];[|constructor]. change (ball (proj1_sig d) x (' Qclamp01 (approximate x d))%CR). rewrite <- CRAbsSmall_ball. pose proof (ball_approx_r x d) as Z. rewrite <- CRAbsSmall_ball in Z. revert Z. generalize (approximate x d). clear - Hx0 Hx1. intros s [Z0 Z1]. simpl. split. apply Qmax_case. intros _. apply leEq_transitive with 0%CR. rewrite <- CRopp_0. apply inv_resp_leEq. change (0<='proj1_sig d)%CR. rewrite -> CRle_Qle. apply Qpos_nonneg. change (@cg_minus CRasCGroup x (inject_Q_CR 0)) with (x-0)%CR. rewrite CRopp_0, CRplus_0_r. exact Hx0. intros H. apply (CRle_trans Z0). apply (minus_resp_leEq_rht CRasCOrdField (Cunit s) (' Qmin 1 s)%CR x). rewrite -> CRle_Qle. apply Qmin_lb_r. rewrite -> Qmax_min_distr_r. apply Qmin_case. intros _. apply (@CRle_trans _ (1-1)%CR). apply (CRplus_le_r x 1%CR (CRopp 1%CR)). assumption. rewrite CRplus_opp. rewrite -> CRle_Qle. exact (Qpos_nonneg d). intros H. refine (CRle_trans _ Z1). apply (minus_resp_leEq_rht CRasCOrdField _ _ x). rewrite -> CRle_Qle. apply Qmax_ub_r. } eapply MVP_uc_fun_close_right; [|apply n_Function_ball01_sym;apply Hd0]. eapply MVP_uc_fun_close_left. apply uc_prf. eapply ball_ex_weak_le;[|apply Z]. apply QposInf_min_lb_r. rewrite -> CRle_Qle in Hy0. rewrite -> CRle_Qle in Hy1. rewrite -> MVP_uc_fun_sub_Q;auto. eapply MVP_uc_fun_close_sig_wd. reflexivity. reflexivity. simpl. apply Morphism_prf. eapply eq_transitive. apply csbf_wd. reflexivity. symmetry. apply (MVP_map_C_ inject_Q_hom). symmetry. change (cpoly_map_fun (MultivariatePolynomial Q_as_CRing n) (MultivariatePolynomial CRasCRing n) (MVP_map inject_Q_hom n) p) with (cpoly_map (MVP_map inject_Q_hom n) p). apply cpoly_map_apply. apply IHn. eapply ball_ex_weak_le;[|apply Z]. apply QposInf_min_lb_l. 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