proposition: Lemma __admitted__dlet_lim f h : (forall n m, (n <= m)%N -> f n <=1 f m) -> \dlet_(x <- dlim f) h x =1 \dlim_(n) \dlet_(x <- f n) h x.
proof: Proof. Admitted. Lemma __admitted__dlim_let (f : nat -> T -> {distr U / R}) (mu : {distr T / R}) : (forall x n m, (n <= m)%N -> f n x <=1 f m x) -> \dlim_(n) \dlet_(x <- mu) (f n x) =1 \dlet_(x <- mu) \dlim_(n) (f n x). Proof using Type. Admitted. End DLimTheory. #[deprecated(since="mathcomp-analysis 0.6.2", note="lacks proof, use __admitted__dlet_lim explicitly if you really want to use this lemma")] Notation dlet_lim := __admitted__dlet_lim. #[deprecated(since="mathcomp-analysis 0.6.2", note="lacks proof, use __admitted__dlim_let explicitly if you really want to use this lemma")] Notation dlim_let := __admitted__dlim_let. Section Marginals. Variable (T U : choiceType) (h : T -> U) (mu : distr T). Definition dmargin := \dlet_(x <- mu) (dunit (h x)). Lemma dmarginE : dmargin = \dlet_(y <- mu) (dunit (h y)). Proof. by []. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum