proposition: Lemma expectation_le (X Y : T -> R) : measurable_fun [set: T] X -> measurable_fun [set: T] Y -> (forall x, 0 <= X x)%R -> (forall x, 0 <= Y x)%R -> {ae P, (forall x, X x <= Y x)%R} -> 'E_P[X] <= 'E_P[Y].
proof: Proof. move=> mX mY X0 Y0 XY; rewrite unlock ae_ge0_le_integral => //. - by move=> t _; apply: X0. - exact/EFin_measurable_fun. - by move=> t _; apply: Y0. - exact/EFin_measurable_fun. - move: XY => [N [mN PN XYN]]; exists N; split => // t /= h. by apply: XYN => /=; apply: contra_not h; rewrite lee_fin. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) HB(structures) exp numfun lebesgue_measure lebesgue_integral reals ereal signed topology normedtype sequences esum measure exp numfun lebesgue_measure lebesgue_integral