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

Section Schwartz.

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

Variable R : RING.

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

Definition C:=Carrier R.
Variable Call:CALL C.


Definition OR:= Monoid_cat.monoid_unit R.

Variable Fins2C:(Sec->C)->listT C.


Axiom dec_eq:forall a b:C,{Equal (s:=R) a b}+{~(Equal (s:=R) a b)}.

Lemma dec_eqR:forall (n:nat)(a:C)( p:Poly n Call),dec_pred (Sec->C) (fun f:Sec->C=>Equal (s:=R) (eval_poly p (Fins2C f)) a).
unfold dec_pred.
simpl;intros.
apply dec_eq.
Qed.

Require Import R_lemma.

Definition Ev_eq_pol0(n:nat)( p:Poly n Call):=Build_Event _ (fun f:Sec->C=>Equal  (eval_poly p (Fins2C f)) OR) (dec_eqR n OR p) .


Axiom Schwartz:forall (E_Var:listT (Sec->C))(p:Poly n Call),(0<INR q)%R->
lengthT E_Var<>0->~(eq_pol p (pol_null n Call))->
               (prob _ E_Var (Ev_eq_pol0 n p)<=INR (degre C Call n p)/INR q)%R.




Lemma dec_eq_nat:forall (p:Poly n Call),
dec_pred _ (fun f:(Sec->C)=> degre C Call n p=0).
unfold dec_pred.
simpl;intros.
apply eq_nat_dec.
Qed.

Definition Ev_deg0(p:Poly n Call):=
Build_Event _ (fun f: (Sec->C)=>degre C Call n p=0) (dec_eq_nat p).



Set Implicit Arguments.
Unset Strict Implicit.

(* Pr(p=0/\deg p=0)<=Pr(cte=0)=1/q
deg p=0 => p=cte  *)
Axiom pr_inter_pol_deg0:forall (E_Var:listT (Sec->C))(p:Poly n Call),
(prob _ E_Var (EventInter _ (Ev_eq_pol0 n p) (Ev_deg0 p))<=1/INR q)%R.


Lemma deg0_prob0:forall (E_Var:listT (Sec->C))(p:Poly n Call),
degre C Call n p=0->(Proba _ E_Var
      (EventInter _ (Ev_eq_pol0 n p) (Eventdiff _ (Ev_deg0 p))))=0.
unfold Proba.
intros.
elim E_Var.
simpl;intros;auto.
simpl;intros.
case (event_inter_aux (Sec -> C) (Ev_eq_pol0 n p)
           (Eventdiff (Sec -> C) (Ev_deg0 p)) a).
simpl;intros;intuition.
simpl;intros;auto.
Qed.

Variable E_Var:listT (Sec->C).
Hypotheses lgt_EVar:(0 < INR (lengthT E_Var))%R.
Lemma lgt_E_Var:(lengthT E_Var)<>0.
generalize lgt_EVar;elim E_Var.
simpl;intros.
absurd (0 < 0)%R;auto with * .
simpl;intros;auto with * .
Qed.


Lemma pr_inter_pol_not_deg0:forall (p:Poly n Call),
(prob _ E_Var (EventInter _ (Ev_eq_pol0  n p) (Eventdiff _ (Ev_deg0 p)))<=INR (degre C Call n p)/INR q)%R.
intros.
case (dec_eq_pol p (pol_null n Call)).
intro.
assert (degre C Call n p=0).
apply (eq_pol_deg0 e);auto.
unfold prob.
rewrite deg0_prob0.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l.
apply Rle_0.
auto with * .
apply Q.
auto with * .
intros.
apply Rle_trans with (prob _ E_Var (Ev_eq_pol0 n p)).
unfold prob.
apply Rle_div.
apply le_inter.
apply lgt_EVar.
apply (Schwartz  E_Var p Q );auto.
apply lgt_E_Var.
Qed.



Lemma Schwartz_ext:forall (p:Poly n Call),
             (prob _ E_Var (Ev_eq_pol0  n p)<=(INR (degre C Call n p) + 1)/INR q)%R.
intros.
unfold prob.
rewrite Prob_plus_op with (B:=(Ev_deg0 p)).
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_plus_distr_r.
rewrite plus_INR.
rewrite Rmult_plus_distr_r.
rewrite <-Rdiv_Rmult.
rewrite <-Rdiv_Rmult.
rewrite <-Rdiv_Rmult.
apply Rplus_le_compat.
generalize (pr_inter_pol_not_deg0   p);unfold prob;intro h;apply h.
apply (pr_inter_pol_deg0 E_Var p).
Qed.

End Schwartz.