upd wrt recent PRs, compat with Coq 8.15

Author: affeldt-aist

theories/kernel.v

@@ -101,35 +101,12 @@ Lemma xsection_preimage_snd (X Y Z : Type) (f : Y -> Z) (A : set Z) (x : X) :
   xsection ((f \o snd) @^-1` A) x = f @^-1` A.
 Proof. by apply/seteqP; split; move=> y/=; rewrite /xsection/= inE. Qed.
 
-Canonical unit_pointedType := PointedType unit tt.
-
-Section discrete_measurable_unit.
-
-Definition discrete_measurable_unit : set (set unit) := [set: set unit].
-
-Let discrete_measurable0 : discrete_measurable_unit set0. Proof. by []. Qed.
-
-Let discrete_measurableC X :
-  discrete_measurable_unit X -> discrete_measurable_unit (~` X).
-Proof. by []. Qed.
-
-Let discrete_measurableU (F : (set unit)^nat) :
-  (forall i, discrete_measurable_unit (F i)) ->
-  discrete_measurable_unit (\bigcup_i F i).
-Proof. by []. Qed.
-
-HB.instance Definition _ := @isMeasurable.Build default_measure_display unit
-  (Pointed.class _) discrete_measurable_unit discrete_measurable0
-  discrete_measurableC discrete_measurableU.
-
-End discrete_measurable_unit.
-
 Lemma measurable_curry (T1 T2 : Type) d (T : semiRingOfSetsType d)
     (G : T1 * T2 -> set T) (x : T1 * T2) :
   measurable (G x) <-> measurable (curry G x.1 x.2).
 Proof. by case: x. Qed.
 
-Lemma emeasurable_itv (R : realType) (i : nat) :
+Lemma emeasurable_itv1 (R : realType) (i : nat) :
   measurable (`[(i%:R)%:E, (i.+1%:R)%:E[%classic : set \bar R).
 Proof.
 rewrite -[X in measurable X]setCK.
@@ -143,13 +120,13 @@ Qed.
 Lemma measurable_fun_fst d1 d2 (T1 : measurableType d1)
   (T2 : measurableType d2) : measurable_fun setT (@fst T1 T2).
 Proof.
-by have /prod_measurable_funP[] := @measurable_fun_id _ (T1 * T2)%type setT.
+by have /prod_measurable_funP[] := @measurable_fun_id _ [the measurableType _ of (T1 * T2)%type] setT.
 Qed.
 
 Lemma measurable_fun_snd d1 d2 (T1 : measurableType d1)
   (T2 : measurableType d2) : measurable_fun setT (@snd T1 T2).
 Proof.
-by have /prod_measurable_funP[] := @measurable_fun_id _ (T1 * T2)%type setT.
+by have /prod_measurable_funP[] := @measurable_fun_id _ [the measurableType _ of (T1 * T2)%type] setT.
 Qed.
 
 Definition swap (T1 T2 : Type) (x : T1 * T2) := (x.2, x.1).
@@ -243,10 +220,6 @@ Proof. by rewrite -fubini_tonelli1// fubini_tonelli2. Qed.
 End fubini_tonelli.
 (* /TODO: PR *)
 
-Definition finite_measure d (T : measurableType d) (R : realType)
-    (mu : set T -> \bar R) :=
-  mu setT < +oo.
-
 Definition sfinite_measure d (T : measurableType d) (R : realType)
     (mu : set T -> \bar R) :=
   exists2 s : {measure set T -> \bar R}^nat,
@@ -274,7 +247,7 @@ Lemma sfinite_fubini :
 Proof.
 have [s1 fm1 m1E] := sfm1.
 have [s2 fm2 m2E] := sfm2.
-rewrite [LHS](eq_measure_integral (mseries s1 0)); last first.
+rewrite [LHS](eq_measure_integral [the measure _ _ of mseries s1 0]); last first.
   by move=> A mA _; rewrite m1E.
 transitivity (\int[mseries s1 0]_x \int[mseries s2 0]_y f (x, y)).
   by apply eq_integral => x _; apply: eq_measure_integral => ? ? _; rewrite m2E.
@@ -352,7 +325,7 @@ Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variable k : (R.-ker X ~> Y)^nat.
 
 Definition kseries : X -> {measure set Y -> \bar R} :=
-  fun x => mseries (k ^~ x) 0.
+  fun x => [the measure _ _ of mseries (k ^~ x) 0].
 
 Lemma measurable_fun_kseries (U : set Y) :
   measurable U ->
@@ -441,7 +414,7 @@ HB.factory Record Kernel_isFinite d d' (X : measurableType d)
 Section kzero.
 Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 
-Definition kzero : X -> {measure set Y -> \bar R} := fun _ : X => mzero.
+Definition kzero : X -> {measure set Y -> \bar R} := fun _ : X => [the measure _ _ of mzero].
 
 Let measurable_fun_kzero U : measurable U ->
   measurable_fun setT (kzero ^~ U).
@@ -463,7 +436,7 @@ Lemma sfinite_finite :
     forall x U, measurable U -> k x U = mseries (k_ ^~ x) 0 U.
 Proof.
 exists (fun n => if n is O then [the _.-ker _ ~> _ of k] else
-  @kzero _ _ X Y R).
+  [the _.-ker _ ~> _ of @kzero _ _ X Y R]).
   by case => [|_]; [exact: measure_uub|exact: kzero_uub].
 move=> t U mU/=; rewrite /mseries.
 rewrite (nneseries_split 1%N)// big_ord_recl/= big_ord0 adde0.
@@ -503,7 +476,7 @@ HB.instance Definition _ n :=
 Lemma sfinite : exists s : (R.-fker X ~> Y)^nat,
   forall x U, measurable U -> k x U = kseries s x U.
 Proof.
-by exists s => x U mU; rewrite /s /= /s; by case: cid2 => ? ? ->.
+by exists (fun n => [the _.-fker _ ~> _ of s n]) => x U mU; rewrite /s /= /s; by case: cid2 => ? ? ->.
 Qed.
 
 End sfinite.
@@ -703,7 +676,7 @@ Variable k : X * Y -> \bar R.
 
 Lemma measurable_fun_xsection_integral
     (l : X -> {measure set Y -> \bar R})
-    (k_ : ({nnsfun (X * Y)%type >-> R})^nat)
+    (k_ : ({nnsfun [the measurableType _ of (X * Y)%type] >-> R})^nat)
     (ndk_ : nondecreasing_seq (k_ : (X * Y -> R)^nat))
     (k_k : forall z, EFin \o (k_ ^~ z) --> k z) :
   (forall n r, measurable_fun setT (fun x => l x (xsection (k_ n @^-1` [set r]) x))) ->
@@ -738,7 +711,8 @@ rewrite [X in measurable_fun _ X](_ : _ = (fun x => \sum_(r \in range (k_ n))
   - by apply: eq_integral => y _; rewrite -fsumEFin.
   - move=> r.
     apply/EFin_measurable_fun/measurable_funrM/measurable_fun_prod1 => /=.
-    by rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) r)).
+    rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) r))//.
+    exact/measurable_funP.
   - by move=> m y _; rewrite nnfun_muleindic_ge0.
 apply: emeasurable_fun_fsum => // r.
 rewrite [X in measurable_fun _ X](_ : _ = (fun x => r%:E *
@@ -747,7 +721,8 @@ rewrite [X in measurable_fun _ X](_ : _ = (fun x => r%:E *
   have [r0|r0] := leP 0%R r.
     rewrite ge0_integralM//; last by move=> y _; rewrite lee_fin.
     apply/EFin_measurable_fun/measurable_fun_prod1 => /=.
-    by rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) r)).
+    rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) r))//.
+    exact/measurable_funP.
   rewrite integral_eq0; last first.
     by move=> y _; rewrite preimage_nnfun0// indic0 mule0.
   by rewrite integral_eq0 ?mule0// => y _; rewrite preimage_nnfun0// indic0.
@@ -805,7 +780,7 @@ Variable f : X -> Y.
 
 Definition kdirac (mf : measurable_fun setT f)
     : X -> {measure set Y -> \bar R} :=
-  fun x => dirac (f x).
+  fun x => [the measure _ _ of dirac (f x)].
 
 Hypothesis mf : measurable_fun setT f.
 
@@ -831,7 +806,7 @@ Arguments kdirac {d d' X Y R f}.
 Section dist_salgebra_instance.
 Context d (T : measurableType d) (R : realType).
 
-Let p0 : probability T R := dirac point.
+Let p0 : probability T R := [the probability _ _ of dirac point].
 
 Definition prob_pointed := Pointed.Class
   (Choice.Class gen_eqMixin (Choice.Class gen_eqMixin gen_choiceMixin)) p0.
@@ -857,7 +832,7 @@ Qed.
 Definition pset : set (set (probability T R)) :=
   [set mset U r | r in `[0%R,1%R] & U in measurable].
 
-Definition pprobability : measurableType pset.-sigma := salgebraType pset.
+Definition pprobability : measurableType pset.-sigma := [the measurableType _ of salgebraType pset].
 
 End dist_salgebra_instance.
 
@@ -898,7 +873,7 @@ Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variables k1 k2 : R.-ker X ~> Y.
 
 Definition kadd : X -> {measure set Y -> \bar R} :=
-  fun x => measure_add (k1 x) (k2 x).
+  fun x => [the measure _ _ of measure_add (k1 x) (k2 x)].
 
 Let measurable_fun_kadd U : measurable U ->
   measurable_fun setT (kadd ^~ U).
@@ -922,7 +897,7 @@ Let sfinite_kadd : exists2 k_ : (R.-ker _ ~> _)^nat, forall n, measure_fam_uub (
     kadd k1 k2 x U = mseries (k_ ^~ x) 0 U.
 Proof.
 have [f1 hk1] := sfinite k1; have [f2 hk2] := sfinite k2.
-exists (fun n => kadd (f1 n) (f2 n)).
+exists (fun n => [the _.-ker _ ~> _ of kadd (f1 n) (f2 n)]).
   move=> n.
   have [r1 f1r1] := measure_uub (f1 n).
   have [r2 f2r2] := measure_uub (f2 n).
@@ -1046,7 +1021,7 @@ Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variable f : R.-ker X ~> Y.
 
 Definition knormalize (P : probability Y R) : X -> {measure set Y -> \bar R} :=
-  mnormalize f P.
+  fun x => [the measure _ _ of mnormalize f P x].
 
 Variable P : probability Y R.
 
@@ -1113,7 +1088,7 @@ Section kcomp_is_measure.
 Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2)
  (Z : measurableType d3) (R : realType).
 Variable l : R.-ker X ~> Y.
-Variable k : R.-ker (X * Y)%type ~> Z.
+Variable k : R.-ker [the measurableType _ of (X * Y)%type] ~> Z.
 
 Local Notation "l \; k" := (kcomp l k).
 
@@ -1139,7 +1114,7 @@ Qed.
 HB.instance Definition _ x := isMeasure.Build _ R _
   ((l \; k) x) (kcomp0 x) (kcomp_ge0 x) (@kcomp_sigma_additive x).
 
-Definition mkcomp : X -> {measure set Z -> \bar R} := l \; k.
+Definition mkcomp : X -> {measure set Z -> \bar R} := fun x => [the measure _ _ of (l \; k) x].
 
 End kcomp_is_measure.
 
@@ -1150,7 +1125,7 @@ Module KCOMP_FINITE_KERNEL.
 Section kcomp_finite_kernel_kernel.
 Context d d' d3 (X : measurableType d) (Y : measurableType d')
   (Z : measurableType d3) (R : realType) (l : R.-fker X ~> Y)
-  (k : R.-ker (X * Y)%type ~> Z).
+  (k : R.-ker [the measurableType _ of (X * Y)%type] ~> Z).
 
 Lemma measurable_fun_kcomp_finite U :
   measurable U -> measurable_fun setT ((l \; k) ^~ U).
@@ -1168,7 +1143,7 @@ Section kcomp_finite_kernel_finite.
 Context d d' d3 (X : measurableType d) (Y : measurableType d')
   (Z : measurableType d3) (R : realType).
 Variable l : R.-fker X ~> Y.
-Variable k : R.-fker (X * Y)%type ~> Z.
+Variable k : R.-fker [the measurableType _ of (X * Y)%type] ~> Z.
 
 Let mkcomp_finite : measure_fam_uub (l \; k).
 Proof.
@@ -1194,7 +1169,7 @@ Section kcomp_sfinite_kernel.
 Context d d' d3 (X : measurableType d) (Y : measurableType d')
   (Z : measurableType d3) (R : realType).
 Variable l : R.-sfker X ~> Y.
-Variable k : R.-sfker (X * Y)%type ~> Z.
+Variable k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z.
 
 Import KCOMP_FINITE_KERNEL.
 
@@ -1206,10 +1181,10 @@ have [kl hkl] : exists kl : (R.-fker X ~> Z) ^nat, forall x U,
     \esum_(i in setT) (l_ i.2 \; k_ i.1) x U = \sum_(i <oo) kl i x U.
   have /ppcard_eqP[f] : ([set: nat] #= [set: nat * nat])%card.
     by rewrite card_eq_sym; exact: card_nat2.
-  exists (fun i => l_ (f i).2 \; k_ (f i).1) => x U.
+  exists (fun i => [the _.-fker _ ~> _ of l_ (f i).2 \; k_ (f i).1]) => x U.
   by rewrite (reindex_esum [set: nat] _ f)// nneseries_esum// fun_true.
 exists kl => x U mU.
-transitivity ((kseries l_ \; kseries k_) x U).
+transitivity (([the _.-ker _ ~> _ of kseries l_] \; [the _.-ker _ ~> _ of kseries k_]) x U).
   rewrite /= /kcomp [in RHS](eq_measure_integral (l x)); last first.
     by move=> *; rewrite hl_.
   by apply: eq_integral => y _; rewrite hk_.
@@ -1239,7 +1214,7 @@ Section kcomp_sfinite_kernel.
 Context d d' d3 (X : measurableType d) (Y : measurableType d')
   (Z : measurableType d3) (R : realType).
 Variable l : R.-sfker X ~> Y.
-Variable k : R.-sfker (X * Y)%type ~> Z.
+Variable k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z.
 
 HB.instance Definition _ :=
   isKernel.Build _ _ X Z R (l \; k) (measurable_fun_mkcomp_sfinite l k).
@@ -1283,7 +1258,8 @@ Lemma measurable_fun_preimage_integral (l : X -> {measure set Y -> \bar R}) :
   (forall n r, measurable_fun setT (l ^~ (k_ n @^-1` [set r]))) ->
   measurable_fun setT (fun x => \int[l x]_z k z).
 Proof.
-move=> h; apply: (measurable_fun_xsection_integral (k \o snd) l k_2) => /=.
+move=> h; apply: (measurable_fun_xsection_integral (k \o snd) l
+  (fun n => [the {nnsfun _ >-> _} of k_2 n])) => /=.
 - by rewrite /k_2 => m n mn; apply/lefP => -[x y] /=; exact/lefP/ndk_.
 - by move=> [x y]; exact: k_k.
 - move=> n r _ /= B mB.
@@ -1310,7 +1286,7 @@ Qed.
 Section integral_kcomp.
 Context d d2 d3 (X : measurableType d) (Y : measurableType d2)
   (Z : measurableType d3) (R : realType).
-Variables (l : R.-sfker X ~> Y) (k : R.-sfker (X * Y)%type ~> Z).
+Variables (l : R.-sfker X ~> Y) (k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z).
 
 Let integral_kcomp_indic x E (mE : measurable E) :
   \int[(l \; k) x]_z (\1_E z)%:E = \int[l x]_y (\int[k (x, y)]_z (\1_E z)%:E).
@@ -1351,7 +1327,7 @@ rewrite /= ge0_integral_fsum//; last 2 first.
   - move=> n y _.
     have := mulemu_ge0 (fun n => f @^-1` [set n]).
     by apply; exact: preimage_nnfun0.
-apply eq_fsbigr => r _.
+apply: eq_fsbigr => r _.
 rewrite (integralM_indic _ (fun r => f @^-1` [set r]))//; last first.
   exact: preimage_nnfun0.
 rewrite /= integral_kcomp_indic; last exact/measurable_sfunP.