] -> P. Proof. by case: asboolP. Qed. +Lemma orW A B : A \/ B -> A + B. +Proof. +have [|NA] := asboolP A; first by left. +have [|NB] := asboolP B; first by right. +by move=> AB; exfalso; case: AB. +Qed. + +Lemma or3W A B C : [\/ A, B | C] -> A + B + C. +Proof. +have [|NA] := asboolP A; first by left; left. +have [|NB] := asboolP B; first by left; right. +have [|NC] := asboolP C; first by right. +by move=> ABC; exfalso; case: ABC. +Qed. + +Lemma or4W A B C D : [\/ A, B, C | D] -> A + B + C + D. +Proof. +have [|NA] := asboolP A; first by left; left; left. +have [|NB] := asboolP B; first by left; left; right. +have [|NC] := asboolP C; first by left; right. +have [|ND] := asboolP D; first by right. +by move=> ABCD; exfalso; case: ABCD. +Qed. + (* Shall this be a coercion ?*) Lemma asboolT (P : Prop) : P -> `[
].
Proof. by case: asboolP. Qed.
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index 2123c01bc..8e3c63d07 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -1242,6 +1242,13 @@ Notation bigcupM1l := bigcupX1l (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to bigcupX1r.")]
Notation bigcupM1r := bigcupX1r (only parsing).
+Lemma set_cst {T I} (x : T) (A : set I) :
+ [set x | _ in A] = if A == set0 then set0 else [set x].
+Proof.
+apply/seteqP; split=> [_ [i +] <-|t]; first by case: ifPn => // /eqP ->.
+by case: ifPn => // /set0P[i Ai ->{t}]; exists i.
+Qed.
+
Section set_order.
Import Order.TTheory.
@@ -1532,6 +1539,9 @@ Proof. by move=> b [x [Aa Ba <-]]; split; apply: imageP. Qed.
Lemma nonempty_image f A : f @` A !=set0 -> A !=set0.
Proof. by case=> b [a]; exists a. Qed.
+Lemma image_nonempty f A : A !=set0 -> f @` A !=set0.
+Proof. by move=> [x] Ax; exists (f x), x. Qed.
+
Lemma image_subset f A B : A `<=` B -> f @` A `<=` f @` B.
Proof. by move=> AB _ [a Aa <-]; exists a => //; apply/AB. Qed.
@@ -1654,6 +1664,8 @@ Proof. by rewrite preimage_false; under eq_fun do rewrite inE. Qed.
End image_lemmas.
Arguments sub_image_setI {aT rT f A B} t _.
+Arguments subset_set1 {_ _ _}.
+Arguments subset_set2 {_ _ _ _}.
Lemma image2_subset {aT bT rT : Type} (f : aT -> bT -> rT)
(A B : set aT) (C D : set bT) : A `<=` B -> C `<=` D ->
diff --git a/classical/functions.v b/classical/functions.v
index e74eff13c..6a0aa6ee9 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -2617,6 +2617,11 @@ Lemma fct_sumE (I T : Type) (M : zmodType) r (P : {pred I}) (f : I -> T -> M)
(\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x.
Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed.
+Lemma fct_prodE (I : Type) (T : pointedType) (M : comRingType) r (P : {pred I})
+ (f : I -> T -> M) (x : T) :
+ (\prod_(i <- r | P i) f i) x = \prod_(i <- r | P i) f i x.
+Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed.
+
Lemma mul_funC (T : Type) {R : comSemiRingType} (f : T -> R) (r : R) :
r \*o f = r \o* f.
Proof. by apply/funext => x/=; rewrite mulrC. Qed.
@@ -2635,6 +2640,10 @@ Lemma sumrfctE (T : Type) (K : zmodType) (s : seq (T -> K)) :
\sum_(f <- s) f = (fun x => \sum_(f <- s) f x).
Proof. by apply/funext => x;elim/big_ind2 : _ => // _ a _ b <- <-. Qed.
+Lemma prodrfctE (T : pointedType) (K : comRingType) (s : seq (T -> K)) :
+ \prod_(f <- s) f = (fun x => \prod_(f <- s) f x).
+Proof. by apply/funext => x;elim/big_ind2 : _ => // _ a _ b <- <-. Qed.
+
Lemma opprfctE (T : Type) (K : zmodType) (f : T -> K) : - f = (fun x => - f x).
Proof. by []. Qed.
@@ -2661,6 +2670,10 @@ Proof. by []. Qed.
Definition fctE :=
(cstE, compE, opprfctE, addrfctE, mulrfctE, scalrfctE, exprfctE).
+Lemma natmulfctE (U : pointedType) (K : ringType) (f : U -> K) n :
+ f *+ n = (fun x => f x *+ n).
+Proof. by elim: n => [//|n h]; rewrite funeqE=> ?; rewrite !mulrSr h. Qed.
+
End function_space_lemmas.
Lemma inv_funK T (R : unitRingType) (f : T -> R) : f\^-1\^-1%R = f.
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 6245db399..07ded8460 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -260,6 +260,10 @@ Proof. by case: n => n; rewrite ?invr_ge0 exprn_ge0. Qed.
Lemma exprz_gt0 [R : numDomainType] n (x : R) (hx : 0 < x) : (0 < x ^ n).
Proof. by case: n => n; rewrite ?invr_gt0 exprn_gt0. Qed.
+(**********************)
+(* not yet backported *)
+(**********************)
+
Section num_trunc_floor_ceil.
Context {R : archiNumDomainType}.
Implicit Type x : R.
@@ -470,3 +474,42 @@ Proof. by move=> ? ? []. Qed.
Lemma inl_inj {A B} : injective (@inl A B).
Proof. by move=> ? ? []. Qed.
+
+Lemma eq_exists2l (A : Type) (P P' Q : A -> Prop) :
+ (forall x, P x <-> P' x) ->
+ (exists2 x, P x & Q x) <-> (exists2 x, P' x & Q x).
+Proof.
+by move=> eqQ; split=> -[x p q]; exists x; move: p q; rewrite ?eqQ.
+Qed.
+
+Lemma eq_exists2r (A : Type) (P Q Q' : A -> Prop) :
+ (forall x, Q x <-> Q' x) ->
+ (exists2 x, P x & Q x) <-> (exists2 x, P x & Q' x).
+Proof.
+by move=> eqP; split=> -[x p q]; exists x; move: p q; rewrite ?eqP.
+Qed.
+
+Declare Scope signature_scope.
+Delimit Scope signature_scope with signature.
+
+Import -(notations) Morphisms.
+Arguments Proper {A}%_type R%_signature m.
+Arguments respectful {A B}%_type (R R')%_signature _ _.
+
+Module ProperNotations.
+
+Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature))
+ (right associativity, at level 55) : signature_scope.
+
+Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
+ (right associativity, at level 55) : signature_scope.
+
+Notation " R ~~> R' " := (@respectful _ _ (Program.Basics.flip (R%signature)) (R'%signature))
+ (right associativity, at level 55) : signature_scope.
+
+Export -(notations) Morphisms.
+End ProperNotations.
+
+Lemma mulr_funEcomp (R : semiRingType) (T : Type) (x : R) (f : T -> R) :
+ x \o* f = *%R^~ x \o f.
+Proof. by []. Qed.
diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam
index a0890eb50..ae70c3561 100644
--- a/coq-mathcomp-analysis.opam
+++ b/coq-mathcomp-analysis.opam
@@ -19,6 +19,7 @@ depends: [
"coq-mathcomp-solvable"
"coq-mathcomp-field"
"coq-mathcomp-bigenough" { (>= "1.0.0") }
+ "coq-interval"
]
tags: [
diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v
index 63ca0e73b..9681124ea 100644
--- a/experimental_reals/discrete.v
+++ b/experimental_reals/discrete.v
@@ -21,7 +21,6 @@ Local Open Scope ring_scope.
Local Open Scope real_scope.
Section ProofIrrelevantChoice.
-
Context {T : choiceType}.
Lemma existsTP (P : T -> Prop) : { x : T | P x } + (forall x, ~ P x).
diff --git a/reals/Make b/reals/Make
index f86bfb55d..f3b0b8fa3 100644
--- a/reals/Make
+++ b/reals/Make
@@ -10,7 +10,6 @@
constructive_ereal.v
reals.v
real_interval.v
-signed.v
interval_inference.v
prodnormedzmodule.v
all_reals.v
diff --git a/reals/signed.v b/reals/signed.v
index 6a4a59a14..b5429d00b 100644
--- a/reals/signed.v
+++ b/reals/signed.v
@@ -126,6 +126,7 @@ Attributes deprecated(since="mathcomp-analysis 1.9.0",
(* Canonical instances are also provided according to types, as a *)
(* fallback when no known operator appears in the expression. Look to *)
(* nat_snum below for an example on how to add your favorite type. *)
+(* *)
(******************************************************************************)
Reserved Notation "{ 'compare' x0 & nz & cond }"
diff --git a/theories/Make b/theories/Make
index ab6dede6e..92b57b5ea 100644
--- a/theories/Make
+++ b/theories/Make
@@ -9,6 +9,7 @@
ereal.v
landau.v
+ess_sup_inf.v
topology_theory/topology.v
topology_theory/bool_topology.v
topology_theory/compact.v
@@ -77,6 +78,9 @@ lebesgue_integral_theory/lebesgue_integral.v
ftc.v
hoelder.v
probability.v
+independence.v
+sampling.v
+sampling_wip.v
lebesgue_stieltjes_measure.v
convex.v
charge.v
diff --git a/theories/all_analysis.v b/theories/all_analysis.v
index b567c7690..2a745ee6a 100644
--- a/theories/all_analysis.v
+++ b/theories/all_analysis.v
@@ -25,3 +25,4 @@ From mathcomp Require Export charge.
From mathcomp Require Export kernel.
From mathcomp Require Export pi_irrational.
From mathcomp Require Export gauss_integral.
+From mathcomp Require Export ess_sup_inf.
diff --git a/theories/charge.v b/theories/charge.v
index 8cdeda7e8..6a7362f4d 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -1866,7 +1866,7 @@ have nuf A : d.-measurable A -> nu A = \int[mu]_(x in A) f x.
move=> A mA; rewrite nuf ?inE//; apply: ae_eq_integral => //.
- exact/measurable_funTS.
- exact/measurable_funTS.
-- exact: ae_eq_subset ff'.
+- exact: (@ae_eq_subset _ _ _ _ mu setT A f f' (@subsetT _ A)).
Qed.
End radon_nikodym_sigma_finite.
@@ -2092,6 +2092,10 @@ move=> mE; apply: integral_ae_eq => //.
by rewrite -Radon_Nikodym_SigmaFinite.f_integral.
Qed.
+(* TODO: move back to measure.v, current version incompatible *)
+Lemma ae_eq_mul2l (f g h : T -> \bar R) D : f = g %[ae mu in D] -> (h \* f) = (h \* g) %[ae mu in D].
+Proof. by apply: filterS => x /= /[apply] ->. Qed.
+
Lemma Radon_Nikodym_change_of_variables f E : measurable E ->
nu.-integrable E f ->
\int[mu]_(x in E) (f x * ('d (charge_of_finite_measure nu) '/d mu) x) =
diff --git a/theories/ereal.v b/theories/ereal.v
index 2f7d013e8..c806831d4 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -463,6 +463,21 @@ rewrite lteNl => /ereal_sup_gt[_ [y Sy <-]].
by rewrite lteNl oppeK => xlty; exists y.
Qed.
+Lemma ereal_infEN S : ereal_inf S = - ereal_sup [set - x | x in S].
+Proof. by []. Qed.
+
+Lemma ereal_supN S : ereal_sup [set - x | x in S] = - ereal_inf S.
+Proof. by rewrite oppeK. Qed.
+
+Lemma ereal_infN S : ereal_inf [set - x | x in S] = - ereal_sup S.
+Proof.
+rewrite /ereal_inf; congr (- ereal_sup _) => /=.
+by rewrite image_comp/=; under eq_imagel do rewrite /= oppeK; rewrite image_id.
+Qed.
+
+Lemma ereal_supEN S : ereal_sup S = - ereal_inf [set - x | x in S].
+Proof. by rewrite ereal_infN oppeK. Qed.
+
End ereal_supremum.
Section ereal_supremum_realType.
@@ -523,7 +538,7 @@ Proof.
by move=> Soo; apply/eqP; rewrite eq_le leey/=; exact: ereal_sup_ubound.
Qed.
-Lemma ereal_sup_le S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S.
+Lemma ereal_sup_ge S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S.
Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ubound. Qed.
Lemma ereal_sup_ninfty S : ereal_sup S = -oo <-> S `<=` [set -oo].
@@ -591,11 +606,84 @@ rewrite -ereal_sup_EFin; [|exact/has_lb_ubN|exact/nonemptyN].
by rewrite !image_comp.
Qed.
+Lemma ereal_supP S x :
+ reflect (forall y : \bar R, S y -> y <= x) (ereal_sup S <= x).
+Proof.
+apply/(iffP idP) => [+ y Sy|].
+ by move=> /(le_trans _)->//; rewrite ereal_sup_ge//; exists y.
+apply: contraPP => /negP; rewrite -ltNge -existsPNP.
+by move=> /ereal_sup_gt[y Sy ltyx]; exists y => //; rewrite lt_geF.
+Qed.
+
+Lemma ereal_infP S x :
+ reflect (forall y : \bar R, S y -> x <= y) (x <= ereal_inf S).
+Proof.
+rewrite leeNr; apply/(equivP (ereal_supP _ _)); setoid_rewrite leeNr.
+split=> [ge_x y Sy|ge_x _ [y Sy <-]]; rewrite ?oppeK// ?ge_x//.
+by rewrite -[y]oppeK ge_x//; exists y.
+Qed.
+
+Lemma ereal_sup_gtP S x :
+ reflect (exists2 y : \bar R, S y & x < y) (x < ereal_sup S).
+Proof.
+rewrite ltNge; apply/(equivP negP); rewrite -(rwP (ereal_supP _ _)) -existsPNP.
+by apply/eq_exists2r => y; rewrite (rwP2 negP idP) -ltNge.
+Qed.
+
+Lemma ereal_inf_ltP S x :
+ reflect (exists2 y : \bar R, S y & y < x) (ereal_inf S < x).
+Proof.
+rewrite ltNge; apply/(equivP negP); rewrite -(rwP (ereal_infP _ _)) -existsPNP.
+by apply/eq_exists2r => y; rewrite (rwP2 negP idP) -ltNge.
+Qed.
+
+Lemma ereal_inf_leP S x : S (ereal_inf S) ->
+ reflect (exists2 y : \bar R, S y & y <= x) (ereal_inf S <= x).
+Proof.
+move=> Sinf; apply: (iffP idP); last exact: ereal_inf_le.
+by move=> Sx; exists (ereal_inf S).
+Qed.
+
+Lemma ereal_sup_geP S x : S (ereal_sup S) ->
+ reflect (exists2 y : \bar R, S y & x <= y) (x <= ereal_sup S).
+Proof.
+move=> Ssup; apply: (iffP idP); last exact: ereal_sup_ge.
+by move=> Sx; exists (ereal_sup S).
+Qed.
+
+Lemma lb_ereal_infNy_adherent S e :
+ ereal_inf S = -oo -> exists2 x : \bar R, S x & x < e%:E.
+Proof. by move=> infNy; apply/ereal_inf_ltP; rewrite infNy ltNyr. Qed.
+
+Lemma ereal_sup_real : @ereal_sup R (range EFin) = +oo.
+Proof.
+rewrite hasNub_ereal_sup//; last by exists 0%R.
+by apply/has_ubPn => x; exists (x+1)%R => //; rewrite ltrDl.
+Qed.
+
+Lemma ereal_inf_real : @ereal_inf R (range EFin) = -oo.
+Proof.
+rewrite /ereal_inf [X in ereal_sup X](_ : _ = range EFin); last first.
+ apply/seteqP; split => x/=[y].
+ by move=> [z] _ <- <-; exists (-z)%R.
+ by move=> _ <-; exists (-y%:E); first (by exists (-y)%R); rewrite oppeK.
+by rewrite ereal_sup_real.
+Qed.
+
End ereal_supremum_realType.
#[deprecated(since="mathcomp-analysis 1.3.0", note="Renamed `ereal_sup_ubound`.")]
Notation ereal_sup_ub := ereal_sup_ubound (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="Renamed `ereal_inf_lbound`.")]
Notation ereal_inf_lb := ereal_inf_lbound (only parsing).
+#[deprecated(since="mathcomp-analysis 1.10.0", note="Renamed `ereal_sup_ge`.")]
+Notation ereal_sup_le := ereal_sup_ge.
+
+Arguments ereal_supP {R S x}.
+Arguments ereal_infP {R S x}.
+Arguments ereal_sup_gtP {R S x}.
+Arguments ereal_inf_ltP {R S x}.
+Arguments ereal_sup_geP {R S x}.
+Arguments ereal_inf_leP {R S x}.
Lemma restrict_abse T (R : numDomainType) (f : T -> \bar R) (D : set T) :
(abse \o f) \_ D = abse \o (f \_ D).
diff --git a/theories/ess_sup_inf.v b/theories/ess_sup_inf.v
new file mode 100644
index 000000000..2312636ef
--- /dev/null
+++ b/theories/ess_sup_inf.v
@@ -0,0 +1,343 @@
+From HB Require Import structures.
+From mathcomp Require Import all_ssreflect all_algebra archimedean finmap.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop reals interval_inference ereal.
+From mathcomp Require Import topology normedtype sequences esum numfun.
+From mathcomp Require Import measure lebesgue_measure.
+
+(**md**************************************************************************)
+(* ``` *)
+(* ess_sup f == essential supremum of the function f : T -> R where T is a *)
+(* semiRingOfSetsType and R is a realType *)
+(* ess_inf f == essential infimum *)
+(* ``` *)
+(* *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Import Order.TTheory GRing.Theory Num.Def Num.Theory.
+Import numFieldNormedType.Exports.
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+Local Open Scope ereal_scope.
+
+Section essential_supremum.
+Context d {T : measurableType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Implicit Types (f g : T -> \bar R) (h k : T -> R).
+
+(* TODO: move *)
+Lemma measure0_ae (P : set T) : mu [set: T] = 0 -> \forall x \ae mu, P x.
+Proof. by move=> x; exists setT; split. Qed.
+
+Definition ess_sup f := ereal_inf [set y | \forall x \ae mu, f x <= y].
+
+Lemma ess_supEae (f : T -> \bar R) :
+ ess_sup f = ereal_inf [set y | \forall x \ae mu, f x <= y].
+Proof. by []. Qed.
+
+Lemma ae_le_measureP f y : measurable_fun setT f ->
+ (\forall x \ae mu, f x <= y) <-> (mu (f @^-1` `]y, +oo[) = 0).
+Proof.
+move=> f_meas; have fVroo_meas : d.-measurable (f @^-1` `]y, +oo[).
+ by rewrite -[_ @^-1` _]setTI; apply/f_meas=> //; exact/emeasurable_itv.
+have setCfVroo : (f @^-1` `]y, +oo[) = ~` [set x | f x <= y].
+ by apply: setC_inj; rewrite preimage_setC setCitv/= set_itvxx setU0 setCK.
+split.
+ move=> [N [dN muN0 inN]]; rewrite (subset_measure0 _ dN)// => x.
+ by rewrite setCfVroo; apply: inN.
+set N := (X in mu X) => muN0; exists N; rewrite -setCfVroo.
+by split => //; exact: fVroo_meas.
+Qed.
+
+Lemma ess_supEmu0 (f : T -> \bar R) : measurable_fun setT f ->
+ ess_sup f = ereal_inf [set y | mu (f @^-1` `]y, +oo[) = 0].
+Proof.
+by move=> ?; congr (ereal_inf _); apply/predeqP => r; exact: ae_le_measureP.
+Qed.
+
+Lemma ess_sup_ge f : \forall x \ae mu, f x <= ess_sup f.
+Proof.
+rewrite ess_supEae//; set I := (X in ereal_inf X).
+have [->|IN0] := eqVneq I set0.
+ by rewrite ereal_inf0; apply: nearW => ?; rewrite leey.
+have [u uI uinf] := ereal_inf_seq IN0.
+rewrite -(cvg_lim _ uinf)//; near=> x.
+rewrite lime_ge//; first by apply/cvgP: uinf.
+by apply: nearW; near: x; apply/ae_foralln => n; apply: uI.
+Unshelve. all: by end_near. Qed.
+
+Lemma ess_supP f a : reflect (\forall x \ae mu, f x <= a) (ess_sup f <= a).
+Proof.
+apply: (iffP (ereal_inf_leP _)) => /=; last 2 first.
+- by move=> [y fy ya]; near do apply: le_trans ya.
+- by move=> fa; exists a.
+by rewrite -ess_supEae//; exact: ess_sup_ge.
+Unshelve. all: by end_near. Qed.
+
+Lemma le_ess_sup f g : (\forall x \ae mu, f x <= g x) -> ess_sup f <= ess_sup g.
+Proof.
+move=> fg; apply/ess_supP => //.
+near do rewrite (le_trans (near fg _ _))//=.
+exact: ess_sup_ge.
+Unshelve. all: by end_near. Qed.
+
+Lemma eq_ess_sup f g : (\forall x \ae mu, f x = g x) -> ess_sup f = ess_sup g.
+Proof.
+move=> fg; apply/eqP; rewrite eq_le !le_ess_sup//=;
+ by apply: filterS fg => x ->.
+Qed.
+
+Lemma ess_sup_cst r : 0 < mu [set: T] -> ess_sup (cst r) = r.
+Proof.
+move=> muT_gt0; apply/eqP; rewrite eq_le; apply/andP; split.
+ by apply/ess_supP => //; apply: nearW.
+have ae_proper := ae_properfilter_algebraOfSetsType muT_gt0.
+by near (almost_everywhere mu) => x; near: x; apply: ess_sup_ge.
+Unshelve. all: by end_near. Qed.
+
+Lemma ess_sup_ae_cst f r : 0 < mu [set: T] ->
+ (\forall x \ae mu, f x = r) -> ess_sup f = r.
+Proof. by move=> muT_gt0 /= /eq_ess_sup->; rewrite ess_sup_cst. Qed.
+
+Lemma ess_sup_gee f y : 0 < mu [set: T] ->
+ (\forall x \ae mu, y <= f x)%E -> y <= ess_sup f.
+Proof. by move=> *; rewrite -(ess_sup_cst y)//; apply: le_ess_sup. Qed.
+
+Lemma abs_sup_eq0_ae_eq f : ess_sup (abse \o f) = 0 -> f = \0 %[ae mu].
+Proof.
+move=> ess_sup_f_eq0; near=> x => _ /=; apply/eqP.
+rewrite -abse_eq0 eq_le abse_ge0 andbT; near: x.
+by apply/ess_supP; rewrite ess_sup_f_eq0.
+Unshelve. all: by end_near. Qed.
+
+Lemma abs_ess_sup_eq0 f : mu [set: T] > 0 ->
+ f = \0 %[ae mu] -> ess_sup (abse \o f) = 0.
+Proof.
+move=> muT_gt0 f0; apply/eqP; rewrite eq_le; apply/andP; split.
+ by apply/ess_supP => /=; near do rewrite (near f0 _ _)//= normr0//.
+by rewrite -[0]ess_sup_cst// le_ess_sup//=; near=> x; rewrite abse_ge0.
+Unshelve. all: by end_near. Qed.
+
+Lemma ess_sup_pZl f (a : R) : (0 < a)%R ->
+ ess_sup (cst a%:E \* f) = a%:E * ess_sup f.
+Proof.
+move=> /[dup] /ltW a_ge0 a_gt0.
+gen have esc_le : a f a_ge0 a_gt0 /
+ (ess_sup (cst a%:E \* f) <= a%:E * ess_sup f)%E.
+ by apply/ess_supP; near do rewrite /cst/= lee_pmul2l//; apply/ess_supP.
+apply/eqP; rewrite eq_le esc_le// -lee_pdivlMl//=.
+apply: le_trans (esc_le _ _ _ _); rewrite ?invr_gt0 ?invr_ge0//.
+by under eq_fun do rewrite muleA -EFinM mulVf ?mul1e ?gt_eqF//.
+Unshelve. all: by end_near. Qed.
+
+Lemma ess_supZl f (a : R) : mu [set: T] > 0 -> (0 <= a)%R ->
+ ess_sup (cst a%:E \* f) = a%:E * ess_sup f.
+Proof.
+move=> muTN0; case: ltgtP => // [a_gt0|<-] _; first exact: ess_sup_pZl.
+by under eq_fun do rewrite mul0e; rewrite mul0e ess_sup_cst.
+Qed.
+
+Lemma ess_sup_eqNyP f : ess_sup f = -oo <-> \forall x \ae mu, f x = -oo.
+Proof.
+rewrite (rwP eqP) -leeNy_eq (eq_near (fun=> rwP eqP)).
+by under eq_near do rewrite -leeNy_eq; apply/(rwP2 idP (ess_supP _ _)).
+Qed.
+
+Lemma ess_supD f g : ess_sup (f \+ g) <= ess_sup f + ess_sup g.
+Proof.
+by apply/ess_supP; near do rewrite lee_add//; apply/ess_supP.
+Unshelve. all: by end_near. Qed.
+
+Lemma ess_sup_absD f g :
+ ess_sup (abse \o (f \+ g)) <= ess_sup (abse \o f) + ess_sup (abse \o g).
+Proof.
+rewrite (le_trans _ (ess_supD _ _))// le_ess_sup//.
+by apply/nearW => x; apply/lee_abs_add.
+Qed.
+
+End essential_supremum.
+Arguments ess_sup_ae_cst {d T R mu f}.
+Arguments ess_supP {d T R mu f a}.
+
+Section real_essential_supremum.
+Context d {T : measurableType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Implicit Types f : T -> R.
+
+Notation ess_supr f := (ess_sup mu (EFin \o f)).
+
+Lemma ess_supr_bounded f : ess_supr f < +oo ->
+ exists M, \forall x \ae mu, (f x <= M)%R.
+Proof.
+set g := EFin \o f => ltfy; have [|supfNy] := eqVneq (ess_sup mu g) -oo.
+ by move=> /ess_sup_eqNyP fNy; exists 0%:R; apply: filterS fNy.
+have supf_fin : ess_supr f \is a fin_num by case: ess_sup ltfy supfNy.
+by exists (fine (ess_supr f)); near do rewrite -lee_fin fineK//; apply/ess_supP.
+Unshelve. all: by end_near. Qed.
+
+Lemma ess_sup_eqr0_ae_eq f : ess_supr (normr \o f) = 0 -> f = 0%R %[ae mu].
+Proof.
+under [X in ess_sup _ X]eq_fun do rewrite /= -abse_EFin.
+move=> /abs_sup_eq0_ae_eq; apply: filterS => x /= /(_ _)/eqP.
+by rewrite eqe => /(_ _)/eqP.
+Qed.
+
+Lemma ess_suprZl f (y : R) : mu setT > 0 -> (0 <= y)%R ->
+ ess_supr (cst y \* f)%R = y%:E * ess_supr f.
+Proof. by move=> muT_gt0 r_ge0; rewrite -ess_supZl. Qed.
+
+Lemma ess_sup_ger f x : 0 < mu [set: T] -> (forall t, x <= (f t)%:E) ->
+ x <= ess_supr f.
+Proof. by move=> muT f0; apply/ess_sup_gee => //=; apply: nearW. Qed.
+
+Lemma ess_sup_ler f y : (forall t, (f t)%:E <= y) -> ess_supr f <= y.
+Proof. by move=> ?; apply/ess_supP; apply: nearW. Qed.
+
+Lemma ess_sup_cstr y : (0 < mu setT)%E -> (ess_supr (cst y) = y%:E)%E.
+Proof. by move=> muN0; rewrite (ess_sup_ae_cst y%:E)//=; apply: nearW. Qed.
+
+Lemma ess_suprD f g : ess_supr (f \+ g) <= ess_supr f + ess_supr g.
+Proof. by rewrite (le_trans _ (ess_supD _ _ _)). Qed.
+
+Lemma ess_sup_normD f g :
+ ess_supr (normr \o (f \+ g)) <= ess_supr (normr \o f) + ess_supr (normr \o g).
+Proof.
+rewrite (le_trans _ (ess_suprD _ _))// le_ess_sup//.
+by apply/nearW => x; apply/ler_normD.
+Qed.
+
+End real_essential_supremum.
+Notation ess_supr mu f := (ess_sup mu (EFin \o f)).
+
+Section essential_infimum.
+Context d {T : measurableType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Implicit Types f : T -> \bar R.
+
+Definition ess_inf f := ereal_sup [set y | \forall x \ae mu, y <= f x].
+Notation ess_sup := (ess_sup mu).
+
+Lemma ess_infEae (f : T -> \bar R) :
+ ess_inf f = ereal_sup [set y | \forall x \ae mu, y <= f x].
+Proof. by []. Qed.
+
+Lemma ess_infEN (f : T -> \bar R) : ess_inf f = - ess_sup (\- f).
+Proof.
+rewrite ess_supEae ess_infEae ereal_infEN oppeK; congr (ereal_sup _).
+apply/seteqP; split=> [y /= y_le|_ [/= y y_ge <-]].
+ by exists (- y); rewrite ?oppeK//=; apply: filterS y_le => x; rewrite leeN2.
+by apply: filterS y_ge => x; rewrite leeNl.
+Qed.
+
+Lemma ess_supEN (f : T -> \bar R) : ess_sup f = - ess_inf (\- f).
+Proof.
+by rewrite ess_infEN oppeK; apply/eq_ess_sup/nearW => ?; rewrite oppeK.
+Qed.
+
+Lemma ess_infN (f : T -> \bar R) : ess_inf (\- f) = - ess_sup f.
+Proof. by rewrite ess_supEN oppeK. Qed.
+
+Lemma ess_supN (f : T -> \bar R) : ess_sup (\- f) = - ess_inf f.
+Proof. by rewrite ess_infEN oppeK. Qed.
+
+Lemma ess_infP f a : reflect (\forall x \ae mu, a <= f x) (a <= ess_inf f).
+Proof.
+by rewrite ess_infEN leeNr; apply: (iffP ess_supP);
+ apply: filterS => x; rewrite leeN2.
+Qed.
+
+Lemma ess_inf_le f : \forall x \ae mu, ess_inf f <= f x.
+Proof. exact/ess_infP. Qed.
+
+Lemma le_ess_inf f g : (\forall x \ae mu, f x <= g x) -> ess_inf f <= ess_inf g.
+Proof.
+move=> fg; apply/ess_infP => //.
+near do rewrite (le_trans _ (near fg _ _))//=.
+exact: ess_inf_le.
+Unshelve. all: by end_near. Qed.
+
+Lemma eq_ess_inf f g : (\forall x \ae mu, f x = g x) -> ess_inf f = ess_inf g.
+Proof.
+move=> fg; apply/eqP; rewrite eq_le !le_ess_inf//=;
+ by apply: filterS fg => x ->.
+Qed.
+
+Lemma ess_inf_cst r : 0 < mu [set: T] -> ess_inf (cst r) = r.
+Proof.
+by move=> ?; rewrite ess_infEN (ess_sup_ae_cst (- r)) ?oppeK//=; apply: nearW.
+Qed.
+
+Lemma ess_inf_ae_cst f r : 0 < mu [set: T] ->
+ (\forall x \ae mu, f x = r) -> ess_inf f = r.
+Proof. by move=> muT_gt0 /= /eq_ess_inf->; rewrite ess_inf_cst. Qed.
+
+Lemma ess_inf_gee f y : 0 < mu [set: T] ->
+ (\forall x \ae mu, y <= f x)%E -> y <= ess_inf f.
+Proof. by move=> *; rewrite -(ess_inf_cst y)//; apply: le_ess_inf. Qed.
+
+Lemma ess_inf_pZl f (a : R) : (0 < a)%R ->
+ (ess_inf (cst a%:E \* f) = a%:E * ess_inf f).
+Proof.
+move=> a_gt0; rewrite !ess_infEN muleN; congr (- _)%E.
+by under eq_fun do rewrite -muleN; rewrite ess_sup_pZl.
+Qed.
+
+Lemma ess_infZl f (a : R) : mu [set: T] > 0 -> (0 <= a)%R ->
+ (ess_inf (cst a%:E \* f) = a%:E * ess_inf f).
+Proof.
+move=> muTN0; case: ltgtP => // [a_gt0|<-] _; first exact: ess_inf_pZl.
+by under eq_fun do rewrite mul0e; rewrite mul0e ess_inf_cst.
+Qed.
+
+Lemma ess_inf_eqyP f : ess_inf f = +oo <-> \forall x \ae mu, f x = +oo.
+Proof.
+rewrite (rwP eqP) -leye_eq (eq_near (fun=> rwP eqP)).
+by under eq_near do rewrite -leye_eq; apply/(rwP2 idP (ess_infP _ _)).
+Qed.
+
+Lemma ess_infD f g : ess_inf (f \+ g) >= ess_inf f + ess_inf g.
+Proof.
+by apply/ess_infP; near do rewrite lee_add//; apply/ess_infP.
+Unshelve. all: by end_near. Qed.
+
+End essential_infimum.
+Arguments ess_inf_ae_cst {d T R mu f}.
+Arguments ess_infP {d T R mu f a}.
+
+Section real_essential_infimum.
+Context d {T : measurableType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Implicit Types f : T -> R.
+
+Notation ess_infr f := (ess_inf mu (EFin \o f)).
+
+Lemma ess_infr_bounded f : ess_infr f > -oo ->
+ exists M, \forall x \ae mu, (f x >= M)%R.
+Proof.
+set g := EFin \o f => ltfy; have [|inffNy] := eqVneq (ess_inf mu g) +oo.
+ by move=> /ess_inf_eqyP fNy; exists 0%:R; apply: filterS fNy.
+have inff_fin : ess_infr f \is a fin_num by case: ess_inf ltfy inffNy.
+by exists (fine (ess_infr f)); near do rewrite -lee_fin fineK//; apply/ess_infP.
+Unshelve. all: by end_near. Qed.
+
+Lemma ess_infrZl f (y : R) : mu setT > 0 -> (0 <= y)%R ->
+ ess_infr (cst y \* f)%R = y%:E * ess_infr f.
+Proof. by move=> muT_gt0 r_ge0; rewrite -ess_infZl. Qed.
+
+Lemma ess_inf_ger f x : 0 < mu [set: T] -> (forall t, x <= (f t)%:E) ->
+ x <= ess_infr f.
+Proof. by move=> muT f0; apply/ess_inf_gee => //=; apply: nearW. Qed.
+
+Lemma ess_inf_ler f y : (forall t, y <= (f t)%:E) -> y <= ess_infr f.
+Proof. by move=> ?; apply/ess_infP; apply: nearW. Qed.
+
+Lemma ess_inf_cstr y : (0 < mu setT)%E -> (ess_infr (cst y) = y%:E)%E.
+Proof. by move=> muN0; rewrite (ess_inf_ae_cst y%:E)//=; apply: nearW. Qed.
+
+End real_essential_infimum.
+Notation ess_infr mu f := (ess_inf mu (EFin \o f)).
diff --git a/theories/exp.v b/theories/exp.v
index 230b3c1ab..17ea59abb 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -536,6 +536,9 @@ have /expR_total_gt1[y [H1y H2y H3y]] : 1 <= x^-1 by rewrite ltW // !invf_cp1.
by exists (-y); rewrite expRN H3y invrK.
Qed.
+Lemma norm_expR : normr \o expR = (expR : R -> R).
+Proof. by apply/funext => x /=; rewrite ger0_norm ?expR_ge0. Qed.
+
Local Open Scope convex_scope.
Lemma convex_expR (t : {i01 R}) (a b : R^o) :
expR (a <| t |> b) <= (expR a : R^o) <| t |> (expR b : R^o).
diff --git a/theories/hoelder.v b/theories/hoelder.v
index 06385c4ac..49daef3ef 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -1,19 +1,43 @@
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
-From mathcomp Require Import mathcomp_extra unstable boolp classical_sets.
-From mathcomp Require Import functions cardinality fsbigop reals ereal.
-From mathcomp Require Import topology normedtype sequences real_interval.
-From mathcomp Require Import esum measure lebesgue_measure lebesgue_integral.
-From mathcomp Require Import numfun exp convex interval_inference.
+From mathcomp Require Import mathcomp_extra unstable boolp interval_inference.
+From mathcomp Require Import classical_sets functions cardinality fsbigop reals.
+From mathcomp Require Import ereal topology normedtype sequences real_interval.
+From mathcomp Require Import esum measure ess_sup_inf lebesgue_measure.
+From mathcomp Require Import lebesgue_integral numfun exp convex.
(**md**************************************************************************)
(* # Hoelder's Inequality *)
(* *)
-(* This file provides Hoelder's inequality. *)
+(* This file provides the Lp-norm, Hoelder's inequality and its consequences, *)
+(* most notably Minkowski's inequality, the convexity of the power function, *)
+(* and a definition of Lp-spaces. *)
+(* *)
(* ``` *)
-(* 'N[mu]_p[f] := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1 *)
-(* The corresponding definition is Lnorm. *)
+(* 'N[mu]_p[f] == the Lp-norm of f with measure mu *)
+(* conjugate p == a real number q such that p^-1 + q^-1 = 1 when *)
+(* p is real, otherwise conjugate +oo = 1 and *)
+(* conjugate -oo = 0 *)
+(* ``` *)
+(* *)
+(* Lp-spaces and properties of Lp-norms: *)
+(* *)
+(* ``` *)
+(* finite_norm mu p f := the L-norm of 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 *)
+(* p1 is a proof that the extended real number p is *)
+(* greater or equal to 1. *)
+(* The HB class is Lfun. *)
+(* f \in lfun == holds for f : LfunType mu p1 *)
+(* Lequiv f g == f is equal to g almost everywhere *)
+(* The functions f and g have type LfunType mu p1. *)
+(* Lequiv is made a canonical equivalence relation. *)
+(* LspaceType mu p1 == type of the elements of the Lp space for the *)
+(* measure mu *)
+(* mu.-Lspace p == Lp space as a set *)
(* ``` *)
(* *)
(******************************************************************************)
@@ -33,85 +57,189 @@ Reserved Notation "'N[ mu ]_ p [ F ]"
(* for use as a local notation when the measure is in context: *)
Reserved Notation "'N_ p [ F ]"
(at level 5, F at level 36, format "'[' ''N_' p '/ ' [ F ] ']'").
+Reserved Notation "mu .-Lspace p" (at level 4, format "mu .-Lspace p").
Declare Scope Lnorm_scope.
+Local Open Scope ereal_scope.
HB.lock Definition Lnorm {d} {T : measurableType d} {R : realType}
- (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) :=
+ (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> \bar R) :=
match p with
- | p%:E => (if p == 0%R then
- mu (f @^-1` (setT `\ 0%R))
- else
- (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1)%E
- | +oo%E => (if mu [set: T] > 0 then ess_sup mu (normr \o f) else 0)%E
- | -oo%E => 0%E
+ | p%:E => (\int[mu]_x `|f x| `^ p) `^ p^-1
+ (* (mu (f @^-1` (setT `\ 0%R))) when p = 0? *)
+ | +oo%E => if mu [set: T] > 0 then ess_sup mu (abse \o f) else 0
+ | -oo%E => if mu [set: T] > 0 then ess_inf mu (abse \o f) else 0
end.
Canonical locked_Lnorm := Unlockable Lnorm.unlock.
Arguments Lnorm {d T R} mu p f.
+Local Close Scope ereal_scope.
Section Lnorm_properties.
Context d {T : measurableType d} {R : realType}.
Variable mu : {measure set T -> \bar R}.
Local Open Scope ereal_scope.
-Implicit Types (p : \bar R) (f g : T -> R) (r : R).
+Implicit Types (p : \bar R) (f g : T -> \bar R) (r : R).
Local Notation "'N_ p [ f ]" := (Lnorm mu p f).
-Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E.
+Lemma Lnorm0 p : 1 <= p -> 'N_p[cst 0] = 0.
+Proof.
+rewrite unlock /Lnorm.
+case: p => [r||//].
+- rewrite lee_fin => r1.
+ have r0 : r != 0%R by rewrite gt_eqF// (lt_le_trans _ r1).
+ under eq_integral => x _ do rewrite /= normr0 powR0//.
+ by rewrite integral0 poweR0r// invr_neq0.
+case: ifPn => //mu0 _; rewrite (ess_sup_ae_cst 0)//.
+by apply: nearW => x; rewrite /= normr0.
+Qed.
+
+Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|.
Proof.
-rewrite unlock oner_eq0 invr1// poweRe1//.
- by apply: eq_integral => t _; rewrite powRr1.
-by apply: integral_ge0 => t _; rewrite powRr1.
+rewrite unlock invr1// poweRe1//; under eq_integral do [rewrite poweRe1//=] => //.
+exact: integral_ge0.
Qed.
-Lemma Lnorm_ge0 p f : 0 <= 'N_p[f].
+Lemma Lnorm_abse f p :
+ 'N_p[abse \o f] = 'N_p[f].
Proof.
-rewrite unlock; move: p => [r/=|/=|//].
- by case: ifPn => // r0; exact: poweR_ge0.
-by case: ifPn => // /ess_sup_ge0; apply => t/=.
+rewrite unlock/=.
+have -> : (abse \o (abse \o f)) = abse \o f.
+ by apply: funext => x/=; rewrite abse_id.
+case: p => [r|//|//].
+by under eq_integral => x _ do rewrite abse_id.
Qed.
Lemma eq_Lnorm p f g : f =1 g -> 'N_p[f] = 'N_p[g].
-Proof. by move=> fg; congr Lnorm; exact/funext. Qed.
+Proof. by move=> fg; congr Lnorm; apply/eq_fun => ?; rewrite /= fg. Qed.
-Lemma Lnorm_eq0_eq0 r f : (0 < r)%R -> measurable_fun setT f ->
- 'N_r%:E[f] = 0 -> ae_eq mu [set: T] (fun t => (`|f t| `^ r)%:E) (cst 0).
+Lemma poweR_Lnorm f r : r != 0%R ->
+ 'N_r%:E[f] `^ r = \int[mu]_x (`| f x | `^ r).
Proof.
-move=> r0 mf; rewrite unlock (gt_eqF r0) => /poweR_eq0_eq0 fp.
-apply/ae_eq_integral_abs => //=.
- apply: measurableT_comp => //.
- apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //.
- exact: measurableT_comp.
-under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//.
-by rewrite fp//; apply: integral_ge0 => t _; rewrite lee_fin powR_ge0.
+move=> r0; rewrite unlock -poweRrM mulVf// poweRe1//.
+by apply: integral_ge0 => x _; exact: poweR_ge0.
Qed.
-Lemma powR_Lnorm f r : r != 0%R ->
- 'N_r%:E[f] `^ r = \int[mu]_x (`| f x | `^ r)%:E.
+Lemma oppe_Lnorm f p : 'N_p[\- f]%E = 'N_p[f].
+Proof.
+have NfE : abse \o (\- f) = abse \o f.
+ by apply/funext => x /=; rewrite abseN.
+rewrite unlock /Lnorm NfE; case: p => /= [r|//|//].
+by under eq_integral => x _ do rewrite abseN.
+Qed.
+
+Lemma Lnorm_cst1 r : ('N_r%:E[cst 1] = (mu setT)`^(r^-1)).
+Proof.
+rewrite unlock /Lnorm; under eq_integral do rewrite /= normr1 powR1.
+by rewrite integral_cst// mul1e.
+Qed.
+
+End Lnorm_properties.
+
+Section Lnorm_properties.
+Context d {T : measurableType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Local Open Scope ereal_scope.
+Implicit Types (p : \bar R) (f g : T -> R) (r : R).
+
+Local Notation "'N_ p [ f ]" := (Lnorm mu p (EFin \o f)).
+
+Lemma Lnormr_ge0 p f : 0 <= 'N_p[f].
Proof.
-move=> r0; rewrite unlock (negbTE r0) -poweRrM mulVf// poweRe1//.
-by apply: integral_ge0 => x _; rewrite lee_fin// powR_ge0.
+rewrite unlock; move: p => [r/=|/=|//]; first exact: poweR_ge0.
+- by case: ifPn => // /ess_sup_ger; apply => t/=.
+- by case: ifPn => // muT0; apply/ess_infP/nearW => x /=.
Qed.
+Lemma Lnormr_eq0_eq0 (f : T -> R) p :
+ measurable_fun setT f -> (0 < p)%E -> 'N_p[f] = 0 -> f = 0%R %[ae mu].
+Proof.
+rewrite unlock /Lnorm => mf.
+case: p => [r||//].
+- rewrite lte_fin => r0 /poweR_eq0_eq0 => /(_ (integral_ge0 _ _)) h.
+ have : \int[mu]_x (`|f x| `^ r)%:E = 0.
+ by apply: h => x _; rewrite lee_fin powR_ge0.
+ under eq_integral => x _ do rewrite -[_%:E]gee0_abs ?lee_fin ?powR_ge0//.
+ have mp : measurable_fun [set: T] (fun x : T => (`|f x| `^ r)%:E).
+ apply: measurableT_comp => //.
+ apply (measurableT_comp (measurable_powR _)) => //.
+ exact: measurableT_comp.
+ move/(ae_eq_integral_abs _ measurableT mp).
+ apply: filterS => x/= /[apply].
+ by case=> /powR_eq0_eq0 /eqP; rewrite normr_eq0 => /eqP.
+- case: ifPn => [mu0 _|].
+ move=> /abs_sup_eq0_ae_eq/=.
+ by apply: filterS => x/= /(_ I) /eqP + _; rewrite eqe => /eqP.
+ rewrite ltNge => /negbNE mu0 _ _.
+ suffices mueq0: mu setT = 0 by exact: ae_eq0.
+ by apply/eqP; rewrite eq_le mu0/=.
+Qed.
+
+Lemma powR_Lnorm f r : r != 0%R ->
+ 'N_r%:E[f] `^ r = \int[mu]_x (`| f x | `^ r)%:E.
+Proof. by move=> r0; rewrite poweR_Lnorm. Qed.
+
+Lemma oppr_Lnorm f p : 'N_p[\- f]%R = 'N_p[f].
+Proof. by rewrite -[RHS]oppe_Lnorm. Qed.
+
End Lnorm_properties.
+#[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `Lnormr_ge0`")]
+Notation Lnorm_ge0 := Lnormr_ge0 (only parsing).
+#[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `Lnormr_eq0_eq0`")]
+Notation Lnorm_eq0_eq0 := Lnormr_eq0_eq0 (only parsing).
#[global]
-Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core.
+Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnormr_ge0] : core.
-Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f).
+Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f) : ereal_scope.
Section lnorm.
-(* l-norm is just L-norm applied to counting *)
Context d {T : measurableType d} {R : realType}.
Local Open Scope ereal_scope.
-Local Notation "'N_ p [ f ]" := (Lnorm counting p f).
+(** lp-norm is just Lp-norm applied to counting *)
+Local Notation "'N_ p [ f ]" := (Lnorm counting p (EFin \o f)).
Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R ->
'N_p%:E [f] = (\sum_(k > *)
(* g_sigma_algebraType G == the measurableType corresponding to <> *)
(* This is an HB alias. *)
+(* g_sigma_algebra_preimage f == sigma-algebra generated by the function f *)
+(* g_sigma_algebra_preimageType f == the measurableType corresponding to *)
+(* g_sigma_algebra_preimage f *)
+(* This is an HB alias. *)
+(* f.-preimage.-measurable A == A measurable for g_sigma_algebra_preimage f *)
(* mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets *)
(* ``` *)
(* *)
@@ -273,8 +278,6 @@ From mathcomp Require Import sequences esum numfun.
(* ## More measure-theoretic definitions *)
(* ``` *)
(* m1 `<< m2 == m1 is absolutely continuous w.r.t. m2 or m2 dominates m1 *)
-(* ess_sup f == essential supremum of the function f : T -> R where T is a *)
-(* semiRingOfSetsType and R is a realType *)
(* ``` *)
(* *)
(******************************************************************************)
@@ -282,6 +285,7 @@ From mathcomp Require Import sequences esum numfun.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
+Import ProperNotations.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Reserved Notation "'s<|' D , G '|>'" (at level 40, G, D at next level).
@@ -294,6 +298,9 @@ Reserved Notation "'\d_' a" (at level 8, a at level 2, format "'\d_' a").
Reserved Notation "G .-sigma" (at level 1, format "G .-sigma").
Reserved Notation "G .-sigma.-measurable"
(at level 2, format "G .-sigma.-measurable").
+Reserved Notation "f .-preimage" (at level 1, format "f .-preimage").
+Reserved Notation "f .-preimage.-measurable"
+ (at level 2, format "f .-preimage.-measurable").
Reserved Notation "d .-ring" (at level 1, format "d .-ring").
Reserved Notation "d .-ring.-measurable"
(at level 2, format "d .-ring.-measurable").
@@ -1306,6 +1313,10 @@ move=> A B mA mB; case: (semi_measurableD A B) => // [D [Dfin Dl -> _]].
by apply: fin_bigcup_measurable.
Qed.
+Lemma seqDU_measurable (F : sequence (set T)) :
+ (forall n, measurable (F n)) -> forall n, measurable (seqDU F n).
+Proof. by move=> Fmeas n; apply/measurableD/bigsetU_measurable. Qed.
+
End ringofsets_lemmas.
Section algebraofsets_lemmas.
@@ -1739,6 +1750,17 @@ Lemma preimage_set_system_id {aT : Type} (D : set aT) (F : set (set aT)) :
preimage_set_system D idfun F = setI D @` F.
Proof. by []. Qed.
+Lemma preimage_set_system_compS (aT : Type)
+ d (rT : measurableType d) d' (T : sigmaRingType d')
+ (g : rT -> T) (f : aT -> rT) (D : set aT) :
+ measurable_fun setT g ->
+ preimage_set_system D (g \o f) measurable `<=`
+ preimage_set_system D f measurable.
+Proof.
+move=> mg A; rewrite /preimage_set_system => -[B GB]; exists (g @^-1` B) => //.
+by rewrite -[X in measurable X]setTI; exact: mg.
+Qed.
+
(* f is measurable on the sigma-algebra generated by itself *)
Lemma preimage_set_system_measurable_fun d (aT : pointedType)
(rT : measurableType d) (D : set aT) (f : aT -> rT) :
@@ -1837,6 +1859,58 @@ Notation sigma_algebra_image_class := sigma_algebra_image (only parsing).
#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `g_sigma_preimageE`")]
Notation sigma_algebra_preimage_classE := g_sigma_preimageE (only parsing).
+Definition preimage_display {T T'} : (T -> T') -> measure_display.
+Proof. exact. Qed.
+
+Definition g_sigma_algebra_preimageType d' (T : pointedType)
+ (T' : measurableType d') (f : T -> T') : Type := T.
+
+Definition g_sigma_algebra_preimage d' (T : pointedType)
+ (T' : measurableType d') (f : T -> T') :=
+ preimage_set_system setT f (@measurable _ T').
+
+Section preimage_generated_sigma_algebra.
+Context {d'} (T : pointedType) (T' : measurableType d').
+Variable f : T -> T'.
+
+Let preimage_set0 : g_sigma_algebra_preimage f set0.
+Proof.
+rewrite /g_sigma_algebra_preimage /preimage_class/=.
+by exists set0 => //; rewrite preimage_set0 setI0.
+Qed.
+
+Let preimage_setC A :
+ g_sigma_algebra_preimage f A -> g_sigma_algebra_preimage f (~` A).
+Proof.
+rewrite /g_sigma_algebra_preimage /preimage_class/= => -[B mB] <-{A}.
+by exists (~` B); [exact: measurableC|rewrite !setTI preimage_setC].
+Qed.
+
+Let preimage_bigcup (F : (set T)^nat) :
+ (forall i, g_sigma_algebra_preimage f (F i)) ->
+ g_sigma_algebra_preimage f (\bigcup_i (F i)).
+Proof.
+move=> mF; rewrite /g_sigma_algebra_preimage /preimage_class/=.
+pose g := fun i => sval (cid2 (mF i)).
+pose mg := fun i => svalP (cid2 (mF i)).
+exists (\bigcup_i g i).
+ by apply: bigcup_measurable => k; case: (mg k).
+rewrite setTI /g preimage_bigcup; apply: eq_bigcupr => k _.
+by case: (mg k) => _; rewrite setTI.
+Qed.
+
+HB.instance Definition _ := Pointed.on (g_sigma_algebra_preimageType f).
+
+HB.instance Definition _ := @isMeasurable.Build (preimage_display f)
+ (g_sigma_algebra_preimageType f) (g_sigma_algebra_preimage f)
+ preimage_set0 preimage_setC preimage_bigcup.
+
+End preimage_generated_sigma_algebra.
+
+Notation "f .-preimage" := (preimage_display f) : measure_display_scope.
+Notation "f .-preimage.-measurable" :=
+ (measurable : set (set (g_sigma_algebra_preimageType f))) : classical_set_scope.
+
Local Open Scope ereal_scope.
Definition subset_sigma_subadditive {T} {R : numFieldType}
@@ -2008,6 +2082,10 @@ have /[!big_ord0] ->// := @measure_semi_additive _ _ _ mu (fun=> set0) 0%N.
exact: trivIset_set0.
Qed.
+Lemma measure_gt0 x : (0%R < mu x) = (mu x != 0).
+Proof. by rewrite lt_def measure_ge0 andbT. Qed.
+
+
Hint Resolve measure0 : core.
Hint Resolve measure_ge0 : core.
@@ -4102,7 +4180,8 @@ Qed.
Section ae.
Definition almost_everywhere d (T : semiRingOfSetsType d) (R : realFieldType)
- (mu : set T -> \bar R) (P : T -> Prop) := mu.-negligible (~` [set x | P x]).
+ (mu : set T -> \bar R) : set_system T :=
+ fun P => mu.-negligible (~` [set x | P x]).
Let almost_everywhereT d (T : semiRingOfSetsType d) (R : realFieldType)
(mu : {content set T -> \bar R}) : almost_everywhere mu setT.
@@ -4121,16 +4200,14 @@ Proof.
by rewrite /almost_everywhere => mA mB; rewrite setCI; exact: negligibleU.
Qed.
-#[global]
-Instance ae_filter_ringOfSetsType d {T : ringOfSetsType d} (R : realFieldType)
+Definition ae_filter_ringOfSetsType d {T : ringOfSetsType d} (R : realFieldType)
(mu : {measure set T -> \bar R}) : Filter (almost_everywhere mu).
Proof.
by split; [exact: almost_everywhereT|exact: almost_everywhereI|
exact: almost_everywhereS].
Qed.
-#[global]
-Instance ae_properfilter_algebraOfSetsType d {T : algebraOfSetsType d}
+Definition ae_properfilter_algebraOfSetsType d {T : algebraOfSetsType d}
(R : realFieldType) (mu : {measure set T -> \bar R}) :
mu [set: T] > 0 -> ProperFilter (almost_everywhere mu).
Proof.
@@ -4143,83 +4220,128 @@ End ae.
#[global] Hint Extern 0 (Filter (almost_everywhere _)) =>
(apply: ae_filter_ringOfSetsType) : typeclass_instances.
+#[global] Hint Extern 0 (Filter (nbhs (almost_everywhere _))) =>
+ (apply: ae_filter_ringOfSetsType) : typeclass_instances.
#[global] Hint Extern 0 (ProperFilter (almost_everywhere _)) =>
(apply: ae_properfilter_algebraOfSetsType) : typeclass_instances.
+#[global] Hint Extern 0 (ProperFilter (nbhs (almost_everywhere _))) =>
+ (apply: ae_properfilter_algebraOfSetsType) : typeclass_instances.
-Definition almost_everywhere_notation d (T : semiRingOfSetsType d)
- (R : realFieldType) (mu : set T -> \bar R) (P : T -> Prop)
- & (phantom Prop (forall x, P x)) := almost_everywhere mu P.
-Notation "{ 'ae' m , P }" :=
- (almost_everywhere_notation m (inPhantom P)) : type_scope.
-
-Lemma aeW {d} {T : semiRingOfSetsType d} {R : realFieldType}
+Notation "{ 'ae' m , P }" := {near almost_everywhere m, P} : type_scope.
+Notation "\forall x \ae mu , P" := (\forall x \near almost_everywhere mu, P)
+ (format "\forall x \ae mu , P",
+ x name, P at level 200, at level 200): type_scope.
+Definition ae_eq d (T : semiRingOfSetsType d) (R : realType) (mu : {measure set T -> \bar R})
+ (V : T -> Type) D (f g : forall x, V x) := (\forall x \ae mu, D x -> f x = g x).
+Notation "f = g %[ae mu 'in' D ]" := (\forall x \ae mu, D x -> f x = g x)
+ (format "f = g '%[ae' mu 'in' D ]", g at next level, D at level 200, at level 70).
+Notation "f = g %[ae mu ]" := (f = g %[ae mu in setT ])
+ (format "f = g '%[ae' mu ]", g at next level, at level 70).
+
+Lemma aeW {d} {T : ringOfSetsType d} {R : realFieldType}
(mu : {measure set _ -> \bar R}) (P : T -> Prop) :
- (forall x, P x) -> {ae mu, forall x, P x}.
+ (forall x, P x) -> \forall x \ae mu, P x.
Proof.
move=> aP; have -> : P = setT by rewrite predeqE => t; split.
by apply/negligibleP; [rewrite setCT|rewrite setCT measure0].
Qed.
+Instance ae_eq_equiv d (T : ringOfSetsType d) R mu V D :
+ Equivalence (@ae_eq d T R mu V D).
+Proof.
+split.
+- by move=> f; near=> x.
+- by move=> f g eqfg; near=> x => Dx; rewrite (near eqfg).
+- by move=> f g h eqfg eqgh; near=> x => Dx; rewrite (near eqfg) ?(near eqgh).
+Unshelve. all: by end_near. Qed.
+
Section ae_eq.
-Local Open Scope ereal_scope.
+Local Open Scope ring_scope.
Context d (T : sigmaRingType d) (R : realType).
+Implicit Types (U V : Type) (W : ringType).
Variables (mu : {measure set T -> \bar R}) (D : set T).
-Implicit Types f g h i : T -> \bar R.
-
-Definition ae_eq f g := {ae mu, forall x, D x -> f x = g x}.
+Local Notation ae_eq := (ae_eq mu D).
-Lemma ae_eq0 f g : measurable D -> mu D = 0 -> ae_eq f g.
+Lemma ae_eq0 U (f g : T -> U) : measurable D -> mu D = 0 -> f = g %[ae mu in D].
Proof. by move=> mD D0; exists D; split => // t/= /not_implyP[]. Qed.
-Lemma ae_eq_comp (j : \bar R -> \bar R) f g :
+Instance comp_ae_eq U V (j : T -> U -> V) :
+ Proper (ae_eq ==> ae_eq) (fun f x => j x (f x)).
+Proof. by move=> f g; apply: filterS => x /[apply] /= ->. Qed.
+
+Instance comp_ae_eq2 U U' V (j : T -> U -> U' -> V) :
+ Proper (ae_eq ==> ae_eq ==> ae_eq) (fun f g x => j x (f x) (g x)).
+Proof. by move=> f f' + g g'; apply: filterS2 => x + + Dx => -> // ->. Qed.
+
+Instance comp_ae_eq2' U U' V (j : U -> U' -> V) :
+ Proper (ae_eq ==> ae_eq ==> ae_eq) (fun f g x => j (f x) (g x)).
+Proof. by move=> f f' + g g'; apply: filterS2 => x + + Dx => -> // ->. Qed.
+
+Instance sub_ae_eq2 : Proper (ae_eq ==> ae_eq ==> ae_eq) (@GRing.sub_fun T R).
+Proof. exact: (@comp_ae_eq2' _ _ R (fun x y => x - y)). Qed.
+
+Lemma ae_eq_refl U (f : T -> U) : ae_eq f f. Proof. exact/aeW. Qed.
+Hint Resolve ae_eq_refl : core.
+
+Lemma ae_eq_comp U V (j : U -> V) f g :
ae_eq f g -> ae_eq (j \o f) (j \o g).
-Proof. by apply: filterS => x /[apply] /= ->. Qed.
+Proof. by move->. Qed.
-Lemma ae_eq_funeposneg f g : ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-.
-Proof.
-split=> [fg|[]].
- split; apply: filterS fg => x /[apply].
- by rewrite !funeposE => ->.
- by rewrite !funenegE => ->.
-apply: filterS2 => x + + Dx => /(_ Dx) fg /(_ Dx) gf.
-by rewrite (funeposneg f) (funeposneg g) fg gf.
-Qed.
+Lemma ae_eq_comp2 U V (j : T -> U -> V) f g :
+ ae_eq f g -> ae_eq (fun x => j x (f x)) (fun x => j x (g x)).
+Proof. by apply: filterS => x /[swap] + ->. Qed.
-Lemma ae_eq_refl f : ae_eq f f. Proof. exact/aeW. Qed.
+Lemma ae_eq_funeposneg (f g : T -> \bar R) :
+ (ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-)%E.
+Proof.
+split=> [fg|[pfg nfg]].
+ by split; near=> x => Dx; rewrite !(funeposE,funenegE) (near fg).
+by near=> x => Dx; rewrite (funeposneg f) (funeposneg g) ?(near pfg, near nfg).
+Unshelve. all: by end_near. Qed.
-Lemma ae_eq_sym f g : ae_eq f g -> ae_eq g f.
-Proof. by apply: filterS => x + Dx => /(_ Dx). Qed.
+Lemma ae_eq_sym U (f g : T -> U) : ae_eq f g -> ae_eq g f.
+Proof. by symmetry. Qed.
-Lemma ae_eq_trans f g h : ae_eq f g -> ae_eq g h -> ae_eq f h.
-Proof. by apply: filterS2 => x + + Dx => /(_ Dx) ->; exact. Qed.
+Lemma ae_eq_trans U (f g h : T -> U) : ae_eq f g -> ae_eq g h -> ae_eq f h.
+Proof. by apply transitivity. Qed.
-Lemma ae_eq_sub f g h i : ae_eq f g -> ae_eq h i -> ae_eq (f \- h) (g \- i).
-Proof. by apply: filterS2 => x + + Dx => /(_ Dx) -> /(_ Dx) ->. Qed.
+Lemma ae_eq_sub W (f g h i : T -> W) : ae_eq f g -> ae_eq h i -> ae_eq (f \- h) (g \- i).
+Proof. by apply: filterS2 => x + + Dx => /= /(_ Dx) -> /(_ Dx) ->. Qed.
-Lemma ae_eq_mul2r f g h : ae_eq f g -> ae_eq (f \* h) (g \* h).
-Proof. by apply: filterS => x /[apply] ->. Qed.
+Lemma ae_eq_mul2r W (f g h : T -> W) : ae_eq f g -> ae_eq (f \* h) (g \* h).
+Proof. by move=>/(ae_eq_comp2 (fun x y => y * h x)). Qed.
-Lemma ae_eq_mul2l f g h : ae_eq f g -> ae_eq (h \* f) (h \* g).
-Proof. by apply: filterS => x /[apply] ->. Qed.
+Lemma ae_eq_mul2l W (f g h : T -> W) : ae_eq f g -> ae_eq (h \* f) (h \* g).
+Proof. by move=>/(ae_eq_comp2 (fun x y => h x * y)). Qed.
-Lemma ae_eq_mul1l f g : ae_eq f (cst 1) -> ae_eq g (g \* f).
-Proof. by apply: filterS => x /[apply] ->; rewrite mule1. Qed.
+Lemma ae_eq_mul1l W (f g : T -> W) : ae_eq f (cst 1) -> ae_eq g (g \* f).
+Proof. by apply: filterS => x /= /[apply] ->; rewrite mulr1. Qed.
-Lemma ae_eq_abse f g : ae_eq f g -> ae_eq (abse \o f) (abse \o g).
+Lemma ae_eq_abse (f g : T -> \bar R) : ae_eq f g -> ae_eq (abse \o f) (abse \o g).
Proof. by apply: filterS => x /[apply] /= ->. Qed.
+Lemma ae_foralln (P : nat -> T -> Prop) : (forall n, \forall x \ae mu, P n x) -> \forall x \ae mu, forall n, P n x.
+Proof.
+move=> /(_ _)/cid - /all_sig[A /all_and3[Ameas muA0 NPA]].
+have seqDUAmeas := seqDU_measurable Ameas.
+exists (\bigcup_n A n); split => //.
+- exact/bigcup_measurable.
+- rewrite seqDU_bigcup_eq measure_bigcup//.
+ rewrite eseries0// => i _ _.
+ rewrite (@subset_measure0 _ _ _ _ _ (A i))//=.
+ exact: subset_seqDU.
+- by move=> x /=; rewrite -existsNP => -[n NPnx]; exists n => //; apply: NPA.
+Qed.
+
End ae_eq.
Section ae_eq_lemmas.
-Context d (T : sigmaRingType d) (R : realType).
-Implicit Types mu : {measure set T -> \bar R}.
+Context d (T : sigmaRingType d) (R : realType) (U : Type).
+Implicit Types (mu : {measure set T -> \bar R}) (A : set T) (f g : T -> U).
Lemma ae_eq_subset mu A B f g : B `<=` A -> ae_eq mu A f g -> ae_eq mu B f g.
-Proof.
-move=> BA [N [mN N0 fg]]; exists N; split => //.
-by apply: subset_trans fg; apply: subsetC => z /= /[swap] /BA ? ->.
-Qed.
+Proof. by move=> BA; apply: filterS => x + /BA; apply. Qed.
End ae_eq_lemmas.
@@ -5355,29 +5477,11 @@ End absolute_continuity.
Notation "m1 `<< m2" := (measure_dominates m1 m2).
Section absolute_continuity_lemmas.
-Context d (T : measurableType d) (R : realType).
-Implicit Types m : {measure set T -> \bar R}.
+Context d (T : measurableType d) (R : realType) (U : Type).
+Implicit Types (m : {measure set T -> \bar R}) (f g : T -> U).
Lemma measure_dominates_ae_eq m1 m2 f g E : measurable E ->
m2 `<< m1 -> ae_eq m1 E f g -> ae_eq m2 E f g.
Proof. by move=> mE m21 [A [mA A0 ?]]; exists A; split => //; exact: m21. Qed.
End absolute_continuity_lemmas.
-
-Section essential_supremum.
-Context d {T : semiRingOfSetsType d} {R : realType}.
-Variable mu : {measure set T -> \bar R}.
-Implicit Types f : T -> R.
-
-Definition ess_sup f :=
- ereal_inf (EFin @` [set r | mu (f @^-1` `]r, +oo[) = 0]).
-
-Lemma ess_sup_ge0 f : 0 < mu [set: T] -> (forall t, 0 <= f t)%R ->
- 0 <= ess_sup f.
-Proof.
-move=> muT f0; apply: lb_ereal_inf => _ /= [r /eqP rf <-]; rewrite leNgt.
-apply/negP => r0; apply/negP : rf; rewrite gt_eqF// (_ : _ @^-1` _ = setT)//.
-by apply/seteqP; split => // x _ /=; rewrite in_itv/= (lt_le_trans _ (f0 x)).
-Qed.
-
-End essential_supremum.
diff --git a/theories/numfun.v b/theories/numfun.v
index c3083f244..d75163bf4 100644
--- a/theories/numfun.v
+++ b/theories/numfun.v
@@ -15,12 +15,15 @@ From mathcomp Require Import sequences function_spaces.
(* ``` *)
(* {nnfun T >-> R} == type of non-negative functions *)
(* f ^\+ == the function formed by the non-negative outputs *)
-(* of f (from a type to the type of extended real *)
-(* numbers) and 0 otherwise *)
-(* rendered as f ⁺ with company-coq (U+207A) *)
+(* of f and 0 otherwise *)
+(* The codomain of f is the real numbers in scope *)
+(* ring_scope and the extended real numbers in scope *)
+(* ereal_scope. *)
+(* It is rendered as f ⁺ with company-coq (U+207A). *)
(* f ^\- == the function formed by the non-positive outputs *)
(* of f and 0 o.w. *)
-(* rendered as f ⁻ with company-coq (U+207B) *)
+(* Similar to ^\+. *)
+(* It is rendered as f ⁻ with company-coq (U+207B). *)
(* \1_ A == indicator function 1_A *)
(* ``` *)
(* *)
@@ -129,6 +132,149 @@ Proof. by apply/funext=> x; rewrite /patch/=; case: ifP; rewrite ?mule0. Qed.
End erestrict_lemmas.
+Section funrposneg.
+Local Open Scope ring_scope.
+
+Definition funrpos T (R : realDomainType) (f : T -> R) :=
+ fun x => maxr (f x) 0.
+Definition funrneg T (R : realDomainType) (f : T -> R) :=
+ fun x => maxr (- f x) 0.
+
+End funrposneg.
+
+Notation "f ^\+" := (funrpos f) : ring_scope.
+Notation "f ^\-" := (funrneg f) : ring_scope.
+
+Section funrposneg_lemmas.
+Local Open Scope ring_scope.
+Variables (T : Type) (R : realDomainType) (D : set T).
+Implicit Types (f g : T -> R) (r : R).
+
+Lemma funrpos_ge0 f x : 0 <= f^\+ x.
+Proof. by rewrite /funrpos /= le_max lexx orbT. Qed.
+
+Lemma funrneg_ge0 f x : 0 <= f^\- x.
+Proof. by rewrite /funrneg le_max lexx orbT. Qed.
+
+Lemma funrposN f : (\- f)^\+ = f^\-. Proof. exact/funext. Qed.
+
+Lemma funrnegN f : (\- f)^\- = f^\+.
+Proof. by apply/funext => x; rewrite /funrneg opprK. Qed.
+
+(* TODO: the following lemmas require a pointed type and realDomainType does
+not seem to be at this point
+
+Lemma funrpos_restrict f : (f \_ D)^\+ = (f^\+) \_ D.
+Proof.
+by apply/funext => x; rewrite /patch/_^\+; case: ifP; rewrite //= maxxx.
+Qed.
+
+Lemma funrneg_restrict f : (f \_ D)^\- = (f^\-) \_ D.
+Proof.
+by apply/funext => x; rewrite /patch/_^\-; case: ifP; rewrite //= oppr0 maxxx.
+Qed.*)
+
+Lemma ge0_funrposE f : (forall x, D x -> 0 <= f x) -> {in D, f^\+ =1 f}.
+Proof. by move=> f0 x; rewrite inE => Dx; apply/max_idPl/f0. Qed.
+
+Lemma ge0_funrnegE f : (forall x, D x -> 0 <= f x) -> {in D, f^\- =1 cst 0}.
+Proof.
+by move=> f0 x; rewrite inE => Dx; apply/max_idPr; rewrite lerNl oppr0 f0.
+Qed.
+
+Lemma le0_funrposE f : (forall x, D x -> f x <= 0) -> {in D, f^\+ =1 cst 0}.
+Proof. by move=> f0 x; rewrite inE => Dx; exact/max_idPr/f0. Qed.
+
+Lemma le0_funrnegE f : (forall x, D x -> f x <= 0) -> {in D, f^\- =1 \- f}.
+Proof.
+by move=> f0 x; rewrite inE => Dx; apply/max_idPl; rewrite lerNr oppr0 f0.
+Qed.
+
+Lemma ge0_funrposM r f : (0 <= r)%R ->
+ (fun x => r * f x)^\+ = (fun x => r * (f^\+ x)).
+Proof. by move=> ?; rewrite funeqE => x; rewrite /funrpos maxr_pMr// mulr0. Qed.
+
+Lemma ge0_funrnegM r f : (0 <= r)%R ->
+ (fun x => r * f x)^\- = (fun x => r * (f^\- x)).
+Proof.
+by move=> r0; rewrite funeqE => x; rewrite /funrneg -mulrN maxr_pMr// mulr0.
+Qed.
+
+Lemma le0_funrposM r f : (r <= 0)%R ->
+ (fun x => r * f x)^\+ = (fun x => - r * (f^\- x)).
+Proof.
+move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr.
+by rewrite funrposN ge0_funrnegM ?oppr_ge0.
+Qed.
+
+Lemma le0_funrnegM r f : (r <= 0)%R ->
+ (fun x => r * f x)^\- = (fun x => - r * (f^\+ x)).
+Proof.
+move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr.
+by rewrite funrnegN ge0_funrposM ?oppr_ge0.
+Qed.
+
+Lemma funr_normr f : normr \o f = f^\+ \+ f^\-.
+Proof.
+rewrite funeqE => x /=; have [fx0|/ltW fx0] := leP (f x) 0.
+- rewrite ler0_norm// /funrpos /funrneg.
+ move/max_idPr : (fx0) => ->; rewrite add0r.
+ by move: fx0; rewrite -{1}oppr0 lerNr => /max_idPl ->.
+- rewrite ger0_norm// /funrpos /funrneg; move/max_idPl : (fx0) => ->.
+ by move: fx0; rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0.
+Qed.
+
+Lemma funrposneg f : f = (fun x => f^\+ x - f^\- x).
+Proof.
+rewrite funeqE => x; rewrite /funrpos /funrneg; have [|/ltW] := leP (f x) 0.
+ by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r.
+by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0.
+Qed.
+
+Lemma funrD_Dpos f g : f \+ g = (f \+ g)^\+ \- (f \+ g)^\-.
+Proof.
+apply/funext => x; rewrite /funrpos /funrneg/=; have [|/ltW] := lerP 0 (f x + g x).
+- by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0.
+- by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r.
+Qed.
+
+Lemma funrD_posD f g : f \+ g = (f^\+ \+ g^\+) \- (f^\- \+ g^\-).
+Proof.
+apply/funext => x; rewrite /funrpos /funrneg/=.
+have [|fx0] := lerP 0 (f x); last rewrite add0r.
+- rewrite -{1}oppr0 lerNl => /max_idPr ->; have [|/ltW] := lerP 0 (g x).
+ by rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0 subr0.
+ by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite addr0 sub0r opprK.
+- move/ltW : (fx0); rewrite -{1}oppr0 lerNr => /max_idPl ->.
+ have [|]/= := lerP 0 (g x); last rewrite add0r.
+ by rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0 opprK addrC.
+ by rewrite -oppr0 ltrNr -{1}oppr0 => /ltW/max_idPl ->; rewrite opprD !opprK.
+Qed.
+
+Lemma funrpos_le f g :
+ {in D, forall x, f x <= g x} -> {in D, forall x, f^\+ x <= g^\+ x}.
+Proof.
+move=> fg x Dx; rewrite /funrpos /maxr; case: ifPn => fx; case: ifPn => gx //.
+- by rewrite leNgt.
+- by move: fx; rewrite -leNgt => /(lt_le_trans gx); rewrite ltNge fg.
+- exact: fg.
+Qed.
+
+Lemma funrneg_le f g :
+ {in D, forall x, f x <= g x} -> {in D, forall x, g^\- x <= f^\- x}.
+Proof.
+move=> fg x Dx; rewrite /funrneg /maxr; case: ifPn => gx; case: ifPn => fx //.
+- by rewrite leNgt.
+- by move: gx; rewrite -leNgt => /(lt_le_trans fx); rewrite ltrN2 ltNge fg.
+- by rewrite lerN2; exact: fg.
+Qed.
+
+End funrposneg_lemmas.
+#[global]
+Hint Extern 0 (is_true (0%R <= _ ^\+ _)%R) => solve [apply: funrpos_ge0] : core.
+#[global]
+Hint Extern 0 (is_true (0%R <= _ ^\- _)%R) => solve [apply: funrneg_ge0] : core.
+
HB.lock
Definition funepos T (R : realDomainType) (f : T -> \bar R) :=
fun x => maxe (f x) 0.
@@ -294,6 +440,17 @@ Hint Extern 0 (is_true (0%R <= _ ^\+ _)%E) => solve [apply: funepos_ge0] : core.
#[global]
Hint Extern 0 (is_true (0%R <= _ ^\- _)%E) => solve [apply: funeneg_ge0] : core.
+Section funrpos_funepos_lemmas.
+Context {T : Type} {R : realDomainType}.
+
+Lemma funerpos (f : T -> R) : (EFin \o f)^\+%E = (EFin \o f^\+).
+Proof. by apply/funext => x; rewrite funeposE /funrpos/= EFin_max. Qed.
+
+Lemma funerneg (f : T -> R) : (EFin \o f)^\-%E = (EFin \o f^\-).
+Proof. by apply/funext => x; rewrite funenegE /funrneg/= EFin_max. Qed.
+
+End funrpos_funepos_lemmas.
+
Definition indic {T} {R : ringType} (A : set T) (x : T) : R := (x \in A)%:R.
Reserved Notation "'\1_' A" (at level 8, A at level 2, format "'\1_' A") .
Notation "'\1_' A" := (indic A) : ring_scope.
diff --git a/theories/probability.v b/theories/probability.v
index bb799a389..5634b420a 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -8,7 +8,7 @@ From mathcomp Require Import exp numfun lebesgue_measure lebesgue_integral.
From mathcomp Require Import reals interval_inference ereal topology normedtype.
From mathcomp Require Import sequences derive esum measure exp trigo realfun.
From mathcomp Require Import numfun lebesgue_measure lebesgue_integral kernel.
-From mathcomp Require Import ftc gauss_integral.
+From mathcomp Require Import ftc gauss_integral hoelder.
(**md**************************************************************************)
(* # Probability *)
@@ -16,6 +16,10 @@ From mathcomp Require Import ftc gauss_integral.
(* This file provides basic notions of probability theory. See measure.v for *)
(* the type probability T R (a measure that sums to 1). *)
(* *)
+(* About integrability: as a rule of thumb, in this file, we favor the use *)
+(* of `lfun P n` hypotheses instead of the `integrable` predicate from *)
+(* `lebesgue_integral.v`. *)
+(* *)
(* ``` *)
(* {RV P >-> T'} == random variable: a measurable function to the *)
(* measurableType T' from the measured space *)
@@ -89,11 +93,30 @@ Definition random_variable d d' (T : measurableType d) (T' : measurableType d')
Notation "{ 'RV' P >-> T' }" := (@random_variable _ _ _ T' _ P) : form_scope.
+(* TODO: move elsewhere *)
+Section todo_move.
+
+Arguments sub_countable [T U].
+
+Lemma countable_range_comp (T0 T1 T2 : Type) (f : T0 -> T1) (g : T1 -> T2) :
+ countable (range f) \/ countable (range g) -> countable (range (g \o f)).
+Proof.
+rewrite -(image_comp f g).
+case.
+ move=> cf; apply: (sub_countable _ (range f))=> //.
+ exact: card_image_le.
+move=> cg; apply: (sub_countable _ (range g))=> //.
+exact/subset_card_le/image_subset.
+Qed.
+
Lemma notin_range_measure d d' (T : measurableType d) (T' : measurableType d')
(R : realType) (P : {measure set T -> \bar R}) (X : T -> R) r :
r \notin range X -> P (X @^-1` [set r]) = 0%E.
Proof. by rewrite notin_setE => hr; rewrite preimage10. Qed.
+End todo_move.
+Arguments countable_range_comp [T0 T1 T2].
+
Lemma probability_range d d' (T : measurableType d) (T' : measurableType d')
(R : realType) (P : probability T R) (X : {RV P >-> R}) :
P (X @^-1` range X) = 1%E.
@@ -149,6 +172,12 @@ Lemma integral_distribution (X : {RV P >-> T'}) (f : T' -> \bar R) :
\int[distribution P X]_y f y = \int[P]_x (f \o X) x.
Proof. by move=> mf intf; rewrite integral_pushforward. Qed.
+Lemma probability_setC' A : d.-measurable A -> P A = 1 - P (~` A).
+Proof.
+move=> mA. rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI (~` A)) -measureD ?setTD ?setCK//; first exact: measurableC.
+by rewrite [ltLHS](@probability_setT _ _ _ P) ltry.
+Qed.
+
End transfer_probability.
Definition cdf d (T : measurableType d) (R : realType) (P : probability T R)
@@ -256,9 +285,9 @@ Context d (T : measurableType d) (R : realType) (P : probability T R).
Lemma expectation_def (X : {RV P >-> R}) : 'E_P[X] = (\int[P]_w (X w)%:E)%E.
Proof. by rewrite unlock. Qed.
-Lemma expectation_fin_num (X : {RV P >-> R}) : P.-integrable setT (EFin \o X) ->
+Lemma expectation_fin_num (X : T -> R) : X \in lfun P 1 ->
'E_P[X] \is a fin_num.
-Proof. by move=> ?; rewrite unlock integral_fune_fin_num. Qed.
+Proof. by move=> ?; rewrite unlock integral_fune_fin_num; last exact/lfun1_integrable. Qed.
Lemma expectation_cst r : 'E_P[cst r] = r%:E.
Proof. by rewrite unlock/= integral_cst//= probability_setT mule1. Qed.
@@ -273,12 +302,12 @@ move: iX => /integrableP[? Xoo]; rewrite (le_lt_trans _ Xoo)// unlock.
exact: le_trans (le_abse_integral _ _ _).
Qed.
-Lemma expectationZl (X : {RV P >-> R}) (iX : P.-integrable [set: T] (EFin \o X))
- (k : R) : 'E_P[k \o* X] = k%:E * 'E_P [X].
-Proof. by rewrite unlock muleC -integralZr. Qed.
+Lemma expectationZl (X : T -> R) (k : R) : X \in lfun P 1 ->
+ 'E_P[k \o* X] = k%:E * 'E_P [X].
+Proof. by move=> ?; rewrite unlock muleC -integralZr; last exact/lfun1_integrable. Qed.
-Lemma expectation_ge0 (X : {RV P >-> R}) :
- (forall x, 0 <= X x)%R -> 0 <= 'E_P[X].
+Lemma expectation_ge0 (X : T -> R) : (forall x, 0 <= X x)%R ->
+ 0 <= 'E_P[X].
Proof.
by move=> ?; rewrite unlock integral_ge0// => x _; rewrite lee_fin.
Qed.
@@ -297,66 +326,131 @@ move=> mX mY X0 Y0 XY; rewrite unlock ae_ge0_le_integral => //.
by apply: XYN => /=; apply: contra_not h; rewrite lee_fin.
Qed.
-Lemma expectationD (X Y : {RV P >-> R}) :
- P.-integrable [set: T] (EFin \o X) -> P.-integrable [set: T] (EFin \o Y) ->
+Lemma expectationD (X Y : T -> R) : X \in lfun P 1 -> Y \in lfun P 1 ->
'E_P[X \+ Y] = 'E_P[X] + 'E_P[Y].
-Proof. by move=> ? ?; rewrite unlock integralD_EFin. Qed.
+Proof. by move=> ? ?; rewrite unlock integralD_EFin; [ | |exact/lfun1_integrable..]. Qed.
-Lemma expectationB (X Y : {RV P >-> R}) :
- P.-integrable [set: T] (EFin \o X) -> P.-integrable [set: T] (EFin \o Y) ->
+Lemma expectationB (X Y : T -> R) : X \in lfun P 1 -> Y \in lfun P 1 ->
'E_P[X \- Y] = 'E_P[X] - 'E_P[Y].
-Proof. by move=> ? ?; rewrite unlock integralB_EFin. Qed.
+Proof. by move=> ? ?; rewrite unlock integralB_EFin; [ | |exact/lfun1_integrable..]. Qed.
-Lemma expectation_sum (X : seq {RV P >-> R}) :
- (forall Xi, Xi \in X -> P.-integrable [set: T] (EFin \o Xi)) ->
+Lemma expectation_sum (X : seq (T -> R)) :
+ (forall Xi, Xi \in X -> Xi \in lfun P 1) ->
'E_P[\sum_(Xi <- X) Xi] = \sum_(Xi <- X) 'E_P[Xi].
Proof.
elim: X => [|X0 X IHX] intX; first by rewrite !big_nil expectation_cst.
-have intX0 : P.-integrable [set: T] (EFin \o X0).
- by apply: intX; rewrite in_cons eqxx.
-have {}intX Xi : Xi \in X -> P.-integrable [set: T] (EFin \o Xi).
- by move=> XiX; apply: intX; rewrite in_cons XiX orbT.
-rewrite !big_cons expectationD ?IHX// (_ : _ \o _ = fun x =>
- \sum_(f <- map (fun x : {RV P >-> R} => EFin \o x) X) f x).
- by apply: integrable_sum => // _ /mapP[h hX ->]; exact: intX.
-by apply/funext => t/=; rewrite big_map sumEFin mfun_sum.
+rewrite !big_cons expectationD; last 2 first.
+ by rewrite intX// mem_head.
+ by rewrite big_seq rpred_sum// => Y YX/=; rewrite intX// inE YX orbT.
+by rewrite IHX//= => Xi XiX; rewrite intX// inE XiX orbT.
+Qed.
+
+Lemma sum_RV_ge0 (X : seq {RV P >-> R}) x :
+ (forall Xi, Xi \in X -> 0 <= Xi x)%R ->
+ (0 <= (\sum_(Xi <- X) Xi) x)%R.
+Proof.
+elim: X => [|X0 X IHX] Xi_ge0; first by rewrite big_nil.
+rewrite big_cons.
+rewrite addr_ge0//=; first by rewrite Xi_ge0// in_cons eq_refl.
+by rewrite IHX// => Xi XiX; rewrite Xi_ge0// in_cons XiX orbT.
Qed.
End expectation_lemmas.
#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to `expectationZl`")]
Notation expectationM := expectationZl (only parsing).
+
+
+
+(* Section product_lebesgue_measure. *)
+(* Context {R : realType}. *)
+
+(* Definition p := [the sigma_finite_measure _ _ of *)
+(* ([the sigma_finite_measure _ _ of (@lebesgue_measure R)] \x *)
+(* [the sigma_finite_measure _ _ of (@lebesgue_measure R)])]%E. *)
+
+(* Fixpoint iter_mprod (n : nat) : {d & measurableType d} := *)
+(* match n with *)
+(* | 0%N => existT measurableType _ (salgebraType R.-ocitv.-measurable) *)
+(* | n'.+1 => let t' := iter_mprod n' in *)
+(* let a := existT measurableType _ (salgebraType R.-ocitv.-measurable) in *)
+(* existT _ _ [the measurableType (projT1 a, projT1 t').-prod of *)
+(* (projT2 a * projT2 t')%type] *)
+(* end. *)
+
+(* Fixpoint measurable_of_typ (t : typ) : {d & measurableType d} := *)
+(* match t with *)
+(* | Unit => existT _ _ munit *)
+(* | Bool => existT _ _ mbool *)
+(* | Nat => existT _ _ (nat : measurableType _) *)
+(* | Real => existT _ _ *)
+(* [the measurableType _ of (@measurableTypeR R)] *)
+(* end. *)
+
+(* Set Printing All. *)
+
+(* Fixpoint measurable_of_typ (d : nat) : {d & measurableType d} := *)
+(* match d with *)
+(* | O => existT _ _ (@lebesgue_measure R) *)
+(* | d'.+1 => existT _ _ *)
+(* [the measurableType (projT1 (@lebesgue_measure R), *)
+(* projT1 (measurable_of_typ d')).-prod%mdisp of *)
+(* ((@lebesgue_measure R) \x *)
+(* projT2 (measurable_of_typ d'))%E] *)
+(* end. *)
+
+(* Definition mtyp_disp t : measure_display := projT1 (measurable_of_typ t). *)
+
+(* Definition mtyp t : measurableType (mtyp_disp t) := *)
+(* projT2 (measurable_of_typ t). *)
+
+(* Definition measurable_of_seq (l : seq typ) : {d & measurableType d} := *)
+(* iter_mprod (map measurable_of_typ l). *)
+
+
+(* Fixpoint leb_meas (d : nat) := *)
+(* match d with *)
+(* | 0%N => @lebesgue_measure R *)
+(* | d'.+1 => *)
+(* ((leb_meas d') \x (@lebesgue_measure R))%E *)
+(* end. *)
+
+
+
+
+
+(* End product_lebesgue_measure. *)
+
+
HB.lock Definition covariance {d} {T : measurableType d} {R : realType}
(P : probability T R) (X Y : T -> R) :=
'E_P[(X \- cst (fine 'E_P[X])) * (Y \- cst (fine 'E_P[Y]))]%E.
Canonical covariance_unlockable := Unlockable covariance.unlock.
Arguments covariance {d T R} P _%_R _%_R.
+Hint Extern 0 (fin_num_fun _) =>
+ (apply: fin_num_measure) : core.
+
Section covariance_lemmas.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType) (P : probability T R).
-Lemma covarianceE (X Y : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) ->
- P.-integrable setT (EFin \o Y) ->
- P.-integrable setT (EFin \o (X * Y)%R) ->
+Lemma covarianceE (X Y : T -> R) :
+ X \in lfun P 1 -> Y \in lfun P 1 ->
+ (X * Y)%R \in lfun P 1 ->
covariance P X Y = 'E_P[X * Y] - 'E_P[X] * 'E_P[Y].
Proof.
-move=> X1 Y1 XY1.
-have ? : 'E_P[X] \is a fin_num by rewrite fin_num_abs// integrable_expectation.
-have ? : 'E_P[Y] \is a fin_num by rewrite fin_num_abs// integrable_expectation.
+move=> l1X l1Y l1XY.
rewrite unlock [X in 'E_P[X]](_ : _ = (X \* Y \- fine 'E_P[X] \o* Y
\- fine 'E_P[Y] \o* X \+ fine ('E_P[X] * 'E_P[Y]) \o* cst 1)%R); last first.
- apply/funeqP => x /=; rewrite mulrDr !mulrDl/= mul1r fineM// mulrNN addrA.
+ apply/funeqP => x /=; rewrite mulrDr !mulrDl/= mul1r.
+ rewrite fineM ?expectation_fin_num// mulrNN addrA.
by rewrite mulrN mulNr [Z in (X x * Y x - Z)%R]mulrC.
-have ? : P.-integrable [set: T] (EFin \o (X \* Y \- fine 'E_P[X] \o* Y)%R).
- by rewrite compreBr ?integrableB// compre_scale ?integrableZl.
-rewrite expectationD/=; last 2 first.
- - by rewrite compreBr// integrableB// compre_scale ?integrableZl.
- - by rewrite compre_scale// integrableZl// finite_measure_integrable_cst.
-rewrite 2?expectationB//= ?compre_scale// ?integrableZl//.
-rewrite 3?expectationZl//= ?finite_measure_integrable_cst//.
-by rewrite expectation_cst mule1 fineM// EFinM !fineK// muleC subeK ?fin_numM.
+rewrite expectationD/= ?rpredB//= ?lfunp_scale ?lfun_cst//.
+rewrite 2?expectationB//= ?rpredB ?lfunp_scale// 3?expectationZl//= ?lfun_cst//.
+rewrite expectation_cst mule1 fineM ?expectation_fin_num// EFinM.
+rewrite !fineK ?expectation_fin_num//.
+by rewrite muleC subeK ?fin_numM ?expectation_fin_num.
Qed.
Lemma covarianceC (X Y : T -> R) : covariance P X Y = covariance P Y X.
@@ -364,55 +458,50 @@ Proof.
by rewrite unlock; congr expectation; apply/funeqP => x /=; rewrite mulrC.
Qed.
-Lemma covariance_fin_num (X Y : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) ->
- P.-integrable setT (EFin \o Y) ->
- P.-integrable setT (EFin \o (X * Y)%R) ->
+Lemma covariance_fin_num (X Y : T -> R) :
+ X \in lfun P 1 -> Y \in lfun P 1 ->
+ (X * Y)%R \in lfun P 1 ->
covariance P X Y \is a fin_num.
Proof.
-by move=> X1 Y1 XY1; rewrite covarianceE// fin_numB fin_numM expectation_fin_num.
+by move=> ? ? ?; rewrite covarianceE// fin_numB fin_numM expectation_fin_num.
Qed.
-Lemma covariance_cst_l c (X : {RV P >-> R}) : covariance P (cst c) X = 0.
+Lemma covariance_cst_l c (X : T -> R) : covariance P (cst c) X = 0.
Proof.
rewrite unlock expectation_cst/=.
rewrite [X in 'E_P[X]](_ : _ = cst 0%R) ?expectation_cst//.
by apply/funeqP => x; rewrite /GRing.mul/= subrr mul0r.
Qed.
-Lemma covariance_cst_r (X : {RV P >-> R}) c : covariance P X (cst c) = 0.
+Lemma covariance_cst_r (X : T -> R) c : covariance P X (cst c) = 0.
Proof. by rewrite covarianceC covariance_cst_l. Qed.
-Lemma covarianceZl a (X Y : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) ->
- P.-integrable setT (EFin \o Y) ->
- P.-integrable setT (EFin \o (X * Y)%R) ->
+Lemma covarianceZl a (X Y : T -> R) :
+ X \in lfun P 1 -> Y \in lfun P 1 ->
+ (X * Y)%R \in lfun P 1 ->
covariance P (a \o* X)%R Y = a%:E * covariance P X Y.
Proof.
move=> X1 Y1 XY1.
-have aXY : (a \o* X * Y = a \o* (X * Y))%R.
- by apply/funeqP => x; rewrite mulrAC.
-rewrite [LHS]covarianceE => [||//|] /=; last 2 first.
-- by rewrite compre_scale ?integrableZl.
-- by rewrite aXY compre_scale ?integrableZl.
+have aXY : (a \o* X * Y = a \o* (X * Y))%R by apply/funeqP => x; rewrite mulrAC.
+rewrite [LHS]covarianceE => [||//|] //=; last 2 first.
+- by rewrite lfunp_scale.
+- by rewrite aXY lfunp_scale.
rewrite covarianceE// aXY !expectationZl//.
by rewrite -muleA -muleBr// fin_num_adde_defr// expectation_fin_num.
Qed.
-Lemma covarianceZr a (X Y : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) ->
- P.-integrable setT (EFin \o Y) ->
- P.-integrable setT (EFin \o (X * Y)%R) ->
+Lemma covarianceZr a (X Y : T -> R) :
+ X \in lfun P 1 -> Y \in lfun P 1 ->
+ (X * Y)%R \in lfun P 1 ->
covariance P X (a \o* Y)%R = a%:E * covariance P X Y.
Proof.
move=> X1 Y1 XY1.
by rewrite [in RHS]covarianceC covarianceC covarianceZl; last rewrite mulrC.
Qed.
-Lemma covarianceNl (X Y : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) ->
- P.-integrable setT (EFin \o Y) ->
- P.-integrable setT (EFin \o (X * Y)%R) ->
+Lemma covarianceNl (X Y : T -> R) :
+ X \in lfun P 1 -> Y \in lfun P 1 ->
+ (X * Y)%R \in lfun P 1 ->
covariance P (\- X)%R Y = - covariance P X Y.
Proof.
move=> X1 Y1 XY1.
@@ -420,76 +509,63 @@ have -> : (\- X = -1 \o* X)%R by apply/funeqP => x /=; rewrite mulrN mulr1.
by rewrite covarianceZl// EFinN mulNe mul1e.
Qed.
-Lemma covarianceNr (X Y : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) ->
- P.-integrable setT (EFin \o Y) ->
- P.-integrable setT (EFin \o (X * Y)%R) ->
+Lemma covarianceNr (X Y : T -> R) :
+ X \in lfun P 1 -> Y \in lfun P 1 ->
+ (X * Y)%R \in lfun P 1 ->
covariance P X (\- Y)%R = - covariance P X Y.
Proof. by move=> X1 Y1 XY1; rewrite !(covarianceC X) covarianceNl 1?mulrC. Qed.
-Lemma covarianceNN (X Y : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) ->
- P.-integrable setT (EFin \o Y) ->
- P.-integrable setT (EFin \o (X * Y)%R) ->
+Lemma covarianceNN (X Y : T -> R) :
+ X \in lfun P 1 -> Y \in lfun P 1 ->
+ (X * Y)%R \in lfun P 1 ->
covariance P (\- X)%R (\- Y)%R = covariance P X Y.
Proof.
-move=> X1 Y1 XY1.
-have NY : P.-integrable setT (EFin \o (\- Y)%R) by rewrite compreN ?integrableN.
-by rewrite covarianceNl ?covarianceNr ?oppeK//= mulrN compreN ?integrableN.
+by move=> ? ? ?; rewrite covarianceNl//= ?covarianceNr ?oppeK ?mulrN//= ?rpredN.
Qed.
-Lemma covarianceDl (X Y Z : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
- P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) ->
- P.-integrable setT (EFin \o Z) -> P.-integrable setT (EFin \o (Z ^+ 2)%R) ->
- P.-integrable setT (EFin \o (X * Z)%R) ->
- P.-integrable setT (EFin \o (Y * Z)%R) ->
+Lemma covarianceDl (X Y Z : T -> R) :
+ X \in lfun P 2%:E -> Y \in lfun P 2%:E -> Z \in lfun P 2%:E ->
covariance P (X \+ Y)%R Z = covariance P X Z + covariance P Y Z.
Proof.
-move=> X1 X2 Y1 Y2 Z1 Z2 XZ1 YZ1.
-rewrite [LHS]covarianceE//= ?mulrDl ?compreDr// ?integrableD//.
-rewrite 2?expectationD//=.
+move=> X2 Y2 Z2.
+have X1 := lfun_inclusion12 X2.
+have Y1 := lfun_inclusion12 Y2.
+have Z1 := lfun_inclusion12 Z2.
+have XY1 := lfun2M2_1 X2 Y2.
+have YZ1 := lfun2M2_1 Y2 Z2.
+have XZ1 := lfun2M2_1 X2 Z2.
+rewrite [LHS]covarianceE//= ?mulrDl ?compreDr ?rpredD//= 2?expectationD//=.
rewrite muleDl ?fin_num_adde_defr ?expectation_fin_num//.
rewrite oppeD ?fin_num_adde_defr ?fin_numM ?expectation_fin_num//.
by rewrite addeACA 2?covarianceE.
Qed.
-Lemma covarianceDr (X Y Z : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
- P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) ->
- P.-integrable setT (EFin \o Z) -> P.-integrable setT (EFin \o (Z ^+ 2)%R) ->
- P.-integrable setT (EFin \o (X * Y)%R) ->
- P.-integrable setT (EFin \o (X * Z)%R) ->
+Lemma covarianceDr (X Y Z : T -> R) :
+ X \in lfun P 2%:E -> Y \in lfun P 2%:E -> Z \in lfun P 2%:E ->
covariance P X (Y \+ Z)%R = covariance P X Y + covariance P X Z.
Proof.
-move=> X1 X2 Y1 Y2 Z1 Z2 XY1 XZ1.
-by rewrite covarianceC covarianceDl ?(covarianceC X) 1?mulrC.
+by move=> X2 Y2 Z2; rewrite covarianceC covarianceDl ?(covarianceC X) 1?mulrC.
Qed.
-Lemma covarianceBl (X Y Z : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
- P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) ->
- P.-integrable setT (EFin \o Z) -> P.-integrable setT (EFin \o (Z ^+ 2)%R) ->
- P.-integrable setT (EFin \o (X * Z)%R) ->
- P.-integrable setT (EFin \o (Y * Z)%R) ->
+Lemma covarianceBl (X Y Z : T -> R) :
+ X \in lfun P 2%:E -> Y \in lfun P 2%:E -> Z \in lfun P 2%:E ->
covariance P (X \- Y)%R Z = covariance P X Z - covariance P Y Z.
Proof.
-move=> X1 X2 Y1 Y2 Z1 Z2 XZ1 YZ1.
-rewrite -[(X \- Y)%R]/(X \+ (\- Y))%R covarianceDl ?covarianceNl//=.
-- by rewrite compreN// integrableN.
-- by rewrite mulrNN.
-- by rewrite mulNr compreN// integrableN.
+move=> X2 Y2 Z2.
+have Y1 := lfun_inclusion12 Y2.
+have Z1 := lfun_inclusion12 Z2.
+have YZ1 := lfun2M2_1 Y2 Z2.
+by rewrite -[(X \- Y)%R]/(X \+ (\- Y))%R covarianceDl ?covarianceNl ?rpredN.
Qed.
-Lemma covarianceBr (X Y Z : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
- P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) ->
- P.-integrable setT (EFin \o Z) -> P.-integrable setT (EFin \o (Z ^+ 2)%R) ->
- P.-integrable setT (EFin \o (X * Y)%R) ->
- P.-integrable setT (EFin \o (X * Z)%R) ->
+Lemma covarianceBr (X Y Z : T -> R) :
+ X \in lfun P 2%:E -> Y \in lfun P 2%:E -> Z \in lfun P 2%:E ->
covariance P X (Y \- Z)%R = covariance P X Y - covariance P X Z.
Proof.
-move=> X1 X2 Y1 Y2 Z1 Z2 XY1 XZ1.
+move=> X2 Y2 Z2.
+have Y1 := lfun_inclusion12 Y2.
+have Z1 := lfun_inclusion12 Z2.
+have YZ1 := lfun2M2_1 Y2 Z2.
by rewrite !(covarianceC X) covarianceBl 1?(mulrC _ X).
Qed.
@@ -502,19 +578,23 @@ Context d (T : measurableType d) (R : realType) (P : probability T R).
Definition variance (X : T -> R) := covariance P X X.
Local Notation "''V_' P [ X ]" := (variance X).
-Lemma varianceE (X : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
+Lemma varianceE (X : T -> R) : X \in lfun P 2%:E ->
'V_P[X] = 'E_P[X ^+ 2] - ('E_P[X]) ^+ 2.
-Proof. by move=> X1 X2; rewrite /variance covarianceE. Qed.
+Proof.
+move=> X2.
+by rewrite /variance covarianceE ?lfun2M2_1// lfun_inclusion12 ?fin_num_measure.
+Qed.
-Lemma variance_fin_num (X : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o X ^+ 2)%R ->
+Lemma variance_fin_num (X : T -> R) : X \in lfun P 2%:E ->
'V_P[X] \is a fin_num.
-Proof. by move=> /[dup]; apply: covariance_fin_num. Qed.
+Proof.
+move=> X2.
+by rewrite covariance_fin_num ?lfun2M2_1// lfun_inclusion12 ?fin_num_measure.
+Qed.
-Lemma variance_ge0 (X : {RV P >-> R}) : (0 <= 'V_P[X])%E.
+Lemma variance_ge0 (X : T -> R) : 0 <= 'V_P[X].
Proof.
-by rewrite /variance unlock; apply: expectation_ge0 => x; apply: sqr_ge0.
+by rewrite /variance unlock; apply: expectation_ge0 => x; exact: sqr_ge0.
Qed.
Lemma variance_cst r : 'V_P[cst r] = 0%E.
@@ -524,107 +604,85 @@ rewrite [X in 'E_P[X]](_ : _ = cst 0%R) ?expectation_cst//.
by apply/funext => x; rewrite /GRing.exp/GRing.mul/= subrr mulr0.
Qed.
-Lemma varianceZ a (X : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
+Lemma varianceZ a (X : T -> R) : X \in lfun P 2%:E ->
'V_P[(a \o* X)%R] = (a ^+ 2)%:E * 'V_P[X].
Proof.
-move=> X1 X2; rewrite /variance covarianceZl//=.
-- by rewrite covarianceZr// muleA.
-- by rewrite compre_scale// integrableZl.
-- rewrite [X in EFin \o X](_ : _ = (a \o* X ^+ 2)%R); last first.
- by apply/funeqP => x; rewrite mulrA.
- by rewrite compre_scale// integrableZl.
+move=> X2.
+have X1 := lfun_inclusion12 X2.
+rewrite /variance covarianceZl//=.
+- by rewrite covarianceZr// ?muleA ?EFinM// lfun2M2_1.
+- by rewrite lfunp_scale.
+- by rewrite lfun2M2_1// lfunp_scale// ler1n.
Qed.
-Lemma varianceN (X : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
- 'V_P[(\- X)%R] = 'V_P[X].
-Proof. by move=> X1 X2; rewrite /variance covarianceNN. Qed.
+Lemma varianceN (X : T -> R) : X \in lfun P 2%:E -> 'V_P[(\- X)%R] = 'V_P[X].
+Proof.
+move=> X2.
+by rewrite /variance covarianceNN ?lfun2M2_1 ?lfun_inclusion12 ?fin_num_measure.
+Qed.
-Lemma varianceD (X Y : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
- P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) ->
- P.-integrable setT (EFin \o (X * Y)%R) ->
+Lemma varianceD (X Y : T -> R) : X \in lfun P 2%:E -> Y \in lfun P 2%:E ->
'V_P[X \+ Y]%R = 'V_P[X] + 'V_P[Y] + 2%:E * covariance P X Y.
Proof.
-move=> X1 X2 Y1 Y2 XY1.
+move=> X2 Y2.
+have X1 := lfun_inclusion12 X2.
+have Y1 := lfun_inclusion12 Y2.
+have XY1 := lfun2M2_1 X2 Y2.
rewrite -['V_P[_]]/(covariance P (X \+ Y)%R (X \+ Y)%R).
-have XY : P.-integrable [set: T] (EFin \o (X \+ Y)%R).
- by rewrite compreDr// integrableD.
-rewrite covarianceDl//=; last 3 first.
-- rewrite -expr2 sqrrD compreDr ?integrableD// compreDr// integrableD//.
- rewrite -mulr_natr -[(_ * 2)%R]/(2 \o* (X * Y))%R compre_scale//.
- exact: integrableZl.
-- by rewrite mulrDr compreDr ?integrableD.
-- by rewrite mulrDr mulrC compreDr ?integrableD.
-rewrite covarianceDr// covarianceDr; [|by []..|by rewrite mulrC |exact: Y2].
+rewrite covarianceDl ?rpredD ?lee1n//= covarianceDr// covarianceDr//.
rewrite (covarianceC P Y X) [LHS]addeA [LHS](ACl (1*4*(2*3)))/=.
by rewrite -[2%R]/(1 + 1)%R EFinD muleDl ?mul1e// covariance_fin_num.
Qed.
-Lemma varianceB (X Y : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
- P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) ->
- P.-integrable setT (EFin \o (X * Y)%R) ->
+Lemma varianceB (X Y : T -> R) : X \in lfun P 2%:E -> Y \in lfun P 2%:E ->
'V_P[(X \- Y)%R] = 'V_P[X] + 'V_P[Y] - 2%:E * covariance P X Y.
Proof.
-move=> X1 X2 Y1 Y2 XY1.
+move=> X2 Y2.
+have X1 := lfun_inclusion12 X2.
+have Y1 := lfun_inclusion12 Y2.
+have XY1 := lfun2M2_1 X2 Y2.
rewrite -[(X \- Y)%R]/(X \+ (\- Y))%R.
-rewrite varianceD/= ?varianceN ?covarianceNr ?muleN//.
-- by rewrite compreN ?integrableN.
-- by rewrite mulrNN.
-- by rewrite mulrN compreN ?integrableN.
+by rewrite varianceD/= ?varianceN ?covarianceNr ?muleN ?rpredN.
Qed.
-Lemma varianceD_cst_l c (X : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
+Lemma varianceD_cst_l c (X : T -> R) : X \in lfun P 2%:E ->
'V_P[(cst c \+ X)%R] = 'V_P[X].
Proof.
-move=> X1 X2.
-rewrite varianceD//=; last 3 first.
-- exact: finite_measure_integrable_cst.
-- by rewrite compre_scale// integrableZl// finite_measure_integrable_cst.
-- by rewrite mulrC compre_scale ?integrableZl.
-by rewrite variance_cst add0e covariance_cst_l mule0 adde0.
+move=> X2.
+by rewrite varianceD ?lfun_cst// variance_cst add0e covariance_cst_l mule0 adde0.
Qed.
-Lemma varianceD_cst_r (X : {RV P >-> R}) c :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
+Lemma varianceD_cst_r (X : T -> R) c : X \in lfun P 2%:E ->
'V_P[(X \+ cst c)%R] = 'V_P[X].
Proof.
-move=> X1 X2.
+move=> X2.
have -> : (X \+ cst c = cst c \+ X)%R by apply/funeqP => x /=; rewrite addrC.
exact: varianceD_cst_l.
Qed.
-Lemma varianceB_cst_l c (X : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
+Lemma varianceB_cst_l c (X : T -> R) : X \in lfun P 2%:E ->
'V_P[(cst c \- X)%R] = 'V_P[X].
Proof.
-move=> X1 X2.
-rewrite -[(cst c \- X)%R]/(cst c \+ (\- X))%R varianceD_cst_l/=; last 2 first.
-- by rewrite compreN ?integrableN.
-- by rewrite mulrNN; apply: X2.
-by rewrite varianceN.
+move=> X2; rewrite -[(cst c \- X)%R]/(cst c \+ (\- X))%R.
+by rewrite varianceD_cst_l/= ?rpredN// varianceN.
Qed.
-Lemma varianceB_cst_r (X : {RV P >-> R}) c :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
+Lemma varianceB_cst_r (X : T -> R) c : X \in lfun P 2%:E ->
'V_P[(X \- cst c)%R] = 'V_P[X].
Proof.
-by move=> X1 X2; rewrite -[(X \- cst c)%R]/(X \+ (cst (- c)))%R varianceD_cst_r.
+by move=> X2; rewrite -[(X \- cst c)%R]/(X \+ (cst (- c)))%R varianceD_cst_r.
Qed.
-Lemma covariance_le (X Y : {RV P >-> R}) :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
- P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) ->
- P.-integrable setT (EFin \o (X * Y)%R) ->
+Lemma covariance_le (X Y : T -> R) : X \in lfun P 2%:E -> Y \in lfun P 2%:E ->
covariance P X Y <= sqrte 'V_P[X] * sqrte 'V_P[Y].
Proof.
-move=> X1 X2 Y1 Y2 XY1.
+move=> X2 Y2.
+have X1 := lfun_inclusion12 X2.
+have Y1 := lfun_inclusion12 Y2.
+have XY1 := lfun2M2_1 X2 Y2.
rewrite -sqrteM ?variance_ge0//.
rewrite lee_sqrE ?sqrte_ge0// sqr_sqrte ?mule_ge0 ?variance_ge0//.
-rewrite -(fineK (variance_fin_num X1 X2)) -(fineK (variance_fin_num Y1 Y2)).
+rewrite -(fineK (variance_fin_num X2)) -(fineK (variance_fin_num Y2)).
rewrite -(fineK (covariance_fin_num X1 Y1 XY1)).
rewrite -EFin_expe -EFinM lee_fin -(@ler_pM2l _ 4) ?ltr0n// [leRHS]mulrA.
rewrite [in leLHS](_ : 4 = 2 * 2)%R -natrM// [in leLHS]natrM mulrACA -expr2.
@@ -642,21 +700,37 @@ rewrite -lee_fin !EFinD EFinM fineK ?variance_fin_num// muleC -varianceZ//.
rewrite 2!EFinM ?fineK ?variance_fin_num// ?covariance_fin_num//.
rewrite -muleA [_ * r%:E]muleC -covarianceZl//.
rewrite addeAC -varianceD ?variance_ge0//=.
-- by rewrite compre_scale ?integrableZl.
-- rewrite [X in EFin \o X](_ : _ = r ^+2 \o* X ^+ 2)%R 1?mulrACA//.
- by rewrite compre_scale ?integrableZl.
-- by rewrite -mulrAC compre_scale// integrableZl.
+by rewrite lfunp_scale// ler1n.
Qed.
End variance.
Notation "'V_ P [ X ]" := (variance P X).
+(* TODO: move earlier *)
+Section mfun_measurable_realType.
+Context {d} {aT : measurableType d} {rT : realType}.
+
+HB.instance Definition _ (f : {mfun aT >-> rT}) :=
+ @isMeasurableFun.Build d _ _ _ f^\+
+ (measurable_funrpos (@measurable_funPT _ _ _ _ f)).
+
+HB.instance Definition _ (f : {mfun aT >-> rT}) :=
+ @isMeasurableFun.Build d _ _ _ f^\-
+ (measurable_funrneg (@measurable_funPT _ _ _ _ f)).
+
+HB.instance Definition _ (f : {mfun aT >-> rT}) :=
+ @isMeasurableFun.Build d _ _ _ (@normr _ _ \o f)
+ (measurableT_comp (@normr_measurable _ _) (@measurable_funPT _ _ _ _ f)).
+
+End mfun_measurable_realType.
+
+Reserved Notation "'M_ X t" (format "''M_' X t", at level 5, t, X at next level).
+
Section markov_chebyshev_cantelli.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType) (P : probability T R).
-Lemma markov (X : {RV P >-> R}) (f : R -> R) (eps : R) :
- (0 < eps)%R ->
+Lemma markov (X : {RV P >-> R}) (f : R -> R) (eps : R) : (0 < eps)%R ->
measurable_fun [set: R] f -> (forall r, 0 <= r -> 0 <= f r)%R ->
{in Num.nneg &, {homo f : x y / x <= y}}%R ->
(f eps)%:E * P [set x | eps%:E <= `| (X x)%:E | ] <=
@@ -673,14 +747,19 @@ apply: (le_trans (@le_integral_comp_abse _ _ _ P _ measurableT (EFin \o X)
- by rewrite unlock.
Qed.
-Definition mmt_gen_fun (X : {RV P >-> R}) (t : R) := 'E_P[expR \o t \o* X].
+Definition mmt_gen_fun0 (X : {RV P >-> R}) (t : R) := [the {mfun T >-> R} of expR \o t \o* X].
+
+Definition mmt_gen_fun (X : {RV P >-> R}) (t : R) := 'E_P[mmt_gen_fun0 X t].
Local Notation "'M_ X t" := (mmt_gen_fun X t).
+Definition nth_mmt (X : {RV P >-> R}) (n : nat) := 'E_P[X^+n].
+
Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R ->
P [set x | X x >= a]%R <= 'M_X r * (expR (- (r * a)))%:E.
Proof.
move=> t0; rewrite /mmt_gen_fun.
-have -> : expR \o r \o* X = (normr \o normr) \o (expR \o r \o* X).
+have -> : mmt_gen_fun0 X r = (normr \o normr) \o (expR \o r \o* X) :> (T -> R).
+ (* TODO: lemmas *)
by apply: funext => t /=; rewrite normr_id ger0_norm ?expR_ge0.
rewrite expRN lee_pdivlMr ?expR_gt0//.
rewrite (le_trans _ (markov _ (expR_gt0 (r * a)) _ _ _))//; last first.
@@ -715,58 +794,33 @@ by move=> /le_trans; apply; rewrite /variance [in leRHS]unlock.
Qed.
Lemma cantelli (X : {RV P >-> R}) (lambda : R) :
- P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
- (0 < lambda)%R ->
+ (X : T -> R) \in lfun P 2%:E -> (0 < lambda)%R ->
P [set x | lambda%:E <= (X x)%:E - 'E_P[X]]
<= (fine 'V_P[X] / (fine 'V_P[X] + lambda^2))%:E.
Proof.
-move=> X1 X2 lambda_gt0.
-have finEK : (fine 'E_P[X])%:E = 'E_P[X].
- by rewrite fineK ?unlock ?integral_fune_fin_num.
+move=> /[dup] X2 /lfun_inclusion12 X1 lambda_gt0.
+have finEK : (fine 'E_P[X])%:E = 'E_P[X] by rewrite fineK ?expectation_fin_num.
have finVK : (fine 'V_P[X])%:E = 'V_P[X] by rewrite fineK ?variance_fin_num.
pose Y := (X \- cst (fine 'E_P[X]))%R.
-have Y1 : P.-integrable [set: T] (EFin \o Y).
- rewrite compreBr => [|//]; apply: integrableB X1 _ => [//|].
- exact: finite_measure_integrable_cst.
-have Y2 : P.-integrable [set: T] (EFin \o (Y ^+ 2)%R).
- rewrite sqrrD/= compreDr => [|//].
- apply: integrableD => [//||]; last first.
- rewrite -[(_ ^+ 2)%R]/(cst ((- fine 'E_P[X]) ^+ 2)%R).
- exact: finite_measure_integrable_cst.
- rewrite compreDr => [|//]; apply: integrableD X2 _ => [//|].
- rewrite [X in EFin \o X](_ : _ = (- fine 'E_P[X] * 2) \o* X)%R; last first.
- by apply/funeqP => x /=; rewrite -mulr_natl mulrC mulrA.
- by rewrite compre_scale => [|//]; apply: integrableZl X1.
+have Y2 : (Y : T -> R) \in lfun P 2%:E.
+ by rewrite /Y rpredB ?lee1n//= => _; rewrite lfun_cst.
have EY : 'E_P[Y] = 0.
- rewrite expectationB/= ?finite_measure_integrable_cst//.
- rewrite expectation_cst finEK subee//.
- by rewrite unlock; apply: integral_fune_fin_num X1.
+ rewrite expectationB ?lfun_cst//= expectation_cst.
+ by rewrite finEK subee// expectation_fin_num.
have VY : 'V_P[Y] = 'V_P[X] by rewrite varianceB_cst_r.
have le (u : R) : (0 <= u)%R ->
P [set x | lambda%:E <= (X x)%:E - 'E_P[X]]
<= ((fine 'V_P[X] + u^2) / (lambda + u)^2)%:E.
move=> uge0; rewrite EFinM.
- have YU1 : P.-integrable [set: T] (EFin \o (Y \+ cst u)%R).
- rewrite compreDr => [|//]; apply: integrableD Y1 _ => [//|].
- exact: finite_measure_integrable_cst.
- have YU2 : P.-integrable [set: T] (EFin \o ((Y \+ cst u) ^+ 2)%R).
- rewrite sqrrD/= compreDr => [|//].
- apply: integrableD => [//||]; last first.
- rewrite -[(_ ^+ 2)%R]/(cst (u ^+ 2))%R.
- exact: finite_measure_integrable_cst.
- rewrite compreDr => [|//]; apply: integrableD Y2 _ => [//|].
- rewrite [X in EFin \o X](_ : _ = (2 * u) \o* Y)%R; last first.
- by apply/funeqP => x /=; rewrite -mulr_natl mulrCA.
- by rewrite compre_scale => [|//]; apply: integrableZl Y1.
have -> : (fine 'V_P[X] + u^2)%:E = 'E_P[(Y \+ cst u)^+2]%R.
rewrite -VY -[RHS](@subeK _ _ (('E_P[(Y \+ cst u)%R])^+2)); last first.
- by rewrite fin_numX ?unlock ?integral_fune_fin_num.
- rewrite -varianceE/= -/Y -?expe2//.
- rewrite expectationD/= ?EY ?add0e ?expectation_cst -?EFinM; last 2 first.
- - rewrite compreBr => [|//]; apply: integrableB X1 _ => [//|].
- exact: finite_measure_integrable_cst.
- - exact: finite_measure_integrable_cst.
- by rewrite (varianceD_cst_r _ Y1 Y2) EFinD fineK ?(variance_fin_num Y1 Y2).
+ rewrite fin_numX// expectation_fin_num//= rpredD ?lfun_cst//.
+ by rewrite rpredB// lfun_cst.
+ rewrite -varianceE/=; last first.
+ by rewrite rpredD ?lee1n//= => _; rewrite lfun_cst.
+ rewrite -expe2 expectationD/= ?lfun_cst//; last by rewrite rpredB ?lfun_cst.
+ rewrite EY// add0e expectation_cst -EFinM.
+ by rewrite (varianceD_cst_r _ Y2) EFinD fineK ?variance_fin_num.
have le : [set x | lambda%:E <= (X x)%:E - 'E_P[X]]
`<=` [set x | ((lambda + u)^2)%:E <= ((Y x + u)^+2)%:E].
move=> x /= le; rewrite lee_fin; apply: lerXn2r.
@@ -776,7 +830,7 @@ have le (u : R) : (0 <= u)%R ->
- by rewrite lerD2r -lee_fin EFinB finEK.
apply: (le_trans (le_measure _ _ _ le)).
- rewrite -[[set _ | _]]setTI inE; apply: emeasurable_fun_c_infty => [//|].
- by apply: emeasurable_funB => //; exact: measurable_int X1.
+ by apply: emeasurable_funB=> //; apply/measurable_int/lfun1_integrable/X1.
- rewrite -[[set _ | _]]setTI inE; apply: emeasurable_fun_c_infty => [//|].
rewrite measurable_EFinP [X in measurable_fun _ X](_ : _ =
(fun x => x ^+ 2) \o (fun x => Y x + u))%R//.
@@ -805,9 +859,10 @@ by rewrite -mulrDl -mulrDr (addrC u0) [in RHS](mulrAC u0) -exprnP expr2 !mulrA.
Qed.
End markov_chebyshev_cantelli.
+Notation "'M_ X t" := (mmt_gen_fun X t) : ereal_scope.
HB.mixin Record MeasurableFun_isDiscrete d d' (T : measurableType d)
- (T' : measurableType d') (X : T -> T') of @MeasurableFun d d' T T' X := {
+ (T' : measurableType d') (X : T -> T') (*of @MeasurableFun d d' T T' X*) := {
countable_range : countable (range X)
}.
@@ -826,6 +881,22 @@ Definition discrete_random_variable d d' (T : measurableType d)
Notation "{ 'dRV' P >-> T }" :=
(@discrete_random_variable _ _ _ T _ P) : form_scope.
+Section dRV_comp.
+Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2) (T3 : measurableType d3).
+Context (R : realType) (P : probability T1 R) (X : {dRV P >-> T2}) (f : {mfun T2 >-> T3}).
+
+Let countable_range_comp_dRV : countable (range (f \o X)).
+Proof. apply: countable_range_comp; left; exact: countable_range. Qed.
+
+(*
+HB.instance Definition _ :=
+ MeasurableFun_isDiscrete.Build _ _ _ _ _ countable_range_comp_dRV.
+*)
+
+Definition dRV_comp (* : {dRV P >-> T3} *) := f \o X.
+
+End dRV_comp.
+
Section dRV_definitions.
Context {d} {d'} {T : measurableType d} {T' : measurableType d'} {R : realType}
(P : probability T R).
@@ -909,11 +980,12 @@ End distribution_dRV.
Section discrete_distribution.
Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType) (P : probability T R).
+Context d d' (T : measurableType d) (U : measurableType d') (R : realType) (P : probability T R).
+Hypothesis mx : forall x : U, measurable [set x].
-Lemma dRV_expectation (X : {dRV P >-> R}) :
- P.-integrable [set: T] (EFin \o X) ->
- 'E_P[X] = \sum_(n >.
+
+Lemma g_sigma_preimage_comp d1 {T1 : semiRingOfSetsType d1} n
+ {T : pointedType} (f1 : 'I_n -> T -> T1) [T3 : Type] (g : T3 -> T) :
+ g_sigma_preimage (fun i => f1 i \o g) =
+ preimage_set_system [set: T3] g (g_sigma_preimage f1).
+Proof.
+rewrite {1}/g_sigma_preimage.
+rewrite -g_sigma_preimageE; congr (<>).
+destruct n as [|n].
+ rewrite !big_ord0 /preimage_set_system/=.
+ by apply/esym; rewrite -subset0 => t/= [].
+rewrite predeqE => C; split.
+- rewrite -bigcup_mkord_ord => -[i Ii [A mA <-{C}]].
+ exists (f1 (Ordinal Ii) @^-1` A).
+ rewrite -bigcup_mkord_ord; exists i => //.
+ exists A => //; rewrite setTI// (_ : Ordinal _ = inord i)//.
+ by apply/val_inj => /=;rewrite inordK.
+ rewrite !setTI// -comp_preimage// (_ : Ordinal _ = inord i)//.
+ by apply/val_inj => /=;rewrite inordK.
+- move=> [A].
+ rewrite -bigcup_mkord_ord => -[i Ii [B mB <-{A}]] <-{C}.
+ rewrite -bigcup_mkord_ord.
+ exists i => //.
+ by exists B => //; rewrite !setTI -comp_preimage.
+Qed.
+
+HB.instance Definition _ (n : nat) (T : pointedType) :=
+ isPointed.Build (n.-tuple T) (nseq n point).
+
+Lemma countable_range_bool d (T : measurableType d) (b : bool) :
+ countable (range (@cst T _ b)).
+Proof. exact: countableP. Qed.
+
+HB.instance Definition _ d (T : measurableType d) b :=
+ MeasurableFun_isDiscrete.Build d _ T _ (cst b) (countable_range_bool T b).
+
+Definition measure_tuple_display : measure_display -> measure_display.
+Proof. exact. Qed.
+
+Section measurable_tuple.
+Context {d} {T : measurableType d}.
+Variable n : nat.
+
+Let coors : 'I_n -> n.-tuple T -> T := fun i x => @tnth n T x i.
+
+Let tuple_set0 : g_sigma_preimage coors set0.
+Proof. exact: sigma_algebra0. Qed.
+
+Let tuple_setC A : g_sigma_preimage coors A -> g_sigma_preimage coors (~` A).
+Proof. exact: sigma_algebraC. Qed.
+
+Let tuple_bigcup (F : _^nat) : (forall i, g_sigma_preimage coors (F i)) ->
+ g_sigma_preimage coors (\bigcup_i (F i)).
+Proof. exact: sigma_algebra_bigcup. Qed.
+
+HB.instance Definition _ := @isMeasurable.Build (measure_tuple_display d)
+ (n.-tuple T) (g_sigma_preimage coors) tuple_set0 tuple_setC tuple_bigcup.
+
+End measurable_tuple.
+
+Lemma measurable_tnth d (T : measurableType d) n (i : 'I_n) :
+ measurable_fun [set: n.-tuple T] (@tnth _ T ^~ i).
+Proof.
+move=> _ Y mY; rewrite setTI; apply: sub_sigma_algebra => /=.
+rewrite -bigcup_seq/=; exists i => //=; first by rewrite mem_index_enum.
+by exists Y => //; rewrite setTI.
+Qed.
+
+Section measurable_cons.
+Context d d1 (T : measurableType d) (T1 : measurableType d1).
+
+Lemma cons_measurable_funP (n : nat) (h : T -> n.-tuple T1) :
+ measurable_fun setT h <->
+ forall i : 'I_n, measurable_fun setT ((@tnth _ T1 ^~ i) \o h).
+Proof.
+apply: (@iff_trans _ (g_sigma_preimage
+ (fun i : 'I_n => (@tnth _ T1 ^~ i) \o h) `<=` measurable)).
+- rewrite g_sigma_preimage_comp; split=> [mf A [C HC <-]|f12].
+ exact: mf.
+ by move=> _ A mA; apply: f12; exists A.
+- split=> [h12|mh].
+ move=> i _ A mA.
+ apply: h12.
+ apply: sub_sigma_algebra.
+ destruct n as [|n].
+ by case: i => [] [].
+ rewrite -bigcup_mkord_ord.
+ exists i => //; first by red.
+ exists A => //.
+ rewrite !setTI.
+ rewrite (_ : inord i = i)//.
+ by apply/val_inj => /=; rewrite inordK.
+ apply: smallest_sub; first exact: sigma_algebra_measurable.
+ destruct n as [|n].
+ by rewrite big_ord0.
+ rewrite -bigcup_mkord_ord.
+ apply: bigcup_sub => i Ii.
+ move=> A [C mC <-].
+ exact: mh.
+Qed.
+
+Lemma measurable_cons (f : T -> T1) n (g : T -> n.-tuple T1) :
+ measurable_fun setT f -> measurable_fun setT g ->
+ measurable_fun setT (fun x : T => [the n.+1.-tuple T1 of (f x) :: (g x)]).
+Proof.
+move=> mf mg; apply/cons_measurable_funP => /= i.
+have [->|i0] := eqVneq i ord0.
+ by rewrite (_ : _ \o _ = f).
+have @j : 'I_n.
+ apply: (@Ordinal _ i.-1).
+ rewrite prednK//.
+ have := ltn_ord i.
+ by rewrite ltnS.
+ by rewrite lt0n.
+rewrite (_ : _ \o _ = (fun x => tnth (g x) j))//.
+ apply: (@measurableT_comp _ _ _ _ _ _
+ (fun x : n.-tuple T1 => tnth x j) _ g) => //.
+ exact: measurable_tnth.
+apply/funext => t/=.
+rewrite (_ : i = lift ord0 j) ?tnthS//.
+apply/val_inj => /=.
+by rewrite /bump/= add1n prednK// lt0n.
+Qed.
+
+End measurable_cons.
+
+(* NB: not used *)
+Lemma behead_mktuple n {T : eqType} (t : n.+1.-tuple T) :
+ behead t = [tuple (tnth t (lift ord0 i)) | i < n].
+Proof.
+destruct n as [|n].
+ rewrite !tuple0.
+ apply: size0nil.
+ by rewrite size_behead size_tuple.
+apply: (@eq_from_nth _ (tnth_default t ord0)).
+ by rewrite size_behead !size_tuple.
+move=> i ti.
+rewrite nth_behead/= (nth_map ord0); last first.
+ rewrite size_enum_ord.
+ by rewrite size_behead size_tuple in ti.
+rewrite (tnth_nth (tnth_default t ord0)).
+congr nth.
+rewrite /= /bump/= add1n; congr S.
+apply/esym.
+rewrite size_behead size_tuple in ti.
+have := @nth_ord_enum _ ord0 (Ordinal ti).
+by move=> ->.
+Qed.
+
+Lemma measurable_behead d (T : measurableType d) n :
+ measurable_fun setT (fun x : n.+1.-tuple T => [tuple of behead x] : n.-tuple T).
+Proof.
+red=> /=.
+move=> _ Y mY.
+rewrite setTI.
+set bh := (bh in preimage bh).
+have bhYE : (bh @^-1` Y) = [set x :: y | x in setT & y in Y].
+ rewrite /bh.
+ apply/seteqP; split=> x /=.
+ move=> ?; exists (thead x)=> //.
+ exists [tuple of behead x] => //=.
+ by rewrite [in RHS](tuple_eta x).
+ case=> x0 _ [] y Yy xE.
+ suff->: [tuple of behead x] = y by [].
+ apply/val_inj=> /=.
+ by rewrite -xE.
+have:= mY.
+rewrite /measurable/= => + F [] sF.
+pose F' := image_set_system setT bh F.
+move=> /(_ F') /=.
+have-> : F' Y = F (bh @^-1` Y) by rewrite /F' /image_set_system /= setTI.
+move=> /[swap] H; apply; split; first exact: sigma_algebra_image.
+move=> A; rewrite /= /F' /image_set_system /= setTI.
+set X := (X in X A).
+move => XA.
+apply: H; rewrite big_ord_recl /=; right.
+set X' := (X' in X' (preimage _ _)).
+have-> : X' = preimage_set_system setT bh X.
+ rewrite /X.
+ rewrite (big_morph _ (preimage_set_systemU _ _) (preimage_set_system0 _ _)).
+ apply: eq_bigr=> i _.
+ rewrite -preimage_set_system_comp.
+ congr preimage_set_system.
+ apply: funext=> t.
+ rewrite (tuple_eta t) /bh /= tnthS.
+ by congr tnth; apply/val_inj.
+exists A=> //.
+by rewrite setTI.
+Qed.
+
+Section tuple_sum.
+Context d (T : measurableType d) (R : realType) (P : probability T R).
+
+Definition Tnth n (X : n.-tuple {mfun T >-> R}) i : n.-tuple T -> R :=
+ fun t => (tnth X i) (tnth t i).
+
+Lemma measurable_Tnth n (X : n.-tuple {mfun T >-> R}) i :
+ measurable_fun [set: n.-tuple T] (Tnth X i).
+Proof. by apply: measurableT_comp => //; exact: measurable_tnth. Qed.
+
+HB.instance Definition _ n (X : n.-tuple {mfun T >-> R}) (i : 'I_n) :=
+ isMeasurableFun.Build _ _ _ _ (Tnth X i) (measurable_Tnth X i).
+
+Lemma measurable_tuple_sum n (X : n.-tuple {mfun T >-> R}) :
+ measurable_fun setT (\sum_(i < n) (Tnth X i))%R.
+Proof.
+rewrite [X in measurable_fun _ X](_ : _
+ = (fun x => \sum_(i < n) Tnth X i x)); last first.
+ by apply/funext => x; rewrite fct_sumE.
+apply: measurable_sum => i/=; apply/measurableT_comp => //.
+exact: measurable_tnth.
+Qed.
+
+HB.instance Definition _ n (s : n.-tuple {mfun T >-> R}) :=
+ isMeasurableFun.Build _ _ _ _ (\sum_(i < n) Tnth s i)%R (measurable_tuple_sum s).
+
+Lemma measurable_tuple_prod m n (s : m.-tuple {mfun T >-> R}) (f : 'I_n -> 'I_m) :
+ measurable_fun setT (\prod_(i < n) Tnth s (f i))%R.
+Proof.
+rewrite [X in measurable_fun _ X](_ : _
+ = (fun x => \prod_(i < n) Tnth s (f i) x)); last first.
+ by apply/funext => x; rewrite fct_prodE.
+by apply: measurable_prod => /= i _; apply/measurableT_comp.
+Qed.
+
+HB.instance Definition _ m n (s : m.-tuple {mfun T >-> R}) (f : 'I_n -> 'I_m) :=
+ isMeasurableFun.Build _ _ _ _ (\prod_(i < n) Tnth s (f i))%R (measurable_tuple_prod s f).
+
+End tuple_sum.
+
+Section pro1.
+Context {d1} {T1 : measurableType d1} {d2} {T2 : measurableType d2}
+ (R : realType) (P1 : probability T1 R) (P2 : probability T2 R).
+
+Definition pro1 := (P1 \x P2)%E.
+
+HB.instance Definition _ := Measure.on pro1.
+
+Lemma pro1_setT : pro1 setT = 1%E.
+Proof.
+rewrite /pro1 -setXTT product_measure1E// -[RHS]mule1.
+by rewrite -{1}(@probability_setT _ _ _ P1) -(@probability_setT _ _ _ P2).
+Qed.
+
+HB.instance Definition _ := Measure_isProbability.Build _ _ _ pro1 pro1_setT.
+End pro1.
+
+Section pro2.
+Context {d1} {T1 : measurableType d1} {d2} {T2 : measurableType d2}
+ (R : realType) (P1 : probability T1 R) (P2 : probability T2 R).
+
+Definition pro2 := (P1 \x^ P2)%E.
+
+HB.instance Definition _ := Measure.on pro2.
+
+Lemma pro2_setT : pro2 setT = 1%E.
+Proof.
+rewrite /pro2 -setXTT product_measure2E// -[RHS]mule1.
+by rewrite -{1}(@probability_setT _ _ _ P1) -(@probability_setT _ _ _ P2).
+Qed.
+
+HB.instance Definition _ := Measure_isProbability.Build _ _ _ pro2 pro2_setT.
+End pro2.
+
+Section iterated_product_of_probability_measures.
+Context d (T : measurableType d) (R : realType) (P : probability T R).
+
+Fixpoint ipro (n : nat) : set (n.-tuple T) -> \bar R :=
+ match n with
+ | 0%N => \d_([::] : 0.-tuple T)
+ | m.+1 => fun A => (P \x^ @ipro m)%E [set (thead x, [tuple of behead x]) | x in A]
+ end.
+
+Lemma ipro_measure n : @ipro n set0 = 0 /\ (forall A, 0 <= @ipro n A)%E
+ /\ semi_sigma_additive (@ipro n).
+Proof.
+elim: n => //= [|n ih].
+ by repeat split => //; exact: measure_semi_sigma_additive.
+pose build_Mpro := isMeasure.Build _ _ _ (@ipro n) ih.1 ih.2.1 ih.2.2.
+pose Mpro : measure _ R := HB.pack (@ipro n) build_Mpro.
+pose ppro : measure _ R := (P \x^ Mpro)%E.
+split.
+ rewrite image_set0 /product_measure2 /=.
+ under eq_fun => x do rewrite ysection0 measure0 (_ : 0 = cst 0 x)//.
+ by rewrite (_ : @ipro n = Mpro)// integral_cst// mul0e.
+split.
+ by move => A; rewrite (_ : @ipro n = Mpro).
+rewrite (_ : @ipro n = Mpro)// (_ : (P \x^ Mpro)%E = ppro)//.
+move=> F mF dF mUF.
+rewrite image_bigcup.
+move=> [:save].
+apply: measure_semi_sigma_additive.
+- abstract: save.
+ move=> i.
+ pose f (t : n.+1.-tuple T) := (@thead n T t, [the _.-tuple T of behead t]).
+ pose f' (x : T * n.-tuple T) := [the n.+1.-tuple T of x.1 :: x.2].
+ rewrite [X in measurable X](_ : _ = f' @^-1` F i); last first.
+ apply/seteqP; split=> [x/= [t Fit] <-{x}|[x1 x2] /= Fif'].
+ rewrite /f'/=.
+ by rewrite (tuple_eta t) in Fit.
+ exists (f' (x1, x2)) => //.
+ rewrite /f' /= theadE//; congr pair.
+ exact/val_inj.
+ rewrite -[X in measurable X]setTI.
+ suff: measurable_fun setT f' by exact.
+ exact: measurable_cons.
+- (* TODO: lemma? *)
+ apply/trivIsetP => i j _ _ ij.
+ move/trivIsetP : dF => /(_ i j Logic.I Logic.I ij).
+ rewrite -!subset0 => ij0 /= [_ _] [[t Fit] [<- <-]]/=.
+ move=> [u Fju [hut tut]].
+ have := ij0 t; apply; split => //.
+ suff: t = u by move=> ->.
+ rewrite (tuple_eta t) (tuple_eta u) hut.
+ by apply/val_inj => /=; rewrite tut.
+- apply: bigcup_measurable => j _.
+ exact: save.
+Qed.
+
+HB.instance Definition _ n := isMeasure.Build _ _ _ (@ipro n)
+ (@ipro_measure n).1 (@ipro_measure n).2.1 (@ipro_measure n).2.2.
+
+Lemma ipro_setT n : @ipro n setT = 1%E.
+Proof.
+elim: n => [|n ih]/=; first by rewrite diracT.
+rewrite /product_measure2 /ysection/=.
+under eq_fun => x.
+ rewrite [X in P X](_ : _ = [set: T]); last first.
+ under eq_fun => y.
+ rewrite [X in _ \in X](_ : _ = setT); last first.
+ apply: funext=> z/=.
+ apply: propT.
+ exists (z.1 :: z.2) => //=.
+ case: z => z1 z2/=.
+ congr pair.
+ exact/val_inj.
+ over.
+ by apply: funext => y /=; rewrite in_setT trueE.
+ rewrite probability_setT.
+ over.
+by rewrite integral_cst// mul1e.
+Qed.
+
+HB.instance Definition _ n :=
+ Measure_isProbability.Build _ _ _ (@ipro n) (@ipro_setT n).
+
+End iterated_product_of_probability_measures.
+Arguments ipro {d T R} P n.
+
+Notation "\X_ n P" := (ipro P n) (at level 10, n, P at next level,
+ format "\X_ n P").
+
+Section integral_ipro.
+Context d (T : measurableType d) (R : realType) (P : probability T R).
+Local Open Scope ereal_scope.
+
+Definition phi n := fun w : T * n.-tuple T => [the _.-tuple _ of w.1 :: w.2].
+
+Lemma mphi n : measurable_fun [set: T * n.-tuple T] (@phi n).
+Proof. exact: measurable_cons. Qed.
+
+Definition psi n := fun w : n.+1.-tuple T => (thead w, [the _.-tuple _ of behead w]).
+
+Lemma mpsi n : measurable_fun [set: _.-tuple _] (@psi n).
+Proof.
+by apply/measurable_fun_prod => /=;
+ [exact: measurable_tnth|exact: measurable_behead].
+Qed.
+
+Lemma phiK n : cancel (@phi n) (@psi n).
+Proof.
+by move=> [x1 x2]; rewrite /psi /phi/=; congr pair => /=; exact/val_inj.
+Qed.
+
+Let psiK n : cancel (@psi n) (@phi n).
+Proof. by move=> x; rewrite /psi /phi/= [RHS]tuple_eta. Qed.
+
+Lemma integral_ipro n (f : n.+1.-tuple T -> R) :
+ (\X_n.+1 P).-integrable [set: n.+1.-tuple T] (EFin \o f) ->
+ \int[\X_n.+1 P]_w (f w)%:E =
+ \int[pro2 P (\X_n P)]_w (f (w.1 :: w.2))%:E.
+Proof.
+move=> /integrableP[mf intf].
+rewrite -(@integral_pushforward _ _ _ _ R _ (@mphi n) _ setT
+ (fun x : n.+1.-tuple T => (f x)%:E)); [|by []| |by []].
+ apply: eq_measure_integral => A mA _.
+ rewrite /=.
+ rewrite /pushforward.
+ rewrite /pro2.
+ rewrite /phi/=.
+ rewrite /preimage/=.
+ congr (_ _).
+ apply/seteqP; split => [x/= [t At <-/=]|x/= Ax].
+ move: At.
+ by rewrite {1}(tuple_eta t)//.
+ exists (x.1 :: x.2) => //=.
+ destruct x as [x1 x2] => //=.
+ congr pair.
+ exact/val_inj.
+rewrite /=.
+apply/integrable_prodP.
+rewrite /=.
+apply/integrableP; split => /=.
+ apply: measurableT_comp => //=.
+ exact: mphi.
+apply: le_lt_trans (intf).
+rewrite [leRHS](_ : _ = \int[\X_n.+1 P]_x
+ ((((abse \o (@EFin R \o (f \o (@phi n))))) \o (@psi n)) x)); last first.
+ by apply: eq_integral => x _ /=; rewrite psiK.
+rewrite le_eqVlt; apply/orP; left; apply/eqP.
+rewrite -[RHS](@integral_pushforward _ _ _ _ R _ (@mpsi n) _ setT
+ (fun x : T * n.-tuple T => ((abse \o (EFin \o (f \o (@phi n)))) x)))//.
+- apply: eq_measure_integral => // A mA _.
+ apply: product_measure_unique => // B C mB mC.
+ rewrite /= /pushforward/=.
+ rewrite -product_measure2E//=.
+ congr (_ _).
+ (* TODO: lemma *)
+ apply/seteqP; split => [[x1 x2]/= [t [Bt Ct]] [<- <-//]|].
+ move=> [x1 x2] [B1 C2] /=.
+ exists (x1 :: x2) => //=.
+ split=> //.
+ rewrite [X in C X](_ : _ = x2)//.
+ exact/val_inj.
+ congr pair => //.
+ exact/val_inj.
+- apply/measurable_EFinP => //=.
+ apply: measurableT_comp => //=.
+ apply: measurableT_comp => //=.
+ exact/measurable_EFinP.
+ exact: mphi.
+- have : (\X_n.+1 P).-integrable [set: n.+1.-tuple T] (EFin \o f).
+ exact/integrableP.
+- apply: le_integrable => //=.
+ + apply: measurableT_comp => //=; last exact: mpsi.
+ apply/measurable_EFinP => //=.
+ apply: measurableT_comp => //=.
+ apply: measurableT_comp => //=; last exact: mphi.
+ by apply/measurable_EFinP => //=.
+ + move=> x _.
+ by rewrite normr_id// psiK.
+Qed.
+
+Lemma integral_ipro_ge0 n (f : n.+1.-tuple T -> R) :
+ measurable_fun setT f -> (forall x, 0 <= f x)%R ->
+ \int[\X_n.+1 P]_w (f w)%:E = \int[pro2 P (\X_n P)]_w (f (w.1 :: w.2))%:E.
+Proof.
+move=> mf f0.
+rewrite -(@ge0_integral_pushforward _ _ _ _ R _ (@mphi n) _ setT
+ (fun x : n.+1.-tuple T => (f x)%:E)); [ | by [] | exact: measurableT_comp | ].
+ apply: eq_measure_integral => A mA _.
+ rewrite /=.
+ rewrite /pushforward.
+ rewrite /pro2.
+ rewrite /phi/=.
+ rewrite /preimage/=.
+ congr (_ _).
+ apply/seteqP; split => [x/= [t At <-/=]|x/= Ax].
+ move: At.
+ by rewrite {1}(tuple_eta t)//.
+ exists (x.1 :: x.2) => //=.
+ destruct x as [x1 x2] => //=.
+ congr pair.
+ exact/val_inj.
+move=> x/= _.
+by rewrite lee_fin.
+Qed.
+
+Lemma ipro_tnth n A i:
+ d.-measurable A ->
+ (\X_n P) ((tnth (T:=T))^~ i @^-1` A) = P A.
+Proof.
+elim: n A i => [|n ih A].
+ by move=> A; case; case => //.
+case; case => [i0|m mn mA].
+- transitivity ((P \x^ \X_n P) (A `*` [set: n.-tuple T])).
+ rewrite /ipro.
+ congr (_ _).
+ apply: funext => x/=.
+ apply/propext; split.
+ move=> [y] Ay0 <-; split => //=.
+ by rewrite /thead (_ : ord0 = Ordinal i0)//=; apply: val_inj => /=.
+ move=> []Ax _. exists (x.1 :: x.2) => //=.
+ rewrite /thead tnth0 [RHS]surjective_pairing.
+ congr (_, _).
+ by apply: val_inj => /=.
+ rewrite /product_measure2/= setXT.
+ under [X in integral _ _ X]eq_fun => x do rewrite ysection_preimage_fst.
+ by rewrite integral_cst//= probability_setT mule1.
+have mn' : (m < n)%N by rewrite -ltnS.
+transitivity ((P \x^ \X_n P) ([set: T] `*` ((tnth (T:=T)^~ (Ordinal mn') @^-1` A)))).
+ rewrite /ipro.
+ congr (_ _).
+ apply: funext => x/=.
+ apply/propext; split.
+ move=> [y]/= Ay <-; split => //=.
+ rewrite tnth_behead/=.
+ rewrite (_ : inord m.+1 = Ordinal mn)//.
+ apply: val_inj => //=.
+ by rewrite inordK.
+ move=> [_ Ax].
+ exists [tuple of x.1 :: x.2].
+ rewrite (_ : Ordinal mn = lift ord0 (Ordinal mn'))//=; last first.
+ apply: val_inj => /=.
+ by rewrite /bump//=.
+ by rewrite tnthS.
+ move: x Ax.
+ case => x1 x2/= Ax.
+ congr (_ ,_ ).
+ by apply: val_inj.
+rewrite product_measure2E//=; first by rewrite probability_setT mul1e ih.
+rewrite -[X in measurable X]setTI.
+exact: measurable_tnth.
+Qed.
+
+Lemma integral_tnth n (f : {mfun T >-> R}) i :
+ \int[\X_n P]_x (`|f (tnth x i)|)%:E = \int[P]_x (`|f x|)%:E.
+Proof.
+rewrite -(preimage_setT ((@tnth n _)^~ i)).
+rewrite -(@ge0_integral_pushforward _ _ _ _ _ _ (measurable_tnth i) (\X_n P) _ (EFin \o normr \o f) measurableT).
+- apply: eq_measure_integral => A mA _/=.
+ by rewrite /pushforward ipro_tnth.
+- by do 2 apply: measurableT_comp => //.
+by move=> y _/=; rewrite lee_fin normr_ge0.
+Qed.
+
+Lemma tnth_integrable n (F : n.-tuple {mfun T >-> R}) i :
+ P.-integrable [set: T] (EFin \o tnth F i) ->
+ (\X_n P).-integrable [set: n.-tuple T] (EFin \o Tnth F i).
+Proof.
+move=> /integrableP/=[mF iF]; rewrite /Tnth.
+apply/integrableP; split.
+ apply: measurableT_comp => //.
+ apply: measurableT_comp => //.
+ exact: measurable_tnth.
+rewrite /=.
+by rewrite (integral_tnth (tnth F i)).
+Qed.
+
+Lemma integral_ipro_tnth n (F : n.-tuple {mfun T >-> R}) :
+ (forall Fi : {mfun T >-> R}, Fi \in F -> (Fi : T -> R) \in lfun P 1) ->
+ forall i : 'I_n, \int[\X_n P]_x (Tnth F i x)%:E = \int[P]_x (tnth F i x)%:E.
+Proof.
+elim: n F => //=[F FiF|]; first by case=> m i0.
+move=> m ih F lfunFi/=.
+rewrite [X in integral X](_ : _ = \X_m.+1 P)//.
+case; case => [i0|i im].
+ rewrite [LHS](@integral_ipro m (Tnth F (Ordinal i0))); last first.
+ by apply/tnth_integrable/lfun1_integrable/lfunFi/mem_tnth.
+ under eq_fun => x do
+ rewrite /Tnth (_ : tnth (_ :: _) _ = tnth [tuple of x.1 :: x.2] ord0)// tnth0.
+ rewrite -fubini1'/fubini_F/=; last first.
+ apply/integrable12ltyP => /=.
+ apply: measurableT_comp => //=.
+ exact: measurableT_comp.
+ under eq_integral => x _ do rewrite integral_cst//= probability_setT mule1.
+ have /lfunFi : tnth F (Ordinal i0) \in F by apply/tnthP; exists (Ordinal i0).
+ by move/lfun1_integrable /integrableP => [_].
+ apply: eq_integral => x _.
+ by rewrite integral_cst//= probability_setT mule1.
+rewrite [LHS](@integral_ipro m (Tnth F (Ordinal im))); last first.
+ by apply/tnth_integrable/lfun1_integrable/lfunFi/mem_tnth.
+have jm : (i < m)%nat by rewrite ltnS in im.
+have liftjm : Ordinal im = lift ord0 (Ordinal jm).
+ by apply: val_inj; rewrite /= /bump add1n.
+rewrite (tuple_eta F).
+under eq_integral => x _ do rewrite /Tnth !liftjm !tnthS.
+rewrite -fubini2'/fubini_G/=; last first.
+ apply/integrable12ltyP => /=.
+ apply: measurableT_comp => //=.
+ apply: measurableT_comp => //=.
+ apply: (@measurableT_comp _ _ _ _ _ _ (fun x => tnth x (Ordinal jm)) _ (fun x => x.2)).
+ exact: measurable_tnth.
+ exact: measurable_snd.
+ rewrite [ltLHS](_ : _ = \int[\X_m P]_y `|tnth (behead_tuple F) (Ordinal jm) (tnth y (Ordinal jm))|%:E); last first.
+ by rewrite integral_cst//= probability_setT mule1.
+ have : (tnth F (lift ord0 (Ordinal jm)) : T -> R) \in lfun P 1.
+ by rewrite lfunFi// mem_tnth.
+ rewrite {1}(tuple_eta F) tnthS.
+ by move/lfun1_integrable/tnth_integrable/integrableP => [_]/=.
+transitivity (\int[\X_m P]_x (tnth (behead F) (Ordinal jm) (tnth x (Ordinal jm)))%:E).
+ apply: eq_integral => /=x _.
+ by rewrite integral_cst//= probability_setT mule1.
+rewrite [LHS]ih; last by move=> Fi FiF; apply: lfunFi; rewrite mem_behead.
+apply: eq_integral => x _.
+by rewrite liftjm tnthS.
+Qed.
+
+End integral_ipro.
+
+Section properties_of_expectation.
+Context d (T : measurableType d) (R : realType) (P : probability T R).
+Local Open Scope ereal_scope.
+
+Lemma expectation_sum_ipro n (X : n.-tuple {RV P >-> R}) :
+ [set` X] `<=` lfun P 1 ->
+ 'E_(\X_n P)[\sum_(i < n) Tnth X i] = \sum_(i < n) ('E_P[(tnth X i)]).
+Proof.
+move=>/= bX.
+rewrite (_ : \sum_(i < n) Tnth X i = \sum_(Xi <- [seq Tnth X i | i in 'I_n]) Xi)%R; last first.
+ by rewrite big_map big_enum.
+rewrite expectation_sum/=.
+ rewrite big_map big_enum/=.
+ apply: eq_bigr => i i_n.
+ rewrite unlock.
+ exact: integral_ipro_tnth.
+move=> Xi /tnthP[i] ->.
+pose j := cast_ord (card_ord _) i.
+apply/lfun1_integrable => /=.
+rewrite /image_tuple tnth_map.
+apply: tnth_integrable.
+rewrite (_ : (tnth (enum_tuple 'I_n) i) = j); last first.
+ apply: val_inj => //=.
+ rewrite /tnth nth_enum_ord//.
+ have := ltn_ord i.
+ move/leq_trans.
+ apply.
+ by rewrite card_ord leqnn.
+by have /bX/lfun1_integrable : (tnth X j) \in X by apply/tnthP; exists j.
+Qed.
+
+Lemma expectation_pro2 d1 d2 (T1 : measurableType d1) (T2 : measurableType d2)
+ (P1 : probability T1 R) (P2 : probability T2 R)
+ (X : T1 -> R) (Y : T2 -> R) :
+ (X : _ -> _) \in lfun P1 1 ->
+ (Y : _ -> _) \in lfun P2 1 ->
+ let XY := fun (x : T1 * T2) => (X x.1 * Y x.2)%R in
+ 'E_(pro2 P1 P2)[XY] = 'E_P1[X] * 'E_P2[Y].
+Proof.
+move=> /[dup]lX /sub_lfun_mfun +/[dup]lY /sub_lfun_mfun.
+rewrite !inE/= => mX mY.
+rewrite unlock /expectation/=. rewrite /pro2. rewrite -fubini1'/=; last first.
+ apply/integrable21ltyP.
+ - apply/measurable_EFinP => //=.
+ by apply: measurable_funM => //=; apply/measurableT_comp.
+ - under eq_integral.
+ move=> t _.
+ under eq_integral.
+ move=> x _.
+ rewrite /= normrM EFinM muleC.
+ over.
+ rewrite integralZl//; last first.
+ exact/lfun1_integrable/lfun_norm.
+ over.
+ rewrite /=.
+ rewrite ge0_integralZr//; last 2 first.
+ apply/measurable_EFinP => //.
+ by apply/measurableT_comp => //.
+ by apply: integral_ge0 => //.
+ rewrite lte_mul_pinfty//.
+ - exact: integral_ge0.
+ - exact/integral_fune_fin_num/lfun1_integrable/lfun_norm.
+ - by move: lX => /lfun1_integrable/integrableP[_ /=].
+rewrite /fubini_F/=.
+under eq_integral => x _.
+ under eq_integral => y _ do rewrite EFinM.
+ rewrite integralZl//; last exact/lfun1_integrable.
+ rewrite -[X in _ * X]fineK ?integral_fune_fin_num//; last exact/lfun1_integrable.
+ over.
+rewrite /=integralZr//; last exact/lfun1_integrable.
+by rewrite fineK// integral_fune_fin_num; last exact/lfun1_integrable.
+Qed.
+
+End properties_of_expectation.
+
+Section properties_of_independence.
+Context d (T : measurableType d) (R : realType) (P : probability T R).
+Local Open Scope ereal_scope.
+
+(* TODO: delete? *)
+Lemma boundedM U (f g : U -> R) (A : set U) :
+ [bounded f x | x in A] ->
+ [bounded g x | x in A] ->
+ [bounded (f x * g x)%R | x in A].
+Proof.
+move=> bF bG.
+rewrite/bounded_near.
+case: bF => M1 [M1real M1f].
+case: bG => M2 [M2real M2g].
+near=> M.
+rewrite/globally/= => x xA.
+rewrite normrM.
+rewrite (@le_trans _ _ (`|M1 + 1| * `|M2 + 1|)%R)//.
+rewrite ler_pM//.
+ by rewrite M1f// (lt_le_trans _ (ler_norm _))// ltrDl.
+by rewrite M2g// (lt_le_trans _ (ler_norm _))// ltrDl.
+Unshelve. all: by end_near.
+Qed.
+
+Lemma abse_prod [I : Type] (r : seq I) (Q : pred I) (F : I -> \bar R) :
+ `|\prod_(i <- r | Q i) F i| = (\prod_(i <- r | Q i) `|F i|).
+Proof.
+elim/big_ind2 : _ => //.
+ by rewrite abse1.
+move=> x1 x2 ? ? <- <-.
+by rewrite abseM.
+Qed.
+
+Lemma expectation_product n (X : n.-tuple {RV P >-> R}) :
+ [set` X] `<=` lfun P 1 ->
+ 'E_(\X_n P)[ \prod_(i < n) Tnth X i] = \prod_(i < n) 'E_P[ (tnth X i) ].
+Proof.
+elim: n X => [X|n IH X] lfunX/=.
+ by rewrite !big_ord0 expectation_cst.
+rewrite unlock /expectation.
+rewrite [X in integral X](_ : _ = \X_n.+1 P)//.
+pose F : n.+1.-tuple T -> R := (\prod_(i < n.+1) Tnth X i)%R.
+have mF : measurable_fun setT F by apply: measurable_tuple_prod.
+pose build_mF := isMeasurableFun.Build _ _ _ _ F mF.
+pose MF : {mfun _ >-> _} := HB.pack F build_mF.
+have h1 : (thead X : _ -> _) \in lfun P 1 by exact/lfunX/mem_tnth.
+have h2 : (\prod_(i < n) Tnth (behead_tuple X) i)%R \in lfun (\X_n P) 1.
+ apply/lfun1_integrable/integrableP => /=; split.
+ apply: measurableT_comp => //.
+ exact: measurable_tuple_prod.
+ under eq_integral => x _ do rewrite -abse_EFin.
+ apply/abse_integralP => //=.
+ apply: measurableT_comp => //.
+ exact: measurable_tuple_prod.
+ have := IH (behead_tuple X).
+ rewrite unlock /= => ->; last by move => x /mem_behead/lfunX.
+ rewrite abse_prod finite_prod_ge0// => i.
+ rewrite abse_ge0//= abse_integralP//; last first.
+ exact: measurableT_comp.
+ have: (tnth (behead_tuple X) i) \in X by apply/mem_behead/mem_tnth.
+ by move/(lfunX (tnth (behead_tuple X) i))/lfun1_integrable/integrableP => [_].
+rewrite [LHS](@integral_ipro _ _ _ _ _ MF) /pro2; last first.
+ rewrite /MF/F; apply/integrableP; split.
+ exact: measurableT_comp.
+ rewrite integral_ipro_ge0/=; last 2 first.
+ - exact: measurableT_comp.
+ - by [].
+ rewrite [ltLHS](_ : _ = \int[pro2 P (\X_n P)]_x (`|thead X x.1| * `|(\prod_(i < n) Tnth (behead_tuple X) i) x.2|)%:E); last first.
+ apply: eq_integral => x _.
+ rewrite big_ord_recl normrM /Tnth (tuple_eta X) !fct_prodE/= !tnth0/=.
+ congr ((_ * `|_|)%:E).
+ by apply: eq_bigr => i _/=; rewrite !tnthS -tuple_eta.
+ pose tuple_prod := (\prod_(i < n) Tnth (behead_tuple X) i)%R.
+ pose meas_tuple_prod := measurable_tuple_prod (behead_tuple X) id.
+ pose build_MTP := isMeasurableFun.Build _ _ _ _ tuple_prod meas_tuple_prod.
+ pose MTP : {mfun _ >-> _} := HB.pack tuple_prod build_MTP.
+ pose normMTP : {mfun _ >-> _} := normr \o MTP.
+ rewrite [ltLHS](_ : _ = \int[P]_w `|thead X w|%:E * \int[\X_n P]_w `|tuple_prod w|%:E); last first.
+ have := @expectation_pro2 _ _ _ _ _ P (\X_n P) (normr \o thead X) (normMTP).
+ rewrite unlock /= /tuple_prod => <- //.
+ - exact/lfun_norm.
+ - exact/lfun_norm.
+ rewrite lte_mul_pinfty ?ge0_fin_numE ?integral_ge0//.
+ by move: h1 => /lfun1_integrable/integrableP[_].
+ by move: h2 => /lfun1_integrable/integrableP[_].
+under eq_fun.
+ move=> /=x.
+ rewrite /F/MF big_ord_recl/= /Tnth/= fctE tnth0.
+ rewrite fct_prodE.
+ under eq_bigr.
+ move=> i _.
+ rewrite tnthS.
+ over.
+ over.
+have /lfun1_integrable/integrableP/=[mXi iXi] := lfunX _ (mem_tnth ord0 X).
+have ? : \int[\X_n P]_x0 (\prod_(i < n) tnth X (lift ord0 i) (tnth x0 i))%:E < +oo.
+ under eq_integral => x _.
+ rewrite [X in X%:E](_ : _ = \prod_(i < n) tnth (behead_tuple X) i (tnth x i))%R; last first.
+ by apply: eq_bigr => i _; rewrite (tuple_eta X) tnthS -tuple_eta.
+ over.
+ rewrite /= -(_ : 'E_(\X_n P)[\prod_(i < n) Tnth (behead_tuple X) i]%R = \int[\X_n P]_x _); last first.
+ rewrite unlock.
+ apply: eq_integral => /=x _.
+ by rewrite /Tnth fct_prodE.
+ rewrite IH.
+ rewrite ltey_eq finite_prod_fin_num//= => i.
+ rewrite fin_num_abs unlock.
+ apply/abse_integralP => //.
+ exact: measurableT_comp.
+ have: (tnth (behead_tuple X) i) \in X by apply/mem_behead/mem_tnth.
+ by move/(lfunX (tnth (behead_tuple X) i))/lfun1_integrable/integrableP => [_/=].
+ by move=> Xi XiX; rewrite lfunX//= mem_behead.
+have ? : measurable_fun [set: n.-tuple T]
+ (fun x : n.-tuple T => \prod_(i < n) tnth X (lift ord0 i) (tnth x i))%R.
+ apply: measurable_prod => //= i i_n.
+ apply: measurableT_comp => //.
+ exact: measurable_tnth.
+rewrite /=.
+have ? : \int[\X_n P]_x `|\prod_(i < n) tnth X (lift ord0 i) (tnth x i)|%:E < +oo.
+ move: h2 => /lfun1_integrable/integrableP[?].
+ apply: le_lt_trans.
+ rewrite le_eqVlt; apply/orP; left; apply/eqP.
+ apply: eq_integral => x _/=.
+ rewrite fct_prodE/=.
+ congr (`| _ |%:E).
+ apply: eq_bigr => i _.
+ by rewrite {1}(tuple_eta X) tnthS.
+rewrite -fubini1' /fubini_F/=; last first.
+ apply/integrable21ltyP => //=.
+ apply: measurableT_comp => //.
+ apply: measurable_funM => //=.
+ exact: measurableT_comp.
+ apply: measurable_prod => //= i i_n.
+ apply: measurableT_comp => //.
+ exact: (measurableT_comp (measurable_tnth i) measurable_snd).
+ under eq_integral => y _.
+ under eq_integral => x _ do rewrite normrM EFinM.
+ rewrite integralZr//; last exact/lfun1_integrable/lfun_norm/lfunX/mem_tnth.
+ rewrite -[X in X * _]fineK ?ge0_fin_numE ?integral_ge0//.
+ over.
+ rewrite integralZl ?fineK ?lte_mul_pinfty ?integral_ge0//=.
+ - by rewrite ge0_fin_numE ?integral_ge0.
+ - by rewrite ge0_fin_numE ?integral_ge0.
+ - apply/integrableP; split; first by do 2 apply: measurableT_comp => //.
+ by under eq_integral => x _ do rewrite /=normr_id.
+under eq_integral => x _.
+ under eq_integral => y _ do rewrite EFinM.
+ rewrite integralZl/=; last 2 first.
+ - apply: measurableT.
+ - by apply/integrableP; split => //; first by apply: measurableT_comp => //.
+ rewrite -[X in _ * X]fineK; last first.
+ rewrite fin_num_abs. apply/abse_integralP => //.
+ exact/measurable_EFinP.
+ over.
+rewrite /= integralZr//; last exact/lfun1_integrable/lfunX/mem_tnth.
+rewrite fineK; last first.
+ rewrite fin_num_abs. apply/abse_integralP => //.
+ exact/measurable_EFinP.
+rewrite [X in _ * X](_ : _ = 'E_(\X_n P)[\prod_(i < n) Tnth (behead X) i])%R; last first.
+ rewrite [in RHS]unlock /Tnth.
+ apply: eq_integral => x _.
+ rewrite fct_prodE.
+ congr (_%:E).
+ apply: eq_bigr => i _.
+ rewrite tnth_behead.
+ congr (_ _ _).
+ congr (_ _ _).
+ apply: val_inj => /=.
+ by rewrite /bump/= inordK// ltnS.
+rewrite IH; last first.
+- by move => x /mem_behead/lfunX.
+rewrite big_ord_recl/=.
+congr (_ * _).
+apply: eq_bigr => /=i _.
+rewrite unlock /expectation.
+apply: eq_integral => x _.
+congr EFin.
+by rewrite [in RHS](tuple_eta X) tnthS.
+Qed.
+
+End properties_of_independence.
+
+HB.mixin Record RV_isBernoulli d (T : measurableType d) (R : realType)
+ (P : probability T R) (p : R) (X : T -> bool) of @isMeasurableFun d _ T bool X := {
+ bernoulliP : distribution P X = bernoulli p }.
+
+#[short(type=bernoulliRV)]
+HB.structure Definition BernoulliRV d (T : measurableType d) (R : realType)
+ (P : probability T R) (p : R) :=
+ {X of @RV_isBernoulli _ _ _ P p X}.
+Arguments bernoulliRV {d T R}.
+
+Section properties_of_BernoulliRV.
+Local Open Scope ereal_scope.
+Context d (T : measurableType d) {R : realType} (P : probability T R).
+Variable p : R.
+Hypothesis p01 : (0 <= p <= 1)%R.
+
+Lemma preimage_set1 (X : T -> bool) r : X @^-1` [set r] = [set i | X i == r].
+Proof. by apply/seteqP; split => [x /eqP H//|x /eqP]. Qed.
+
+Lemma bernoulli_RV1 (X : bernoulliRV P p) : P [set i | X i == 1%R] = p%:E.
+Proof.
+have/(congr1 (fun f => f [set 1%:R])):= @bernoulliP _ _ _ _ _ X.
+rewrite bernoulliE//.
+rewrite diracE/= mem_set// mule1// diracE/= memNset//.
+rewrite mule0 adde0 -preimage_set1.
+by rewrite /distribution /= => <-.
+Qed.
+
+Lemma bernoulli_RV2 (X : bernoulliRV P p) : P [set i | X i == 0%R] = (`1-p)%:E.
+Proof.
+have/(congr1 (fun f => f [set 0%:R])):= @bernoulliP _ _ _ _ _ X.
+rewrite bernoulliE//.
+rewrite diracE/= memNset//.
+rewrite mule0// diracE/= mem_set// add0e mule1.
+rewrite /distribution /= => <-.
+by rewrite -preimage_set1.
+Qed.
+
+Lemma bernoulli_expectation (X : bernoulliRV P p) :
+ 'E_P[bool_to_real R X] = p%:E.
+Proof.
+rewrite unlock.
+rewrite -(@ge0_integral_distribution _ _ _ _ _ _ X (EFin \o GRing.natmul 1))//; last first.
+ by move=> y //=.
+rewrite /bernoulli/=.
+rewrite (@eq_measure_integral _ _ _ _ (bernoulli p)); last first.
+ by move=> A mA _ /=; congr (_ _); exact: bernoulliP.
+rewrite integral_bernoulli//=.
+by rewrite -!EFinM -EFinD mulr0 addr0 mulr1.
+Qed.
+
+Lemma integrable_bernoulli (X : bernoulliRV P p) :
+ P.-integrable [set: T] (EFin \o bool_to_real R X).
+Proof.
+apply/integrableP; split.
+ by apply: measurableT_comp => //; exact: measurable_bool_to_real.
+have -> : \int[P]_x `|(EFin \o bool_to_real R X) x| = 'E_P[bool_to_real R X].
+ rewrite unlock /expectation.
+ apply: eq_integral => x _.
+ by rewrite gee0_abs //= lee_fin.
+by rewrite bernoulli_expectation// ltry.
+Qed.
+
+Lemma lfun_bernoulli (X : bernoulliRV P p) q :
+ 1 <= q -> (bool_to_real R X : T -> R) \in lfun P q.
+Proof.
+move=> q1.
+apply: (@lfun_bounded _ _ _ P _ 1%R) => //t.
+by rewrite /bool_to_real/= ler_norml lern1 (@le_trans _ _ 0%R) ?leq_b1.
+Qed.
+
+Lemma bool_RV_sqr (X : {RV P >-> bool}) :
+ ((bool_to_real R X ^+ 2) = bool_to_real R X :> (T -> R))%R.
+Proof.
+apply: funext => x /=.
+rewrite /GRing.exp /bool_to_real /GRing.mul/=.
+by case: (X x) => /=; rewrite ?mulr1 ?mulr0.
+Qed.
+
+Lemma bernoulli_variance (X : bernoulliRV P p) :
+ 'V_P[bool_to_real R X] = (p * (`1-p))%:E.
+Proof.
+rewrite (@varianceE _ _ _ _ (bool_to_real R X));
+ [|rewrite ?[X in _ \o X]bool_RV_sqr; apply: lfun_bernoulli..]; last first.
+ by rewrite lee1n.
+rewrite [X in 'E_P[X]]bool_RV_sqr !bernoulli_expectation//.
+by rewrite expe2 -EFinD onemMr.
+Qed.
+
+Definition real_of_bool n : _ -> n.-tuple _ :=
+ map_tuple (bool_to_real R : bernoulliRV P p -> {mfun _ >-> _}).
+
+Definition trial_value n (X : n.-tuple {RV P >-> _}) : {RV (\X_n P) >-> R : realType} :=
+ (\sum_(i < n) Tnth X i)%R.
+
+Definition bool_trial_value n := @trial_value n \o @real_of_bool n.
+
+Lemma btr_ge0 (X : {RV P >-> bool}) t : (0 <= bool_to_real R X t)%R.
+Proof. by []. Qed.
+
+Lemma btr_le1 (X : {RV P >-> bool}) t : (bool_to_real R X t <= 1)%R.
+Proof. by rewrite /bool_to_real/=; case: (X t). Qed.
+
+Lemma expectation_bernoulli_trial n (X : n.-tuple (bernoulliRV P p)) :
+ 'E_(\X_n P)[bool_trial_value X] = (n%:R * p)%:E.
+Proof.
+rewrite expectation_sum_ipro; last first.
+ by move=> Xi /tnthP [i] ->; rewrite tnth_map; apply: lfun_bernoulli.
+transitivity (\sum_(i < n) p%:E).
+ by apply: eq_bigr => k _; rewrite !tnth_map bernoulli_expectation.
+by rewrite sumEFin big_const_ord iter_addr addr0 mulrC mulr_natr.
+Qed.
+
+Lemma bernoulli_trial_ge0 n (X : n.-tuple (bernoulliRV P p)) :
+ (forall t, 0 <= bool_trial_value X t)%R.
+Proof.
+move=> t.
+rewrite [leRHS]fct_sumE.
+apply/sumr_ge0 => /= i _.
+rewrite /Tnth.
+by rewrite !tnth_map.
+Qed.
+
+Lemma bernoulli_trial_mmt_gen_fun n (X_ : n.-tuple (bernoulliRV P p)) (t : R) :
+ let X := bool_trial_value X_ in
+ 'M_X t = \prod_(i < n) 'M_(bool_to_real R (tnth X_ i) : {RV P >-> _}) t.
+Proof.
+pose mmtX : 'I_n -> {RV P >-> R : realType} := fun i => expR \o t \o* bool_to_real R (tnth X_ i).
+transitivity ('E_(\X_n P)[ \prod_(i < n) Tnth (mktuple mmtX) i ])%R.
+ congr expectation => /=; apply: funext => x/=.
+ rewrite fct_sumE.
+ rewrite big_distrl/= expR_sum.
+ rewrite [in RHS]fct_prodE.
+ apply: eq_bigr => i _.
+ by rewrite /Tnth !tnth_map /mmtX/= tnth_ord_tuple.
+rewrite /mmtX.
+rewrite expectation_product; last first.
+- move=> _ /mapP [/= i _ ->].
+ apply/lfun1_integrable.
+ apply: (bounded_RV_integrable (expR `|t|)) => // t0.
+ rewrite expR_ge0/= ler_expR/=.
+ rewrite /bool_to_real/=.
+ case: (tnth X_ i t0) => //=; rewrite ?mul1r ?mul0r//.
+ by rewrite ler_norm.
+apply: eq_bigr => /= i _.
+congr expectation.
+rewrite /=.
+by rewrite tnth_map/= tnth_ord_tuple.
+Qed.
+
+Arguments sub_countable [T U].
+Arguments card_le_finite [T U].
+
+Lemma bernoulli_mmt_gen_fun (X : bernoulliRV P p) (t : R) :
+ 'M_(bool_to_real R X : {RV P >-> R : realType}) t = (p * expR t + (1-p))%:E.
+Proof.
+rewrite/mmt_gen_fun.
+pose mmtX : {RV P >-> R : realType} := expR \o t \o* (bool_to_real R X).
+set A := X @^-1` [set true].
+set B := X @^-1` [set false].
+have mA: measurable A by exact: measurable_sfunP.
+have mB: measurable B by exact: measurable_sfunP.
+have dAB: [disjoint A & B]
+ by rewrite /disj_set /A /B preimage_true preimage_false setICr.
+have TAB: setT = A `|` B by rewrite -preimage_setU -setT_bool preimage_setT.
+rewrite unlock.
+rewrite TAB integral_setU_EFin -?TAB//.
+under eq_integral.
+ move=> x /=.
+ rewrite /A inE /bool_to_real /= => ->.
+ rewrite mul1r.
+ over.
+rewrite integral_cst//.
+under eq_integral.
+ move=> x /=.
+ rewrite /B inE /bool_to_real /= => ->.
+ rewrite mul0r.
+ over.
+rewrite integral_cst//.
+rewrite /A /B /preimage /=.
+under eq_set do rewrite (propext (rwP eqP)).
+rewrite bernoulli_RV1.
+under eq_set do rewrite (propext (rwP eqP)).
+rewrite bernoulli_RV2.
+rewrite -EFinD; congr (_ + _)%:E; rewrite mulrC//.
+by rewrite expR0 mulr1.
+Qed.
+
+(* wrong lemma *)
+Lemma binomial_mmt_gen_fun n (X_ : n.-tuple (bernoulliRV P p)) (t : R) :
+ let X := bool_trial_value X_ : {RV \X_n P >-> R : realType} in
+ 'M_X t = ((p * expR t + (1 - p))`^(n%:R))%:E.
+Proof.
+move: p01 => /andP[p0 p1] bX/=.
+rewrite bernoulli_trial_mmt_gen_fun//.
+under eq_bigr => i _ do rewrite bernoulli_mmt_gen_fun//.
+rewrite big_const iter_mule mule1 cardT size_enum_ord -EFin_expe powR_mulrn//.
+by rewrite addr_ge0// ?subr_ge0// mulr_ge0// expR_ge0.
+Qed.
+
+Lemma mmt_gen_fun_expectation n (X_ : n.-tuple (bernoulliRV P p)) (t : R) :
+ (0 <= t)%R ->
+ let X := bool_trial_value X_ : {RV \X_n P >-> R : realType} in
+ 'M_X t <= (expR (fine 'E_(\X_n P)[X] * (expR t - 1)))%:E.
+Proof.
+move=> t_ge0/=.
+have /andP[p0 p1] := p01.
+rewrite binomial_mmt_gen_fun// lee_fin.
+rewrite expectation_bernoulli_trial//.
+rewrite addrCA -{2}(mulr1 p) -mulrN -mulrDr.
+rewrite -mulrA (mulrC (n%:R)) expRM ge0_ler_powR// ?nnegrE ?expR_ge0//.
+ by rewrite addr_ge0// mulr_ge0// subr_ge0 -expR0 ler_expR.
+exact: expR_ge1Dx.
+Qed.
+
+End properties_of_BernoulliRV.
+
+(* the lemmas used in the sampling theorem that are generic w.r.t. R : realType *)
+Section sampling_theorem_part1.
+Local Open Scope ereal_scope.
+Context {d} {T : measurableType d} {R : realType} (P : probability T R).
+Variable p : R.
+Hypothesis p01 : (0 <= p <= 1)%R.
+
+(* [end of Theorem 2.4, Rajani]*)
+Lemma end_thm24 n (X_ : n.-tuple (bernoulliRV P p)) (t delta : R) :
+ (0 < delta)%R ->
+ let X := bool_trial_value X_ in
+ let mu := 'E_(\X_n P)[X] in
+ let t := ln (1 + delta) in
+ (expR (expR t - 1) `^ fine mu)%:E *
+ (expR (- t * (1 + delta)) `^ fine mu)%:E <=
+ ((expR delta / (1 + delta) `^ (1 + delta)) `^ fine mu)%:E.
+Proof.
+move=> d0 /=.
+rewrite -EFinM lee_fin -powRM ?expR_ge0// ge0_ler_powR ?nnegrE//.
+- by rewrite fine_ge0// expectation_ge0// => x; exact: bernoulli_trial_ge0.
+- by rewrite divr_ge0// powR_ge0.
+- rewrite lnK ?posrE ?addr_gt0// addrAC subrr add0r ler_wpM2l ?expR_ge0//.
+ by rewrite -powRN mulNr -mulrN expRM lnK// posrE addr_gt0.
+Qed.
+
+(* [theorem 2.4, Rajani] / [thm 4.4.(2), MU] *)
+Theorem sampling_ineq1 n (X_ : n.-tuple (bernoulliRV P p)) (delta : R) :
+ (0 < delta)%R ->
+ let X := bool_trial_value X_ in
+ let mu := 'E_(\X_n P)[X] in
+ (\X_n P) [set i | X i >= (1 + delta) * fine mu]%R <=
+ ((expR delta / ((1 + delta) `^ (1 + delta))) `^ (fine mu))%:E.
+Proof.
+rewrite /= => delta0.
+set X := bool_trial_value X_.
+set mu := 'E_(\X_n P)[X].
+set t := ln (1 + delta).
+have t0 : (0 < t)%R by rewrite ln_gt0// ltrDl.
+apply: (le_trans (chernoff _ _ t0)).
+apply: (@le_trans _ _ ((expR (fine mu * (expR t - 1)))%:E *
+ (expR (- (t * ((1 + delta) * fine mu))))%:E)).
+ rewrite lee_pmul2r ?lte_fin ?expR_gt0//.
+ by apply: mmt_gen_fun_expectation => //; exact: ltW.
+rewrite mulrC expRM -mulNr mulrA expRM.
+exact: end_thm24.
+Qed.
+
+Section xlnx_bounding.
+Local Open Scope ring_scope.
+Local Arguments derive_val {R V W a v f df}.
+
+Let f (x : R) := x ^+ 2 - 2 * x * ln x.
+Let idf (x : R) : 0 < x -> {df : R | is_derive x 1 f df}.
+Proof.
+move=> x0.
+evar (df : (R : Type)); exists df.
+apply: is_deriveD; first by [].
+apply: is_deriveN.
+apply: is_deriveM; first by [].
+exact: is_derive1_ln.
+Defined.
+Let f1E : f 1 = 1. Proof. by rewrite /f expr1n ln1 !mulr0 subr0. Qed.
+Let Df_gt0 (x : R) : 0 < x -> x != 1 -> 0 < 'D_1 f x.
+Proof.
+move=> x0 x1.
+rewrite (derive_val (svalP (idf x0))) /=.
+clear idf.
+rewrite exp_derive deriveM// derive_cst derive_id .
+rewrite scaler0 addr0 /GRing.scale /= !mulr1 expr1.
+rewrite -mulrA divff ?lt0r_neq0//.
+rewrite (mulrC _ 2) -mulrDr -mulrBr mulr_gt0//.
+rewrite opprD addrA subr_gt0 -ltr_expR.
+have:= x0; rewrite -lnK_eq => /eqP ->.
+rewrite -[ltLHS]addr0 -(subrr 1) addrCA expR_gt1Dx//.
+by rewrite subr_eq0.
+Qed.
+
+Let sqrxB2xlnx_lt1 (c x : R) :
+ x \in `]0, 1[ -> x ^+ 2 - 2 * x * ln x < 1.
+Proof.
+rewrite in_itv=> /andP [] x0 x1.
+fold (f x).
+simpl in idf.
+rewrite -f1E.
+apply: (@gtr0_derive1_homo _ f 0 1 false false).
+- move=> t /[!in_itv] /= /andP [] + _.
+ by case/idf=> ? /@ex_derive.
+- move=> t /[!in_itv] /= /andP [] t0 t1.
+ apply: Df_gt0=> //.
+ by rewrite (lt_eqF t1).
+- apply: derivable_within_continuous => t /[!in_itv] /= /andP [] + _.
+ by case/idf=> ? /@ex_derive.
+- by rewrite in_itv/=; apply/andP; split=> //; apply/ltW.
+- by rewrite in_itv /= ltr01 lexx.
+- assumption.
+Qed.
+
+Let sqrxB2xlnx_gt1 (c x : R) :
+ 1 < x -> 1 < x ^+ 2 - 2 * x * ln x.
+Proof.
+move=> x1.
+have x0 : 0 < x by rewrite (lt_trans _ x1).
+fold (f x).
+simpl in idf.
+rewrite -f1E.
+apply: (@gtr0_derive1_homo _ f 1 x true false).
+- move=> t /[!in_itv] /= /andP [] + _ => t1.
+ have: 0 < t by rewrite (lt_trans _ t1).
+ by case/idf=> ? /@ex_derive.
+- move=> t /[!in_itv] /= /andP [] t1 tx.
+ have t0: 0 < t by rewrite (lt_trans _ t1).
+ apply: Df_gt0=> //.
+ by rewrite (gt_eqF t1).
+- apply: derivable_within_continuous => t /[!in_itv] /= /andP [] + _ => t1.
+ have: 0 < t by rewrite (lt_le_trans _ t1).
+ by case/idf=> ? /@ex_derive.
+- by rewrite in_itv/=; apply/andP; split=> //; apply/ltW.
+- by rewrite in_itv /= lexx andbT ltW.
+- assumption.
+Qed.
+
+Lemma xlnx_lbound_i01 (c x : R) :
+ c <= 2 -> x \in `]0, 1[ -> x ^+ 2 - 1 < c * x * ln x.
+Proof.
+pose c' := c - 2.
+have-> : c = c' + 2 by rewrite /c' addrAC -addrA subrr addr0.
+rewrite -lerBrDr subrr.
+move: c'; clear c => c.
+rewrite ltrBlDr -ltrBlDl.
+rewrite le_eqVlt=> /orP [/eqP-> |]; first by rewrite add0r; exact: sqrxB2xlnx_lt1.
+move=> c0 /[dup] x01 /[!in_itv] /andP [] x0 x1.
+rewrite -mulrA (addrC c) mulrDl !mulrA opprD addrA.
+rewrite -[ltRHS]addr0 ltrD// ?sqrxB2xlnx_lt1// oppr_lt0.
+by rewrite -mulrA nmulr_lgt0// nmulr_llt0// ln_lt0.
+Qed.
+
+Lemma xlnx_ubound_i1y (c x : R) :
+ c <= 2 -> 1 < x -> c * x * ln x < x ^+ 2 - 1.
+Proof.
+pose c' := c - 2.
+have-> : c = c' + 2 by rewrite /c' addrAC -addrA subrr addr0.
+rewrite -lerBrDr subrr.
+move: c'; clear c => c.
+rewrite ltrBrDr -ltrBrDl.
+rewrite le_eqVlt=> /orP [/eqP-> |]; first by rewrite add0r; exact: sqrxB2xlnx_gt1.
+move=> c0 x1.
+rewrite -mulrA (addrC c) mulrDl !mulrA opprD addrA.
+rewrite -[ltLHS]addr0 ltrD// ?sqrxB2xlnx_gt1// oppr_gt0.
+by rewrite nmulr_rlt0 ?ln_gt0// nmulr_rlt0 ?(lt_trans _ x1).
+Qed.
+End xlnx_bounding.
+
+(* [Theorem 2.6, Rajani] / [thm 4.5.(2), MU] *)
+Theorem sampling_ineq3 n (X : n.-tuple (bernoulliRV P p)) (delta : R) :
+ (0 < delta < 1)%R ->
+ let X' := bool_trial_value X : {RV \X_n P >-> R : realType} in
+ let mu := 'E_(\X_n P)[X'] in
+ (\X_n P) [set i | X' i <= (1 - delta) * fine mu]%R <= (expR (-(fine mu * delta ^+ 2) / 2)%R)%:E.
+Proof.
+move=> /andP[delta0 delta1] /=.
+set X' := bool_trial_value X : {RV \X_n P >-> R : realType}.
+set mu := 'E_(\X_n P)[X'].
+have /andP[p0 p1] := p01.
+apply: (@le_trans _ _ (((expR (- delta) / ((1 - delta) `^ (1 - delta))) `^ (fine mu))%:E)).
+ (* using Markov's inequality somewhere, see mu's book page 66 *)
+ have H1 t : (t < 0)%R ->
+ (\X_n P) [set i | (X' i <= (1 - delta) * fine mu)%R] = (\X_n P) [set i | `|(expR \o t \o* X') i|%:E >= (expR (t * (1 - delta) * fine mu))%:E].
+ move=> t0; apply: congr1; apply: eq_set => x /=.
+ rewrite lee_fin ger0_norm ?expR_ge0// ler_expR (mulrC _ t) -mulrA.
+ by rewrite -[in RHS]ler_ndivrMl// mulrA mulVf ?lt_eqF// mul1r.
+ set t := ln (1 - delta).
+ have ln1delta : (t < 0)%R.
+ (* TODO: lacking a lemma here *)
+ rewrite -oppr0 ltrNr -lnV ?posrE ?subr_gt0// ln_gt0//.
+ by rewrite invf_gt1// ?subr_gt0// ltrBlDr ltrDl.
+ have {H1}-> := H1 _ ln1delta.
+ apply: (@le_trans _ _ (((fine 'E_(\X_n P)[normr \o expR \o t \o* X']) / (expR (t * (1 - delta) * fine mu))))%:E).
+ rewrite EFinM lee_pdivlMr ?expR_gt0// muleC fineK.
+ apply: (@markov _ _ _ (\X_n P) (expR \o t \o* X' : {RV (\X_n P) >-> R : realType}) id (expR (t * (1 - delta) * fine mu))%R _ _ _ _) => //.
+ - by apply: expR_gt0.
+ - rewrite norm_expR.
+ have -> : 'E_(\X_n P)[expR \o t \o* X'] = 'M_X' t by [].
+ by rewrite binomial_mmt_gen_fun.
+ apply: (@le_trans _ _ (((expR ((expR t - 1) * fine mu)) / (expR (t * (1 - delta) * fine mu))))%:E).
+ rewrite norm_expR lee_fin ler_wpM2r ?invr_ge0 ?expR_ge0//.
+ have -> : 'E_(\X_n P)[expR \o t \o* X'] = 'M_X' t by [].
+ rewrite binomial_mmt_gen_fun//.
+ rewrite /mu /X' expectation_bernoulli_trial//.
+ rewrite !lnK ?posrE ?subr_gt0//.
+ rewrite expRM powRrM powRAC.
+ rewrite ge0_ler_powR ?ler0n// ?nnegrE ?powR_ge0//.
+ by rewrite addr_ge0 ?mulr_ge0// subr_ge0// ltW.
+ rewrite addrAC subrr sub0r -expRM.
+ rewrite addrCA -{2}(mulr1 p) -mulrBr addrAC subrr sub0r mulrC mulNr.
+ by apply: expR_ge1Dx.
+ rewrite !lnK ?posrE ?subr_gt0//.
+ rewrite -addrAC subrr sub0r -mulrA [X in (_ / X)%R]expRM lnK ?posrE ?subr_gt0//.
+ rewrite -[in leRHS]powR_inv1 ?powR_ge0// powRM// ?expR_ge0 ?invr_ge0 ?powR_ge0//.
+ by rewrite powRAC powR_inv1 ?powR_ge0// powRrM expRM.
+rewrite lee_fin.
+rewrite -mulrN -mulrA [in leRHS]mulrC expRM ge0_ler_powR// ?nnegrE.
+- by rewrite fine_ge0// expectation_ge0// => x; exact: bernoulli_trial_ge0.
+- by rewrite divr_ge0 ?expR_ge0// powR_ge0.
+- by rewrite expR_ge0.
+- rewrite -ler_ln ?posrE ?divr_gt0 ?expR_gt0 ?powR_gt0 ?subr_gt0//.
+ rewrite expRK// ln_div ?posrE ?expR_gt0 ?powR_gt0 ?subr_gt0//.
+ rewrite expRK//.
+ rewrite /powR (*TODO: lemma ln of powR*) gt_eqF ?subr_gt0// expRK.
+ (* analytical argument reduced to xlnx_lbound_i01; p.66 of mu's book *)
+ rewrite ler_pdivlMr// mulrDl.
+ rewrite -lerBrDr -lerBlDl !mulNr !opprK [in leRHS](mulrC _ 2) mulrA.
+ rewrite ltW// (le_lt_trans _ (xlnx_lbound_i01 _ _))//; last first.
+ by rewrite memB_itv add0r in_itv/=; apply/andP; split.
+ by rewrite addrC lerBrDr mulr_natr -[in leRHS]sqrrN opprB sqrrB1.
+Qed.
+End sampling_theorem_part1.
+
+(* this is a preliminary for the second part of the proof of the sampling lemma *)
+Module with_interval.
+Declare Scope bigQ_scope.
+Import Reals.
+Import Rstruct Rstruct_topology.
+Import Interval.Tactic.
+
+Section exp2_le8.
+Let R := Rdefinitions.R.
+Local Open Scope ring_scope.
+
+Lemma exp2_le8 : (exp 2 <= 8)%R.
+Proof. interval. Qed.
+
+Lemma exp2_le8_conversion : reflect (exp 2 <= 8)%R (expR 2 <= 8 :> R).
+Proof.
+rewrite RexpE (_ : 8%R = 8); last
+ by rewrite !mulrS -!RplusE Rplus_0_r !RplusA !IZRposE/=.
+by apply: (iffP idP) => /RleP.
+Qed.
+
+End exp2_le8.
+End with_interval.
+
+Section xlnx_bounding_with_interval.
+Let R := Rdefinitions.R.
+Local Open Scope ring_scope.
+
+Lemma xlnx_lbound_i12 (x : R) : x \in `]0, 1[ -> x + x^+2 / 3 <= (1 + x) * ln (1 + x).
+Proof.
+move=> x01; rewrite -subr_ge0.
+pose f (x : R^o) := (1 + x) * ln (1 + x) - (x + x ^+ 2 / 3).
+have f0 : f 0 = 0 by rewrite /f expr0n /= mul0r !addr0 ln1 mulr0 subr0.
+rewrite [leRHS](_ : _ = f x) // -f0.
+evar (df0 : R -> R); evar (df : R -> R).
+have idf (y : R^o) : 0 < 1 + y -> is_derive y (1:R) f (df y).
+ move=> y1.
+ rewrite (_ : df y = df0 y).
+ apply: is_deriveB; last exact: is_deriveD.
+ apply: is_deriveM=> //.
+ apply: is_derive1_comp=> //.
+ exact: is_derive1_ln.
+ rewrite /df0.
+ rewrite deriveD// derive_cst derive_id.
+ rewrite /GRing.scale /= !(mulr0,add0r,mulr1).
+ rewrite divff ?lt0r_neq0// opprD addrAC addrA subrr add0r.
+ instantiate (df := fun y : R => - (3^-1 * (y + y)) + ln (1 + y)).
+ reflexivity.
+clear df0.
+have y1cc y : y \in `[0, 1] -> 0 < 1 + y.
+ rewrite in_itv /= => /andP [] y0 ?.
+ by have y1: 0 < 1 + y by apply: (le_lt_trans y0); rewrite ltrDr.
+have y1oo y : y \in `]0, 1[ -> 0 < 1 + y by move/subset_itv_oo_cc/y1cc.
+have dfge0 y : y \in `]0, 1[ -> 0 <= df y.
+ move=> y01.
+ have:= y01.
+ rewrite /df in_itv /= => /andP [] y0 y1.
+ rewrite -lerBlDl opprK add0r -mulr2n -(mulr_natl _ 2) mulrA.
+ rewrite [in leLHS](_ : y = 1 + y - 1); last by rewrite addrAC subrr add0r.
+ pose iy:= Itv01 (ltW y0) (ltW y1).
+ have y1E: 1 + y = @convex.conv _ R^o iy 1 2.
+ rewrite convRE /= /onem mulr1 (mulr_natr _ 2) mulr2n.
+ by rewrite addrACA (addrC (- y)) subrr addr0.
+ rewrite y1E; apply: (le_trans _ (concave_ln _ _ _))=> //.
+ rewrite -y1E addrAC subrr add0r convRE ln1 mulr0 add0r /=.
+ rewrite mulrC ler_pM// ?(@ltW _ _ 0)// mulrC.
+ rewrite ler_pdivrMr//.
+ rewrite -[leLHS]expRK -[leRHS]expRK ler_ln ?posrE ?expR_gt0//.
+ rewrite expRM/= powR_mulrn ?expR_ge0// lnK ?posrE//.
+ rewrite !exprS expr0 mulr1 -!natrM mulnE /=.
+ exact/with_interval.exp2_le8_conversion/with_interval.exp2_le8.
+apply: (@ger0_derive1_homo R f 0 1 true false).
+- by move=> y /y1oo /idf /@ex_derive.
+- by move=> y /[dup] /y1oo /idf /@derive_val ->; exact: dfge0.
+- by apply: derivable_within_continuous=> y /y1cc /idf /@ex_derive.
+- by rewrite bound_itvE.
+- exact: subset_itv_oo_cc.
+- by have:= x01; rewrite in_itv=> /andP /= [] /ltW.
+Qed.
+
+End xlnx_bounding_with_interval.
+
+(* the rest of the sampling theorem including lemmas relying on the Rocq standard library *)
+Section sampling_theorem_part2.
+Local Open Scope ereal_scope.
+Let R := Rdefinitions.R.
+Context d (T : measurableType d) (P : probability T R).
+Variable p : R.
+Hypothesis p01 : (0 <= p <= 1)%R.
+Local Open Scope ereal_scope.
+
+(* [Theorem 2.5, Rajani] *)
+Theorem sampling_ineq2 n (X : n.-tuple (bernoulliRV P p)) (delta : R) :
+ let X' := bool_trial_value X in
+ let mu := 'E_(\X_n P)[X'] in
+ (0 < n)%nat ->
+ (0 < delta < 1)%R ->
+ (\X_n P) [set i | X' i >= (1 + delta) * fine mu]%R <=
+ (expR (- (fine mu * delta ^+ 2) / 3))%:E.
+Proof.
+move=> X' mu n0 /[dup] delta01 /andP[delta0 _].
+apply: (@le_trans _ _ (expR ((delta - (1 + delta) * ln (1 + delta)) * fine mu))%:E).
+ rewrite expRM expRB (mulrC _ (ln _)) expRM lnK; last rewrite posrE addr_gt0//.
+ exact: sampling_ineq1.
+apply: (@le_trans _ _ (expR ((delta - (delta + delta ^+ 2 / 3)) * fine mu))%:E).
+ rewrite lee_fin ler_expR ler_wpM2r//.
+ by rewrite fine_ge0//; apply: expectation_ge0 => t; exact: bernoulli_trial_ge0.
+ rewrite lerB//.
+ apply: xlnx_lbound_i12.
+ by rewrite in_itv /=.
+rewrite le_eqVlt; apply/orP; left; apply/eqP; congr (expR _)%:E.
+by rewrite opprD addrA subrr add0r mulrC mulrN mulNr mulrA.
+Qed.
+
+(* [Corollary 2.7, Rajani] / [Corollary 4.7, MU] *)
+Corollary sampling_ineq4 n (X : n.-tuple (bernoulliRV P p)) (delta : R) :
+ (0 < delta < 1)%R ->
+ (0 < n)%nat ->
+ (0 < p)%R ->
+ let X' := bool_trial_value X in
+ let mu := 'E_(\X_n P)[X'] in
+ (\X_n P) [set i | `|X' i - fine mu | >= delta * fine mu]%R <=
+ (expR (- (fine mu * delta ^+ 2) / 3)%R *+ 2)%:E.
+Proof.
+move=> /andP[d0 d1] n0 p0 /=.
+set X' := bool_trial_value X.
+set mu := 'E_(\X_n P)[X'].
+under eq_set => x.
+ rewrite ler_normr.
+ rewrite lerBrDl opprD opprK -{1}(mul1r (fine mu)) -mulrDl.
+ rewrite -lerBDr -(lerN2 (- _)%R) opprK opprB.
+ rewrite -{2}(mul1r (fine mu)) -mulrBl.
+ rewrite -!lee_fin.
+ over.
+rewrite /=.
+rewrite set_orb.
+rewrite measureU; last 3 first.
+- rewrite -(@setIidr _ setT [set _ | _]) ?subsetT//.
+ apply: emeasurable_fun_le => //.
+ apply/measurable_EFinP.
+ exact: measurableT_comp.
+- rewrite -(@setIidr _ setT [set _ | _]) ?subsetT//.
+ apply: emeasurable_fun_le => //.
+ apply/measurable_EFinP.
+ exact: measurableT_comp.
+- rewrite disjoints_subset => x /=.
+ rewrite /mem /in_mem/= => X0; apply/negP.
+ rewrite -ltNge.
+ apply: (@lt_le_trans _ _ _ _ _ _ X0).
+ rewrite !EFinM.
+ rewrite lte_pmul2r//; first by rewrite lte_fin ltrD2l gt0_cp.
+ by rewrite fineK /mu/X' expectation_bernoulli_trial// lte_fin mulr_gt0 ?ltr0n.
+rewrite mulr2n EFinD leeD//=.
+- by apply: sampling_ineq2; rewrite //d0 d1.
+- have d01 : (0 < delta < 1)%R by rewrite d0.
+ apply: (le_trans (@sampling_ineq3 _ _ _ _ p p01 _ X delta d01)).
+ rewrite lee_fin ler_expR !mulNr lerN2.
+ rewrite ler_pM//; last by rewrite lef_pV2 ?posrE ?ler_nat.
+ rewrite mulr_ge0 ?fine_ge0 ?sqr_ge0//.
+ rewrite /mu unlock /expectation integral_ge0// => x _.
+ by rewrite /X' lee_fin; exact: bernoulli_trial_ge0.
+Qed.
+
+(* [Theorem 3.1, Rajani] / [thm 4.7, MU] *)
+Theorem sampling n (X : n.-tuple (bernoulliRV P p)) (theta delta : R) :
+ let X' x := (bool_trial_value X x) / n%:R in
+ (0 < p)%R ->
+ (0 < delta <= 1)%R -> (0 < theta < p)%R -> (0 < n)%nat ->
+ (3 / theta ^+ 2 * ln (2 / delta) <= n%:R)%R ->
+ (\X_n P) [set i | `| X' i - p | <= theta]%R >= 1 - delta%:E.
+Proof.
+move=> X' p0 /andP[delta0 delta1] /andP[theta0 thetap] n0 tdn.
+have /andP[_ p1] := p01.
+set epsilon := theta / p.
+have epsilon01 : (0 < epsilon < 1)%R.
+ by rewrite /epsilon ?ltr_pdivrMr ?divr_gt0 ?mul1r.
+have thetaE : theta = (epsilon * p)%R.
+ by rewrite /epsilon -mulrA mulVf ?mulr1// gt_eqF.
+have step1 : (\X_n P) [set i | `| X' i - p | >= epsilon * p]%R <=
+ ((expR (- (p * n%:R * (epsilon ^+ 2)) / 3)) *+ 2)%:E.
+ rewrite [X in (\X_n P) X <= _](_ : _ =
+ [set i | `| bool_trial_value X i - p * n%:R | >= epsilon * p * n%:R]%R); last first.
+ apply/seteqP; split => [t|t]/=.
+ move/(@ler_wpM2r _ n%:R (ler0n _ _)) => /le_trans; apply.
+ rewrite -[X in (_ * X)%R](@ger0_norm _ n%:R)// -normrM mulrBl.
+ by rewrite -mulrA mulVf ?mulr1// ?gt_eqF ?ltr0n.
+ move/(@ler_wpM2r _ n%:R^-1); rewrite invr_ge0// ler0n => /(_ erefl).
+ rewrite -(mulrA _ _ n%:R^-1) divff ?mulr1 ?gt_eqF ?ltr0n//.
+ move=> /le_trans; apply.
+ rewrite -[X in (_ * X)%R](@ger0_norm _ n%:R^-1)// -normrM mulrBl.
+ by rewrite -mulrA divff ?mulr1// gt_eqF// ltr0n.
+ rewrite -mulrA.
+ have -> : (p * n%:R)%R = fine (p * n%:R)%:E by [].
+ rewrite -(mulrC _ p) -(expectation_bernoulli_trial p01 X).
+ exact: (@sampling_ineq4 _ X epsilon).
+have step2 : (\X_n P) [set i | `| X' i - p | >= theta]%R <=
+ ((expR (- (n%:R * theta ^+ 2) / 3)) *+ 2)%:E.
+ rewrite thetaE; move/le_trans : step1; apply.
+ rewrite lee_fin ler_wMn2r// ler_expR mulNr lerNl mulNr opprK.
+ rewrite -2![in leRHS]mulrA [in leRHS]mulrCA.
+ rewrite /epsilon -mulrA mulVf ?gt_eqF// mulr1 -!mulrA !ler_wpM2l ?(ltW theta0)//.
+ rewrite mulrCA ler_wpM2l ?(ltW theta0)//.
+ rewrite [X in (_ * X)%R]mulrA mulVf ?gt_eqF// -[leLHS]mul1r [in leRHS]mul1r.
+ by rewrite ler_wpM2r// invf_ge1.
+suff : delta%:E >= (\X_n P) [set i | (`|X' i - p| >=(*NB: this >= in the pdf *) theta)%R].
+ rewrite [X in (\X_n P) X <= _ -> _](_ : _ = ~` [set i | (`|X' i - p| < theta)%R]); last first.
+ apply/seteqP; split => [t|t]/=.
+ by rewrite leNgt => /negP.
+ by rewrite ltNge => /negP/negPn.
+ have ? : measurable [set i | (`|X' i - p| < theta)%R].
+ under eq_set => x do rewrite -lte_fin.
+ rewrite -(@setIidr _ setT [set _ | _]) ?subsetT /X'//.
+ by apply: emeasurable_fun_lt => //; apply: measurableT_comp => //;
+ apply: measurableT_comp => //; apply: measurable_funD => //;
+ apply: measurable_funM.
+ rewrite probability_setC// lee_subel_addr//.
+ rewrite -lee_subel_addl//; last by rewrite fin_num_measure.
+ move=> /le_trans; apply.
+ rewrite le_measure ?inE//.
+ under eq_set => x do rewrite -lee_fin.
+ rewrite -(@setIidr _ setT [set _ | _]) ?subsetT /X'//.
+ by apply: emeasurable_fun_le => //; apply: measurableT_comp => //;
+ apply: measurableT_comp => //; apply: measurable_funD => //;
+ apply: measurable_funM.
+ by move=> t/= /ltW.
+(* NB: last step in the pdf *)
+apply: (le_trans step2).
+rewrite lee_fin -(mulr_natr _ 2) -ler_pdivlMr//.
+rewrite -(@lnK _ (delta / 2)); last by rewrite posrE divr_gt0.
+rewrite ler_expR mulNr lerNl -lnV; last by rewrite posrE divr_gt0.
+rewrite invf_div ler_pdivlMr// mulrC.
+rewrite -ler_pdivrMr; last by rewrite exprn_gt0.
+by rewrite mulrAC.
+Qed.
+
+End sampling_theorem_part2.
diff --git a/theories/sequences.v b/theories/sequences.v
index cbe564d5f..1f5b0a8ee 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -282,6 +282,9 @@ apply/funext => n; rewrite -setIDA; apply/seteqP; split; last first.
by rewrite /seqDU -setIDA bigcup_mkord -big_distrr/= setDIr setIUr setDIK set0U.
Qed.
+Lemma subset_seqDU (A : (set T)^nat) (i : nat) : seqDU A i `<=` A i.
+Proof. by move=> ?; apply: subDsetl. Qed.
+
End seqDU.
Arguments trivIset_seqDU {T} F.
#[global] Hint Resolve trivIset_seqDU : core.
diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v
index 79bc3a1b3..82c92c727 100644
--- a/theories/topology_theory/nat_topology.v
+++ b/theories/topology_theory/nat_topology.v
@@ -38,7 +38,7 @@ Qed.
HB.instance Definition _ := Order_isNbhs.Build _ nat nat_nbhs_itv.
HB.instance Definition _ := DiscreteUniform_ofNbhs.Build nat.
-HB.instance Definition _ {R : numDomainType} :=
+HB.instance Definition _ {R : numDomainType} :=
@DiscretePseudoMetric_ofUniform.Build R nat.
Lemma nbhs_infty_gt N : \forall n \near \oo, (N < n)%N.
@@ -48,13 +48,16 @@ Proof. by exists N.+1. Qed.
Lemma nbhs_infty_ge N : \forall n \near \oo, (N <= n)%N.
Proof. by exists N. Qed.
-Lemma nbhs_infty_ger {R : realType} (r : R) :
- \forall n \near \oo, (r <= n%:R)%R.
+Lemma nbhs_infty_gtr {R : realType} (r : R) : \forall n \near \oo, r < n%:R.
Proof.
-exists `|Num.ceil r|%N => // n /=; rewrite -(ler_nat R); apply: le_trans.
-by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm.
+exists `|Num.ceil r|.+1%N => // n /=; rewrite -(ler_nat R); apply: lt_le_trans.
+rewrite (le_lt_trans (ceil_ge _))// -natr1 natr_absz ltr_pwDr// ler_int.
+exact: ler_norm.
Qed.
+Lemma nbhs_infty_ger {R : realType} (r : R) : \forall n \near \oo, r <= n%:R.
+Proof. by apply: filterS (nbhs_infty_gtr r) => x /ltW. Qed.
+
Lemma cvg_addnl N : addn N @ \oo --> \oo.
Proof.
by move=> P [n _ Pn]; exists (n - N)%N => // m; rewrite /= leq_subLR => /Pn.