wip

theories/lebesgue_integral.v

@@ -4617,7 +4617,7 @@ End measurable_fun_ysection.
 
 Section product_measures.
 Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
-Context (m1 : {measure set T1 -> \bar R}) (m2 : {measure set T2 -> \bar R}).
+Context (m1 : set T1 -> \bar R) (m2 : set T2 -> \bar R).
 
 Definition product_measure1 := (fun A => \int[m1]_x (m2 \o xsection A) x)%E.
 Definition product_measure2 := (fun A => \int[m2]_x (m1 \o ysection A) x)%E.
@@ -4635,19 +4635,16 @@ Variable m2 : {sigma_finite_measure set T2 -> \bar R}.
 Implicit Types A : set (T1 * T2).
 
 Let pm10 : (m1 \x m2) set0 = 0.
-Proof. by rewrite [LHS]integral0_eq// => x/= _; rewrite xsection0 measure0. Qed.
+Proof. by rewrite [LHS]integral0_eq// => x/= _; rewrite xsection0. Qed.
 
 Let pm1_ge0 A : 0 <= (m1 \x m2) A.
-Proof.
-by apply: integral_ge0 => // *; exact/measure_ge0/measurable_xsection.
-Qed.
+Proof. by apply: integral_ge0 => // *. Qed.
 
 Let pm1_sigma_additive : semi_sigma_additive (m1 \x m2).
 Proof.
 move=> F mF tF mUF.
 rewrite [X in _ --> X](_ : _ = \sum_(n <oo) (m1 \x m2) (F n)).
-  apply/cvg_closeP; split; last by rewrite closeE.
-  by apply: is_cvg_nneseries => *; exact: integral_ge0.
+  by apply/cvg_closeP; split; [exact: is_cvg_nneseries|rewrite closeE].
 rewrite -integral_nneseries//; last by move=> n; exact: measurable_fun_xsection.
 apply: eq_integral => x _; apply/esym/cvg_lim => //=; rewrite xsection_bigcup.
 apply: (measure_sigma_additive _ (trivIset_xsection tF)) => ?.
@@ -4686,41 +4683,53 @@ Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
 Variable m1 : {sigma_finite_measure set T1 -> \bar R}.
 Variable m2 : {sigma_finite_measure set T2 -> \bar R}.
 
+Let product_measure_sigma_finite : sigma_finite setT (m1 \x m2).
+Proof.
+have /sigma_finiteP[F TF [ndF Foo]] := sigma_finiteT m1.
+have /sigma_finiteP[G TG [ndG Goo]] := sigma_finiteT m2.
+exists (fun n => F n `*` G n).
+ rewrite -setMTT TF TG predeqE => -[x y]; split.
+    move=> [/= [n _ Fnx] [k _ Gky]]; exists (maxn n k) => //; split.
+    - by move: x Fnx; exact/subsetPset/ndF/leq_maxl.
+    - by move: y Gky; exact/subsetPset/ndG/leq_maxr.
+  by move=> [n _ []/= ? ?]; split; exists n.
+move=> k; have [? ?] := Foo k; have [? ?] := Goo k.
+split; first exact: measurableM.
+by rewrite product_measure1E// lte_mul_pinfty// ge0_fin_numE.
+Qed.
+
+HB.instance Definition _ := Measure_isSigmaFinite.Build _ _ _ (m1 \x m2)
+  product_measure_sigma_finite.
+
 Lemma product_measure_unique
     (m' : {measure set [the semiRingOfSetsType _ of T1 * T2] -> \bar R}) :
-    (forall A1 A2, measurable A1 -> measurable A2 ->
-      m' (A1 `*` A2) = m1 A1 * m2 A2) ->
+    (forall A B, measurable A -> measurable B -> m' (A `*` B) = m1 A * m2 B) ->
   forall X : set (T1 * T2), measurable X -> (m1 \x m2) X = m' X.
 Proof.
-move=> m'E; pose m := product_measure1 m1 m2.
-have /sigma_finiteP [F1 F1_T [F1_nd F1_oo]] := sigma_finiteT m1.
-have /sigma_finiteP [F2 F2_T [F2_nd F2_oo]] := sigma_finiteT m2.
-have UF12T : \bigcup_k (F1 k `*` F2 k) = setT.
-  rewrite -setMTT F1_T F2_T predeqE => -[x y]; split.
+move=> m'E.
+have /sigma_finiteP[F TF [ndF Foo]] := sigma_finiteT m1.
+have /sigma_finiteP[G TG [ndG Goo]] := sigma_finiteT m2.
+have UFGT : \bigcup_k (F k `*` G k) = setT.
+  rewrite -setMTT TF TG predeqE => -[x y]; split.
     by move=> [n _ []/= ? ?]; split; exists n.
-  move=> [/= [n _ F1nx] [k _ F2ky]]; exists (maxn n k) => //; split.
-  - by move: x F1nx; apply/subsetPset/F1_nd; rewrite leq_maxl.
-  - by move: y F2ky; apply/subsetPset/F2_nd; rewrite leq_maxr.
-have mF1F2 n : measurable (F1 n `*` F2 n) /\ m (F1 n `*` F2 n) < +oo.
-  have [? ?] := F1_oo n; have [? ?] := F2_oo n.
-  split; first exact: measurableM.
-  by rewrite /m product_measure1E // lte_mul_pinfty// ge0_fin_numE.
-have sm : sigma_finite setT m by exists (fun n => F1 n `*` F2 n).
-pose C : set (set (T1 * T2)) := [set C |
-  exists A1, measurable A1 /\ exists A2, measurable A2 /\ C = A1 `*` A2].
+  move=> [/= [n _ Fnx] [k _ Gky]]; exists (maxn n k) => //; split.
+  - by move: x Fnx; exact/subsetPset/ndF/leq_maxl.
+  - by move: y Gky; exact/subsetPset/ndG/leq_maxr.
+pose C : set (set (T1 * T2)) :=
+  [set C | exists A, measurable A /\ exists B, measurable B /\ C = A `*` B].
 have CI : setI_closed C.
   move=> /= _ _ [X1 [mX1 [X2 [mX2 ->]]]] [Y1 [mY1 [Y2 [mY2 ->]]]].
   rewrite -setMI; exists (X1 `&` Y1); split; first exact: measurableI.
   by exists (X2 `&` Y2); split => //; exact: measurableI.
-move=> X mX; apply: (measure_unique C (fun n => F1 n `*` F2 n)) => //.
+move=> X mX; apply: (measure_unique C (fun n => F n `*` G n)) => //.
 - rewrite measurable_prod_measurableType //; congr (<<s _ >>).
-  rewrite predeqE; split => [[A1 mA1 [A2 mA2 <-]]|[A1 [mA1 [A2 [mA2 ->]]]]].
-    by exists A1; split => //; exists A2; split.
-  by exists A1 => //; exists A2.
-- move=> n; rewrite /C /=; exists (F1 n); split; first by have [] := F1_oo n.
-  by exists (F2 n); split => //; have [] := F2_oo n.
+  rewrite predeqE; split => [[A mA [B mB <-]]|[A [mA [B [mB ->]]]]].
+    by exists A; split => //; exists B.
+  by exists A => //; exists B.
+- move=> n; rewrite /C /=; exists (F n); split; first by have [] := Foo n.
+  by exists (G n); split => //; have [] := Goo n.
 - by move=> A [A1 [mA1 [A2 [mA2 ->]]]]; rewrite m'E//= product_measure1E.
-- move=> k; have [? ?] := F1_oo k; have [? ?] := F2_oo k.
+- move=> k; have [? ?] := Foo k; have [? ?] := Goo k.
   by rewrite /= product_measure1E// lte_mul_pinfty// ge0_fin_numE.
 Qed.
 

theories/lebesgue_measure.v

@@ -341,6 +341,8 @@ Definition lebesgue_measure {R : realType} :
 HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R).
 HB.instance Definition _ (R : realType) :=
   SigmaFiniteContent.on (@lebesgue_measure R).
+HB.instance Definition _ (R : realType) :=
+  SigmaFiniteMeasure.on (@lebesgue_measure R).
 
 Section ps_infty.
 Context {T : Type}.

theories/lebesgue_stieltjes_measure.v

@@ -497,7 +497,7 @@ Lemma sigmaT_finite_lebesgue_stieltjes_measure (f : cumulative R) :
   sigma_finite setT (lebesgue_stieltjes_measure f).
 Proof. exact/measure_extension_sigma_finite/wlength_sigma_finite. Qed.
 
-HB.instance Definition _ (f : cumulative R) := @isSigmaFinite.Build _ _ _
+HB.instance Definition _ (f : cumulative R) := @Measure_isSigmaFinite.Build _ _ _
   (lebesgue_stieltjes_measure f) (sigmaT_finite_lebesgue_stieltjes_measure f).
 
 End wlength_extension.

theories/probability.v

@@ -256,6 +256,68 @@ End expectation_lemmas.
 (* TODO: move *)
 From mathcomp Require Import fsbigop.
 
+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 (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.
+
+(* independent class of events, klenke def 2.11, p.59 *)
+Section independent_class.
+Context {d : measure_display} {T : measurableType d} {R : realType}
+        {P : probability T R}.
+Variable (I : choiceType) (E : I -> set (set T)).
+Hypothesis mE : forall i, E i `<=` measurable.
+
+Definition independent_class :=
+  forall J : {fset I},
+    forall e : I -> set T, (forall i, (E i) (e i)) ->
+      P (\big[setI/setT]_(i <- J) e i) = (\prod_(i <- J) P (e i))%E.
+
+End independent_class.
+
 Section independent_events.
 Context d (T : measurableType d) (R : realType) (P : probability T R).
 Local Open Scope ereal_scope.
@@ -641,9 +703,13 @@ Qed.
 
 Lemma inde_expectation (I : choiceType) (A : set I) (X : I -> {RV P >-> R}) :
   mutually_independent_RV A X ->
-    forall B : {fset I}, [set` B] `<=` A -> 'E_P[\prod_(i <- B) X i] = \prod_(i <- B) 'E_P[X i].
+    forall B : {fset I}, [set` B] `<=` A ->
+    'E_P[\prod_(i <- B) X i] = \prod_(i <- B) 'E_P[X i].
 Proof.
-move=> irvX B BleA.
+move=> AX B BA.
+rewrite [in LHS]unlock.
+rewrite /mutually_independent_RV in AX.
+rewrite /mutually_independent in AX.
 Admitted.
 
 End independent_RVs.