proposition: Lemma convexf_ptP : (forall x, a <= x <= b -> 0 <= L x - f x)%coqR -> forall t : {prob R}, convex_function_at f a b t.
proof: Proof. move=> H t; rewrite /convex_function_at. set x := (Prob.p t * a + (Prob.p t).~ * b)%coqR. have : (a <= x <= b)%coqR. rewrite /x; split. - apply (@leR_trans (Prob.p t * a + (Prob.p t).~ * a)). rewrite -mulRDl addRCA addR_opp subRR addR0 mul1R. by apply/RleP; rewrite lexx. have [->|t1] := eqVneq t 1%:pr. by rewrite mul1R onem1 2!mul0R; exact/RleP. rewrite leR_add2l; apply leR_wpmul2l => //; exact/ltRW. - apply (@leR_trans (Prob.p t * b + (Prob.p t).~ * b)); last first. rewrite -mulRDl addRCA addR_opp subRR addR0 mul1R. by apply/RleP; rewrite lexx. rewrite leR_add2r; apply leR_wpmul2l => //; exact/ltRW. move/H; rewrite subR_ge0 => /leR_trans; apply. rewrite LE //. have -> : ((b - x) / (b - a) = Prob.p t)%coqR. rewrite /x -addR_opp oppRD addRCA mulRBl mul1R oppRB (addRCA b). rewrite addR_opp subRR addR0 -mulRN addRC -mulRDr addR_opp. rewrite /Rdiv -mulRA mulRV ?mulR1 // subR_eq0'; exact/gtR_eqF. have -> : ((x - a) / (b - a) = (Prob.p t).~)%coqR. rewrite /x -addR_opp addRAC -{1}(oppRK a) mulRN -mulNR -{2}(mul1R (- a)%coqR). rewrite -mulRDl (addRC _ R1) addR_opp -mulRDr addRC addR_opp. rewrite /Rdiv -mulRA mulRV ?mulR1 // subR_eq0'; exact/gtR_eqF. by apply/RleP; rewrite lexx. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist