measurability for tuples

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,18 @@
 
 ### Added
 
+- in `classical_sets.v`
+  + lemma `bigcup_mkord_ord`
+
+- in `measure.v`:
+  + definition `g_sigma_preimage`
+  + lemma `g_sigma_preimage_comp`
+  + definition `measure_tuple_display`
+  + lemma `measurable_tnth`
+  + lemma `measurable_fun_tnthP`
+  + lemma `measurable_cons`
+  + lemma `measurable_behead`
+
 ### Changed
 
 ### Renamed

classical/classical_sets.v

@@ -2311,6 +2311,13 @@ rewrite -(big_mkord xpredT F) -bigcup_seq.
 by apply: eq_bigcupl; split=> i; rewrite /= mem_index_iota leq0n.
 Qed.
 
+Lemma bigcup_mkord_ord n (G : 'I_n.+1 -> set T) :
+  \bigcup_(i < n.+1) G (inord i) = \big[setU/set0]_(i < n.+1) G i.
+Proof.
+rewrite bigcup_mkord; apply: eq_bigr => /= i _; congr G.
+by apply/val_inj => /=; rewrite inordK.
+Qed.
+
 Lemma bigcap_mkord n F : \bigcap_(i < n) F i = \big[setI/setT]_(i < n) F i.
 Proof. by apply: setC_inj; rewrite setC_bigsetI setC_bigcap bigcup_mkord. Qed.
 
@@ -2493,6 +2500,8 @@ HB.instance Definition _ := isPointed.Build Prop False.
 HB.instance Definition _ := isPointed.Build nat 0.
 HB.instance Definition _ (T T' : pointedType) :=
   isPointed.Build (T * T')%type (point, point).
+HB.instance Definition _ (n : nat) (T : pointedType) :=
+  isPointed.Build (n.-tuple T) (nseq n point).
 HB.instance Definition _ m n (T : pointedType) :=
   isPointed.Build 'M[T]_(m, n) (\matrix_(_, _) point)%R.
 HB.instance Definition _ (T : choiceType) := isPointed.Build (option T) None.

theories/measure.v

@@ -268,6 +268,11 @@ From mathcomp Require Import sequences esum numfun.
 (*                                   generated from T1 x T2, with T1 and T2   *)
 (*                                   semiRingOfSetsType's with resp. display  *)
 (*                                   d1 and d2                                *)
+(*  g_sigma_preimage n (f : 'I_n -> aT -> rT) == the sigma-algebra over aT    *)
+(*                                   generated by the projections f           *)
+(*                                   n.-tuple T is equipped with a            *)
+(*                                   measurableType using g_sigma_preimage    *)
+(*                                   and the tnth projections.                *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* ## More measure-theoretic definitions                                      *)
@@ -5261,6 +5266,126 @@ Arguments measurable_snd {d1 d2 T1 T2}.
 #[global] Hint Extern 0 (measurable_fun _ snd) =>
   solve [apply: measurable_snd] : core.
 
+Definition g_sigma_preimage d (rT : semiRingOfSetsType d) (aT : Type)
+    (n : nat) (f : 'I_n -> aT -> rT) : set (set aT) :=
+  <<s \big[setU/set0]_(i < n) preimage_set_system setT (f i) measurable >>.
+
+Lemma g_sigma_preimage_comp d1 {T1 : semiRingOfSetsType d1} n
+    {T : pointedType} (f : 'I_n -> T -> T1) {T2 : Type} (g : T2 -> T) :
+  g_sigma_preimage (fun i => f i \o g) =
+  preimage_set_system [set: T2] g (g_sigma_preimage f).
+Proof.
+rewrite -[RHS]g_sigma_preimageE; congr (<<s _ >>).
+case: n => [|n] in f *; first by rewrite !big_ord0 preimage_set_system0.
+rewrite predeqE => B; split.
+- rewrite -bigcup_mkord_ord => -[i Ii [A mA <-{B}]].
+  have iE : Ordinal Ii = inord i by apply/val_inj => /=; rewrite inordK.
+  exists (f (inord i) @^-1` A) => //.
+  rewrite -bigcup_mkord_ord; exists i => //.
+  by exists A => //; rewrite -iE setTI.
+- move=> [C].
+  rewrite -bigcup_mkord_ord => -[i Ii [A mA <-{C}]] <-{B}.
+  rewrite -bigcup_mkord_ord; exists i => //.
+  by exists A => //; rewrite !setTI -comp_preimage.
+Qed.
+
+Definition measure_tuple_display : measure_display -> measure_display.
+Proof. exact. Qed.
+
+Section measurable_tuple.
+Context {d} {T : sigmaRingType d}.
+Variable n : nat.
+
+Let coors : 'I_n -> n.-tuple T -> T := fun i x => @tnth n T x i.
+
+Let tuple_set0 : g_sigma_preimage coors set0.
+Proof. exact: sigma_algebra0. Qed.
+
+Let tuple_setC A : g_sigma_preimage coors A -> g_sigma_preimage coors (~` A).
+Proof. exact: sigma_algebraC. Qed.
+
+Let tuple_bigcup (F : _^nat) : (forall i, g_sigma_preimage coors (F i)) ->
+  g_sigma_preimage coors (\bigcup_i (F i)).
+Proof. exact: sigma_algebra_bigcup. Qed.
+
+HB.instance Definition _ := @isMeasurable.Build (measure_tuple_display d)
+  (n.-tuple T) (g_sigma_preimage coors) tuple_set0 tuple_setC tuple_bigcup.
+
+End measurable_tuple.
+
+Lemma measurable_tnth d (T : sigmaRingType d) n (i : 'I_n) :
+  measurable_fun [set: n.-tuple T] (@tnth _ T ^~ i).
+Proof.
+move=> _ Y mY; rewrite setTI; apply: sub_sigma_algebra => /=.
+rewrite -bigcup_seq/=; exists i => /=; first by rewrite mem_index_enum.
+by exists Y => //; rewrite setTI.
+Qed.
+
+Section measurable_cons.
+Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2).
+
+Lemma measurable_fun_tnthP n (f : T1 -> n.-tuple T2) :
+  measurable_fun [set: T1] f <->
+  forall i, measurable_fun [set: T1] (@tnth n T2 ^~ i \o f).
+Proof.
+apply: (@iff_trans _ (g_sigma_preimage
+    (fun i => @tnth n T2 ^~ i \o f) `<=` measurable)).
+  rewrite g_sigma_preimage_comp; split=> [mf A [/= C preC <-]|prefS].
+    exact: mf.
+  by move=> _ A mA; apply: prefS; exists A.
+split=> [tnthfS i|mf].
+- move=> _ A mA.
+  apply: tnthfS; apply: sub_sigma_algebra.
+  case: n i => [[] []//|n i] in f *.
+  rewrite -bigcup_mkord_ord.
+  exists i; first exact: ltn_ord.
+  by exists A => //; rewrite inord_val.
+- apply: smallest_sub; first exact: sigma_algebra_measurable.
+  case: n => [|n] in f mf *; first by rewrite big_ord0.
+  rewrite -bigcup_mkord_ord; apply: bigcup_sub => i Ii.
+  by move=> A [B mB <-]; exact: mf.
+Qed.
+
+Lemma measurable_cons (f : T1 -> T2) n (g : T1 -> n.-tuple T2) :
+  measurable_fun [set: T1] f -> measurable_fun [set: T1] g ->
+  measurable_fun [set: T1] (fun x => [the n.+1.-tuple T2 of f x :: g x]).
+Proof.
+move=> mf mg; apply/measurable_fun_tnthP => /= i.
+have [->//|i0] := eqVneq i ord0.
+have i1n : (i.-1 < n)%N by rewrite prednK ?lt0n// -ltnS.
+pose j := Ordinal i1n.
+rewrite (_ : _ \o _ = fun x => tnth (g x) j)//.
+  apply: (@measurableT_comp _ _ _ _ _ _ (fun x => tnth x j)) => //=.
+  exact: measurable_tnth.
+apply/funext => x /=.
+rewrite (_ : i = lift ord0 j) ?tnthS//.
+by apply/val_inj => /=; rewrite /bump/= add1n prednK// lt0n.
+Qed.
+
+End measurable_cons.
+
+Lemma measurable_behead d (T : measurableType d) n :
+  measurable_fun [set: n.+1.-tuple T] (fun x => [tuple of behead x]).
+Proof.
+move=> _ Y mY; rewrite setTI.
+set f := fun x : (n.+1).-tuple T => [tuple of behead x] : n.-tuple T.
+move: mY; rewrite /measurable/= => + F [] sF.
+pose F' := image_set_system setT f F.
+move=> /(_ F') /=.
+have -> : F' Y = F (f @^-1` Y) by rewrite /F' /image_set_system /= setTI.
+move=> /[swap] bigF; apply; split; first exact: sigma_algebra_image.
+move=> A; rewrite /= {}/F' /image_set_system /= setTI.
+set bign := (X in X A) => bignA.
+apply: bigF; rewrite big_ord_recl /=; right.
+set bign1 := (X in X (_ @^-1` _)).
+have -> : bign1 = preimage_set_system [set: n.+1.-tuple T] f bign.
+  rewrite (big_morph _ (preimage_set_systemU _ _) (preimage_set_system0 _ _)).
+  apply: eq_bigr => i _; rewrite -preimage_set_system_comp.
+  congr preimage_set_system.
+  by apply: funext=> t/=; rewrite [in LHS](tuple_eta t) tnthS.
+by exists A => //; rewrite setTI.
+Qed.
+
 Lemma measurable_fun_if_pair d d' (X : measurableType d)
     (Y : measurableType d') (x y : X -> Y) :
   measurable_fun setT x -> measurable_fun setT y ->