From 76eaa2cbb35565171653c218c7885d4501c6949e Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sun, 29 Dec 2024 21:33:45 +0100 Subject: [PATCH] Better Von Neumann trick + generalization --- classical/classical_sets.v | 19 ++++ classical/mathcomp_extra.v | 6 + reals/constructive_ereal.v | 3 + theories/measure.v | 8 ++ theories/prob_lang.v | 228 ++++++++++++++++++++++++++----------- 5 files changed, 198 insertions(+), 66 deletions(-) diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 4331a45b6..95265327e 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -1439,9 +1439,15 @@ Implicit Types (A B : set aT) (f : aT -> rT) (Y : set rT). Lemma imageP f A a : A a -> (f @` A) (f a). Proof. by exists a. Qed. +Lemma image_f f A a : a \in A -> f a \in [set f x | x in A]. +Proof. by rewrite !inE; apply/imageP. Qed. + Lemma imageT (f : aT -> rT) (a : aT) : range f (f a). Proof. by apply: imageP. Qed. +Lemma mem_range f a : f a \in range f. +Proof. by rewrite !inE; apply/imageT. Qed. + End base_image_lemmas. #[global] Hint Extern 0 ((?f @` _) (?f _)) => solve [apply: imageP; assumption] : core. @@ -1456,6 +1462,10 @@ Proof. by move=> f_inj; rewrite propeqE; split => [[b Ab /f_inj <-]|/(imageP f)//]. Qed. +Lemma mem_image {f A a} : injective f -> + (f a \in [set f x | x in A]) = (a \in A). +Proof. by move=> /image_inj finj; apply/idP/idP; rewrite !inE finj. Qed. + Lemma image_id A : id @` A = A. Proof. by rewrite eqEsubset; split => a; [case=> /= x Ax <-|exists a]. Qed. @@ -1730,6 +1740,15 @@ Proof. by apply/disj_setPS/disj_setPS; rewrite -some_setI -some_set0 sub_image_someP. Qed. + +Lemma inl_in_set_inr A B (x : A) (Y : set B) : + inl x \in [set inr y | y in Y] = false. +Proof. by apply/negP; rewrite inE/= => -[]. Qed. + +Lemma inr_in_set_inr A B (y : B) (Y : set B) : + inr y \in [set @inr A B y | y in Y] = (y \in Y). +Proof. by apply/idP/idP => [/[!inE][/= [x ? [<-]]]|/[!inE]]//; exists y. Qed. + Section bigop_lemmas. Context {T I : Type}. Implicit Types (A : set T) (i : I) (P : set I) (F G : I -> set T). diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 7f5eeb3af..c8637e37f 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -588,3 +588,9 @@ rewrite mulr_ile1 ?andbT//. by have := xs01 x; rewrite inE xs orbT => /(_ _)/andP[]. by rewrite ih// => e xs; rewrite xs01// in_cons xs orbT. Qed. + +Lemma inr_inj {A B} : injective (@inr A B). +Proof. by move=> ? ? []. Qed. + +Lemma inl_inj {A B} : injective (@inl A B). +Proof. by move=> ? ? []. Qed. diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index a119e963f..348fa231f 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -670,6 +670,9 @@ Definition fin_num := [qualify a x : \bar R | (x != -oo) && (x != +oo)]. Fact fin_num_key : pred_key fin_num. Proof. by []. Qed. (*Canonical fin_num_keyd := KeyedQualifier fin_num_key.*) +Lemma fin_numP_EFin x : reflect (exists r, x = r%:E) (x \in fin_num). +Proof. by case: x => [r'||]//=; constructor; [exists r'| case | case ]. Qed. + Lemma fin_numE x : (x \is a fin_num) = (x != -oo) && (x != +oo). Proof. by []. Qed. diff --git a/theories/measure.v b/theories/measure.v index feee9731d..194f8939a 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1507,6 +1507,12 @@ by move=> fg mf mD A mA; rewrite [X in measurable X](_ : _ = D `&` f @^-1` A); [exact: mf|exact/esym/eq_preimage]. Qed. +Lemma measurable_fun_eqP D (f g : T1 -> T2) : + {in D, f =1 g} -> measurable_fun D f <-> measurable_fun D g. +Proof. +by move=> eq_fg; split; apply/eq_measurable_fun => // ? ?; rewrite eq_fg. +Qed. + Lemma measurable_cst D (r : T2) : measurable_fun D (cst r : T1 -> _). Proof. by move=> mD /= Y mY; rewrite preimage_cst; case: ifPn; rewrite ?setIT ?setI0. @@ -1574,6 +1580,8 @@ End measurable_fun. solve [apply: measurable_id] : core. Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}. #[deprecated(since="mathcomp-analysis 0.6.2", note="renamed `eq_measurable_fun`")] +Arguments measurable_fun_eqP {d1 d2 T1 T2 D} f {g}. +#[deprecated(since="mathcomp-analysis 0.6.2", note="renamed `eq_measurable_fun`")] Notation measurable_fun_ext := eq_measurable_fun (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_id`")] Notation measurable_fun_id := measurable_id (only parsing). diff --git a/theories/prob_lang.v b/theories/prob_lang.v index 9bc329960..70b89df55 100644 --- a/theories/prob_lang.v +++ b/theories/prob_lang.v @@ -1321,6 +1321,131 @@ Definition iterate : R.-sfker G ~> B := case_nat (kcounting R) iterate_. End iterate. +Section iterate_unit. + +Let unit := measurableTypeUnit. +Let bool := measurableTypeBool. +Context d {G : measurableType d} {R : realType}. +Context dB (B : measurableFinType dB). + +Section iterate_elim. +Variables (t : R.-sfker (G * unit) ~> (unit + B)%type) + (u : G -> unit) (mu : measurable_fun setT u). +Variables (r : R) (tlE : forall gamma, t (gamma, tt) [set inl tt] = r%:E). + +Variables (gamma : G) (X : set B) (q : R). +Hypothesis trE : t (gamma, tt) [set inr x | x in X] = q%:E. + +Let q_ge0 : (0 <= q)%R. Proof. by rewrite -lee_fin -trE measure_ge0. Qed. +Let r_ge0 : (0 <= r)%R. +Proof. by rewrite -lee_fin -(tlE gamma) measure_ge0. Qed. + +Lemma iterate_E n : iterate_ t mu n gamma X = (geometric q r n)%:E. +Proof. +elim: n => [|n IHn] //=; + rewrite /kcomp; rewrite integral_kcomp//=; + rewrite /= integral_dirac//= ?diracT ?mul1e ?expr0 ?exprS ?mulr1. + rewrite (eq_integral (EFin \o \1_[set inr x | x in X]))//=; last first. + move=> [a' _|b _]//=; last first. + by rewrite diracE indicE/= (mem_image inr_inj). + rewrite /kcomp/= indicE /= ge0_integral_mscale//= normr0 mul0e. + by rewrite [_ \in _](introF idP)// inE /= => -[]. + by rewrite ?unitE integral_indic//= setIT. +pose g : unit + B -> R^o := (geometric q r n \o* \1_[set inl tt])%R. +rewrite (eq_integral (EFin \o g))//=; last first. + move=> [[] _|b _]//=. + by rewrite /g/= indicE//= in_set1 inE eqxx mul1r. + rewrite /kcomp/= ge0_integral_mscale//= normr0 mul0e. + by rewrite /g /= indicE//= in_set1 inE mul0r. +rewrite /g /=; under eq_integral do rewrite EFinM. +rewrite integralZr//=; last first. + apply/integrableP; split=> //. + under eq_integral => x. + rewrite gee0_abs//=; last first. + by rewrite indicE lee_fin natr_ge0//. + over. + by rewrite /= integral_indic// setIT [u gamma]unitE tlE ltey. +by rewrite integral_indic//= [u gamma]unitE setIT tlE -EFinM mulrCA. +Qed. + +Hypothesis r_lt1 : (r < 1)%R. + +Lemma iterateE : iterate t mu gamma X = (q / (1 - r))%:E. +Proof. +rewrite /= /kcomp/= /case_nat_/= /mseries. +under eq_integral => n _. + under (@congr_lim _ _ _ \o @eq_fun _ _ _ _) => k. + under eq_bigr do rewrite fun_if/= (fun_if (@^~ _))/mzero eq_sym. + rewrite -big_mkcond/= big_nat1_eq. + over. +over. +rewrite /= (eq_integral (EFin \o geometric q r))//=; last first. + move=> k _; apply/lim_near_cst => //; rewrite iterate_E ?r_ge0 ?r_lt1//. + by near do rewrite ifT//. +have cvgg: series (geometric q r) x @[x --> \oo] --> (q / (1 - r))%R. + by apply/cvg_geometric_series; rewrite ger0_norm ?r_lt1//. +have limgg := cvg_lim (@Rhausdorff R) cvgg. +have sumgE : \big[+%R/0%R]_(0 <= k x; rewrite inE trueE. +rewrite -(@nneseries_esum _ _ predT)//=. +under eq_eseriesr do rewrite ger0_norm// ?geometric_ge0//. +by rewrite sumgE ltey. +Unshelve. all: end_near. Qed. + +End iterate_elim. + +Import CASE_SUM. + +Variables (t : R.-pker (G * unit) ~> (unit + B)%type) + (u : G -> unit) (mu : measurable_fun setT u). +Variables (r : R) (r_lt1 : (r < 1)%R). +Hypothesis (tlE : forall gamma, t (gamma, tt) [set inl tt] = r%:E). + +Let trE gamma X : t (gamma, tt) [set inr x | x in X] \in fin_num. +Proof. +apply/fin_numPlt; rewrite (@lt_le_trans _ _ 0)//=. +rewrite (@le_lt_trans _ _ 1)//= ?ltey//. +rewrite -( @prob_kernel _ _ _ _ _ t (gamma, tt) ). +by apply/le_measure => //=; rewrite inE//=. +Qed. + +Lemma iterate_normalize p : + iterate t mu = knormalize (case_sum (letin (ret mu) t) + (fun u' => fail) + (fun v => ret (measurable_cst v))) p. +Proof. +apply/eq_sfkernel => gamma U. +have /fin_numP_EFin[q trE'] := trE gamma U. +rewrite (iterateE mu tlE trE')//; symmetry. +rewrite /= /mnormalize/= (fun_if (@^~ U))/=. +set m := kcomp _ _ _. +have mE V : m V = t (gamma, tt) [set inr x | x in V]. + rewrite /m/= /kcomp/= integral_kcomp//= integral_dirac//= diracT mul1e. + rewrite (eq_integral (EFin \o \1_[set inr x | x in V])). + by rewrite integral_indic ?setIT ?unitE. + move=> [x|x] xV /=; rewrite indicE. + rewrite ?inl_in_set_inr /kcomp/=. + by rewrite ge0_integral_mscale//= ?normr0 mul0e. + by rewrite inr_in_set_inr// indicE. +rewrite !mE trE'. +suff -> : t (gamma, tt) (range inr) = 1 - t (gamma, tt) [set inl tt]. + by rewrite tlE -EFinB/= orbF eqe subr_eq0 eq_sym lt_eqF. +rewrite -( @prob_kernel _ _ _ _ _ t (gamma, tt) ). +have -> : [set: unit + B] = [set inl tt] `|` (range inr). + symmetry; apply/eq_set => -[[]|b]//=; apply/propT; first by left. + by right; exists b. +rewrite measureU//=; first by rewrite addeAC subee ?add0e// ?tlE//. +by apply/eq_set => -[[]|b]//=; apply/propF; case=> []// _ []. +Qed. + +End iterate_unit. + (* an s-finite kernel to test that two expressions are different *) Section lift_neq. Context {R : realType} d (G : measurableType d). @@ -1379,17 +1504,15 @@ Definition trick : R.-sfker (T * unit) ~> (unit + bool)%type := (letin (ret macc1of4) (ret minrb)) (ret minltt)))). -Definition von_neumann_trick_kernel : _ -> _ := +Definition kvon_neumann_trick : _ -> _ := (@iterate _ _ R _ unit _ bool trick _ ktt). -Definition von_neumann_trick x : _ -> _ := von_neumann_trick_kernel x. +Definition von_neumann_trick x : _ -> _ := kvon_neumann_trick x. -HB.instance Definition _ := SFiniteKernel.on von_neumann_trick_kernel. +HB.instance Definition _ := SFiniteKernel.on kvon_neumann_trick. HB.instance Definition _ x := Measure.on (von_neumann_trick x). Section von_neumann_trick_proof. -Hypothesis D_nontrivial : 0 < D [set true] < 1. - Let p : R := fine (D [set true]). Let q : R := p * (1 - p). Let r : R := p ^+ 2 + (1 - p) ^+ 2. @@ -1432,6 +1555,30 @@ by case: (set_bool A) => /eqP->/=; -EFinD addrNK. Qed. +Lemma trick_bool gamma b : trick gamma [set inr b] = q%:E. +Proof. +rewrite /trick/= /kcomp /= intDE//= /kcomp/= !intDE//= /kcomp. +rewrite !integral_dirac ?diracT//= ?mul1e. +rewrite !iteE//= ?diracE/= /kcomp/=. +rewrite !integral_dirac ?diracT ?diracE ?mul1e//=. +rewrite /finrb ?inl_in_set_inr//= /acc1of4/= ?inr_in_set_inr !in_set1 !inE. +rewrite /q -?(EFinB, EFinN, EFinM, EFinD); congr (_)%:E. +by case: b => //=; ring. +Qed. + +Lemma trick_unit gamma : trick gamma [set inl tt] = r%:E. +Proof. +rewrite /trick/= /kcomp /= intDE//= /kcomp/= !intDE//= /kcomp. +rewrite !integral_dirac ?diracT//= ?mul1e. +rewrite !iteE//= ?diracE/= /kcomp/=. +rewrite !integral_dirac ?diracT ?diracE ?mul1e//=. +rewrite /finrb ?inl_in_set_inr//= /acc1of4/= ?inr_in_set_inr. +rewrite !in_set1 !inE/=. +by rewrite /r -?(EFinB, EFinN, EFinM, EFinD); congr (_)%:E; ring. +Qed. + +Hypothesis D_nontrivial : 0 < D [set true] < 1. + Let p_gt0 : (0 < p)%R. Proof. by rewrite -lte_fin -Dtrue; case/andP : D_nontrivial. Qed. @@ -1446,74 +1593,23 @@ rewrite /r -subr_gt0 [ltRHS](_ : _ = 2 * p * (1 - p))%R; last by ring. by rewrite !mulr_gt0. Qed. -Lemma iterate_trick gamma n (b : bool) : - @iterate_ _ _ R _ unit _ bool trick _ ktt n gamma [set b] - = (geometric q r n)%:E. -Proof. -elim: n => [|n IHn] //=; rewrite /kcomp; rewrite integral_kcomp//=; - rewrite integral_dirac//= ?diracT ?mul1e integral_kcomp//=; - under eq_integral do [rewrite integral_kcomp//=; - under eq_integral do rewrite integral_kcomp//= - ?integral_dirac//= ?diracT ?mul1e]; - do ![rewrite intDE//=; last by - [move=> b'; do !rewrite integral_ge0//= => *]]; - rewrite !iteE//= ?integral_kcomp//= - ?integral_dirac//= ?diracT ?mul1e/=; - rewrite /acc1of4/= /kcomp ?ge0_integral_mscale //= - ?diracE/= ?in_set1 ?inE/= - ?(mule0, mul0e, adde0, add0e, mule1, normr0)//=; - rewrite -?(EFinB, EFinN, EFinM, EFinD) ?lee_fin ?expr0 ?mulr1//. - by case: b => //=; rewrite ?(mulr0, mulr1, add0r, addr0)// ?[(_ * p)%R]mulrC. -rewrite IHn -?(EFinB, EFinN, EFinM, EFinD) ?lee_fin ?expr0 ?mulr1//. -rewrite [geometric _ _ _]lock !mulrA -mulrDl addrC. -by rewrite /geometric/= -/r -lock mulrCA exprS. -Qed. - -Lemma iterate_trickT gamma n : - @iterate_ _ _ R _ unit _ bool trick _ ktt n gamma [set: bool] = - (2 * geometric q r n)%:E. -Proof. -rewrite setT_bool measureU//=; last first. - by rewrite disjoints_subset => -[]//. -by rewrite !iterate_trick -EFinD -mulr2n mulr_natl. -Qed. - Lemma von_neumann_trick_prob_kernel gamma b : - von_neumann_trick_kernel gamma [set b] = 2^-1%:E. + kvon_neumann_trick gamma [set b] = 2^-1%:E. Proof. -rewrite /= /kcomp/= /case_nat_/= /mseries. -under eq_integral => n _. - under (@congr_lim _ _ _ \o @eq_fun _ _ _ _) => k. - under eq_bigr do rewrite fun_if/= (fun_if (@^~ _))/mzero eq_sym. - rewrite -big_mkcond/= big_nat1_eq iterate_trick. - over. -over. -rewrite /= (eq_integral (EFin \o geometric q r))//=; last first. - by move=> k _; apply/lim_near_cst => //; near do rewrite ifT//. -have cvgg: series (geometric q r) x @[x --> \oo] --> (q / (1 - r))%R. - by apply/cvg_geometric_series; rewrite ger0_norm ?r_lt1. -have limgg := cvg_lim (@Rhausdorff R) cvgg. -have sumgE : \big[+%R/0%R]_(0 <= k *; field. rewrite [X in X != _](_ : _ = 2 * (p * (1 - p)))%R; last by ring. - by rewrite mulf_eq0 ?pnatr_eq0/= mulf_neq0// gt_eqF ?p_gt0 ?p'_gt0//. -suff summableg : summable setT (EFin \o geometric q r) - by rewrite integral_count. -rewrite /summable /=. -rewrite (_ : [set: nat] = [set x | x \in predT]); last first. - by apply/eq_set => x; rewrite inE trueE. -rewrite -(@nneseries_esum _ _ predT)//=. -under eq_eseriesr do rewrite ger0_norm// ?geometric_ge0//. -by rewrite sumgE ltey. -Unshelve. all: end_near. Qed. + by rewrite mulf_eq0 ?pnatr_eq0/= mulf_neq0// gt_eqF ?p_gt0 ?p'_gt0. +- by move=> gamma'; exact: trick_unit. +- suff -> : [set inr x | x in [set b]] = [set inr b] by exact: trick_bool. + by move=> A; apply/seteqP; split=> [a [_ ->]|_ ->]//=; exists b. +Qed. Lemma von_neumann_trick_prob_kernelT gamma : von_neumann_trick gamma [set: bool] = 1. Proof. -rewrite setT_bool measureU//=; last first. - by rewrite disjoints_subset => -[]. +rewrite setT_bool measureU//=; last by rewrite disjoints_subset => -[]. rewrite !von_neumann_trick_prob_kernel -EFinD. by have := splitr (1 : R); rewrite mul1r => <-. Qed. @@ -1522,7 +1618,7 @@ HB.instance Definition _ gamma := Measure.on (von_neumann_trick gamma). HB.instance Definition _ gamma := Measure_isProbability.Build _ _ _ (von_neumann_trick gamma) (von_neumann_trick_prob_kernelT gamma). HB.instance Definition _ := Kernel_isProbability.Build _ _ _ _ _ - von_neumann_trick_kernel von_neumann_trick_prob_kernelT. + kvon_neumann_trick von_neumann_trick_prob_kernelT. Theorem von_neumann_trickP gamma : von_neumann_trick gamma =1 bernoulli 2^-1. Proof. by apply: eq_bernoulli; rewrite von_neumann_trick_prob_kernel. Qed.