From 1546986dab9e42e30cd912a02750760f56c3a625 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 18 Jul 2024 18:39:39 +0900 Subject: [PATCH 1/2] improve bounds --- robust/weightedmean.v | 56 +++++++++++++++++++++++++++++++++++++++---- 1 file changed, 52 insertions(+), 4 deletions(-) diff --git a/robust/weightedmean.v b/robust/weightedmean.v index 4338d8a0..57abe7b3 100644 --- a/robust/weightedmean.v +++ b/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. From 6d8b57273c25e358fc5782df9ca23a052805c4f4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 18 Jul 2024 19:13:50 +0900 Subject: [PATCH 2/2] more tests but failing --- robust/weightedmean.v | 40 +++++++++++++++++++++++++++------------- 1 file changed, 27 insertions(+), 13 deletions(-) diff --git a/robust/weightedmean.v b/robust/weightedmean.v index 57abe7b3..bfcd709f 100644 --- a/robust/weightedmean.v +++ b/robust/weightedmean.v @@ -471,11 +471,10 @@ End pos_evar. (*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 / 1253)%mcR. +Notation denom := (3317 / 1000)%mcR.*) -(* -Notation eps_max := (100%:R / 1253%:R)%mcR. +(*Notation eps_max := (100%:R / 1253%:R)%mcR. Notation denom := (3317%:R / 1000%:R)%mcR. Lemma eps_maxRE : eps_max = (100 / 1253)%coqR. @@ -486,7 +485,7 @@ Proof. by rewrite RdivE; congr (_ / _)%mcR; rewrite /= -INRE INR_IZR_INZ. Qed.*) -(*Notation eps_max := (100%:R / 1252%:R)%mcR. +Notation eps_max := (100%:R / 1252%:R)%mcR. Notation denom := (33178%:R / 10000%:R)%mcR. Lemma eps_maxRE : eps_max = (100 / 1252)%coqR. @@ -495,7 +494,7 @@ 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.*) +Qed. Section invariant. Local Open Scope ring_scope. @@ -898,17 +897,31 @@ rewrite (_ : 2 = 2%coqR); last by rewrite !IZRposE// -!coqRE. by rewrite (_ : 4 = 4%coqR)// !IZRposE// -!coqRE. Qed. +Lemma from_mcR_to_coqR_manually2 (e : R) : + (1 - 3 / 2 * e - + (1 - e) * + (16^-1 + 2 * e * ((4 * Num.sqrt (2 - e))^-1 + (Num.sqrt (1 - e))^-1) ^+ 2))%mcR = + (1 - 3 / 2 * e - + (1 - e) * + (/16 + 2 * e * (/(4 * sqrt (2 - 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. rewrite /bound_evar_ineq/bound_intermediate; apply/RleP. -(* this works for small constants:*) +(* this works for small constants: rewrite -!coqRE. rewrite -!RsqrtE'. - interval. -(* this works for large constants: + interval.*) +(* this works for large constants:*) rewrite from_mcR_to_coqR_manually eps_maxRE denomRE. rewrite -[in X in (_ <= X)%coqR]coqRE. -interval.*) +interval. Qed. (**md ## lemma 1.4, page 5 (part 2) *) @@ -950,10 +963,11 @@ have ->// : 2 / denom * `V (WP.-RV X) <= `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 : +(*rewrite -!coqRE -!RsqrtE' => ? ?.*) +(* doesn't work yet :*) +rewrite from_mcR_to_coqR_manually2 denomRE eps_maxRE. move=> ? ?. -rewrite from_mcR_to_coqR_manually denomRE.*) +rewrite -![in X in (X <= _)%coqR]coqRE. interval with (i_prec 20, i_bisect eps). Qed.