generalizing expectation

CHANGELOG_UNRELEASED.md

@@ -56,6 +56,7 @@
     `nbhs_one_point_compactification_weakE`,
     `locally_compact_completely_regular`, and
     `completely_regular_regular`.
+  + new lemmas `near_in_itvoy`, `near_in_itvNyo`
 
 - in file `mathcomp_extra.v`,
   + new definition `sigT_fun`.
@@ -87,11 +88,76 @@
     `wedge_compact`, `wedge_connected`.
 
 - in `boolp.`:
-  + lemma `existT_inj`
+  + lemma `existT_inj2`
 - in file `order_topology.v`
   + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and
     `max_fun_continuous`.
 
+- in file `boolp.v`,
+  + new lemmas `uncurryK`, and `curryK`
+- in file `weak_topology.v`,
+  + new lemma `continuous_comp_weak`
+- in file `function_spaces.v`,
+  + new definition `eval`
+  + new lemmas `continuous_curry_fun`, `continuous_curry_cvg`, 
+    `eval_continuous`, and `compose_continuous`
+
+- in file `wedge_sigT.v`,
++ new definitions `wedge_fun`, and `wedge_prod`.
++ new lemmas `wedge_fun_continuous`, `wedge_lift_funE`, 
+  `wedge_fun_comp`, `wedge_prod_pointE`, `wedge_prod_inj`, 
+  `wedge_prod_continuous`, `wedge_prod_open`, `wedge_hausdorff`, and 
+  `wedge_fun_joint_continuous`.
+
+- in `boolp.v`:
+  + lemmas `existT_inj1`, `surjective_existT`
+
+- in file `homotopy_theory/path.v`,
+  + new definitions `reparameterize`, `mk_path`, and `chain_path`.
+  + new lemmas `path_eqP`, and `chain_path_cts_point`.
+- in file `homotopy_theory/wedge_sigT.v`,
+  + new definition `bpwedge_shared_pt`.
+  + new notations `bpwedge`, and `bpwedge_lift`.
+- 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 `approx_A` (was `Let A`)
+  + definition `approx_B` (was `Let B`)
+  + lemma `measurable_fun_sum`
+  + lemma `integrable_indic`
+
+- 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 file `normedtype.v`,
@@ -143,10 +209,48 @@
     `subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`,
     `setX_of_sigTK`, `setX_of_sigT_continuous`, and `sigT_of_setX_continuous`.
 
+- in `tvs.v`:
+  + HB structures `NbhsNmodule`, `NbhsZmodule`, `NbhsLmodule`, `TopologicalNmodule`,
+    `TopologicalZmodule`
+  + notation `topologicalLmoduleType`, HB structure `TopologicalLmodule`
+  + HB structures `UniformZmodule`, `UniformLmodule`
+  + definition `convex`
+  + mixin `Uniform_isTvs`
+  + type `tvsType`, HB.structure `Tvs`
+  + HB.factory `TopologicalLmod_isTvs`
+  + lemma `nbhs0N`
+  + lemma `nbhsN`
+  + lemma `nbhsT`
+  + lemma `nbhsB`
+  + lemma `nbhs0Z`
+  + lemma `nbhZ`
+
+- in `lebesgue_integrale.v`
+  + change implicits of `measurable_funP`
+
 ### Changed
 
+- in normedtype.v
+  + HB structure `normedModule` now depends on a Tvs
+    instead of a Lmodule
+  + Factory `PseudoMetricNormedZmod_Lmodule_isNormedModule` becomes
+    `PseudoMetricNormedZmod_Tvs_isNormedModule`
+  + Section `prod_NormedModule` now depends on a `numFieldType`
+
 ### Renamed
 
+- in `normedtype.v`:
+  + `near_in_itv` -> `near_in_itvoo`
+
+- in normedtype.v
+  + Section `regular_topology` to `standard_topology`
+
+- in `lebesgue_measure.v`:
+  + `measurable_fun_indic` -> `measurable_indic`
+
+- in `probability.v`:
+  + `expectationM` -> `expectationMl`
+
 ### Generalized
 
 - in `lebesgue_integral.v`:
@@ -161,6 +265,9 @@
 - in `topology_structure.v`:
   + lemma `closureC`
 
+- in file `lebesgue_integral.v`:
+  + lemma `approximation`
+
 ### Removed
 
 - in `lebesgue_integral.v`:
@@ -175,6 +282,10 @@
   + 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)
+
 ### Infrastructure
 
 ### Misc

_CoqProject

@@ -63,11 +63,13 @@ theories/topology_theory/sigT_topology.v
 
 theories/homotopy_theory/homotopy.v
 theories/homotopy_theory/wedge_sigT.v
+theories/homotopy_theory/path.v
 
 theories/separation_axioms.v
 theories/function_spaces.v
 theories/ereal.v
 theories/cantor.v
+theories/tvs.v
 theories/normedtype.v
 theories/realfun.v
 theories/sequences.v

classical/boolp.v

@@ -88,13 +88,21 @@ move=> PQA; suff: {x | P x /\ Q x} by move=> [a [*]]; exists a.
 by apply: cid; case: PQA => x; exists x.
 Qed.
 
-Lemma existT_inj (A : eqType) (P : A -> Type) (p : A) (x y : P p) :
-  existT P p x = existT P p y -> x = y.
+Lemma existT_inj1 (T : Type) (P : T -> Type) (x y : T) (Px : P x) (Py : P y) :
+  existT P x Px = existT P y Py -> x = y.
+Proof. by case. Qed.
+
+Lemma existT_inj2 (T : eqType) (P : T -> Type) (x : T) (Px1 Px2 : P x) :
+  existT P x Px1 = existT P x Px2 -> Px1 = Px2.
 Proof.
-apply: Eqdep_dec.inj_pair2_eq_dec => a b.
-by have [|/eqP] := eqVneq a b; [left|right].
+apply: Eqdep_dec.inj_pair2_eq_dec => y z.
+by have [|/eqP] := eqVneq y z; [left|right].
 Qed.
 
+Lemma surjective_existT (T : Type) (P : T -> Type) (p : {x : T & P x}):
+  existT [eta P] (projT1 p) (projT2 p) = p.
+Proof. by case: p. Qed.
+
 Record mextensionality := {
   _ : forall (P Q : Prop), (P <-> Q) -> (P = Q);
   _ : forall {T U : Type} (f g : T -> U),
@@ -969,3 +977,9 @@ Lemma inhabited_witness: inhabited T -> T.
 Proof. by rewrite inhabitedE => /cid[]. Qed.
 
 End Inhabited.
+
+Lemma uncurryK {X Y Z : Type} : cancel (@uncurry X Y Z) curry.
+Proof. by move=> f; rewrite funeq2E. Qed.
+
+Lemma curryK {X Y Z : Type} : cancel curry (@uncurry X Y Z).
+Proof. by move=> f; rewrite funeqE=> -[]. Qed.

classical/classical_sets.v

@@ -2485,6 +2485,16 @@ Proof. by apply/eqP => /seteqP[] /(_ point) /(_ Logic.I). Qed.
 
 End PointedTheory.
 
+HB.mixin Record isBiPointed (X : Type) of Equality X := {
+  zero : X;
+  one : X;
+  zero_one_neq : zero != one;
+}.
+
+#[short(type="biPointedType")]
+HB.structure Definition BiPointed := 
+  { X of Choice X & isBiPointed X }.
+
 Variant squashed T : Prop := squash (x : T).
 Arguments squash {T} x.
 Notation "$| T |" := (squashed T) : form_scope.

reals/constructive_ereal.v

@@ -551,6 +551,31 @@ Notation "\sum_ ( i 'in' A ) F" :=
 Notation "\sum_ ( i 'in' A ) F" :=
   (\big[+%E/0%E]_(i in A) F%E) : ereal_scope.
 
+Notation "\prod_ ( i <- r | P ) F" :=
+  (\big[*%E/1%:E]_(i <- r | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( i <- r ) F" :=
+  (\big[*%E/1%:E]_(i <- r) F%E) : ereal_scope.
+Notation "\prod_ ( m <= i < n | P ) F" :=
+  (\big[*%E/1%:E]_(m <= i < n | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( m <= i < n ) F" :=
+  (\big[*%E/1%:E]_(m <= i < n) F%E) : ereal_scope.
+Notation "\prod_ ( i | P ) F" :=
+  (\big[*%E/1%:E]_(i | P%B) F%E) : ereal_scope.
+Notation "\prod_ i F" :=
+  (\big[*%E/1%:E]_i F%E) : ereal_scope.
+Notation "\prod_ ( i : t | P ) F" :=
+  (\big[*%E/1%:E]_(i : t | P%B) F%E) (only parsing) : ereal_scope.
+Notation "\prod_ ( i : t ) F" :=
+  (\big[*%E/1%:E]_(i : t) F%E) (only parsing) : ereal_scope.
+Notation "\prod_ ( i < n | P ) F" :=
+  (\big[*%E/1%:E]_(i < n | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( i < n ) F" :=
+  (\big[*%E/1%:E]_(i < n) F%E) : ereal_scope.
+Notation "\prod_ ( i 'in' A | P ) F" :=
+  (\big[*%E/1%:E]_(i in A | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( i 'in' A ) F" :=
+  (\big[*%E/1%:E]_(i in A) F%E) : ereal_scope.
+
 Section ERealOrderTheory.
 Context {R : numDomainType}.
 Implicit Types x y z : \bar R.

theories/Make

@@ -31,10 +31,12 @@ topology_theory/sigT_topology.v
 
 homotopy_theory/homotopy.v
 homotopy_theory/wedge_sigT.v
+homotopy_theory/path.v
 
 separation_axioms.v
 function_spaces.v
 cantor.v
+tvs.v
 normedtype.v
 realfun.v
 sequences.v

theories/charge.v

@@ -92,7 +92,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
-Import numFieldTopology.Exports.
+Import numFieldNormedType.Exports.
 
 Local Open Scope ring_scope.
 Local Open Scope classical_set_scope.
@@ -1921,29 +1921,29 @@ Lemma change_of_variables f E : (forall x, 0 <= f x) ->
   \int[mu]_(x in E) (f x * ('d nu '/d mu) x) = \int[nu]_(x in E) f x.
 Proof.
 move=> f0 mE mf; set g := 'd nu '/d mu.
-have [h [ndh hf]] := approximation mE mf (fun x _ => f0 x).
+pose h := nnsfun_approx mE mf.
 have -> : \int[nu]_(x in E) f x =
     lim (\int[nu]_(x in E) (EFin \o h n) x @[n --> \oo]).
   have fE x : E x -> f x = lim ((EFin \o h n) x @[n --> \oo]).
-    by move=> Ex; apply/esym/cvg_lim => //; exact: hf.
+    by move=> Ex; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
   under eq_integral => x /[!inE] /fE -> //.
   apply: monotone_convergence => //.
   - move=> n; apply/measurable_EFinP.
     by apply: (measurable_funS measurableT) => //; exact/measurable_funP.
   - by move=> n x Ex //=; rewrite lee_fin.
-  - by move=> x Ex a b /ndh /=; rewrite lee_fin => /lefP.
+  - by move=> x Ex a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
 have -> : \int[mu]_(x in E) (f \* g) x =
     lim (\int[mu]_(x in E) ((EFin \o h n) \* g) x @[n --> \oo]).
   have fg x :E x -> f x * g x = lim (((EFin \o h n) \* g) x @[n --> \oo]).
     by move=> Ex; apply/esym/cvg_lim => //; apply: cvgeMr;
-      [exact: f_fin_num|exact: hf].
+      [exact: f_fin_num|exact: cvg_nnsfun_approx].
   under eq_integral => x /[!inE] /fg -> //.
   apply: monotone_convergence => [//| | |].
   - move=> n; apply/emeasurable_funM; apply/measurable_funTS.
       exact/measurable_EFinP.
     exact: measurable_int (f_integrable _).
   - by move=> n x Ex //=; rewrite mule_ge0 ?lee_fin//=; exact: f_ge0.
-  - by move=> x Ex a b /ndh /= /lefP hahb; rewrite lee_wpmul2r ?lee_fin// f_ge0.
+  - by move=> x Ex a b ab/=; rewrite lee_wpmul2r ?lee_fin ?f_ge0//; exact/lefP/nd_nnsfun_approx.
 suff suf n : \int[mu]_(x in E) ((EFin \o h n) x * g x) =
     \int[nu]_(x in E) (EFin \o h n) x.
   by under eq_fun do rewrite suf.
@@ -2008,7 +2008,7 @@ Proof.
 move=> numu mula mE; have nula := measure_dominates_trans numu mula.
 have mf : measurable_fun E ('d nu '/d mu).
   exact/measurable_funTS/(measurable_int _ (f_integrable _)).
-have [h [ndh hf]] := approximation mE mf (fun x _ => f_ge0 numu x).
+pose h := approximation mE mf.
 apply: integral_ae_eq => //.
 - apply: (integrableS measurableT) => //.
   apply: f_integrable.
@@ -2018,7 +2018,7 @@ apply: integral_ae_eq => //.
 - move=> A AE mA; rewrite change_of_variables//.
   + by rewrite -!f_integral.
   + exact: f_ge0.
-  + exact: measurable_funS mf.
+  + by move: (mf); exact: measurable_funS.
 Qed.
 
 End chain_rule.

theories/derive.v

@@ -2,8 +2,8 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import reals signed topology prodnormedzmodule normedtype.
-From mathcomp Require Import landau forms.
+From mathcomp Require Import reals signed topology prodnormedzmodule tvs.
+From mathcomp Require Import normedtype landau forms.
 
 (**md**************************************************************************)
 (* # Differentiation                                                          *)
@@ -788,13 +788,14 @@ by rewrite prod_normE/= !normrZ !normfV !normr_id !mulVf ?gt_eqF// maxxx ltr1n.
 Qed.
 
 Lemma bilinear_eqo (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) :
-  continuous (fun p => f p.1 p.2) -> (fun p => f p.1 p.2) =o_ 0 id.
+  continuous (fun p => f p.1 p.2) -> (fun p => f p.1 p.2) =o_ (0 : U * V') id.
 Proof.
 move=> fc; have [_ /posnumP[k] fschwarz] := bilinear_schwarz fc.
 apply/eqoP=> _ /posnumP[e]; near=> x; rewrite (le_trans (fschwarz _ _))//.
 rewrite ler_pM ?pmulr_rge0 //; last by rewrite num_le_max /= lexx orbT.
 rewrite -ler_pdivlMl //.
-suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite num_le_max /= lexx.
+suff : `|x| <= k%:num ^-1 * e%:num.
+  by apply: le_trans; rewrite num_le_max /= lexx.
 near: x; rewrite !near_simpl; apply/nbhs_le_nbhs_norm.
 by exists (k%:num ^-1 * e%:num) => //= ? /=; rewrite /= distrC subr0 => /ltW.
 Unshelve. all: by end_near. Qed.
@@ -803,7 +804,7 @@ Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p :
   continuous (fun p => f p.1 p.2) ->
   continuous (fun q => (f p.1 q.2 + f q.1 p.2)) /\
   (fun q => f q.1 q.2) \o shift p = cst (f p.1 p.2) +
-    (fun q => f p.1 q.2 + f q.1 p.2) +o_ 0 id.
+    (fun q => f p.1 q.2 + f q.1 p.2) +o_ (0 : U * V') id.
 Proof.
 move=> fc; split=> [q|].
   by apply: (@continuousD _ _ _ (fun q => f p.1 q.2) (fun q => f q.1 p.2));

theories/exp.v

@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import mathcomp_extra reals ereal signed.
-From mathcomp Require Import topology normedtype landau sequences derive.
+From mathcomp Require Import topology tvs normedtype landau sequences derive.
 From mathcomp Require Import realfun itv convex.
 
 (**md**************************************************************************)
@@ -228,7 +228,7 @@ suff Cc : limn (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> limn (series s).
 apply: cvg_zero => /=.
 suff Cc : limn
     (series (fun n => c n * (((h + x) ^+ n - x ^+ n) / h - n%:R * x ^+ n.-1)))
-    @[h --> 0^'] --> (0 : R).
+    @[h --> 0^'] --> 0.
   apply: cvg_sub0 Cc.
   apply/cvgrPdist_lt => eps eps_gt0 /=.
   near=> h; rewrite sub0r normrN /=.