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.
Reference:
- R. Affeldt, C. Cohen, A. Saito. Semantics of probabilistic programs
using s-finite kernels in Coq. CPP 2023
```
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
```
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.
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 [set: X] (
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%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].
Proof.
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].
Proof.
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).
Proof.
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 [set: X] (
kseries ^~ U).
Proof.
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 [set: Y] f ->
\int[kseries k x]_y (
f y)
= \sum_(
i
<oo)
\int[k i x]_y (
f y).
Proof.
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_kernel_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 }.
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"
:= (
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')
:
(
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%type 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 [set: X] (
kzero ^~ U).
Proof.
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.
Let
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.
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_kernel_subdef k)
in x.
Let
ms
n
: @isKernel d d' X Y R (
s n).
Proof.
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_kernel
: exists
s
: (
R.
-fker X ~> Y)
^nat,
forall
x
U,
measurable U -> k x U = kseries s x U.
Proof.
exists (
fun
n
=> [the _.
-fker _ ~> _ of s n])
=> x U mU.
by 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.
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.
HB.instance Definition _ := sfinite_subdef.
HB.end.
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,
forall
n,
measure_fam_uub (
k_ n)
&
forall
x
U,
measurable U -> kseries k x U = mseries (
k_ ^~ x)
0 U.
Proof.
HB.instance Definition _ :=
Kernel_isSFinite_subdef.Build _ _ _ _ R (
kseries k)
sfinite_kseries.
End sfkseries.
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 [set: X]] <= 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%type 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 [set: X]] <= 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.
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%type 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 [set: Y] = 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.
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.
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 [set: X] (
phi A)
].
Let
phiM
(
A
: set X)
B
: phi (
A `*` B)
= (
fun
x
=> kD x B * (
\1_A x)
%:E).
Proof.
Lemma
measurable_prod_subset_xsection_kernel
:
(
forall
x,
exists
M,
forall
X,
measurable X -> kD x X < M%:E)
->
measurable `<=` XY.
Proof.
End xsection_kernel.
End measurable_prod_subset_kernel.
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).
Proof.
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
: forall
z,
EFin \o (
k_ ^~ z)
--> k z)
:
(
forall
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)).
Proof.
Lemma
measurable_fun_integral_finite_kernel
(
l
: R.
-fker X ~> Y)
(
k0
: forall
z,
0 <= k z) (
mk
: measurable_fun [set: X * Y] k)
:
measurable_fun [set: X] (
fun
x
=> \int[l x]_y k (
x, y)).
Proof.
Lemma
measurable_fun_integral_sfinite_kernel
(
l
: R.
-sfker X ~> Y)
(
k0
: forall
t,
0 <= k t) (
mk
: measurable_fun [set: X * Y] k)
:
measurable_fun [set: X] (
fun
x
=> \int[l x]_y k (
x, y)).
Proof.
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).
Proof.
move=> mU; apply/EFin_measurable_fun.
by rewrite (
_ : (
fun
x
=> _)
= mindic R mU \o f)
//; exact/measurableT_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 = [set: probability T R].
Proof.
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).
Proof.
HB.instance Definition _ :=
@isKernel.
Build _ _ X Y R (
kprobability mP)
measurable_fun_kprobability.
Let
kprobability_prob
x
: kprobability mP x [set: Y] = 1.
Proof.
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 [set: X] (
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.
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.
HB.instance Definition _
t
:=
Kernel_isFinite.Build _ _ _ _ R (
kadd k1 k2)
kadd_finite_uub.
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).
Proof.
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).
Proof.
HB.instance Definition _ := isKernel.Build _ _ _ _ R (
knormalize P)
measurable_fun_knormalize.
Let
knormalize1
x
: knormalize P x [set: Y] = 1.
Proof.
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] ~> Z.
Let
kcomp0
x
: kcomp l k x set0 = 0.
Proof.
Let
kcomp_ge0
x
U
: 0 <= kcomp l k x U
Proof.
Let
kcomp_sigma_additive
x
: semi_sigma_additive (
kcomp l k x).
Proof.
HB.instance Definition _
x
:= isMeasure.Build _ _ R
(
kcomp 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 kcomp 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).
Proof.
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] ~> Z.
Let
mkcomp_finite
: measure_fam_uub (
mkcomp l k).
Proof.
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] ~> 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.
Lemma
measurable_fun_mkcomp_sfinite
U
: measurable U ->
measurable_fun [set: X] ((
l \; k)
^~ U).
Proof.
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.
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,
[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
Proof.
by []. Qed.
HB.instance Definition _
n
:= @isNonNegFun.
Build _ _ _ (
k_2_ge0 n).
Let
mk_2
n
: measurable_fun [set: X * Y] (
k_2 n).
Proof.
HB.instance Definition _
n
:= @isMeasurableFun.
Build _ _ _ _ (
mk_2 n).
Let
fk_2
n
: finite_set (
range (
k_2 n)).
Proof.
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 [set: X] (
l ^~ (
k_ n @^-1` [set r])))
->
measurable_fun [set: X] (
fun
x
=> \int[l x]_z k z).
Proof.
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 [set: X] (
l ^~ U))
(
k
: Y -> \bar R) (
k0
: forall
z,
0 <= k z) (
mk
: measurable_fun [set: Y] k)
:
measurable_fun [set: X] (
fun
x
=> \int[l x]_y k y).
Proof.
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[kcomp l k x]_z (
\1_E z)
%:E = \int[l x]_y (
\int[k (
x, y)
]_z (
\1_E z)
%:E).
Proof.
Let
integral_kcomp_nnsfun
x
(
f
: {nnsfun Z >-> R})
:
\int[kcomp l k x]_z (
f z)
%:E = \int[l x]_y (
\int[k (
x, y)
]_z (
f z)
%:E).
Proof.
Lemma
integral_kcomp
x
f
: (
forall
z,
0 <= f z)
-> measurable_fun [set: Z] f ->
\int[kcomp l k x]_z f z = \int[l x]_y (
\int[k (
x, y)
]_z f z).
Proof.
End integral_kcomp.