proposition: Lemma delta_conv f g : convex f -> convex g -> delta (conv f g) =1 fmerge (delta f) (delta g).
proof: Proof. move=> [fI dfI] [gI dgI] n. rewrite -delta_fnorm; last by apply: increasing_conv. rewrite -(delta_ext (conv_fnorm _ _)) //. have/delta_ext-> : conv (fnorm f) (fnorm g) =1 conv (fun n => \sum_(i < n) (delta (fnorm f)) i) (fun n => \sum_(i < n) (delta (fnorm g)) i). by apply: conv_ext => i; apply: sum_delta. have/delta_ext-> : (conv (fun n : nat => \sum_(i < n) delta (fnorm f) i) (fun n : nat => \sum_(i < n) delta (fnorm g) i)) =1 (fun n => \sum_(i < n) (fmerge (delta (fnorm f)) (delta (fnorm g))) i). move=> k; rewrite -sum_fmerge_conv //. by apply: increasing_ext dfI => i; rewrite delta_fnorm. by apply: increasing_ext dgI => i; rewrite delta_fnorm. rewrite /delta big_ord_recr /= addnC addnK. by apply: fmerge_aux_ext => i; apply: delta_fnorm. Qed.
imports: mathcomp(all_ssreflect finmap)