minor generalization

Co-authored-by: @AyumuSaito

CHANGELOG_UNRELEASED.md

@@ -138,6 +138,8 @@
     `mem_conv_itvcc`, `range_conv`, `range_factor`
   + generalize to realFieldType:
     * `mem_factor_itv`
+- lemma `preimage_cst` generalized and moved from `lebesgue_integral.v`
+  to `functions.v`
 
 ### Renamed
 
@@ -153,6 +155,7 @@
   + `g_measurable_ptType` -> `salgebraType_ptType`
 - in `lebesgue_measure.v`:
   + `itvs` -> `ocitv_type`
+  + `measurable_fun_sum` -> `emeasurable_fun_sum`
 
 ### Removed
 

theories/functions.v

@@ -2480,6 +2480,13 @@ Import GRing.Theory.
 
 Definition cst {T T' : Type} (x : T') : T -> T' := fun=> x.
 
+Lemma preimage_cst {aT rT : Type} (a : aT) (A : set aT) :
+  @cst rT _ a @^-1` A = if a \in A then setT else set0.
+Proof.
+apply/seteqP; rewrite /preimage; split; first by move=> *; rewrite mem_set.
+by case: ifPn => [/[!inE] ?//|_]; exact: sub0set.
+Qed.
+
 Obligation Tactic := idtac.
 
 Program Definition fct_zmodMixin (T : Type) (M : zmodType) :=

theories/lebesgue_integral.v

@@ -464,13 +464,6 @@ move=> t0; rewrite preimage10//= => -[x _].
 by apply: contraPnot t0 => <-; rewrite le_gtF.
 Qed.
 
-Lemma preimage_cst T (R : eqType) (x y : R) :
-  @cst T _ x @^-1` [set y] = if x == y then setT else set0.
-Proof.
-apply/seteqP; rewrite /preimage; split => [z/= <-//|]; first by rewrite eqxx.
-by move=> z/=; case: ifPn => [/eqP|].
-Qed.
-
 Lemma preimage_cstM T (R : realFieldType) (x y : R) (f : T -> R) :
   x != 0 -> (cst x \* f) @^-1` [set y] = f @^-1` [set y / x].
 Proof.
@@ -696,8 +689,8 @@ Qed.
 
 Lemma sintegral0 : sintegral mu (cst 0%R) = 0.
 Proof.
-by rewrite sintegralE fsbig1// => r _; rewrite preimage_cst; case: ifPn;
-  rewrite ?measure0 ?mule0// => /eqP <-; rewrite mul0e.
+rewrite sintegralE fsbig1// => r _; rewrite preimage_cst.
+by case: ifPn => [/[!inE] <-|]; rewrite ?mul0e// measure0 mule0.
 Qed.
 
 Lemma sintegral_ge0 (f : {nnsfun T >-> R}) : 0 <= sintegral mu f.
@@ -1805,6 +1798,16 @@ apply: hwlogD => //.
 - by move=> ? [].
 Qed.
 
+Lemma emeasurable_fun_sum D I s (h : I -> (T -> \bar R)) :
+  (forall n, measurable_fun D (h n)) ->
+  measurable_fun D (fun x => \sum_(i <- s) h i x).
+Proof.
+elim: s => [|s t ih] mf.
+  by under eq_fun do rewrite big_nil; exact: measurable_fun_cst.
+under eq_fun do rewrite big_cons //=; apply: emeasurable_funD => //.
+exact: ih.
+Qed.
+
 Lemma emeasurable_funB D f g :
   measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \- g).
 Proof.
@@ -1872,20 +1875,6 @@ Qed.
 
 End emeasurable_fun.
 
-Section measurable_fun_sum.
-Local Open Scope ereal_scope.
-Variables (d : measure_display) (T : measurableType d) (R : realType) (D : set T) (I : Type).
-Variables (f : I -> (T -> \bar R)) (mf : forall n, measurable_fun D (f n)).
-
-Lemma measurable_fun_sum s : measurable_fun D (fun x => \sum_(i <- s) f i x).
-Proof.
-elim: s => [|h t ih].
-  by under eq_fun do rewrite big_nil; exact: measurable_fun_cst.
-under eq_fun do rewrite big_cons //=; apply: emeasurable_funD => // => x Dx.
-Qed.
-
-End measurable_fun_sum.
-
 Section ge0_integral_sum.
 Local Open Scope ereal_scope.
 Variables (d : measure_display) (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}).
@@ -1903,7 +1892,7 @@ rewrite big_cons /= -ih -ge0_integralD//.
 - by apply: eq_integral => x Dx; rewrite big_cons.
 - by move=> *; apply: f0.
 - by move=> *; apply: sume_ge0 => // k _; exact: f0.
-- exact: measurable_fun_sum.
+- exact: emeasurable_fun_sum.
 Qed.
 
 End ge0_integral_sum.
@@ -2075,7 +2064,7 @@ rewrite monotone_convergence //.
 - rewrite -lim_mkord.
   rewrite (_ : (fun _ => _) = (fun n => (\sum_(k < n) \int[mu]_(x in D) f k x)))//.
   by rewrite funeqE => n; rewrite ge0_integral_sum// big_mkord.
-- by move=> n; exact: measurable_fun_sum.
+- by move=> n; exact: emeasurable_fun_sum.
 - by move=> n x Dx; apply: sume_ge0 => m _; exact: f0.
 - by move=> x Dx m n mn; apply: lee_sum_nneg_natr => // k _ _; exact: f0.
 Qed.
@@ -4598,7 +4587,7 @@ Qed.
 
 Lemma sfun_measurable_fun_fubini_tonelli_F : measurable_fun setT F.
 Proof.
-rewrite sfun_fubini_tonelli_FE//; apply: measurable_fun_sum => // r.
+rewrite sfun_fubini_tonelli_FE//; apply: emeasurable_fun_sum => // r.
 by apply: emeasurable_funeM => //; apply: measurable_fun_xsection => // /[!inE].
 Qed.
 
@@ -4623,7 +4612,7 @@ Qed.
 
 Lemma sfun_measurable_fun_fubini_tonelli_G : measurable_fun setT G.
 Proof.
-rewrite sfun_fubini_tonelli_GE//; apply: measurable_fun_sum => // r.
+rewrite sfun_fubini_tonelli_GE//; apply: emeasurable_fun_sum => // r.
 by apply: emeasurable_funeM => //; apply: measurable_fun_ysection => // /[!inE].
 Qed.
 

theories/measure.v

@@ -943,11 +943,7 @@ Qed.
 Lemma measurable_fun_cst (D : set T1) (r : T2) :
   measurable_fun D (cst r : T1 -> _).
 Proof.
-move=> mD A mA; have [rA|rA] := boolP (r \in A).
-- rewrite [X in measurable X](_ : _ = D) // predeqE => t; split=> [[]//|Dt].
-  by split => //; rewrite inE in rA.
-- rewrite [X in measurable X](_ : _ = set0)// predeqE.
-  by move=> t; split=> // -[]; rewrite notin_set in rA.
+by move=> mD /= Y mY; rewrite preimage_cst; case: ifPn; rewrite ?setIT ?setI0.
 Qed.
 
 Lemma measurable_funU (D E : set T1) (f : T1 -> T2) :