restore the parameter of sigma_finite

CHANGELOG_UNRELEASED.md

@@ -140,7 +140,6 @@
 - in `measure.v`:
   + order of arguments of `isContent`, `Content`, `measure0`, `isMeasure0`,
     `Measure`, `isSigmaFinite`, `SigmaFiniteContent`, `SigmaFiniteMeasure`
-  + `sigma_finite` now specialized to the full set
 
 ### Renamed
 

theories/lebesgue_integral.v

@@ -4382,7 +4382,7 @@ have mF1F2 n : measurable (F1 n `*` F2 n) /\ m (F1 n `*` F2 n) < +oo.
   have [? ?] := F1_oo n; have [? ?] := F2_oo n.
   split; first exact: measurableM.
   by rewrite /m product_measure1E // lte_mul_pinfty// ge0_fin_numE.
-have sm : sigma_finite m by exists (fun n => F1 n `*` F2 n).
+have sm : sigma_finite setT m by exists (fun n => F1 n `*` F2 n).
 pose C : set (set (T1 * T2)) := [set C |
   exists A1, measurable A1 /\ exists A2, measurable A2 /\ C = A1 `*` A2].
 have CI : setI_closed C.

theories/lebesgue_measure.v

@@ -378,7 +378,7 @@ do !case: ifPn => //= ?; do ?by rewrite ?adde_ge0 ?lee_fin// ?subr_ge0// ?ltW.
 by rewrite addrAC lee_fin ler_add// subr_le0 leNgt.
 Qed.
 
-Lemma hlength_sigma_finite : sigma_finite (hlength : set ocitv_type -> _).
+Lemma hlength_sigma_finite : sigma_finite setT (hlength : set ocitv_type -> _).
 Proof.
 exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic).
   apply/esym; rewrite -subTset => x _ /=; exists `|(floor `|x| + 1)%R|%N => //=.

theories/measure.v

@@ -111,8 +111,8 @@ From HB Require Import structures.
 (*     {sfinite_measure set T -> \bar R} == type of s-finite measures         *)
 (*     Measure_isSFinite == factory for s-finite measures                     *)
 (*                                                                            *)
-(*     sigma_finite f == the measure function f is sigma-finite on the full   *)
-(*                       set [set: T]  with T : semiRingOfSetsType            *)
+(*     sigma_finite A f == the measure function f is sigma-finite on the set  *)
+(*                         A : set T  with T : semiRingOfSetsType             *)
 (*     isSigmaFinite == mixin corresponding to sigma finiteness               *)
 (*     {sigma_finite_content set T -> \bar R} == contents that are also sigma *)
 (*                                               finite                       *)
@@ -2559,13 +2559,13 @@ Definition sfinite_measure_def d (T : measurableType d) (R : realType)
     forall U, measurable U -> mu U = mseries s 0 U.
 
 Definition sigma_finite d (T : semiRingOfSetsType d) (R : numDomainType)
-    (mu : set T -> \bar R) :=
-  exists2 F : (set T)^nat, setT = \bigcup_(i : nat) F i &
+    (A : set T) (mu : set T -> \bar R) :=
+  exists2 F : (set T)^nat, A = \bigcup_(i : nat) F i &
       forall i, measurable (F i) /\ mu (F i) < +oo.
 
 Lemma fin_num_fun_sigma_finite d (T : algebraOfSetsType d)
     (R : realFieldType) (mu : set T -> \bar R) : mu set0 < +oo ->
-  fin_num_fun mu -> sigma_finite mu.
+  fin_num_fun mu -> sigma_finite setT mu.
 Proof.
 move=> muoo; exists (fun i => if i \in [set 0%N] then setT else set0).
   by rewrite -bigcup_mkcondr setTI bigcup_const//; exists 0%N.
@@ -2574,7 +2574,7 @@ Qed.
 
 Lemma sfinite_measure_sigma_finite d (T : measurableType d)
     (R : realType) (mu : {measure set T -> \bar R}) :
-  sigma_finite mu -> sfinite_measure_def mu.
+  sigma_finite setT mu -> sfinite_measure_def mu.
 Proof.
 move=> [F UF mF]; rewrite /sfinite_measure_def.
 have mDF k : measurable (seqDU F k).
@@ -2609,7 +2609,7 @@ Notation "{ 'sfinite_measure' 'set' T '->' '\bar' R }" :=
     format "{ 'sfinite_measure'  'set'  T  '->'  '\bar'  R }") : ring_scope.
 
 HB.mixin Record isSigmaFinite d (T : semiRingOfSetsType d) (R : numFieldType)
-  (mu : set T -> \bar R) := { sigma_finiteT : sigma_finite mu }.
+  (mu : set T -> \bar R) := { sigma_finiteT : sigma_finite setT mu }.
 
 #[short(type="sigma_finite_content")]
 HB.structure Definition SigmaFiniteContent d T R :=
@@ -2634,7 +2634,7 @@ Notation "{ 'sigma_finite_measure' 'set' T '->' '\bar' R }" :=
 
 HB.factory Record Measure_isSigmaFinite d (T : measurableType d) (R : realType)
     (mu : set T -> \bar R) of isMeasure _ _ _ mu :=
-  { sigma_finiteT : sigma_finite mu }.
+  { sigma_finiteT : sigma_finite setT mu }.
 
 HB.builders Context d (T : measurableType d) (R : realType)
   mu of @Measure_isSigmaFinite d T R mu.
@@ -2649,7 +2649,7 @@ HB.instance Definition _ := @isSigmaFinite.Build _ _ _ mu sigma_finiteT.
 HB.end.
 
 Lemma sigma_finite_mzero d (T : measurableType d) (R : realType) :
-  sigma_finite (@mzero d T R).
+  sigma_finite setT (@mzero d T R).
 Proof. by apply: fin_num_fun_sigma_finite => //; rewrite measure0. Qed.
 
 HB.instance Definition _ d (T : measurableType d) (R : realType) :=
@@ -2692,7 +2692,7 @@ Qed.
 
 HB.instance Definition _ := @Measure_isSFinite_subdef.Build d T R k sfinite.
 
-Let sigma_finite : sigma_finite k.
+Let sigma_finite : sigma_finite setT k.
 Proof.
 by apply: fin_num_fun_sigma_finite; [rewrite measure0|exact: fin_num_measure].
 Qed.
@@ -2832,7 +2832,7 @@ HB.instance Definition _ x :=
 End pdirac.
 
 Lemma sigma_finite_counting (R : realType) :
-  sigma_finite (@counting [choiceType of nat] R).
+  sigma_finite [set: nat] (@counting _ R).
 Proof.
 exists (fun n => `I_n.+1); first by apply/seteqP; split=> //x _; exists x => /=.
 by move=> k; split => //; rewrite /counting/= asboolT// ltry.
@@ -2964,11 +2964,11 @@ End boole_inequality.
 Notation le_mu_bigsetU := Boole_inequality.
 
 Section sigma_finite_lemma.
-Context d (R : realFieldType) (T : ringOfSetsType d)
+Context d (R : realFieldType) (T : ringOfSetsType d) (A : set T)
         (mu : {content set T -> \bar R}).
 
-Lemma sigma_finiteP : sigma_finite mu ->
-  exists2 F, setT = \bigcup_i F i &
+Lemma sigma_finiteP : sigma_finite A mu ->
+  exists2 F, A = \bigcup_i F i &
     nondecreasing_seq F /\ forall i, measurable (F i) /\ mu (F i) < +oo.
 Proof.
 move=> [S AS moo]; exists (fun n => \big[setU/set0]_(i < n.+1) S i).
@@ -3805,16 +3805,16 @@ Qed.
 HB.instance Definition _ := isMeasure.Build _ _ _ Hahn_ext
   Hahn_ext0 Hahn_ext_ge0 Hahn_ext_sigma_additive.
 
-Lemma Hahn_ext_sigma_finite : @sigma_finite _ T _ mu ->
-  @sigma_finite _ _ _ Hahn_ext.
+Lemma Hahn_ext_sigma_finite : @sigma_finite _ T _ setT mu ->
+  @sigma_finite _ _ _ setT Hahn_ext.
 Proof.
 move=> -[S setTS mS]; exists S => //; move=> i; split.
   by have := (mS i).1; exact: sub_sigma_algebra.
 by rewrite /Hahn_ext /= measurable_mu_extE //;
   [exact: (mS i).2 | exact: (mS i).1].
 Qed.
 
-Lemma Hahn_ext_unique : sigma_finite mu ->
+Lemma Hahn_ext_unique : sigma_finite [set: T] mu ->
   (forall mu' : {measure set I -> \bar R},
     (forall X, d.-measurable X -> mu X = mu' X) ->
     (forall X, (d.-measurable).-sigma.-measurable X -> Hahn_ext X = mu' X)).