Skip to content

Commit

Permalink
rebase wrt branch on finite measures
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist committed Feb 12, 2023
1 parent 2e923d4 commit 9038840
Show file tree
Hide file tree
Showing 3 changed files with 64 additions and 57 deletions.
74 changes: 29 additions & 45 deletions theories/kernel.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,37 +53,23 @@ apply: measurableU.
exact: emeasurable_itv_bnd_pinfty.
Qed.

Definition sfinite_measure d (T : measurableType d) (R : realType)
(mu : set T -> \bar R) :=
exists2 s : {measure set T -> \bar R}^nat,
forall n, finite_measure (s n) & forall U, measurable U -> mu U = mseries s 0 U.

Lemma finite_measure_sigma_finite d (T : measurableType d) (R : realType)
(mu : {measure set T -> \bar R}) :
finite_measure mu -> sigma_finite setT mu.
Proof.
exists (fun i => if i \in [set 0%N] then setT else set0).
by rewrite -bigcup_mkcondr setTI bigcup_const//; exists 0%N.
move=> n; split; first by case: ifPn.
by case: ifPn => // _; rewrite ?measure0//; exact: finite_measure.
Qed.

Section sfinite_fubini.
Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
Variables (m1 : {measure set X -> \bar R}) (sfm1 : sfinite_measure m1).
Variables (m2 : {measure set Y -> \bar R}) (sfm2 : sfinite_measure m2).
Variables (m1 : {sfinite_measure set X -> \bar R}).
Variables (m2 : {sfinite_measure set Y -> \bar R}).
Variables (f : X * Y -> \bar R) (f0 : forall xy, 0 <= f xy).
Hypothesis mf : measurable_fun setT f.

Lemma sfinite_fubini :
\int[m1]_x \int[m2]_y f (x, y) = \int[m2]_y \int[m1]_x f (x, y).
Proof.
have [s1 fm1 m1E] := sfm1.
have [s2 fm2 m2E] := sfm2.
have [s1 m1E] := sfinite_measure m1.
have [s2 m2E] := sfinite_measure m2.
rewrite [LHS](eq_measure_integral [the measure _ _ of mseries s1 0]); last first.
by move=> A mA _; rewrite m1E.
by move=> A mA _; rewrite /= -m1E.
transitivity (\int[mseries s1 0]_x \int[mseries s2 0]_y f (x, y)).
by apply eq_integral => x _; apply: eq_measure_integral => ? ? _; rewrite m2E.
apply eq_integral => x _; apply: eq_measure_integral => ? ? _.
by rewrite /= -m2E.
transitivity (\sum_(n <oo) \int[s1 n]_x \sum_(m <oo) \int[s2 m]_y f (x, y)).
rewrite ge0_integral_measure_series; [|by []| |]; last 2 first.
by move=> t _; exact: integral_ge0.
Expand All @@ -92,27 +78,23 @@ transitivity (\sum_(n <oo) \int[s1 n]_x \sum_(m <oo) \int[s2 m]_y f (x, y)).
apply/funext => x.
by rewrite ge0_integral_measure_series//; exact/measurable_fun_prod1.
apply: ge0_emeasurable_fun_sum; first by move=> k x; exact: integral_ge0.
move=> k; apply: measurable_fun_fubini_tonelli_F => //=.
exact: finite_measure_sigma_finite.
by move=> k; apply: measurable_fun_fubini_tonelli_F.
apply: eq_eseries => n _; apply eq_integral => x _.
by rewrite ge0_integral_measure_series//; exact/measurable_fun_prod1.
transitivity (\sum_(n <oo) \sum_(m <oo) \int[s1 n]_x \int[s2 m]_y f (x, y)).
apply eq_eseries => n _; rewrite integral_nneseries//.
move=> m; apply: measurable_fun_fubini_tonelli_F => //=.
exact: finite_measure_sigma_finite.
by move=> m; exact: measurable_fun_fubini_tonelli_F.
by move=> m x _; exact: integral_ge0.
transitivity (\sum_(n <oo) \sum_(m <oo) \int[s2 m]_y \int[s1 n]_x f (x, y)).
apply eq_eseries => n _; apply eq_eseries => m _.
by rewrite fubini_tonelli//; exact: finite_measure_sigma_finite.
transitivity (\sum_(n <oo) \int[mseries s2 0]_y \int[s1 n]_x f (x, y)).
apply eq_eseries => n _ /=. rewrite ge0_integral_measure_series//.
by move=> y _; exact: integral_ge0.
apply: measurable_fun_fubini_tonelli_G => //=.
by apply: finite_measure_sigma_finite; exact: fm1.
exact: measurable_fun_fubini_tonelli_G.
transitivity (\int[mseries s2 0]_y \sum_(n <oo) \int[s1 n]_x f (x, y)).
rewrite integral_nneseries//.
move=> n; apply: measurable_fun_fubini_tonelli_G => //=.
by apply: finite_measure_sigma_finite; exact: fm1.
by move=> n; apply: measurable_fun_fubini_tonelli_G.
by move=> n y _; exact: integral_ge0.
transitivity (\int[mseries s2 0]_y \int[mseries s1 0]_x f (x, y)).
apply eq_integral => y _.
Expand All @@ -123,7 +105,7 @@ by apply eq_integral => y _; apply eq_measure_integral => A mA _ /=; rewrite m1E
Qed.

End sfinite_fubini.
Arguments sfinite_fubini {d d' X Y R m1} _ {m2} _ f.
Arguments sfinite_fubini {d d' X Y R} m1 m2 f.

Reserved Notation "R .-ker X ~> Y" (at level 42, format "R .-ker X ~> Y").
Reserved Notation "R .-sfker X ~> Y" (at level 42, format "R .-sfker X ~> Y").
Expand All @@ -143,8 +125,8 @@ Notation "R .-ker X ~> Y" := (kernel X Y R).

Arguments measurable_kernel {_ _ _ _ _} _.

Lemma eq_kernel d d' (T : measurableType d) (T' : measurableType d') (R : realType)
(k1 k2 : R.-ker T ~> T') :
Lemma eq_kernel d d' (T : measurableType d) (T' : measurableType d')
(R : realType) (k1 k2 : R.-ker T ~> T') :
(forall x U, k1 x U = k2 x U) -> k1 = k2.
Proof.
move: k1 k2 => [m1 [[?]]] [m2 [[?]]] /= k12.
Expand Down Expand Up @@ -314,6 +296,17 @@ Qed.

End sfinite.

Lemma sfinite_kernel_measure d d' (Z : measurableType d) (X : measurableType d')
(R : realType) (k : R.-sfker Z ~> X) (z : Z) :
sfinite_measure_def (k z).
Proof.
have [s ks] := sfinite k.
exists (s ^~ z).
move=> n; have [r snr] := measure_uub (s n).
by rewrite /finite_measure (lt_le_trans (snr _))// leey.
by move=> U mU; rewrite ks.
Qed.

HB.instance Definition _ d d' (X : measurableType d)
(Y : measurableType d') (R : realType) :=
@Kernel_isFinite.Build _ _ _ _ R (@kzero _ _ X Y R)
Expand Down Expand Up @@ -411,16 +404,6 @@ have [r k_r] := measure_uub k.
by rewrite /finite_measure (@lt_trans _ _ r%:E) ?ltey.
Qed.

Lemma sfinite_kernel_measure d d' (X : measurableType d)
(Y : measurableType d') (R : realType) (k : R.-sfker X ~> Y) (x : X) :
sfinite_measure (k x).
Proof.
have [k_ k_E] := sfinite k.
exists (fun n => k_ n x); last by move=> A mA; rewrite k_E.
move=> n; rewrite /finite_measure.
exact: finite_kernel_measure.
Qed.

(* see measurable_prod_subset in lebesgue_integral.v;
the differences between the two are:
- m2 is a kernel instead of a measure (the proof uses the
Expand Down Expand Up @@ -1068,12 +1051,12 @@ Let k_2 : (X * Y -> R)^nat := fun n => k_ n \o snd.

Let k_2_ge0 n x : (0 <= k_2 n x)%R. Proof. by []. Qed.

HB.instance Definition _ n := @IsNonNegFun.Build _ _ _ (k_2_ge0 n).
HB.instance Definition _ n := @isNonNegFun.Build _ _ _ (k_2_ge0 n).

Let mk_2 n : measurable_fun setT (k_2 n).
Proof. by apply: measurable_funT_comp => //; exact: measurable_fun_snd. Qed.

HB.instance Definition _ n := @IsMeasurableFun.Build _ _ _ _ (mk_2 n).
HB.instance Definition _ n := @isMeasurableFun.Build _ _ _ _ (mk_2 n).

Let fk_2 n : finite_set (range (k_2 n)).
Proof.
Expand All @@ -1096,7 +1079,8 @@ move=> h; apply: (measurable_fun_xsection_integral (k \o snd) l
have := h n r measurableT B mB; rewrite !setTI.
suff : (l ^~ (k_ n @^-1` [set r])) @^-1` B =
(fun x => l x (xsection (k_2 n @^-1` [set r]) x)) @^-1` B by move=> ->.
by apply/seteqP; split => x/=; rewrite xsection_preimage_snd.
by apply/seteqP; split => x/=;
rewrite (comp_preimage _ snd (k_ n)) xsection_preimage_snd.
Qed.

End measurable_fun_preimage_integral.
Expand Down
39 changes: 31 additions & 8 deletions theories/prob_lang.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,9 +50,6 @@ Proof. by rewrite /onem/= subr_ge0. Qed.
Definition onem_nonneg (R : numDomainType) (p : {nonneg R})
(p1 : (p%:num <= 1)%R) :=
NngNum (onem_nonneg_proof p1).

Lemma expR_ge0 (R : realType) (x : R) : (0 <= expR x)%R.
Proof. by rewrite ltW// expR_gt0. Qed.
(* /TODO: PR *)

Section bernoulli.
Expand Down Expand Up @@ -674,6 +671,30 @@ Variables (t : R.-sfker Z ~> X)
(u' : R.-sfker [the measurableType _ of (Z * X)%type] ~> Y)
(uu' : forall x, u =1 fun z => u' (z, x)).

Definition T z : set X -> \bar R := t z.
Let T0 z : (T z) set0 = 0. Proof. by []. Qed.
Let T_ge0 z x : 0 <= (T z) x. Proof. by []. Qed.
Let T_semi_sigma_additive z : semi_sigma_additive (T z).
Proof. exact: measure_semi_sigma_additive. Qed.
HB.instance Definition _ z := @isMeasure.Build _ R X (T z) (T0 z) (T_ge0 z)
(@T_semi_sigma_additive z).

Let sfinT z : sfinite_measure_def (T z). Proof. exact: sfinite_kernel_measure. Qed.
HB.instance Definition _ z := @Measure_isSFinite_subdef.Build _ X R
(T z) (sfinT z).

Definition U z : set Y -> \bar R := u z.
Let U0 z : (U z) set0 = 0. Proof. by []. Qed.
Let U_ge0 z x : 0 <= (U z) x. Proof. by []. Qed.
Let U_semi_sigma_additive z : semi_sigma_additive (U z).
Proof. exact: measure_semi_sigma_additive. Qed.
HB.instance Definition _ z := @isMeasure.Build _ R Y (U z) (U0 z) (U_ge0 z)
(@U_semi_sigma_additive z).

Let sfinU z : sfinite_measure_def (U z). Proof. exact: sfinite_kernel_measure. Qed.
HB.instance Definition _ z := @Measure_isSFinite_subdef.Build _ Y R
(U z) (sfinU z).

Lemma letinC z A : measurable A ->
letin t
(letin u'
Expand All @@ -689,13 +710,15 @@ under eq_integral.
rewrite letinE -uu'.
under eq_integral do rewrite retE /=.
over.
rewrite (sfinite_fubini _ _ (fun x => \d_(x.1, x.2) A ))//; last 3 first.
exact: sfinite_kernel_measure.
exact: sfinite_kernel_measure.
rewrite (sfinite_fubini
[the {sfinite_measure set X -> \bar R} of T z]
[the {sfinite_measure set Y -> \bar R} of U z]
(fun x => \d_(x.1, x.2) A ))//; last first.
apply/EFin_measurable_fun => /=; rewrite (_ : (fun x => _) = mindic R mA)//.
by apply/funext => -[].
apply eq_integral => y _.
by rewrite letinE/= -tt'; apply eq_integral => // x _; rewrite retE.
rewrite /=.
apply: eq_integral => y _.
by rewrite letinE/= -tt'; apply: eq_integral => // x _; rewrite retE.
Qed.

End letinC.
Expand Down
8 changes: 4 additions & 4 deletions theories/wip.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,10 +51,10 @@ Lemma measurable_fun_gauss_density m s :
measurable_fun setT (gauss_density m s).
Proof.
apply: measurable_funM; first exact: measurable_fun_cst.
apply: measurable_fun_comp => /=.
apply: measurable_funT_comp => /=.
by apply: continuous_measurable_fun; apply continuous_expR.
apply: measurable_funM; last exact: measurable_fun_cst.
apply: measurable_fun_comp => /=; first exact: measurable_fun_opp.
apply: measurable_funT_comp => /=; first exact: measurable_fun_opp.
apply: measurable_fun_exprn.
apply: measurable_funM => /=; last exact: measurable_fun_cst.
apply: measurable_funD => //; first exact: measurable_fun_id.
Expand Down Expand Up @@ -111,7 +111,7 @@ Let f1 (x : R) := (gauss01_density x) ^-1.

Let mf1 : measurable_fun setT f1.
Proof.
apply: (measurable_fun_comp' (F := [set r : R | r != 0%R])) => //.
apply: (measurable_fun_comp (F := [set r : R | r != 0%R])) => //.
- exact: open_measurable.
- by move=> /= r [t _ <-]; rewrite gt_eqF// gauss_density_gt0.
- apply: open_continuous_measurable_fun => //.
Expand All @@ -124,7 +124,7 @@ Variable mu : {measure set mR R -> \bar R}.
Definition staton_lebesgue : R.-sfker T ~> _ :=
letin (sample (@gauss01 R))
(letin
(score (measurable_fun_comp mf1 var2of2))
(score (measurable_funT_comp mf1 var2of2))
(ret var2of3)).

Lemma staton_lebesgueE x U : measurable U ->
Expand Down

0 comments on commit 9038840

Please sign in to comment.