letinA

Author: affeldt-aist

theories/kernel.v

@@ -41,27 +41,6 @@ Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 Local Open Scope ereal_scope.
 
-(* PR 516 in progress *)
-HB.mixin Record isProbability d (T : measurableType d)
-  (R : realType) (P : set T -> \bar R) of isMeasure d R T P :=
-  { probability_setT : P setT = 1%E }.
-
-#[short(type=probability)]
-HB.structure Definition Probability d (T : measurableType d) (R : realType) :=
-  {P of isProbability d T R P & isMeasure d R T P }.
-
-Section probability_lemmas.
-Context d (T : measurableType d) (R : realType) (P : probability T R).
-
-Lemma probability_le1 (A : set T) : measurable A -> (P A <= 1)%E.
-Proof.
-move=> mA; rewrite -(@probability_setT _ _ _ P).
-by apply: le_measure => //; rewrite ?in_setE.
-Qed.
-
-End probability_lemmas.
-(* /PR 516 in progress *)
-
 (* TODO: PR*)
 Lemma setT0 (T : pointedType) : setT != set0 :> set T.
 Proof. by apply/eqP => /seteqP[] /(_ point) /(_ Logic.I). Qed.
@@ -684,10 +663,10 @@ Lemma measurable_fun_xsection_integral
 Proof.
 move=> h.
 rewrite (_ : (fun x => _) =
-    (fun x => elim_sup (fun n => \int[l x]_y (k_ n (x, y))%:E))); last first.
+    (fun x => lim_esup (fun n => \int[l x]_y (k_ n (x, y))%:E))); last first.
   apply/funext => x.
   transitivity (lim (fun n => \int[l x]_y (k_ n (x, y))%:E)); last first.
-    rewrite is_cvg_elim_supE//.
+    rewrite is_cvg_lim_esupE//.
     apply: ereal_nondecreasing_is_cvg => m n mn.
     apply: ge0_le_integral => //.
     - by move=> y _; rewrite lee_fin.
@@ -996,7 +975,7 @@ case: ifPn => [_|_]; first exact: measure_semi_sigma_additive.
 rewrite (_ : (fun _ => _) = ((fun n => \sum_(0 <= i < n) f x (F i)) \*
                           cst ((fine (f x setT))^-1)%:E)); last first.
   by apply/funext => n; rewrite -ge0_sume_distrl.
-by apply: ereal_cvgMr => //; exact: measure_semi_sigma_additive.
+by apply: cvgeMr => //; exact: measure_semi_sigma_additive.
 Qed.
 
 HB.instance Definition _ x := isMeasure.Build _ _ _ (mnormalize x)
@@ -1173,8 +1152,8 @@ Variable k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z.
 
 Import KCOMP_FINITE_KERNEL.
 
-Lemma mkcomp_sfinite : exists k_ : (R.-fker X ~> Z)^nat, forall x U, measurable U ->
-  (l \; k) x U = kseries k_ x U.
+Lemma mkcomp_sfinite : exists k_ : (R.-fker X ~> Z)^nat,
+  forall x U, measurable U -> (l \; k) x U = kseries k_ x U.
 Proof.
 have [k_ hk_] := sfinite k; have [l_ hl_] := sfinite l.
 have [kl hkl] : exists kl : (R.-fker X ~> Z) ^nat, forall x U,

theories/prob_lang.v

@@ -408,7 +408,7 @@ Section insn2.
 Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 
 Definition ret (f : X -> Y) (mf : measurable_fun setT f)
-  : R.-sfker X ~> Y := [the R.-sfker _ ~> _ of kdirac mf].
+  : R.-pker X ~> Y := [the R.-pker _ ~> _ of kdirac mf].
 
 Definition sample (P : pprobability Y R) : R.-pker X ~> Y :=
   [the R.-pker _ ~> _ of kprobability (measurable_fun_cst P)].
@@ -632,6 +632,35 @@ Qed.
 
 End letin_ite.
 
+Section letinA.
+Context d d' d1 d2 d3 (X : measurableType d) (Y : measurableType d')
+  (T1 : measurableType d1) (T2 : measurableType d2) (T3 : measurableType d3)
+  (R : realType).
+Import Notations.
+Variables (t : R.-sfker X ~> T1)
+          (u : R.-sfker [the measurableType _ of (X * T1)%type] ~> T2)
+          (v : R.-sfker [the measurableType _ of (X * T2)%type] ~> Y)
+          (v' : R.-sfker [the measurableType _ of (X * T1 * T2)%type] ~> Y)
+          (vv' : forall y, v =1 fun xz => v' (xz.1, y, xz.2)).
+
+Lemma letinA x A : measurable A ->
+  letin t (letin u v') x A
+  =
+  (letin (letin t u) v) x A.
+Proof.
+move=> mA.
+rewrite !letinE.
+under eq_integral do rewrite letinE.
+rewrite integral_kcomp; [|by []|].
+- apply: eq_integral => y _.
+  apply: eq_integral => z _.
+  by rewrite (vv' y).
+have /measurable_fun_prod1 := @measurable_kernel _ _ _ _ _ v _ mA.
+exact.
+Qed.
+
+End letinA.
+
 Section letinC.
 Context d d1 d' (X : measurableType d) (Y : measurableType d1)
   (Z : measurableType d') (R : realType).
@@ -677,12 +706,18 @@ Section constants.
 Variable R : realType.
 Local Open Scope ring_scope.
 
-Lemma onem12 : `1- (1 / 2%:R) = (1%:R / 2%:R)%:nng%:num :> R.
-Proof. by rewrite /onem/= {1}(splitr 1) addrK. Qed.
+Lemma onem1S n : `1- (1 / n.+1%:R) = (n%:R / n.+1%:R)%:nng%:num :> R.
+Proof.
+by rewrite /onem/= -{1}(@divrr _ n.+1%:R) ?unitfE// -mulrBl -natr1 addrK.
+Qed.
 
-Lemma p12 : (1 / 2%:R)%:nng%:num <= 1 :> R.
+Lemma p1S n : (1 / n.+1%:R)%:nng%:num <= 1 :> R.
 Proof. by rewrite ler_pdivr_mulr//= mul1r ler1n. Qed.
 
+Lemma p12 : (1 / 2%:R)%:nng%:num <= 1 :> R. Proof. by rewrite p1S. Qed.
+
+Lemma p14 : (1 / 4%:R)%:nng%:num <= 1 :> R. Proof. by rewrite p1S. Qed.
+
 Lemma onem27 : `1- (2 / 7%:R) = (5%:R / 7%:R)%:nng%:num :> R.
 Proof. by apply/eqP; rewrite subr_eq/= -mulrDl -natrD divrr// unitfE. Qed.
 
@@ -691,6 +726,7 @@ Proof. by rewrite /= lter_pdivr_mulr// mul1r ler_nat. Qed.
 
 End constants.
 Arguments p12 {R}.
+Arguments p14 {R}.
 Arguments p27 {R}.
 
 Section poisson.
@@ -833,7 +869,8 @@ Definition bernoulli_and : R.-sfker T ~> mbool :=
         (ret (measurable_fun_mand var2of3 var3of3)))).
 
 Lemma bernoulli_andE t U :
-  bernoulli_and t U = (1 / 4 * \1_U true)%:E + (3 / 4 * \1_U false)%:E.
+  bernoulli_and t U =
+  sample [the probability _ _ of bernoulli p14] t U.
 Proof.
 rewrite /bernoulli_and.
 rewrite !letin_sample_bernoulli//=.
@@ -844,12 +881,14 @@ rewrite !muleA.
 rewrite -addeA.
 rewrite -muleDl//.
 rewrite -!EFinM.
-rewrite !onem12/= -splitr mulr1.
+rewrite !onem1S/= -splitr mulr1.
 have -> : (1 / 2 * (1 / 2) = 1 / 4 :> R)%R.
   by rewrite mulf_div mulr1// -natrM.
-congr (_ + (_ * _)%:E).
+rewrite /bernoulli/= measure_addE/= /mscale/= -!EFinM.
+congr( _ + (_ * _)%:E).
 have -> : (1 / 2 = 2 / 4 :> R)%R.
   by apply/eqP; rewrite eqr_div// ?pnatr_eq0// mul1r -natrM.
+rewrite onem1S//.
 by rewrite -mulrDl.
 Qed.
 
@@ -968,4 +1007,3 @@ by rewrite addr_gt0// mulr_gt0//= ?divr_gt0// ?ltr0n// exp_density_gt0 ?ltr0n.
 Qed.
 
 End staton_bus_exponential.
-