diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6f2daa3446..e4099bc37d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -68,6 +68,17 @@ `integral_exponential_pdf`, `integrable_exponential_pdf` - in `exp.v` + lemma `expR_ge1Dxn` +- 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 diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 8e3c63d07f..44dd372c0f 100644 --- a/classical/classical_sets.v +++ b/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. diff --git a/theories/measure.v b/theories/measure.v index f1aaa5ccff..f39b038913 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -276,6 +276,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 *) @@ -5336,6 +5341,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) := + <>. + +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 (<>). +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 ->