proposition: Lemma bijective_isdistr {F1 F2 : finType} {w0 : F1} {w0' : F2} {S1 S2 : choiceType} {s1 : S1} {s2 : S2} {f : F1 -> F2} (f_bij : bijective f) : isdistr (@f_dprod F1 F2 S1 S2 w0 w0' s1 s2 f).
proof: Proof. rewrite /f_dprod. split. - move => [[w1 st1] [w2 st2]]. destruct ((st1 == s1) && (st2 == s2) && (f w1 == w2)) eqn:Heq; auto. exact r_nonneg. - rewrite /= => J uniq_J. rewrite [X in X<=_](bigID [pred j : _ | (j.1.2 == s1) && (j.2.2 == s2) && (f j.1.1 == j.2.1)]) /=. lazymatch goal with | |- context [ _ + ?x ] => assert (e : x == 0) end. { rewrite psumr_eq0. - apply/allP. intros [[w1 st1] [w2 st2]] h. cbn. match goal with | |- context [ if ?b then _ else _ ] => destruct b end. + cbn. reflexivity. + cbn. apply/eqP. reflexivity. - intros [[w1 st1] [w2 st2]]. cbn. intros h. match goal with | |- context [ if ?b then _ else _ ] => destruct b end. 1: discriminate. auto. } move: e => /eqP e. rewrite e. clear e. rewrite GRing.Theory.addr0. erewrite sum_oneq_eq with (G := fun i => r). 2:{ intros [[w1 st1] [w2 st2]]. cbn. intros h. rewrite h. reflexivity. } rewrite big_const_seq. cbn. match goal with | |- context [ count ?p _ ] => set (P := p) end. pose (J' := [seq p <- J | P p ]). assert (e1 : count P J = size J'). { rewrite size_filter. reflexivity. } pose (g := fun i => ((i, s1), (f i, s2))). pose (proj := fun (j : F1 * S1 * (F2 * S2)) => let '((i,_),_) := j in i). pose (g' := g \o proj). pose (J'' := [seq g' j | j <- J' ]). assert (e2 : J' = J''). { clear - uniq_J. subst J' J''. induction J as [| [[w1 st1] [w2 st2]] J ih]. - cbn. reflexivity. - simpl. destruct (P _) eqn:e. + simpl. f_equal. * unfold P in e. simpl in e. move: e => /andP [e /eqP ?]. move: e => /andP [/eqP ? /eqP ?]. subst. reflexivity. * eapply ih. cbn in uniq_J. move: uniq_J => /andP []. auto. + eapply ih. cbn in uniq_J. move: uniq_J => /andP []. auto. } subst g'. unfold J'' in e2. rewrite -> map_comp in e2. assert (uniq_J' : uniq J'). { subst J'. apply filter_uniq. auto. } pose (I := [seq g i | i <- enum F1]). assert (e3 : (size J' <= size I)%N). { subst I. rewrite size_map. rewrite e2. rewrite size_map. eapply uniq_leq_size. 1:{ rewrite e2 in uniq_J'. apply map_uniq in uniq_J'. auto. } intros x h. rewrite mem_enum. reflexivity. } rewrite -e1 in e3. subst I. rewrite size_map in e3. rewrite -cardE in e3. rewrite item_addr0_mulr. eapply Order.POrderTheory.le_trans with (y := @r _ w0 *~ #|F1|). + rewrite -mulrzr. rewrite -[X in _<=X]mulrzr. rewrite ler_pmul2l. * rewrite ler_int. auto. * unfold r. apply mulr_gt0. -- cbn. rewrite ltr01. reflexivity. -- rewrite -(@pmulr_rgt0 _ #|F1|%:~R). ++ rewrite -(GRing.mul1r (#|F1|%:~R / #|F1|%:~R)). rewrite GRing.mulrA. rewrite GRing.Theory.mulfK. ** rewrite ltr01. reflexivity. ** unshelve eapply card_non_zero. auto. ++ eapply fintype0 in w0 as h. destruct #|F1| eqn:e. 1: contradiction. rewrite ltr0n. reflexivity. + unfold r. rewrite -[X in X <= _]mulrzr. rewrite GRing.div1r. erewrite <- GRing.mulr1. rewrite -GRing.mulrA. rewrite GRing.Theory.mulKf. * auto. * unshelve eapply card_non_zero. auto. Qed.
imports: 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 UniformDistrLemmas Prelude choice_type StateTransformingLaxMorph RulesStateProb)