proposition: Lemma convex_function_sym (f : T -> U) a b : (forall t, convex_function_at f a b t) -> (forall t, convex_function_at f b a t).
proof: Proof. move=> H t; move: (H (Prob.p t).~%:pr). by rewrite /convex_function_at /= convC -probK (convC _ (f a)) -probK. 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