expectation of product

CHANGELOG_UNRELEASED.md

@@ -14,6 +14,25 @@
   + lemma `partition_disjoint_bigfcup`
 - in `lebesgue_measure.v`:
   + lemma `measurable_indicP`
+- in `constructive_ereal.v`:
+  + notation `\prod_( i <- r | P ) F` for extended real numbers and its variants
+
+- in `numfun.v`:
+  + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-`
+  + lemmas `funrpos_ge0`, `funrneg_ge0`, `funrposN`, `funrnegN`, `ge0_funrposE`,
+    `ge0_funrnegE`, `le0_funrposE`, `le0_funrnegE`, `ge0_funrposM`, `ge0_funrnegM`,
+    `le0_funrposM`, `le0_funrnegM`, `funr_normr`, `funrposneg`, `funrD_Dpos`,
+    `funrD_posD`, `funrpos_le`, `funrneg_le`
+  + lemmas `funerpos`, `funerneg`
+
+- in `measure.v`:
+  + lemma `preimage_class_comp`
+  + defintions `mapping_display`, `g_sigma_algebra_mappingType`, `g_sigma_algebra_mapping`,
+    notations `.-mapping`, `.-mapping.-measurable`
+
+- in `lebesgue_measure.v`:
+  + lemma `measurable_indicP`
+  + lemmas `measurable_funrpos`, `measurable_funrneg`
 
 - in `lebesgue_integral.v`:
   + definition `dyadic_approx` (was `Let A`)
@@ -27,12 +46,80 @@
 - in `probability.v`:
   + lemma `expectation_def`
   + notation `'M_`
+- in `probability.v`:
+  + lemma `expectationM_ge0`
+  + definition `independent_events`
+  + definition `mutual_independence`
+  + definition `independent_RVs`
+  + definition `independent_RVs2`
+  + lemmas `g_sigma_algebra_mapping_comp`, `g_sigma_algebra_mapping_funrpos`,
+    `g_sigma_algebra_mapping_funrneg`
+  + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`,
+    `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`,
+    `independent_RVs2_funrpospos`
+  + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`,
+    ` expectation_prod`
 
 ### Changed
 
 - in `lebesgue_integrale.v`
   + change implicits of `measurable_funP`
 
+
+- in file `normedtype.v`,
+     changed `completely_regular_space` to depend on uniform separators
+     which removes the dependency on `R`.  The old formulation can be
+     recovered easily with `uniform_separatorP`.
+
+- moved from `Rstruct.v` to `Rstruct_topology.v`
+  + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`,
+    `continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_dnbhs`
+    and `nbhs_pt_comp`
+
+- moved from `real_interval.v` to `normedtype.v`
+  + lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`,
+    `Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`,
+    `disj_itv_Rhull`
+- in `topology.v`:
+  + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`,
+    `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned
+	into local `Let`'s
+
+- in `lebesgue_integral.v`:
+  + structure `SimpleFun` now inside a module `HBSimple`
+  + structure `NonNegSimpleFun` now inside a module `HBNNSimple`
+  + lemma `cst_nnfun_subproof` has now a different statement
+  + lemma `indic_nnfun_subproof` has now a different statement
+- in `mathcomp_extra.v`:
+  + definition `idempotent_fun`
+
+- in `topology_structure.v`:
+  + definitions `regopen`, `regclosed`
+  + lemmas `closure_setC`, `interiorC`, `closureU`, `interiorU`,
+           `closureEbigcap`, `interiorEbigcup`,
+	   `closure_open_regclosed`, `interior_closed_regopen`,
+	   `closure_interior_idem`, `interior_closure_idem`
+
+- in file `topology_structure.v`,
+  + mixin `isContinuous`, type `continuousType`, structure `Continuous`
+  + new lemma `continuousEP`.
+  + new definition `mkcts`.
+
+- in file `subspace_topology.v`,
+  + new lemmas `continuous_subspace_setT`, `nbhs_prodX_subspace_inE`, and
+    `continuous_subspace_prodP`.
+  + type `continuousFunType`, HB structure `ContinuousFun`
+
+- in file `subtype_topology.v`,
+  + new lemmas `subspace_subtypeP`, `subspace_sigL_continuousP`,
+    `subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`,
+    `setX_of_sigTK`, `setX_of_sigT_continuous`, and `sigT_of_setX_continuous`.
+
+- in `lebesgue_integrale.v`
+  + change implicits of `measurable_funP`
+
+### Changed
+
 ### Renamed
 
 - in `lebesgue_measure.v`:
@@ -55,6 +142,9 @@
   + `mineMr` -> `mine_pMr`
   + `mineMl` -> `mine_pMl`
 
+- in `probability.v`:
+  + `expectationM` -> `expectationMl`
+
 ### Generalized
 
 - in `probability.v`:
@@ -76,6 +166,26 @@
 
 ### Removed
 
+- in `topology_structure.v`:
+  + lemma `closureC`
+
+- in file `lebesgue_integral.v`:
+  + lemma `approximation`
+
+### Removed
+
+- in `lebesgue_integral.v`:
+  + definition `cst_mfun`
+  + lemma `mfun_cst`
+
+- in `cardinality.v`:
+  + lemma `cst_fimfun_subproof`
+
+- in `lebesgue_integral.v`:
+  + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead)
+  + lemma `cst_nnfun_subproof` (turned into a `Let`)
+  + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead)
+
 - in `lebesgue_integral.v`:
   + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`)
   + notation `measurable_fun_indic` (deprecation since 0.6.3)

theories/lebesgue_integral.v

@@ -1608,7 +1608,11 @@ move=> m n mn; rewrite (nnsfun_approxE n) (nnsfun_approxE m).
 exact: nd_approx.
 Qed.
 
+<<<<<<< HEAD
 #[deprecated(since="mathcomp-analysis 1.8.0", note="use `nnsfun_approx`, `cvg_nnsfun_approx`, and `nd_nnsfun_approx` instead")]
+=======
+#[deprecated(since="mathcomp-analysis 1.7.0", note="use `nnsfun_approx`, `cvg_nnsfun_approx`, and `nd_nnsfun_approx` instead")]
+>>>>>>> da1f3437 (expectation of product)
 Lemma approximation : (forall t, D t -> (0 <= f t)%E) ->
   exists g : {nnsfun T >-> R}^nat, nondecreasing_seq (g : (T -> R)^nat) /\
                         (forall x, D x -> EFin \o g^~ x @ \oo --> f x).

theories/lebesgue_measure.v

@@ -1053,6 +1053,12 @@ by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //;
   [exact: measurable_fun_ltr|exact: measurable_funS mg|exact: measurable_funS mf].
 Qed.
 
+Lemma measurable_funrpos D f : measurable_fun D f -> measurable_fun D f^\+.
+Proof. by move=> mf; exact: measurable_maxr. Qed.
+
+Lemma measurable_funrneg D f : measurable_fun D f -> measurable_fun D f^\-.
+Proof. by move=> mf; apply: measurable_maxr => //; exact: measurableT_comp. Qed.
+
 Lemma measurable_minr D f g :
   measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \min g).
 Proof.

theories/measure.v

@@ -70,6 +70,11 @@ From HB Require Import structures.
 (*   G.-sigma.-measurable A == A is measurable for the sigma-algebra <<s G >> *)
 (*    g_sigma_algebraType G == the measurableType corresponding to <<s G >>   *)
 (*                             This is an HB alias.                           *)
+(* g_sigma_algebra_mapping f == sigma-algebra generated by the mapping f      *)
+(* g_sigma_algebra_mappingType f == the measurableType corresponding to       *)
+(*                             g_sigma_algebra_mapping f                      *)
+(*                             This is an HB alias.                           *)
+(* f.-mapping.-measurable A == A is measurable for g_sigma_algebra_mapping f  *)
 (*    mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets  *)
 (* ```                                                                        *)
 (*                                                                            *)
@@ -296,6 +301,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 .-mapping" (at level 1, format "f .-mapping").
+Reserved Notation "f .-mapping.-measurable"
+ (at level 2, format "f .-mapping.-measurable").
 Reserved Notation "d .-ring" (at level 1, format "d .-ring").
 Reserved Notation "d .-ring.-measurable"
  (at level 2, format "d .-ring.-measurable").
@@ -1729,6 +1737,16 @@ Definition preimage_class (aT rT : Type) (D : set aT) (f : aT -> rT)
     (G : set (set rT)) : set (set aT) :=
   [set D `&` f @^-1` B | B in G].
 
+Lemma preimage_class_comp (aT : Type)
+    d (rT : measurableType d) d' (T : sigmaRingType d')
+    (g : rT -> T) (f : aT -> rT) (D : set aT) :
+  measurable_fun setT g ->
+  preimage_class D (g \o f) measurable `<=` preimage_class D f measurable.
+Proof.
+move=> mg A; rewrite /preimage_class/= => -[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_class_measurable_fun d (aT : pointedType) (rT : measurableType d)
   (D : set aT) (f : aT -> rT) :
@@ -1813,6 +1831,58 @@ Qed.
 
 End measurability.
 
+Definition mapping_display {T T'} : (T -> T') -> measure_display.
+Proof. exact. Qed.
+
+Definition g_sigma_algebra_mappingType d' (T : pointedType)
+  (T' : measurableType d') (f : T -> T') : Type := T.
+
+Definition g_sigma_algebra_mapping d' (T : pointedType)
+    (T' : measurableType d') (f : T -> T') :=
+  preimage_class setT f (@measurable _ T').
+
+Section mapping_generated_sigma_algebra.
+Context {d'} (T : pointedType) (T' : measurableType d').
+Variable f : T -> T'.
+
+Let mapping_set0 : g_sigma_algebra_mapping f set0.
+Proof.
+rewrite /g_sigma_algebra_mapping /preimage_class/=.
+by exists set0 => //; rewrite preimage_set0 setI0.
+Qed.
+
+Let mapping_setC A :
+  g_sigma_algebra_mapping f A -> g_sigma_algebra_mapping f (~` A).
+Proof.
+rewrite /g_sigma_algebra_mapping /preimage_class/= => -[B mB] <-{A}.
+by exists (~` B); [exact: measurableC|rewrite !setTI preimage_setC].
+Qed.
+
+Let mapping_bigcup (F : (set T)^nat) :
+  (forall i, g_sigma_algebra_mapping f (F i)) ->
+  g_sigma_algebra_mapping f (\bigcup_i (F i)).
+Proof.
+move=> mF; rewrite /g_sigma_algebra_mapping /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_mappingType f).
+
+HB.instance Definition _ := @isMeasurable.Build (mapping_display f)
+  (g_sigma_algebra_mappingType f) (g_sigma_algebra_mapping f)
+  mapping_set0 mapping_setC mapping_bigcup.
+
+End mapping_generated_sigma_algebra.
+
+Notation "f .-mapping" := (mapping_display f) : measure_display_scope.
+Notation "f .-mapping.-measurable" :=
+  (measurable : set (set (g_sigma_algebra_mappingType f))) : classical_set_scope.
+
 Local Open Scope ereal_scope.
 
 Definition subset_sigma_subadditive {T} {R : numFieldType}