Distribution have a sub probability measures

_CoqProject

@@ -152,6 +152,7 @@ theories/probability_theory/poisson_distribution.v
 theories/probability_theory/beta_distribution.v
 theories/probability_theory/probability.v
 theories/probability_theory/independence.v
+theories/probability_theory/counting_distr.v
 
 theories/convex.v
 theories/charge.v

classical/classical_sets.v

@@ -2229,6 +2229,9 @@ End bigop_lemmas.
 Arguments bigcup_setD1 {T I} x.
 Arguments bigcap_setD1 {T I} x.
 
+Lemma bigcup_id {T: Type} (P: set T) : \bigcup_(i in P) [set i] = P.
+Proof.  by rewrite bigcup_imset1 // image_id. Qed.
+
 Lemma setD_bigcup {T} (I : eqType) (F : I -> set T) (P : set I) (j : I) : P j ->
   F j `\` \bigcup_(i in [set k | P k /\ k != j]) (F j `\` F i) =
   \bigcap_(i in P) F i.

reals/constructive_ereal.v

@@ -529,7 +529,7 @@ HB.instance Definition _ := Order.hasTop.Build ereal_display (\bar R) leey.
 End ERealOrder_realDomainType.
 
 Section ERealZmodule.
-Context {R : zmodType}.
+Context {R : baseZmodType}.
 Implicit Types x y z : \bar R.
 
 Definition oppe x :=
@@ -1190,6 +1190,13 @@ Lemma fin_numM x y : x \is a fin_num -> y \is a fin_num ->
   x * y \is a fin_num.
 Proof. by move: x y => [x| |] [y| |]. Qed.
 
+Lemma fin_numMK (a b : \bar R):
+  fine (a * b) = (fine a * fine b)%R.
+Proof.
+by case: a => [r| |]; case: b => [s| |]//=;
+rewrite /mule/= ?mulr0 ?mul0r//; do ![case: ifPn => //= _].
+Qed.
+
 Lemma prode_fin_num (I : Type) (s : seq I) (P : pred I) (f : I -> \bar R) :
   (forall i, P i -> f i \is a fin_num) ->
   \prod_(i <- s | P i) f i \is a fin_num.

theories/esum.v

@@ -399,6 +399,11 @@ rewrite funenegN (@ge0_funeposE _ _ B)// => y By; apply: f0.
 by case: AB => _; exact.
 Qed.
 
+Lemma esum_abse (f : T -> R) :
+  (forall i, 0 <= f i)%R ->
+  (\esum_(x in [set: T]) (f x)%:E = \esum_(x in [set: T]) `|(f x)%:E|)%E.
+Proof. by move => ?; apply eq_esum => ?? ; rewrite gee0_abs // lee_tofin. Qed.
+
 End esum.
 Arguments eq_esum {R T} A f g.
 
@@ -603,9 +608,10 @@ Qed.
 Arguments infinite_esum_cst {R T} c.
 
 Section esumZ.
-Context {R : realType} {T : choiceType} (A : set T) (f : T -> \bar R).
+Context {R : realType} {T : choiceType} (A : set T).
 
-Let ge0_esumZ c : 0 <= c -> (forall t, A t -> 0 <= f t) ->
+Let ge0_esumZ c (f : T -> \bar R) :
+  0 <= c -> (forall t, A t -> 0 <= f t) ->
   \esum_(t in A) c * f t = c * \esum_(t in A) f t.
 Proof.
 rewrite le_eqVlt => /predU1P[<- _|c0 f0].
@@ -614,7 +620,8 @@ rewrite [in LHS]ge0_esum; first by move=> x /f0 ax0; rewrite ?mule_ge0// ltW.
 by rewrite ge0_esum//; apply: PosEsum.pos_esumZ => //; exact: ltW.
 Qed.
 
-Lemma esumZ c : (forall x, A x -> 0 <= f x) ->
+Lemma esumZ c (f : T -> \bar R) :
+  (forall x, A x -> 0 <= f x) ->
   \esum_(x in A) c * f x = c * \esum_(x in A) f x.
 Proof.
 move=> h; rewrite (eq_esum _ _ (fun x => esg c * (`|c| * f x))).
@@ -632,6 +639,15 @@ transitivity (esg c * \esum_(x in A) `|c| * f x).
 by rewrite (eq_esum _ _ (fun x => `|c| * f x))// ge0_esumZ// muleA -numEesg.
 Qed.
 
+Lemma EFin_esumZ (c : R) (f : T -> R) :
+  (0 <= c)%R -> (forall i, 0 <= f i)%R ->
+  \esum_(i in A) (c * f i)%:E = (c%:E * \esum_(i in A) (f i)%:E)%E.
+Proof.
+  move=> c0 a0; rewrite -esumZ.
+- by move=> i ?; rewrite lee_fin; exact: a0.
+- by apply: eq_esum => i _; rewrite EFinM.
+Qed.
+
 End esumZ.
 
 Lemma esumD {R : realType} {T : choiceType} (I : set T) (f g : T -> \bar R) :

theories/hoelder.v

@@ -24,7 +24,8 @@ From mathcomp Require Import numfun exp real_measure lebesgue_integral.
 (* Lp-spaces and properties of Lp-norms:                                      *)
 (*                                                                            *)
 (* ```                                                                        *)
-(*    finite_norm mu p f := the L-norm of real-valued function f is finite    *)
+(*    finite_norm mu p f := the L-norm of extended real-valued function f is  *)
+(*                          finite    *)
 (*                          The parameter p is an extended real.              *)
 (*        LfunType mu p1 == type of measurable functions f with a finite      *)
 (*                          L-norm                                            *)
@@ -785,15 +786,15 @@ Qed.
 End minkowski.
 
 Definition finite_norm d (T : measurableType d) (R : realType)
-    (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) :=
-  ('N[ mu ]_p [ EFin \o f ] < +oo)%E.
+    (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> \bar R) :=
+  ('N[ mu ]_p [ f ] < +oo)%E.
 
 Import MeasurableR.
 
 HB.mixin Record isLfunction d (T : measurableType d) (R : realType)
     (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) (f : T -> R)
   & @MeasurableFun d _ T R f := {
-  Lfunction_finite : finite_norm mu p f
+  Lfunction_finite : finite_norm mu p (EFin \o f)
 }.
 
 #[short(type=LfunType)]
@@ -865,7 +866,7 @@ Import numFieldNormedType.Exports HBNNSimple.
 HB.mixin Record isFinLebesgue d (T : measurableType d) (R : realType)
     (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E)
     (f : {mfun_ mu, T >-> R}) := {
-  Lebesgue_finite : finite_norm mu p f
+  Lebesgue_finite : finite_norm mu p (EFin \o f)
 }.
 
 #[short(type=LspaceType)]
@@ -896,7 +897,7 @@ Section Lfun_pred.
 Context {d} {T : measurableType d} {R : realType}
   (mu : {measure set T -> \bar R}) (p : \bar R).
 
-Definition finLfun : {pred _ -> _} := mem [set f | finite_norm mu p f].
+Definition finLfun : {pred _ -> _} := mem [set f : T -> R | finite_norm mu p (EFin \o f)].
 Definition Lfun : {pred _ -> _} := [predI @mfun _ _ T R & finLfun].
 Definition Lfun_key : pred_key Lfun. Proof. exact. Qed.
 Canonical Lfun_keyed := KeyedPred Lfun_key.

theories/numfun.v

@@ -768,6 +768,20 @@ rewrite funeqE => x /=; rewrite !fctE/=; have [fx0|/ltW fx0] := leP (f x) 0.
   by move: fx0; rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0.
 Qed.
 
+Lemma le_funrpos f x: `|f^\+ x| <= `|f x|.
+Proof.
+rewrite ger0_norm ?funrpos_ge0//.
+have := funrposDneg f => /(congr1 (fun g => g x)); rewrite /= => <-.
+by rewrite lerDl funrneg_ge0.
+Qed.
+
+Lemma le_funrneg f x: `|f^\- x| <= `|f x|.
+Proof.
+rewrite ger0_norm ?funrneg_ge0//.
+have := funrposDneg f => /(congr1 (fun g => g x)); rewrite /= => <-.
+by rewrite lerDr funrpos_ge0.
+Qed.
+
 Lemma funrposBneg f : f^\+ - f^\- = f.
 Proof.
 apply/funext => x.