generalize SimpleFun codomain from realType to sigmaRingType

CHANGELOG_UNRELEASED.md

@@ -3,6 +3,14 @@
 ## [Unreleased]
 
 ### Added
+- in `borel_hierarchy.v`:
+  + 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`
 
@@ -254,6 +262,8 @@
 
 - in `simple_functions.v`:
   + lemmas `fctD`, `fctN`, `fctM`, `fctZ`
+  + structure `SimpleFun` (and notation `{sfun aT >-> _}`): codomain
+    generalized from `realType` to `sigmaRingType d'`, adding a display parameter `d'`;
 
 ### Deprecated
 

theories/borel_hierarchy.v

@@ -20,7 +20,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import Order.TTheory GRing.Theory Num.Theory.
+Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Import numFieldNormedType.Exports.
 
 Local Open Scope classical_set_scope.
@@ -80,6 +80,31 @@ Qed.
 
 End irrational_Gdelta.
 
+Definition borel_type (T : topologicalType) := g_sigma_algebraType (@open T).
+
+Section borel_normedModType.
+Local Open Scope ring_scope.
+Context {R : realType} {V : normedModType R}.
+
+Lemma singleton_bigcap (x : V) :
+  [set x] = \bigcap_(k : nat) ball x (k.+1%:R)^-1.
+Proof.
+apply/seteqP; split => [_ -> k _|y xy].
+  by rewrite -ball_normE/= subrr normr0 invr_gt0 ltr0n.
+apply/eqP; rewrite eq_sym -subr_eq0 -normr_eq0 eq_le normr_ge0 andbT.
+apply/ler_addgt0Pl => e e0; rewrite addr0.
+have := xy (truncn e^-1) I; rewrite -ball_normE/= => /ltW/le_trans; apply.
+by rewrite invf_ple ?posrE ?ltr0n ?invr_gt0//; apply/ltW/truncnS_gt.
+Qed.
+
+Lemma measurable1 (x : borel_type V) : measurable [set x].
+Proof.
+rewrite singleton_bigcap; apply: bigcap_measurable => // k _.
+by apply: sub_sigma_algebra; exact: ball_open.
+Qed.
+
+End borel_normedModType.
+
 Lemma not_rational_Gdelta (R : realType) : ~ Gdelta (@rational R).
 Proof.
 apply/forall2NP => A; apply/not_andP => -[oA ratrA].

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                                                         *)
@@ -72,46 +73,49 @@ Local Open Scope ring_scope.
 
 Module HBSimple.
 
-HB.structure Definition SimpleFun d (aT : sigmaRingType d) (rT : realType) :=
-  {f of @isMeasurableFun d _ aT rT f & @FiniteImage aT rT f}.
+HB.structure Definition SimpleFun d d'
+    (aT : sigmaRingType d) (bT : sigmaRingType d') :=
+  {f of @isMeasurableFun d d' aT bT f & @FiniteImage aT bT f}.
 
 End HBSimple.
 
-Notation "{ 'sfun' aT >-> T }" := (@HBSimple.SimpleFun.type _ aT T) : form_scope.
+Notation "{ 'sfun' aT >-> T }" :=
+  (@HBSimple.SimpleFun.type _ _ aT T) : form_scope.
 Notation "[ 'sfun' 'of' f ]" := [the {sfun _ >-> _} of f] : form_scope.
 
 Module HBNNSimple.
 Import HBSimple.
 
 HB.structure Definition NonNegSimpleFun
     d (aT : sigmaRingType d) (rT : realType) :=
-  {f of @SimpleFun d _ _ f & @NonNegFun aT rT f}.
+  {f of @SimpleFun d _ _ _ f & @NonNegFun aT rT f}.
 
 End HBNNSimple.
 
-Notation "{ 'nnsfun' aT >-> T }" := (@HBNNSimple.NonNegSimpleFun.type _ aT%type T) : form_scope.
+Notation "{ 'nnsfun' aT >-> T }" :=
+  (@HBNNSimple.NonNegSimpleFun.type _ aT%type T) : form_scope.
 Notation "[ 'nnsfun' 'of' f ]" := [the {nnsfun _ >-> _} of f] : form_scope.
 
 Section sfun_pred.
-Context {d} {aT : sigmaRingType d} {rT : realType}.
-Definition sfun : {pred _ -> _} := [predI @mfun _ _ aT rT & fimfun].
+Context {d d'} {aT : sigmaRingType d} {bT : sigmaRingType d'}.
+Definition sfun : {pred _ -> _} := [predI @mfun _ _ aT bT & fimfun].
 Definition sfun_key : pred_key sfun. Proof. exact. Qed.
 Canonical sfun_keyed := KeyedPred sfun_key.
 Lemma sub_sfun_mfun : {subset sfun <= mfun}. Proof. by move=> x /andP[]. Qed.
 Lemma sub_sfun_fimfun : {subset sfun <= fimfun}. Proof. by move=> x /andP[]. Qed.
 End sfun_pred.
 
 Section sfun.
-Context {d} {aT : measurableType d} {rT : realType}.
-Notation T := {sfun aT >-> rT}.
-Notation sfun := (@sfun _ aT rT).
+Context {d d'} {aT : measurableType d} {bT : sigmaRingType d'}.
+Notation T := {sfun aT >-> bT}.
+Notation sfun := (@sfun _ _ aT bT).
 Section Sub.
-Context (f : aT -> rT) (fP : f \in sfun).
+Context (f : aT -> bT) (fP : f \in sfun).
 Definition sfun_Sub1_subproof :=
-  @isMeasurableFun.Build d _ aT rT f (set_mem (sub_sfun_mfun fP)).
+  @isMeasurableFun.Build d d' aT bT f (set_mem (sub_sfun_mfun fP)).
 #[local] HB.instance Definition _ := sfun_Sub1_subproof.
 Definition sfun_Sub2_subproof :=
-  @FiniteImage.Build aT rT f (set_mem (sub_sfun_fimfun fP)).
+  @FiniteImage.Build aT bT f (set_mem (sub_sfun_fimfun fP)).
 
 Import HBSimple.
 
@@ -135,24 +139,24 @@ Proof. by []. Qed.
 
 HB.instance Definition _ := isSub.Build _ _ T sfun_rect sfun_valP.
 
-Lemma sfuneqP (f g : {sfun aT >-> rT}) : f = g <-> f =1 g.
+Lemma sfuneqP (f g : {sfun aT >-> bT}) : f = g <-> f =1 g.
 Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
 
-HB.instance Definition _ := [Choice of {sfun aT >-> rT} by <:].
+HB.instance Definition _ := [Choice of {sfun aT >-> bT} by <:].
 
 (* NB: already in cardinality.v *)
-HB.instance Definition _ x : @FImFun aT rT (cst x) := FImFun.on (cst x).
+HB.instance Definition _ x : @FImFun aT bT (cst x) := FImFun.on (cst x).
 
-Definition cst_sfun x : {sfun aT >-> rT} := cst x.
+Definition cst_sfun x : {sfun aT >-> bT} := cst x.
 
 Lemma cst_sfunE x : @cst_sfun x =1 cst x. Proof. by []. Qed.
 
 End sfun.
 
 (* a better way to refactor function stuffs *)
-Lemma fctD (T : Type) (K : pzRingType) (f g : T -> K) : f + g = f \+ g.
+Lemma fctD (T : Type) (N : nmodType) (f g : T -> N) : f + g = f \+ g.
 Proof. by []. Qed.
-Lemma fctN (T : Type) (K : pzRingType) (f : T -> K) : - f = \- f.
+Lemma fctN (T : Type) (N : zmodType) (f : T -> N) : - f = \- f.
 Proof. by []. Qed.
 Lemma fctM (T : Type) (K : pzRingType) (f g : T -> K) : f * g = f \* g.
 Proof. by []. Qed.
@@ -165,13 +169,13 @@ Definition fctWE := (fctD, fctN, fctM, fctZ).
 Section ring.
 Context d (aT : measurableType d) (rT : realType).
 
-Lemma sfun_subring_closed : subring_closed (@sfun d aT rT).
+Lemma sfun_subring_closed : subring_closed (@sfun d _ aT rT).
 Proof.
 by split=> [|f g|f g]; rewrite ?inE/= ?rpred1//;
    move=> /andP[/= mf ff] /andP[/= mg fg]; rewrite !(rpredB, rpredM).
 Qed.
 
-HB.instance Definition _ := GRing.isSubringClosed.Build _ sfun
+HB.instance Definition _ := GRing.isSubringClosed.Build _ (@sfun d _ aT rT)
   sfun_subring_closed.
 HB.instance Definition _ := [SubChoice_isSubComPzRing of {sfun aT >-> rT} by <:].
 
@@ -213,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.