proposition: Lemma MVP_upperBound_correct : forall n p v, UnitHyperInterval v -> MVP_apply _ p v[<=]MVP_upperBound n p.
proof: Proof. induction n; intros p v H. apply Qle_refl. revert p H. dependent inversion v as [|a n0 v0]. clear H. intros p [[Ha0 Ha1] Hv]. stepl (@MVP_apply Q_as_CRing (S n) (let (n0, b) := BernsteinCoefficents (MVP_C_ Q_as_CRing n) p in evalBernsteinBasis (MultivariatePolynomial Q_as_CRing n) b) (@Vector.cons Q a n v0)); [|apply MVP_apply_wd;[apply evalBernsteinCoefficents|reflexivity]]. simpl (MVP_upperBound (S n) p). destruct (BernsteinCoefficents (MVP_C_ Q_as_CRing n) p) as [m b]. apply Qle_trans with (Vector.t_rec (MultivariatePolynomial Q_as_CRing n) (fun (n1 : nat) (_ : Vector.t (MultivariatePolynomial Q_as_CRing n) n1) => Q) 0 (fun (c : MultivariatePolynomial Q_as_CRing n) (n1 : nat) (_ : Vector.t (MultivariatePolynomial Q_as_CRing n) n1) (rec : Q) => Qmax (MVP_apply _ c v0) rec) m b). clear IHn Hv. destruct m as [|m]. rewrite (V0_eq b). unfold evalBernsteinBasis. simpl. rewrite -> zero_MVP_apply. apply Qle_refl. unfold evalBernsteinBasis. match goal with |- (?A <= ?B) => set (L:=A); set (R:=B) end. change (L[<=]R). rstepr (R[*][1]). rewrite <- (@one_MVP_apply Q_as_CRing _ (Vector.cons _ a _ v0)). stepr (R[*](@MVP_apply Q_as_CRing (S n) (@Sumx (cpoly_cring _) _ (fun i H => Bernstein _ (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans _ _ _ H (Nat.le_refl _))))) (Vector.cons _ a _ v0))). fold (MultivariatePolynomial Q_as_CRing n). unfold L, R; clear L R. generalize (Nat.le_refl (S m)). revert b. generalize (S m) at 1 2 5 6 7 8 11. induction b as [| a0]; intros l. simpl. rewrite -> zero_MVP_apply. apply Qle_refl. simpl (Vector.t_rec (MultivariatePolynomial Q_as_CRing n) (fun (n2 : nat) (_ : Vector.t (MultivariatePolynomial Q_as_CRing n) n2) => Q) 0 (fun (c : MultivariatePolynomial Q_as_CRing n) (n2 : nat) (_ : Vector.t (MultivariatePolynomial Q_as_CRing n) n2) (rec : Q) => Qmax (MVP_apply Q_as_CRing c v0) rec) (S n1) (Vector.cons _ a0 _ b)). simpl (evalBernsteinBasisH (MultivariatePolynomial Q_as_CRing n) (Vector.cons (MultivariatePolynomial Q_as_CRing n) a0 n1 b) l). simpl (Sumx (fun (i : nat) (H : (i < S n1)%nat) => Bernstein (MultivariatePolynomial Q_as_CRing n) (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) H l)))). do 2 rewrite -> MVP_plus_apply. rewrite -> (Qplus_comm (@MVP_apply Q_as_CRing (S n) (Sumx (fun (i : nat) (l0 : (i < n1)%nat) => Bernstein (MultivariatePolynomial Q_as_CRing n) (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) (Nat.lt_lt_succ_r i n1 l0) l)))) (Vector.cons Q a n v0))). rewrite -> Qmult_comm. rewrite -> Qmult_plus_distr_l. apply Qplus_le_compat; rewrite -> Qmult_comm; rewrite -> Qmax_mult_pos_distr_l. replace LHS with (MVP_apply Q_as_CRing a0 v0 * @MVP_apply Q_as_CRing (S n) (Bernstein (MultivariatePolynomial Q_as_CRing n) (proj1 (Nat.lt_succ_r n1 m) (Nat.lt_le_trans n1 (S n1) (S m) (Nat.lt_succ_diag_r n1) l))) (Vector.cons _ a _ v0)). apply Qmax_ub_l. simpl. rewrite <- (MVP_mult_apply Q_as_CRing). apply: MVP_apply_wd; try reflexivity. replace (proj1 (Nat.lt_succ_r n1 m) (Nat.lt_le_trans n1 (S n1) (S m) (Nat.lt_succ_diag_r n1) l)) with (proj2 (Nat.succ_le_mono n1 m) l) by apply le_irrelevent. replace (le_S_n n1 m l) with (proj2 (Nat.succ_le_mono n1 m) l) by apply le_irrelevent. apply c_mult_apply. apply MVP_BernsteinNonNeg; auto. eapply Qle_trans;[|apply Qmax_ub_r]. set (R:=Vector.t_rec (MultivariatePolynomial Q_as_CRing n) (fun (n2 : nat) (_ : Vector.t (MultivariatePolynomial Q_as_CRing n) n2) => Q) 0 (fun (c : MultivariatePolynomial Q_as_CRing n) (n2 : nat) (_ : Vector.t (MultivariatePolynomial Q_as_CRing n) n2) (rec : Q) => Qmax (MVP_apply Q_as_CRing c v0) rec) n1 b) in *. replace RHS with (R*@MVP_apply Q_as_CRing (S n) (Sumx (fun (i : nat) (l0 : (i < n1)%nat) => Bernstein (MultivariatePolynomial Q_as_CRing n) (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i n1 (S m) l0 (Nat.lt_le_incl _ _ l))))) (Vector.cons _ a _ v0)). apply IHb. apply: mult_wdr. apply MVP_apply_wd; try reflexivity. apply Sumx_wd. intros i H. replace (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) (Nat.lt_lt_succ_r i n1 H) l)) with (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i n1 (S m) H (Nat.lt_le_incl n1 (S m) l))) by apply le_irrelevent. reflexivity. clear - Ha0 Ha1. induction n1. rewrite -> zero_MVP_apply. auto with *. simpl (Sumx (fun (i : nat) (l0 : (i < S n1)%nat) => Bernstein (MultivariatePolynomial Q_as_CRing n) (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S (S n1)) (S m) (Nat.lt_lt_succ_r i (S n1) l0) l)))). rewrite -> MVP_plus_apply. apply: plus_resp_nonneg. stepr (@MVP_apply Q_as_CRing (S n) (Sumx (fun (i : nat) (l0 : (i < n1)%nat) => Bernstein (MultivariatePolynomial Q_as_CRing n) (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) (Nat.lt_lt_succ_r i n1 l0) (Nat.lt_le_incl _ _ l))))) (Vector.cons _ a _ v0)). apply IHn1. apply MVP_apply_wd; try reflexivity. apply Sumx_wd. intros i H. replace (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S n1) (S m) (Nat.lt_lt_succ_r i n1 H) (Nat.lt_le_incl (S n1) (S m) l))) with (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S (S n1)) (S m) (Nat.lt_lt_succ_r i (S n1) (Nat.lt_lt_succ_r i n1 H)) l)) by apply le_irrelevent. reflexivity. apply MVP_BernsteinNonNeg; auto with *. apply mult_wdr. apply MVP_apply_wd; try reflexivity. simpl (MultivariatePolynomial Q_as_CRing (S n)). rewrite <- (fun X => partitionOfUnity X m). apply Sumx_wd. intros i H. replace (proj1 (Nat.lt_succ_r i m) (Nat.lt_le_trans i (S m) (S m) H (Nat.le_refl (S m)))) with (proj1 (Nat.lt_succ_r i m) H) by apply le_irrelevent. reflexivity. clear - IHn Hv. induction b. auto with *. apply Qmax_le_compat. apply IHn; apply Hv. auto. 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