Multivariable polynomails
Here we prove that multivariable polynomials over the rationals are uniformly continuous on the unit hyperinterval. Hence they can be lifted to apply to real numbers. This allows real numbers to be used in polynomial expressions so that each variable is only approximated once.
Define the type of multivariable polynomials with n variables
Fixpoint MultivariatePolynomial (n:nat) : CRing :=
match n with
| O => F
| S n' => cpoly_cring (MultivariatePolynomial n')
end.
match n with
| O => F
| S n' => cpoly_cring (MultivariatePolynomial n')
end.
The constant multivariable polynomial
Fixpoint MVP_C_ (n:nat) : RingHom F (MultivariatePolynomial n) :=
match n return RingHom F (MultivariatePolynomial n) with
| O => RHid _
| S n' => RHcompose _ _ _ _C_ (MVP_C_ n')
end.
match n return RingHom F (MultivariatePolynomial n) with
| O => RHid _
| S n' => RHcompose _ _ _ _C_ (MVP_C_ n')
end.
Apply a multivariable polynomial to a vector of input values
Fixpoint MVP_apply (n:nat) : MultivariatePolynomial n -> (vector F n) -> F :=
match n return MultivariatePolynomial n -> vector F n -> F with
| O => fun x _ => x
| (S n') => fun p v => (MVP_apply (p ! (MVP_C_ _ (Vhead _ _ v))) (Vtail _ _ v))
end.
End MultivariatePolynomial.
Lemma zero_MVP_apply : forall F n v, MVP_apply F (0:MultivariatePolynomial F n) v[=]0.
Lemma one_MVP_apply : forall F n v, MVP_apply F (1:MultivariatePolynomial F n) v[=]1.
Lemma C_MVP_apply : forall F n q v, MVP_apply F (MVP_C_ F n q) v[=]q.
Lemma MVP_plus_apply: forall F n (p q : MultivariatePolynomial F n) v,
MVP_apply F (p[+]q) v [=] MVP_apply F p v[+]MVP_apply F q v.
Lemma MVP_mult_apply: forall F n (p q : MultivariatePolynomial F n) v,
MVP_apply F (p[*]q) v [=] MVP_apply F p v[*]MVP_apply F q v.
Lemma MVP_c_mult_apply: forall F n (p : MultivariatePolynomial F n) c v,
MVP_apply F (MVP_C_ _ _ c[*]p) v[=]c[*]MVP_apply F p v.
Lemma MVP_apply_hom_strext : forall (F:CRing) n (v:vector F n), fun_strext (fun (p:MultivariatePolynomial F n) => MVP_apply _ p v).
Definition MVP_apply_hom_csf (F:CRing) n (v:vector F n) :=
Build_CSetoid_fun _ _ _ (MVP_apply_hom_strext F v).
Definition MVP_apply_hom (F:CRing) n (v:vector F n) : RingHom (MultivariatePolynomial F n) F.
Defined.
match n return MultivariatePolynomial n -> vector F n -> F with
| O => fun x _ => x
| (S n') => fun p v => (MVP_apply (p ! (MVP_C_ _ (Vhead _ _ v))) (Vtail _ _ v))
end.
End MultivariatePolynomial.
Lemma zero_MVP_apply : forall F n v, MVP_apply F (0:MultivariatePolynomial F n) v[=]0.
Lemma one_MVP_apply : forall F n v, MVP_apply F (1:MultivariatePolynomial F n) v[=]1.
Lemma C_MVP_apply : forall F n q v, MVP_apply F (MVP_C_ F n q) v[=]q.
Lemma MVP_plus_apply: forall F n (p q : MultivariatePolynomial F n) v,
MVP_apply F (p[+]q) v [=] MVP_apply F p v[+]MVP_apply F q v.
Lemma MVP_mult_apply: forall F n (p q : MultivariatePolynomial F n) v,
MVP_apply F (p[*]q) v [=] MVP_apply F p v[*]MVP_apply F q v.
Lemma MVP_c_mult_apply: forall F n (p : MultivariatePolynomial F n) c v,
MVP_apply F (MVP_C_ _ _ c[*]p) v[=]c[*]MVP_apply F p v.
Lemma MVP_apply_hom_strext : forall (F:CRing) n (v:vector F n), fun_strext (fun (p:MultivariatePolynomial F n) => MVP_apply _ p v).
Definition MVP_apply_hom_csf (F:CRing) n (v:vector F n) :=
Build_CSetoid_fun _ _ _ (MVP_apply_hom_strext F v).
Definition MVP_apply_hom (F:CRing) n (v:vector F n) : RingHom (MultivariatePolynomial F n) F.
Defined.
MVP_map applies a ring homomorphism to the coefficents of a multivariable polynomial
Fixpoint MVP_map R S (f:RingHom R S) (n:nat) : RingHom (MultivariatePolynomial R n) (MultivariatePolynomial S n) :=
match n return RingHom (MultivariatePolynomial R n) (MultivariatePolynomial S n) with
| O => f
| (S n') => cpoly_map (MVP_map f n')
end.
Lemma MVP_map_C_ : forall R S (f:RingHom R S) n c,
MVP_map f n (MVP_C_ _ _ c)[=]MVP_C_ _ _ (f c).
match n return RingHom (MultivariatePolynomial R n) (MultivariatePolynomial S n) with
| O => f
| (S n') => cpoly_map (MVP_map f n')
end.
Lemma MVP_map_C_ : forall R S (f:RingHom R S) n c,
MVP_map f n (MVP_C_ _ _ c)[=]MVP_C_ _ _ (f c).
Some upper bound on the polynomial on 0,1
Fixpoint MVP_upperBound (n:nat) : MultivariatePolynomial Q_as_CRing n -> Q :=
match n return MultivariatePolynomial Q_as_CRing n -> Q with
| O => fun x => x
| (S n') => fun p => let (m,b) := BernsteinCoefficents (MVP_C_ Q_as_CRing n') p
in vector_rec _ (fun _ _ => Q) 0%Q
(fun c _ _ rec => Qmax (MVP_upperBound n' c) rec) m b
end.
match n return MultivariatePolynomial Q_as_CRing n -> Q with
| O => fun x => x
| (S n') => fun p => let (m,b) := BernsteinCoefficents (MVP_C_ Q_as_CRing n') p
in vector_rec _ (fun _ _ => Q) 0%Q
(fun c _ _ rec => Qmax (MVP_upperBound n' c) rec) m b
end.
Some lower bound on the polynomial on 0,1
Fixpoint MVP_lowerBound (n:nat) : MultivariatePolynomial Q_as_CRing n -> Q :=
match n return MultivariatePolynomial Q_as_CRing n -> Q with
| O => fun x => x
| (S n') => fun p => let (m,b) := BernsteinCoefficents (MVP_C_ Q_as_CRing n') p
in vector_rec _ (fun _ _ => Q) 0%Q
(fun c _ _ rec => Qmin (MVP_lowerBound n' c) rec) m b
end.
match n return MultivariatePolynomial Q_as_CRing n -> Q with
| O => fun x => x
| (S n') => fun p => let (m,b) := BernsteinCoefficents (MVP_C_ Q_as_CRing n') p
in vector_rec _ (fun _ _ => Q) 0%Q
(fun c _ _ rec => Qmin (MVP_lowerBound n' c) rec) m b
end.
Definition of the unit hyperinterval of n dimensions
Fixpoint UnitHyperInterval (n:nat) (v:vector Q n) : Prop :=
match v with
| Vnil => True
| Vcons a _ v' => 0 <= a <= 1 /\ UnitHyperInterval v'
end.
match v with
| Vnil => True
| Vcons a _ v' => 0 <= a <= 1 /\ UnitHyperInterval v'
end.
Return the ith entry of a vector
Fixpoint Vector_ix A (n i:nat) (H:(i < n)%nat) (v:vector A n) : A :=
match v in vector _ m return (i < m)%nat -> A with
| Vnil => fun p => False_rect _ (lt_n_O _ p)
| Vcons c n' v' => fun _ => match lt_le_dec i n' with
| left p => Vector_ix p v'
| right _ => c
end
end H.
match v in vector _ m return (i < m)%nat -> A with
| Vnil => fun p => False_rect _ (lt_n_O _ p)
| Vcons c n' v' => fun _ => match lt_le_dec i n' with
| left p => Vector_ix p v'
| right _ => c
end
end H.
The upper and lower bounds are correct.
Lemma MVP_upperBound_correct : forall n p v, UnitHyperInterval v -> MVP_apply _ p v[<=]MVP_upperBound n p.
Lemma MVP_lowerBound_correct : forall n p v, UnitHyperInterval v -> MVP_lowerBound n p[<=]MVP_apply _ p v.
Lemma MVP_lowerBound_correct : forall n p v, UnitHyperInterval v -> MVP_lowerBound n p[<=]MVP_apply _ p v.
Use the upper and lower bounds of the derivative of a polynomial to
define its modulus of continuity.
Definition MVP_apply_modulus n (p:MultivariatePolynomial Q_as_CRing (S n)) :=
let p' := (_D_ p) in
Qscale_modulus (Qmax (MVP_upperBound (S n) p') (-(MVP_lowerBound (S n) p'))).
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 (MVP_apply_modulus p e) x y ->
forall (v:vector Q n), UnitHyperInterval v -> ball e (MVP_apply _ p (Vcons _ x _ v):Q) (MVP_apply _ p (Vcons _ y _ v)).
let p' := (_D_ p) in
Qscale_modulus (Qmax (MVP_upperBound (S n) p') (-(MVP_lowerBound (S n) p'))).
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 (MVP_apply_modulus p e) x y ->
forall (v:vector Q n), UnitHyperInterval v -> ball e (MVP_apply _ p (Vcons _ x _ v):Q) (MVP_apply _ p (Vcons _ y _ v)).
Clamp a value to the unit interval
Definition Qclamp01 := QboundBelow_uc (0) ∘ QboundAbove_uc 1.
Lemma Qclamp01_clamped : forall x, 0 <= Qclamp01 x <= 1.
Lemma Qclamp01_le : forall x y, x <= y -> Qclamp01 x <= Qclamp01 y.
Lemma Qclamp01_close : forall e x y, Qabs (x-y) <= e -> Qabs (Qclamp01 x - Qclamp01 y) <= e.
Lemma Qclamp01_clamped : forall x, 0 <= Qclamp01 x <= 1.
Lemma Qclamp01_le : forall x y, x <= y -> Qclamp01 x <= Qclamp01 y.
Lemma Qclamp01_close : forall e x y, Qabs (x-y) <= e -> Qabs (Qclamp01 x - Qclamp01 y) <= e.
Definition of a setoid function type of n parameters
Fixpoint n_Function X Y (n:nat) :=
match n with
|O => Y
|S n' => extSetoid X (n_Function X Y n')
end.
match n with
|O => Y
|S n' => extSetoid X (n_Function X Y n')
end.
Definition of a uniformly continuous function type of n parameters
Fixpoint n_UniformlyContinuousFunction (X Y:MetricSpace) (n:nat) :=
match n with
|O => Y
|S n' => X --> (n_UniformlyContinuousFunction X Y n')
end.
match n with
|O => Y
|S n' => X --> (n_UniformlyContinuousFunction X Y n')
end.
MVP_uc_sig is a recursive type definition that is needed for part of the definition of
of a multivariable polynomial as a uniformly continuous function.
Fixpoint MVP_uc_sig (n:nat) :MultivariatePolynomial Q_as_CRing n -> n_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace n -> Type :=
match n return MultivariatePolynomial Q_as_CRing n -> n_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace n -> Type with
| O => fun p x => p==x
| (S n') => fun p f => forall v, MVP_uc_sig n' (p ! (MVP_C_ Q_as_CRing _ (Qclamp01 v))) (f v)
end.
match n return MultivariatePolynomial Q_as_CRing n -> n_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace n -> Type with
| O => fun p x => p==x
| (S n') => fun p f => forall v, MVP_uc_sig n' (p ! (MVP_C_ Q_as_CRing _ (Qclamp01 v))) (f v)
end.
Multivariable polynomials are uniformly continuous on the unit hyper interval
Definition MVP_uc : forall n (p:MultivariatePolynomial Q_as_CRing n),
{f:n_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace n
|MVP_uc_sig _ p f}.
Defined.
Definition MVP_uc_Q := (fun n p => ProjT1 (MVP_uc n p)).
Add Parametric Morphism n : (@MVP_uc_Q n) with signature (@st_eq _) ==> (@st_eq _) as MVP_uc_Q_wd.
Fixpoint n_Cap X Y (plX : PrelengthSpace X) n : Complete (n_UniformlyContinuousFunction X Y n) -->
n_UniformlyContinuousFunction (Complete X) (Complete Y) n :=
match n return Complete (n_UniformlyContinuousFunction X Y n) -->
n_UniformlyContinuousFunction (Complete X) (Complete Y) n with
| O => uc_id _
| (S n') => (uc_compose_uc _ _ _ (@n_Cap X Y plX n')) ∘ (@Cap X _ plX)
end.
{f:n_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace n
|MVP_uc_sig _ p f}.
Defined.
Definition MVP_uc_Q := (fun n p => ProjT1 (MVP_uc n p)).
Add Parametric Morphism n : (@MVP_uc_Q n) with signature (@st_eq _) ==> (@st_eq _) as MVP_uc_Q_wd.
Fixpoint n_Cap X Y (plX : PrelengthSpace X) n : Complete (n_UniformlyContinuousFunction X Y n) -->
n_UniformlyContinuousFunction (Complete X) (Complete Y) n :=
match n return Complete (n_UniformlyContinuousFunction X Y n) -->
n_UniformlyContinuousFunction (Complete X) (Complete Y) n with
| O => uc_id _
| (S n') => (uc_compose_uc _ _ _ (@n_Cap X Y plX n')) ∘ (@Cap X _ plX)
end.
A Cmap for an n parameter function.
Definition n_Cmap X Y (plX : PrelengthSpace X) n : n_UniformlyContinuousFunction X Y n -->
n_UniformlyContinuousFunction (Complete X) (Complete Y) n :=
(@n_Cap X Y plX n) ∘ (@Cunit _).
Add Parametric Morphism X Y plX n : (@n_Cap X Y plX n)
with signature (@st_eq _) ==> (@st_eq _) as n_Cap_wd.
Add Parametric Morphism X Y plX n : (@n_Cmap X Y plX n)
with signature (@st_eq _) ==> (@st_eq _) as n_Cmap_wd.
Qed.
n_UniformlyContinuousFunction (Complete X) (Complete Y) n :=
(@n_Cap X Y plX n) ∘ (@Cunit _).
Add Parametric Morphism X Y plX n : (@n_Cap X Y plX n)
with signature (@st_eq _) ==> (@st_eq _) as n_Cap_wd.
Add Parametric Morphism X Y plX n : (@n_Cmap X Y plX n)
with signature (@st_eq _) ==> (@st_eq _) as n_Cmap_wd.
Qed.
Multivariable polynomials on the unit hyper interval can be applied to real numbers
Definition MVP_uc_fun n (p:MultivariatePolynomial _ n) :
n_UniformlyContinuousFunction CR CR n :=
n_Cmap _ QPrelengthSpace n (MVP_uc_Q n p).
Add Parametric Morphism n : (@MVP_uc_fun n)
with signature (@st_eq _) ==> (@st_eq _) as MVP_uc_fun_wd.
Qed.
Section MVP_correct.
n_UniformlyContinuousFunction CR CR n :=
n_Cmap _ QPrelengthSpace n (MVP_uc_Q n p).
Add Parametric Morphism n : (@MVP_uc_fun n)
with signature (@st_eq _) ==> (@st_eq _) as MVP_uc_fun_wd.
Qed.
Section MVP_correct.
Correctness lemmas for MVP_uc_fun.
Lemma MVP_uc_fun_sub_Q : forall n (p:MultivariatePolynomial _ (S n)) x,
0 <= x -> x <= 1 ->
(MVP_uc_fun (S n) p ('x)%CR)[=](MVP_uc_fun n (p!(MVP_C_ _ _ x))).
Fixpoint MVP_CR_apply n : extSetoid (MultivariatePolynomial CRasCRing n) (n_Function CR CR n) :=
match n return extSetoid (MultivariatePolynomial CRasCRing n) (n_Function CR CR n) with
| O => id
| S n' => Build_Morphism _ (n_Function CR CR (S n')) (fun p => Build_Morphism _ _ (fun x => MVP_CR_apply n' (p!(MVP_C_ _ n' x)))
(fun (x y : RegularFunction Q_as_MetricSpace) (Hxy : regFunEq x y) =>
Morphism_prf (MVP_CR_apply n') p ! (MVP_C_ CRasCRing n' x)
p ! (MVP_C_ CRasCRing n' y)
(cpoly_apply_wd (MultivariatePolynomial CRasCRing n') p p
(MVP_C_ CRasCRing n' x) (MVP_C_ CRasCRing n' y) (reflexivity p)
(csf_wd CRasCSetoid (MultivariatePolynomial CRasCRing n')
(MVP_C_ CRasCRing n') x y Hxy))))
(fun (x1 x2 : cpoly_cring (MultivariatePolynomial CRasCRing n'))
(H : x1[=]x2) (x : RegularFunction Q_as_MetricSpace) =>
Morphism_prf (MVP_CR_apply n') x1 ! (MVP_C_ CRasCRing n' x)
x2 ! (MVP_C_ CRasCRing n' x)
(cpoly_apply_wd (MultivariatePolynomial CRasCRing n') x1 x2
(MVP_C_ CRasCRing n' x) (MVP_C_ CRasCRing n' x) H
(reflexivity (MVP_C_ CRasCRing n' x))))
end.
Fixpoint MVP_uc_fun_correct_sig_Q n : n_UniformlyContinuousFunction CR CR n -> n_Function CR CR n -> Prop :=
match n return n_UniformlyContinuousFunction CR CR n -> n_Function CR CR n -> Prop with
| O => fun a b => st_eq a b
| S n' => fun f g => forall x, (0 <= x)%Q -> (x <= 1)%Q -> MVP_uc_fun_correct_sig_Q n' (f ('x)%CR) (g ('x)%CR)
end.
Add Parametric Morphism n :
(@MVP_uc_fun_correct_sig_Q n) with signature (@st_eq _) ==> (@st_eq _) ==> iff as MVP_uc_fun_correct_sig_Q_wd.
Qed.
Lemma MVP_uc_fun_correct_Q : forall n (p:MultivariatePolynomial Q_as_CRing n),
MVP_uc_fun_correct_sig_Q n (MVP_uc_fun n p) (MVP_CR_apply n (MVP_map inject_Q_hom n p)).
Fixpoint MVP_uc_fun_close_sig n e : n_UniformlyContinuousFunction CR CR n -> n_Function CR CR n -> Prop :=
match n return n_UniformlyContinuousFunction CR CR n -> n_Function CR CR n -> Prop with
| O => fun a b => ball e a b
| S n' => fun f g => forall x, ('0 <= x)%CR -> (x <= '1)%CR -> MVP_uc_fun_close_sig n' e (f x) (g x)
end.
Add Parametric Morphism n :
(@MVP_uc_fun_close_sig n) with signature QposEq ==> (@st_eq _) ==> (@st_eq _) ==> iff as MVP_uc_fun_close_sig_wd.
Qed.
Lemma MVP_uc_fun_close_weaken : forall n (e1 e2:Qpos) f g, (e1 <= e2) ->
MVP_uc_fun_close_sig n e1 f g ->
MVP_uc_fun_close_sig n e2 f g.
Fixpoint n_Function_ball01 n e : n_Function CR CR n -> n_Function CR CR n -> Prop :=
match n return n_Function CR CR n -> n_Function CR CR n -> Prop with
| O => ball e
| S n' => fun f g => forall x, ('0 <= x)%CR -> (x <= '1)%CR -> n_Function_ball01 n' e (f x) (g x)
end.
Add Parametric Morphism n :
(@n_Function_ball01 n) with signature QposEq ==> (@st_eq _) ==> (@st_eq _) ==> iff as n_Function_ball01_wd.
Qed.
Lemma MVP_uc_fun_close_left : forall n (e1 e2:Qpos) f1 f2 g,
ball e1 f1 f2 ->
MVP_uc_fun_close_sig n e2 f2 g ->
MVP_uc_fun_close_sig n (e1+e2) f1 g.
Lemma MVP_uc_fun_close_right : forall n (e1 e2:Qpos) f g1 g2,
MVP_uc_fun_close_sig n e1 f g1 ->
n_Function_ball01 n e2 g1 g2 ->
MVP_uc_fun_close_sig n (e1+e2) f g2.
Lemma n_Function_ball01_sym : forall n e f g,
(n_Function_ball01 n e f g) ->
(n_Function_ball01 n e g f).
Lemma n_Function_ball01_triangle : forall n e1 e2 f g h,
(n_Function_ball01 n e1 f g) ->
(n_Function_ball01 n e2 g h) ->
(n_Function_ball01 n (e1+e2)%Qpos f h).
Lemma n_Function_ball01_plus : forall n e p1 p2 p3,
(n_Function_ball01 n e (MVP_CR_apply n p2) (MVP_CR_apply n p3)) ->
(n_Function_ball01 n e (MVP_CR_apply n (p1[+]p2)) (MVP_CR_apply n (p1[+]p3))).
Lemma n_Function_ball01_mult_C : forall n e c q1 q2,
('0 <= c)%CR -> (c <= '1)%CR ->
(n_Function_ball01 n e (MVP_CR_apply n q1) (MVP_CR_apply n q2)) ->
(n_Function_ball01 n e (MVP_CR_apply n ((MVP_C_ _ _ c)[*]q1))
(MVP_CR_apply n ((MVP_C_ _ _ c)[*]q2))).
Fixpoint MVP_is_Bound01 n (M:CR) : MultivariatePolynomial CRasCRing n -> Prop :=
match n return MultivariatePolynomial CRasCRing n -> Prop with
| O => fun a => AbsSmall M a
| S n' => fun p => forall x, ('0 <= x)%CR -> (x <= '1)%CR ->
MVP_is_Bound01 n' M (p ! (MVP_C_ _ _ x))
end.
Add Parametric Morphism n :
(@MVP_is_Bound01 n) with signature (@st_eq _) ==> (@st_eq _) ==> iff as MVP_is_Bound01_wd.
Lemma MVP_is_Bound01_plus : forall n M N p q,
MVP_is_Bound01 n M p -> MVP_is_Bound01 n N q ->
MVP_is_Bound01 n (M+N)%CR (p[+]q).
Lemma MVP_is_Bound01_mult01 : forall n M p x,
('0 <= x)%CR -> (x <= '1)%CR ->
MVP_is_Bound01 n M p ->
MVP_is_Bound01 n M (MVP_C_ _ n x[*]p).
Lemma n_Function_ball01_mult : forall n e x y p M,
MVP_is_Bound01 n ('M)%CR p ->
ball_ex (Qscale_modulus M e) x y ->
n_Function_ball01 n e
(MVP_CR_apply n (MVP_C_ CRasCRing n x[*]p))
(MVP_CR_apply n (MVP_C_ CRasCRing n y[*]p)).
Fixpoint MVP_poor_Bound01 n : MultivariatePolynomial Q_as_CRing n -> Q :=
match n return MultivariatePolynomial Q_as_CRing n -> Q with
| O => Qabs
| S n' => fix MVP_poor_Bound01_H p : Q :=
match p with
| cpoly_zero => 0
| cpoly_linear s p' => MVP_poor_Bound01 n' s + MVP_poor_Bound01_H p'
end
end.
Lemma MVP_poor_Bound01_zero : forall n, MVP_poor_Bound01 n (0)==0.
Add Parametric Morphism n :
(@MVP_poor_Bound01 n) with signature (@st_eq _) ==> Qeq as MVP_poor_Bound01_wd.
Qed.
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).
Lemma MVP_CR_apply_cont : forall n e (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 e (MVP_CR_apply _ (MVP_map inject_Q_hom _ p) x)
(MVP_CR_apply _ (MVP_map inject_Q_hom _ p) ('y)%CR)}.
Lemma MVP_uc_fun_close : forall n e (p:MultivariatePolynomial Q_as_CRing n),
MVP_uc_fun_close_sig n e (MVP_uc_fun n p) (MVP_CR_apply n (MVP_map inject_Q_hom n p)).
Fixpoint MVP_uc_fun_correct_sig n : n_UniformlyContinuousFunction CR CR n -> n_Function CR CR n -> Prop :=
match n return n_UniformlyContinuousFunction CR CR n -> n_Function CR CR n -> Prop with
| O => fun a b => a[=]b
| S n' => fun f g => forall x, ('0 <= x)%CR -> (x <= '1)%CR -> MVP_uc_fun_correct_sig n' (f x) (g x)
end.
0 <= x -> x <= 1 ->
(MVP_uc_fun (S n) p ('x)%CR)[=](MVP_uc_fun n (p!(MVP_C_ _ _ x))).
Fixpoint MVP_CR_apply n : extSetoid (MultivariatePolynomial CRasCRing n) (n_Function CR CR n) :=
match n return extSetoid (MultivariatePolynomial CRasCRing n) (n_Function CR CR n) with
| O => id
| S n' => Build_Morphism _ (n_Function CR CR (S n')) (fun p => Build_Morphism _ _ (fun x => MVP_CR_apply n' (p!(MVP_C_ _ n' x)))
(fun (x y : RegularFunction Q_as_MetricSpace) (Hxy : regFunEq x y) =>
Morphism_prf (MVP_CR_apply n') p ! (MVP_C_ CRasCRing n' x)
p ! (MVP_C_ CRasCRing n' y)
(cpoly_apply_wd (MultivariatePolynomial CRasCRing n') p p
(MVP_C_ CRasCRing n' x) (MVP_C_ CRasCRing n' y) (reflexivity p)
(csf_wd CRasCSetoid (MultivariatePolynomial CRasCRing n')
(MVP_C_ CRasCRing n') x y Hxy))))
(fun (x1 x2 : cpoly_cring (MultivariatePolynomial CRasCRing n'))
(H : x1[=]x2) (x : RegularFunction Q_as_MetricSpace) =>
Morphism_prf (MVP_CR_apply n') x1 ! (MVP_C_ CRasCRing n' x)
x2 ! (MVP_C_ CRasCRing n' x)
(cpoly_apply_wd (MultivariatePolynomial CRasCRing n') x1 x2
(MVP_C_ CRasCRing n' x) (MVP_C_ CRasCRing n' x) H
(reflexivity (MVP_C_ CRasCRing n' x))))
end.
Fixpoint MVP_uc_fun_correct_sig_Q n : n_UniformlyContinuousFunction CR CR n -> n_Function CR CR n -> Prop :=
match n return n_UniformlyContinuousFunction CR CR n -> n_Function CR CR n -> Prop with
| O => fun a b => st_eq a b
| S n' => fun f g => forall x, (0 <= x)%Q -> (x <= 1)%Q -> MVP_uc_fun_correct_sig_Q n' (f ('x)%CR) (g ('x)%CR)
end.
Add Parametric Morphism n :
(@MVP_uc_fun_correct_sig_Q n) with signature (@st_eq _) ==> (@st_eq _) ==> iff as MVP_uc_fun_correct_sig_Q_wd.
Qed.
Lemma MVP_uc_fun_correct_Q : forall n (p:MultivariatePolynomial Q_as_CRing n),
MVP_uc_fun_correct_sig_Q n (MVP_uc_fun n p) (MVP_CR_apply n (MVP_map inject_Q_hom n p)).
Fixpoint MVP_uc_fun_close_sig n e : n_UniformlyContinuousFunction CR CR n -> n_Function CR CR n -> Prop :=
match n return n_UniformlyContinuousFunction CR CR n -> n_Function CR CR n -> Prop with
| O => fun a b => ball e a b
| S n' => fun f g => forall x, ('0 <= x)%CR -> (x <= '1)%CR -> MVP_uc_fun_close_sig n' e (f x) (g x)
end.
Add Parametric Morphism n :
(@MVP_uc_fun_close_sig n) with signature QposEq ==> (@st_eq _) ==> (@st_eq _) ==> iff as MVP_uc_fun_close_sig_wd.
Qed.
Lemma MVP_uc_fun_close_weaken : forall n (e1 e2:Qpos) f g, (e1 <= e2) ->
MVP_uc_fun_close_sig n e1 f g ->
MVP_uc_fun_close_sig n e2 f g.
Fixpoint n_Function_ball01 n e : n_Function CR CR n -> n_Function CR CR n -> Prop :=
match n return n_Function CR CR n -> n_Function CR CR n -> Prop with
| O => ball e
| S n' => fun f g => forall x, ('0 <= x)%CR -> (x <= '1)%CR -> n_Function_ball01 n' e (f x) (g x)
end.
Add Parametric Morphism n :
(@n_Function_ball01 n) with signature QposEq ==> (@st_eq _) ==> (@st_eq _) ==> iff as n_Function_ball01_wd.
Qed.
Lemma MVP_uc_fun_close_left : forall n (e1 e2:Qpos) f1 f2 g,
ball e1 f1 f2 ->
MVP_uc_fun_close_sig n e2 f2 g ->
MVP_uc_fun_close_sig n (e1+e2) f1 g.
Lemma MVP_uc_fun_close_right : forall n (e1 e2:Qpos) f g1 g2,
MVP_uc_fun_close_sig n e1 f g1 ->
n_Function_ball01 n e2 g1 g2 ->
MVP_uc_fun_close_sig n (e1+e2) f g2.
Lemma n_Function_ball01_sym : forall n e f g,
(n_Function_ball01 n e f g) ->
(n_Function_ball01 n e g f).
Lemma n_Function_ball01_triangle : forall n e1 e2 f g h,
(n_Function_ball01 n e1 f g) ->
(n_Function_ball01 n e2 g h) ->
(n_Function_ball01 n (e1+e2)%Qpos f h).
Lemma n_Function_ball01_plus : forall n e p1 p2 p3,
(n_Function_ball01 n e (MVP_CR_apply n p2) (MVP_CR_apply n p3)) ->
(n_Function_ball01 n e (MVP_CR_apply n (p1[+]p2)) (MVP_CR_apply n (p1[+]p3))).
Lemma n_Function_ball01_mult_C : forall n e c q1 q2,
('0 <= c)%CR -> (c <= '1)%CR ->
(n_Function_ball01 n e (MVP_CR_apply n q1) (MVP_CR_apply n q2)) ->
(n_Function_ball01 n e (MVP_CR_apply n ((MVP_C_ _ _ c)[*]q1))
(MVP_CR_apply n ((MVP_C_ _ _ c)[*]q2))).
Fixpoint MVP_is_Bound01 n (M:CR) : MultivariatePolynomial CRasCRing n -> Prop :=
match n return MultivariatePolynomial CRasCRing n -> Prop with
| O => fun a => AbsSmall M a
| S n' => fun p => forall x, ('0 <= x)%CR -> (x <= '1)%CR ->
MVP_is_Bound01 n' M (p ! (MVP_C_ _ _ x))
end.
Add Parametric Morphism n :
(@MVP_is_Bound01 n) with signature (@st_eq _) ==> (@st_eq _) ==> iff as MVP_is_Bound01_wd.
Lemma MVP_is_Bound01_plus : forall n M N p q,
MVP_is_Bound01 n M p -> MVP_is_Bound01 n N q ->
MVP_is_Bound01 n (M+N)%CR (p[+]q).
Lemma MVP_is_Bound01_mult01 : forall n M p x,
('0 <= x)%CR -> (x <= '1)%CR ->
MVP_is_Bound01 n M p ->
MVP_is_Bound01 n M (MVP_C_ _ n x[*]p).
Lemma n_Function_ball01_mult : forall n e x y p M,
MVP_is_Bound01 n ('M)%CR p ->
ball_ex (Qscale_modulus M e) x y ->
n_Function_ball01 n e
(MVP_CR_apply n (MVP_C_ CRasCRing n x[*]p))
(MVP_CR_apply n (MVP_C_ CRasCRing n y[*]p)).
Fixpoint MVP_poor_Bound01 n : MultivariatePolynomial Q_as_CRing n -> Q :=
match n return MultivariatePolynomial Q_as_CRing n -> Q with
| O => Qabs
| S n' => fix MVP_poor_Bound01_H p : Q :=
match p with
| cpoly_zero => 0
| cpoly_linear s p' => MVP_poor_Bound01 n' s + MVP_poor_Bound01_H p'
end
end.
Lemma MVP_poor_Bound01_zero : forall n, MVP_poor_Bound01 n (0)==0.
Add Parametric Morphism n :
(@MVP_poor_Bound01 n) with signature (@st_eq _) ==> Qeq as MVP_poor_Bound01_wd.
Qed.
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).
Lemma MVP_CR_apply_cont : forall n e (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 e (MVP_CR_apply _ (MVP_map inject_Q_hom _ p) x)
(MVP_CR_apply _ (MVP_map inject_Q_hom _ p) ('y)%CR)}.
Lemma MVP_uc_fun_close : forall n e (p:MultivariatePolynomial Q_as_CRing n),
MVP_uc_fun_close_sig n e (MVP_uc_fun n p) (MVP_CR_apply n (MVP_map inject_Q_hom n p)).
Fixpoint MVP_uc_fun_correct_sig n : n_UniformlyContinuousFunction CR CR n -> n_Function CR CR n -> Prop :=
match n return n_UniformlyContinuousFunction CR CR n -> n_Function CR CR n -> Prop with
| O => fun a b => a[=]b
| S n' => fun f g => forall x, ('0 <= x)%CR -> (x <= '1)%CR -> MVP_uc_fun_correct_sig n' (f x) (g x)
end.
Finally, the correctness lemma.
Lemma MVP_uc_fun_correct : forall n (p:MultivariatePolynomial Q_as_CRing n),
MVP_uc_fun_correct_sig n (MVP_uc_fun n p) (MVP_CR_apply n (MVP_map inject_Q_hom n p)).
End MVP_correct.
MVP_uc_fun_correct_sig n (MVP_uc_fun n p) (MVP_CR_apply n (MVP_map inject_Q_hom n p)).
End MVP_correct.