proposition: Lemma __admitted__exp_dlet mu (nu : T -> {distr U / R}) F : (forall eta, \E?_[eta] F) -> \E_[dlet nu mu] F = \E_[mu] (fun x => \E_[nu x] F).
proof: Proof. Proof using Type*. Admitted. End PrTheory. #[deprecated(since="mathcomp-analysis 0.6.2", note="relies on admitted, use __deprecated__pr_dlet explicitly if you really want to use this lemma")] Notation pr_dlet := __deprecated__pr_dlet. #[deprecated(since="mathcomp-analysis 0.6.2", note="lacks proof, use __admitted__exp_split explicitly if you really want to use this lemma")] Notation exp_split := __admitted__exp_split. #[deprecated(since="mathcomp-analysis 0.6.2", note="lacks proof, use __admitted__exp_dlet explicitly is you really want to use this lemma")] Notation exp_dlet := __admitted__exp_dlet. Section Jensen. Context {R : realType} {I : finType}. Definition convexon (a b : \bar R) (f : R -> R) := forall x y, (a <= x%:E <= b)%E -> (a <= y%:E <= b)%E -> forall t, 0 <= t <= 1 -> f (t * x + (1 - t) * y) <= t * (f x) + (1 - t) * (f y). Notation convex f := (convexon -oo +oo f). Section Jensen. Context (f : R -> R) (x l : I -> R). Hypothesis cvx_f : convex f. Hypothesis ge0_l : forall x, 0 <= l x. Hypothesis eq1_l : \sum_i (l i) = 1. Lemma Jensen : f (\sum_i (l i * x i)) <= \sum_i (l i * f (x i)). Proof. case: (index_enum I) eq1_l => [|i s]; rewrite ?(big_nil, big_cons). by move/esym/eqP; rewrite oner_eq0. elim: {i} s (l i) (ge0_l i) (x i) => [|j s ih] li ge0_li xi. by rewrite !big_nil !addr0 => ->; rewrite !mul1r. rewrite !big_cons; have := ge0_l j; rewrite le_eqVlt. case/orP => [/eqP<-|gt0_lj]. by rewrite !Monoid.simpm /= !Monoid.simpm; apply/ih. rewrite !addrA => eq1; pose z := (li * xi + l j * x j) / (li + l j). have nz_lij: li + l j != 0 by rewrite gt_eqF ?ltr_wpDl. have/ih := eq1 => -/(_ _ z); rewrite [_ * (_ / _)]mulrC. rewrite mulfVK // => {}ih; apply/(le_trans (ih _)). by rewrite addr_ge0 ?ge0_l. rewrite lerD2r {ih}/z [_ / _]mulrDl ![_*_/_]mulrAC. set c1 : R := _ / _; set c2 : R := _ / _; have eqc2: c2 = 1 - c1. apply/(mulfI nz_lij); rewrite mulrBr mulr1 ![(li + l j)*_]mulrC. by apply/eqP; rewrite !mulfVK // eq_sym subr_eq addrC. set c := (li + l j); pose z := (c * c1 * f xi + c * c2 * f (x j)). apply/(@le_trans _ _ z); last by rewrite /z ![_*(_/_)]mulrC !mulfVK. rewrite {}/z -![c * _ * _]mulrA -mulrDr ler_wpM2l ?addr_ge0 //. rewrite eqc2 cvx_f // ?leNye ?leey // divr_ge0 ?addr_ge0 //=. by rewrite ler_pdivrMr ?mul1r ?lerDl ?ltr_wpDl. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum