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

@@ -5,18 +5,47 @@ 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 normed_module measurable_structure.
-
-Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-Import Order.TTheory GRing.Theory Num.Def Num.Theory.
-Import numFieldNormedType.Exports.
-
-Local Open Scope classical_set_scope.
-Local Open Scope ring_scope.
-Local Open Scope measure_display_scope.
+From mathcomp Require Import borel_hierarchy.
+
+(**md**************************************************************************)
+(* # Simple functions                                                         *)
+(*                                                                            *)
+(* This file contains a formalization of simple functions and with basic      *)
+(* properties (addition, etc.).                                               *)
+(*                                                                            *)
+(* About the use of simple functions:                                         *)
+(* Because of a limitation of HB <= 1.8.0, we need some care to be able to    *)
+(* use simple functions.                                                      *)
+(* The structure SimpleFun (resp. NonNegSimpleFun) is located inside the      *)
+(* module HBSimple (resp. HBNNSimple).                                        *)
+(* As a consequence, we need to import HBSimple (resp. HBNNSimple) to use the *)
+(* coercion from simple functions (resp. non-negative simple functions) to    *)
+(* Rocq functions.                                                            *)
+(* Also, assume that f (e.g., cst, indic) is equipped with the structure of   *)
+(* MeasurableFun. For f to be equipped with the structure of SimpleFun        *)
+(* (resp. NonNegSimpleFun), one need locally to import HBSimple (resp.        *)
+(* HBNNSimple) and to instantiate FiniteImage (resp. NonNegFun) locally.      *)
+(*                                                                            *)
+(* Detailed contents:                                                         *)
+(* ````                                                                       *)
+(*         {sfun T >-> R} == type of simple functions                         *)
+(*                           They form a (potentially zero) ring.             *)
+(*       {nnsfun T >-> R} == type of non-negative simple functions            *)
+(*          indic_sfun mD := mindic _ mD                                      *)
+(*             cst_sfun r == constant simple function                         *)
+(*           cst_nnsfun r == constant simple function                         *)
+(*                nnsfun0 := cst_nnsfun 0                                     *)
+(*         add_nnsfun f g := f \+ g                                           *)
+(*         mul_nnsfun f g := f \* g                                           *)
+(*         max_nnsfun f g := f \max g                                         *)
+(*       proj_nssfun f mA == projection of the function f to the set A        *)
+(*                            mA is a proof that A is measurable              *)
+(*       scale_nnsfun k f == scales f by the non-negative real number k       *)
+(*         sum_nnsfun f n := \big[add_nnsfun/nnsfun0]_(i < n) f i             *)
+(*      bigmax_nnsfun f n := \big[max_nnsfun/nnsfun0]_(i < n) f i             *)
+(* ````                                                                       *)
+(*                                                                            *)
+(******************************************************************************)
 
 Reserved Notation "{ 'nnfun' aT >-> T }"
   (at level 0, format "{ 'nnfun'  aT  >->  T }").
@@ -209,6 +238,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.