proposition: Lemma magnify_conv (T : isConvexSpace_.ConvexSpace.Exports.convType) (p q r : {prob real_realType}) (x y : T) (H : Prob.p p < Prob.p q < Prob.p r) : (x <|p|> y) <| magnified_weight H |> (x <|r|> y) = x <|q|> y.
proof: Proof. case: (H) => pq qr. have rp : 0 < Prob.p r - Prob.p p by rewrite subR_gt0; apply (ltR_trans pq). have rp' : Prob.p r - Prob.p p != 0 by apply/gtR_eqF. apply: S1_inj; rewrite ![in LHS]affine_conv/= !convptE. rewrite !scaleptDr !scaleptA // (addptC ((Prob.p (m (conj pq qr)) * Prob.p p) *' S1 x)) addptA. rewrite addptC !addptA -scaleptDl//; last first. by apply: mulR_ge0. by apply: mulR_ge0. rewrite -!addptA -scaleptDl//; last first. by apply: mulR_ge0. by apply: mulR_ge0. rewrite (_ : conj pq qr = H)//. have -> : ((Prob.p (m H)).~ * (Prob.p r).~ + Prob.p (m H) * (Prob.p p).~ = (Prob.p (m H) * Prob.p p + (Prob.p (m H)).~ * Prob.p r).~)%coqR. rewrite /onem. rewrite -!RminusE. rewrite -R1E. rewrite -RplusE -2!RmultE. ring. pose tmp := (Prob.p (m H) * Prob.p p + (Prob.p (m H)).~ * Prob.p r). rewrite -[X in X.~ *' _ +' _]/tmp. rewrite -/tmp. suff -> : tmp = Prob.p q. by rewrite affine_conv convptE addptC. rewrite /tmp /m /= /onem. rewrite mulRDl mul1R addRCA -Rmult_opp_opp -mulRDr (addRC (- Prob.p p)) addR_opp. rewrite mulNR mulRAC -mulRA. rewrite !RmultE. rewrite mulrV // mulr1. rewrite -RminusE. ring. Qed.
imports: HB(structures) Reals Lra mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals mathcomp_extra Rstruct lra) infotheo(ssrR realType_ext Reals_ext) infotheo(proba convex necset) monae_lib hierarchy monad_lib fail_lib infotheo(fdist) mathcomp(reals Rstruct) infotheo(Reals_ext)