improve bounds

robust/weightedmean.v

@@ -468,8 +468,34 @@ Qed.
 
 End pos_evar.
 
-Notation eps_max := (10 / 126)%mcR.
-Notation denom := ((3 / 10)^-1)%mcR.
+(*Notation eps_max := (10 / 126)%mcR.*)
+(*Notation denom := ((3 / 10)^-1)%mcR.*)
+
+Notation eps_max := (100 / 1253)%mcR.
+Notation denom := (3317 / 1000)%mcR.
+
+(*
+Notation eps_max := (100%:R / 1253%:R)%mcR.
+Notation denom := (3317%:R / 1000%:R)%mcR.
+
+Lemma eps_maxRE : eps_max = (100 / 1253)%coqR.
+Proof. by rewrite RdivE; congr (_ / _)%mcR; rewrite /= -INRE INR_IZR_INZ. Qed.
+
+Lemma denomRE : denom = (3317 / 1000)%coqR.
+Proof.
+by rewrite RdivE; congr (_ / _)%mcR; rewrite /= -INRE INR_IZR_INZ.
+Qed.*)
+
+(*Notation eps_max := (100%:R / 1252%:R)%mcR.
+Notation denom := (33178%:R / 10000%:R)%mcR.
+
+Lemma eps_maxRE : eps_max = (100 / 1252)%coqR.
+Proof. by rewrite RdivE; congr (_ / _)%mcR; rewrite /= -INRE INR_IZR_INZ. Qed.
+
+Lemma denomRE : denom = (33178 / 10000)%coqR.
+Proof.
+by rewrite RdivE; congr (_ / _)%mcR; rewrite /= -INRE -common.uint_N_nat INR_IPR.
+Qed.*)
 
 Section invariant.
 Local Open Scope ring_scope.
@@ -862,9 +888,28 @@ Let eps_max01 : (0 < eps_max < 1 :> R). Proof. lra. Qed.
 
 Hypothesis low_eps : eps <= eps_max.
 
-(* TODO: "interval" in the identifier? *)
+Lemma from_mcR_to_coqR_manually (e : R) :
+  16^-1 + 2 * e * ((4 * Num.sqrt (2 - e))^-1 + (Num.sqrt (1 - e))^-1) ^+ 2 =
+  (/ 16%:R + 2%:R * e * (/ (4%:R * sqrt (2%:R - e)) + / sqrt (1 - e)) ^ 2)%coqR.
+Proof.
+rewrite !coqRE !RsqrtE'.
+rewrite (_ : 16 = 16%coqR); last by rewrite !IZRposE// -!coqRE.
+rewrite (_ : 2 = 2%coqR); last by rewrite !IZRposE// -!coqRE.
+by rewrite (_ : 4 = 4%coqR)// !IZRposE// -!coqRE.
+Qed.
+
 Lemma bound_evar_ineq_by_interval : bound_evar_ineq eps_max.
-Proof. by rewrite /bound_evar_ineq/bound_intermediate; apply/RleP; rewrite -!coqRE -!RsqrtE'; interval. Qed.
+Proof.
+rewrite /bound_evar_ineq/bound_intermediate; apply/RleP.
+(* this works for small constants:*)
+  rewrite -!coqRE.
+  rewrite -!RsqrtE'.
+  interval.
+(* this works for large constants:
+rewrite from_mcR_to_coqR_manually eps_maxRE denomRE.
+rewrite -[in X in (_ <= X)%coqR]coqRE.
+interval.*)
+Qed.
 
 (**md ## lemma 1.4, page 5 (part 2) *)
 (**md ## eqn A.6--A.9, page 63 *)
@@ -906,6 +951,9 @@ have ->// :  2 / denom * `V (WP.-RV X) <=
 rewrite ler_wpM2r // ?variance_ge0' // /bound_intermediate.
 apply/RleP. move: low_eps => /RleP. move: eps0 => /RleP.
 rewrite -!coqRE -!RsqrtE' => ? ?.
+(* doesn't work yet :
+move=> ? ?.
+rewrite from_mcR_to_coqR_manually denomRE.*)
 interval with (i_prec 20, i_bisect eps).
 Qed.