proposition: Lemma discrete_commute : forall A B (d1:distr A) (d2:distr B) (f:MF (A*B)), is_discrete d1 -> prod_distr_com d1 d2 f.
proof: Proof. red; intros A B d1 d2 f ((cf,cfr,pt),H); simpl. unfold arg_swap; unfold swap; simpl. apply Oeq_trans with (mu d2 (fun x : B => discrete cf pt (fun x0 : A => f (x0, x)))). unfold discrete; simpl. rewrite (mu_serie_eq d2 (fun k x => cf k * f (pt k, x))). apply Oeq_trans with (discrete cf pt (fun x : A => mu d2 (fun x0 : B => f (x, x0)))); auto. rewrite discrete_simpl; apply serie_eq_compat; intro k. apply Oeq_sym; apply (mu_stable_mult d2 (cf k) (fun x0 : B => f (pt k, x0))). intros; apply wretract_le with cf; auto. apply (mu_stable_eq d2); simpl; apply ford_eq_intro; intro x. apply Oeq_trans with (mu (Discrete (Build_discr cfr pt)) (fun x0 : A => f (x0, x))); auto. apply Oeq_sym; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)