proposition: Lemma Uniform_eval (i : Index ) {S : choiceType} {s : S} : forall (st : S) (w : fin_family i), @Uniform i S s (w, st) = if st == s then @r (fin_family i) (F_w0 i) else 0.
proof: Proof. cbn. rewrite /SDistr_bind /SDistr_unit => st w /=. rewrite dletE. match goal with | |- psum ?k = _ => eassert (k = _) as H end. { extensionality x. rewrite dunit1E. eassert (((x, s) == (w, st))%:R = (x == w)%:R * (s == st)%:R). { destruct (x == w) eqn:e1, (s == st) eqn:e2. all: cbn. all: cbn in e1. all: rewrite ?e1 ?e2. all: cbn. all: rewrite ?GRing.mulr1 ?GRing.mul0r ?GRing.mulr0. all: reflexivity. } rewrite H. rewrite GRing.mulrA. rewrite -dunit1E. reflexivity. } rewrite H. clear H. rewrite psumZr. 2:{ destruct (s == st). all: cbn. - apply (@ler01 R). - apply Order.POrderTheory.lexx. } rewrite -dletE. rewrite dlet_dunit_id. destruct (s == st) eqn:Heq. - have Heq' : st == s. apply /eqP. by move /eqP: Heq. rewrite Heq'. rewrite GRing.mulr1. reflexivity. - have Heq' : st == s = false. apply /eqP. move /eqP: Heq. congruence. rewrite Heq'. rewrite GRing.mulr0. reflexivity. Unshelve. exact (Real.ringType R). 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)