diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 83b78d3cac..dc67809d18 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -20,4 +20,4 @@ ### Infrastructure -### Misc +### Misc \ No newline at end of file diff --git a/_CoqProject b/_CoqProject index 1a9dd0cdc9..a8ebbde651 100644 --- a/_CoqProject +++ b/_CoqProject @@ -34,10 +34,16 @@ theories/lebesgue_measure.v theories/forms.v theories/derive.v theories/measure.v +theories/kernel.v +theories/prob_lang.v theories/numfun.v theories/lebesgue_integral.v +theories/kernel.v theories/summability.v theories/signed.v +theories/prob_lang.v +theories/wip.v +theories/lang_syntax.v theories/altreals/xfinmap.v theories/altreals/discrete.v theories/altreals/realseq.v diff --git a/theories/binomial.v b/theories/binomial.v new file mode 100644 index 0000000000..e9dc4c8488 --- /dev/null +++ b/theories/binomial.v @@ -0,0 +1,71 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +Require Import mathcomp_extra boolp classical_sets signed functions cardinality. +Require Import reals ereal topology normedtype sequences esum measure. +Require Import lebesgue_measure fsbigop numfun lebesgue_integral kernel. +Require Import prob_lang. + +Local Open Scope ring_scope. +Import Order.TTheory GRing.Theory Num.Def Num.ExtraDef Num.Theory. + +Section bernoulli. +Variable (R : realType) (p : {nonneg R}%R) (p1 : (p%:num <= 1)%R). + +Lemma b10 : bernoulli p1 [set 0%N] = (`1-(p%:num))%:E. +Proof. +rewrite /bernoulli/= /measure_add/= /msum. +rewrite 2!big_ord_recr/= big_ord0 add0e. +rewrite /mscale/= !diracE memNset// mem_set//= mule1 mule0 add0e //. +Qed. + +Lemma b11 : bernoulli p1 [set 1%N] = p%:num%:E. +Proof. +rewrite /bernoulli/= /measure_add/= /msum. +rewrite 2!big_ord_recr/= big_ord0 add0e. +rewrite /mscale/= !diracE mem_set// memNset//= mule1 mule0 adde0 //. +Qed. + +End bernoulli. +Section binomial. +Variables (R : realType). + +Definition binomial2 (p : {nonneg R}) (p1 : p%:num <= 1) := + measure_add + (mscale (p%:num ^+ 2)%:nng (dirac 2%N)) + (measure_add + (mscale (2 * p%:num * (onem_nonneg p1)%:num)%:nng (dirac 1%N)) + (mscale ((onem_nonneg p1)%:num ^+ 2)%:nng (dirac 0%N))). + +Lemma b20 p p1 : binomial2 p p1 [set 2%N] = (p%:num ^+ 2)%:E. +Proof. +rewrite /binomial2/= /measure_add/= /msum !big_ord_recr/= big_ord0 add0e. +rewrite /msum !big_ord_recr/= big_ord0 add0e. +rewrite /mscale/= !diracE mem_set//= memNset// memNset// mule1 mule0 mule0 add0e adde0//. +Qed. + +End binomial. + +Section example. +Variables (R : realType). + +Goal binomial2 R (1 / 2)%:nng p12 [set 2%N] = (1 / 4)%:E. +Proof. +rewrite b20 /= expr2. +by rewrite mulf_div -natrM [in LHS]mul1r. +Qed. + +(* Lemma measurable_fun_bernoulli (U : set _) : + measurable U -> + measurable_fun setT (@bernoulli R p). +Proof. +move=> mU. +by apply: ge0_emeasurable_fun_sum => // n; exact/measurable_kernel. +Qed. *) + +HB.instance Definition _ := + isKernel.Build _ _ _ _ _ (bernoulli p1) measurable_fun_kseries. + +Check letin bernoulli. + +Check p27. + diff --git a/theories/kernel.v b/theories/kernel.v new file mode 100644 index 0000000000..80c2a1cf35 --- /dev/null +++ b/theories/kernel.v @@ -0,0 +1,1186 @@ +(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +Require Import mathcomp_extra boolp classical_sets signed functions cardinality. +Require Import reals ereal topology normedtype sequences esum measure. +Require Import lebesgue_measure fsbigop numfun lebesgue_integral. + +(******************************************************************************) +(* Kernels *) +(* *) +(* This file provides a formation of kernels and extends the theory of *) +(* measures with, e.g., Tonelli-Fubini's theorem for s-finite measures. *) +(* The main result is the fact that s-finite kernels are stable by *) +(* composition. *) +(* *) +(* finite_measure mu == the measure mu is finite *) +(* sfinite_measure mu == the measure mu is s-finite *) +(* R.-ker X ~> Y == kernel *) +(* kseries == countable sum of kernels *) +(* R.-sfker X ~> Y == s-finite kernel *) +(* R.-fker X ~> Y == finite kernel *) +(* R.-spker X ~> Y == subprobability kernel *) +(* R.-pker X ~> Y == probability kernel *) +(* mset U r == the set probability measures mu such that mu U < r *) +(* pset == the sets mset U r with U measurable and r \in [0,1] *) +(* pprobability == the measurable type generated by pset *) +(* kprobability m == kernel defined by a probability measure *) +(* kdirac mf == kernel defined by a measurable function *) +(* kadd k1 k2 == lifting of the addition of measures to kernels *) +(* mnormalize f == normalization of a kernel to a probability *) +(* l \; k == composition of kernels *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. + +(* PR in progress *) +Lemma emeasurable_itv (R : realType) (i : interval (\bar R)) : + measurable ([set` i]%classic : set \bar R). +Proof. +rewrite -[X in measurable X]setCK; apply: measurableC. +rewrite set_interval.setCitv /=; apply: measurableU => [|]. +- move: i => [[b1 i1|[|]] i2] /=; rewrite ?set_interval.set_itvE//. + exact: emeasurable_itv_ninfty_bnd. +- move: i => [i1 [b2 i2|[|]]] /=; rewrite ?set_interval.set_itvE//. + exact: emeasurable_itv_bnd_pinfty. +Qed. + +Section sfinite_fubini. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +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. +pose s1 := sfinite_measure_seq m1. +pose s2 := sfinite_measure_seq m2. +rewrite [LHS](eq_measure_integral [the measure _ _ of mseries s1 0]); last first. + by move=> A mA _; rewrite /=; exact: sfinite_measure_seqP. +transitivity (\int[mseries s1 0]_x \int[mseries s2 0]_y f (x, y)). + apply: eq_integral => x _; apply: eq_measure_integral => ? ? _. + exact: sfinite_measure_seqP. +transitivity (\sum_(n t _; exact: integral_ge0. + rewrite [X in measurable_fun _ X](_ : _ = + fun x => \sum_(n x. + by rewrite ge0_integral_measure_series//; exact/measurable_fun_prod1. + apply: ge0_emeasurable_fun_sum; first by move=> k x; exact: integral_ge0. + by move=> k; apply: measurable_fun_fubini_tonelli_F. + apply: eq_eseriesr => n _; apply: eq_integral => x _. + by rewrite ge0_integral_measure_series//; exact/measurable_fun_prod1. +transitivity (\sum_(n n _; rewrite integral_nneseries//. + by move=> m; exact: measurable_fun_fubini_tonelli_F. + by move=> m x _; exact: integral_ge0. +transitivity (\sum_(n n _; apply: eq_eseriesr => m _. + by rewrite fubini_tonelli//; exact: finite_measure_sigma_finite. +transitivity (\sum_(n n _; rewrite ge0_integral_measure_series//. + by move=> y _; exact: integral_ge0. + exact: measurable_fun_fubini_tonelli_G. +transitivity (\int[mseries s2 0]_y \sum_(n 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 _. + by rewrite ge0_integral_measure_series//; exact/measurable_fun_prod2. +transitivity (\int[m2]_y \int[mseries s1 0]_x f (x, y)). + by apply: eq_measure_integral => A mA _ /=; rewrite sfinite_measure_seqP. +apply: eq_integral => y _; apply: eq_measure_integral => A mA _ /=. +by rewrite sfinite_measure_seqP. +Qed. + +End sfinite_fubini. +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"). +Reserved Notation "R .-fker X ~> Y" (at level 42, format "R .-fker X ~> Y"). +Reserved Notation "R .-spker X ~> Y" (at level 42, format "R .-spker X ~> Y"). +Reserved Notation "R .-pker X ~> Y" (at level 42, format "R .-pker X ~> Y"). + +HB.mixin Record isKernel d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := + { measurable_kernel : forall U, measurable U -> measurable_fun setT (k ^~ U) }. + +#[short(type=kernel)] +HB.structure Definition Kernel + d d' (X : measurableType d) (Y : measurableType d') (R : realType) := + { k & isKernel _ _ X Y R k }. +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') : + (forall x U, k1 x U = k2 x U) -> k1 = k2. +Proof. +move: k1 k2 => [m1 [[?]]] [m2 [[?]]] /= k12. +have ? : m1 = m2. + by apply/funext => t; apply/eq_measure; apply/funext => U; rewrite k12. +by subst m1; f_equal; f_equal; f_equal; apply/Prop_irrelevance. +Qed. + +Section kseries. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variable k : (R.-ker X ~> Y)^nat. + +Definition kseries : X -> {measure set Y -> \bar R} := + fun x => [the measure _ _ of mseries (k ^~ x) 0]. + +Lemma measurable_fun_kseries (U : set Y) : + measurable U -> + measurable_fun setT (kseries ^~ U). +Proof. +move=> mU. +by apply: ge0_emeasurable_fun_sum => // n; exact/measurable_kernel. +Qed. + +HB.instance Definition _ := + isKernel.Build _ _ _ _ _ kseries measurable_fun_kseries. + +End kseries. + +Lemma integral_kseries d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : (R.-ker X ~> Y)^nat) (f : Y -> \bar R) x : + (forall y, 0 <= f y) -> + measurable_fun setT f -> + \int[kseries k x]_y (f y) = \sum_(i f0 mf; rewrite /kseries/= ge0_integral_measure_series. +Qed. + +Section measure_fam_uub. +Context d d' (X : measurableType d) (Y : measurableType d') (R : numFieldType). +Variable k : X -> {measure set Y -> \bar R}. + +Definition measure_fam_uub := exists r, forall x, k x [set: Y] < r%:E. + +Lemma measure_fam_uubP : measure_fam_uub <-> + exists r : {posnum R}, forall x, k x [set: Y] < r%:num%:E. +Proof. +split => [|] [r kr]; last by exists r%:num. +suff r_gt0 : (0 < r)%R by exists (PosNum r_gt0). +by rewrite -lte_fin; apply: (le_lt_trans _ (kr point)). +Qed. + +End measure_fam_uub. + +HB.mixin Record Kernel_isSFinite_subdef + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := { + sfinite_subdef : exists2 s : (R.-ker X ~> Y)^nat, + forall n, measure_fam_uub (s n) & + forall x U, measurable U -> k x U = kseries s x U }. + +#[short(type=sfinite_kernel)] +HB.structure Definition SFiniteKernel + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) := + {k of @Kernel _ _ _ _ R k & Kernel_isSFinite_subdef _ _ X Y R k }. +Notation "R .-sfker X ~> Y" := (sfinite_kernel X Y R). + +Arguments sfinite_subdef {_ _ _ _ _} _. + +Lemma eq_sfkernel d d' (T : measurableType d) (T' : measurableType d') (R : realType) + (k1 k2 : R.-sfker T ~> T') : + (forall x U, k1 x U = k2 x U) -> k1 = k2. +Proof. +move: k1 k2 => [m1 [[?] [?]]] [m2 [[?] [?]]] /= k12. +have ? : m1 = m2. + by apply/funext => t; apply/eq_measure; apply/funext => U; rewrite k12. +by subst m1; f_equal; f_equal; f_equal; apply/Prop_irrelevance. +Qed. + +HB.mixin Record SFiniteKernel_isFinite + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := + { measure_uub : measure_fam_uub k }. + +#[short(type=finite_kernel)] +HB.structure Definition FiniteKernel + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) := + {k of @SFiniteKernel _ _ _ _ _ k & + SFiniteKernel_isFinite _ _ X Y R k }. +Notation "R .-fker X ~> Y" := (finite_kernel X Y R). + +Arguments measure_uub {_ _ _ _ _} _. + +HB.factory Record Kernel_isFinite d d' (X : measurableType d) + (Y : measurableType d') (R : realType) (k : X -> {measure set Y -> \bar R}) + of isKernel _ _ _ _ _ k := { + measure_uub : measure_fam_uub k }. + +Section kzero. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). + +Definition kzero : X -> {measure set Y -> \bar R} := fun _ : X => [the measure _ _ of mzero]. + +Let measurable_fun_kzero U : measurable U -> + measurable_fun setT (kzero ^~ U). +Proof. by move=> ?/=; exact: measurable_fun_cst. Qed. + +HB.instance Definition _ := + @isKernel.Build _ _ X Y R kzero measurable_fun_kzero. + +Lemma kzero_uub : measure_fam_uub kzero. +Proof. by exists 1%R => /= t; rewrite /mzero/=. Qed. + +End kzero. + +HB.builders Context d d' (X : measurableType d) (Y : measurableType d') + (R : realType) k of Kernel_isFinite d d' X Y R k. + +Lemma sfinite_finite : + exists2 k_ : (R.-ker _ ~> _)^nat, forall n, measure_fam_uub (k_ n) & + forall x U, measurable U -> k x U = mseries (k_ ^~ x) 0 U. +Proof. +exists (fun n => if n is O then [the _.-ker _ ~> _ of k] else + [the _.-ker _ ~> _ of @kzero _ _ X Y R]). + by case => [|_]; [exact: measure_uub|exact: kzero_uub]. +move=> t U mU/=; rewrite /mseries. +rewrite (nneseries_split 1%N)// big_ord_recl/= big_ord0 adde0. +rewrite ereal_series (@eq_eseriesr _ _ (fun=> 0%E)); last by case. +by rewrite eseries0// adde0. +Qed. + +HB.instance Definition _ := + @Kernel_isSFinite_subdef.Build d d' X Y R k sfinite_finite. + +HB.instance Definition _ := + @SFiniteKernel_isFinite.Build d d' X Y R k measure_uub. + +HB.end. + +Section sfinite. +Context d d' (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (k : R.-sfker X ~> Y). + +Let s : (X -> {measure set Y -> \bar R})^nat := + let: exist2 x _ _ := cid2 (sfinite_subdef k) in x. + +Let ms n : @isKernel d d' X Y R (s n). +Proof. +split; rewrite /s; case: cid2 => /= s' s'_uub kE. +exact: measurable_kernel. +Qed. + +HB.instance Definition _ n := ms n. + +Let s_uub n : measure_fam_uub (s n). +Proof. by rewrite /s; case: cid2. Qed. + +HB.instance Definition _ n := + @Kernel_isFinite.Build d d' X Y R (s n) (s_uub n). + +Lemma sfinite : exists s : (R.-fker X ~> Y)^nat, + forall x U, measurable U -> k x U = kseries s x U. +Proof. +by exists (fun n => [the _.-fker _ ~> _ of s n]) => x U mU; rewrite /s /= /s; by case: cid2 => ? ? ->. +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 (k z). +Proof. +have [s ks] := sfinite k. +exists (s ^~ z). + move=> n; have [r snr] := measure_uub (s n). + by apply: lty_fin_num_fun; rewrite (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) + (@kzero_uub _ _ X Y R). + +HB.factory Record Kernel_isSFinite d d' (X : measurableType d) + (Y : measurableType d') (R : realType) (k : X -> {measure set Y -> \bar R}) + of isKernel _ _ _ _ _ k := { + sfinite : exists s : (R.-fker X ~> Y)^nat, + forall x U, measurable U -> k x U = kseries s x U }. + +HB.builders Context d d' (X : measurableType d) (Y : measurableType d') + (R : realType) k of Kernel_isSFinite d d' X Y R k. + +Lemma sfinite_subdef : Kernel_isSFinite_subdef d d' X Y R k. +Proof. +split; have [s sE] := sfinite; exists s => //. +by move=> n; exact: measure_uub. +Qed. + +HB.instance Definition _ := (*@isSFinite0.Build d d' X Y R k*) sfinite_subdef. + +HB.end. + +HB.mixin Record FiniteKernel_isSubProbability + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := + { sprob_kernel : ereal_sup [set k x [set: Y] | x in setT] <= 1}. + +#[short(type=sprobability_kernel)] +HB.structure Definition SubProbabilityKernel + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) := + {k of @FiniteKernel _ _ _ _ _ k & + FiniteKernel_isSubProbability _ _ X Y R k }. +Notation "R .-spker X ~> Y" := (sprobability_kernel X Y R). + +HB.factory Record Kernel_isSubProbability + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) of isKernel _ _ X Y R k := + { sprob_kernel : ereal_sup [set k x [set: Y] | x in setT] <= 1}. + +HB.builders Context d d' (X : measurableType d) (Y : measurableType d') + (R : realType) k of Kernel_isSubProbability d d' X Y R k. + +Let finite : @Kernel_isFinite d d' X Y R k. +Proof. +split; exists 2%R => /= ?; rewrite (@le_lt_trans _ _ 1%:E) ?lte_fin ?ltr1n//. +by rewrite (le_trans _ sprob_kernel)//; exact: ereal_sup_ub. +Qed. + +HB.instance Definition _ := finite. + +HB.instance Definition _ := @FiniteKernel_isSubProbability.Build _ _ _ _ _ k sprob_kernel. + +HB.end. + +HB.mixin Record SubProbability_isProbability + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := + { prob_kernel : forall x, k x [set: Y] = 1}. + +#[short(type=probability_kernel)] +HB.structure Definition ProbabilityKernel + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) := + {k of @SubProbabilityKernel _ _ _ _ _ k & + SubProbability_isProbability _ _ X Y R k }. +Notation "R .-pker X ~> Y" := (probability_kernel X Y R). + +HB.factory Record Kernel_isProbability + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) of isKernel _ _ X Y R k := + { prob_kernel : forall x, k x setT = 1 }. + +HB.builders Context d d' (X : measurableType d) (Y : measurableType d') + (R : realType) k of Kernel_isProbability d d' X Y R k. + +Let sprob_kernel : @Kernel_isSubProbability d d' X Y R k. +Proof. +by split; apply: ub_ereal_sup => x [y _ <-{x}]; rewrite prob_kernel. +Qed. + +HB.instance Definition _ := sprob_kernel. + +HB.instance Definition _ := @SubProbability_isProbability.Build _ _ _ _ _ k prob_kernel. + +HB.end. + +Lemma finite_kernel_measure d d' (X : measurableType d) + (Y : measurableType d') (R : realType) (k : R.-fker X ~> Y) (x : X) : + fin_num_fun (k x). +Proof. +have [r k_r] := measure_uub k. +by apply: lty_fin_num_fun; rewrite (@lt_trans _ _ r%:E) ?ltey. +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 + measurability of each measure of the family) + - as a consequence, m2D_bounded holds for all x *) +Section measurable_prod_subset_kernel. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Implicit Types A : set (X * Y). + +Section xsection_kernel. +Variable (k : R.-ker X ~> Y) (D : set Y) (mD : measurable D). +Let kD x := mrestr (k x) mD. +HB.instance Definition _ x := Measure.on (kD x). +Let phi A := fun x => kD x (xsection A x). +Let XY := [set A | measurable A /\ measurable_fun setT (phi A)]. + +Let phiM (A : set X) B : phi (A `*` B) = (fun x => kD x B * (\1_A x)%:E). +Proof. +rewrite funeqE => x; rewrite indicE /phi/=. +have [xA|xA] := boolP (x \in A); first by rewrite mule1 in_xsectionM. +by rewrite mule0 notin_xsectionM// set0I measure0. +Qed. + +Lemma measurable_prod_subset_xsection_kernel : + (forall x, exists M, forall X, measurable X -> kD x X < M%:E) -> + measurable `<=` XY. +Proof. +move=> kD_ub; rewrite measurable_prod_measurableType. +set C := [set A `*` B | A in measurable & B in measurable]. +have CI : setI_closed C. + move=> _ _ [X1 mX1 [X2 mX2 <-]] [Y1 mY1 [Y2 mY2 <-]]. + exists (X1 `&` Y1); first exact: measurableI. + by exists (X2 `&` Y2); [exact: measurableI|rewrite setMI]. +have CT : C setT by exists setT => //; exists setT => //; rewrite setMTT. +have CXY : C `<=` XY. + move=> _ [A mA [B mB <-]]; split; first exact: measurableM. + rewrite phiM. + apply: emeasurable_funM => //; first exact/measurable_kernel/measurableI. + by apply/EFin_measurable_fun; rewrite (_ : \1_ _ = mindic R mA). +suff monoB : monotone_class setT XY by exact: monotone_class_subset. +split => //; [exact: CXY| |exact: xsection_ndseq_closed]. +move=> A B BA [mA mphiA] [mB mphiB]; split; first exact: measurableD. +suff : phi (A `\` B) = (fun x => phi A x - phi B x). + by move=> ->; exact: emeasurable_funB. +rewrite funeqE => x; rewrite /phi/= xsectionD// measureD. +- by rewrite setIidr//; exact: le_xsection. +- exact: measurable_xsection. +- exact: measurable_xsection. +- have [M kM] := kD_ub x. + rewrite (lt_le_trans (kM (xsection A x) _)) ?leey//. + exact: measurable_xsection. +Qed. + +End xsection_kernel. + +End measurable_prod_subset_kernel. + +(* see measurable_fun_xsection in lebesgue_integral.v + the difference is that this section uses a finite kernel m2 + instead of a sigma-finite measure m2 *) +Section measurable_fun_xsection_finite_kernel. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variable k : R.-fker X ~> Y. +Implicit Types A : set (X * Y). + +Let phi A := fun x => k x (xsection A x). +Let XY := [set A | measurable A /\ measurable_fun setT (phi A)]. + +Lemma measurable_fun_xsection_finite_kernel A : + A \in measurable -> measurable_fun setT (phi A). +Proof. +move: A; suff : measurable `<=` XY by move=> + A; rewrite inE => /[apply] -[]. +move=> /= A mA; rewrite /XY/=; split => //; rewrite (_ : phi _ = + (fun x => mrestr (k x) measurableT (xsection A x))); last first. + by apply/funext => x//=; rewrite /mrestr setIT. +apply measurable_prod_subset_xsection_kernel => // x. +have [r hr] := measure_uub k; exists r => B mB. +by rewrite (le_lt_trans _ (hr x)) // /mrestr /= setIT le_measure// inE. +Qed. + +End measurable_fun_xsection_finite_kernel. + +Section measurable_fun_integral_finite_sfinite. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variable k : X * Y -> \bar R. + +Lemma measurable_fun_xsection_integral + (l : X -> {measure set Y -> \bar R}) + (k_ : ({nnsfun [the measurableType _ of (X * Y)%type] >-> R})^nat) + (ndk_ : nondecreasing_seq (k_ : (X * Y -> R)^nat)) + (k_k : forall z, EFin \o (k_ ^~ z) --> k z) : + (forall n r, measurable_fun setT (fun x => l x (xsection (k_ n @^-1` [set r]) x))) -> + measurable_fun setT (fun x => \int[l x]_y k (x, y)). +Proof. +move=> h. +rewrite (_ : (fun x => _) = + (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_lim_esupE//. + apply: ereal_nondecreasing_is_cvg => m n mn. + apply: ge0_le_integral => //. + - by move=> y _; rewrite lee_fin. + - exact/EFin_measurable_fun/measurable_fun_prod1. + - by move=> y _; rewrite lee_fin. + - exact/EFin_measurable_fun/measurable_fun_prod1. + - by move=> y _; rewrite lee_fin; exact/lefP/ndk_. + rewrite -monotone_convergence//. + - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: k_k. + - by move=> n; exact/EFin_measurable_fun/measurable_fun_prod1. + - by move=> n y _; rewrite lee_fin. + - by move=> y _ m n mn; rewrite lee_fin; exact/lefP/ndk_. +apply: measurable_fun_lim_esup => n. +rewrite [X in measurable_fun _ X](_ : _ = (fun x => \int[l x]_y + (\sum_(r \in range (k_ n)) + r * \1_(k_ n @^-1` [set r]) (x, y))%:E)); last first. + by apply/funext => x; apply: eq_integral => y _; rewrite fimfunE. +rewrite [X in measurable_fun _ X](_ : _ = (fun x => \sum_(r \in range (k_ n)) + (\int[l x]_y (r * \1_(k_ n @^-1` [set r]) (x, y))%:E))); last first. + apply/funext => x; rewrite -ge0_integral_fsum//. + - by apply: eq_integral => y _; rewrite -fsumEFin. + - move=> r. + apply/EFin_measurable_fun/measurable_funrM/measurable_fun_prod1 => /=. + rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) (measurable_set1 r)))//. + exact/measurable_funP. + - by move=> m y _; rewrite nnfun_muleindic_ge0. +apply: emeasurable_fun_fsum => // r. +rewrite [X in measurable_fun _ X](_ : _ = (fun x => r%:E * + \int[l x]_y (\1_(k_ n @^-1` [set r]) (x, y))%:E)); last first. + apply/funext => x; under eq_integral do rewrite EFinM. + have [r0|r0] := leP 0%R r. + rewrite ge0_integralM//; last by move=> y _; rewrite lee_fin. + apply/EFin_measurable_fun/measurable_fun_prod1 => /=. + rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) (measurable_set1 r)))//. + exact/measurable_funP. + rewrite integral0_eq; last first. + by move=> y _; rewrite preimage_nnfun0// indic0 mule0. + by rewrite integral0_eq ?mule0// => y _; rewrite preimage_nnfun0// indic0. +apply/measurable_funeM. +rewrite (_ : (fun x => _) = (fun x => l x (xsection (k_ n @^-1` [set r]) x))). + exact/h. +apply/funext => x; rewrite integral_indic//; last first. + rewrite (_ : (fun x => _) = xsection (k_ n @^-1` [set r]) x). + exact: measurable_xsection. + by rewrite /xsection; apply/seteqP; split=> y/= /[!inE]. +congr (l x _); apply/funext => y1/=; rewrite /xsection/= inE. +by apply/propext; tauto. +Qed. + +Lemma measurable_fun_integral_finite_kernel (l : R.-fker X ~> Y) + (k0 : forall z, 0 <= k z) (mk : measurable_fun setT k) : + measurable_fun setT (fun x => \int[l x]_y k (x, y)). +Proof. +have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x). +apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r. +have [l_ hl_] := measure_uub l. +by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. +Qed. + +Lemma measurable_fun_integral_sfinite_kernel (l : R.-sfker X ~> Y) + (k0 : forall t, 0 <= k t) (mk : measurable_fun setT k) : + measurable_fun setT (fun x => \int[l x]_y k (x, y)). +Proof. +have [k_ [ndk_ k_k]] := approximation measurableT mk (fun xy _ => k0 xy). +apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r. +have [l_ hl_] := sfinite l. +rewrite (_ : (fun x => _) = + (fun x => mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first. + by apply/funext => x; rewrite hl_//; exact/measurable_xsection. +apply: ge0_emeasurable_fun_sum => // m. +by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. +Qed. + +End measurable_fun_integral_finite_sfinite. +Arguments measurable_fun_xsection_integral {_ _ _ _ _} k l. +Arguments measurable_fun_integral_finite_kernel {_ _ _ _ _} k l. +Arguments measurable_fun_integral_sfinite_kernel {_ _ _ _ _} k l. + +Section kdirac. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variable f : X -> Y. + +Definition kdirac (mf : measurable_fun setT f) + : X -> {measure set Y -> \bar R} := + fun x => [the measure _ _ of dirac (f x)]. + +Hypothesis mf : measurable_fun setT f. + +Let measurable_fun_kdirac U : measurable U -> + measurable_fun setT (kdirac mf ^~ U). +Proof. +move=> mU; apply/EFin_measurable_fun. +by rewrite (_ : (fun x => _) = mindic R mU \o f)//; exact/measurable_funT_comp. +Qed. + +HB.instance Definition _ := isKernel.Build _ _ _ _ _ (kdirac mf) + measurable_fun_kdirac. + +Let kdirac_prob x : kdirac mf x setT = 1. +Proof. by rewrite /kdirac/= diracT. Qed. + +HB.instance Definition _ := Kernel_isProbability.Build _ _ _ _ _ + (kdirac mf) kdirac_prob. + +End kdirac. +Arguments kdirac {d d' X Y R f}. + +Section dist_salgebra_instance. +Context d (T : measurableType d) (R : realType). + +Let p0 : probability T R := [the probability _ _ of dirac point]. + +Definition prob_pointed := Pointed.Class + (Choice.Class gen_eqMixin (Choice.Class gen_eqMixin gen_choiceMixin)) p0. + +Canonical probability_eqType := EqType (probability T R) prob_pointed. +Canonical probability_choiceType := ChoiceType (probability T R) prob_pointed. +Canonical probability_ptType := PointedType (probability T R) prob_pointed. + +Definition mset (U : set T) (r : R) := [set mu : probability T R | mu U < r%:E]. + +Lemma lt0_mset (U : set T) (r : R) : (r < 0)%R -> mset U r = set0. +Proof. +move=> r0; apply/seteqP; split => // x/=. +by apply/negP; rewrite -leNgt (@le_trans _ _ 0)// lee_fin ltW. +Qed. + +Lemma gt1_mset (U : set T) (r : R) : measurable U -> (1 < r)%R -> mset U r = setT. +Proof. +move=> mU r1; apply/seteqP; split => // x/= _. +by rewrite /mset/= (le_lt_trans (probability_le1 _ _)). +Qed. + +Definition pset : set (set (probability T R)) := + [set mset U r | r in `[0%R,1%R] & U in measurable]. + +Definition pprobability : measurableType pset.-sigma := + [the measurableType _ of salgebraType pset]. + +End dist_salgebra_instance. + +Section kprobability. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variable P : X -> pprobability Y R. + +Definition kprobability (mP : measurable_fun setT P) + : X -> {measure set Y -> \bar R} := P. + +Hypothesis mP : measurable_fun setT P. + +Let measurable_fun_kprobability U : measurable U -> + measurable_fun setT (kprobability mP ^~ U). +Proof. +move=> mU. +apply: (measurability (ErealGenInftyO.measurableE R)) => _ /= -[_ [r ->] <-]. +rewrite setTI preimage_itv_infty_o -/(P @^-1` mset U r). +have [r0|r0] := leP 0%R r; last by rewrite lt0_mset// preimage_set0. +have [r1|r1] := leP r 1%R; last by rewrite gt1_mset// preimage_setT. +move: mP => /(_ measurableT (mset U r)); rewrite setTI; apply. +by apply: sub_sigma_algebra; exists r => /=; [rewrite in_itv/= r0|exists U]. +Qed. + +HB.instance Definition _ := + @isKernel.Build _ _ X Y R (kprobability mP) measurable_fun_kprobability. + +Let kprobability_prob x : kprobability mP x setT = 1. +Proof. by rewrite /kprobability/= probability_setT. Qed. + +HB.instance Definition _ := + @Kernel_isProbability.Build _ _ X Y R (kprobability mP) kprobability_prob. + +End kprobability. + +Section kadd. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variables k1 k2 : R.-ker X ~> Y. + +Definition kadd : X -> {measure set Y -> \bar R} := + fun x => [the measure _ _ of measure_add (k1 x) (k2 x)]. + +Let measurable_fun_kadd U : measurable U -> + measurable_fun setT (kadd ^~ U). +Proof. +move=> mU; rewrite /kadd. +rewrite (_ : (fun _ => _) = (fun x => k1 x U + k2 x U)); last first. + by apply/funext => x; rewrite -measure_addE. +by apply: emeasurable_funD; exact/measurable_kernel. +Qed. + +HB.instance Definition _ := + @isKernel.Build _ _ _ _ _ kadd measurable_fun_kadd. +End kadd. + +Section sfkadd. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variables k1 k2 : R.-sfker X ~> Y. + +Let sfinite_kadd : exists2 k_ : (R.-ker _ ~> _)^nat, forall n, measure_fam_uub (k_ n) & + forall x U, measurable U -> + kadd k1 k2 x U = mseries (k_ ^~ x) 0 U. +Proof. +have [f1 hk1] := sfinite k1; have [f2 hk2] := sfinite k2. +exists (fun n => [the _.-ker _ ~> _ of kadd (f1 n) (f2 n)]). + move=> n. + have [r1 f1r1] := measure_uub (f1 n). + have [r2 f2r2] := measure_uub (f2 n). + exists (r1 + r2)%R => x/=. + by rewrite /msum !big_ord_recr/= big_ord0 add0e EFinD lte_add. +move=> x U mU. +rewrite /kadd/= -/(measure_add (k1 x) (k2 x)) measure_addE hk1//= hk2//=. +rewrite /mseries -nneseriesD//; apply: eq_eseriesr => n _ /=. +by rewrite -/(measure_add (f1 n x) (f2 n x)) measure_addE. +Qed. + +HB.instance Definition _ t := + Kernel_isSFinite_subdef.Build _ _ _ _ R (kadd k1 k2) sfinite_kadd. +End sfkadd. + +Section fkadd. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variables k1 k2 : R.-fker X ~> Y. + +Let kadd_finite_uub : measure_fam_uub (kadd k1 k2). +Proof. +have [f1 hk1] := measure_uub k1; have [f2 hk2] := measure_uub k2. +exists (f1 + f2)%R => x; rewrite /kadd /=. +rewrite -/(measure_add (k1 x) (k2 x)). +by rewrite measure_addE EFinD; exact: lte_add. +Qed. + +HB.instance Definition _ t := + Kernel_isFinite.Build _ _ _ _ R (kadd k1 k2) kadd_finite_uub. +End fkadd. + +(* TODO: move *) +Section kernel_measurable_preimage. +Context d d' (T : measurableType d) (T' : measurableType d') (R : realType). + +Lemma measurable_eq_cst (f : R.-ker T ~> T') k : + measurable [set t | f t setT == k]. +Proof. +rewrite [X in measurable X](_ : _ = (f ^~ setT) @^-1` [set k]); last first. + by apply/seteqP; split => t/= /eqP. +have /(_ measurableT [set k]) := measurable_kernel f setT measurableT. +by rewrite setTI; exact. +Qed. + +Lemma measurable_neq_cst (f : R.-ker T ~> T') k : + measurable [set t | f t setT != k]. +Proof. +rewrite [X in measurable X](_ : _ = (f ^~ setT) @^-1` [set~ k]); last first. + by apply/seteqP; split => t /eqP. +have /(_ measurableT [set~ k]) := measurable_kernel f setT measurableT. +by rewrite setTI; apply => //; exact: measurableC. +Qed. + +End kernel_measurable_preimage. + +(* TODO: move *) +Lemma measurable_fun_eq_cst d d' (T : measurableType d) + (T' : measurableType d') (R : realType) (f : R.-ker T ~> T') k : + measurable_fun setT (fun t => f t setT == k). +Proof. +move=> _ /= B mB; rewrite setTI. +have [/eqP->|/eqP->|/eqP->|/eqP->] := set_bool B. +- exact: measurable_eq_cst. +- rewrite (_ : _ @^-1` _ = [set b | f b setT != k]); last first. + by apply/seteqP; split => [t /negbT//|t /negbTE]. + exact: measurable_neq_cst. +- by rewrite preimage_set0. +- by rewrite preimage_setT. +Qed. + +Section mnormalize. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variables (f : X -> {measure set Y -> \bar R}) (P : probability Y R). + +Definition mnormalize x := + let evidence := f x [set: Y] in + if (evidence == 0) || (evidence == +oo) then fun U => P U + else fun U => f x U * (fine evidence)^-1%:E. + +Let mnormalize0 x : mnormalize x set0 = 0. +Proof. +by rewrite /mnormalize; case: ifPn => // _; rewrite measure0 mul0e. +Qed. + +Let mnormalize_ge0 x U : 0 <= mnormalize x U. +Proof. by rewrite /mnormalize; case: ifPn => //; case: ifPn. Qed. + +Let mnormalize_sigma_additive x : semi_sigma_additive (mnormalize x). +Proof. +move=> F mF tF mUF; rewrite /mnormalize/=. +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: cvgeMr => //; exact: measure_semi_sigma_additive. +Qed. + +HB.instance Definition _ x := isMeasure.Build _ _ _ (mnormalize x) + (mnormalize0 x) (mnormalize_ge0 x) (@mnormalize_sigma_additive x). + +Let mnormalize1 x : mnormalize x setT = 1. +Proof. +rewrite /mnormalize; case: ifPn; first by rewrite probability_setT. +rewrite negb_or => /andP[ft0 ftoo]. +have ? : f x setT \is a fin_num. + by rewrite ge0_fin_numE// lt_neqAle ftoo/= leey. +by rewrite -{1}(@fineK _ (f x setT))// -EFinM divrr// ?unitfE fine_eq0. +Qed. + +HB.instance Definition _ x := + Measure_isProbability.Build _ _ _ (mnormalize x) (mnormalize1 x). + +End mnormalize. + +Section knormalize. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variable f : R.-ker X ~> Y. + +Definition knormalize (P : probability Y R) : X -> {measure set Y -> \bar R} := + fun x => [the measure _ _ of mnormalize f P x]. + +Variable P : probability Y R. + +Let measurable_fun_knormalize U : + measurable U -> measurable_fun setT (knormalize P ^~ U). +Proof. +move=> mU; rewrite /knormalize/= /mnormalize /=. +rewrite (_ : (fun _ => _) = (fun x => + if f x setT == 0 then P U else if f x setT == +oo then P U + else f x U * (fine (f x setT))^-1%:E)); last first. + apply/funext => x; case: ifPn => [/orP[->//|->]|]; first by case: ifPn. + by rewrite negb_or=> /andP[/negbTE -> /negbTE ->]. +apply: measurable_fun_if => //; + [exact: measurable_fun_eq_cst|exact: measurable_fun_cst|]. +apply: measurable_fun_if => //. +- rewrite setTI [X in measurable X](_ : _ = [set t | f t setT != 0]). + exact: measurable_neq_cst. + by apply/seteqP; split => [x /negbT//|x /negbTE]. +- by apply: (@measurable_funS _ _ _ _ setT) => //; exact: measurable_fun_eq_cst. +- exact: measurable_fun_cst. +- apply: emeasurable_funM. + by have := measurable_kernel f U mU; exact: measurable_funS. + apply/EFin_measurable_fun. + apply: (@measurable_fun_comp _ _ _ _ _ _ [set r : R | r != 0%R]) => //. + + exact: open_measurable. + + move=> /= r [t] [] [_ ft0] ftoo ftr; apply/eqP => r0. + move: (ftr); rewrite r0 => /eqP; rewrite fine_eq0 ?ft0//. + by rewrite ge0_fin_numE// lt_neqAle leey ftoo. + + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0. + exact: inv_continuous. + + apply: measurable_funT_comp => /=; first exact: measurable_fun_fine. + by have := measurable_kernel f _ measurableT; exact: measurable_funS. +Qed. + +HB.instance Definition _ := isKernel.Build _ _ _ _ R (knormalize P) + measurable_fun_knormalize. + +Let knormalize1 x : knormalize P x setT = 1. +Proof. +rewrite /knormalize/= /mnormalize. +case: ifPn => [_|]; first by rewrite probability_setT. +rewrite negb_or => /andP[fx0 fxoo]. +have ? : f x setT \is a fin_num by rewrite ge0_fin_numE// lt_neqAle fxoo/= leey. +rewrite -{1}(@fineK _ (f x setT))//=. +by rewrite -EFinM divrr// ?lte_fin ?ltr1n// ?unitfE fine_eq0. +Qed. + +HB.instance Definition _ := + @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) knormalize1. + +End knormalize. + +Section kcomp_def. +Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2) + (Z : measurableType d3) (R : realType). +Variable l : X -> {measure set Y -> \bar R}. +Variable k : (X * Y)%type -> {measure set Z -> \bar R}. + +Definition kcomp x U := \int[l x]_y k (x, y) U. + +End kcomp_def. + +Section kcomp_is_measure. +Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2) + (Z : measurableType d3) (R : realType). +Variable l : R.-ker X ~> Y. +Variable k : R.-ker [the measurableType _ of (X * Y)%type] ~> Z. + +Local Notation "l \; k" := (kcomp l k). + +Let kcomp0 x : (l \; k) x set0 = 0. +Proof. +by rewrite /kcomp (eq_integral (cst 0)) ?integral0// => y _; rewrite measure0. +Qed. + +Let kcomp_ge0 x U : 0 <= (l \; k) x U. Proof. exact: integral_ge0. Qed. + +Let kcomp_sigma_additive x : semi_sigma_additive ((l \; k) x). +Proof. +move=> U mU tU mUU; rewrite [X in _ --> X](_ : _ = + \int[l x]_y (\sum_(n V _. + by apply/esym/cvg_lim => //; exact/measure_semi_sigma_additive. +apply/cvg_closeP; split. + by apply: is_cvg_nneseries => n _; exact: integral_ge0. +rewrite closeE// integral_nneseries// => n. +by have /measurable_fun_prod1 := measurable_kernel k _ (mU n). +Qed. + +HB.instance Definition _ x := isMeasure.Build _ R _ + ((l \; k) x) (kcomp0 x) (kcomp_ge0 x) (@kcomp_sigma_additive x). + +Definition mkcomp : X -> {measure set Z -> \bar R} := fun x => [the measure _ _ of (l \; k) x]. + +End kcomp_is_measure. + +Notation "l \; k" := (mkcomp l k) : ereal_scope. + +Module KCOMP_FINITE_KERNEL. + +Section kcomp_finite_kernel_kernel. +Context d d' d3 (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType) (l : R.-fker X ~> Y) + (k : R.-ker [the measurableType _ of (X * Y)%type] ~> Z). + +Lemma measurable_fun_kcomp_finite U : + measurable U -> measurable_fun setT ((l \; k) ^~ U). +Proof. +move=> mU; apply: (measurable_fun_integral_finite_kernel (k ^~ U)) => //=. +exact/measurable_kernel. +Qed. + +HB.instance Definition _ := + isKernel.Build _ _ X Z R (l \; k) measurable_fun_kcomp_finite. + +End kcomp_finite_kernel_kernel. + +Section kcomp_finite_kernel_finite. +Context d d' d3 (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). +Variable l : R.-fker X ~> Y. +Variable k : R.-fker [the measurableType _ of (X * Y)%type] ~> Z. + +Let mkcomp_finite : measure_fam_uub (l \; k). +Proof. +have /measure_fam_uubP[r hr] := measure_uub k. +have /measure_fam_uubP[s hs] := measure_uub l. +apply/measure_fam_uubP; exists (PosNum [gt0 of (r%:num * s%:num)%R]) => x /=. +apply: (@le_lt_trans _ _ (\int[l x]__ r%:num%:E)). + apply: ge0_le_integral => //. + - have /measurable_fun_prod1 := measurable_kernel k _ measurableT. + exact. + - exact/measurable_fun_cst. + - by move=> y _; exact/ltW/hr. +by rewrite integral_cst//= EFinM lte_pmul2l. +Qed. + +HB.instance Definition _ := + Kernel_isFinite.Build _ _ X Z R (l \; k) mkcomp_finite. + +End kcomp_finite_kernel_finite. +End KCOMP_FINITE_KERNEL. + +Section kcomp_sfinite_kernel. +Context d d' d3 (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). +Variable l : R.-sfker X ~> Y. +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. +Proof. +have [k_ hk_] := sfinite k; have [l_ hl_] := sfinite l. +have [kl hkl] : exists kl : (R.-fker X ~> Z) ^nat, forall x U, + \esum_(i in setT) (l_ i.2 \; k_ i.1) x U = \sum_(i [the _.-fker _ ~> _ of l_ (f i).2 \; k_ (f i).1]) => x U. + by rewrite (reindex_esum [set: nat] _ f)// nneseries_esum// fun_true. +exists kl => x U mU. +transitivity (([the _.-ker _ ~> _ of kseries l_] \; [the _.-ker _ ~> _ of kseries k_]) x U). + rewrite /= /kcomp [in RHS](eq_measure_integral (l x)); last first. + by move=> *; rewrite hl_. + by apply: eq_integral => y _; rewrite hk_. +rewrite /= /kcomp/= integral_nneseries//=; last first. + by move=> n; have /measurable_fun_prod1 := measurable_kernel (k_ n) _ mU; exact. +transitivity (\sum_(i i _; rewrite integral_kseries//. + by have /measurable_fun_prod1 := measurable_kernel (k_ i) _ mU; exact. +rewrite /mseries -hkl/=. +rewrite (_ : setT = setT `*`` (fun=> setT)); last by apply/seteqP; split. +rewrite -(@esum_esum _ _ _ _ _ (fun i j => (l_ j \; k_ i) x U))//. +rewrite nneseries_esum; last by move=> n _; exact: nneseries_ge0. +by rewrite fun_true; apply: eq_esum => /= i _; rewrite nneseries_esum// fun_true. +Qed. + +Lemma measurable_fun_mkcomp_sfinite U : measurable U -> + measurable_fun setT ((l \; k) ^~ U). +Proof. +move=> mU; apply: (measurable_fun_integral_sfinite_kernel (k ^~ U)) => //. +exact/measurable_kernel. +Qed. + +End kcomp_sfinite_kernel. + +Module KCOMP_SFINITE_KERNEL. +Section kcomp_sfinite_kernel. +Context d d' d3 (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). +Variable l : R.-sfker X ~> Y. +Variable k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z. + +HB.instance Definition _ := + isKernel.Build _ _ X Z R (l \; k) (measurable_fun_mkcomp_sfinite l k). + +#[export] +HB.instance Definition _ := + Kernel_isSFinite.Build _ _ X Z R (l \; k) (mkcomp_sfinite l k). + +End kcomp_sfinite_kernel. +End KCOMP_SFINITE_KERNEL. +HB.export KCOMP_SFINITE_KERNEL. + +Section measurable_fun_preimage_integral. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variables (k : Y -> \bar R) + (k_ : ({nnsfun Y >-> R}) ^nat) + (ndk_ : nondecreasing_seq (k_ : (Y -> R)^nat)) + (k_k : forall z, setT z -> EFin \o (k_ ^~ z) --> k z). + +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). + +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). + +Let fk_2 n : finite_set (range (k_2 n)). +Proof. +have := @fimfunP _ _ (k_ n). +suff : range (k_ n) = range (k_2 n) by move=> <-. +by apply/seteqP; split => r [y ?] <-; [exists (point, y)|exists y.2]. +Qed. + +HB.instance Definition _ n := @FiniteImage.Build _ _ _ (fk_2 n). + +Lemma measurable_fun_preimage_integral (l : X -> {measure set Y -> \bar R}) : + (forall n r, measurable_fun setT (l ^~ (k_ n @^-1` [set r]))) -> + measurable_fun setT (fun x => \int[l x]_z k z). +Proof. +move=> h; apply: (measurable_fun_xsection_integral (k \o snd) l + (fun n => [the {nnsfun _ >-> _} of k_2 n])) => /=. +- by rewrite /k_2 => m n mn; apply/lefP => -[x y] /=; exact/lefP/ndk_. +- by move=> [x y]; exact: k_k. +- move=> n r _ /= B mB. + 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 (comp_preimage _ snd (k_ n)) xsection_preimage_snd. +Qed. + +End measurable_fun_preimage_integral. + +Lemma measurable_fun_integral_kernel + d d' (X : measurableType d) (Y : measurableType d') (R : realType) + (l : X -> {measure set Y -> \bar R}) + (ml : forall U, measurable U -> measurable_fun setT (l ^~ U)) + (* NB: l is really just a kernel *) + (k : Y -> \bar R) (k0 : forall z, 0 <= k z) (mk : measurable_fun setT k) : + measurable_fun setT (fun x => \int[l x]_y k y). +Proof. +have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x). +by apply: (measurable_fun_preimage_integral ndk_ k_k) => n r; exact/ml. +Qed. + +Section integral_kcomp. +Context d d2 d3 (X : measurableType d) (Y : measurableType d2) + (Z : measurableType d3) (R : realType). +Variables (l : R.-sfker X ~> Y) (k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z). + +Let integral_kcomp_indic x E (mE : measurable E) : + \int[(l \; k) x]_z (\1_E z)%:E = \int[l x]_y (\int[k (x, y)]_z (\1_E z)%:E). +Proof. +rewrite integral_indic//= /kcomp. +by apply: eq_integral => y _; rewrite integral_indic. +Qed. + +Let integral_kcomp_nnsfun x (f : {nnsfun Z >-> R}) : + \int[(l \; k) x]_z (f z)%:E = \int[l x]_y (\int[k (x, y)]_z (f z)%:E). +Proof. +under [in LHS]eq_integral do rewrite fimfunE -fsumEFin//. +rewrite ge0_integral_fsum//; last 2 first. + - move=> r; apply/EFin_measurable_fun/measurable_funrM. + have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP. + by rewrite (_ : \1__ = mindic R fr). + - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0. +under [in RHS]eq_integral. + move=> y _. + under eq_integral. + by move=> z _; rewrite fimfunE -fsumEFin//; over. + rewrite /= ge0_integral_fsum//; last 2 first. + - move=> r; apply/EFin_measurable_fun/measurable_funrM. + have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP. + by rewrite (_ : \1__ = mindic R fr). + - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0. + under eq_fsbigr. + move=> r _. + rewrite (integralM_indic _ (fun r => f @^-1` [set r]))//; last first. + by move=> r0; rewrite preimage_nnfun0. + rewrite integral_indic// setIT. + over. + over. +rewrite /= ge0_integral_fsum//; last 2 first. + - move=> r; apply: measurable_funeM. + have := measurable_kernel k (f @^-1` [set r]) (measurable_sfunP f (measurable_set1 r)). + by move=> /measurable_fun_prod1; exact. + - move=> n y _. + have := mulemu_ge0 (fun n => f @^-1` [set n]). + by apply; exact: preimage_nnfun0. +apply: eq_fsbigr => r _. +rewrite (integralM_indic _ (fun r => f @^-1` [set r]))//; last first. + exact: preimage_nnfun0. +rewrite /= integral_kcomp_indic; last exact/measurable_sfunP. +have [r0|r0] := leP 0%R r. + rewrite ge0_integralM//; last first. + have := measurable_kernel k (f @^-1` [set r]) (measurable_sfunP f (measurable_set1 r)). + by move/measurable_fun_prod1; exact. + by congr (_ * _); apply: eq_integral => y _; rewrite integral_indic// setIT. +rewrite integral0_eq ?mule0; last first. + by move=> y _; rewrite integral0_eq// => z _; rewrite preimage_nnfun0// indic0. +by rewrite integral0_eq// => y _; rewrite preimage_nnfun0// measure0 mule0. +Qed. + +Lemma integral_kcomp x f : (forall z, 0 <= f z) -> measurable_fun setT f -> + \int[(l \; k) x]_z f z = \int[l x]_y (\int[k (x, y)]_z f z). +Proof. +move=> f0 mf. +have [f_ [ndf_ f_f]] := approximation measurableT mf (fun z _ => f0 z). +transitivity (\int[(l \; k) x]_z (lim (EFin \o f_^~ z))). + by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: f_f. +rewrite monotone_convergence//; last 3 first. + by move=> n; exact/EFin_measurable_fun. + by move=> n z _; rewrite lee_fin. + by move=> z _ a b /ndf_ /lefP ab; rewrite lee_fin. +rewrite (_ : (fun _ => _) = + (fun n => \int[l x]_y (\int[k (x, y)]_z (f_ n z)%:E)))//; last first. + by apply/funext => n; rewrite integral_kcomp_nnsfun. +transitivity (\int[l x]_y lim (fun n => \int[k (x, y)]_z (f_ n z)%:E)). + rewrite -monotone_convergence//; last 3 first. + - move=> n; apply: measurable_fun_integral_kernel => //. + + move=> U mU; have := measurable_kernel k _ mU. + by move=> /measurable_fun_prod1; exact. + + by move=> z; rewrite lee_fin. + + exact/EFin_measurable_fun. + - by move=> n y _; apply: integral_ge0 => // z _; rewrite lee_fin. + - move=> y _ a b ab; apply: ge0_le_integral => //. + + by move=> z _; rewrite lee_fin. + + exact/EFin_measurable_fun. + + by move=> z _; rewrite lee_fin. + + exact/EFin_measurable_fun. + + by move: ab => /ndf_ /lefP ab z _; rewrite lee_fin. +apply: eq_integral => y _; rewrite -monotone_convergence//; last 3 first. + - by move=> n; exact/EFin_measurable_fun. + - by move=> n z _; rewrite lee_fin. + - by move=> z _ a b /ndf_ /lefP; rewrite lee_fin. +by apply: eq_integral => z _; apply/cvg_lim => //; exact: f_f. +Qed. + +End integral_kcomp. diff --git a/theories/lang_syntax.v b/theories/lang_syntax.v new file mode 100644 index 0000000000..dc04423006 --- /dev/null +++ b/theories/lang_syntax.v @@ -0,0 +1,1318 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +Require Import mathcomp_extra boolp classical_sets signed functions cardinality. +Require Import reals ereal topology normedtype sequences esum measure. +Require Import lebesgue_measure fsbigop numfun lebesgue_integral kernel. +Require Import prob_lang. + +Set Implicit Arguments. +Implicit Types V : Set. +Unset Strict Implicit. +Set Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. + +Require Import String ZArith. +Local Open Scope string. + +Import Notations. + +Declare Scope lang_scope. + +Reserved Notation "l # e -D-> v ; mv" (at level 40). +Reserved Notation "l # e -P-> v" (at level 40). + +Section type_syntax. +Variables (R : realType). + +Section string_eq. + +Definition string_eqMixin := @EqMixin string eqb eqb_spec. +Canonical string_eqType := EqType string string_eqMixin. + +End string_eq. + +Fixpoint prod_meas (l : list {d & measurableType d}) + : {d & measurableType d} := + match l with + | [::] => existT measurableType _ munit + | h :: t => let t' := prod_meas t in + existT _ _ [the measurableType (projT1 h, projT1 t').-prod of (projT2 h * projT2 t')%type] + end. + +Inductive stype := +| sunit : stype +| sbool : stype +| sreal : stype +| spair : stype -> stype -> stype +| sprob : stype -> stype +| slist : list stype -> stype. + +Canonical stype_eqType := Equality.Pack (@gen_eqMixin stype). + +Fixpoint typei (t : stype) : {d & measurableType d} := + match t with + | sunit => existT _ _ munit + | sbool => existT _ _ mbool + | sreal => existT _ _ (mR R) + | spair A B => existT _ _ + [the measurableType (projT1 (typei A), projT1 (typei B)).-prod%mdisp of + (projT2 (typei A) * projT2 (typei B))%type] + | sprob A => existT _ _ (pprobability (projT2 (typei A)) R) + | slist l => prod_meas (map typei l) + end. + +Definition typei2 t := projT2 (typei t). + +End type_syntax. + +Arguments typei {R}. +Arguments typei2 {R}. + +Definition context := seq (string * stype)%type. + +Section expr. +Variables (R : realType). + +Inductive expD : context -> stype -> Type := +| expWD l st x (e : expD l st) : x.1 \notin map fst l -> expD (x :: l) st +| exp_unit l : expD l sunit +| exp_bool l : bool -> expD l sbool +| exp_real l : R -> expD l sreal +| exp_pair l t1 t2 : expD l t1 -> expD l t2 -> expD l (spair t1 t2) +| exp_var (l : context) x t : (* x \in map fst l -> *) + t = nth sunit (map snd l) (seq.index x (map fst l)) -> + expD l t +| exp_bernoulli l (r : {nonneg R}) (r1 : (r%:num <= 1)%R) : expD l (sprob sbool) +| exp_poisson l : nat -> expD l sreal -> expD l sreal +| exp_norm l t : expP l t -> expD l (sprob t) +with expP : context -> stype -> Type := +| expWP l st x (e : expP l st) : x.1 \notin map fst l -> expP (x :: l) st +| exp_if l t : expD l sbool -> expP l t -> expP l t -> expP l t +| exp_letin l t1 t2 (x : string) : + expP l t1 -> expP ((x, t1) :: l) t2 -> expP l t2 +(* | exp_sample : forall t l, expD (sprob t) l -> expP t l *) +| exp_sample_bern l (r : {nonneg R}) (r1 : (r%:num <= 1)%R) : expP l sbool +| exp_score l : expD l sreal -> expP l sunit +| exp_return l t : expD l t -> expP l t. + +End expr. + +Arguments expD {R}. +Arguments expP {R}. +Arguments expWD {R l st x}. +Arguments exp_unit {R l}. +Arguments exp_bool {R l}. +Arguments exp_real {R l}. +Arguments exp_pair {R l _ _}. +Arguments exp_var {R _}. +Arguments exp_bernoulli {R l}. +Arguments exp_poisson {R l}. +Arguments exp_norm {R l _}. +Arguments expWP {R l st x}. +Arguments exp_if {R l t}. +Arguments exp_letin {R l _ _}. +Arguments exp_sample_bern {R} l r. +Arguments exp_score {R l}. +Arguments exp_return {R l _}. + +Declare Custom Entry expr. +Notation "[ e ]" := e (e custom expr at level 5) : lang_scope. +Notation "x ':r'" := (@exp_real _ _ x%R) (in custom expr at level 1) : lang_scope. +Notation "'Ret' x" := (@exp_return _ _ _ x) (in custom expr at level 2) : lang_scope. +Notation "% x" := (@exp_var _ _ x _ erefl) (in custom expr at level 1) : lang_scope. +Notation "%WP x # e" := (@expWP _ _ _ (x, _) e erefl) (in custom expr at level 1) : lang_scope. +Notation "( x , y )" := (exp_pair x y) (in custom expr at level 1) : lang_scope. +Notation "'Let' x '<~' e 'In' f" := (exp_letin x e f) + (in custom expr at level 3, + x constr, + (* e custom expr at level 2, *) + f custom expr at level 3, + left associativity) : lang_scope. +(*Notation "( x )" := x (in custom expr, x at level 50).*) +Notation "'If' e1 'Then' e2 'Else' e3" := (exp_if e1 e2 e3) (in custom expr at level 1) : lang_scope. +Notation "{ x }" := x (in custom expr, x constr) : lang_scope. +Notation "x" := x (in custom expr at level 0, x ident) : lang_scope. + +Section varof. +Context {R : realType}. + +Fixpoint varof (l : seq stype) (i : nat) : + typei2 (slist l) -> @typei2 R (nth sunit l i) := + match + l return (typei2 (slist l) -> typei2 (nth sunit l i)) + with + | [::] => match i with | O => id | j.+1 => id end + | _ :: _ => match i with + | O => fst + | j.+1 => fun H => varof j H.2 + end + end. + +Lemma mvarof (l : seq stype) (i : nat) : measurable_fun setT (@varof l i). +Proof. +elim: l i => //= h t ih [|j]; first exact: measurable_fun_fst. +exact: (measurable_funT_comp (ih _) (@measurable_fun_snd _ _ _ _)). +Qed. +End varof. +Arguments varof {R} l i. +Arguments mvarof {R} l i. + +Section eval. +Variables (R : realType). + +Lemma eq_probability d (Y : measurableType d) (m1 m2 : probability Y R) : + (m1 = m2 :> (set Y -> \bar R)) -> m1 = m2. +Proof. +move: m1 m2 => [m1 +] [m2 +] /= m1m2. +rewrite -{}m1m2 => -[[c11 c12] [m01] [sf1] [sig1] [fin1] [sub1] [p1]] + [[c21 c22] [m02] [sf2] [sig2] [fin2] [sub2] [p2]]. +have ? : c11 = c21 by exact: Prop_irrelevance. +subst c21. +have ? : c12 = c22 by exact: Prop_irrelevance. +subst c22. +have ? : m01 = m02 by exact: Prop_irrelevance. +subst m02. +have ? : sf1 = sf2 by exact: Prop_irrelevance. +subst sf2. +have ? : sig1 = sig2 by exact: Prop_irrelevance. +subst sig2. +have ? : fin1 = fin2 by exact: Prop_irrelevance. +subst fin2. +have ? : sub1 = sub2 by exact: Prop_irrelevance. +subst sub2. +have ? : p1 = p2 by exact: Prop_irrelevance. +subst p2. +by f_equal. +Qed. + +Section measurable_fun_normalize. +Context d d' (X : measurableType d) (Y : measurableType d'). +Variable k : R.-sfker X ~> Y. + +Lemma measurable_fun_normalize : + measurable_fun setT (fun x => normalize k point x : pprobability Y R). +Proof. +apply: (@measurability _ _ _ _ _ _ + (@pset _ _ _ : set (set (pprobability Y R)))) => //. +move=> _ -[_ [r r01] [Ys mYs <-]] <-. +rewrite /normalize /mnormalize /mset /preimage/=. +apply: emeasurable_fun_infty_o => //. +rewrite /mnormalize/=. +rewrite (_ : (fun x => _) = (fun x => if (k x setT == 0) || (k x setT == +oo) + then \d_point Ys else k x Ys * ((fine (k x setT))^-1)%:E)); last first. + by apply/funext => x/=; case: ifPn. +apply: measurable_fun_if => //. +- apply: (measurable_fun_bool true) => //. + rewrite (_ : _ @^-1` _ = [set t | k t setT == 0] `|` + [set t | k t setT == +oo]); last first. + by apply/seteqP; split=> x /= /orP//. + by apply: measurableU; [exact: measurable_eq_cst|exact: measurable_eq_cst]. +- exact: measurable_fun_cst. +- apply/emeasurable_funM. + by apply: (@measurable_funS _ _ _ _ setT) => //; exact/measurable_kernel. + apply/EFin_measurable_fun; rewrite setTI. + apply: (@measurable_fun_comp _ _ _ _ _ _ [set r : R | r != 0%R]). + + exact: open_measurable. + + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey. + + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0. + exact: inv_continuous. + + apply: (@measurable_fun_comp _ _ _ _ _ _ setT) => //. + exact: measurable_fun_fine. + by apply: (@measurable_funS _ _ _ _ setT) => //; exact: measurable_kernel. +Qed. + +End measurable_fun_normalize. + +Definition eta1 x (l : context) t + (f : @typei2 R (slist (map snd l)) -> @typei2 R t) : + typei2 (slist (map snd (x :: l))) -> @typei2 R t := + f \o snd. + +Lemma meta1 x (l : context) t + (f : @typei2 R (slist (map snd l)) -> @typei2 R t) + (mf : measurable_fun setT f) : + measurable_fun setT (@eta1 x l t f). +Proof. by apply/(measurable_funT_comp mf); exact: measurable_fun_snd. Qed. + +Definition keta1 (x : string * stype) (l : context) t + (k : R.-sfker (@typei2 R (slist (map snd l))) ~> @typei2 R t) : + @typei2 R (slist (map snd (x :: l))) -> {measure set @typei2 R t -> \bar R} + := k \o snd. + +Section kernel_eta1. +Variables (x : string * stype) (l : context) (t : stype) + (k : R.-sfker (@typei2 R (slist (map snd l))) ~> @typei2 R t). + +Let mk U : measurable U -> measurable_fun setT ((@keta1 x l t k) ^~ U). +Proof. +move=> mU; rewrite (_ : (@keta1 x l t k) ^~ U = (k ^~ U) \o snd)//. +apply: measurable_funT_comp. + exact: measurable_kernel. +exact: measurable_fun_snd. +Qed. + +HB.instance Definition _ := + isKernel.Build _ _ _ _ _ (@keta1 x l t k) mk. +End kernel_eta1. + +Section sfkernel. +Variables (x : string * stype) (l : context) (t : stype) + (k : R.-sfker (@typei2 R (slist (map snd l))) ~> @typei2 R t). + +Let sk : exists2 s : (R.-ker (@typei2 R (slist (map snd (x :: l)))) ~> @typei2 R t)^nat, + forall n, measure_fam_uub (s n) & + forall x0 U, measurable U -> (@keta1 x l t k) x0 U = kseries s x0 U . +Proof. +have [s hs] := sfinite k. +exists (fun n => [the _.-ker _ ~> _ of @keta1 x l t (s n)]). + move=> n. + have [M hM] := measure_uub (s n). + exists M => x0. + exact: hM. +move=> x0 U mU. +by rewrite /keta1/= hs. +Qed. + +HB.instance Definition _ := + Kernel_isSFinite_subdef.Build _ _ _ _ _ (@keta1 x l t k) sk. + +End sfkernel. + +Section fkernel_eta1. +Variables (x : string * stype) (l : context) (t : stype) + (k : R.-fker (@typei2 R (slist (map snd l))) ~> @typei2 R t). + +Let uub : measure_fam_uub (@keta1 x l t k). +Proof. +have [M hM] := measure_uub k. +exists M => x0. +exact: hM. +Qed. + +HB.instance Definition _ := @Kernel_isFinite.Build _ _ _ _ _ + (@keta1 x l t k) uub. +End fkernel_eta1. + +Fixpoint free_varsD l t (e : @expD R l t) : seq string := + match e with + | exp_var _ x (*_*) _ _ => [:: x] + | exp_poisson _ _ e => free_varsD e + | exp_pair _ _ _ e1 e2 => free_varsD e1 ++ free_varsD e2 + | exp_unit _ => [::] + | exp_bool _ _ => [::] + | exp_real _ _ => [::] + | exp_bernoulli _ _ _ => [::] + | exp_norm _ _ e => free_varsP e + | expWD _ _ x e _ => rem x.1 (free_varsD e) + end +with free_varsP T l (e : expP T l) : seq _ := + match e with + | exp_if _ _ e1 e2 e3 => free_varsD e1 ++ free_varsP e2 ++ free_varsP e3 + | exp_letin _ _ _ x e1 e2 => free_varsP e1 ++ rem x (free_varsP e2) + | exp_sample_bern _ _ _ => [::] + | exp_score _ e => free_varsD e + | exp_return _ _ e => free_varsD e + | expWP _ _ x e _ => free_varsP e (*NB: why different from expWD case?*) + end. + +Inductive evalD : forall (l : context) (T : stype) (e : @expD R l T) + (f : typei2 (slist (map snd l)) -> typei2 T), + measurable_fun setT f -> Prop := +| E_unit l : + l # exp_unit -D-> cst tt ; ktt + +| E_bool l b : + l # exp_bool b -D-> cst b ; kb b + +| E_real l r : + l # exp_real r -D-> cst r ; kr r + +| E_pair l t1 t2 (G := slist (map snd l)) e1 f1 mf1 e2 f2 mf2 : + l # e1 -D-> f1 ; mf1 -> + l # e2 -D-> f2 ; mf2 -> + + l # exp_pair e1 e2 -D-> fun x => (f1 x, f2 x) ; + @measurable_fun_pair _ _ _ (typei2 G) (typei2 t1) (typei2 t2) f1 f2 mf1 mf2 + +| E_var (l : context) (x : string) : + let i := seq.index x (map fst l) in + l # exp_var x _ erefl -D-> varof (map snd l) i ; mvarof (map snd l) i + +| E_bernoulli l (r : {nonneg R}) (r1 : (r%:num <= 1)%R) : + l # exp_bernoulli r r1 -D-> + cst [the probability _ _ of bernoulli r1] ; measurable_fun_cst _ + +| E_poisson l k e f mf : + l # e -D-> f ; mf -> + l # exp_poisson k e -D-> poisson k \o f ; + measurable_funT_comp (mpoisson k) mf + +| E_norm l (t : stype) (e : expP l t) (k : R.-sfker _ ~> typei2 t) : + l # e -P-> k -> + l # exp_norm e -D-> (normalize k point : _ -> pprobability _ _) ; + measurable_fun_normalize k + +| E_WD l (t : stype) (e : expD l t) x (xl : x.1 \notin map fst l) f mf : + l # e -D-> f ; mf -> + (x :: l) # expWD e xl -D-> (@eta1 x l t f) ; (@meta1 x l t f mf) + +where "l # e -D-> v ; mv" := (@evalD l _ e v mv) + +with evalP : forall (l : context) (T : stype), + expP l T -> + R.-sfker (typei2 (slist (map snd l))) ~> typei2 T -> Prop := +| E_sample l (r : {nonneg R}) (r1 : (r%:num <= 1)%R) : + l # @exp_sample_bern R _ r r1 -P-> + sample [the probability _ _ of bernoulli r1] + +| E_ifP l T e1 f1 mf e2 k2 e3 k3 : + l # e1 -D-> f1 ; mf -> + l # e2 -P-> k2 -> + l # e3 -P-> k3 -> + l # exp_if e1 e2 e3 : expP l T -P-> ite mf k2 k3 + +| E_score l (G := slist (map snd l)) e (f : typei2 G -> R) + (mf : measurable_fun _ f) : + l # e : expD l sreal -D-> f ; mf -> + l # exp_score e -P-> [the R.-sfker _ ~> _ of kscore mf] + +| E_return l T e (f : _ -> _) (mf : measurable_fun _ f) : + l # e -D-> f ; mf -> + l # exp_return e : expP l T -P-> ret mf + +| E_letin (l : context) (G := slist (map snd l)) (t1 t2 : stype) + (x : string) (e1 : expP l t1) (e2 : expP ((x, t1) :: l) t2) + (k1 : R.-sfker (typei2 G) ~> typei2 t1) + (k2 : R.-sfker (typei2 (spair t1 G)) ~> typei2 t2) : + l # e1 -P-> k1 -> + ((x, t1) :: l)%SEQ # e2 -P-> k2 -> + l # exp_letin x e1 e2 -P-> letin' k1 k2 + +| E_WP l (t : stype) (e : expP l t) x (xl : x.1 \notin map fst l) k : + l # e -P-> k -> + (x :: l) # expWP e xl -P-> [the R.-sfker _ ~> _ of @keta1 x l t k] +where "l # e -P-> v" := (@evalP l _ e v). + +End eval. +Notation "l # e -D-> v ; mv" := (@evalD _ l _ e v mv) : lang_scope. +Notation "l # e -P-> v" := (@evalP _ l _ e v) : lang_scope. + +Ltac inj_ex H := revert H; + match goal with + | |- existT ?P ?l (existT ?Q ?t (existT ?R ?u (existT ?T ?v ?v1))) = + existT ?P ?l (existT ?Q ?t (existT ?R ?u (existT ?T ?v ?v2))) -> _ => + (intro H; do 4 apply Classical_Prop.EqdepTheory.inj_pair2 in H) + | |- existT ?P ?l (existT ?Q ?t (existT ?R ?u ?v1)) = + existT ?P ?l (existT ?Q ?t (existT ?R ?u ?v2)) -> _ => + (intro H; do 3 apply Classical_Prop.EqdepTheory.inj_pair2 in H) + | |- existT ?P ?l (existT ?Q ?t ?v1) = + existT ?P ?l (existT ?Q ?t ?v2) -> _ => + (intro H; do 2 apply Classical_Prop.EqdepTheory.inj_pair2 in H) + | |- existT ?P ?l ?v1 = + existT ?P ?l ?v2 -> _ => + (intro H; apply Classical_Prop.EqdepTheory.inj_pair2 in H) +end. + +Scheme evalD_mut_ind := Induction for evalD Sort Prop +with evalP_mut_ind := Induction for evalP Sort Prop. + +Scheme expD_mut_ind := Induction for expD Sort Prop +with expP_mut_ind := Induction for expP Sort Prop. + +Section eval_prop. +Local Open Scope lang_scope. +Variables (R : realType). + +Lemma evalD_uniq (l : context) (G := slist (map snd l)) t + (e : @expD R l t) (u v : typei2 G -> typei2 t) + (mu : measurable_fun setT u) (mv : measurable_fun setT v) : + l # e -D-> u ; mu -> l # e -D-> v ; mv -> u = v. +Proof. +move=> hu. +apply: (@evalD_mut_ind R + (fun l (G := slist (map snd l)) t (e : expD l t) (f : typei2 G -> typei2 t) + (mf : measurable_fun setT f) (h1 : evalD e mf) => + forall (v : typei2 G -> typei2 t) (mv : measurable_fun setT v), evalD e mv -> f = v) + (fun l (G := slist (map snd l)) t (e : expP l t) + (u : R.-sfker typei2 G ~> typei2 t) (h1 : evalP e u) => + forall (v : R.-sfker typei2 G ~> typei2 t), evalP e v -> u = v)); last exact: hu. +all: (rewrite {l G t e u v mu mv hu}). +- move=> l {}v {}mv. + inversion 1; subst l0. + by inj_ex H3. +- move=> l b {}v {}mv. + inversion 1; subst l0 b0. + by inj_ex H3. +- move=> l r {}v {}mv. + inversion 1; subst l0 r0. + by inj_ex H3. +- move=> l t1 t2 G e1 f1 mf1 e2 f2 mf2 ev1 IH1 ev2 IH2 {}v {}mv. + simple inversion 1 => //; subst l0. + case: H3 => ? ?; subst t0 t3. + inj_ex H4; case: H4 => He1 He2. + inj_ex He1; subst e0. + inj_ex He2; subst e3. + inj_ex H5; subst v. + by move=> /IH1 <- /IH2 <-. +- move=> l x n {}v {}mv. + inversion 1; subst l0 x0. + inj_ex H6. + by inj_ex H7. +- move=> l r r1 {}v {}mv. + inversion 1; subst l0 r0. + inj_ex H3; subst v. + by have -> : r1 = r3 by exact: Prop_irrelevance. +- move=> l k e0 f mf ev IH {}v {}mv. + inversion 1; subst l0 k0. + inj_ex H2; subst e0. + inj_ex H4; subst v. + by rewrite (IH _ _ H3). +- move=> l t e0 k ev IH {}v {}mv. + inversion 1; subst l0 t0. + inj_ex H2; subst e0. + inj_ex H4; subst v. + by rewrite (IH _ H3). +- move=> l t e0 x xl f mf ev IH {}v {}mv. + simple inversion 1 => //; subst t0. + case: H1 => ? ?; subst x0 l0. + inj_ex H3; case: H3 => H3; inj_ex H3; subst e0. + inj_ex H4; subst v. + by move=> /IH <-. +- move=> l r r1 p. + inversion 1; subst l0 r0. + inj_ex H3; subst p. + by have -> : r1 = r3 by exact: Prop_irrelevance. +- move=> l t e0 f1 mf1 e2 k2 e3 k3 ev1 IH1 ev2 IH2 ev3 IH3 k. + inversion 1; subst l0 T. + inj_ex H0; subst e0. + inj_ex H1; subst e4. + inj_ex H5; subst k. + inj_ex H2; subst e5. + have ? := IH1 _ _ H6; subst f2. + have -> : mf1 = mf by exact: Prop_irrelevance. + by rewrite (IH2 _ H7) (IH3 _ H8). +- move=> l G e0 f mf ev IH k. + simple inversion 1 => //; subst l0. + inj_ex H4; subst k. + inj_ex H3; case: H3 => H3; inj_ex H3; subst e0. + move/IH => ?; subst f0. + by have -> : mf = mf0 by exact: Prop_irrelevance. +- move=> l t e0 f mf ev IH k. + inversion 1; subst l0 T. + inj_ex H5; subst e1. + inj_ex H7; subst k. + have ? := IH _ _ H3; subst f1. + by have -> : mf = mf1 by exact: Prop_irrelevance. +- move=> l G t1 t2 x e1 e2 k1 k2 ev1 IH1 ev2 IH2 k. + inversion 1; subst l0 t0 t3 x0. + inj_ex H10; subst k. + inj_ex H8; subst e5. + inj_ex H7; subst e4. + by rewrite (IH1 _ H4) (IH2 _ H11). +- move=> l t e0 x xl k1 ev IH {}k. + inversion 1; subst l0 t0 x0. + inj_ex H4; subst e0. + inj_ex H5; subst k. + by rewrite (IH _ H3). +Qed. + +Lemma evalP_uniq (l : context) t (e : expP l t) + (u v : R.-sfker typei2 (slist (map snd l)) ~> typei2 t) : + evalP e u -> evalP e v -> u = v. +Proof. +move=> hu. +apply: (@evalP_mut_ind R + (fun l (G := slist (map snd l)) t (e : expD l t) (f : typei2 G -> typei2 t) + (mf : measurable_fun setT f) (h1 : evalD e mf) => + forall (v : typei2 G -> typei2 t) (mv : measurable_fun setT v), evalD e mv -> f = v) + (fun l (G := slist (map snd l)) t (e : expP l t) + (u : R.-sfker typei2 G ~> typei2 t) (h1 : evalP e u) => + forall (v : R.-sfker typei2 G ~> typei2 t), evalP e v -> u = v)); last exact: hu. +all: rewrite {l t e u v hu}. +- move=> l {}v {}mv. + inversion 1; subst l0. + by inj_ex H3. +- move=> l b {}v {}mv. + inversion 1; subst l0 b0. + by inj_ex H3. +- move=> l r {}v {}mv. + inversion 1; subst l0 r0. + by inj_ex H3. +- move=> l t1 t2 G e1 f1 mf1 e2 f2 mf2 ev1 IH1 ev2 IH2 {}v {}mv. + simple inversion 1 => //; subst l0. + case: H3 => ? ?; subst t0 t3. + inj_ex H4; case: H4 => He1 He2. + inj_ex He1; subst e0. + inj_ex He2; subst e3. + inj_ex H5; subst v. + move=> e1f0 e2f3. + by rewrite (IH1 _ _ e1f0) (IH2 _ _ e2f3). +- move=> l x n {}v {}mv. + inversion 1; subst l0. + inj_ex H7; subst v. + by inj_ex H6. +- move=> l r r1 {}v {}mv. + inversion 1; subst l0 r0. + inj_ex H3; subst v. + by have -> : r1 = r3 by exact: Prop_irrelevance. +- move=> l k e f mf ev IH {}v {}mv. + inversion 1; subst l0 k0. + inj_ex H2; subst e0. + inj_ex H4; subst v. + inj_ex H5; subst mv. + by rewrite (IH _ _ H3). +- move=> l t e k ev IH {}v {}mv. + inversion 1; subst l0 t0. + inj_ex H2; subst e0. + inj_ex H4; subst v. + inj_ex H5; subst mv. + by rewrite (IH _ H3). +- move=> l t e x xl f mf ev IH {}v {}mv. + simple inversion 1 => //; subst t0. + case: H1 => ? ?; subst x0 l0. + inj_ex H3; case: H3 => H3. + inj_ex H3; subst e0. + inj_ex H4; subst v. + inj_ex H5; subst mv. + by move/IH => <-. +- move=> l r r1 ev. + inversion 1; subst l0 r0. + inj_ex H3; subst ev. + by have -> : r1 = r3 by exact: Prop_irrelevance. +- move=> l t e f mf e1 k1 e2 k2 ev IH ev1 IH1 ev2 IH2 k. + inversion 1; subst l0 T. + inj_ex H0; subst e0. + inj_ex H1; subst e3. + inj_ex H5; subst k. + inj_ex H2; subst e4. + have ? := IH _ _ H6; subst f0. + have -> : mf0 = mf by exact: Prop_irrelevance. + by rewrite (IH1 _ H7) (IH2 _ H8). +- move=> l G e f mf ev IH k. + simple inversion 1 => //; subst l0. + inj_ex H4; subst k. + inj_ex H3; case: H3 => H3; inj_ex H3; subst e0. + move=> /IH ?; subst f0. + by have -> : mf = mf0 by exact: Prop_irrelevance. +- move=> l t e f mf ev IH k. + inversion 1; subst T l0. + inj_ex H7; subst k. + inj_ex H5; subst e1. + have ? := IH _ _ H3; subst f1. + by have -> : mf = mf1 by exact: Prop_irrelevance. +- move=> l G t1 t2 x e1 e2 k1 k2 ev1 IH1 ev2 IH2 k. + inversion 1; subst l0 x0 t3 t0. + inj_ex H10; subst k. + inj_ex H7; subst e4. + inj_ex H8; subst e5. + by rewrite (IH1 _ H4) (IH2 _ H11). +- move=> l t e x xl k1 ev IH {}k. + inversion 1; subst x0 l0 t0. + inj_ex H4; subst e0. + inj_ex H5; subst k. + by rewrite (IH _ H3). +Qed. + +Lemma evalD_full (l : context) (t : stype) e : + exists f (mf : measurable_fun _ f), @evalD R l t e f mf. +Proof. +apply: (@expD_mut_ind R + (fun l t (e : expD l t) => exists f (mf : measurable_fun setT f), evalD e mf) + (fun l t (e : expP l t) => exists k, evalP e k)). +all: rewrite {l t e}. +- move=> l st x e [f [mf fmf]] xl. + by exists (eta1 f), (meta1 mf); exact/E_WD. +- by do 2 eexists; exact: E_unit. +- by do 2 eexists; exact: E_bool. +- by do 2 eexists; exact: E_real. +- move=> l t1 t2 e1 [f1 [mf1 H1]] e2 [f2 [mf2 H2]]. + by exists (fun x => (f1 x, f2 x)); eexists; exact: E_pair. +- by move=> l x t tE; subst t; eexists; eexists; exact: E_var. +- by move=> r r1; eexists; eexists; exact: E_bernoulli. +- move=> l k e [f [mf H]]. + exists (poisson k \o f), (measurable_funT_comp (mpoisson k) mf). + exact: E_poisson. +- move=> l t e [k H]. + by exists (normalize k point), (measurable_fun_normalize k); exact: E_norm. +- move=> l st x e [k H1] xl. + by exists [the _.-sfker _ ~> _ of keta1 k]; exact: E_WP. +- move=> l t e1 [f [mf H1]] e2 [k2 H2] e3 [k3 H3]. + by exists (ite mf k2 k3); exact: E_ifP. +- move=> l t1 t2 x e1 [k1 ev1] e2 [k2 ev2]. + by exists (letin' k1 k2); exact: E_letin. +- move=> l r r1. + by exists (sample [the pprobability _ _ of bernoulli r1]); exact: E_sample. +- move=> l e [f [mf f_mf]]. + by exists (score mf); exact: E_score. +- by move=> l t e [f [mf f_mf]]; exists (ret mf); exact: E_return. +Qed. + +Lemma evalP_full (l : context) (t : stype) e : + exists (k : R.-sfker _ ~> _), @evalP R l t e k. +Proof. +apply: (@expP_mut_ind R + (fun l t (e : expD l t) => exists f (mf : measurable_fun _ f), evalD e mf) + (fun l t (e : expP l t) => exists k, evalP e k)). +all: rewrite {l t e}. +- move=> l t x e [f [mf H]] xl. + by exists (eta1 f), (meta1 mf); exact: E_WD. +- by do 2 eexists; exact: E_unit. +- by do 2 eexists; exact: E_bool. +- by do 2 eexists; exact: E_real. +- move=> l t1 t2 e1 [f1 [mf1 H1]] e2 [f2 [mf2 H2]]. + by exists (fun x => (f1 x, f2 x)); eexists; exact: E_pair. +- by move=> l x t tE; subst t; eexists; eexists; exact: E_var. +- by move=> r r1; eexists; eexists; exact: E_bernoulli. +- move=> l k e [f [mf H]]. + exists (poisson k \o f), (measurable_funT_comp (mpoisson k) mf). + exact: E_poisson. +- move=> l t e []k H. + by exists (normalize k point), (measurable_fun_normalize k); exact: E_norm. +- move=> l s x e [k H1] xl. + by exists [the _.-sfker _ ~> _ of keta1 k]; exact: E_WP. +- move=> l t e1 [f [mf H1]] e2 [k2 H2] e3 [k3 H3]. + by exists (ite mf k2 k3); exact: E_ifP. +- move=> l t1 t2 x e1 [k1 ev1] e2 [k2 ev2]. + by exists (letin' k1 k2); exact: E_letin. +- move=> l r r1. + by exists (sample [the pprobability _ _ of bernoulli r1]); exact: E_sample. +- by move=> l e [f [mf H]]; exists (score mf); exact: E_score. +- by move=> l t e [f [mf H]]; exists (ret mf); exact: E_return. +Qed. + +Definition execP l t (e : @expP R l t) : + R.-sfker (@typei2 R (slist (map snd l))) ~> @typei2 R t. +Proof. +have /cid h := @evalP_full l t e. +exact: (proj1_sig h). +Defined. + +Lemma evalP_execP l t e : l # e -P-> @execP l t e. +Proof. by rewrite /execP/= /sval ?/ssr_have/=; case: cid. Qed. + +Definition execD l t (e : @expD R l t) : + {f : (@typei2 R (slist (map snd l))) -> @typei2 R t & measurable_fun setT f}. +Proof. +have /cid [f /cid[mf H]] := @evalD_full l t e. +by exists f. +Defined. + +Lemma evalD_execD l t e : let: x := @execD l t e in + l # e -D-> projT1 x ; projT2 x. +Proof. +rewrite /execD ?/ssr_have /= /sval /=; case: cid => f [mf ef]. +by case: cid. +Defined. + +Definition execP_ret_real (l : context) (r : R) : + R.-sfker (@typei2 R (slist (map snd l))) ~> @typei2 R sreal := + execP (exp_return (exp_real r)). + +Scheme expD_mut_rec := Induction for expD Sort Type +with expP_mut_rec := Induction for expP Sort Type. + +Definition rem_context l t (e : @expP R l t) (H : free_varsP e = [::]) : @expP R [::] t. +move: H. +apply: (@expP_mut_rec R + (fun (l : context) (t : stype) (e : expD l t) => + free_varsD e = [::] -> expD [::] t) + (fun (l : context) (t : stype) (e : expP l t) => + free_varsP e = [::] -> expP [::] t) + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ l t e). +- move=> l0 st x e0 H1 xl H2. +(* apply (expWD e0 x). *) +admit. +move=> ? ?; exact: exp_unit. +move=> ? b ?; exact: (exp_bool b). +move=> ? r ?; exact: (exp_real r). +move=> t1 t2 ? e1 t1nil e2 t2nil H. +rewrite /= in H. +apply: exp_pair. +apply: t1nil. +(* by destruct (free_varsD e1). +apply: t2nil. +destruct (free_varsD e2). +reflexivity. +move/(congr1 size) : H. +by rewrite size_cat/= addnS. +done. +move=> ? r r1 H. +apply: exp_bernoulli. +exact: r1. +rewrite /=. +move=> ? n e1 h H. +apply: (exp_poisson n). +exact: h. +rewrite /=. +move=> ? ? e1 h H. +apply: exp_norm. +exact: h. +admit. +move=> ? ? e1 h1 e2 h2 e3 h3 /= H. +apply: exp_if. +apply: h1. +by destruct (free_varsD e1). +apply: h2. +move: H. +destruct (free_varsP e2) => //=. +move=>/(congr1 size). +by rewrite !size_cat/= addnS. +apply: h3. +destruct (free_varsP e3) => //=. +move/(congr1 size) : H. +by rewrite !size_cat/= !addnS. +rewrite /=. +move=> ? t1 t2 x e1 h1 e2 h2 H. *) +Abort. + +(* Variables (dT : measure_display) (T : measurableType dT). +(* Definition m := fun A => (_ : {measure set (@typei2 R A) -> \bar R}). *) + +Axiom same_expP : forall (l l' : context) (T : stype) (e : @expP R T l) + (e' : @expP R T l'), Prop. *) + +Lemma evalP_uni_new x r + (u : R.-sfker munit ~> mR R) + (v : R.-sfker (typei2 (slist [seq i.2 | i <- [:: (x, sreal)]])) ~> mR R) : + evalP (exp_return (exp_real r) : expP [::] sreal) u -> + evalP (exp_return (exp_real r) : expP [:: (x, sreal)] sreal) v -> + forall x0 t, v (x0, t) = u t. +Proof. +move=> H1 H2. +have -> : u = ret (kr r). +have := @evalP_uniq [::] sreal (exp_return (exp_real r)) u (ret (kr r)) H1. +apply. +apply/E_return /E_real. +suff : v = ret (kr r) by move=> ->. +have := @evalP_uniq [:: (x, sreal)] sreal (exp_return (exp_real r)) v (ret (kr r)) H2. +apply. +exact/E_return/E_real. +Qed. + +Require Import JMeq. + +Obligation Tactic := idtac. + +Program Fixpoint wP {st} {l : context} (x : string * stype) (e : @expP R l st) + : @expP R (x :: l) st := +match e with +| exp_return l0 _ e0 => @exp_return R (x :: l0) _ (wD x e0) +| exp_if l0 _ e1 e2 e3 => @exp_if R (x :: l0) _ (wD x e1) (wP x e2) (wP x e3) +| exp_letin l0 _ _ x0 e1 e2 => @exp_letin R (x :: l0) _ _ x0 (wP x e1) (wP _ e2) +| exp_sample_bern l0 _ _ => _ +| exp_score l0 e1 => _ +| expWP l0 _ x e0 xl => _ +end with wD {st} {l : context} x (e : @expD R l st) := +match e with +| _ => _ +end. +Next Obligation. +Admitted. +Next Obligation. +move=> st l x e l0 ? ? x0 e1 e2 l0l ? ?. +Admitted. +Next Obligation. +Admitted. +Next Obligation. +Admitted. +Next Obligation. +Admitted. +Next Obligation. +Admitted. + +(*Definition vx : R.-sfker munit ~> mR R := execP_ret_real [::] 1. +Definition VX z : set (mR R) -> \bar R := vx z. +Let VX0 z : (VX z) set0 = 0. Proof. by []. Qed. +Let VX_ge0 z x : 0 <= (VX z) x. Proof. by []. Qed. +Let VX_semi_sigma_additive z : semi_sigma_additive (VX z). +Proof. exact: measure_semi_sigma_additive. Qed. +HB.instance Definition _ z := @isMeasure.Build _ R (mR R) (VX z) (VX0 z) + (VX_ge0 z) (@VX_semi_sigma_additive z). +Let sfinVX z : sfinite_measure (VX z). Proof. exact: sfinite_kernel_measure. Qed. +HB.instance Definition _ z := @Measure_isSFinite_subdef.Build _ (mR R) R + (VX z) (sfinVX z). + +Definition vy' : R.-sfker munit ~> mR R := execP_ret_real [::] 2. +Definition VY z : set (mR R) -> \bar R := vy' z. +Let VY0 z : (VY z) set0 = 0. Proof. by []. Qed. +Let VY_ge0 z x : 0 <= (VY z) x. Proof. by []. Qed. +Let VY_semi_sigma_additive z : semi_sigma_additive (VY z). +Proof. exact: measure_semi_sigma_additive. Qed. +HB.instance Definition _ z := @isMeasure.Build _ R (mR R) (VY z) (VY0 z) + (VY_ge0 z) (@VY_semi_sigma_additive z). +Let sfinVY z : sfinite_measure (VY z). Proof. exact: sfinite_kernel_measure. Qed. +HB.instance Definition _ z := @Measure_isSFinite_subdef.Build _ (mR R) R + (VY z) (sfinVY z).*) + +Lemma execP_WP_keta1 x l (st : stype_eqType) (e : expP l st) (xl : x.1 \notin map fst l) : + execP (@expWP R l st _ e xl) = [the _.-sfker _ ~> _ of keta1 (execP e)]. +Proof. +apply: evalP_uniq; first exact/evalP_execP. +by apply: E_WP; exact: evalP_execP. +Qed. + +Lemma execP_letin l x t1 t2 (e1 : expP l t1) (e2 : expP ((x, t1) :: l) t2) : + execP [Let x <~ e1 In e2] = letin' (execP e1) (execP e2) :> (R.-sfker _ ~> _). +Proof. +apply: evalP_uniq; first exact/evalP_execP. +by apply: E_letin; exact/evalP_execP. +Qed. + +Lemma execP_ret l t (e : @expD R l t) : execP [Ret e] = ret (projT2 (execD e)). +Proof. +apply: evalP_uniq; first exact: evalP_execP. +by apply: E_return; exact: evalD_execD. +Qed. + +Lemma execD_pair l (G := slist (map snd l)) t1 t2 + (x : @expD R l t1) + (y : @expD R l t2) : + let f := projT1 (execD x) in + let g := projT1 (execD y) in + let mf := projT2 (execD x) in + let mg := projT2 (execD y) in + execD [(x, y)] = + @existT _ _ (fun z => (f z, g z)) + (@measurable_fun_pair _ _ _ (typei2 (slist (map snd l))) (typei2 t1) (typei2 t2) + f g mf mg). +Proof. +move=> f g mf mg. +rewrite /f /g /mf /mg. +set lhs := LHS. +set rhs := RHS. +have h : projT1 lhs = projT1 rhs. + apply: (@evalD_uniq l _ [(x, y)] (projT1 lhs) (projT1 rhs) (projT2 lhs) (projT2 rhs)). + exact: evalD_execD. + by apply: E_pair; exact: evalD_execD. +exact: eq_sigT_hprop. +Qed. + +Lemma execD_var l (x : string) : + let i := seq.index x (map fst l) in + @execD l _ [% {x} ] = existT _ (varof (map snd l) i) (@mvarof R (map snd l) i). +Proof. +rewrite /execD /=. +case: cid => f ?. +case: cid => ? ev1. +have ev2 := (E_var R l x). +have fcstr := (evalD_uniq ev1 ev2). +subst. +congr existT. +apply Prop_irrelevance. +Qed. + +End eval_prop. + +Section staton_bus. +Local Open Scope ring_scope. +Local Open Scope lang_scope. +Variables (R : realType). + +Example __ : @evalD R [::] _ [{3}:r] (cst 3) (kr 3). +Proof. apply/E_real. Qed. + +Example ex_ret : @evalP R [::] _ [Ret {3}:r] (ret (kr 3)). +Proof. apply/E_return/E_real. Qed. + +Check ret (kr 3) : R.-sfker _ ~> (mR R). +Check ret (kr 3) tt : {measure set mR R -> \bar R}. +Goal (ret (kr 3) : R.-sfker _ ~> (mR R)) tt [set: R] = 1%:E. +Proof. rewrite /= diracE in_setT //. Qed. + +Structure tagged_context := Tag {untag : context}. + +Definition recurse_tag h := Tag h. +Canonical found_tag h := recurse_tag h. + +Structure find (s : string) (t : stype) := Find { + context_of : tagged_context ; + ctxt_prf : t = nth sunit (map snd (untag context_of)) + (seq.index s (map fst (untag context_of)))}. + +Lemma left_pf (s : string) (t : stype) (l : context) : + t = nth sunit (map snd ((s, t) :: l)) (seq.index s (map fst ((s, t) :: l))). +Proof. +by rewrite /= !eqxx/=. +Qed. + +Canonical found_struct s t (l : context) : find s t := + Eval hnf in @Find s t (found_tag ((s, t) :: l)) (@left_pf s t l). + +Lemma right_pf (s : string) (t : stype) (l : context) u t' : + s != u -> + t' = nth sunit (map snd l) (seq.index u (map fst l)) -> + t' = nth sunit (map snd ((s, t) :: l)) (seq.index u (map fst ((s, t) :: l))). +Proof. +move=> su ut'l /=. +case: ifPn => //=. +by rewrite (negbTE su). +Qed. + +Definition varx := "x". +Definition varr := "r". +Definition var_ := "_". + +Class diff (s tu : string) := Diff { + diff_su : s != tu +}. + +Global Instance diff_x : diff "_" varx := @Diff "_" varx erefl. +Global Instance diff_r : diff "_" _ := @Diff "_" varr erefl. +Global Instance diffx_ : diff "x" _ := @Diff "x" var_ erefl. +Global Instance diffxr : diff "x" _ := @Diff "x" varr erefl. +Global Instance diffrx : diff "r" _ := @Diff "r" varx erefl. +Global Instance diffr_ : diff "r" _ := @Diff "r" var_ erefl. + +Canonical recurse_struct s t t' u {su : diff s u} (l : find u t') : find u t' := + Eval hnf in @Find u t' (recurse_tag ((s, t) :: untag (context_of l))) + (@right_pf s t (untag (context_of l)) u t' (@diff_su _ _ su) (ctxt_prf l)). + +Definition exp_var' (x : string) (t : stype) (g : find x t) := + @exp_var R (untag (context_of g)) x t (ctxt_prf g). + +Notation "%1 x" := (@exp_var' x%string _ _) (in custom expr at level 1). + +Example staton_bus_exp := exp_norm ( + [Let "x" <~ {exp_sample_bern [::] (2 / 7%:R)%:nng p27} In + Let "r" <~ If %1{"x"} Then Ret {3}:r Else Ret {10}:r In + Let "_" <~ {exp_score (exp_poisson 4 [%1{"r"}])} In + Ret %1{"x"}]). + +Definition sample_bern : R.-sfker munit ~> mbool := + sample [the probability _ _ of bernoulli p27]. +Definition ite_3_10 : + R.-sfker [the measurableType _ of (mbool * munit)%type] ~> (mR R) := + ite var1of4' (ret k3) (ret k10). +Definition score_poi : + R.-sfker [the measurableType _ of (mR R * (mbool * munit))%type] ~> munit := + score (measurable_funT_comp (mpoisson 4) var1of4'). + +Local Definition kstaton_bus'' := + letin' sample_bern + (letin' ite_3_10 + (letin' score_poi (ret var3of4'))). + +Example eval_staton_bus_exp : + [::] # staton_bus_exp -D-> _ ; measurable_fun_normalize kstaton_bus''. +Proof. +apply/E_norm/E_letin. +- exact/E_sample. +- apply/E_letin. + + apply/E_ifP. + * rewrite /exp_var' /=. + rewrite (_ : left_pf _ _ _ = erefl) //. + set l := (X in X # _ -D-> _ ; _). + rewrite (_ : var1of2 = @mvarof R (map snd l) 0)//. + exact: (E_var _ _ "x"). + * exact/E_return/E_real. + * exact/E_return/E_real. +- apply: E_letin. + + apply/E_score/E_poisson. + rewrite /exp_var'/=. + rewrite (_ : left_pf _ _ _ = erefl) //. + set l := (X in X # _ -D-> _ ; _). + rewrite (_ : var1of2 = @mvarof R (map snd l) 0)//. + exact: (E_var _ _ "r"). + + apply/E_return. + rewrite /exp_var'/=. + rewrite (_ : right_pf _ _ _ = erefl) //. + set l := (X in X # _ -D-> _ ; _). + rewrite (_ : var3of4' = @mvarof R (map snd l) 2)//. + exact: (E_var _ _ "x"). +Qed. + +End staton_bus. + +Section letinC. +Local Open Scope lang_scope. +Variable R : realType. + +Check [Let "x" <~ Ret %{"y"} In Ret %{"x"}]. + +Lemma execP_WP_keta1 x l (st : stype_eqType) (e : expP l st) (xl : x.1 \notin map fst l) : + execP (@expWP R l st _ e xl) = [the _.-sfker _ ~> _ of keta1 (execP e)]. +Proof. +apply: evalP_uniq; first exact/evalP_execP. +by apply: E_WP; exact: evalP_execP. +Qed. + +Lemma execD_real l r : + @execD R l _ [r :r] = existT _ (cst r) (kr r). +Proof. +rewrite /execD /=. +case: cid => f ?. +case: cid => ? ev1. +have ev2 := (E_real l r). +have fcstr := (evalD_uniq ev1 ev2). +subst. +congr existT. +apply Prop_irrelevance. +Qed. + +Lemma execD_var l x : + let i := seq.index x (map fst l) in + @execD R l _ [%x] = existT _ (varof (map snd l) i) (@mvarof R (map snd l) i). +Proof. +rewrite /execD /=. +case: cid => f ?. +case: cid => ? ev1. +have ev2 := (E_var R l x). +have fcstr := (evalD_uniq ev1 ev2). +subst. +congr existT. +apply Prop_irrelevance. +Qed. + +Lemma execP_letin l x t1 t2 (e1 : expP l t1) (e2 : expP ((x, t1) :: l) t2) : + execP [Let x <~ e1 In e2] = letin' (execP e1) (execP e2) :> (R.-sfker _ ~> _). +Proof. +apply: evalP_uniq; first exact/evalP_execP. +by apply: E_letin; exact/evalP_execP. +Qed. + +Lemma execP_ret l t (e : @expD R l t) : execP [Ret e] = ret (projT2 (execD e)). +Proof. +apply: evalP_uniq; first exact: evalP_execP. +by apply: E_return; exact: evalD_execD. +Qed. + +Lemma execD_pair l (G := slist (map snd l)) t1 t2 + (x : @expD R l t1) + (y : @expD R l t2) : + let f := projT1 (execD x) in + let g := projT1 (execD y) in + let mf := projT2 (execD x) in + let mg := projT2 (execD y) in + execD [(x, y)] = + @existT _ _ (fun z => (f z, g z)) + (@measurable_fun_pair _ _ _ (typei2 (slist (map snd l))) (typei2 t1) (typei2 t2) + f g mf mg). +Proof. +move=> f g mf mg. +rewrite /f /g /mf /mg. +set lhs := LHS. +set rhs := RHS. +have h : projT1 lhs = projT1 rhs. + apply: (@evalD_uniq R l _ [(x, y)] (projT1 lhs) (projT1 rhs) (projT2 lhs) (projT2 rhs)). + exact: evalD_execD. + by apply: E_pair; exact: evalD_execD. +exact: eq_sigT_hprop. +Qed. + +Lemma ex_var_ret l : @execP R l _ [Let "x" <~ Ret {1}:r In Ret %{"x"}] = letin' (ret (kr 1)) (ret var1of2). +Proof. +rewrite execP_letin; congr letin'. +by rewrite execP_ret execD_real. +by rewrite execP_ret execD_var; congr ret. +Qed. + +(* Lemma letin_pair l : @letin' _ _ _ _ _ _ R (ret (kr 1)) + (letin' (ret (kr 2)) + (ret + (measurable_fun_pair (T:=typei2 (slist [:: sreal, sreal & [seq i.2 | i <- l]])) (T1:= + typei2 sreal) (T2:=typei2 sreal) + (f:=fun H : R * (R * projT2 (prod_meas [seq typei i | i <- [seq i.2 | i <- l]])) => H.2.1) + (g:=fst) (mvarof (R:=R) (l:=[:: ("y", sreal), ("x", sreal) & l]) (i:=1)) + (mvarof (R:=R) (l:=[:: ("y", sreal), ("x", sreal) & l]) (i:=0))))) + = ret (measurable_fun_pair (kr 1) (kr 2)). +Proof. +apply: eq_sfkernel => ? U. +rewrite retE diracE. +rewrite letin'E. +under eq_integral. + move=> x xS. + rewrite letin'E. + under eq_integral do rewrite retE diracE /=. + over. +rewrite !retE !integral_dirac //=. +by rewrite indicT //= 2!mul1e. +apply (@measurable_fun_pair _ _ _ (mR R) _ _ (cst 1) id). +Admitted. *) + +Lemma ex_var_ret2 l : + @execP R l _ [Let "x" <~ Ret {1}:r In Let "y" <~ Ret {2}:r In + Ret (%{"x"}, %{"y"})] = + @execP R l _ [Let "y" <~ Ret {2}:r In Let "x" <~ Ret {1}:r In + Ret (%{"x"}, %{"y"})]. +Proof. +rewrite !execP_letin !execP_ret !execD_real. +rewrite !execD_pair !execD_var /=. +(* rewrite letin_pair /=. +by rewrite execP_ret execD_real. +by rewrite execP_ret execD_var; congr ret. *) +Admitted. + +Lemma letinC_new l t1 t2 (e1 : @expP R l t1) (e2 : expP l t2) + (xl : "x" \notin map fst l) (yl : "y" \notin map fst l) : + forall U, measurable U -> + execP [Let "x" <~ e1 In + Let "y" <~ {@expWP _ _ _ ("x", t1) e2 xl} In + Ret (%{"x"}, %{"y"})] ^~ U = + execP [Let "y" <~ e2 In + Let "x" <~ {@expWP _ _ _ ("y", t2) e1 yl} In + Ret (%{"x"}, %{"y"})] ^~ U. +Proof. +move=> U mU; apply/funext => x. +rewrite 4!execP_letin. +rewrite 2!execP_WP_keta1. +rewrite 2!execP_ret /=. +rewrite 2!execD_pair/=. +rewrite (execD_var _ _ "x")/= (execD_var _ _ "y")/=. +apply: trans_eq. + apply: trans_eq; last first. + apply: (@letin'C _ _ _ _ _ _ _ (execP e1) (execP (@expWP _ _ _ ("y", t2) e1 yl)) _ + (execP e2) (execP (@expWP _ _ _ ("x", t1) e2 xl)) _). + - by rewrite -/typei => y z; rewrite execP_WP_keta1. + - by move=> y z; rewrite execP_WP_keta1. + - exact: x. + - by rewrite -/typei; exact: mU. + rewrite -/typei execP_WP_keta1/=. + set lhs := measurable_fun_pair _ _. + set rhs := measurable_fun_pair _ _. + by have -> : lhs = rhs by exact: Prop_irrelevance. +rewrite -/typei. +rewrite (execD_var _ _ "x")/= (execD_var _ _ "y")/=. +rewrite execP_WP_keta1/=. +set lhs := measurable_fun_pair _ _. +set rhs := measurable_fun_pair _ _. +by have -> : lhs = rhs by exact: Prop_irrelevance. +Qed. + +Lemma letinC l t1 t2 (e1 : @expP R l t1) (e2 : expP l t2) + (xl : "x" \notin map fst l) (yl : "y" \notin map fst l) + (v1 v2 : R.-sfker typei2 (slist (map snd l)) ~> typei2 (spair t1 t2)) : + l # [Let "x" <~ e1 In + Let "y" <~ {@expWP _ _ _ ("x", t1) e2 xl} In + Ret (%{"x"}, %{"y"})] -P-> v1 + -> + l # [Let "y" <~ e2 In + Let "x" <~ {@expWP _ _ _ ("y", t2) e1 yl} In + Ret (%{"x"}, %{"y"})] -P-> v2 -> + forall U, measurable U -> v1 ^~ U = v2 ^~ U. +Proof. +move=> ev1 ev2. +pose k1 : R.-sfker _ ~> typei2 t1 := execP e1. +pose k2' : R.-sfker _ ~> _ := @execP R (("x", t1) :: l) t2 (@expWP _ _ _ ("x", t1) e2 xl). +pose vx : R.-sfker typei2 (slist (map snd l)) ~> + [the measurableType _ of (typei2 t1 * typei2 t2)%type] := + letin' k1 + (letin' k2' + (ret (measurable_fun_pair + (T:= [the measurableType _ of + (typei2 t2 * (typei2 t1 * (projT2 (prod_meas (map typei (map snd l))))))%type]) + (T1:= typei2 t1) + (f := fst \o snd) (g:= fst) var2of4' var1of2))). +have ev1' : l # [Let "x" <~ e1 In Let "y" <~ {@expWP _ _ _ ("x", t1) e2 xl} In Ret (%{"x"}, %{"y"})] -P-> vx. + apply: E_letin; first exact: evalP_execP. + apply: E_letin; first exact: evalP_execP. + apply/E_return/E_pair. + - have -> : var2of4' = @mvarof R (t2 :: t1 :: map snd l) 1 by []. + exact: E_var. + - have -> : var1of2 = @mvarof R (t2 :: t1 :: map snd l) 0 by []. + exact: E_var. +rewrite (evalP_uniq ev1 ev1'). +pose k2 : R.-sfker _ ~> typei2 t2 := @execP R l t2 e2. +pose k1' : R.-sfker _ ~> _ := @execP R [:: ("y", t2) & l] t1 (@expWP _ _ _ ("y", t2) e1 yl). +pose vy : R.-sfker typei2 (slist (map snd l)) ~> + [the measurableType _ of (typei2 t1 * typei2 t2)%type] := + letin' k2 (letin' k1' + (ret (measurable_fun_pair + (T := [the measurableType _ of + typei2 t1 * (typei2 t2 * (projT2 (prod_meas (map typei (map snd l)))))]%type) + (T2 := typei2 t2) (f := fst) (g:= fst \o snd) var1of2 var2of4'))). +have ev2' : l # [Let "y" <~ e2 In Let "x" <~ {@expWP _ _ _ ("y", t2) e1 yl} In Ret (%{"x"}, %{"y"})] -P-> vy. + apply: E_letin; first exact: evalP_execP. + apply: E_letin; first exact: evalP_execP. + apply/E_return/E_pair. + - have -> : var1of2 = @mvarof R (t1 :: t2 :: map snd l) 0 by []. + exact: E_var. + - have -> : var2of4' = @mvarof R (t1 :: t2 :: map snd l) 1 by []. + exact: E_var. +rewrite (evalP_uniq ev2 ev2'). +rewrite /vx /vy => t U/=. +apply/funext => x. +apply: (@letin'C _ _ _ (typei2 t1) (typei2 t2)). +- move=> ST /= TATBU. + rewrite /k1' /k1. + by rewrite (@execP_WP_keta1 _ ("y", t2) _ _ e1). +- move=> ST /= TATBU. + rewrite /k2 /k2'. + by rewrite (@execP_WP_keta1 _ ("x", t1) _ _ e2). +- by []. +Qed. + +Example letinr_ ta tb (l := [:: ("r", ta); ("_", tb)]) t1 t2 + (e1 : @expP R l t1) (e2 : expP l t2) + (v1 v2 : (R.-sfker typei2 (slist (map snd l)) ~> typei2 (spair t1 t2))) : + l # [Let "x" <~ e1 In + Let "y" <~ %WP {"x"} # e2 In + Ret (%{"x"}, %{"y"})] -P-> v1 + -> + l # [Let "y" <~ e2 In + Let "x" <~ %WP {"y"} # e1 In + Ret (%{"x"}, %{"y"})] -P-> v2 -> + forall U, measurable U -> v1 ^~ U = v2 ^~ U. +Proof. exact: letinC. Abort. + +Example letinC12 (v1 v2 : R.-sfker munit ~> typei2 (spair sreal sreal)) U : + measurable U -> + [::] # [Let "x" <~ Ret {1}:r In + Let "y" <~ Ret {2}:r In + Ret (%{"x"}, %{"y"})] -P-> v1 -> + [::] # [Let "y" <~ Ret {2}:r In + Let "x" <~ Ret {1}:r In + Ret (%{"x"}, %{"y"})] -P-> v2 -> + v1 ^~ U = v2 ^~ U. +Proof. +(*move=> mU hv1 hv2. +have := @letinC [::] sreal sreal + (@exp_return _ _ _ (exp_real 1)) + (@exp_return _ _ _ (exp_real 2)) erefl erefl v1 v2. +apply => //. xxx*) +set d := (x in (projT1 x).-measurable _). +move=> mM ev1 ev2. +pose vx : R.-sfker munit ~> mR R := execP_ret_real [::] 1. +pose vy : R.-sfker [the measurableType _ of (mR R * munit)%type] ~> mR R := + execP_ret_real [:: ("x", sreal)] 2. +have -> : v1 = letin' vx (letin' vy (ret (measurable_fun_pair var2of3' var1of3'))). + apply: (evalP_uniq ev1). + apply: E_letin; first exact: evalP_execP. + apply: E_letin; first exact: evalP_execP. + apply/E_return/E_pair. + - have -> : var2of3' = @mvarof R [:: sreal; sreal] 1 by []. + exact: E_var. + - have -> : var1of4' = @mvarof R [:: sreal; sreal] 0 by []. + exact: E_var. +pose vy' : R.-sfker munit ~> mR R := execP_ret_real [::] 2. +pose vx' : R.-sfker [the measurableType _ of (mR R * munit)%type] ~> mR R := + execP_ret_real [:: ("y", sreal)] 1. +have -> : v2 = letin' vy' (letin' vx' (ret (measurable_fun_pair var1of3' var2of3'))). + apply: (evalP_uniq ev2). + apply: E_letin; first exact: evalP_execP. + apply: E_letin; first exact: evalP_execP. + apply/E_return/E_pair. + - have -> : var1of3' = @mvarof R [:: sreal; sreal] 0 by []. + exact: E_var. + - have -> : var2of3' = @mvarof R [:: sreal; sreal] 1 by []. + exact: E_var. +apply/funext => -[]. +apply: letin'C; [ | | by []]. +- move=> /= r []. + rewrite /vx /vx'. + rewrite (@evalP_uni_new _ "y" 1 vx vx'); first by []. + + exact: evalP_execP. + + exact: evalP_execP. +- move=> x0 t0. + rewrite /vy /vy'. + apply/esym/evalP_uni_new. + + exact: evalP_execP. + + exact: evalP_execP. +Qed. + +End letinC. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 96bb978d32..c4c7567de3 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -4090,8 +4090,12 @@ Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Implicit Types A : set (T1 * T2). Section xsection. -Variables (pt2 : T2) (m2 : {measure set T2 -> \bar R}). -Let phi A := m2 \o xsection A. +Variables (pt2 : T2) (m2 : T1 -> {measure set T2 -> \bar R}). +(* the generalization from m2 : {measure set T2 -> \bar R}t to + T1 -> {measure set T2 -> \bar R} is needed to develop the theory + of kernels; the original type was sufficient for the development + of the theory of integration *) +Let phi A x := m2 x (xsection A x). Let B := [set A | measurable A /\ measurable_fun setT (phi A)]. Lemma xsection_ndseq_closed : ndseq_closed B. diff --git a/theories/prob_lang.v b/theories/prob_lang.v new file mode 100644 index 0000000000..65dce052bb --- /dev/null +++ b/theories/prob_lang.v @@ -0,0 +1,1199 @@ +(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import rat. +Require Import mathcomp_extra boolp classical_sets signed functions cardinality. +Require Import reals ereal topology normedtype sequences esum measure. +Require Import lebesgue_measure fsbigop numfun lebesgue_integral exp kernel. + +(******************************************************************************) +(* Semantics of a probabilistic programming language using s-finite kernels *) +(* *) +(* bernoulli r1 == Bernoulli probability with r1 a proof that *) +(* r : {nonneg R} is smaller than 1 *) +(* *) +(* sample P == sample according to the probability P *) +(* letin l k == execute l, augment the context, and execute k *) +(* ret mf == access the context with f and return the result *) +(* score mf == observe t from d, where f is the density of d and *) +(* t occurs in f *) +(* e.g., score (r e^(-r * t)) = observe t from exp(r) *) +(* pnormalize k P == normalize the kernel k into a probability kernel, *) +(* P is a default probability in case normalization is *) +(* not possible *) +(* ite mf k1 k2 == access the context with the boolean function f and *) +(* behaves as k1 or k2 according to the result *) +(* *) +(* poisson == Poisson distribution function *) +(* exp_density == density function for exponential distribution *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.ExtraDef Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. + +(* TODO: PR *) +Lemma onem1' (R : numDomainType) (p : R) : (p + `1- p = 1)%R. +Proof. by rewrite /onem addrCA subrr addr0. Qed. + +Lemma onem_nonneg_proof (R : numDomainType) (p : {nonneg R}) : + (p%:num <= 1 -> 0 <= `1-(p%:num))%R. +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). +(* /TODO: PR *) + +Section bernoulli. +Variables (R : realType) (p : {nonneg R}) (p1 : (p%:num <= 1)%R). +Local Open Scope ring_scope. + +Definition bernoulli : set _ -> \bar R := + measure_add + [the measure _ _ of mscale p [the measure _ _ of dirac true]] + [the measure _ _ of mscale (onem_nonneg p1) [the measure _ _ of dirac false]]. + +HB.instance Definition _ := Measure.on bernoulli. + +Local Close Scope ring_scope. + +Let bernoulli_setT : bernoulli [set: _] = 1. +Proof. +rewrite /bernoulli/= /measure_add/= /msum 2!big_ord_recr/= big_ord0 add0e/=. +by rewrite /mscale/= !diracT !mule1 -EFinD onem1'. +Qed. + +HB.instance Definition _ := @Measure_isProbability.Build _ _ R bernoulli bernoulli_setT. + +End bernoulli. + +Section mscore. +Context d (T : measurableType d) (R : realType). +Variable f : T -> R. + +Definition mscore t : {measure set _ -> \bar R} := + let p := NngNum (normr_ge0 (f t)) in + [the measure _ _ of mscale p [the measure _ _ of dirac tt]]. + +Lemma mscoreE t U : mscore t U = if U == set0 then 0 else `| (f t)%:E |. +Proof. +rewrite /mscore/= /mscale/=; have [->|->] := set_unit U. + by rewrite eqxx dirac0 mule0. +by rewrite diracT mule1 (negbTE setT0). +Qed. + +Lemma measurable_fun_mscore U : measurable_fun setT f -> + measurable_fun setT (mscore ^~ U). +Proof. +move=> mr; under eq_fun do rewrite mscoreE/=. +have [U0|U0] := eqVneq U set0; first exact: measurable_fun_cst. +by apply: measurable_funT_comp => //; exact: measurable_funT_comp. +Qed. + +End mscore. + +(* decomposition of score into finite kernels *) +Module SCORE. +Section score. +Context d (T : measurableType d) (R : realType). +Variable f : T -> R. + +Definition k (mf : measurable_fun setT f) i t U := + if i%:R%:E <= mscore f t U < i.+1%:R%:E then + mscore f t U + else + 0. + +Hypothesis mf : measurable_fun setT f. + +Lemma k0 i t : k mf i t (set0 : set unit) = 0 :> \bar R. +Proof. by rewrite /k measure0; case: ifP. Qed. + +Lemma k_ge0 i t B : 0 <= k mf i t B. +Proof. by rewrite /k; case: ifP. Qed. + +Lemma k_sigma_additive i t : semi_sigma_additive (k mf i t). +Proof. +move=> /= F mF tF mUF; rewrite /k /=. +have [F0|UF0] := eqVneq (\bigcup_n F n) set0. + rewrite F0 measure0 (_ : (fun _ => _) = cst 0). + by case: ifPn => _; exact: cvg_cst. + apply/funext => k; rewrite big1// => n _. + by move: F0 => /bigcup0P -> //; rewrite measure0; case: ifPn. +move: (UF0) => /eqP/bigcup0P/existsNP[m /not_implyP[_ /eqP Fm0]]. +rewrite [in X in _ --> X]mscoreE (negbTE UF0). +rewrite -(cvg_shiftn m.+1)/=. +case: ifPn => ir. + rewrite (_ : (fun _ => _) = cst `|(f t)%:E|); first exact: cvg_cst. + apply/funext => n. + rewrite big_mkord (bigD1 (widen_ord (leq_addl n _) (Ordinal (ltnSn m))))//=. + rewrite [in X in X + _]mscoreE (negbTE Fm0) ir big1 ?adde0// => /= j jk. + rewrite mscoreE; have /eqP -> : F j == set0. + have [/eqP//|Fjtt] := set_unit (F j). + move/trivIsetP : tF => /(_ j m Logic.I Logic.I jk). + by rewrite Fjtt setTI => /eqP; rewrite (negbTE Fm0). + by rewrite eqxx; case: ifP. +rewrite (_ : (fun _ => _) = cst 0); first exact: cvg_cst. +apply/funext => n. +rewrite big_mkord (bigD1 (widen_ord (leq_addl n _) (Ordinal (ltnSn m))))//=. +rewrite [in X in if X then _ else _]mscoreE (negbTE Fm0) (negbTE ir) add0e. +rewrite big1//= => j jm; rewrite mscoreE; have /eqP -> : F j == set0. + have [/eqP//|Fjtt] := set_unit (F j). + move/trivIsetP : tF => /(_ j m Logic.I Logic.I jm). + by rewrite Fjtt setTI => /eqP; rewrite (negbTE Fm0). +by rewrite eqxx; case: ifP. +Qed. + +HB.instance Definition _ i t := isMeasure.Build _ _ _ + (k mf i t) (k0 i t) (k_ge0 i t) (@k_sigma_additive i t). + +Lemma measurable_fun_k i U : measurable U -> measurable_fun setT (k mf i ^~ U). +Proof. +move=> /= mU; rewrite /k /= (_ : (fun x => _) = + (fun x => if i%:R%:E <= x < i.+1%:R%:E then x else 0) \o (mscore f ^~ U)) //. +apply: measurable_funT_comp => /=; last exact/measurable_fun_mscore. +rewrite (_ : (fun x => _) = (fun x => x * + (\1_(`[i%:R%:E, i.+1%:R%:E [%classic : set _) x)%:E)); last first. + apply/funext => x; case: ifPn => ix; first by rewrite indicE/= mem_set ?mule1. + by rewrite indicE/= memNset ?mule0// /= in_itv/=; exact/negP. +apply: emeasurable_funM => /=; first exact: measurable_fun_id. +apply/EFin_measurable_fun. +by rewrite (_ : \1__ = mindic R (emeasurable_itv `[(i%:R)%:E, (i.+1%:R)%:E[)). +Qed. + +Definition mk i t := [the measure _ _ of k mf i t]. + +HB.instance Definition _ i := + isKernel.Build _ _ _ _ _ (mk i) (measurable_fun_k i). + +Lemma mk_uub i : measure_fam_uub (mk i). +Proof. +exists i.+1%:R => /= t; rewrite /k mscoreE setT_unit. +by case: ifPn => //; case: ifPn => // _ /andP[]. +Qed. + +HB.instance Definition _ i := + Kernel_isFinite.Build _ _ _ _ _ (mk i) (mk_uub i). + +End score. +End SCORE. + +Section kscore. +Context d (T : measurableType d) (R : realType). +Variable f : T -> R. + +Definition kscore (mf : measurable_fun setT f) + : T -> {measure set _ -> \bar R} := + mscore f. + +Variable mf : measurable_fun setT f. + +Let measurable_fun_kscore U : measurable U -> + measurable_fun setT (kscore mf ^~ U). +Proof. by move=> /= _; exact: measurable_fun_mscore. Qed. + +HB.instance Definition _ := isKernel.Build _ _ T _ R + (kscore mf) measurable_fun_kscore. + +Import SCORE. + +Let sfinite_kscore : exists k : (R.-fker T ~> _)^nat, + forall x U, measurable U -> + kscore mf x U = mseries (k ^~ x) 0 U. +Proof. +rewrite /=; exists (fun i => [the R.-fker _ ~> _ of mk mf i]) => /= t U mU. +rewrite /mseries /kscore/= mscoreE; case: ifPn => [/eqP U0|U0]. + by apply/esym/eseries0 => i _; rewrite U0 measure0. +rewrite /mk /= /k /= mscoreE (negbTE U0). +apply/esym/cvg_lim => //. +rewrite -(cvg_shiftn `|floor (fine `|(f t)%:E|)|%N.+1)/=. +rewrite (_ : (fun _ => _) = cst `|(f t)%:E|); first exact: cvg_cst. +apply/funext => n. +pose floor_f := widen_ord (leq_addl n `|floor `|f t| |.+1) + (Ordinal (ltnSn `|floor `|f t| |)). +rewrite big_mkord (bigD1 floor_f)//= ifT; last first. + rewrite lee_fin lte_fin; apply/andP; split. + by rewrite natr_absz (@ger0_norm _ (floor `|f t|)) ?floor_ge0 ?floor_le. + rewrite -addn1 natrD natr_absz. + by rewrite (@ger0_norm _ (floor `|f t|)) ?floor_ge0 ?lt_succ_floor. +rewrite big1 ?adde0//= => j jk. +rewrite ifF// lte_fin lee_fin. +move: jk; rewrite neq_ltn/= => /orP[|] jr. +- suff : (j.+1%:R <= `|f t|)%R by rewrite leNgt => /negbTE ->; rewrite andbF. + rewrite (_ : j.+1%:R = j.+1%:~R)// floor_ge_int. + move: jr; rewrite -lez_nat => /le_trans; apply. + by rewrite -[leRHS](@ger0_norm _ (floor `|f t|)) ?floor_ge0. +- suff : (`|f t| < j%:R)%R by rewrite ltNge => /negbTE ->. + move: jr; rewrite -ltz_nat -(@ltr_int R) (@gez0_abs (floor `|f t|)) ?floor_ge0//. + by rewrite ltr_int -floor_lt_int. +Qed. + +HB.instance Definition _ := + @Kernel_isSFinite.Build _ _ _ _ _ (kscore mf) sfinite_kscore. + +End kscore. + +(* decomposition of ite into s-finite kernels *) +Module ITE. +Section ite. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). + +Section kiteT. +Variable k : R.-ker X ~> Y. + +Definition kiteT : X * bool -> {measure set Y -> \bar R} := + fun xb => if xb.2 then k xb.1 else [the measure _ _ of mzero]. + +Let measurable_fun_kiteT U : measurable U -> measurable_fun setT (kiteT ^~ U). +Proof. +move=> /= mcU; rewrite /kiteT. +rewrite (_ : (fun _ => _) = + (fun x => if x.2 then k x.1 U else mzero U)); last first. + by apply/funext => -[t b]/=; case: ifPn. +apply: (@measurable_fun_if_pair _ _ _ _ (k ^~ U) (fun=> mzero U)). + exact/measurable_kernel. +exact: measurable_fun_cst. +Qed. + +#[export] +HB.instance Definition _ := isKernel.Build _ _ _ _ _ + kiteT measurable_fun_kiteT. +End kiteT. + +Section sfkiteT. +Variable k : R.-sfker X ~> Y. + +Let sfinite_kiteT : exists2 k_ : (R.-ker _ ~> _)^nat, + forall n, measure_fam_uub (k_ n) & + forall x U, measurable U -> kiteT k x U = mseries (k_ ^~ x) 0 U. +Proof. +have [k_ hk /=] := sfinite k. +exists (fun n => [the _.-ker _ ~> _ of kiteT (k_ n)]) => /=. + move=> n; have /measure_fam_uubP[r k_r] := measure_uub (k_ n). + by exists r%:num => /= -[x []]; rewrite /kiteT//= /mzero//. +move=> [x b] U mU; rewrite /kiteT; case: ifPn => hb; first by rewrite hk. +by rewrite /mseries eseries0. +Qed. + +#[export] +HB.instance Definition _ t := @Kernel_isSFinite_subdef.Build _ _ _ _ _ + (kiteT k) sfinite_kiteT. +End sfkiteT. + +Section fkiteT. +Variable k : R.-fker X ~> Y. + +Let kiteT_uub : measure_fam_uub (kiteT k). +Proof. +have /measure_fam_uubP[M hM] := measure_uub k. +exists M%:num => /= -[]; rewrite /kiteT => t [|]/=; first exact: hM. +by rewrite /= /mzero. +Qed. + +#[export] +HB.instance Definition _ t := Kernel_isFinite.Build _ _ _ _ _ + (kiteT k) kiteT_uub. +End fkiteT. + +Section kiteF. +Variable k : R.-ker X ~> Y. + +Definition kiteF : X * bool -> {measure set Y -> \bar R} := + fun xb => if ~~ xb.2 then k xb.1 else [the measure _ _ of mzero]. + +Let measurable_fun_kiteF U : measurable U -> measurable_fun setT (kiteF ^~ U). +Proof. +move=> /= mcU; rewrite /kiteF. +rewrite (_ : (fun x => _) = + (fun x => if x.2 then mzero U else k x.1 U)); last first. + by apply/funext => -[t b]/=; rewrite if_neg//; case: ifPn. +apply: (@measurable_fun_if_pair _ _ _ _ (fun=> mzero U) (k ^~ U)). + exact: measurable_fun_cst. +exact/measurable_kernel. +Qed. + +#[export] +HB.instance Definition _ := isKernel.Build _ _ _ _ _ + kiteF measurable_fun_kiteF. + +End kiteF. + +Section sfkiteF. +Variable k : R.-sfker X ~> Y. + +Let sfinite_kiteF : exists2 k_ : (R.-ker _ ~> _)^nat, + forall n, measure_fam_uub (k_ n) & + forall x U, measurable U -> kiteF k x U = mseries (k_ ^~ x) 0 U. +Proof. +have [k_ hk /=] := sfinite k. +exists (fun n => [the _.-ker _ ~> _ of kiteF (k_ n)]) => /=. + move=> n; have /measure_fam_uubP[r k_r] := measure_uub (k_ n). + by exists r%:num => /= -[x []]; rewrite /kiteF//= /mzero//. +move=> [x b] U mU; rewrite /kiteF; case: ifPn => hb; first by rewrite hk. +by rewrite /mseries eseries0. +Qed. + +#[export] +HB.instance Definition _ := @Kernel_isSFinite_subdef.Build _ _ _ _ _ + (kiteF k) sfinite_kiteF. + +End sfkiteF. + +Section fkiteF. +Variable k : R.-fker X ~> Y. + +Let kiteF_uub : measure_fam_uub (kiteF k). +Proof. +have /measure_fam_uubP[M hM] := measure_uub k. +by exists M%:num => /= -[]; rewrite /kiteF/= => t; case => //=; rewrite /mzero. +Qed. + +#[export] +HB.instance Definition _ := Kernel_isFinite.Build _ _ _ _ _ + (kiteF k) kiteF_uub. + +End fkiteF. +End ite. +End ITE. + +Section ite. +Context d d' (T : measurableType d) (T' : measurableType d') (R : realType). +Variables (f : T -> bool) (u1 u2 : R.-sfker T ~> T'). + +Definition mite (mf : measurable_fun setT f) : T -> set T' -> \bar R := + fun t => if f t then u1 t else u2 t. + +Variables mf : measurable_fun setT f. + +Let mite0 t : mite mf t set0 = 0. +Proof. by rewrite /mite; case: ifPn. Qed. + +Let mite_ge0 t U : 0 <= mite mf t U. +Proof. by rewrite /mite; case: ifPn. Qed. + +Let mite_sigma_additive t : semi_sigma_additive (mite mf t). +Proof. +by rewrite /mite; case: ifPn => ft; exact: measure_semi_sigma_additive. +Qed. + +HB.instance Definition _ t := isMeasure.Build _ _ _ (mite mf t) + (mite0 t) (mite_ge0 t) (@mite_sigma_additive t). + +Import ITE. + +(* +Definition kite : R.-sfker T ~> T' := + kdirac mf \; kadd (kiteT u1) (kiteF u2). +*) +Definition kite := + [the R.-sfker _ ~> _ of kdirac mf] \; + [the R.-sfker _ ~> _ of kadd + [the R.-sfker _ ~> T' of kiteT u1] + [the R.-sfker _ ~> T' of kiteF u2] ]. + +End ite. + +Section insn2. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). + +Definition ret (f : X -> Y) (mf : measurable_fun setT f) + : 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)]. + +Definition normalize (k : R.-sfker X ~> Y) P : X -> probability Y R := + fun x => [the probability _ _ of mnormalize k P x]. + +Definition ite (f : X -> bool) (mf : measurable_fun setT f) + (k1 k2 : R.-sfker X ~> Y) : R.-sfker X ~> Y := + locked [the R.-sfker X ~> Y of kite k1 k2 mf]. + +End insn2. +Arguments ret {d d' X Y R f} mf. +Arguments sample {d d' X Y R}. + +Section insn2_lemmas. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). + +Lemma retE (f : X -> Y) (mf : measurable_fun setT f) x : + ret mf x = \d_(f x) :> (_ -> \bar R). +Proof. by []. Qed. + +Lemma sampleE (P : probability Y R) (x : X) : sample P x = P. +Proof. by []. Qed. + +Lemma normalizeE (f : R.-sfker X ~> Y) P x U : + normalize f P x U = + if (f x [set: Y] == 0) || (f x [set: Y] == +oo) then P U + else f x U * ((fine (f x [set: Y]))^-1)%:E. +Proof. by rewrite /normalize /= /mnormalize; case: ifPn. Qed. + +Lemma iteE (f : X -> bool) (mf : measurable_fun setT f) + (k1 k2 : R.-sfker X ~> Y) x : + ite mf k1 k2 x = if f x then k1 x else k2 x. +Proof. +apply/eq_measure/funext => U. +rewrite /ite; unlock => /=. +rewrite /kcomp/= integral_dirac//=. +rewrite indicT mul1e. +rewrite -/(measure_add (ITE.kiteT k1 (x, f x)) (ITE.kiteF k2 (x, f x))). +rewrite measure_addE. +rewrite /ITE.kiteT /ITE.kiteF/=. +by case: ifPn => fx /=; rewrite /mzero ?(adde0,add0e). +Qed. + +End insn2_lemmas. + +Section insn3. +Context d d' d3 (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). + +Definition letin (l : R.-sfker X ~> Y) (k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z) + : R.-sfker X ~> Z := + [the R.-sfker X ~> Z of l \; k]. + +End insn3. + +Section insn3_lemmas. +Context d d' d3 (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). + +Lemma letinE (l : R.-sfker X ~> Y) (k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z) x U : + letin l k x U = \int[l x]_y k (x, y) U. +Proof. by []. Qed. + +End insn3_lemmas. + +(* rewriting laws *) +Section letin_return. +Context d d' d3 (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). + +Lemma letin_kret (k : R.-sfker X ~> Y) + (f : X * Y -> Z) (mf : measurable_fun setT f) x U : + measurable U -> + letin k (ret mf) x U = k x (curry f x @^-1` U). +Proof. +move=> mU; rewrite letinE. +under eq_integral do rewrite retE. +rewrite integral_indic ?setIT//. +move/measurable_fun_prod1 : mf => /(_ x measurableT U mU). +by rewrite setTI. +Qed. + +Lemma letin_retk + (f : X -> Y) (mf : measurable_fun setT f) + (k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z) + x U : measurable U -> + letin (ret mf) k x U = k (x, f x) U. +Proof. +move=> mU; rewrite letinE retE integral_dirac ?indicT ?mul1e//. +have /measurable_fun_prod1 := measurable_kernel k _ mU. +exact. +Qed. + +End letin_return. + +Section insn1. +Context d (X : measurableType d) (R : realType). + +Definition score (f : X -> R) (mf : measurable_fun setT f) + : R.-sfker X ~> _ := + [the R.-sfker X ~> _ of kscore mf]. + +End insn1. + +Section hard_constraint. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). + +Definition fail := + letin (score (@measurable_fun_cst _ _ X _ setT (0%R : R))) + (ret (@measurable_fun_cst _ _ _ Y setT point)). + +Lemma failE x U : fail x U = 0. +Proof. by rewrite /fail letinE ge0_integral_mscale//= normr0 mul0e. Qed. + +End hard_constraint. +Arguments fail {d d' X Y R}. + +Module Notations. + +Notation var1of2 := (@measurable_fun_fst _ _ _ _). +Notation var2of2 := (@measurable_fun_snd _ _ _ _). +Notation var1of3 := (measurable_funT_comp (@measurable_fun_fst _ _ _ _) + (@measurable_fun_fst _ _ _ _)). +Notation var2of3 := (measurable_funT_comp (@measurable_fun_snd _ _ _ _) + (@measurable_fun_fst _ _ _ _)). +Notation var3of3 := (@measurable_fun_snd _ _ _ _). + +Notation mR := Real_sort__canonical__measure_Measurable. +Notation munit := Datatypes_unit__canonical__measure_Measurable. +Notation mbool := Datatypes_bool__canonical__measure_Measurable. + +End Notations. + +Section cst_fun. +Context d (T : measurableType d) (R : realType). + +Definition kr (r : R) := @measurable_fun_cst _ _ T _ setT r. +Definition k3 : measurable_fun _ _ := kr 3%:R. +Definition k10 : measurable_fun _ _ := kr 10%:R. +Definition ktt := @measurable_fun_cst _ _ T _ setT tt. +Definition kb (b : bool) := @measurable_fun_cst _ _ T _ setT b. + +End cst_fun. +Arguments kr {d T R}. +Arguments k3 {d T R}. +Arguments k10 {d T R}. +Arguments ktt {d T}. +Arguments kb {d T}. + +Section insn1_lemmas. +Import Notations. +Context d (T : measurableType d) (R : realType). + +Let kcomp_scoreE d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) + (g : R.-sfker [the measurableType _ of (T1 * unit)%type] ~> T2) + f (mf : measurable_fun setT f) r U : + (score mf \; g) r U = `|f r|%:E * g (r, tt) U. +Proof. +rewrite /= /kcomp /kscore /= ge0_integral_mscale//=. +by rewrite integral_dirac// indicT mul1e. +Qed. + +Lemma scoreE d' (T' : measurableType d') (x : T * T') (U : set T') (f : R -> R) + (r : R) (r0 : (0 <= r)%R) + (f0 : (forall r, 0 <= r -> 0 <= f r)%R) (mf : measurable_fun setT f) : + score (measurable_funT_comp mf var2of2) + (x, r) (curry (snd \o fst) x @^-1` U) = + (f r)%:E * \d_x.2 U. +Proof. by rewrite /score/= /mscale/= ger0_norm// f0. Qed. + +Lemma score_score (f : R -> R) (g : R * unit -> R) + (mf : measurable_fun setT f) + (mg : measurable_fun setT g) : + letin (score mf) (score mg) = + score (measurable_funM mf (measurable_fun_prod2 tt mg)). +Proof. +apply/eq_sfkernel => x U. +rewrite {1}/letin; unlock. +by rewrite kcomp_scoreE/= /mscale/= diracE normrM muleA EFinM. +Qed. + +Import Notations. + +(* hard constraints to express score below 1 *) +Lemma score_fail (r : {nonneg R}) (r1 : (r%:num <= 1)%R) : + score (kr r%:num) = + letin (sample [the probability _ _ of bernoulli r1] : R.-pker T ~> _) + (ite var2of2 (ret ktt) fail). +Proof. +apply/eq_sfkernel => x U. +rewrite letinE/= /sample; unlock. +rewrite integral_measure_add//= ge0_integral_mscale//= ge0_integral_mscale//=. +rewrite integral_dirac//= integral_dirac//= !indicT/= !mul1e. +by rewrite /mscale/= iteE//= iteE//= failE mule0 adde0 ger0_norm. +Qed. + +End insn1_lemmas. + +Section letin_ite. +Context d d2 d3 (T : measurableType d) (T2 : measurableType d2) + (Z : measurableType d3) (R : realType). +Variables (k1 k2 : R.-sfker T ~> Z) (u : R.-sfker [the measurableType _ of (T * Z)%type] ~> T2) + (f : T -> bool) (mf : measurable_fun setT f) + (t : T) (U : set T2). + +Lemma letin_iteT : f t -> letin (ite mf k1 k2) u t U = letin k1 u t U. +Proof. +move=> ftT. +rewrite !letinE/=. +apply: eq_measure_integral => V mV _. +by rewrite iteE ftT. +Qed. + +Lemma letin_iteF : ~~ f t -> letin (ite mf k1 k2) u t U = letin k2 u t U. +Proof. +move=> ftF. +rewrite !letinE/=. +apply: eq_measure_integral => V mV _. +by rewrite iteE (negbTE ftF). +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). + +Import Notations. + +Variables (t : R.-sfker Z ~> X) + (t' : R.-sfker [the measurableType _ of (Z * Y)%type] ~> X) + (tt' : forall y, t =1 fun z => t' (z, y)) + (u : R.-sfker Z ~> Y) + (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 (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 (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' + (ret (measurable_fun_pair var2of3 var3of3))) z A = + letin u + (letin t' + (ret (measurable_fun_pair var3of3 var2of3))) z A. +Proof. +move=> mA. +rewrite !letinE. +under eq_integral. + move=> x _. + rewrite letinE -uu'. + under eq_integral do rewrite retE /=. + over. +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 => -[]. +rewrite /=. +apply: eq_integral => y _. +by rewrite letinE/= -tt'; apply: eq_integral => // x _; rewrite retE. +Qed. + +End letinC. + +(* sample programs *) + +Section constants. +Variable R : realType. +Local Open Scope ring_scope. + +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 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. + +Lemma p27 : (2 / 7%:R)%:nng%:num <= 1 :> R. +Proof. by rewrite /= lter_pdivr_mulr// mul1r ler_nat. Qed. + +End constants. +Arguments p12 {R}. +Arguments p14 {R}. +Arguments p27 {R}. + +Section poisson. +Variable R : realType. +Local Open Scope ring_scope. + +(* density function for Poisson *) +Definition poisson k r : R := r ^+ k / k`!%:R^-1 * expR (- r). + +Lemma poisson_ge0 k r : 0 <= r -> 0 <= poisson k r. +Proof. +move=> r0; rewrite /poisson mulr_ge0 ?expR_ge0//. +by rewrite mulr_ge0// exprn_ge0. +Qed. + +Lemma poisson_gt0 k r : 0 < r -> 0 < poisson k.+1 r. +Proof. +move=> r0; rewrite /poisson mulr_gt0 ?expR_gt0//. +by rewrite divr_gt0// ?exprn_gt0// invr_gt0 ltr0n fact_gt0. +Qed. + +Lemma mpoisson k : measurable_fun setT (poisson k). +Proof. +apply: measurable_funM => /=. + apply: measurable_funM => //=; last exact: measurable_fun_cst. + exact/measurable_fun_exprn/measurable_fun_id. +apply: measurable_funT_comp; last exact: measurable_fun_opp. +by apply: continuous_measurable_fun; exact: continuous_expR. +Qed. + +Definition poisson3 := poisson 4 3%:R. (* 0.168 *) +Definition poisson10 := poisson 4 10%:R. (* 0.019 *) + +End poisson. + +Section exponential. +Variable R : realType. +Local Open Scope ring_scope. + +(* density function for exponential *) +Definition exp_density x r : R := r * expR (- r * x). + +Lemma exp_density_gt0 x r : 0 < r -> 0 < exp_density x r. +Proof. by move=> r0; rewrite /exp_density mulr_gt0// expR_gt0. Qed. + +Lemma exp_density_ge0 x r : 0 <= r -> 0 <= exp_density x r. +Proof. by move=> r0; rewrite /exp_density mulr_ge0// expR_ge0. Qed. + +Lemma mexp_density x : measurable_fun setT (exp_density x). +Proof. +apply: measurable_funM => /=; first exact: measurable_fun_id. +apply: measurable_funT_comp. + by apply: continuous_measurable_fun; exact: continuous_expR. +apply: measurable_funM => /=; first exact: measurable_fun_opp. +exact: measurable_fun_cst. +Qed. + +End exponential. + +Lemma letin_sample_bernoulli d d' (T : measurableType d) + (T' : measurableType d') (R : realType)(r : {nonneg R}) (r1 : (r%:num <= 1)%R) + (u : R.-sfker [the measurableType _ of (T * bool)%type] ~> T') x y : + letin (sample [the probability _ _ of bernoulli r1]) u x y = + r%:num%:E * u (x, true) y + (`1- (r%:num))%:E * u (x, false) y. +Proof. +rewrite letinE/=. +rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=. +by rewrite !ge0_integral_mscale//= !integral_dirac//= indicT 2!mul1e. +Qed. + +Section sample_and_return. +Import Notations. +Context d (T : measurableType d) (R : realType). + +Definition sample_and_return : R.-sfker T ~> _ := + letin + (sample [the probability _ _ of bernoulli p27]) (* T -> B *) + (ret var2of2) (* T * B -> B *). + +Lemma sample_and_returnE t U : sample_and_return t U = + (2 / 7%:R)%:E * \d_true U + (5%:R / 7%:R)%:E * \d_false U. +Proof. +by rewrite /sample_and_return letin_sample_bernoulli !retE onem27. +Qed. + +End sample_and_return. + +(* trivial example *) +Section sample_and_branch. +Import Notations. +Context d (T : measurableType d) (R : realType). + +(* let x = sample (bernoulli (2/7)) in + let r = case x of {(1, _) => return (k3()), (2, _) => return (k10())} in + return r *) + +Definition sample_and_branch : R.-sfker T ~> mR R := + letin + (sample [the probability _ _ of bernoulli p27]) (* T -> B *) + (ite var2of2 (ret k3) (ret k10)). + +Lemma sample_and_branchE t U : sample_and_branch t U = + (2 / 7%:R)%:E * \d_(3%:R : R) U + + (5%:R / 7%:R)%:E * \d_(10%:R : R) U. +Proof. +by rewrite /sample_and_branch letin_sample_bernoulli/= !iteE !retE onem27. +Qed. + +End sample_and_branch. + +Section bernoulli_and. +Context d (T : measurableType d) (R : realType). +Import Notations. + +Definition mand (x y : T * mbool * mbool -> mbool) + (t : T * mbool * mbool) : mbool := x t && y t. + +Lemma measurable_fun_mand (x y : T * mbool * mbool -> mbool) : + measurable_fun setT x -> measurable_fun setT y -> + measurable_fun setT (mand x y). +Proof. +move=> /= mx my; apply: (@emeasurable_fun_bool _ _ _ _ true). +rewrite [X in measurable X](_ : _ = + (x @^-1` [set true]) `&` (y @^-1` [set true])); last first. + by rewrite /mand; apply/seteqP; split => z/= /andP. +apply: measurableI. +- by rewrite -[X in measurable X]setTI; exact: mx. +- by rewrite -[X in measurable X]setTI; exact: my. +Qed. + +Definition bernoulli_and : R.-sfker T ~> mbool := + (letin (sample [the probability _ _ of bernoulli p12]) + (letin (sample [the probability _ _ of bernoulli p12]) + (ret (measurable_fun_mand var2of3 var3of3)))). + +Lemma bernoulli_andE t U : + bernoulli_and t U = + sample [the probability _ _ of bernoulli p14] t U. +Proof. +rewrite /bernoulli_and 3!letin_sample_bernoulli/= /mand/= muleDr//= -muleDl//. +rewrite !muleA -addeA -muleDl// -!EFinM !onem1S/= -splitr mulr1. +have -> : (1 / 2 * (1 / 2) = 1 / 4 :> R)%R by rewrite mulf_div mulr1// -natrM. +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. +by rewrite onem1S// -mulrDl. +Qed. + +End bernoulli_and. + +Section staton_bus. +Import Notations. +Context d (T : measurableType d) (R : realType) (h : R -> R). +Hypothesis mh : measurable_fun setT h. +Definition kstaton_bus : R.-sfker T ~> mbool := + letin (sample [the probability _ _ of bernoulli p27]) + (letin + (letin (ite var2of2 (ret k3) (ret k10)) + (score (measurable_funT_comp mh var3of3))) + (ret var2of3)). + +Definition staton_bus := normalize kstaton_bus. + +End staton_bus. + +(* let x = sample (bernoulli (2/7)) in + let r = case x of {(1, _) => return (k3()), (2, _) => return (k10())} in + let _ = score (1/4! r^4 e^-r) in + return x *) +Section staton_bus_poisson. +Import Notations. +Context d (T : measurableType d) (R : realType). +Let poisson4 := @poisson R 4%N. +Let mpoisson4 := @mpoisson R 4%N. + +Definition kstaton_bus_poisson : R.-sfker (mR R) ~> mbool := + kstaton_bus _ mpoisson4. + +Let kstaton_bus_poissonE t U : kstaton_bus_poisson t U = + (2 / 7%:R)%:E * (poisson4 3%:R)%:E * \d_true U + + (5%:R / 7%:R)%:E * (poisson4 10%:R)%:E * \d_false U. +Proof. +rewrite /kstaton_bus. +rewrite letin_sample_bernoulli. +rewrite -!muleA; congr (_ * _ + _ * _). +- rewrite letin_kret//. + rewrite letin_iteT//. + rewrite letin_retk//. + by rewrite scoreE//= => r r0; exact: poisson_ge0. +- by rewrite onem27. + rewrite letin_kret//. + rewrite letin_iteF//. + rewrite letin_retk//. + by rewrite scoreE//= => r r0; exact: poisson_ge0. +Qed. + +(* true -> 2/7 * 0.168 = 2/7 * 3^4 e^-3 / 4! *) +(* false -> 5/7 * 0.019 = 5/7 * 10^4 e^-10 / 4! *) + +Lemma staton_busE P (t : R) U : + let N := ((2 / 7%:R) * poisson4 3%:R + + (5%:R / 7%:R) * poisson4 10%:R)%R in + staton_bus mpoisson4 P t U = + ((2 / 7%:R)%:E * (poisson4 3%:R)%:E * \d_true U + + (5%:R / 7%:R)%:E * (poisson4 10%:R)%:E * \d_false U) * N^-1%:E. +Proof. +rewrite /staton_bus normalizeE /= !kstaton_bus_poissonE !diracT !mule1 ifF //. +apply/negbTE; rewrite gt_eqF// lte_fin. +by rewrite addr_gt0// mulr_gt0//= ?divr_gt0// ?ltr0n// poisson_gt0// ltr0n. +Qed. + +End staton_bus_poisson. + +(* let x = sample (bernoulli (2/7)) in + let r = case x of {(1, _) => return (k3()), (2, _) => return (k10())} in + let _ = score (r e^-(15/60 r)) in + return x *) +Section staton_bus_exponential. +Import Notations. +Context d (T : measurableType d) (R : realType). +Let exp1560 := @exp_density R (ratr (15%:Q / 60%:Q)). +Let mexp1560 := @mexp_density R (ratr (15%:Q / 60%:Q)). + +(* 15/60 = 0.25 *) + +Definition kstaton_bus_exponential : R.-sfker (mR R) ~> mbool := + kstaton_bus _ mexp1560. + +Let kstaton_bus_exponentialE t U : kstaton_bus_exponential t U = + (2 / 7%:R)%:E * (exp1560 3%:R)%:E * \d_true U + + (5%:R / 7%:R)%:E * (exp1560 10%:R)%:E * \d_false U. +Proof. +rewrite /kstaton_bus. +rewrite letin_sample_bernoulli. +rewrite -!muleA; congr (_ * _ + _ * _). +- rewrite letin_kret//. + rewrite letin_iteT//. + rewrite letin_retk//. + rewrite scoreE//= => r r0; exact: exp_density_ge0. +- by rewrite onem27. + rewrite letin_kret//. + rewrite letin_iteF//. + rewrite letin_retk//. + by rewrite scoreE//= => r r0; exact: exp_density_ge0. +Qed. + +(* true -> 5/7 * 0.019 = 5/7 * 10^4 e^-10 / 4! *) +(* false -> 2/7 * 0.168 = 2/7 * 3^4 e^-3 / 4! *) + +Lemma staton_bus_exponentialE P (t : R) U : + let N := ((2 / 7%:R) * exp1560 3%:R + + (5%:R / 7%:R) * exp1560 10%:R)%R in + staton_bus mexp1560 P t U = + ((2 / 7%:R)%:E * (exp1560 3%:R)%:E * \d_true U + + (5%:R / 7%:R)%:E * (exp1560 10%:R)%:E * \d_false U) * N^-1%:E. +Proof. +rewrite /staton_bus. +rewrite normalizeE /= !kstaton_bus_exponentialE !diracT !mule1 ifF //. +apply/negbTE; rewrite gt_eqF// lte_fin. +by rewrite addr_gt0// mulr_gt0//= ?divr_gt0// ?ltr0n// exp_density_gt0 ?ltr0n. +Qed. + +End staton_bus_exponential. + + +Notation var1of3' := (@measurable_fun_fst _ _ _ _). +Notation var2of3' := (measurable_funT_comp (@measurable_fun_fst _ _ _ _) (@measurable_fun_snd _ _ _ _)). +Notation var3of3' := (measurable_funT_comp (@measurable_fun_fst _ _ _ _) (measurable_funT_comp (@measurable_fun_snd _ _ _ _) (@measurable_fun_snd _ _ _ _))). + +Notation var1of4' := (@measurable_fun_fst _ _ _ _). +Notation var2of4' := (measurable_funT_comp (@measurable_fun_fst _ _ _ _) (@measurable_fun_snd _ _ _ _)). +Notation var3of4' := (measurable_funT_comp (@measurable_fun_fst _ _ _ _) (measurable_funT_comp (@measurable_fun_snd _ _ _ _) (@measurable_fun_snd _ _ _ _))). +Notation var4of4' := (measurable_funT_comp (@measurable_fun_fst _ _ _ _) (measurable_funT_comp (@measurable_fun_snd _ _ _ _) (measurable_funT_comp (@measurable_fun_snd _ _ _ _) (@measurable_fun_snd _ _ _ _)))). + +Section mswap. +Variables (d d' d3 : _) (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). +Variable k : R.-ker [the measurableType _ of (Y * X)%type] ~> Z. + +Definition mswap xy U := k (swap xy) U. + +Let mswap0 xy : mswap xy set0 = 0. +Proof. done. Qed. + +Let mswap_ge0 x U : 0 <= mswap x U. +Proof. done. Qed. + +Let mswap_sigma_additive x : semi_sigma_additive (mswap x). +Proof. exact: measure_semi_sigma_additive. Qed. + +HB.instance Definition _ x := isMeasure.Build _ R _ + (mswap x) (mswap0 x) (mswap_ge0 x) (@mswap_sigma_additive x). + +Definition mkswap : _ -> {measure set Z -> \bar R} := + fun x => [the measure _ _ of mswap x]. + +Let measurable_fun_kswap U : + measurable U -> measurable_fun setT (mkswap ^~ U). +Proof. +move=> mU. +rewrite [X in measurable_fun _ X](_ : _ = ((fun xy => k xy U) \o (@swap _ _)))//. +apply measurable_funT_comp. + exact/measurable_kernel. +exact: measurable_fun_swap. +Qed. + +HB.instance Definition _ := + isKernel.Build _ _ [the measurableType _ of (X * Y)%type] Z R mkswap measurable_fun_kswap. + +End mswap. + +Section mswap_sfinite_kernel. +Variables (d d' d3 : _) (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). +Variable k : R.-sfker [the measurableType _ of (Y * X)%type] ~> Z. + +(* Import KSWAP_FINITE_KERNEL. *) + +Let mkswap_sfinite : + exists2 k_ : (R.-ker [the measurableType _ of (X * Y)%type] ~> Z)^nat, + forall n, measure_fam_uub (k_ n) & + forall x U, measurable U -> mkswap k x U = kseries k_ x U. +Proof. +have [k_ /= kE] := sfinite k. +exists (fun n => [the R.-ker _ ~> _ of mkswap (k_ n)]). + move=> n. + have /measure_fam_uubP[M hM] := measure_uub (k_ n). + by exists M%:num => x/=; exact: hM. +move=> xy U mU. +by rewrite /mswap/= kE. +Qed. + +HB.instance Definition _ := + Kernel_isSFinite_subdef.Build _ _ _ Z R (mkswap k) mkswap_sfinite. + +End mswap_sfinite_kernel. + +(* Module KSWAP_FINITE_KERNEL. *) + +Section kswap_finite_kernel_finite. +Context d d' d3 (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType) + (k : R.-fker [the measurableType _ of (Y * X)%type] ~> Z). + +Let mkswap_finite : measure_fam_uub (mkswap k). +Proof. +have /measure_fam_uubP[r hr] := measure_uub k. +apply/measure_fam_uubP; exists (PosNum [gt0 of r%:num%R]) => x /=. +exact: hr. +Qed. + +HB.instance Definition _ := + Kernel_isFinite.Build _ _ _ Z R (mkswap k) mkswap_finite. + +End kswap_finite_kernel_finite. +(* End KSWAP_FINITE_KERNEL. *) + +(* Module MSWAP_SFINITE_KERNEL. *) + +Reserved Notation "f .; g" (at level 60, right associativity, + format "f .; '/ ' g"). + +Notation "l .; k" := (mkcomp l [the _.-ker _ ~> _ of mkswap k]) : ereal_scope. + +(* TODO: move to kernel.v *) + +Section letin'. +Variables (d d' d3 : _) (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). + +Definition letin' (l : R.-sfker X ~> Y) + (k : R.-sfker [the measurableType (d', d).-prod of (Y * X)%type] ~> Z) := + locked [the R.-sfker X ~> Z of l .; k]. + +Lemma letin'E (l : R.-sfker X ~> Y) + (k : R.-sfker [the measurableType (d', d).-prod of (Y * X)%type] ~> Z) x U : + letin' l k x U = \int[l x]_y k (y, x) U. +Proof. by rewrite /letin'; unlock. Qed. + +End letin'. + +Section letin'C. +Context d d1 d' (X : measurableType d) (Y : measurableType d1) + (Z : measurableType d') (R : realType). + +Import Notations. + +Variables (t : R.-sfker Z ~> X) + (t' : R.-sfker [the measurableType _ of (Y * Z)%type] ~> X) + (tt' : forall y, t =1 fun z => t' (y, z)) + (u : R.-sfker Z ~> Y) + (u' : R.-sfker [the measurableType _ of (X * Z)%type] ~> Y) + (uu' : forall x, u =1 fun z => u' (x, z)). + +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 (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 (U' z). Proof. exact: sfinite_kernel_measure. Qed. +HB.instance Definition _ z := @Measure_isSFinite_subdef.Build _ Y R + (U' z) (sfinU z). + +Lemma letin'C z A : measurable A -> + letin' t + (letin' u' + (ret (measurable_fun_pair var2of3' var1of3'))) z A = + letin' u + (letin' t' + (ret (measurable_fun_pair var1of3' var2of3'))) z A. +Proof. +move=> mA. +rewrite !letin'E. +under eq_integral. + move=> x _. + rewrite letin'E -uu'. + under eq_integral do rewrite retE /=. + over. +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 => -[]. +rewrite /=. +apply: eq_integral => y _. +by rewrite letin'E/= -tt'; apply: eq_integral => // x _; rewrite retE. +Qed. + +End letin'C. diff --git a/theories/sample.v b/theories/sample.v new file mode 100644 index 0000000000..a01ad27fa9 --- /dev/null +++ b/theories/sample.v @@ -0,0 +1,59 @@ + +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +Require Import reals ereal classical_sets numfun. +Require Import measure kernel lebesgue_integral signed. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. + +Section sample. +Variables (R : realType) (d : measure_display) (T : measurableType d). + +Lemma __ : true \in [set true]. +rewrite inE //. +Qed. + +Lemma _k x (s : set T) : kernel_from_dirac x s = dirac x s :> \bar R. +Proof. by []. Qed. + +Check kernel_from_dirac : T -> measure R T. (* T ^^> T *) + +Lemma _k1 : kernel_from_dirac true [set true] = 1 :> \bar R. +Proof. rewrite /= diracE __ //. Qed. + +Lemma _k2 : kernel_from_dirac false [set: bool] = 1 :> \bar R. +Proof. rewrite /= diracE in_setT //. Qed. + +(* bernoulli *) +Check bernoulli27 R : measure _ _. +Check sample_bernoulli27 R : kernel R _ _. + +Lemma _k3 : sample_bernoulli27 R tt set0 = 0. +Proof. by rewrite measure0. Qed. + +Lemma _k4 (s : set bool) : sample_bernoulli27 R tt s = bernoulli27 R s. +Proof. by []. Qed. + +(* star *) +Check Return R : kernel R _ _. + +Lemma _s (b : bool) : + star (Return R) (sample_bernoulli27 R) tt [set (tt, b)] = + bernoulli27 R [set b]. +Proof. +rewrite /star /=. +rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=. +rewrite !ge0_integral_mscale//=. +rewrite !integral_dirac//=. +rewrite 2!indicE 2!in_setT 2!mul1e. +rewrite /msum 2!big_ord_recl/= big_ord0 adde0/= /mscale /=. +admit. +Abort. + + +End sample. diff --git a/theories/semantics.v b/theories/semantics.v new file mode 100644 index 0000000000..a3ab19e3ae --- /dev/null +++ b/theories/semantics.v @@ -0,0 +1,89 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +Require Import mathcomp_extra boolp classical_sets signed functions cardinality. +Require Import reals ereal topology normedtype sequences esum measure. +Require Import lebesgue_measure fsbigop numfun lebesgue_integral kernel. + + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. + +Definition onem (R : numDomainType) (p : R) := (1 - p)%R. + +Lemma onem1 (R : numDomainType) (p : R) : (p + onem p = 1)%R. +Proof. by rewrite /onem addrCA subrr addr0. Qed. + +Lemma onem_nonneg_proof (R : numDomainType) (p : {nonneg R}) (p1 : (p%:num <= 1)%R) : + (0 <= onem p%:num)%R. +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). + +Section bernoulli. +Variables (R : realType) (p : {nonneg R}) (p1 : (p%:num <= 1)%R). +Local Open Scope ring_scope. + +Definition bernoulli : set _ -> \bar R := + measure_add + [the measure _ _ of mscale p [the measure _ _ of dirac true]] + [the measure _ _ of mscale (onem_nonneg p1) [the measure _ _ of dirac false]]. + +HB.instance Definition _ := Measure.on bernoulli. + +Example bernoulli_set0 : bernoulli set0 = 0%:E. +Proof. by []. Qed. +Example bernoulli_setT : bernoulli setT = 1%:E. +Proof. +rewrite /bernoulli/= /measure_add/= /msum 2!big_ord_recr/= big_ord0 add0e/=. +by rewrite /mscale/= !diracE !in_setT !mule1 -EFinD onem1. +Qed. + +HB.instance Definition _ := @isProbability.Build _ _ R bernoulli bernoulli_setT. + +End bernoulli. + +Section score. +Variables (R : realType) (d : _) (T : measurableType d). +Variables (r : T -> R). + +Definition score (t : T) (U : set unit) : \bar R := + if U == set0 then 0 else `| (r t)%:E |. + +Let score0 t : score t (set0 : set unit) = 0 :> \bar R. +Proof. by rewrite /score eqxx. Qed. + +Let score_ge0 t U : 0 <= score t U. +Proof. by rewrite /score; case: ifP. Qed. + +Let score_sigma_additive t : semi_sigma_additive (score t). +Proof. +move=> /= F mF tF mUF; rewrite /score; case: ifPn => [/eqP/bigcup0P F0|]. + rewrite (_ : (fun _ => _) = cst 0); first exact: cvg_cst. + apply/funext => k. + under eq_bigr do rewrite F0// eqxx. + by rewrite big1. +move=> /eqP/bigcup0P/existsNP[k /not_implyP[_ /eqP Fk0]]. +rewrite -(cvg_shiftn k.+1)/=. +rewrite (_ : (fun _ => _) = cst `|(r t)%:E|); first exact: cvg_cst. +apply/funext => n. +rewrite big_mkord (bigD1 (widen_ord (leq_addl n _) (Ordinal (ltnSn k))))//=. +rewrite (negbTE Fk0) big1 ?adde0// => i/= ik; rewrite ifT//. +have [/eqP//|Fitt] := set_unit (F i). +move/trivIsetP : tF => /(_ i k Logic.I Logic.I ik). +by rewrite Fitt setTI => /eqP; rewrite (negbTE Fk0). +Qed. + +HB.instance Definition _ (t : T) := isMeasure.Build _ _ _ + (score t) (score0 t) (score_ge0 t) (@score_sigma_additive t). + +Definition k_ (i : nat) + +End score. \ No newline at end of file diff --git a/theories/wip.v b/theories/wip.v new file mode 100644 index 0000000000..a2820ea8f8 --- /dev/null +++ b/theories/wip.v @@ -0,0 +1,149 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import rat. +Require Import mathcomp_extra boolp classical_sets signed functions cardinality. +Require Import reals ereal topology normedtype sequences esum measure. +Require Import lebesgue_measure fsbigop numfun lebesgue_integral exp kernel. +Require Import trigo prob_lang. + +(******************************************************************************) +(* Semantics of a probabilistic programming language using s-finite kernels *) +(* (wip) *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.ExtraDef Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. + +Section gauss. +Variable R : realType. +Local Open Scope ring_scope. + +(* density function for gauss *) +Definition gauss_density m s x : R := + (s * sqrtr (pi *+ 2))^-1 * expR (- ((x - m) / s) ^+ 2 / 2%:R). + +Lemma gauss_density_ge0 m s x : 0 <= s -> 0 <= gauss_density m s x. +Proof. by move=> s0; rewrite mulr_ge0 ?expR_ge0// invr_ge0 mulr_ge0. Qed. + +Lemma gauss_density_gt0 m s x : 0 < s -> 0 < gauss_density m s x. +Proof. +move=> s0; rewrite mulr_gt0 ?expR_gt0// invr_gt0 mulr_gt0//. +by rewrite sqrtr_gt0 pmulrn_rgt0// pi_gt0. +Qed. + +Definition gauss01_density : R -> R := gauss_density 0 1. + +Lemma gauss01_densityE x : + gauss01_density x = (sqrtr (pi *+ 2))^-1 * expR (- (x ^+ 2) / 2%:R). +Proof. by rewrite /gauss01_density /gauss_density mul1r subr0 divr1. Qed. + +Definition mgauss01 (V : set R) := + (\int[lebesgue_measure]_(x in V) (gauss01_density x)%:E)%E. + +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_funT_comp => /=. + by apply: continuous_measurable_fun; apply continuous_expR. +apply: measurable_funM; last exact: measurable_fun_cst. +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. +exact: measurable_fun_cst. +Qed. + +Let mgauss010 : mgauss01 set0 = 0%E. +Proof. by rewrite /mgauss01 integral_set0. Qed. + +Let mgauss01_ge0 A : (0 <= mgauss01 A)%E. +Proof. +by rewrite /mgauss01 integral_ge0//= => x _; rewrite lee_fin gauss_density_ge0. +Qed. + +Axiom integral_gauss01_density : + (\int[lebesgue_measure]_x (gauss01_density x)%:E = 1%E)%E. + +Let mgauss01_sigma_additive : semi_sigma_additive mgauss01. +Proof. +move=> /= F mF tF mUF. +rewrite /mgauss01/= integral_bigcup//=; last first. + split. + apply/EFin_measurable_fun. + exact: measurable_funS (measurable_fun_gauss_density 0 1). + rewrite (_ : (fun x => _) = (EFin \o gauss01_density)); last first. + by apply/funext => x; rewrite gee0_abs// lee_fin gauss_density_ge0. + apply: le_lt_trans. + apply: (@subset_integral _ _ _ _ _ setT) => //=. + apply/EFin_measurable_fun. + exact: measurable_fun_gauss_density. + by move=> ? _; rewrite lee_fin gauss_density_ge0. + by rewrite integral_gauss01_density// ltey. +apply: is_cvg_ereal_nneg_natsum_cond => n _ _. +by apply: integral_ge0 => /= x ?; rewrite lee_fin gauss_density_ge0. +Qed. + +HB.instance Definition _ := isMeasure.Build _ _ _ + mgauss01 mgauss010 mgauss01_ge0 mgauss01_sigma_additive. + +Let mgauss01_setT : mgauss01 [set: _] = 1%E. +Proof. by rewrite /mgauss01 integral_gauss01_density. Qed. + +HB.instance Definition _ := @Measure_isProbability.Build _ _ R mgauss01 mgauss01_setT. + +Definition gauss01 := [the probability _ _ of mgauss01]. + +End gauss. + +Section gauss_lebesgue. +Import Notations. +Context d (T : measurableType d) (R : realType). + +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])) => //. +- exact: open_measurable. +- by move=> /= r [t _ <-]; rewrite gt_eqF// gauss_density_gt0. +- apply: open_continuous_measurable_fun => //. + by apply/in_setP => x /= x0; exact: inv_continuous. +- exact: measurable_fun_gauss_density. +Qed. + +Variable mu : {measure set mR R -> \bar R}. + +Definition staton_lebesgue : R.-sfker T ~> _ := + letin (sample (@gauss01 R : pprobability _ _)) + (letin + (score (measurable_funT_comp mf1 var2of2)) + (ret var2of3)). + +Lemma staton_lebesgueE x U : measurable U -> + staton_lebesgue x U = lebesgue_measure U. +Proof. +move=> mU; rewrite [in LHS]/staton_lebesgue/=. +rewrite [in LHS]letinE /=. +transitivity (\int[@mgauss01 R]_(y in U) (f1 y)%:E). + rewrite -[in RHS](setTI U) integral_setI_indic//=. + apply: eq_integral => /= r _. + rewrite letinE/= ge0_integral_mscale//= ger0_norm//; last first. + by rewrite invr_ge0// gauss_density_ge0. + by rewrite integral_dirac// indicT mul1e diracE indicE. +transitivity (\int[lebesgue_measure]_(x in U) (gauss01_density x * f1 x)%:E). + admit. +transitivity (\int[lebesgue_measure]_(x in U) (\1_U x)%:E). + apply: eq_integral => /= y yU. + by rewrite /f1 divrr ?indicE ?yU// unitfE gt_eqF// gauss_density_gt0. +by rewrite integral_indic//= setIid. +Abort. + +End gauss_lebesgue.