Require Import Reals.
Require Import listT.
Require Import prob.
Require Import R_lemma.
Require Import Schwartz_Pol2Expr.
Require Import Ring_cat.
Require Import Pol_is_ring.
Require Import POLY_ax.

Section Schwartz_ext.

Variable Sec:Set.
(*n=card Sec*)
Variable n:nat.

Variable Zq_ring : RING.

(* card R=q *)
Variable q:nat.
Hypotheses Q: (0 < INR q)%R.

Definition Zq:=(Zq Zq_ring).
Variable Call:CALL Zq.

Variable  Expr:Set->Type.
Variable transl:Expr Sec -> Poly n Call.
Variable Fins2list : (Sec ->  Zq) ->  listT Zq.

Variable Ef:listT (Sec->Zq).
Hypotheses length_Ef:lengthT Ef<>0.

Definition pr := prob (Sec ->  Zq) Ef.
 
Definition pr_cond := PrCondList (Sec ->  Zq) Ef.
 
Hypotheses dec_Evalstozero:
 forall (e : Expr Sec) (x : Sec ->  Zq),
  ({ Evalstozero transl Fins2list x e }) + ({ ~ Evalstozero transl Fins2list x e }).

Lemma pr_cond_eval0:
 forall (p : Expr Sec) (ps : listT (Expr Sec)),
 (SumList (mapT pr (mapT (Ev_Evalstozero dec_Evalstozero ) ps)) < 1)%R ->
  (pr_cond ((Ev_Evalstozero dec_Evalstozero) p) (mapT (Ev_Evalstozero dec_Evalstozero) ps) <=
   pr ((Ev_Evalstozero dec_Evalstozero) p) / (1 - SumList (mapT pr (mapT (Ev_Evalstozero dec_Evalstozero) ps))))%R.
intros.
unfold pr; unfold pr_cond.
apply PrCondList_sum.
apply length_Ef.
apply H.
Qed.
Require Import Raxioms.
 

(* schwartz 's lemma:
  for a polynomial p 
  Pr(p(x1,...,xn)=0)<=degre p / card X  where x1,..,xn belong to X and p is non identically null *)
Hypotheses schwartz_:
   forall (p:Poly n Call),
~(eq_pol p (pol_null n Call))->
               (prob _ Ef (Ev_eq_pol0 Fins2list  p)<=INR (degre  p)/INR q)%R. 

Lemma le_Sumlist:
 forall (ps : listT (Expr Sec)) (d : nat) ,
 ListPred (Exprnon0 transl Fins2list) ps ->
 ListPred (fun p => (degre_Expr transl) p <= d) ps ->
  (SumList (mapT pr (mapT (Ev_Evalstozero dec_Evalstozero) ps)) <=
   INR (lengthT ps * d)%nat / INR q)%R.
intros ps d.
induction ps as [|a ps Hrecps].
simpl.
intros.
apply RIneq.Req_le.
unfold Rdiv.
symmetry.
apply RIneq.Rmult_0_l.
simpl.
intros.
assert
 ((INR (d + lengthT ps * d)%nat / INR q)%R =
  (INR d / INR q + INR (lengthT ps * d)%nat / INR q)%R).
apply plus_Rplus_div.
rewrite H1.
apply Rplus_le2.
apply RIneq.Rle_trans with ( r2 := (INR ((degre_Expr transl) a) / INR q)%R ).
unfold pr;unfold Zq.
apply schwartz.
apply schwartz_.
intuition.
apply Rle_inv_monotony_r.
apply Q.
apply RIneq.le_INR.
intuition.
apply (Hrecps).
intuition.
intuition.
Qed.
(* an extensionality of schwartz's lemma:
  for all poly p and list of poly ps
  if p<>0, exists q in ps, s.t,q<>0, deg p<=d and 
  for all q in ps deg q<=d then
  Pr(p=0|ps=0)<=d/(q-(length ps)*d   *)
 
Lemma SchwartzExt:
 forall (p : Expr Sec) (ps : listT (Expr Sec)) (d : nat),
 (Exprnon0 transl Fins2list) p ->
 ListPred (Exprnon0 transl Fins2list) ps ->
 (degre_Expr transl) p <= d ->
 ListPred (fun p => (degre_Expr transl) p <= d) ps ->
 (INR (lengthT ps * d)%nat / INR q < 1)%R ->
  (pr_cond ((Ev_Evalstozero dec_Evalstozero) p) (mapT (Ev_Evalstozero dec_Evalstozero) ps) <=
   INR d / (INR q - INR (lengthT ps * d)%nat))%R.
intros.
apply RIneq.Rle_trans
     with
      ( r2 :=
      (pr ((Ev_Evalstozero dec_Evalstozero) p) / (1 - SumList (mapT pr (mapT (Ev_Evalstozero dec_Evalstozero) ps))))%R
      ).
apply pr_cond_eval0.
apply RIneq.Rle_lt_trans with ( r2 := (INR (lengthT ps * d)%nat / INR q)%R ).
apply (le_Sumlist ps d ).
apply H0.
apply H2.
apply H3.
assert (pr ((Ev_Evalstozero dec_Evalstozero) p) <= INR d / INR q)%R.
apply RIneq.Rle_trans with ( r2 := (INR ((degre_Expr transl) p) / INR q)%R ).
unfold pr;unfold Zq.
apply schwartz.
apply schwartz_.
apply H.
apply Rle_inv_monotony_r.
apply Q.
apply RIneq.le_INR.
apply H1.
apply RIneq.Rle_trans
     with
      ( r2 :=
      ((INR d / INR q) / (1 - SumList (mapT pr (mapT (Ev_Evalstozero dec_Evalstozero) ps))))%R ).
apply Rle_inv_monotony_r.
apply Rlt_minus_r.
apply RIneq.Rle_lt_trans with ( r2 := (INR (lengthT ps * d)%nat / INR q)%R ).
apply (le_Sumlist ps d ).
apply H0.
apply H2.
apply H3.
apply H4.
apply RIneq.Rle_trans
     with ( r2 := ((INR d / INR q) / (1 - INR (lengthT ps * d)%nat / INR q))%R ).
apply Rle_inv_monotony.
apply Rlt_minus_r.
apply H3.
apply Rle_Ropp1_compatibility.
apply (le_Sumlist ps d ).
apply H0.
apply H2.
apply Rle_lt_inv.
apply RIneq.pos_INR.
apply Q.
apply RIneq.Req_le.
apply lem16.
assert (0 < INR q)%R.
apply Q.
auto with real.
assert (INR (lengthT ps * d)%nat < INR q)%R.
apply Rlt_monotony_contra1.
apply Q.
exact H3.
assert (0 < INR q)%R.
apply Q.
generalize H6.
auto with real.
Qed.

End Schwartz_ext.