Library mathcomp.analysis.kernel
(* 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 mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop.
Require Import reals ereal signed topology normedtype sequences esum measure.
Require Import numfun lebesgue_measure lebesgue_integral.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop.
Require Import reals ereal signed topology normedtype sequences esum measure.
Require Import numfun lebesgue_measure lebesgue_integral.
Kernels
This file provides a formation of kernels, s-finite kernels, finite
kernels, subprobability kernels, and probability kernels. The main
formalized result is the fact that s-finite kernels are stable by
composition.
R.-ker X ~> Y == kernel from X to Y where X and Y are of type
measurableType
The HB class is Kernel.
measure_fam_uub k == the kernel k is uniformly upper-bounded
R.-sfker X ~> Y == s-finite kernel
The HB class is SFiniteKernel.
R.-fker X ~> Y == finite kernel
The HB class is FiniteKernel.
R.-spker X ~> Y == subprobability kernel
The HB class is SubProbabilityKernel.
R.-pker X ~> Y == probability kernel
The HB class is ProbabilityKernel.
kseries == countable sum of kernels
It is declared as an instance of the structure
Kernel. It is also an instance of the structure
SFiniteKernel if the sum is over s-finite kernels.
kzero == kernel defined using the mzero measure
kdirac mf == kernel defined by a measurable function
mset U r == the set of 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
kadd k1 k2 == lifting of the addition of measures to kernels
l \; k == composition of kernels
ref: R. Affeldt, C. Cohen, A. Saito, Semantics of probabilistic programs
using s-finite kernels in Coq, CPP 2023
Set Implicit Arguments.
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.
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").
#[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%type Y R).
Arguments measurable_kernel {_ _ _ _ _} _.
Lemma kernel_measurable_eq_cst d d' (T : measurableType d)
(T' : measurableType d') (R : realType) (f : R.-ker T ~> T') k :
measurable [set t | f t [set: T'] == k].
Lemma kernel_measurable_neq_cst d d' (T : measurableType d)
(T' : measurableType d') (R : realType) (f : R.-ker T ~> T') k :
measurable [set t | f t [set: T'] != k].
Lemma kernel_measurable_fun_eq_cst d d' (T : measurableType d)
(T' : measurableType d') (R : realType) (f : R.-ker T ~> T') k :
measurable_fun [set: T] (fun t ⇒ f t [set: T'] == k).
Lemma eq_kernel d d' (T : measurableType d) (T' : measurableType d')
(R : realType) (k1 k2 : R.-ker T ~> T') :
(∀ x U, k1 x U = k2 x U) → k1 = k2.
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 [set: X] (kseries ^~ U).
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 :
(∀ y, 0 ≤ f y) →
measurable_fun [set: Y] f →
\int[kseries k x]_y (f y) = \sum_(i <oo) \int[k i x]_y (f y).
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 := ∃ r, ∀ x, k x [set: Y] < r%:E.
Lemma measure_fam_uubP : measure_fam_uub ↔
∃ r : {posnum R}, ∀ x, k x [set: Y] < r%:num%:E.
End measure_fam_uub.
Notation "R .-sfker X ~> Y" := (SFiniteKernel.type X%type Y R).
Arguments sfinite_kernel_subdef {_ _ _ _ _} _.
Lemma eq_sfkernel d d' (T : measurableType d) (T' : measurableType d')
(R : realType) (k1 k2 : R.-sfker T ~> T') :
(∀ x U, k1 x U = k2 x U) → k1 = k2.
#[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%type Y R).
Arguments measure_uub {_ _ _ _ _} _.
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 [set: X] (kzero ^~ U).
Lemma kzero_uub : measure_fam_uub kzero.
End kzero.
Let sfinite_finite :
exists2 k_ : (R.-ker _ ~> _)^nat, ∀ n, measure_fam_uub (k_ n) &
∀ x U, measurable U → k x U = mseries (k_ ^~ x) 0 U.
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_kernel_subdef k) in x.
Let ms n : @isKernel d d' X Y R (s n).
Let s_uub n : measure_fam_uub (s n).
Lemma sfinite_kernel : ∃ s : (R.-fker X ~> Y)^nat,
∀ x U, measurable U → k x U = kseries s x U.
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).
Lemma sfinite_subdef : Kernel_isSFinite_subdef d d' X Y R k.
Section sfkseries.
Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
Variables k : (R.-sfker X ~> Y)^nat.
Let sfinite_kseries : exists2 k_ : (R.-ker _ ~> _)^nat,
∀ n, measure_fam_uub (k_ n) &
∀ x U, measurable U → kseries k x U = mseries (k_ ^~ x) 0 U.
End sfkseries.
#[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%type Y R).
Let finite : @Kernel_isFinite d d' X Y R k.
#[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%type Y R).
Let sprob_kernel : @Kernel_isSubProbability d d' X Y R k.
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).
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.
Let phi A := fun x ⇒ kD x (xsection A x).
Let XY := [set A | measurable A ∧ measurable_fun [set: X] (phi A)].
Let phiM (A : set X) B : phi (A `*` B) = (fun x ⇒ kD x B × (\1_A x)%:E).
Lemma measurable_prod_subset_xsection_kernel :
(∀ x, ∃ M, ∀ X, measurable X → kD x X < M%:E) →
measurable `<=` XY.
End xsection_kernel.
End 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.
Let phi A := fun x ⇒ kD x (xsection A x).
Let XY := [set A | measurable A ∧ measurable_fun [set: X] (phi A)].
Let phiM (A : set X) B : phi (A `*` B) = (fun x ⇒ kD x B × (\1_A x)%:E).
Lemma measurable_prod_subset_xsection_kernel :
(∀ x, ∃ M, ∀ X, measurable X → kD x X < M%:E) →
measurable `<=` XY.
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 [set: X] (phi A)].
Lemma measurable_fun_xsection_finite_kernel A :
A \in measurable → measurable_fun [set: X] (phi A).
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] >-> R})^nat)
(ndk_ : nondecreasing_seq (k_ : (X × Y → R)^nat))
(k_k : ∀ z, EFin \o (k_ ^~ z) --> k z) :
(∀ n r,
measurable_fun [set: X] (fun x ⇒ l x (xsection (k_ n @^-1` [set r]) x))) →
measurable_fun [set: X] (fun x ⇒ \int[l x]_y k (x, y)).
Lemma measurable_fun_integral_finite_kernel (l : R.-fker X ~> Y)
(k0 : ∀ z, 0 ≤ k z) (mk : measurable_fun [set: X × Y] k) :
measurable_fun [set: X] (fun x ⇒ \int[l x]_y k (x, y)).
Lemma measurable_fun_integral_sfinite_kernel (l : R.-sfker X ~> Y)
(k0 : ∀ t, 0 ≤ k t) (mk : measurable_fun [set: X × Y] k) :
measurable_fun [set: X] (fun x ⇒ \int[l x]_y k (x, y)).
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 [set: X] f)
: X → {measure set Y → \bar R} :=
fun x ⇒ [the measure _ _ of dirac (f x)].
Hypothesis mf : measurable_fun [set: X] f.
Let measurable_fun_kdirac U : measurable U →
measurable_fun [set: X] (kdirac mf ^~ U).
Let kdirac_prob x : kdirac mf x setT = 1.
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.
Lemma gt1_mset (U : set T) (r : R) :
measurable U → (1 < r)%R → mset U r = [set: probability T R].
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 [set: X] P)
: X → {measure set Y → \bar R} := P.
Hypothesis mP : measurable_fun [set: X] P.
Let measurable_fun_kprobability U : measurable U →
measurable_fun [set: X] (kprobability mP ^~ U).
Let kprobability_prob x : kprobability mP x [set: Y] = 1.
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 [set: X] (kadd ^~ U).
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,
∀ n, measure_fam_uub (k_ n) &
∀ x U, measurable U →
kadd k1 k2 x U = mseries (k_ ^~ x) 0 U.
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).
End fkadd.
Lemma measurable_fun_mnormalize d d' (X : measurableType d)
(Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) :
measurable_fun [set: X] (fun x ⇒
[the probability _ _ of mnormalize (k x) point] : pprobability Y R).
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 x) P].
Variable P : probability Y R.
Let measurable_fun_knormalize U :
measurable U → measurable_fun [set: X] (knormalize P ^~ U).
Let knormalize1 x : knormalize P x [set: Y] = 1.
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] ~> Z.
Let kcomp0 x : (l \; k) x set0 = 0.
Let kcomp_ge0 x U : 0 ≤ (l \; k) x U.
Let kcomp_sigma_additive x : semi_sigma_additive ((l \; k) 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] ~> Z).
Lemma measurable_fun_kcomp_finite U :
measurable U → measurable_fun [set: X] ((l \; k) ^~ U).
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] ~> Z.
Let mkcomp_finite : measure_fam_uub (l \; k).
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] ~> Z.
Import KCOMP_FINITE_KERNEL.
Lemma mkcomp_sfinite : ∃ k_ : (R.-fker X ~> Z)^nat,
∀ x U, measurable U → (l \; k) x U = kseries k_ x U.
Lemma measurable_fun_mkcomp_sfinite U : measurable U →
measurable_fun [set: X] ((l \; k) ^~ U).
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] ~> Z.
#[export]
HB.instance Definition _ :=
Kernel_isSFinite.Build _ _ X Z R (l \; k) (mkcomp_sfinite l k).
End kcomp_sfinite_kernel.
End 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 : ∀ z, [set: Y] 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.
Let mk_2 n : measurable_fun [set: X × Y] (k_2 n).
Let fk_2 n : finite_set (range (k_2 n)).
Lemma measurable_fun_preimage_integral (l : X → {measure set Y → \bar R}) :
(∀ n r, measurable_fun [set: X] (l ^~ (k_ n @^-1` [set r]))) →
measurable_fun [set: X] (fun x ⇒ \int[l x]_z k z).
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 : ∀ U, measurable U → measurable_fun [set: X] (l ^~ U))
(* NB: l is really just a kernel *)
(k : Y → \bar R) (k0 : ∀ z, 0 ≤ k z) (mk : measurable_fun [set: Y] k) :
measurable_fun [set: X] (fun x ⇒ \int[l x]_y k y).
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] ~> 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).
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).
Lemma integral_kcomp x f : (∀ z, 0 ≤ f z) → measurable_fun [set: Z] f →
\int[(l \; k) x]_z f z = \int[l x]_y (\int[k (x, y)]_z f z).
End integral_kcomp.
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 [set: X] (phi A)].
Lemma measurable_fun_xsection_finite_kernel A :
A \in measurable → measurable_fun [set: X] (phi A).
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] >-> R})^nat)
(ndk_ : nondecreasing_seq (k_ : (X × Y → R)^nat))
(k_k : ∀ z, EFin \o (k_ ^~ z) --> k z) :
(∀ n r,
measurable_fun [set: X] (fun x ⇒ l x (xsection (k_ n @^-1` [set r]) x))) →
measurable_fun [set: X] (fun x ⇒ \int[l x]_y k (x, y)).
Lemma measurable_fun_integral_finite_kernel (l : R.-fker X ~> Y)
(k0 : ∀ z, 0 ≤ k z) (mk : measurable_fun [set: X × Y] k) :
measurable_fun [set: X] (fun x ⇒ \int[l x]_y k (x, y)).
Lemma measurable_fun_integral_sfinite_kernel (l : R.-sfker X ~> Y)
(k0 : ∀ t, 0 ≤ k t) (mk : measurable_fun [set: X × Y] k) :
measurable_fun [set: X] (fun x ⇒ \int[l x]_y k (x, y)).
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 [set: X] f)
: X → {measure set Y → \bar R} :=
fun x ⇒ [the measure _ _ of dirac (f x)].
Hypothesis mf : measurable_fun [set: X] f.
Let measurable_fun_kdirac U : measurable U →
measurable_fun [set: X] (kdirac mf ^~ U).
Let kdirac_prob x : kdirac mf x setT = 1.
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.
Lemma gt1_mset (U : set T) (r : R) :
measurable U → (1 < r)%R → mset U r = [set: probability T R].
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 [set: X] P)
: X → {measure set Y → \bar R} := P.
Hypothesis mP : measurable_fun [set: X] P.
Let measurable_fun_kprobability U : measurable U →
measurable_fun [set: X] (kprobability mP ^~ U).
Let kprobability_prob x : kprobability mP x [set: Y] = 1.
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 [set: X] (kadd ^~ U).
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,
∀ n, measure_fam_uub (k_ n) &
∀ x U, measurable U →
kadd k1 k2 x U = mseries (k_ ^~ x) 0 U.
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).
End fkadd.
Lemma measurable_fun_mnormalize d d' (X : measurableType d)
(Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) :
measurable_fun [set: X] (fun x ⇒
[the probability _ _ of mnormalize (k x) point] : pprobability Y R).
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 x) P].
Variable P : probability Y R.
Let measurable_fun_knormalize U :
measurable U → measurable_fun [set: X] (knormalize P ^~ U).
Let knormalize1 x : knormalize P x [set: Y] = 1.
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] ~> Z.
Let kcomp0 x : (l \; k) x set0 = 0.
Let kcomp_ge0 x U : 0 ≤ (l \; k) x U.
Let kcomp_sigma_additive x : semi_sigma_additive ((l \; k) 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] ~> Z).
Lemma measurable_fun_kcomp_finite U :
measurable U → measurable_fun [set: X] ((l \; k) ^~ U).
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] ~> Z.
Let mkcomp_finite : measure_fam_uub (l \; k).
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] ~> Z.
Import KCOMP_FINITE_KERNEL.
Lemma mkcomp_sfinite : ∃ k_ : (R.-fker X ~> Z)^nat,
∀ x U, measurable U → (l \; k) x U = kseries k_ x U.
Lemma measurable_fun_mkcomp_sfinite U : measurable U →
measurable_fun [set: X] ((l \; k) ^~ U).
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] ~> Z.
#[export]
HB.instance Definition _ :=
Kernel_isSFinite.Build _ _ X Z R (l \; k) (mkcomp_sfinite l k).
End kcomp_sfinite_kernel.
End 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 : ∀ z, [set: Y] 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.
Let mk_2 n : measurable_fun [set: X × Y] (k_2 n).
Let fk_2 n : finite_set (range (k_2 n)).
Lemma measurable_fun_preimage_integral (l : X → {measure set Y → \bar R}) :
(∀ n r, measurable_fun [set: X] (l ^~ (k_ n @^-1` [set r]))) →
measurable_fun [set: X] (fun x ⇒ \int[l x]_z k z).
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 : ∀ U, measurable U → measurable_fun [set: X] (l ^~ U))
(* NB: l is really just a kernel *)
(k : Y → \bar R) (k0 : ∀ z, 0 ≤ k z) (mk : measurable_fun [set: Y] k) :
measurable_fun [set: X] (fun x ⇒ \int[l x]_y k y).
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] ~> 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).
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).
Lemma integral_kcomp x f : (∀ z, 0 ≤ f z) → measurable_fun [set: Z] f →
\int[(l \; k) x]_z f z = \int[l x]_y (\int[k (x, y)]_z f z).
End integral_kcomp.