Hi all,

I am a beginner and have a question related to solving the goal when comparing sums of reals. We are using infotheo and inside a proof need this assertion.

assert (

let x := mknonnegreal (`E ((X `

-cst `E X) `

^2 `* Ind (A:=U) F: {RV P -> R}) * `

E (Ind (A:=U) F:{RV P -> R})) H2 in

`| `

E ((X `-cst `

E X) `* Ind (A:=U) F: {RV P -> R})| / Pr P F <=

sqrt (x) / Pr P F).

During the proof:

- unfold Rdiv.

Search (?x * ?y <= ?z * ?y).

apply Rmult_le_compat_r.

apply Rlt_le.

Search (0 < / ?x).

apply invR_gt0.

lra.

rewrite <- sqrt_Rsqr_abs.

apply sqrt_le_1_alt.

unfold "`^2". simpl. unfold "`

o".

unfold "`E".

unfold ambient_dist.

rewrite big_distrr.

We hit a goal with a comparison of 2 sums:

delta: R

X: {RV (P) -> (R)}

F: {set U}

H: 0 < delta

H0: delta <= Pr P F

H1: `|`

E_[X | F] - ```
E X| =
```

|`E ((X `

-cst `E X) `

* Ind (A:=U) F : {RV (P) -> (R)})| / Pr P F

H2: 0 <=

`E (((X `

-cst `E X) `

^2) ```
* Ind (A:=U) F : {RV (P) -> (R)}) *
```

E (Ind (A:=U) F : {RV (P) -> (R)})

===

(1/2)

(\sum_(u in U) (X ```
-cst \sum_(u0 in U) X u0 * P u0) u * Ind (A:=U) F u * P u)² <=
\big[Radd_add_law/0]_(i in U)
Rmul_mul_law
(\sum_(u in U)
(X
```

-cst \sum_(u0 in U) X u0 * P u0) u *
((X `-cst \sum_(u0 in U) X u0 * P u0) u * 1) *

Ind (A:=U) F u * P u) (Ind (A:=U) F i * P i)

The idea was to use Lemma leq_sum from bigop.v, modified to fit Real numbers.

Lemma leq_sumR I r (P : pred I) (E1 E2 : I -> R) :

(forall i, P i -> E1 i <= E2 i) ->

\sum_(i <- r | P i) E1 i <= \sum_(i <- r | P i) E2 i.

Proof. move=> leE12. elim/big_ind2: _ => // m1 m2 n1 n2. lra. Qed.

But it ends with an 'Unable to unify' error.

Any tips on how to proceed would be very valuable.

@Reynald Affeldt ?

Hi @Ieva Daukantas . Would you have a self-contained proof script that I can copy-paste for inspection? (I am wondering whether ``*`

is a notation of your own.)

Hi, thank you for the help. It was solved by rewriting previous asserts as there were mistakes.

Last updated: Sep 23 2023 at 08:01 UTC