proposition: Lemma mkcomp_sfinite : exists k_ : (R.-fker X ~> Z)^nat, forall x U, measurable U -> (l \; k) x U = kseries k_ x U.
proof: Proof. have [k_ hk_] := sfinite_kernel k; have [l_ hl_] := sfinite_kernel l. have [kl hkl] : exists kl : (R.-fker X ~> Z) ^nat, forall x U, \esum_(i in setT) (l_ i.2 \; k_ i.1) x U = \sum_(i <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 i => [the _.-fker _ ~> _ of l_ (f i).2 \; k_ (f i).1]) => x U. by rewrite (reindex_esum [set: nat] _ f)// nneseries_esum// fun_true. exists kl => x U mU. transitivity (([the _.-ker _ ~> _ of kseries l_] \; [the _.-ker _ ~> _ of kseries k_]) x U). rewrite /= /kcomp [in RHS](eq_measure_integral (l x)); last first. by move=> *; rewrite hl_. by apply: eq_integral => y _; rewrite hk_. rewrite /= /kcomp/= integral_nneseries//=; last first. by move=> n; exact: measurableT_comp (measurable_kernel (k_ n) _ mU) _. transitivity (\sum_(i <oo) \sum_(j <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)); last by apply/seteqP; split. rewrite -(@esum_esum _ _ _ _ _ (fun i j => (l_ j \; k_ i) x U))//. rewrite nneseries_esum; last by move=> n _; exact: nneseries_ge0. by rewrite fun_true; apply: eq_esum => /= i _; rewrite nneseries_esum// fun_true. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology normedtype sequences esum measure numfun lebesgue_measure lebesgue_integral