proposition: Lemma sum_prod_bij {T : finType} {f : T -> T} (π : (prod_finType T T) -> R) (π_geq0 : forall t, 0 <= π t) : \sum_(jj <- enum (prod_finType T T)) (if f jj.1 == jj.2 then π jj else 0) = \sum_(j <- enum T) (π (j, f j)).
proof: Proof. rewrite [X in X=_](bigID [pred jj : prod_finType T T | f jj.1 == jj.2]) /=. match goal with | |- _ + ?x = _ => assert (e : x == 0) end. { rewrite psumr_eq0. - apply/allP. intros [i j] h. cbn. destruct (f i == j). + cbn. reflexivity. + cbn. apply/eqP. reflexivity. - intros [i j]. cbn. intros h. destruct (f i == j). 1: discriminate. auto. } move: e => /eqP e. rewrite e. clear e. rewrite GRing.Theory.addr0. erewrite sum_oneq_eq with (G := fun ij => π (ij.1, ij.2)). 2:{ intros [i j]. cbn. intro h. rewrite h. reflexivity. } rewrite !enumT. pose proof pair_big_dep as e. specialize e with (F := fun i j => π (i, j)). specialize e with (P := λ _, true). cbn in e. specialize e with (Q := λ i j, f i == j). cbn in e. rewrite -e. clear e. cbn. erewrite sum_oneq_eq with (G := λ i, π (i, f i)). 2:{ intros i _. erewrite <- big_pred1_eq with (F := λ j, π (i, j)). erewrite sum_pred_eq with (Q := λ j, j == f i). 2:{ intro j. destruct (f i == j) eqn:e. - move: e => /eqP e. subst. destruct (f i == f i) eqn:e. + reflexivity. + move: e => /eqP e. contradiction. - move: e => /eqP e. destruct (j == f i) eqn:e'. + move: e' => /eqP e'. subst. contradiction. + reflexivity. } reflexivity. } reflexivity. Qed.
imports: Coq(Relation_Definitions RelationClasses Morphisms Utf8) Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg)