Module mathcomp.experimental_reals.distr

From mathcomp Require Import boot order algebra.
From mathcomp Require Import boolp classical_sets.
From mathcomp Require Import constructive_ereal reals.
From mathcomp Require Import xfinmap discrete realseq realsum.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Unset SsrOldRewriteGoalsOrder.

Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope ring_scope.

Local Notation := Monoid.simpm.

Reserved Notation "\dlet_ ( i <- d ) E"
  (at level 36, E at level 36, i, d at level 50,
     format "'[' \dlet_ ( i <- d ) '/ ' E ']'").

Reserved Notation "\dlim_ ( n ) E"
  (at level 36, E at level 36, n at level 50,
     format "'[' \dlim_ ( n ) '/ ' E ']'").

Reserved Notation "\P_[ mu ] E" (at level 2, format "\P_[ mu ] E").
Reserved Notation "\P_[ mu , A ] E" (at level 2, format "\P_[ mu , A ] E").
Reserved Notation "\E?_[ mu ] f" (at level 2, format "\E?_[ mu ] f").
Reserved Notation "\E_[ mu ] f" (at level 2, format "\E_[ mu ] f").
Reserved Notation "\E_[ mu , A ] f" (at level 2, format "\E_[ mu , A ] f").

Local Notation := (fun => `|f x|) (at level 2).

Section Distribution.
Variables ( : realType) ( : choiceType).

Structure := Distr {
   :> T -> R;
  _  :  forall , 0 <= mu x;
  _  :  summable mu;
  _  :  PosSum.psum mu <= 1
}.

Definition & phant R & phant T := distr.
End Distribution.

Notation := (distr_of (Phant R) (Phant T))
  (at level 0, T at level 2, format "{ 'distr' T / R }")
  : type_scope.

Section DistrCoreTh.
Context { : realType} ( : choiceType) ( : {distr T / R}).

Lemma : forall , 0 <= mu x.

Proof.

by case: mu. Qed.

Lemma : PosSum.psum mu <= 1.

Proof.

by case: mu. Qed.

Lemma : summable mu.

Proof.

by case: mu. Qed.

End DistrCoreTh.

#[global] Hint Extern 0 (is_true (0 <= _)) => solve [apply: ge0_mu] : core.
#[global] Hint Resolve le1_mu summable_mu : core.

Section Clamp.
Context { : realType}.

Definition ( : R) :=
Num.max (Num.min x 1) 0.

Lemma : 0 <= clamp x.

Proof.

by rewrite le_max lexx orbT. Qed.

Lemma : clamp x <= 1.

Proof.

by rewrite ge_max ge_min lexx ler01 orbT. Qed.

Definition := (ge0_clamp, le1_clamp).

Lemma : 0 <= x <= 1 -> clamp x = x.

Proof.

by case/andP=> ge0_x le1_x; rewrite /clamp min_l ?max_l. Qed.

Lemma : clamp (clamp x) = clamp x.

Proof.

by rewrite clamp_in01 // !cp01_clamp. Qed.

Lemma : clamp 0 = 0.

Proof.

by rewrite clamp_in01 // lexx ler01. Qed.

Lemma : clamp 1 = 1.

Proof.

by rewrite clamp_in01 // lexx ler01. Qed.

End Clamp.

Section StdDefs.
Context { : realType} ( : choiceType).

Implicit Types (mu : {distr T / R}) (A B E : pred T) (f : T -> R).

Definition := fun => mu x != 0 :> R.

Lemma ( : {distr T / R}) :
(x \in dinsupp mu) = (mu x != 0).

Proof.

by []. Qed.

Lemma : reflect (mu x <> 0) (x \in dinsupp mu).

Proof.

by apply: (iffP idP) => /eqP. Qed.

Lemma : reflect (mu x = 0) (x \notin dinsupp mu).

Proof.

by rewrite -topredE /dinsupp /= negbK; apply/eqP. Qed.

Definition        := PosSum.psum (fun => (E x)%:R * mu x).
Definition    := pr mu [predI E & A] / pr mu A.
Definition       := sum (fun => f x * mu x).
Definition := sum (fun => f x * prc mu (pred1 x) A).

Definition := summable (fun => f x * mu x).
End StdDefs.

Notation      := (pr mu E).
Notation := (prc mu E A).
Notation      := (esp mu f).
Notation := (espc mu f A).
Notation     := (has_esp mu f).
Notation mu        := (\P_[mu] predT).

Section DistrTheory.
Context { : realType} { : choiceType} ( : T -> R).

Definition :=
  (forall , 0 <= mu x) /\ (forall , uniq J -> \sum_( <- J) mu j <= 1).

Hypothesis : isdistr.

Local Lemma : forall , 0 <= mu x.

Proof.

by case: isd. Qed.

Local Lemma : summable mu.

Proof.

case: isd=> _ h; apply/summable_seqP; exists 1=> //.
move=> s /h /(le_trans _); apply; rewrite le_eqVlt; apply/orP.
by left; apply/eqP/eq_bigr=> i _; rewrite ger0_norm ?isd1.
Qed.

Local Lemma : PosSum.psum mu <= 1.

Proof.

rewrite psumE; [apply/isd1 | apply/isd2 | apply: ge_sup].
by exists 0, fset0; rewrite big_fset0.
apply/ubP=> y [x ->]; rewrite big_fset_seq /=.
by case: isd => _; apply; case: x => x /= /canonical_uniq.
Qed.

Definition := @Distr R T mu isd1 isd2 isd3.

Lemma : mkdistr =1 mu.

Proof.

by []. Qed.

Definition { : choiceType} ( : T -> R) :=
[/\ forall , 0 <= mu x & summable mu].
End DistrTheory.

Lemma { : realType} { : finType} ( : I -> R) :
(isdistr mu) <-> (forall , 0 <= mu x) /\ (\sum_ mu j <= 1).

Proof.

split=> -[ ge0_mu le1]; split=> //.
+ by apply/le1; rewrite /index_enum -enumT enum_uniq.
+ move=> J uqJ; rewrite big_uniq 1?(le_trans _ le1) //=.
by rewrite [X in _<=X](bigID (mem J)) /= lerDl sumr_ge0.
Qed.

Lemma
{ : realType} { : choiceType} ( : {distr T / R}) : mu x <= 1.

Proof.

apply/(@le_trans _ _ (PosSum.psum mu)) => //; rewrite -[mu x]ger0_norm//.
by apply/ger1_psum.
Qed.

Section DistrD.
Context { : realType} { : choiceType} ( : T -> R).

Definition := fun : T => (0 : R).

Lemma : isdistr mnull.

Proof.

by split=> // J _; rewrite big1 ?ler01. Qed.

Definition := locked (mkdistr isd_mnull).

Lemma : dnull x = 0.

Proof.

by unlock dnull. Qed.

Definition : {distr T / R} :=
  if @idP `[< isdistr mu >] is ReflectT Px then
    mkdistr (asboolW Px)
  else dnull.
End DistrD.

Lemma { : realType} { : choiceType} ( : {distr T / R}) :
  dnull <=1 mu.

Proof.

by move=> x; rewrite dnullE ge0_mu. Qed.

Section Restr.
Context { : realType} { : choiceType} ( : pred T).

Definition ( : {distr T / R}) :=
fun => if p x then mu x else 0.

Lemma ( : {distr T / R}) : isdistr (mrestr mu).

Proof.

split=> [x|J]; first by rewrite /mrestr; case: ifP.
move=> eqJ; apply/(@le_trans _ _ (\sum_( <- J) `|mu j|)).
+ apply/ler_sum=> i _; rewrite /mrestr; case: ifPn=> _.
by apply/ler_norm. by apply/normr_ge0.
+ by apply/(le_trans _ (le1_mu mu))/gerfinseq_psum.
Qed.

Definition ( : {distr T / R}) := locked (mkdistr (isd_mrestr mu)).

Lemma ( : {distr T / R}) :
drestr mu x = if p x then mu x else 0.

Proof.

by unlock drestr. Qed.

End Restr.

Section RestrTheory.
Context { : realType} { : choiceType}.

Lemma ( : {distr T / R}) ( : pred T) :
mu x = drestr p mu x + drestr (predC p) mu x.

Proof.

by rewrite !drestrE !inE; case: ifPn; rewrite /= (addr0, add0r). Qed.

Lemma ( : {distr T / R}) ( : pred T) :
(x \in dinsupp (drestr p mu)) = (x \in dinsupp mu) && p x.

Proof.

apply/dinsuppP/idP.
- by rewrite drestrE; case: ifP=> // _ /dinsuppP ->.
- by case/andP; rewrite drestrE => /dinsuppP ? ->.
Qed.

End RestrTheory.

Section DRat.
Context { : realType} ( : choiceType).

Local Notation := {distr T / R}.

Implicit Types (s : seq T).

Definition ( : seq T) : T -> R :=
fun : T => (count (pred1 x) s)%:R / (size s)%:R.

Lemma : forall , 0 <= mrat s x.

Proof.

by move=> x; rewrite mulr_ge0 ?invr_ge0 // ler0n. Qed.

Local Lemma : uniq J -> \sum_( <- J) mrat s i <= 1.

Proof.

move=> uqJ; rewrite -mulr_suml /= -natr_sum; case: (size s =P 0%N).
  by move=> ->; rewrite invr0 mulr0 ler01.
move=> /eqP nz_s; rewrite ler_pdivrMr ?ltr0n ?lt0n // mul1r.
rewrite ler_nat (bigID (mem s)) /= [X in (_+X)%N]big1 ?addn0.
   by move=> i /count_memPn.
have ->: (size s = \sum_( <- undup s) count_mem i s)%N.
  rewrite -sum1_size -big_undup_iterop_count; apply: eq_bigr => i _.
  by rewrite Monoid.iteropE iter_addn addn0 mul1n.
rewrite [X in (_<=X)%N](bigID (mem J)) /= -ltnS -addSn.
rewrite ltn_addr //= ltnS -big_filter -[X in (_<=X)%N]big_filter.
rewrite leq_eqVlt; apply/orP; left; apply/eqP/perm_big.
apply/uniq_perm; rewrite ?filter_uniq ?undup_uniq //.
by move=> x; rewrite !mem_filter mem_undup andbC.
Qed.

Local Lemma : (0 < size s)%N ->
\sum_( <- undup s) mrat s i = 1.

Proof.

move=> gt0_s; rewrite -mulr_suml -natr_sum.
apply/(mulIf (x := (size s)%:R)); first by rewrite pnatr_eq0 -lt0n.
rewrite mul1r divfK ?pnatr_eq0 -?lt0n//; congr (_%:R).
rewrite -sum1_size -[in RHS]big_undup_iterop_count/=; apply: eq_bigr => i _.
by rewrite Monoid.iteropE iter_addn addn0 mul1n.
Qed.

Local Lemma : summable (mrat s).

Proof.

apply/summable_seqP; exists 1=> // J uqJ; rewrite (eq_bigr (mrat s)).
by move=> j _; rewrite ger0_norm ?ge0_mrat.
by apply/has_sup_mrat.
Qed.

Lemma : isdistr (mrat s).

Proof.

by split; [apply/ge0_mrat | apply/has_sup_mrat]. Qed.

Definition := locked (mkdistr (isd_mrat s)).

Lemma :
drat s x = (count_mem x s)%:R / (size s)%:R.

Proof.

by unlock drat; rewrite mkdistrE. Qed.

Definition := locked (drat [:: x]).
Definition := locked (drat (undup s)).

Lemma : (dunit x) y = (x == y)%:R.

Proof.

by unlock dunit; rewrite drat1E /= !(simpm, invr1). Qed.

Lemma : (duni s) x = (x \in s)%:R / (size (undup s))%:R.

Proof.

by unlock duni; rewrite drat1E count_uniq_mem ?(mem_undup, undup_uniq).
Qed.

Lemma :
t' \in dinsupp (dunit t) -> t' = t :> T.

Proof.

by rewrite in_dinsupp dunit1E pnatr_eq0 eqb0 negbK => /eqP.
Qed.

End DRat.

Section Flip.
Context { : realType}.

Definition ( : R) :=
fun => if b then clamp xt else 1 - clamp xt.

Lemma : isdistr (mflip xt).

Proof.

apply/isdistr_finP; split=> [b|].
+ by case: b; rewrite ?subr_ge0 cp01_clamp.
+ by rewrite /index_enum !unlock /= addr0 addrC subrK.
Qed.

Definition ( : R) := locked (mkdistr (isd_mflip xt)).

Lemma : dflip xt =1 mflip xt.

Proof.

by unlock dflip; apply/mkdistrE. Qed.

End Flip.

Section Std.
Context { : realType}.

Local Notation T := {distr T / R}.

Implicit Types (T U : choiceType).

Section Bind.
Context { : choiceType} ( : T -> distr U) ( : distr T).

Definition := fun : U => PosSum.psum (fun => mu x * f x y).

Lemma : isdistr mlet.

Proof.

split=> [x|J uqJ]; first by apply/ge0_psum.
rewrite /mlet psum_bigop; first by move=> y x; rewrite mulr_ge0.
move=> u; apply/(le_summable (g := mu)) => //.
by move=> x; rewrite mulr_ge0 //= ler_piMr ?le1_mu1.
apply/(le_trans _ (le1_mu mu))/le_psum => //.
move=> x; rewrite sumr_ge0 /= => [y _|]; first by rewrite mulr_ge0.
rewrite -mulr_sumr ler_piMr //; apply/(le_trans _ (le1_mu (f x))).
have := summable_mu (f x) => /gerfinseq_psum => /(_ _ uqJ).
by apply/(le_trans _)/ler_sum=> y _; apply/ler_norm.
Qed.

Definition := locked (mkdistr isd_mlet).

Lemma : dlet y = PosSum.psum (fun => mu x * f x y).

Proof.

by unlock dlet. Qed.

End Bind.

Notation := (dlet (fun => E) d).

Definition { : choiceType} ( : A -> {distr A / R}) :=
fun => \dlet_( <- d) f x.

Definition { : choiceType} ( : A -> {distr A / R}) :=
fun => (iter n (dlift f) (dunit a)).

Section BindTheory.
Variables ( : choiceType).

Implicit Types (f g : T -> distr U) (mu nu : distr T).

Lemma : dlet f dnull =1 dnull.

Proof.

move=> x; rewrite dletE dnullE /= /mlet psum_eq0 //.
by move=> y; rewrite dnullE mul0r.
Qed.

Lemma : \dlet_( <- dunit v) f y =1 f v.

Proof.

move=> y; rewrite dletE (psum_finseq (r := [:: v])) //.
move=> x; rewrite !inE dunit1E mulf_eq0 => /norP[].
by rewrite pnatr_eq0 eqb0 negbK => /eqP->.
by rewrite big_seq1 dunit1E eqxx mul1r ger0_norm.
Qed.

Lemma : \dlet_( <- mu) (dunit t) =1 mu.

Proof.

move=> x; rewrite dletE (psum_finseq (r := [:: x])) //.
move=> y; rewrite !inE dunit1E mulf_eq0 pnatr_eq0.
by case/norP; rewrite eqb0 negbK.
by rewrite big_seq1 dunit1E eqxx mulr1 ger0_norm.
Qed.

Lemma : {in dinsupp mu, f =2 g} -> mu =1 nu ->
dlet f mu =1 dlet g nu.

Proof.

move=> eq_f eq_mu; unlock dlet=> y /=; apply/eq_psum=> x.
rewrite -eq_mu; case/boolP: (x \in dinsupp mu) => [/eq_f ->//|].
by move/dinsuppPn=> ->; rewrite !mul0r.
Qed.

Lemma ( : T -> R) :
(forall , 0 <= f x <= 1) -> summable (fun => mu x * f x).

Proof.

move=> in01_f; apply/summableMr=> //.
exists 1 => x; case/andP: (in01_f x) => ge0_fx le1_fx.
by rewrite ger0_norm.
Qed.

Lemma : summable (fun : T => mu x * (f x) y).

Proof.

by apply/summable_mu_wgtd=> x; rewrite ge0_mu le1_mu1. Qed.

Lemma : {in dinsupp mu, f <=2 g} ->
dlet f mu <=1 dlet g mu.

Proof.

(* summable -> refactor *)
move=> le_f; unlock dlet=> y /=; apply/le_psum/summable_mlet.
move=> x; rewrite mulr_ge0 //=; case: (mu x =P 0).
by move=> ->; rewrite !mul0r.
by move/dinsuppPn/le_f/(_ y) => h; rewrite ler_pM.
Qed.

Lemma : mu <=1 nu -> dlet f mu <=1 dlet f nu.

Proof.

move=> le_mu x; unlock dlet; rewrite /= /mlet.
apply/le_psum/summable_mlet => y; rewrite mulr_ge0 //=.
case: (mu y =P 0) => [->|]; first by rewrite mul0r mulr_ge0.
by move=>/dinsuppPn=> h; rewrite ler_pM.
Qed.

Lemma :
    mu <=1 nu
  -> {in dinsupp mu, forall , f x <=1 g x}
  -> \dlet_( <- mu) f x <=1 \dlet_( <- nu) g x.

Proof.

move=> le_mu le_fg x.
by apply/(le_trans (le_in_dlet le_fg _))/le_mu_dlet.
Qed.

Lemma ( : {distr T / R}) ( : {distr U / R}) :
(\dlet_(_ <- mu) nu) y = (dweight mu) * (nu y).

Proof.

rewrite dletE /pr [_ * nu y]mulrC -psumZ //=; apply/eq_psum.
by move=> /= x; rewrite mul1r mulrC.
Qed.

Lemma :
y \in dinsupp (\dlet_( <- mu) f x) ->
exists2 , x \in dinsupp mu & f x y != 0.

Proof.

move/dinsuppP; rewrite dletE => /neq0_psum [x /eqP]; rewrite mulf_eq0.
by case/norP=> /eqP/dinsuppPn mux nz_fxy; exists x.
Qed.

Lemma :
x \in dinsupp mu -> f x y != 0 -> y \in dinsupp (dlet f mu).

Proof.

move=> /dinsuppP /eqP mux nz_fxy; apply/dinsuppP; rewrite dletE.
move/eq0_psum => /(_ (summable_mlet _ _ _) x) => /eqP.
by rewrite mulf_eq0 (negbTE mux) (negbTE nz_fxy).
Qed.

Lemma ( : T -> U) :
{in dinsupp mu, forall , f x != y} -> (\dlet_( <- mu) dunit (f x)) y = 0.

Proof.

move=> h; unlock dlet => /=; apply/psum_eq0 => x.
case/boolP: (x \in dinsupp mu) => [|/dinsuppPn->];
last by rewrite mul0r.
by move/h; rewrite dunit1E => /negbTE ->; rewrite mulr0.
Qed.

Lemma ( : {distr T / R}) ( : T -> {distr U / R}) :
(\dlet_( <- mu) F x) y = 0 -> forall , x \in dinsupp mu -> F x y = 0.

Proof.

unlock dlet; rewrite /= /mlet => /eq0_psum h x /dinsuppP /eqP mu_x.
have {}/h: summable (fun => mu x * F x y).
apply/(le_summable (g := mu)) => // z.
by rewrite mulr_ge0 //= ler_piMr // le1_mu1.
by move/(_ x)/eqP; rewrite mulf_eq0 (negbTE mu_x) /= => /eqP.
Qed.

End BindTheory.

Section DLetDLet.
Context { : choiceType} ( : T -> distr U) ( : U -> distr V).

Lemma ( : {distr T / R}) :
\dlet_( <- \dlet_( <- mu) f1 y) f2 x
=1 \dlet_( <- mu) (\dlet_( <- f1 y) f2 x).

Proof.

move=> z; unlock dlet => /=; rewrite /mlet /=.
pose S := mu x * (f1 x y * f2 y z).
rewrite (eq_psum (F2 := fun => PosSum.psum (S^~ y))) => [x|].
  by rewrite -psumZ //; apply/eq_psum => y /=.
rewrite interchange_psum.
+ by move=> x; apply/summableZ/summable_mlet.
+ rewrite {}/S; apply/(le_summable (g := mu)) => //.
  move=> x; rewrite ge0_psum /= psumZ ?ler_piMr //.
  apply/(le_trans _ (le1_mu (f1 x)))/le_psum => //.
  by move=> y; rewrite mulr_ge0 //= ler_piMr ?le1_mu1.
apply/eq_psum=> y /=; rewrite -psumZr //.
by apply/eq_psum=> x /=; rewrite {}/S mulrA.
Qed.

End DLetDLet.

Section DLetAlg.
Context { : choiceType} ( : {distr T / R}).

Lemma ( : T -> {distr U / R}) :
(forall , mu x = mu1 x + mu2 x) -> (\dlet_( <- mu) f x) z =
(\dlet_( <- mu1) f x) z + (\dlet_( <- mu2) f x) z.

Proof.

move=> muD; rewrite !dletE -psumD /=.
by move=> x; rewrite mulr_ge0. by move=> x; rewrite mulr_ge0.
by apply/summable_mlet. by apply/summable_mlet.
by apply/eq_psum=> x /=; rewrite -mulrDl -muD.
Qed.

End DLetAlg.

Definition ( : nat -> distr T) : T -> R :=
fun => fine (nlim (fun => f n x)).

Lemma ( : nat -> distr T) : isdistr (mlim f).

Proof.

split=> [x|J]; rewrite /mlim.
  case: nlimP=> // l cvSl; apply/fine_ge0/(ncvg_geC _ cvSl).
  by move=> n; apply/ge0_mu.
move=> uqJ; pose F :=
  if `[< iscvg (fun => f n j) >] then fun => f n j else 0%:S.
apply/(@le_trans _ _ (\sum_( <- J) (fine (nlim (F j) (*: R*))))).
  apply/ler_sum=> j _; rewrite /F; case/boolP: `[< _ >] => //.
  move/asboolPn=> h; rewrite nlimC; case: nlimP=> //.
  by case=> // l cf; case: h; exists l.
rewrite -lee_fin -nlim_sumR => [i _|].
  rewrite /F; case/boolP: `[< _ >] => [/asboolP //|].
  by move=> _; apply/iscvgC.
rewrite leNgt; apply/negP; pose s := \sum_( <- J) F j n.
move/ncvg_gt=> -/(_ s (nlim_ncvg _)) [].
  suff: iscvg s by case=> l cs; exists l%:E.
  apply/iscvg_sum=> j _; rewrite /F; case/boolP: `[< _ >].
    by move/asboolP. by move=> _; apply/iscvgC.
move=> K /(_ _ (leqnn K)) /=; apply/negP; rewrite -leNgt.
apply/(@le_trans _ _ (\sum_( <- J) f K j)); last first.
  have /(gerfinseq_psum uqJ) := summable_mu (f K).
  move/le_trans=> -/(_ _ (le1_mu (f K)))=> h.
  by apply/(le_trans _ h)/ler_sum=> i _; apply/ler_norm.
by apply/ler_sum=> j _; rewrite /F; case/boolP: `[< _ >].
Qed.

Definition ( : nat -> distr T) :=
locked (mkdistr (isd_mlim f)).

Notation := (dlim (fun => E)).

Lemma ( : nat -> distr T) :
(\dlim_() f n) x = fine (nlim (fun => f n x)).

Proof.

by unlock dlim. Qed.

Section DLimTheory.
Variables ( : choiceType).

Implicit Types (f g : nat -> distr T) (h : T -> {distr U / R}).
Implicit Types (mu : {distr T / R}).

Lemma : \dlim_() mu =1 mu.

Proof.

by move=> x; rewrite !dlimE; rewrite nlimC. Qed.

Lemma : f =2 g -> dlim f =1 dlim g.

Proof.

move=> eq_f; unlock dlim=> x /=; rewrite /mlim; congr (_ _).
by apply/eq_nlim => n; rewrite eq_f.
Qed.

Lemma :
(forall , (K <= n)%N -> f n =1 g n) -> dlim f =1 dlim g.

Proof.

move=> eq_fg x; rewrite !dlimE; congr (_ _).
by apply/(eq_from_nlim (K := K)); move=> n /eq_fg /(_ x).
Qed.

Definition ( : nat -> {distr T / R}) :
dlim (fun => mu n.+1) =1 dlim mu.

Proof.

by move=> x; rewrite !dlimE -[in RHS]nlim_bump. Qed.

Definition ( : nat -> {distr T / R}) :
dlim (fun => mu (n + p)%N) =1 dlim mu.

Proof.

by move=> x; rewrite !dlimE (nlim_lift (fun => (mu n) x)). Qed.

Definition { : choiceType} ( : nat -> {distr T / R}) :=
  forall , exists , ncvg (fun => f n x) l.

Definition { : choiceType} ( : nat -> {distr T / R}) :=
  exists , forall , ncvg (fun => f n x) l.

CoInductive ( : T) : R -> Type :=
| : forall : R, 0 <= l -> l <= 1 ->
    ncvg (fun => f n x) l%:E -> dlim_spec f x l

| : ~ (exists : \bar R, ncvg (fun => f n x) l) ->
    dlim_spec f x 0.

Lemma : dlim_spec f x (dlim f x).

Proof.

rewrite dlimE; case: nlimP => [l h|?] /=; last by apply/DLimOut.
have: (0%:E <= l)%E by apply/ncvg_geC: h => n; apply/ge0_mu.
have: (l <= 1%:E)%E by apply/ncvg_leC: h => n; apply/le1_mu1.
by case: l h => // l h /= ge0_l ge1_; apply/DLimCvg.
Qed.

Lemma : dcvg f -> forall ,
exists2 , (0 <= l <= 1) & ncvg (f^~ x) l%:E.

Proof.

move=> cv_f x; case: (dlimP f x) => [l ge0_l le1_l cv|].
by exists l => //; apply/andP; split.
by case; case: (cv_f x).
Qed.

Lemma :
(forall , (n <= m)%N -> f n <=1 f m) -> dcvg f.

Proof.

move=> mn_f x; have: forall , (n <= m)%N -> f n x <= f m x.
  by move=> n m /mn_f; apply.
case/ncvg_mono_bnd => {mn_f}; first apply/asboolP/nboundedP.
  exists 2%:R => // n; apply/(@le_lt_trans _ _ 1%:R)/ltr_nat.
  by rewrite ger0_norm // le1_mu1.
by move=> y h; exists y%:E.
Qed.

Lemma : forall , 0 <= dlim f x.

Proof.

by move=> x; case: dlimP. Qed.

Lemma : forall , dlim f x <= 1.

Proof.

by move=> x; case: dlimP => // _; apply/ler01. Qed.

Lemma :
(forall , f n <=1 g n) -> dcvg g -> dlim f <=1 dlim g.

Proof.

move=> le dcvg_g x; case: dlimP => [|_]; last by apply/ge0_dlim.
move=> l _ _ h; case: dlimP => [l' _ _ h'|]; last by case.
by rewrite -lee_fin; apply/(ncvg_le _ h' h).
Qed.

Lemma : (forall , f n <=1 mu) -> dlim f <=1 mu.

Proof.

move=> le x; apply/(@le_trans _ _ ((\dlim_() mu) x)).
by apply/le_dlim => // y; exists (mu y)%:E; apply/ncvgC.
by rewrite dlimE nlimC.
Qed.

Lemma :
(forall , (n <= m)%N -> f n <=1 f m) -> f k <=1 dlim f.

Proof.

move=> mn_f x; rewrite dlimE -lee_fin; pose u := f n x.
apply/(ncvg_homo_le (u := u))=> [m n /mn_f|]; first by apply.
move/dcvg_homo: mn_f => /dcvgP /(_ x) [l _].
by move=> cv; rewrite (nlimE cv).
Qed.

Lemma : (forall , (n <= m)%N -> f n <=1 f m) ->
\dlet_( <- dlim f) h x =1 \dlim_() \dlet_( <- f n) h x.

Proof.

Admitted.

Lemma ( : nat -> T -> {distr U / R}) ( : {distr T / R}) :
  (forall , (n <= m)%N -> f n x <=1 f m x) ->
  \dlim_() \dlet_( <- mu) (f n x) =1
    \dlet_( <- mu) \dlim_() (f n x).
Proof using Type. 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 := __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 := __admitted__dlim_let.

Section Marginals.
Variable ( : choiceType) ( : T -> U) ( : distr T).

Definition := \dlet_( <- mu) (dunit (h x)).

Lemma : dmargin = \dlet_( <- mu) (dunit (h y)).

Proof.

by []. Qed.

End Marginals.

Section MarginalsTh.
Variable ( : choiceType).

Lemma ( : {distr T / R}) ( : T -> U) :
(dmargin f mu) y = PosSum.psum (fun => (f x == y)%:R * mu x).

Proof.

rewrite dmarginE dletE; apply/eq_psum => x //=.
by rewrite mulrC dunit1E.
Qed.

Lemma ( : {distr T / R}) ( : T -> U) ( : U -> {distr V / R}):
\dlet_( <- dmargin f mu) g u =1 \dlet_( <- mu) (g (f t)).

Proof.

move=> x; rewrite dlet_dlet; apply: eq_in_dlet=> //.
by move=> y _ z; rewrite dlet_unit.
Qed.

Lemma ( : {distr T / R}) ( : U -> V) ( : T -> {distr U / R}):
dmargin f (\dlet_( <- mu) g t) =1 \dlet_( <- mu) (dmargin f (g t)).

Proof.

by apply/dlet_dlet. Qed.

Lemma ( : T) ( : T -> U):
dmargin f (dunit t) =1 dunit (f t) :> {distr U / R}.

Proof.

by apply/dlet_unit. Qed.

End MarginalsTh.
End Std.

#[deprecated(since="1.17.0", note="use `dmargin_dlet` instead")]
Notation := dmargin_dlet (only parsing).
#[deprecated(since="1.17.0", note="use `dlet_dmargin` instead")]
Notation := dlet_dmargin (only parsing).
#[deprecated(since="1.17.0", note="use `dlet_dlet` instead")]
Notation := dlet_dlet (only parsing).

Notation mu := (dmargin fst mu).
Notation mu := (dmargin snd mu).

Notation := (dlet (fun => E) d).
Notation := (dlim (fun => E)).

Section DSwap.
Context { : realType} { : choiceType} ( : {distr (A * B) / R}).

Definition : {distr (B * A) / R} :=
dmargin (fun => (xy.2, xy.1)) mu.
End DSwap.

Section DSwapCoreTheory.
Context { : realType} { : choiceType} ( : {distr (A * B) / R}).

Lemma : dswap mu xy = mu (xy.2, xy.1).

Proof.

rewrite dletE /= (psum_finseq (r := [:: (xy.2, xy.1)])) //.
case=> a b; rewrite !inE dunit1E /= mulf_eq0.
by case/norP=> _; rewrite pnatr_eq0 eqb0 negbK=> /eqP <-.
by case: xy=> x y; rewrite big_seq1 dunit1E /= eqxx mulr1 ger0_norm.
Qed.

End DSwapCoreTheory.

Section DSwapTheory.
Context { : realType} { : choiceType} ( : {distr (A * B) / R}).

Lemma : dswap (dswap mu) =1 mu.

Proof.

by case=> x y; rewrite !dswapE. Qed.

Lemma : (xy.2, xy.1) \in dinsupp mu ->
xy \in dinsupp (dswap mu).

Proof.

by move=> h; apply/dinsuppP; rewrite dswapE; apply/dinsuppPn.
Qed.

Lemma : dfst (dswap mu) =1 dsnd mu.

Proof.

move=> z; rewrite dlet_dlet; apply/eq_in_dlet => // -[x y].
by move=> _ t /=; rewrite dlet_unit /=.
Qed.

Lemma : dsnd (dswap mu) =1 dfst mu.

Proof.

move=> z; rewrite dlet_dlet; apply/eq_in_dlet => // -[x y].
by move=> _ t /=; rewrite dlet_unit /=.
Qed.

End DSwapTheory.

#[deprecated(since="1.17.0", note="use `dfst_dswap` instead")]
Notation := dfst_dswap (only parsing).
#[deprecated(since="1.17.0", note="use `dsnd_dswap` instead")]
Notation := dsnd_dswap (only parsing).

Section DFst.
Context { : realType} { : choiceType}.

Lemma ( : {distr (T * U) / R}) :
dfst mu x = PosSum.psum (fun => mu (x, y)).

Proof.

rewrite dmargin_psumE /=; pose h : T * U := (x, y).
rewrite (reindex_psum (P := [pred | z.1 == x]) (h := h)) /=.
+ case=> a b; rewrite !inE/= mulf_eq0 => /norP[].
by rewrite pnatr_eq0 eqb0 negbK.
+ by exists snd => [z|[z1 z2]]; rewrite !inE //= => /eqP ->.
by apply/eq_psum => y; rewrite eqxx mul1r.
Qed.

Lemma ( : {distr (T * U) / R}) :
summable (fun => mu (x, y)).

Proof.

have /summable_seqP /= := summable_mu mu => -[M ge0_M h].
apply/summable_seqP; exists M => // J uqJ; pose X := [seq (x, y) | <- J].
apply/(le_trans _ (h X _)); last by rewrite map_inj_uniq // => y1 y2 [].
by rewrite le_eqVlt big_map eqxx.
Qed.

End DFst.

Section DSnd.
Context { : realType} { : choiceType}.

Lemma ( : {distr (T * U) / R}) :
dsnd mu y = PosSum.psum (fun => mu (x, y)).

Proof.

by rewrite -dfst_dswap dfstE; apply/eq_psum=> x; rewrite dswapE. Qed.

Lemma ( : {distr (T * U) / R}) :
summable (fun => mu (x, y)).

Proof.

have := summable_fst (dswap mu) y; apply/eq_summable.
by move=> x /=; rewrite dswapE.
Qed.

End DSnd.

#[deprecated(since="1.17.0", note="use `dsndE` instead")]
Notation := dsndE (only parsing).

Section PrCoreTheory.
Context { : realType} { : choiceType}.

Implicit Types (mu : {distr T / R}) (A B E : pred T).

Lemma : summable (fun => (E x)%:R * mu x).

Proof.

apply/(le_summable (g := mu)) => [x|]; last by apply/summable_mu.
by rewrite mulr_ge0 ?ler0n //= ler_piMl // lern1 leq_b1.
Qed.

Lemma : \P_[mu] pred0 = 0.

Proof.

by rewrite /pr psum_eq0 // => x /=; rewrite mul0r. Qed.

Lemma : mu x = \P_[mu] (pred1 x).

Proof.

rewrite /pr (psum_finseq (r := [:: x])) // => [y|].
by rewrite !inE; case: (y =P x); rewrite ?(mul0r, eqxx).
by rewrite big_seq1 /= eqxx mul1r ger0_norm.
Qed.

Lemma ( : pred T) : \P_[mu] E = \E_[mu] (fun => (E m)%:R).

Proof.

by rewrite /pr psum_sum // => x; rewrite mulr_ge0 // ler0n. Qed.

Lemma : \P_[mu] predT = PosSum.psum mu.

Proof.

by apply/eq_psum=> x; rewrite mul1r. Qed.

Lemma : \P_[dunit x] E = (E x)%:R :> R.

Proof.

rewrite /pr (psum_finseq (r := [:: x])) //.
move=> y; rewrite !inE dunit1E [x==_]eq_sym.
by case: (y =P x) => //; rewrite mulr0 eqxx.
by rewrite big_seq1 dunit1E eqxx mulr1 ger0_norm ?ler0n.
Qed.

Lemma ( : T -> R) ( : T) : \E_[dunit x] f = f x.

Proof.

rewrite /esp (sum_seq1 x) => [y|]; rewrite dunit1E.
by case: (x == y) => //; rewrite mulr0 eqxx.
by rewrite eqxx mulr1.
Qed.

Lemma : \E_[mu] (fun _ => r) = \P_[mu] predT * r.

Proof.

by rewrite pr_predT psum_sum // [RHS]mulrC -sumZ; apply/eq_sum.
Qed.

Lemma : \E_[mu] (fun _ => 0) = 0.

Proof.

by rewrite exp_cst mulr0. Qed.

Lemma : \E?_[mu] (fun _ => c).

Proof.

by apply/summableMl => //; exists `|c|. Qed.

Lemma : \E?_[mu] (fun _ => 0).

Proof.

by apply/(has_expC mu 0). Qed.

Lemma : \E?_[mu] (fun _ => 1).

Proof.

by apply/(has_expC mu 1). Qed.

Lemma : \E?_[mu] F -> \E?_[mu] (c \*o F).

Proof.

move=> heF; have: summable (c \*o (F \* mu)) by apply/summableZ.
by apply/eq_summable => x /=; rewrite mulrA.
Qed.

Lemma : \E_[mu] (c \*o F) = c * \E_[mu] F.

Proof.

by rewrite -sumZ; apply/eq_sum=> x /=; rewrite mulrA. Qed.

Lemma : 0 <= \P_[mu] A.

Proof.

by apply/ge0_psum. Qed.

Lemma : 0 <= \P_[mu, B] A.

Proof.

by rewrite /prc mulr_ge0 ?invr_ge0 // ge0_pr. Qed.

Lemma :
{in dinsupp mu, A =i B} -> \P_[mu] A = \P_[mu] B.

Proof.

move=> eq_AB; apply/eq_psum => x; case/boolP: (x \in dinsupp mu).
by move/eq_AB; rewrite -!topredE => /= ->.
by move/dinsuppPn=> ->; rewrite !mulr0.
Qed.

Lemma : A =i B -> \P_[mu] A = \P_[mu] B.

Proof.

by move=> eq_AB; apply/eq_in_pr=> x _; apply/eq_AB. Qed.

Lemma ( : T -> R):
{in dinsupp mu, f1 =1 f2} -> \E_[mu] f1 = \E_[mu] f2.

Proof.

move=> eq_f; apply/eq_sum => x; case/boolP: (x \in dinsupp mu).
by move/eq_f=> ->. by move/dinsuppPn=> ->; rewrite !mulr0.
Qed.

Lemma ( : {distr T / R}) ( : pred T) :
E =1 pred0 -> \P_[mu] E = 0.

Proof.

by move=> eq; rewrite -(pr_pred0 mu); apply/eq_pr. Qed.

End PrCoreTheory.

Section PrTheory.
Context { : realType} { : choiceType} { : eqType}.

Implicit Types (mu : {distr T / R}) (A B E : pred T).

Lemma ( : {distr U / R}) :
\P_[dlet f mu] E = \E_[mu] (fun => \P_[f x] E).

Proof.

rewrite /esp -psum_sum => [x|]; first by rewrite mulr_ge0 ?ge0_pr.
rewrite /pr; unlock dlet => /=; rewrite /mlet /=.
pose F := (E x)%:R * (mu y * f y x).
transitivity (PosSum.psum (fun => PosSum.psum (fun => F x y))); rewrite {}/F.
  by apply/eq_psum => x; rewrite -psumZ ?ler0n.
rewrite interchange_psum /=; last first.
  apply/eq_psum=> y /=; rewrite mulrC -psumZ //.
  by apply/eq_psum=> x /=; rewrite mulrCA.
+ have := summable_pr E (dlet f mu); apply/eq_summable.
  by move=> x; rewrite /= dletE psumZ ?ler0n.
+ by move=> t; exact/summable_condl/summable_mlet.
Qed.

Lemma ( : {distr U / R}) :
\P_[dmargin f mu] E = \P_[mu] [pred | f x \in E].

Proof.

by rewrite /dmargin pr_dlet pr_exp; apply/eq_exp=> x _; rewrite pr_dunit.
Qed.

Lemma :
(forall , x \in dinsupp mu -> x \notin A) -> \P_[mu] A = 0.

Proof.

move=> h; apply/psum_eq0=> x; apply/eqP.
rewrite mulf_eq0 orbC; case/boolP: (mu x == 0) => //=.
by move/h; rewrite -topredE /= => /negbTE->.
Qed.

Lemma :
(forall , x \in dinsupp mu -> x \in B -> x \notin A)
-> \P_[mu, B] A = 0.

Proof.

move=> h; rewrite /prc eq0_pr ?mul0r // => x /h {h} /orb_idl.
by rewrite negb_and /= => <-; rewrite orbAC orbN.
Qed.

Lemma : {subset B <= A} -> \P_[mu] B <= \P_[mu] A.

Proof.

move=> le_BA; apply/le_psum; last first.
apply/summableMl => //; exists 1=> // x.
by rewrite ger0_norm ?(ler0n, lern1) ?leq_b1.
move=> x; rewrite mulr_ge0 ?ler0n ?ler_wpM2r //.
rewrite ler_nat; have := le_BA x; rewrite -!topredE /=.
by case: (B x) => // ->.
Qed.

Lemma : \P_[mu] A <= 1.

Proof.

apply/(@le_trans _ _ \P_[mu] predT).
by apply/subset_pr. by rewrite pr_predT le1_mu.
Qed.

Lemma : \E?_[mu] f1 -> \E?_[mu] f2 ->
f1 <=1 f2 -> \E_[mu] f1 <= \E_[mu] f2.

Proof.

move=> sm1 sm2 le_f; apply/le_sum => //.
by move=> x; rewrite ler_wpM2r.
Qed.

Lemma :
(forall , x \in dinsupp mu -> x \in E1 -> x \in E2) ->
\P_[mu] E1 <= \P_[mu] E2.

Proof.

move=> le; rewrite /pr; apply/le_psum; last by apply/summable_pr.
move=> x; rewrite mulr_ge0 ?ler0n //=; case/boolP: (x \in dinsupp mu).
move/le; rewrite -!topredE /= => E12; rewrite ler_wpM2r //.
by rewrite ler_nat; case: (E1 x) E12 => // ->.
by move/dinsuppPn=> ->; rewrite !mulr0.
Qed.

Lemma :
(forall , x \in dinsupp nu -> x \in A -> nu x <= mu x)
-> \P_[nu] A <= \P_[mu] A.

Proof.

move=> h; apply/le_psum; last by apply/summable_pr.
move=> x; rewrite mulr_ge0 ?ler0n //=.
case/boolP: (x \in dinsupp nu) => [/h {}h|]; last first.
by move/dinsuppPn=> ->; rewrite mulr0 mulr_ge0 ?ler0n.
by case/boolP: (A x) => [/h|]; rewrite ?(mul0r, mul1r).
Qed.

Lemma : \P_[mu, B] A <= 1.

Proof.

have := ge0_pr B mu; rewrite /prc le_eqVlt.
case/orP=> [/eqP<-|]; first by rewrite invr0 mulr0 ler01.
by move/ler_pdivrMr=> ->; rewrite mul1r le_in_pr // => x _ /andP[].
Qed.

Lemma : 0 < \P_[mu] A ->
PosSum.psum (fun => \P_[mu, A] (pred1 x)) = 1.

Proof.

move=> gt0_pE; rewrite psumZr ?(invr_ge0, ge0_pr) //.
rewrite (eq_psum (F2 := (fun => (A x)%:R * mu x))); last first.
  by rewrite divff // gt_eqF.
move=> x /=; rewrite /pr (psum_finseq (r := [:: x])) ?big_seq1 //=.
  move=> y; rewrite !inE; case: (y == x) => //=.
  by rewrite mul0r eqxx.
by rewrite !inE eqxx -topredE ger0_norm ?mulr_ge0 ?ler0n.
Qed.

Lemma : \P_[mu] E = 0 -> forall , x \in E -> mu x = 0.

Proof.

move/eq0_psum=> /(_ (summable_pr _ _)) => h x xE; move/(_ x): h.
by move: xE; rewrite -topredE /= => ->; rewrite mul1r.
Qed.

Lemma :
\P_[mu] A = \P_[mu] [predI A & B] + \P_[mu] [predI A & predC B].

Proof.

rewrite {1}/pr (psumID B); first by apply/summable_pr.
congr (_ + _); apply/eq_psum => x; rewrite !inE -!topredE /=;
by rewrite mulrA -natrM mulnb andbC.
Qed.

Lemma ( : pred T) ( : {distr T / R}) :
(forall , x \in A -> x \notin B) ->
\P_[mu] [predU A & B] = \P_[mu] A + \P_[mu] B.

Proof.

move=> dsj; rewrite /pr -psumD; try solve [
by apply/summable_pr | by move=> x; rewrite mulr_ge0 ?ler0n
].
apply/eq_psum=> x /=; rewrite -mulrDl -!topredE /= -natrD.
case/boolP: (A x) => Ax; case/boolP: (B x) => Bx //=.
by move/dsj: Ax; rewrite -topredE /= Bx.
Qed.

Lemma ( : seq U) : uniq r ->
\P_[mu] [pred | f x \in r]
= \sum_( <- r) \P_[mu] [pred | f x == y].

Proof.

elim: r => [_|y r ih]; first by rewrite big_nil pr_pred0_eq //.
case/andP=> yNr /ih {ih}h; rewrite big_cons -h -pr_or_indep.
by move=> x; rewrite !inE => /eqP->. by apply/eq_pr.
Qed.

Lemma ( : seq T) : uniq r ->
\P_[mu] [pred | x \in r] = \sum_( <- r) mu x.

Proof.

elim: r => [_|y r ih]; first by rewrite big_nil pr_pred0_eq //.
case/andP=> yNr /ih {ih}h; rewrite big_cons /= pr_pred1.
by rewrite -h -pr_or_indep // => x /eqP ->.
Qed.

Lemma ( : I -> pred T) ( : seq I) :
    uniq r
  -> (forall , p1 != p2 -> p1 \in r -> p2 \in r -> x \in P p1 -> x \notin P p2)
  -> \P_[mu] [pred | has [pred | x \in P p] r]
  = \sum_( <- r) \P_[mu] (P p).

Proof.

move=> uq_r dj; pose S := \big[orb/false]_( <- r) (x \in P p).
rewrite (eq_pr (B := S)) => [x|]; first by rewrite !inE -big_has.
rewrite {}/S; elim: r uq_r dj => [_|p r ih /andP[pNr /ih {ih}h]] dj.
  by rewrite big_nil pr_pred0_eq // => x; rewrite big_nil.
rewrite big_cons -h => [p1 p2 x ne_p p1r p2r|].
  by apply/dj=> //; rewrite in_cons (p1r, p2r) orbT.
rewrite -pr_or_indep => [x xNPp|].
  rewrite -topredE /= big_has; apply/hasPn => y y_in_r.
  apply/(dj p); rewrite ?in_cons ?(eqxx, y_in_r, orbT) //.
  by apply/contra: pNr=> /eqP->.
by apply/eq_pr=> x; rewrite -!topredE /= big_cons.
Qed.

Lemma : \P_[mu] [predU A & B] =
\P_[mu] A + \P_[mu] B - \P_[mu] [predI A & B].

Proof.

apply/eqP; rewrite eq_sym subr_eq [in X in _==X]addrC; apply/eqP.
rewrite (prID _ B) -addrA -pr_or_indep => [x|].
by rewrite !inE => /andP[].
congr (_ + _); apply/eq_pr => x; rewrite !inE -!topredE /=.
by apply/orb_id2r => /negbTE ->; rewrite andbT.
Qed.

Lemma : \P_[mu] [predI A & B] =
\P_[mu] A + \P_[mu] B - \P_[mu] [predU A & B].

Proof.

by rewrite pr_or subKr. Qed.

Lemma :
\P_[mu] [predU A & B] <= \P_[mu] A + \P_[mu] B.

Proof.

by rewrite pr_or lerBlDr lerDl ge0_pr. Qed.

Lemma :
\P_[mu] [predI A & B] <= \P_[mu] A + \P_[mu] B.

Proof.

by rewrite pr_and lerBlDr lerDl ge0_pr. Qed.

Lemma : \P_[mu](predC E) = \P_[mu] predT - \P_[mu] E.

Proof.

apply/esym/eqP; rewrite subr_eq -pr_or_indep //.
by apply/eqP/eq_pr=> x; rewrite !inE orNb.
Qed.

Lemma : \P_[mu] A =
\P_[mu] B * \P_[mu, B] A
+ \P_[mu] (predC B) * \P_[mu, predC B] A.

Proof.

suff h A' B': \P_[mu] [predI A' & B'] = \P_[mu] B' * \P_[mu, B'] A'.
by rewrite (prID _ B); congr (_ + _); apply/h.
rewrite /prc mulrCA; have [] := eqVneq (\P_[mu] B') 0; last first.
by move=> nzPB'; rewrite divff // mulr1.
move=> zPB'; rewrite zPB' invr0 !mulr0; apply/eq0_pr.
move=> x mux; move/pr_eq0: zPB' => /(_ x) h; rewrite !inE.
by apply/negP=> /andP[_ /h] /dinsuppP.
Qed.

Lemma : \E?_[mu] f -> \E_[mu] f =
    \P_[mu]        A  * \E_[mu,       A] f
  + \P_[mu] (predC A) * \E_[mu, predC A] f.
Proof using Type.
Lemma :
  (exists , forall , `|f x| < M) -> \E?_[mu] f.

Proof.

                          (* TO BE REMOVED *)
case=> M ltM; rewrite /has_esp; apply/summable_seqP.
exists (Num.max M 0); first by rewrite le_max lexx orbT.
move=> J uqJ; apply/(@le_trans _ _ (\sum_( <- J) M * mu j)).
  apply/ler_sum=> j _; rewrite normrM [X in _*X]ger0_norm //.
  by apply/ler_wpM2r=> //; apply/ltW.
case: (ltrP M 0) => [lt0_M|ge0_M].
  rewrite ?(ltW lt0_M) // -mulr_sumr.
  by rewrite nmulr_rle0 //; apply/sumr_ge0.
by rewrite -mulr_sumr ler_piMr // -pr_mem ?le1_pr.
Qed.

Lemma :
(exists , forall , `|F x| <= M) -> \E?_[mu] F.

Proof.

by move=> leM; apply/summableMl. Qed.

Lemma : summable F -> \E?_[mu] F.

Proof.

move=> smF; apply/summableMr => //; exists 1.
by move=> x; rewrite ger0_norm // le1_mu1.
Qed.

Lemma ( : R) :
0 <= M -> (forall , `|F x| <= M) -> \E_[mu] F <= M.

Proof.

move=> ge0M bd; apply/(@le_trans _ _ (\E_[mu] (fun _ => M))).
+ apply/le_exp.
  + by apply/bounded_has_exp; exists M.
  + by apply/has_expC.
  + by move=> x; apply/(le_trans _ (bd x))/ler_norm.
by rewrite exp_cst ler_piMl // le1_pr.
Qed.

Lemma ( : T -> {distr U / R}) :
  (forall , \E?_[eta] F) ->
    \E_[dlet nu mu] F = \E_[mu] (fun => \E_[nu x] F).
Proof using Type*. End PrTheory.

#[deprecated(since="1.17.0", note="use `pr_dlet` instead")]
Notation := pr_dlet (only parsing).

#[deprecated(since="mathcomp-analysis 0.6.2",
  note="lacks proof, use __admitted__exp_split explicitly if you really want to use this lemma")]
Notation := __admitted__exp_split.
#[deprecated(since="mathcomp-analysis 0.6.2",
  note="lacks proof, use __admitted__exp_dlet explicitly is you really want to use this lemma")]
Notation := __admitted__exp_dlet.

Section Jensen.
Context { : realType} { : finType}.

Definition ( : \bar R) ( : R -> R) :=
  forall , (a <= x%:E <= b)%E -> (a <= y%:E <= b)%E ->
    forall , 0 <= t <= 1 ->
      f (t * x + (1 - t) * y) <= t * (f x) + (1 - t) * (f y).

Notation f := (convexon -oo +oo f).

Section Jensen.
Context ( : R -> R) ( : I -> R).

Hypothesis : convex f.
Hypothesis : forall , 0 <= l x.
Hypothesis : \sum_ (l i) = 1.

Lemma : f (\sum_ (l i * x i)) <= \sum_ (l i * f (x i)).

Proof.

case: (index_enum I) eq1_l => [|i s]; rewrite ?(big_nil, big_cons).
  by move/esym/eqP; rewrite oner_eq0.
elim: {i} s (l i) (ge0_l i) (x i) => [|j s ih] li ge0_li xi.
  by rewrite !big_nil !addr0 => ->; rewrite !mul1r.
rewrite !big_cons; have := ge0_l j; rewrite le_eqVlt.
case/orP => [/eqP<-|gt0_lj].
  by rewrite !Monoid.simpm /= !Monoid.simpm; apply/ih.
rewrite !addrA => eq1; pose z := (li * xi + l j * x j) / (li + l j).
have nz_lij: li + l j != 0 by rewrite gt_eqF ?ltr_wpDl.
have/ih := eq1 => -/(_ _ z); rewrite [_ * (_ / _)]mulrC.
rewrite mulfVK // => {}ih; apply/(le_trans (ih _)).
  by rewrite addr_ge0 ?ge0_l.
rewrite lerD2r {ih}/z [_ / _]mulrDl ![_*_/_]mulrAC.
set c1 : R := _ / _; set c2 : R := _ / _; have eqc2: c2 = 1 - c1.
  apply/(mulfI nz_lij); rewrite mulrBr mulr1 ![(li + l j)*_]mulrC.
  by apply/eqP; rewrite !mulfVK // eq_sym subr_eq addrC.
set c := (li + l j); pose z := (c * c1 * f xi + c * c2 * f (x j)).
apply/(@le_trans _ _ z); last by rewrite /z ![_*(_/_)]mulrC !mulfVK.
rewrite {}/z -![c * _ * _]mulrA -mulrDr ler_wpM2l ?addr_ge0 //.
rewrite eqc2 cvx_f // ?leNye ?leey // divr_ge0 ?addr_ge0 //=.
by rewrite ler_pdivrMr ?mul1r ?lerDl ?ltr_wpDl.
Qed.

End Jensen.
End Jensen.

Notation f := (convexon \-inf \+inf f).

Files

Module mathcomp.experimental_reals.distr