Module mathcomp.analysis.kernel

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrnum ssrint interval.
From mathcomp Require Import interval_inference archimedean.
From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
From mathcomp Require Import reals topology ereal normedtype sequences esum.
From mathcomp Require Import measure numfun real_measure lebesgue_integral.

# Kernels This file provides a formation of kernels, s-finite kernels, sigma-finite kernels, finite transition kernels, finite kernels, subprobability kernels, and probability kernels, organized as a hierarchy of mathematical structures. The main formalized results are stability by composition for s-finite kernels [Lemma 3, Staton, ESOP 2017] and subprobability kernels [Theorem 14.26, Klenke 2014]. References: - R. Affeldt, C. Cohen, A. Saito. Semantics of probabilistic programs using s-finite kernels in Coq. CPP 2023 - S. Staton. Commutative Semantics for Probabilistic Programming. ESOP 2017 - A. Klenke. Probability theory: A comprehensive course. 2014 ``` R.-ker X ~> Y == kernel from X to Y where X and Y are of type measurableType The HB class is Kernel. kseries == countable sum of kernels It is declared as an instance of the structure Kernel. It will also be shown to be an instance of SFiniteKernel if the sum is over s-finite kernels. measure_fam_uub k == the kernel k is uniformly upper-bounded R.-sfker X ~> Y == s-finite kernel The HB class is SFiniteKernel. kzero == kernel defined using the mzero measure R.-sigmafker X ~> Y == sigma-finite transition kernel The HB class is SigmaFiniteTransitionKernel. R.-ftker X ~> Y == finite transition kernel The HB class is FiniteTransitionKernel. 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. kdirac mf == kernel defined by a measurable function kprobability m == kernel defined by a probability measure kadd k1 k2 == lifting of the addition of measures to kernels knormalize f P := fun x => mnormalize (f x) P kcomp l k == "parameterized" composition for kernels l has type X -> {measure set Y -> \bar R} k has type X * Y -> {measure set Z -> \bar R} kcomp l k as type X -> set Z -> \bar R l \; k == same as kcomp l k but equipped with the type X -> {measure set Z -> \bar R} kfcomp k f == composition of a "kernel" and a function k has type X -> {measure set Y -> \bar R}. kproduct k1 k2 == "parameterized" product of kernels k1 has type T0 -> {measure set T1 -> \bar R}. k2 has type T0 * T1 -> {measure set T2 -> \bar R}. The result has type T0 -> set (T1 * T2) -> \bar R. mkproduct k1 k2 == same as kproduct k1 k2 but equipped with the type T0 -> {measure set (T1 * T2) -> \bar R} kproduct_snd k1 k2 := kproduct k1 (k2 \o snd) k2 has T1 -> {measure set T2 -> \bar R} It "ignores" the first argument of k2. kcomp_noparam k1 k2 := composition of kernels k1 has type T0 -> {measure set T1 -> \bar R}. k2 has type T1 -> {measure set T2 -> \bar R}. The return type is T0 -> set (T1 * T2) -> \bar R ```

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory 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 .-sigmafker X ~> Y"
  (at level 42, format "R .-sigmafker X ~> Y").
Reserved Notation "R .-ftker X ~> Y"
  (at level 42, format "R .-ftker 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").

. ( d) (Y : measurableType d')
    (R : realType) (k : X -> {measure set Y -> \bar R}) := {
  measurable_kernel :
    forall , measurable U -> measurable_fun [set: X] (k ^~ U) }.

()
.
    ( d) (Y : measurableType d') (R : realType) :=
  { & isKernel _ _ X Y R k }.
Notation := (kernel X%type Y R).

Arguments measurable_kernel {_ _ _ _ _} _.

Lemma ( : measurableType d)
    ( : measurableType d') ( : realType) ( : R.-ker T ~> T') :
  measurable [set | f t [set: T'] == k].

Proof.

rewrite [X in measurable X](_ : _ = (f ^~ setT) @^-1` [set k]).
by apply/seteqP; split => t/= /eqP.
have /(_ measurableT [set k]) := measurable_kernel f setT measurableT.
by rewrite setTI; exact.
Qed.

Lemma ( : measurableType d)
( : measurableType d') ( : realType) ( : R.-ker T ~> T') :
measurable [set | f t [set: T'] != k].

Proof.

rewrite [X in measurable X](_ : _ = (f ^~ setT) @^-1` [set~ k]).
by apply/seteqP; split => t /eqP.
have /(_ measurableT [set~ k]) := measurable_kernel f setT measurableT.
by rewrite setTI; apply => //; exact: measurableC.
Qed.

Lemma ( : measurableType d)
( : measurableType d') ( : realType) ( : R.-ker T ~> T') :
measurable_fun [set: T] (fun => f t [set: T'] == k).

Proof.

move=> _ /= B mB; rewrite setTI.
have [/eqP->|/eqP->|/eqP->|/eqP->] := set_bool B.
- exact: kernel_measurable_eq_cst.
- rewrite (_ : _ @^-1` _ = [set | f b setT != k]).
by apply/seteqP; split => [t /negbT//|t /negbTE].
exact: kernel_measurable_neq_cst.
- by rewrite preimage_set0.
- by rewrite preimage_setT.
Qed.

Lemma ( : measurableType d) ( : measurableType d')
( : realType) ( : R.-ker T ~> T') :
(forall , 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 ( : measurableType d) ( : measurableType d') ( : realType).
Variable : (R.-ker X ~> Y)^nat.

Definition ( : X) : {measure set Y -> \bar R} := mseries (k ^~ x) 0.

Lemma ( : set Y) :
measurable U -> measurable_fun [set: X] (kseries ^~ U).

Proof.

by move=> mU; apply: ge0_emeasurable_sum => // n _; exact/measurable_kernel.
Qed.

.
  isKernel.Build _ _ _ _ _ kseries measurable_fun_kseries.

End kseries.

Lemma ( : measurableType d) ( : measurableType d')
  ( : realType) ( : (R.-ker X ~> Y)^nat) ( : Y -> \bar R) :
  (forall , 0 <= f y) ->
  measurable_fun [set: Y] f ->
  \int[kseries k x]_ (f y) = \sum_( <oo) \int[k i x]_ (f y).

Proof.

by move=> f0 mf; rewrite /kseries/= ge0_integral_measure_series.
Qed.

Section measure_fam_uub.
Context ( : measurableType d) ( : measurableType d') ( : numFieldType).
Variable : X -> {measure set Y -> \bar R}.

Definition := exists , forall , k x [set: Y] < r%:E.

Lemma : measure_fam_uub <->
exists : {posnum R}, forall , k x [set: Y] < r%:num%:E.

Proof.

split => [|] [r kr]; last by exists r%:num.
have [[point _]|/forallNP empty] := pselect (exists : X, True).
suff r_gt0 : (0 < r)%R by exists (PosNum r_gt0).
rewrite -lte_fin; exact: le_lt_trans (kr point).
by exists (PosNum ltr01) => x; have := empty x.
Qed.

End measure_fam_uub.

.
    ( d) (Y : measurableType d') (R : realType)
    (k : X -> {measure set Y -> \bar R}) := {
  sfinite_kernel_subdef : exists2 : (R.-ker X ~> Y)^nat,
    forall , measure_fam_uub (s n) &
    forall , measurable U -> k x U = kseries s x U }.

.
    ( d) (Y : measurableType d') (R : realType) :=
  { of @Kernel _ _ _ _ R k &
         isSFiniteKernel_subdef _ _ X Y R k }.
Notation := (SFiniteKernel.type X%type Y R).
Arguments sfinite_kernel_subdef {_ _ _ _ _} _.

Lemma ( : measurableType d) ( : measurableType d')
    ( : realType) ( : R.-sfker T ~> T') :
  (forall , 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 kzero.
Context ( : measurableType d) ( : measurableType d') ( : realType).

Definition (_ : X) : {measure set Y -> \bar R} := mzero.

Let : measurable U ->
measurable_fun [set: X] (kzero ^~ U).

Proof.

by move=> ?/=; exact: measurable_cst. Qed.

.
.Build _ _ X Y R kzero measurable_fun_kzero.

Lemma : measure_fam_uub kzero.

Proof.

by exists 1%R => /= t; rewrite /mzero/=. Qed.

End kzero.

.
     ( d) (Y : measurableType d')
    (R : realType) (k : X -> {measure set Y -> \bar R}) := {
  kernel_sigma_finite : forall , sigma_finite [set: Y] (k x) }.

()
.
     ( d) (Y : measurableType d') (R : realType) :=
  { of @Kernel _ _ _ _ _ k &
         isSigmaFiniteTransitionKernel _ _ X Y R k }.

Notation := (sigma_finite_kernel X%type Y R).

.
     ( d) (Y : measurableType d')
    (R : realType) (k : X -> {measure set Y -> \bar R}) := {
  kernel_finite_transition : forall , fin_num_fun (k x) }.

#[deprecated(since="mathcomp-analysis 1.11.0",
             note="Use isFiniteTransitionKernel instead.")]
Notation x1 x2 x3 x4 x5 x6 :=
  (isFiniteTransitionKernel x1 x2 x3 x4 x5 x6).

()
.
     ( d) (Y : measurableType d') (R : realType) :=
  { of @SFiniteKernel _ _ _ _ _ k &
         isFiniteTransitionKernel _ _ X Y R k }.

Module .
#[deprecated(since="mathcomp-analysis 1.11.0",
             note="Use isFiniteTransitionKernel.Build instead.")]
Notation x1 x2 x3 x4 x5 x6 :=
  (isFiniteTransitionKernel.Build x1 x2 x3 x4 x5 x6) (only parsing).
End isFiniteTransition.

Notation := (finite_transition_kernel X%type Y R).

.
    ( d) (Y : measurableType d') (R : realType)
    (k : X -> {measure set Y -> \bar R}) := {
  measure_uub : measure_fam_uub k }.

()
.
    ( d) (Y : measurableType d') (R : realType) :=
  { of @FiniteTransitionKernel _ _ _ _ _ k &
         isMeasureFamUub _ _ X Y R k }.
Notation := (finite_kernel X%type Y R).
Arguments measure_uub {_ _ _ _ _} _.

.
    ( d) (Y : measurableType d') (R : realType)
    (k : X -> {measure set Y -> \bar R}) & isKernel _ _ _ _ _ k := {
  measure_uub : measure_fam_uub k }.

. ( d) (Y : measurableType d')
  (R : realType) k & Kernel_isFinite d d' X Y R k.

Let :
  exists2 : (R.-ker _ ~> _)^nat, forall , measure_fam_uub (k_ n) &
    forall , measurable U -> k x U = mseries (k_ ^~ x) 0 U.

Proof.

exists (fun => if n is O return R.-ker X ~> Y then k else @kzero _ _ X Y R).
by case => [|_]; [exact: measure_uub|exact: kzero_uub].
move=> t U mU/=; rewrite /mseries.
rewrite (nneseries_split _ 1%N)// big_mkord big_ord_recl/= big_ord0 adde0.
rewrite ereal_series (@eq_eseriesr _ _ (fun=> 0)); first by case.
by rewrite eseries0// adde0.
Qed.

.
.Build d d' X Y R k sfinite_finite.

Let : sigma_finite setT (k x).

Proof.

apply: fin_num_fun_sigma_finite; first by rewrite measure0.
apply: lty_fin_num_fun.
by have [r kr] := measure_uub; rewrite (lt_trans (kr x)) ?ltry.
Qed.

.
.Build d d' X Y R k kernel_sigma_finite.

Let : forall , fin_num_fun (k x).

Proof.

move=> x U mU.
have [r kr] := measure_uub.
rewrite ge0_fin_numE//.
rewrite (@le_lt_trans _ _ (k x setT)) ?le_measure ?inE//.
by rewrite (lt_trans (kr x)) ?ltry.
Qed.

.
  .Build d d' X Y R k finite_transition_finite.

.
  .Build d d' X Y R k measure_uub.

..

Section sfinite.
Context ( : measurableType d) ( : measurableType d').
Variables ( : realType) ( : R.-sfker X ~> Y).

Let : (X -> {measure set Y -> \bar R})^nat :=
  let: exist2 x _ _ := cid2 (sfinite_kernel_subdef k) in x.

Let : @isKernel d d' X Y R (s n).

Proof.

split; rewrite /s; case: cid2 => /= s' s'_uub kE.
exact: measurable_kernel.
Qed.

. n.

Let : measure_fam_uub (s n).

Proof.

by rewrite /s; case: cid2. Qed.

..Build d d' X Y R (s n) (s_uub n).

Lemma : exists : (R.-fker X ~> Y)^nat,
forall , measurable U -> k x U = kseries s x U.

Proof.

by exists s => x U mU; rewrite /s /= /s; case: cid2 => ? ? ->. Qed.

End sfinite.

Lemma ( : measurableType d) ( : measurableType d')
( : realType) ( : R.-sfker Z ~> X) ( : Z) :
sfinite_measure (k z).

Proof.

have [s ks] := sfinite_kernel 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.

.
     ( d) (Y : measurableType d') (R : realType) :=
  @Kernel_isFinite.Build _ _ _ _ R (@kzero _ _ X Y R)
                                   (@kzero_uub _ _ X Y R).

.
    ( d) (Y : measurableType d') (R : realType)
    (k : X -> {measure set Y -> \bar R}) & isKernel _ _ _ _ _ k := {
  sfinite : exists : (R.-fker X ~> Y)^nat,
    forall , measurable U -> k x U = kseries s x U }.

. ( d) (Y : measurableType d')
  (R : realType) k & Kernel_isSFinite d d' X Y R k.

Lemma : isSFiniteKernel_subdef d d' X Y R k.

Proof.

split; have [s sE] := sfinite; exists s => //.
by move=> n; exact: measure_uub.
Qed.

..

..

Section sfkseries.
Context ( : measurableType d) ( : measurableType d') ( : realType).
Variables : (R.-sfker X ~> Y)^nat.

Let : exists2 : (R.-ker _ ~> _)^nat,
forall , measure_fam_uub (k_ n) &
forall , measurable U -> kseries k x U = mseries (k_ ^~ x) 0 U.

Proof.

have /ppcard_eqP[f] : ([set: nat] #= [set: nat * nat])%card.
  by rewrite card_eq_sym; exact: card_nat2.
pose p : (R.-fker X ~> Y)^nat := sval (cid (sfinite_kernel (k n))).
exists (fun => p (f i).1 (f i).2).
  move=> n; have [r Hr] := measure_uub (p (f n).1 (f n).2).
  by exists r => x /=; exact: Hr.
move=> x U mU; rewrite /kseries /mseries/= /mseries/=.
have kE i : k i x U = \sum_( <oo) p i j x U.
  by rewrite /p /sval/=; case: cid => k_ ->.
transitivity (\esum_( in [set: nat] `*` [set: nat]) p l.1 l.2 x U).
  rewrite (_ : _ `*` _ = setT `*`` (fun=> setT)); first by apply/seteqP; split.
  rewrite -(@esum_esum _ _ _ _ _ (fun => p i j x U))//.
  rewrite nneseries_esumT//; apply: eq_esum => i _.
  by rewrite kE// nneseries_esumT.
rewrite (reindex_esum [set: nat] _ f)//.
  have := @bijTT _ _ f.
  by rewrite -setTT_bijective/= -[in X in set_bij _ X _ -> _](@setXTT nat nat).
by rewrite nneseries_esumT//; exact: eq_esum.
Qed.

.
  isSFiniteKernel_subdef.Build _ _ _ _ R (kseries k) sfinite_kseries.
End sfkseries.

.
    ( d) (Y : measurableType d') (R : realType)
    (k : X -> {measure set Y -> \bar R}) := {
  sprob_kernel : ereal_sup [set k x [set: Y] | in [set: X]] <= 1 }.

()
.
     ( d) (Y : measurableType d') (R : realType) :=
  { of @FiniteKernel _ _ _ _ _ k &
         isSubProbabilityKernel _ _ X Y R k }.
Notation := (sprobability_kernel X%type Y R).

Lemma ( : measurableType d) ( : measurableType d')
    ( : realType) ( : X -> set Y -> \bar R) :
  ereal_sup [set k x [set: _] | in [set: _]] <= 1 <->
  forall , k x [set: Y] <= 1.

Proof.

split => [+ x|k1]; last by apply: ge_ereal_sup => _ /= [z _ <-]; exact: k1.
by apply/le_trans/ereal_sup_ubound => /=; exists x.
Qed.

Lemma ( : measurableType d)
( : measurableType d') ( : realType) ( : R.-spker X ~> Y) :
k x [set: Y] <= 1.

Proof.

by apply: (sprob_kernelP (fun => k x A)).1; exact: sprob_kernel. Qed.

.
    ( d) (Y : measurableType d') (R : realType)
    (k : X -> {measure set Y -> \bar R}) & isKernel _ _ X Y R k := {
  sprob_kernel : ereal_sup [set k x [set: Y] | in [set: X]] <= 1 }.

. ( d) (Y : measurableType d')
  (R : realType) k & Kernel_isSubProbability d d' X Y R k.

Let : @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_ubound.
Qed.

..

.
  .Build _ _ _ _ _ k sprob_kernel.

..

.
    ( d) (Y : measurableType d') (R : realType)
    (k : X -> {measure set Y -> \bar R}) := {
  prob_kernel : forall , k x [set: Y] = 1 }.

()
.
    ( d) (Y : measurableType d') (R : realType) :=
  { of @SubProbabilityKernel _ _ _ _ _ k &
         isProbabilityKernel _ _ X Y R k }.
Notation := (probability_kernel X%type Y R).

.
    ( d) (Y : measurableType d') (R : realType)
    (k : X -> {measure set Y -> \bar R}) & isKernel _ _ X Y R k := {
  prob_kernel : forall , k x [set: Y] = 1 }.

. ( d) (Y : measurableType d')
  (R : realType) k & Kernel_isProbability d d' X Y R k.

Let : @Kernel_isSubProbability d d' X Y R k.

Proof.

by split; apply: ge_ereal_sup => x [y _ <-{x}]; rewrite prob_kernel.
Qed.

..

.
  .Build _ _ _ _ _ k prob_kernel.

..

Lemma ( : measurableType d)
    ( : measurableType d') ( : realType) ( : R.-fker X ~> Y) ( : 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.

Section measurable_prod_subset_kernel.
Context ( : measurableType d) ( : measurableType d') ( : realType).
Implicit Types A : set (X * Y).

Section xsection_kernel.
Variable ( : R.-ker X ~> Y) ( : set Y) ( : measurable D).
Let := mrestr (k x) mD.
..on (kD x).
Let := fun => kD x (xsection A x).
Let := [set | measurable A /\ measurable_fun [set: X] (phi A)].

Let ( : set X) : phi (A `*` B) = (fun => 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_xsectionX.
by rewrite mule0 notin_xsectionX// set0I measure0.
Qed.

Lemma :
(forall , exists , forall , measurable X -> kD x X < M%:E) ->
measurable `<=` XY.

Proof.

move=> kD_ub.
rewrite prod_measurable_rectangle; set C := rectangle _ _.
have CI : setI_closed C by apply: setI_closed_rectangle=> *; exact: measurableI.
have CT : C setT by rewrite -setXTT; exact: rectangle_setX.
have CXY : C `<=` XY.
  move=> _ [A mA [B mB <-]]; split; first exact: measurableX.
  rewrite phiM.
  apply: emeasurable_funM => //; first exact/measurable_kernel/measurableI.
  by apply/measurable_EFinP; rewrite (_ : \1_ _ = mindic R mA).
suff lsystemB : lambda_system setT XY by exact: lambda_system_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 => phi A x - phi B x).
  by move=> ->; exact: emeasurable_funB.
rewrite funeqE => x; rewrite /phi/= xsectionD// measureD/=.
- exact: measurable_xsection.
- exact: measurable_xsection.
- have [M kM] := kD_ub x.
  rewrite (lt_le_trans (kM (xsection A x) _)) ?leey//.
  exact: measurable_xsection.
- by rewrite setIidr//; exact: le_xsection.
Qed.

End xsection_kernel.

End measurable_prod_subset_kernel.

Section measurable_fun_xsection_finite_kernel.
Context ( : measurableType d) ( : measurableType d') ( : realType).
Variable : R.-fker X ~> Y.
Implicit Types A : set (X * Y).

Let := fun => k x (xsection A x).
Let := [set | measurable A /\ measurable_fun [set: X] (phi A)].

Lemma :
A \in measurable -> measurable_fun [set: X] (phi A).

Proof.

move: A; suff : measurable `<=` XY by move=> + A; rewrite inE => /[apply] -[].
move=> /= A mA; rewrite /XY/=; split => //; rewrite (_ : phi _ =
(fun => mrestr (k x) measurableT (xsection A x))).
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 { } { : measurableType d} { : measurableType d'} { : realType}
  ( : X * Y -> \bar R).

Import HBNNSimple.
Import MeasurableR.

Lemma
    ( : X -> {measure set Y -> \bar R})
    ( : {nnsfun (X * Y) >-> R}^nat)
    ( : nondecreasing_seq (k_ : (X * Y -> R)^nat))
    ( : forall , (k_ n z)%:E @[ --> \oo] --> k z) :
  (forall ,
    measurable_fun [set: X] (fun => l x (xsection (k_ n @^-1` [set r]) x))) ->
  measurable_fun [set: X] (fun => \int[l x]_ k (x, y)).

Proof.

move=> h.
rewrite (_ : (fun => _) =
    (fun => limn_esup (fun => \int[l x]_ (k_ n (x, y))%:E))).
  apply/funext => x.
  transitivity (lim (\int[l x]_ (k_ n (x, y))%:E @[ --> \oo])); last first.
    rewrite is_cvg_limn_esupE//.
    apply: ereal_nondecreasing_is_cvgn => m n mn.
    apply: ge0_le_integral => //.
    - by move=> y _; rewrite lee_fin.
    - exact/measurable_EFinP/measurableT_comp.
    - exact/measurable_EFinP/measurableT_comp.
    - by move=> y _; rewrite lee_fin; exact/lefP/ndk_.
  rewrite -monotone_convergence//.
  - by move=> n; exact/measurable_EFinP/measurableT_comp.
  - by move=> n y _; rewrite lee_fin.
  - by move=> y _ m n mn; rewrite lee_fin; exact/lefP/ndk_.
  - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: k_k.
apply: measurable_fun_limn_esup => n.
rewrite [X in measurable_fun _ X](_ : _ = (fun => \int[l x]_
    (\sum_( \in range (k_ n))
      r * \1_(k_ n @^-1` [set r]) (x, y))%:E)).
  by apply/funext => x; apply: eq_integral => y _; rewrite fimfunE.
rewrite [X in measurable_fun _ X](_ : _ = (fun => \sum_( \in range (k_ n))
    (\int[l x]_ (r * \1_(k_ n @^-1` [set r]) (x, y))%:E))).
  apply/funext => x; rewrite -ge0_integral_fsum//.
  - move=> r.
    apply/measurable_EFinP/measurableT_comp => [//|].
    exact/measurableT_comp.
  - by move=> m y _; rewrite nnfun_muleindic_ge0.
  - by apply: eq_integral => y _; rewrite -fsumEFin.
apply: emeasurable_fsum => // r.
rewrite [X in measurable_fun _ X](_ : _ = fun => r%:E *
    \int[l x]_ (\1_(k_ n @^-1` [set r]) (x, y))%:E).
  apply/funext => x; under eq_integral do rewrite EFinM.
  have [r0|r0] := leP 0%R r.
    by rewrite ge0_integralZl//; exact/measurable_EFinP/measurableT_comp.
  rewrite integral0_eq.
    by move=> y _; rewrite preimage_nnfun0// indic0 mule0.
  by rewrite integral0_eq ?mule0// => y _; rewrite preimage_nnfun0// indic0.
apply/measurable_funeM.
rewrite (_ : (fun => _) = (fun => l x (xsection (k_ n @^-1` [set r]) x))); last first.
  exact/h.
apply/funext => x; rewrite integral_indic//; last first.
  congr (l x _); apply/funext => y1/=; rewrite /xsection/= inE.
  by apply/propext; tauto.
rewrite (_ : (fun => _) = xsection (k_ n @^-1` [set r]) x); last first.
  exact: measurable_xsection.
by rewrite /xsection; apply/seteqP; split=> y/= /[!inE].
Qed.

Lemma ( : R.-fker X ~> Y)
( : forall , 0 <= k z) ( : measurable_fun [set: X * Y] k) :
measurable_fun [set: X] (fun => \int[l x]_ k (x, y)).

Proof.

Lemma ( : R.-sfker X ~> Y)
( : forall , 0 <= k t) ( : measurable_fun [set: X * Y] k) :
measurable_fun [set: X] (fun => \int[l x]_ k (x, y)).

Proof.

pose k_ := nnsfun_approx measurableT mk.
apply: (@measurable_fun_xsection_integral _ k_).
- by move=> a b ab; exact/nd_nnsfun_approx.
- by move=> z; exact/cvg_nnsfun_approx.
- move => n r.
  have [l_ hl_] := sfinite_kernel l.
  rewrite (_ : (fun => _) = (fun =>
      mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))).
    by apply/funext => x; rewrite hl_//; exact/measurable_xsection.
  apply: ge0_emeasurable_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 { } { : measurableType d} { : measurableType d'} { : realType}
( : X -> Y).

Definition ( : measurable_fun [set: X] f) ( : X) :
{measure set Y -> \bar R} := dirac (f x).

Hypothesis : measurable_fun [set: X] f.

Import MeasurableR.

Let : measurable U ->
measurable_fun [set: X] (kdirac mf ^~ U).

Proof.

move=> mU; apply/measurable_EFinP.
by rewrite (_ : (fun => _) = mindic R mU \o f)//; exact/measurableT_comp.
Qed.

..Build _ _ _ _ _ (kdirac mf)
measurable_fun_kdirac.

Let : kdirac mf x [set: Y] = 1.

Proof.

by rewrite /kdirac/= diracT. Qed.

..Build _ _ _ _ _
  (kdirac mf) kdirac_prob.

End kdirac.
Arguments kdirac {d d' X Y R f}.

Section kprobability.
Context ( : measurableType d) ( : measurableType d') ( : realType).
Variable : X -> pprobability Y R.

Definition ( : measurable_fun [set: X] P)
  : X -> {measure set Y -> \bar R} := P.

Hypothesis : measurable_fun [set: X] P.

Let : measurable U ->
  measurable_fun [set: X] (kprobability mP ^~ U).

Proof.

move=> mU.
apply: (measurability _ (ErealGenInftyO.measurableE R)) => _ /= -[_ [r ->] <-].
rewrite setTI preimage_itvNyo -/(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.

.
.Build _ _ X Y R (kprobability mP) measurable_fun_kprobability.

Let : kprobability mP x [set: Y] = 1.

Proof.

by rewrite /kprobability/= probability_setT. Qed.

.
.Build _ _ X Y R (kprobability mP) kprobability_prob.

End kprobability.

Section kadd.
Context ( : measurableType d) ( : measurableType d') ( : realType).
Variables : R.-ker X ~> Y.

Definition ( : X) : {measure set Y -> \bar R} :=
measure_add (k1 x) (k2 x).

Let : measurable U -> measurable_fun [set: X] (kadd ^~ U).

Proof.

move=> mU; rewrite /kadd.
rewrite (_ : (fun _ => _) = (fun => k1 x U + k2 x U)).
by apply/funext => x; rewrite -measure_addE.
by apply: emeasurable_funD; exact/measurable_kernel.
Qed.

.
  .Build _ _ _ _ _ kadd measurable_fun_kadd.

End kadd.

Section sfkadd.
Context ( : measurableType d) ( : measurableType d') ( : realType).
Variables : R.-sfker X ~> Y.

Let : exists2 : (R.-ker _ ~> _)^nat,
  forall , measure_fam_uub (k_ n) &
  forall , measurable U ->
    kadd k1 k2 x U = mseries (k_ ^~ x) 0 U.

Proof.

have [f1 hk1] := sfinite_kernel k1; have [f2 hk2] := sfinite_kernel k2.
exists (fun => 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 lteD.
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.

.
isSFiniteKernel_subdef.Build _ _ _ _ R (kadd k1 k2) sfinite_kadd.

End sfkadd.

Section fkadd.
Context ( : measurableType d) ( : measurableType d') ( : realType).
Variables : R.-fker X ~> Y.

Let : 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: lteD.
Qed.

.
  Kernel_isFinite.Build _ _ _ _ R (kadd k1 k2) kadd_finite_uub.

End fkadd.

Section knormalize.
Context { } { : measurableType d} { : measurableType d'} { : realType}
( : R.-ker X ~> Y).

Definition ( : probability Y R) : X -> {measure set Y -> \bar R} :=
  fun => mnormalize (f x) P.

Import MeasurableR.

Let ( : probability Y R) :
  measurable U -> measurable_fun [set: X] (knormalize P ^~ U).

Proof.

move=> mU; rewrite /knormalize/= /mnormalize /=.
rewrite (_ : (fun _ => _) = (fun =>
     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)).
  apply/funext => x; case: ifPn => [/orP[->//|->]|]; first by case: ifPn.
  by rewrite negb_or=> /andP[/negbTE -> /negbTE ->].
apply: measurable_fun_if => //; [exact: kernel_measurable_fun_eq_cst|].
apply: measurable_fun_if => //.
- rewrite setTI [X in measurable X](_ : _ = [set | f t setT != 0]).
    by apply/seteqP; split => [x /negbT//|x /negbTE].
  exact: kernel_measurable_neq_cst.
- by apply: measurable_funTS => //; exact: kernel_measurable_fun_eq_cst.
- apply: emeasurable_funM.
    exact: measurable_funS (measurable_kernel f U mU).
  apply/measurable_EFinP.
  apply: (@measurable_comp _ _ _ _ _ _ [set : 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: measurableT_comp => //=.
    by have := measurable_kernel f _ measurableT; exact: measurable_funS.
Qed.

. ( Y R) :=
isKernel.Build _ _ _ _ R (knormalize P) (measurable_knormalize P).

Let ( : probability Y R) : knormalize P x [set: Y] = 1.

Proof.

by rewrite /knormalize/= probability_setT. Qed.

. ( Y R):=
  @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) (knormalize1 P).

End knormalize.

Import MeasurableR.

Lemma ( : measurableType d)
    ( : pmeasurableType d') ( : realType) ( : R.-ker X ~> Y) :
  measurable_fun [set: X] (fun => mnormalize (k x) point : pprobability Y R).

Proof.

apply: (measurability (@pset _ _ _ : set_system (pprobability Y R))) => //.
move=> _ -[_ [r r01] [Ys mYs <-]] <-.
rewrite /mnormalize /mset /preimage/=.
apply: emeasurable_fun_infty_o => //.
rewrite /mnormalize/=.
rewrite (_ : (fun => _) = (fun => if (k x setT == 0) || (k x setT == +oo)
    then \d_point Ys else k x Ys * ((fine (k x setT))^-1)%:E)).
  by apply/funext => x/=; case: ifPn.
apply: measurable_fun_if => //.
- apply: (measurable_fun_bool true) => //.
  rewrite (_ : _ @^-1` _ = [set | k t setT == 0] `|`
                           [set | k t setT == +oo]).
    by apply/seteqP; split=> x /= /orP.
  by rewrite setTI; apply: measurableU; exact: kernel_measurable_eq_cst.
- apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel.
  apply/measurable_EFinP; rewrite setTI.
  apply: (@measurable_comp _ _ _ _ _ _ [set : 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.
  + by apply: measurableT_comp => //; exact/measurable_funS/measurable_kernel.
Qed.

Section kcomp_def.
Context ( : measurableType d1) ( : measurableType d2)
( : measurableType d3) ( : realType).
Variable : X -> {measure set Y -> \bar R}.
Variable : X * Y -> {measure set Z -> \bar R}.

Definition ( : set Z) := \int[l x]_ k (x, y) U.

End kcomp_def.

Section kcomp_is_measure.
Context ( : measurableType d1) ( : measurableType d2)
( : measurableType d3) ( : realType).
Variables ( : R.-ker X ~> Y) ( : R.-ker (X * Y) ~> Z).

Let : kcomp l k x set0 = 0.

Proof.

by rewrite /kcomp (eq_integral (cst 0)) ?integral0// => y _; rewrite measure0.
Qed.

Let : 0 <= kcomp l k x U

Proof.

exact: integral_ge0. Qed.

Let : semi_sigma_additive (kcomp l k x).

Proof.

move=> U mU tU mUU; rewrite [X in _ --> X](_ : _ =
  \int[l x]_ (\sum_( <oo) k (x, y) (U n))).
  apply: eq_integral => 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.
exact: measurableT_comp (measurable_kernel k _ (mU n)) _.
Qed.

..Build _ _ R
  (kcomp l k x) (kcomp0 x) (kcomp_ge0 x) (@kcomp_sigma_additive x).

Definition : X -> {measure set Z -> \bar R} := kcomp l k.

End kcomp_is_measure.

Notation := (mkcomp l k) : ereal_scope.

Module .

Section kcomp_finite_kernel_kernel.
Context ( : measurableType d) ( : measurableType d')
  ( : measurableType d3) ( : realType) ( : R.-fker X ~> Y)
  ( : R.-ker (X * Y) ~> Z).

Lemma :
  measurable U -> measurable_fun [set: X] ((l \; k) ^~ U).

Proof.

move=> mU; apply: (measurable_fun_integral_finite_kernel (k ^~ U)) => //=.
exact/measurable_kernel.
Qed.

.
isKernel.Build _ _ X Z R (l \; k) measurable_fun_kcomp_finite.

End kcomp_finite_kernel_kernel.

Section kcomp_finite_kernel_finite.
Context ( : measurableType d) ( : measurableType d')
( : measurableType d3) ( : realType).
Variables ( : R.-fker X ~> Y) ( : R.-fker (X * Y) ~> Z).

Let : measure_fam_uub (kcomp 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 => //.
  - exact: measurableT_comp (measurable_kernel k _ measurableT) _.
  - by move=> y _; exact/ltW/hr.
by rewrite integral_cst//= EFinM lte_pmul2l.
Qed.

.
  Kernel_isFinite.Build _ _ X Z R (l \; k) mkcomp_finite.

End kcomp_finite_kernel_finite.
End KCOMP_FINITE_KERNEL.

Section kcomp_sfinite_kernel.
Context ( : measurableType d) ( : measurableType d')
  ( : measurableType d3) ( : realType).
Variable ( : R.-sfker X ~> Y) ( : R.-sfker (X * Y) ~> Z).

Import KCOMP_FINITE_KERNEL.

Lemma : exists : (R.-fker X ~> Z)^nat,
  forall , measurable U -> (l \; k) x U = kseries k_ x U.

Proof.

have [k_ hk_] := sfinite_kernel k; have [l_ hl_] := sfinite_kernel l.
have [kl hkl] : exists : (R.-fker X ~> Z) ^nat, forall ,
    \esum_( in setT) (l_ i.2 \; k_ i.1) x U = \sum_( <oo) kl i x U.
  have /ppcard_eqP[f] : ([set: nat] #= [set: nat * nat])%card.
    by rewrite card_eq_sym; exact: card_nat2.
  exists (fun => l_ (f i).2 \; k_ (f i).1) => x U.
  by rewrite (reindex_esum [set: nat] _ f)// nneseries_esumT.
exists kl => x U mU.
transitivity ((kseries l_ \; kseries k_) x U).
  rewrite /= /kcomp [in RHS](eq_measure_integral (l x)).
    by move=> *; rewrite hl_.
  by apply: eq_integral => y _; rewrite hk_.
rewrite /= /kcomp/= integral_nneseries//=.
  by move=> n; exact: measurableT_comp (measurable_kernel (k_ n) _ mU) _.
transitivity (\sum_( <oo) \sum_( <oo) (l_ j \; k_ i) x U).
  apply: eq_eseriesr => i _; rewrite integral_kseries//.
  by exact: measurableT_comp (measurable_kernel (k_ i) _ mU) _.
rewrite /mseries -hkl/=.
rewrite (_ : setT = setT `*`` (fun=> setT)); first by apply/seteqP; split.
rewrite -(@esum_esum _ _ _ _ _ (fun => (l_ j \; k_ i) x U))//.
rewrite nneseries_esumT; first by move=> *; exact: nneseries_ge0.
by apply: eq_esum => /= i _; rewrite nneseries_esumT.
Qed.

Lemma : measurable U ->
measurable_fun [set: X] ((l \; k) ^~ U).

Proof.

move=> mU; apply: (measurable_fun_integral_sfinite_kernel (k ^~ U)) => //.
exact/measurable_kernel.
Qed.

End kcomp_sfinite_kernel.

Module .
Section kcomp_sfinite_kernel.
Context ( : measurableType d) ( : measurableType d')
  ( : measurableType d3) ( : realType).
Variables ( : R.-sfker X ~> Y) ( : R.-sfker (X * Y) ~> Z).

.
  isKernel.Build _ _ X Z R (l \; k) (measurable_fun_mkcomp_sfinite l k).

.
  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 ( : measurableType d) ( : measurableType d') ( : realType).
Import HBNNSimple.
Variables ( : Y -> \bar R)
  ( : ({nnsfun Y >-> R}) ^nat)
  ( : nondecreasing_seq (k_ : (Y -> R)^nat))
  ( : forall , [set: Y] z -> (k_ n z)%:E @[ --> \oo] --> k z).

Let : (X * Y -> R)^nat := fun => k_ n \o snd.

Let : (0 <= k_2 n x)%R

Proof.

by []. Qed.

..Build _ _ _ (k_2_ge0 n).

Let : measurable_fun [set: X * Y] (k_2 n).

Proof.

by apply: measurableT_comp => //; exact: measurable_snd. Qed.

..Build _ _ _ _ _ (mk_2 n).

Let : finite_set (range (k_2 n)).

Proof.

have [[point _]|/forallNP empty] := pselect (exists : X, True).
  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].
by rewrite (_ : range _ = set0)// -subset0 => r [[x]]; have := empty x.
Qed.

..Build _ _ _ (fk_2 n).

Lemma ( : X -> {measure set Y -> \bar R}) :
(forall , measurable_fun [set: X] (l ^~ (k_ n @^-1` [set r]))) ->
measurable_fun [set: X] (fun => \int[l x]_ k z).

Proof.

move=> h; apply: (measurable_fun_xsection_integral (k \o snd) l k_2) => /=.
- 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 => 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.

Section measurable_fun_integral_kernel.

Import HBNNSimple.

Lemma
     ( : measurableType d) ( : measurableType d') ( : realType)
    ( : X -> {measure set Y -> \bar R})
    ( : forall , measurable U -> measurable_fun [set: X] (l ^~ U))
    ( : Y -> \bar R) ( : forall , 0 <= k z) ( : measurable_fun [set: Y] k) :
  measurable_fun [set: X] (fun => \int[l x]_ k y).

Proof.

pose k_ := nnsfun_approx measurableT mk.
apply: (@measurable_fun_preimage_integral _ _ _ _ _ _ k_) => //.
- by move=> a b ab; exact/nd_nnsfun_approx.
- by move=> z _; exact/cvg_nnsfun_approx.
- by move=> n r; exact/ml.
Qed.

End measurable_fun_integral_kernel.

Section integral_kcomp.
Context ( : measurableType d) ( : measurableType d2)
( : measurableType d3) ( : realType).
Variables ( : R.-sfker X ~> Y) ( : R.-sfker (X * Y) ~> Z).

Let ( : measurable E) :
\int[kcomp l k x]_ (\1_E z)%:E = \int[l x]_ (\int[k (x, y)]_ (\1_E z)%:E).

Proof.

rewrite integral_indic//= /kcomp.
by apply: eq_integral => y _; rewrite integral_indic.
Qed.

Import HBNNSimple.

Let ( : {nnsfun Z >-> R}) :
\int[kcomp l k x]_ (f z)%:E = \int[l x]_ (\int[k (x, y)]_ (f z)%:E).

Proof.

under [in LHS]eq_integral do rewrite fimfunE -fsumEFin//.
rewrite ge0_integral_fsum//.
- by move=> r; exact/measurable_EFinP/measurableT_comp.
- 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//.
  - by move=> r; exact/measurable_EFinP/measurableT_comp.
  - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0.
  under eq_fsbigr.
    move=> r _.
    rewrite (integralZl_indic _ (fun => f @^-1` [set r]))//.
      by move=> r0; rewrite preimage_nnfun0.
    rewrite integral_indic// setIT.
    over.
  over.
rewrite /= ge0_integral_fsum//.
  - move=> r; apply: measurable_funeM.
    exact: measurableT_comp (measurable_kernel k (f @^-1` [set r]) _) _.
  - move=> n y _.
    have := mulemu_ge0 (fun => f @^-1` [set n]).
    by apply; exact: preimage_nnfun0.
apply: eq_fsbigr => r _.
rewrite (integralZl_indic _ (fun => f @^-1` [set r]))//.
  exact: preimage_nnfun0.
rewrite /= integral_kcomp_indic//.
have [r0|r0] := leP 0%R r.
  rewrite ge0_integralZl//.
    exact: measurableT_comp (measurable_kernel k (f @^-1` [set r]) _) _.
  by under eq_integral do rewrite integral_indic// setIT.
rewrite integral0_eq ?mule0.
  by move=> y _; rewrite integral0_eq// => z _; rewrite preimage_nnfun0// indic0.
by rewrite integral0_eq// => y _; rewrite preimage_nnfun0// measure0 mule0.
Qed.

Lemma : (forall , 0 <= f z) -> measurable_fun [set: Z] f ->
\int[kcomp l k x]_ f z = \int[l x]_ (\int[k (x, y)]_ f z).

Proof.

move=> f0 mf.
pose f_ := nnsfun_approx measurableT mf.
transitivity (\int[kcomp l k x]_ (lim ((f_ n z)%:E @[ --> \oo]))).
  by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: cvg_nnsfun_approx.
rewrite monotone_convergence//.
  by move=> n; exact/measurable_EFinP.
  by move=> n z _; rewrite lee_fin.
  by move=> z _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
rewrite (_ : (fun _ => _) =
    (fun => \int[l x]_ (\int[k (x, y)]_ (f_ n z)%:E)))//.
  by apply/funext => n; rewrite integral_kcomp_nnsfun.
transitivity (\int[l x]_ lim ((\int[k (x, y)]_ (f_ n z)%:E) @[ --> \oo])).
  rewrite -monotone_convergence//; last 3 first.
  - move=> n; apply: measurable_fun_integral_kernel => //.
    + by move=> U mU; exact: measurableT_comp (measurable_kernel k _ mU) _.
    + by move=> z; rewrite lee_fin.
    + exact/measurable_EFinP.
  - 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/measurable_EFinP.
    + exact/measurable_EFinP.
    + by move=> z _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
apply: eq_integral => y _; rewrite -monotone_convergence//.
  - by move=> n; exact/measurable_EFinP.
  - by move=> n z _; rewrite lee_fin.
  - by move=> z _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
by apply: eq_integral => z _; apply/cvg_lim => //; exact: cvg_nnsfun_approx.
Qed.

End integral_kcomp.

Section kfcomp.
Context {} {} { : measurableType d1} { : measurableType d2}
  { : realType}.

Definition ( : T1 -> {measure set T2 -> \bar R})
    ( : T1 * T2 -> \bar R) : T1 -> \bar R :=
  fun => \int[k x]_ f (x, y).

Lemma ( : T1 -> {measure set T2 -> \bar R}) :
  kfcomp k (EFin \o cst 1%R) = (k ^~ [set: T2]).

Proof.

by apply/funext => x/=; rewrite /kfcomp/= integral_cst// mul1e. Qed.

Lemma ( : T1 -> {measure set T2 -> \bar R}) : measurable A ->
kfcomp k (EFin \o \1_A) = (fun => k x (xsection A x)).

Proof.

move=> mA; apply/funext=> x; rewrite /kfcomp /= integral_indic// ?setIT//.
- rewrite -[X in measurable X]/(_ @^-1` _) -xsectionE.
exact: measurable_xsection.
- by rewrite -[X in k x X = _]/(_ @^-1` _) -xsectionE.
Qed.

End kfcomp.

Section measurable_kfcomp.

Let ( : measurableType d) ( : realType)
( : {measure set T -> \bar R}) :
fin_num_fun mu -> sigma_finite [set: T] mu.

Proof.

by move=> fmu; apply: fin_num_fun_sigma_finite => //; rewrite measure0.
Qed.

Let ( : measurableType d) ( : realType)
( : {measure set T -> \bar R}) :
fin_num_fun mu -> sfinite_measure mu.

Proof.

move=> fmu.
exists (fun => if n is O then mu else mzero) => [[]//|U mU].
by rewrite /mseries nneseries_recl// eseries0 ?adde0// => -[|].
Qed.

Variables ( : measure_display) ( : measurableType d1)
  ( : measurableType d2) ( : realType) ( : R.-ftker T1 ~> T2)
  ( : T1 * T2 -> \bar R).

Let ( : set T1) ( : set T2) : T1 * T2 -> \bar R := EFin \o \1_(A1 `*` A2).

Let ( : set T1) ( : set T2) : measurable A1 -> measurable A2 ->
  kfcomp k (g A1 A2) = (fun => (\1_A1 x)%:E * k x A2).

Proof.

move=> mA1 mA2; apply/funext => x.
rewrite /kfcomp /g/= integral_indic//.
  rewrite [X in measurable X](_ : _ = xsection (A1 `*` A2) x).
    by rewrite xsectionE.
  by apply: measurable_xsection; exact: measurableX.
have [xA1|xA1] := boolP (x \in A1).
  by rewrite indicE xA1 mul1e setIT -[X in _ _ X = _]xsectionE in_xsectionX.
rewrite indicE (negbTE xA1) mul0e setIT.
by rewrite -[X in _ _ X = _]xsectionE notin_xsectionX.
Qed.

Let := [set | measurable A /\ measurable_fun setT (kfcomp k (EFin \o \1_A))].

Let : setSD_closed D.

Proof.

move=> B A AB; rewrite /D/= => -[mB mIB] [mA mIA].
suff KE : kfcomp k (EFin \o \1_(B `\` A)) =
    kfcomp k (EFin \o \1_B) \- kfcomp k(EFin \o \1_A).
  by split; [exact: measurableD|rewrite KE; exact: emeasurable_funB].
apply/funext => x/=.
pose kx : {measure set T2 -> \bar R} := k x.
pose H1 := isFinNumFun.Build _ _ _ _ (@kernel_finite_transition _ _ _ _ R k x).
pose H2 := isSFinite.Build _ _ _ _ (finite_measure_sfinite
  (@kernel_finite_transition _ _ _ _ R k x)).
pose H3 := isSigmaFinite.Build _ _ _ _ (finite_measure_sigma_finite
  (@kernel_finite_transition _ _ _ _ R k x)).
pose kx' := HB.pack_for (FiniteMeasure.type T2 R) (Measure.sort kx) H1 H2 H3.
have kxE : kx = kx' by exact: eq_measure.
rewrite [in RHS]/kfcomp -integralB_EFin//.
- rewrite -/kx kxE; apply: integrable_indic => //.
  by rewrite -[X in measurable X]xsectionE; exact: measurable_xsection.
- rewrite -/kx kxE; apply: integrable_indic => //.
  by rewrite -[X in measurable X]xsectionE; exact: measurable_xsection.
apply: eq_integral => y _/=; rewrite setDE indicI indicC/=.
rewrite -[in RHS](setCK A) indicC in_setC.
have [xyA|xyA] := boolP (_ \in A); rewrite /= ?mulr1 ?mulr0 ?oppr0 ?adde0//.
by move/set_mem : xyA => /AB Bxy; rewrite indicE mem_set//= EFinN subee.
Qed.

Let : lambda_system setT D.

Proof.

split => //.
- by rewrite /D/= indicT kfcompk1; split => //; exact: measurable_kernel.
- suff: D = [set | (d1, d2).-prod.-measurable A /\
         measurable_fun [set: T1] ((fun => k x (xsection C x)) A)].
    by move=> ->; exact: xsection_ndseq_closed.
  apply/seteqP; split=> [/= A [mA /= mIA]|/= A [/= mA mIA]].
  + by split => //; rewrite -kfcompkindic.
  + by split => //; rewrite kfcompkindic.
Qed.

Import HBNNSimple.

Lemma : measurable_fun [set: T1 * T2] f ->
(forall , 0 <= f t) -> measurable_fun [set: T1] (kfcomp k f).

Proof.

move=> mf f0.
pose f_ := nnsfun_approx measurableT mf.
pose K := kfcomp k.
have Kf_cvg x : K (EFin \o f_ n) x @[ --> \oo] --> K f x.
  pose g' := (EFin \o f_ n) (x, y).
  rewrite [X in _ --> X](_ : _ =
      \int[k x]_ (fun => limn (g' ^~ t)) y).
    apply: eq_integral => y _.
    by apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
  apply: cvg_monotone_convergence => //.
  - by move=> n; apply/measurable_EFinP; exact: measurableT_comp.
  - by move=> n y _; rewrite /= lee_fin.
  - by move=> y _ a b ab/=; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
apply: (emeasurable_fun_cvg (fun => K (EFin \o f_ n))); last first.
  by move=> ? _; exact: Kf_cvg.
move=> m.
have DE : D = @measurable _ (T1 * T2)%type.
  apply/seteqP; split => [/= A []//|].
  rewrite prod_measurable_rectangle.
  apply: lambda_system_subset => //=.
    by apply: setI_closed_rectangle => *; exact: measurableI.
  move=> C [A mA [B mB] <-].
  split; [exact: measurableX|rewrite /K kfcompkg//].
  by apply: emeasurable_funM; [exact/measurable_EFinP|exact: measurable_kernel].
have mK1 ( : set (T1 * T2)) : measurable A ->
    measurable_fun setT (K (EFin \o \1_A)).
  by rewrite -DE => -[].
rewrite [X in measurable_fun _ X](_ : _ = K
    (EFin \o (fun => \sum_( \in range (f_ m)) y *
                       \1_(f_ m @^-1` [set y]) x))%R).
  by apply/funext => x/=; apply: eq_integral => y _ /=; rewrite fimfunE.
rewrite /I/= [X in measurable_fun _ X](_ : _ = (fun =>
   \sum_( \in range (f_ m))
     (\int[k x]_ (y * \1_(f_ m @^-1` [set y]) (x, w2))%:E))).
  apply/funext => x; rewrite /K /kfcomp.
  under eq_integral do rewrite /= -fsumEFin//.
  rewrite /= ge0_integral_fsum//=.
    move=> r.
    under eq_fun do rewrite EFinM.
    by apply: emeasurable_funM => //; exact/measurable_EFinP/measurableT_comp.
  by move=> r y _; rewrite EFinM nnfun_muleindic_ge0.
apply: emeasurable_fsum => // r.
rewrite [X in measurable_fun _ X](_ : _ = (fun =>
    (r%:E * \int[k x]_ (\1_(f_ m @^-1` [set r]) (x, y))%:E))).
  apply/funext => x.
  under eq_integral do rewrite EFinM.
  rewrite integralZl//.
  pose kx : {measure set T2 -> \bar R} := k x.
  pose H1 := isFinNumFun.Build _ _ _ _ (@kernel_finite_transition _ _ _ _ R k x).
  pose H2 := isSFinite.Build _ _ _ _ (finite_measure_sfinite
    (@kernel_finite_transition _ _ _ _ R k x)).
  pose H3 := isSigmaFinite.Build _ _ _ _ (finite_measure_sigma_finite
    (@kernel_finite_transition _ _ _ _ R k x)).
  pose kx' := HB.pack_for (FiniteMeasure.type T2 R) (Measure.sort kx) H1 H2 H3.
  have kxE : kx = kx' by exact: eq_measure.
  rewrite -/kx kxE; apply: integrable_indic => //.
  by rewrite -[X in measurable X]xsectionE; exact: measurable_xsection.
by apply: emeasurable_funM => //; exact: mK1.
Qed.

End measurable_kfcomp.

Section kproduct_def.
Context ( : measurableType d0) ( : measurableType d1)
  ( : measurableType d2) { : realType}.
Variable : T0 -> {measure set T1 -> \bar R}.
Variable : T0 * T1 -> {measure set T2 -> \bar R}.

Local Definition ( : T0 * T1 -> {measure set T2 -> \bar R}) :=
  fun => \int[k xy]_ (\1_A (xy.2, z))%:E.

Definition ( : set (T1 * T2)) :=
  \int[k1 x]_ intker_indic k2 A (x, y).

End kproduct_def.

Section intker_indic_lemmas.
Context ( : measurableType d0)
  ( : measurableType d1) ( : measurableType d2) { : realType}.
Variable : R.-ftker T0 * T1 ~> T2.

Local Lemma : measurable A ->
  measurable_fun [set: T0 * T1] (intker_indic k A).

Proof.

move=> mA; apply: (@measurable_kfcomp _ _ (T0 * T1)%type T2 R k
    (fun => (\1_A (abc.1.2, abc.2))%:E)) => //.
apply/measurable_EFinP => //=; apply: measurableT_comp => //=.
apply/measurable_fun_pairP; split => /=.
  rewrite [X in measurable_fun _ X](_ : _ = snd \o fst)//.
  exact: measurableT_comp.
by rewrite [X in measurable_fun _ X](_ : _ = snd).
Qed.

Local Lemma : measurable A ->
intker_indic k A (x, y) = k (x, y) (xsection A y).

Proof.

move=> mA; rewrite /intker_indic(*NB:lemma?*) integral_indic//.
by rewrite -[X in measurable X]xsectionE; exact: measurable_xsection.
by rewrite setIT xsectionE.
Qed.

Local Lemma ( : (set (T1 * T2)) ^nat) :
  trivIset [set: nat] A -> (forall , measurable (A n)) ->
  intker_indic k (\bigcup_ A n) (x, y) =
  \big[+%R/0%R]_(0 <= <oo) intker_indic k (A i) (x, y).

Proof.

move=> tA mA.
rewrite /intker_indic -(@integral_nneseries _ _ R (k (x, y)) _ measurableT
(fun => (\1_(A i) (y, z))%:E))//.
- move=> n; apply/measurable_EFinP => //; apply: measurable_indic.
by rewrite -[X in measurable X]xsectionE; exact: measurable_xsection.
- by apply: eq_integral => z _ /=; rewrite indic_bigcup.
Qed.

End intker_indic_lemmas.

Section kproduct_snd_def.
Context ( : measurableType d0) ( : measurableType d1)
  ( : measurableType d2) { : realType}.
Variable : T0 -> {measure set T1 -> \bar R}.
Variable : T1 -> {measure set T2 -> \bar R}.

Definition   : T0 -> set (T1 * T2) -> \bar R :=
  kproduct k1 (k2 \o snd).

End kproduct_snd_def.

Theorem ( : measurableType d0)
    ( : measurableType d1) ( : measurableType d2) { : realType}
    ( : R.-ftker T0 ~> T1) ( : R.-ftker (T0 * T1) ~> T2) :
  measurable A -> measurable_fun [set: T0] (kproduct k1 k2 ^~ A).

Proof.

move=> mA; apply: measurable_kfcomp => // t.
exact: measurable_intker_indic.
by apply: integral_ge0 => y _; rewrite lee_fin.
Qed.

Theorem ( : measurableType d0)
    ( : measurableType d1) ( : measurableType d2) { : realType}
    ( : R.-ftker T0 ~> T1) ( : R.-ftker (T0 * T1) ~> T2) :
  semi_sigma_additive (kproduct k1 k2 x).

Proof.

move=> /= A mA tA mbigcup.
rewrite (_ : (fun => _) = (fun =>
    \int[k1 x]_ (\sum_(0 <= < n) intker_indic k2 (A i) (x, y)))).
  apply/funext => n; rewrite ge0_integral_sum//.
    by move=> m; exact: measurable_fun_pair2 (measurable_intker_indic k2 _).
  by move=> m y _; rewrite intker_indicE.
pose g := \sum_(0 <= < n) intker_indic k2 (A i) (x, y).
rewrite [X in _ --> X](_ : _ = \int[k1 x]_ limn (g ^~ y)).
  by apply: eq_integral => y _; rewrite /g intker_indic_bigcup.
apply: (@cvg_monotone_convergence _ _ _ (k1 x) _ measurableT g) => //.
- move=> n; apply: (@emeasurable_sum _ _ R setT _ _
    (fun => intker_indic k2 (A i) (x, t))) => m.
  exact: measurable_fun_pair2 (measurable_intker_indic k2 (mA m)).
- by move=> n y _; apply: sume_ge0 => m _; rewrite intker_indicE.
- move=> y _ a b ab; apply: lee_sum_nneg_natr => // m _ _.
  by rewrite intker_indicE.
Qed.

Section kproduct_measure.
Context ( : measurableType d0)
( : measurableType d1) ( : measurableType d2) { : realType}
( : R.-ftker T0 ~> T1) ( : R.-ftker (T0 * T1) ~> T2).

Let : kproduct k1 k2 x set0 = 0.

Proof.

by apply: integral0_eq => y _; apply: integral0_eq => z _; rewrite indic0.
Qed.

Let : 0 <= kproduct k1 k2 x A.

Proof.

by apply: integral_ge0 => y _; apply: integral_ge0 => z _; rewrite lee_fin.
Qed.

Let : semi_sigma_additive (kproduct k1 k2 x).

Proof.

exact: semi_sigma_additive_kproduct. Qed.

..Build
  (measure_prod_display (d1, d2)) (T1 * T2)%type R (kproduct k1 k2 x)
  (kproduct0 x) (kproduct_ge0 x) (@kproduct_additive x).

Definition :=
  (kproduct k1 k2 : T0 -> {measure set (T1 * T2) -> \bar R}).

End kproduct_measure.

. ( d0)
    (T1 : measurableType d1) (T2 : measurableType d2) {R : realType}
    (k1 : R.-ftker T0 ~> T1) (k2 : R.-ftker (T0 * T1) ~> T2) :=
  @isKernel.Build _ _ T0 (T1 * T2)%type R
    (mkproduct k1 k2) (measurable_kproduct k1 k2).

Section sigma_finite_kproduct.
Context ( : measurableType d0)
  ( : measurableType d1) ( : measurableType d2) { : realType}
  ( : R.-ftker T0 ~> T1) ( : R.-ftker (T0 * T1) ~> T2).

Theorem :
  sigma_finite [set: T1 * T2] (mkproduct k1 k2 x).

Proof.

pose A := [set | k2 (x, w1) setT < n%:R%:E].
have mA n : measurable (A n).
  rewrite /A -[X in measurable X]setTI.
  apply: emeasurable_fun_infty_o => //.
  have := @measurable_kernel _ _ _ _ R k2 _ measurableT.
  exact: measurable_fun_pair2.
have bigcupA : \bigcup_ A n = setT.
  have fink2 xy : fin_num_fun (k2 xy) by exact: kernel_finite_transition.
  apply/seteqP; split => // y _.
  have {}fink2 := fink2 (x, y) _ measurableT.
  exists (Num.truncn (fine (k2 (x, y) setT))).+1 => //=.
  have : (0 <= fine (k2 (x, y) [set: T2]))%R by rewrite fine_ge0.
  by move=> /truncn_itv/andP[_]; rewrite -lte_fin fineK.
have lty n : kproduct k1 k2 x (A n `*` setT) < +oo.
  have fink1 : fin_num_fun (k1 x) by exact: kernel_finite_transition.
  apply: (@le_lt_trans _ _ (n%:R%:E * k1 x (A n))) => /=.
    rewrite [leLHS](_ : _ = \int[k1 x]_( in A n) k2 (x, y) setT).
      rewrite /kproduct [RHS]integral_mkcond; apply: eq_integral => y _.
      rewrite intker_indicE//; first exact: measurableX.
      rewrite patchE; case: ifPn => [Anx|Anx].
        by rewrite in_xsectionX.
      by rewrite notin_xsectionX// measure0.
    apply: (@le_trans _ _ (\int[k1 x]_( in A n) n%:R%:E)).
      apply: ge0_le_integral => //.
      - apply: measurable_funTS.
        have := @measurable_kernel _ _ _ _ _ k2 _ measurableT.
        exact: measurable_fun_pair2.
      - by move=> y; rewrite /A/= => /ltW.
      - by rewrite integral_cst.
    by rewrite lte_mul_pinfty// ltey_eq fink1.
exists (fun => A n `*` setT) => /=.
  by rewrite -setX_bigcupl bigcupA setXTT.
by move=> n; split => //; exact: measurableX.
Qed.

..Build d0
  (measure_prod_display (d1, d2)) T0 (T1 * T2)%type R
    (mkproduct k1 k2) sigma_finite_mkproduct.

End sigma_finite_kproduct.

Section kcomp_noparam_def.
Context ( : measurableType d0) ( : measurableType d1)
  ( : measurableType d2) { : realType}.
Variable : T0 -> {measure set T1 -> \bar R}.
Variable : T1 -> {measure set T2 -> \bar R}.

Definition ( : T0) ( : set T2) : \bar R :=
  \int[k1 x]_ (k2 y A).

End kcomp_noparam_def.

Section spker_snd.
Context ( : measurableType d0)
  ( : measurableType d1) ( : measurableType d2) { : realType}
  ( : R.-spker T1 ~> T2).

Local Definition : (T0 * T1)%type -> {measure set T2 -> \bar R} :=
  k \o snd.

Let : measurable U ->
  measurable_fun [set: _] (kernel_snd ^~ U).

Proof.

move=> mU; have /= mk1 := measurable_kernel k _ mU.
move=> _ /= Y mY; have {}mk1 := mk1 measurableT _ mY.
have -> : [set: T0 * T1] `&` (kernel_snd ^~ U) @^-1` Y =
setT `*` ([set: T1] `&` (k ^~ U) @^-1` Y).
by rewrite !setTI setTX.
exact: measurableX.
Qed.

.
.Build _ _ _ _ _ kernel_snd measurable_kernel_snd.

Let : measure_fam_uub kernel_snd.

Proof.

exists 2%R => /= -[x y].
rewrite /kernel_snd/= (@le_lt_trans _ _ 1%:E) ?lte1n//.
exact: sprob_kernel_le1.
Qed.

.
.Build _ _ _ _ _ kernel_snd measure_uub_kernel_snd.

Let :
ereal_sup [set kernel_snd z [set: _] | in [set: _]] <= 1.

Proof.

by apply: (sprob_kernelP kernel_snd).2 => -[x y]; exact: sprob_kernel_le1.
Qed.

..Build _ _ _ _ _
kernel_snd sprob_kernel_kernel_snd.

Lemma ( : set T2) : measurable A ->
intker_indic kernel_snd ([set: _] `*` A) (x, y) = k y A.

Proof.

move=> mA; rewrite intker_indicE//=; first exact: measurableX.
by congr (k y _); rewrite xsectionE//= setTX.
Qed.

End spker_snd.

Lemma ( : measurableType d0)
    ( : measurableType d1) ( : measurableType d2) { : realType}
    ( : T0 -> {measure set T1 -> \bar R})
    ( : T1 -> {measure set T2 -> \bar R}) :
  measurable A ->
  kcomp_noparam k1 k2 x A = kproduct_snd k1 k2 x (snd @^-1` A).

Proof.

move=> mA; rewrite /kcomp_noparam /kproduct_snd /kproduct.
apply: eq_integral => y _ /=.
by rewrite /intker_indic/= integral_indic// setIT.
Qed.

Section kcomp_noparam_measure.
Context ( : measurableType d0)
( : measurableType d1) ( : measurableType d2) { : realType}
( : R.-spker T0 ~> T1) ( : R.-spker T1 ~> T2).

Let : kcomp_noparam k1 k2 x set0 = 0.

Proof.

by apply: integral0_eq => y _; rewrite measure0. Qed.

Let : 0 <= kcomp_noparam k1 k2 x A.

Proof.

by apply: integral_ge0 => y _; exact: measure_ge0. Qed.

Let :
semi_sigma_additive (kcomp_noparam k1 k2 x).

Proof.

move=> F mF tF mUF.
rewrite kcomp_noparamE// (_ : (fun _ => _) = (fun =>
    \sum_(0 <= < n) kproduct_snd k1 k2 x (snd @^-1` F i))).
  by apply/funext => n; apply: eq_bigr => k _; rewrite kcomp_noparamE.
pose F' := [set: T1] `*` F n.
have kcomp_noparam_bigcup : kcomp_noparam k1 k2 x (\bigcup_ F n) =
    kproduct k1 (kernel_snd k2) x (\bigcup_ F' n).
  by apply: eq_integral => y _; rewrite -setX_bigcupr intker_indic_snd.
rewrite -kcomp_noparamE// kcomp_noparam_bigcup.
rewrite (_ : (fun => _) = (fun =>
    \sum_(0 <= < n) kproduct k1 (kernel_snd k2) x (F' i))).
  apply/funext => n; apply: eq_bigr => i _.
  apply: eq_integral => y _; apply: eq_integral => z _.
  by rewrite /F' setTX.
apply: semi_sigma_additive_kproduct => //.
- by move=> i; exact: measurableX.
- apply/trivIsetP => i j _ _ ij.
  rewrite /F' -setXI setTI.
  move/trivIsetP : tF => /(_ i j Logic.I Logic.I ij) ->.
  by rewrite setX0.
- by apply: bigcup_measurable => k _; exact: measurableX.
Qed.

..Build d2 T2 R (kcomp_noparam k1 k2 x)
  (kcomp_noparam0 x) (kcomp_noparam_ge0 x) (@kcomp_noparam_additive x).

Definition :=
  (kcomp_noparam k1 k2 : T0 -> {measure set T2 -> \bar R}).

Let :
  measurable U -> measurable_fun [set: _] (mkcomp_noparam ^~ U).

Proof.

move=> mU.
rewrite [X in measurable_fun _ X](_ : _ =
    (kproduct k1 (kernel_snd k2))^~ ([set: T1] `*` U)).
  apply/funext => x.
  by apply: eq_integral => y _; rewrite intker_indic_snd.
by apply: measurable_kproduct; exact: measurableX.
Qed.

..Build _ _ _ _ R
  mkcomp_noparam measurable_kernel_mkcomp_noparam.

End kcomp_noparam_measure.

Section subprobability_kcomp_noparam.
Context ( : measurableType d0)
  ( : measurableType d1) ( : measurableType d2) { : realType}
  ( : R.-spker T0 ~> T1) ( : R.-spker T1 ~> T2).

Lemma : mkcomp_noparam k1 k2 x setT <= 1.

Proof.

rewrite /mkcomp_noparam [leLHS]kcomp_noparamE// preimage_setT.
rewrite /kproduct_snd /kproduct.
rewrite [leLHS](_ : _ = \int[k1 x]_ k2 y setT).
  apply: eq_integral => y _.
  rewrite /intker_indic integral_indic//.
    rewrite [X in measurable X](_ : _ = ysection setT y).
      by rewrite ysectionE.
    exact: measurable_ysection.
  by rewrite setIT.
apply: (@le_trans _ _ (\int[k1 x]__ 1)); last first.
  by rewrite integral_cst// mul1e; exact: sprob_kernel_le1.
apply: ge0_le_integral => //; first exact: measurable_kernel.
by move=> y _; exact: sprob_kernel_le1.
Qed.

Let :
ereal_sup [set (kcomp_noparam k1 k2) x setT | in [set: T0]] <= 1.

Proof.

by apply/sprob_kernelP => x; exact: sprob_mkcomp_noparam. Qed.

..Build
_ _ _ _ R (mkcomp_noparam k1 k2) sprob_kernel_kcomp_noparam.

End subprobability_kcomp_noparam.

Files

Module mathcomp.analysis.kernel