proposition: Lemma sampleFsq_f_coupling { F : finType} { w0 : F } { f : F -> F } (f_bij : bijective f): coupling (@sampleFsq_f F w0 f f_bij) (@uniform_F F w0) (@uniform_F F w0).
proof: Proof. destruct f_bij as [f_inv K1 K2]. rewrite /sampleFsq_f /f_dprod; split; apply: distr_ext => w /=. - rewrite /lmg dfstE /mkdistr psum_sum /=. rewrite (sum_seq1 (f w)). destruct (f w == f w) eqn: Hfw; auto. -- exfalso. by move/idP: Hfw. move => y Hy. destruct (f w == y) eqn: Hfw; auto. -- exfalso. move/eqP: Hy; auto. move => x. destruct (f w == x) eqn: Hfw; auto. exact r_nonneg. - rewrite /rmg dsndE /mkdistr psum_sum /=. rewrite (sum_seq1 (f_inv w)). have Heq: (f (f_inv w) == w) by apply /eqP; apply: (K2 w). by rewrite Heq. move => y Hy. destruct (f y == w) eqn: Hfy. -- apply /eqP. move/eqP: Hfy => Hfy. rewrite -Hfy. exact (K1 y). -- exfalso. move/eqP: Hy; auto. move => x. destruct (f x == w) eqn: Hfw; auto. exact r_nonneg. 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)