proposition: Lemma MVP_uc_rec (n : nat) (IHn : forall p : MultivariatePolynomial Q_as_CRing n, {f : n_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace n & MVP_uc_sig n p f}) (p : MultivariatePolynomial Q_as_CRing (S n)) : @is_UniformlyContinuousFunction Q_as_MetricSpace (n_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace n) (fun (x:Q_as_CRing) => ProjT1 (IHn (p ! (MVP_C_ Q_as_CRing _ (Qclamp01 x))))) (MVP_apply_modulus p).
proof: Proof. intros e x y Hxy. assert (Hxy' : ball_ex (MVP_apply_modulus p e) (Qclamp01 x) (Qclamp01 y)) by (destruct (MVP_apply_modulus p e); auto; simpl; rewrite -> Qball_Qabs; apply: Qclamp01_close; rewrite <- Qball_Qabs; auto). destruct (Qclamp01_clamped x) as [Hx0 Hx1]. destruct (Qclamp01_clamped y) as [Hy0 Hy1]. assert (X:=@MVP_apply_modulus_correct _ p (Qclamp01 x) (Qclamp01 y) e Hx0 Hx1 Hy0 Hy1 Hxy'). clear Hxy Hxy'; generalize (proj2_sigT _ _ (IHn p ! (MVP_C_ Q_as_CRing n (Qclamp01 x)))) (proj2_sigT _ _ (IHn p ! (MVP_C_ Q_as_CRing n (Qclamp01 y)))). set (x':=Qclamp01 x) in *; set (y':=Qclamp01 y) in *; simpl in X; revert X. generalize (ProjT1 (IHn p ! (MVP_C_ Q_as_CRing n x'))) (ProjT1 (IHn p ! (MVP_C_ Q_as_CRing n y'))). change (Q_as_CSetoid) with (csg_crr Q_as_CRing). generalize (p ! (MVP_C_ Q_as_CRing n x')) (p ! (MVP_C_ Q_as_CRing n y')). clear - e. induction n. - simpl; intros p q s t H Hs Ht; rewrite <- Hs, <- Ht; apply (H (Vector.nil _)); constructor. - simpl. intros p q s t H Hs Ht. split. apply Qpos_nonneg. intro v; apply (fun H => IHn _ _ _ _ H (Hs v) (Ht v)); intros v0 Hv0; apply (H (Vector.cons _ (Qclamp01 v) _ v0)); split; auto; apply Qclamp01_clamped. 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