HRTBM: local games example

pPomCo · Feb 27, 2023 · 09361d1 · 09361d1
1 parent 0a82121
commit 09361d1
Showing 1 changed file with 125 additions and 0 deletions.
diff --git a/theories/HRtransform.v b/theories/HRtransform.v
@@ -476,5 +476,130 @@ Section HowsonRosenthal.
 
   End TBMTransform.
 
+
+  Lemma HRTBM_Dempster_plays_in G (HG : proper_belgame G (Dempster_conditioning _ _)) lg :
+    HRTBM_plays_in HG lg =1 [pred i_ti | lg (projT1 i_ti) == projT2 i_ti].
+  Proof.
+  rewrite /HRTBM_plays_in => i_ti /=.
+  case (boolP (lg (projT1 i_ti) == projT2 i_ti)) => // H.
+  rewrite orFb ; apply: negbTE ; rewrite negb_exists.
+  apply/forallP => X ; apply/negP => /and3P [Hcontra1 Hcontra2 Hcontra3].
+  move: Hcontra1 ; rewrite in_focalset_focalelement /focal_element /= ffunE.
+  have X_neq_set0 : X != set0 by apply/set0Pn ; exists lg.
+  rewrite (negbTE X_neq_set0)  big_pred0 => [|Y] ; first by rewrite lt0r eqxx andFb.
+  suff H1 : Y :&: [set t : {dffun forall i, T i} | t (projT1 i_ti) == projT2 (i_ti)] == X = false
+    by rewrite H1 andbF.
+  apply/negP => /eqP Hcontra.
+  move: Hcontra2 ; by rewrite -Hcontra in_setI !inE (negbTE H) andbF.
+  Qed.  
+
+  Lemma HRTBM_Strong_plays_in G (HG : proper_belgame G (Strong_conditioning _ _)) lg :
+    HRTBM_plays_in HG lg =1 [pred i_ti | lg (projT1 i_ti) == projT2 i_ti].
+  Proof.
+  rewrite /HRTBM_plays_in => i_ti /=.
+  case (boolP (lg (projT1 i_ti) == projT2 i_ti)) => // H.
+  rewrite orFb ; apply: negbTE ; rewrite negb_exists.
+  apply/forallP => X ; apply/negP => /and3P [Hcontra1 Hcontra2 Hcontra3].
+  move: Hcontra1 ; rewrite in_focalset_focalelement /focal_element /= ffunE.
+  have X_neq_set0 : X != set0 by apply/set0Pn ; exists lg.
+  rewrite (negbTE X_neq_set0) andTb.
+  suff H1 : ~~ (X \subset event_ti (projT2 i_ti))
+    by rewrite (negbTE H1) lt0r eqxx andFb.
+  by apply/subsetPn ; exists lg ; try rewrite !inE.
+  Qed.
+
+
 
 End HowsonRosenthal.
+
+
+Section HRTBMWeakConditioningLocalGames.
+
+  Variable R : realFieldType.
+  Notation I := [finType of 'I_2].
+  Notation A := (fun _ : I => [eqType of 'I_2]).
+  Notation T := (fun _ : I => [finType of 'I_2]).
+
+  Notation Tn := [finType of {ffun forall i, T i}].
+
+  Program Definition HRTBM_Weak_example_m : bpa R Tn :=
+    {| bpa_val := [ffun X => if X == setT then 1 else 0] |}.
+  Next Obligation.
+  have H0T : [set: {dffun 'I_2 -> 'I_2}] != set0
+    by apply/set0Pn ; exists [ffun t => ord0].
+  apply/and3P ; split.
+  + by rewrite ffunE [e in if e then _ else _]eq_sym (negbTE H0T) eqxx.
+  + rewrite (bigD1 setT) //= ffunE eqxx big1 => [|X HX].
+    * by rewrite addr0.
+    * by rewrite ffunE (negbTE HX).
+  + apply/forallP => X.
+    rewrite ffunE.
+    case (boolP (X == setT)) => [->//|H].
+    exact: ler01. by rewrite (negbTE H) //.
+  Defined.
+
+  Definition HRTBM_Weak_example_belgame : belgame R A T :=
+    (HRTBM_Weak_example_m, (fun => fun => fun => 0)).
+
+  Lemma HRTBM_Weak_example_proper : proper_belgame HRTBM_Weak_example_belgame (Weak_conditioning _ _).
+  Proof.
+  apply/forallP => i ; apply/forallP => ti.
+  rewrite/revisable/Weak_conditioning/Weak_revisable/Pl.
+  Search (_ > 0) (_ != 0).
+  apply: lt0r_neq0.
+  rewrite (bigD1 setT) /=.
+  - rewrite ffunE eqxx big1 => [|X /andP [HX1 HX2]].
+    + by rewrite addr0 ltr01.
+    + by rewrite ffunE (negbTE HX2).
+    + apply/set0Pn.
+      exists [ffun j => ti].
+      by rewrite setTI !inE ffunE.
+  Qed.
+
+  Lemma Pl_1 X : X != set0 -> Pl HRTBM_Weak_example_m X = 1.
+  Proof.
+  move => HX.
+  rewrite /Pl.
+  rewrite (bigD1 setT) /=.
+  - rewrite ffunE eqxx big1 => [|Y /andP [HY1 HY2]] ; first by rewrite addr0.
+    by rewrite ffunE (negbTE HY2).
+  - apply/set0Pn.
+    rewrite -card_gt0 in HX.
+    have [t Ht _] := eq_bigmax_cond (fun=>1%N) HX.
+    exists t ; by rewrite setTI.
+  Qed.
+
+
+  Lemma HRTBM_WEAK_example_plays_in lg i_ti : HRTBM_plays_in HRTBM_Weak_example_proper lg i_ti.
+  rewrite /HRTBM_plays_in.
+  apply/orP ; right.
+  apply/existsP ; exists setT.
+  apply/and3P ; split.
+  - rewrite !inE /focal_element /= ffunE.
+    have : setT :&: event_ti (projT2 i_ti) != set0
+      by apply/set0Pn ; exists [ffun _ => projT2 i_ti] ; rewrite in_setI !inE andTb ffunE.
+    move => ->.
+    rewrite ffunE eqxx Pl_1 ; first by rewrite divr_gt0 // ltr01.
+    apply/set0Pn ; exists [ffun _ => projT2 i_ti].
+    by rewrite !inE ffunE.
+  - by rewrite in_setT.
+  - apply/existsP.
+    exists [ffun _ => projT2 i_ti].
+    by rewrite in_setT ffunE eqxx.
+  Qed.
+
+  Lemma HRTBM_Xeak_example_plays_in2 i_ti : exists lg,
+      [&& HRTBM_plays_in HRTBM_Weak_example_proper lg i_ti & lg (projT1 i_ti) != projT2 i_ti].
+  Proof.
+  case (boolP (projT2 i_ti == 0)) => H.
+  - exists [ffun => 1].
+    apply/andP ; split.
+    + by apply HRTBM_WEAK_example_plays_in.
+    + by rewrite ffunE (eqP H).
+  - exists [ffun => 0].
+    apply/andP ; split.
+    + by apply HRTBM_WEAK_example_plays_in.
+    + by rewrite ffunE eq_sym.
+  Qed.
+
+End HRTBMWeakConditioningLocalGames.