lmodType structure on simple functions valued in a normed module

Co-authored-by: Arthur Djevahirdjian <arthur.djevahirdjian@ens-lyon.fr>

Author: hoheinzollern

CHANGELOG_UNRELEASED.md

@@ -7,6 +7,10 @@
   + definition `borel_type`
   + lemmas `singleton_bigcap`, `measurable1`
 
+- in `simple_functions.v`:
+  + lemmas `sfun_op`, `sfun_submod_closed`
+  + `{sfun aT >-> borel_type V}` is an `lmodType` when `V` is a `normedModType`
+
 - in `set_interval.v`:
   + lemmas `setU_itvob1`, `setU_1itvob`
 

theories/lebesgue_integral_theory/simple_functions.v

@@ -6,6 +6,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality reals fsbigop ereal topology tvs.
 From mathcomp Require Import normedtype sequences real_interval esum measure.
 From mathcomp Require Import lebesgue_measure numfun realfun measurable_realfun.
+From mathcomp Require Import borel_hierarchy.
 
 (**md**************************************************************************)
 (* # Simple functions                                                         *)
@@ -216,6 +217,55 @@ Definition scale_sfun k f : {sfun aT >-> rT} := k \o* f.
 End ring.
 Arguments indic_sfun {d aT rT} _.
 
+Section sfun_lmodType.
+Context d (aT : measurableType d) (R : realType).
+Import HBSimple.
+
+HB.instance Definition _ (V : normedModType R) := GRing.Lmodule.on (borel_type V).
+
+Lemma sfun_op (U V W : normedModType R)
+    (f : {sfun aT >-> borel_type U}) (g : {sfun aT >-> borel_type V})
+    (h : U * V -> W) :
+  (fun x => h (f x, g x)) \in @sfun _ _ aT (borel_type W).
+Proof.
+rewrite inE; apply/andP; split; rewrite inE/=.
+  move=> _ Y mY; rewrite setTI.
+  rewrite (_ : _ @^-1` Y =
+      \bigcup_(a in range f) (\bigcup_(b in range g)
+        ((f @^-1` [set a] `&` g @^-1` [set b]) `&` [set _ | Y (h (a, b))]))).
+    apply/seteqP; split=> [x/= Yfg|x [a _] [b _] [[/= <- <-]]//].
+    by exists (f x); [exists x|exists (g x); [exists x|split]].
+  apply: fin_bigcup_measurable; first exact: fimfunP.
+  move=> a _; apply: fin_bigcup_measurable; first exact: fimfunP.
+  move=> b _; apply: measurableI; last first.
+    have [Yhab|Yhab] := pselect (Y (h (a, b))).
+      by rewrite (_ : [set _ | _] = setT);
+          [apply/seteqP; split|exact: measurableT].
+    rewrite (_ : [set _ | _] = set0); last exact: measurable0.
+    by apply/seteqP; split.
+  apply: measurableI.
+    exact: (measurable_funPTI f (measurable1 a)).
+  exact: (measurable_funPTI g (measurable1 b)).
+apply: (sub_finite_set (B := h @` (range f `*` range g))).
+  by move=> _ [x _ <-]/=; exists (f x, g x) => //; split; exists x.
+by apply: finite_image; apply: finite_setX; exact: fimfunP.
+Qed.
+
+Lemma sfun_submod_closed (V : normedModType R) :
+  submod_closed (@sfun _ _ aT (borel_type V)).
+Proof.
+split=> [|k f g sf sg]; first exact: (valP (cst_sfun (0 : borel_type V))).
+exact: (sfun_op (sfun_Sub sf) (sfun_Sub sg) (fun t => k *: t.1 + t.2)).
+Qed.
+
+HB.instance Definition _ (V : normedModType R) :=
+  GRing.isSubmodClosed.Build _ _ (@sfun _ _ aT (borel_type V))
+    (sfun_submod_closed V).
+HB.instance Definition _ (V : normedModType R) :=
+  [SubChoice_isSubLmodule of {sfun aT >-> borel_type V} by <:].
+
+End sfun_lmodType.
+
 Lemma preimage_nnfun0 T (R : realDomainType) (f : {nnfun T >-> R}) t :
   t < 0 -> f @^-1` [set t] = set0.
 Proof.