proposition: Lemma uniform_F_prod_bij : ∀ i j `{Positive i} `{Positive j} (x : 'I_i) (y : 'I_j), mkdistr (mu := λ _ : 'I_i * 'I_j, r (x, y)) (@is_uniform _ (x,y)) = SDistr_bind (λ z : 'I_(i * j), SDistr_unit _ (ch2prod z) ) (mkdistr (mu := λ f : 'I_(i * j), r f) (@is_uniform _ (F_w0 (mkpos (i * j)))) ).
proof: Proof. intros i j pi pj x y. apply distr_ext. simpl. intros [a b]. unfold SDistr_bind. rewrite dletE. simpl. rewrite psumZ. 2:{ unshelve eapply @r_nonneg. eapply ordinal_finType_inhabited. exact _. } unfold r. rewrite card_prod. simpl. rewrite !card_ord. unfold SDistr_unit. unfold dunit. unlock. unfold drat. unlock. simpl. unfold mrat. simpl. erewrite eq_psum. 2:{ simpl. intro u. rewrite GRing.divr1. rewrite addn0. reflexivity. } erewrite psum_finseq with (r := [:: prod2ch (a, b)]). 2: reflexivity. 2:{ simpl. intros u hu. rewrite inE in hu. destruct (ch2prod u == (a,b)) eqn:e. 2:{ exfalso. move: hu => /negP hu. apply hu. apply eqxx. } move: e => /eqP e. rewrite -e. rewrite inE. apply /eqP. symmetry. apply prod2ch_ch2prod. } rewrite bigop.big_cons bigop.big_nil. rewrite ch2prod_prod2ch. rewrite eqxx. simpl. rewrite GRing.addr0. rewrite normr1. rewrite GRing.mulr1. reflexivity. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup pkg_advantage pkg_invariants pkg_distr) Equations.Prop.DepElim Equations(Equations) Crypt(FreeProbProg)