proposition: Lemma convex_expR (t : {i01 R}) (a b : R^o) : expR (a <| t |> b) <= (expR a : R^o) <| t |> (expR b : R^o).
proof: Proof. have [ab|/ltW ba] := leP a b. - apply: second_derivative_convex => //. + by move=> x axb; rewrite derive_expR derive_val expR_ge0. + exact/cvg_at_left_filter/continuous_expR. + exact/cvg_at_right_filter/continuous_expR. + by move=> z zab; rewrite derive_expR; exact: derivable_expR. - rewrite convC [leRHS]convC; apply: second_derivative_convex => //. + by move=> x axb; rewrite derive_expR derive_val expR_ge0. + exact/cvg_at_left_filter/continuous_expR. + exact/cvg_at_right_filter/continuous_expR. + by move=> z zab; rewrite derive_expR; exact: derivable_expR. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex