From 1c38a9134aa49c12bc124b402591da9ba15fee0e Mon Sep 17 00:00:00 2001 From: Avi Shinnar Date: Sun, 8 Dec 2024 17:32:45 -0500 Subject: [PATCH] Add not01_ex05 Signed-off-by: Avi Shinnar --- coq/QLearn/jaakkola_vector.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v index 3be13bb8..af1932fb 100644 --- a/coq/QLearn/jaakkola_vector.v +++ b/coq/QLearn/jaakkola_vector.v @@ -3648,6 +3648,23 @@ Section jaakola_vector2. lra. Qed. + Lemma not01_ex05 : (~ forall (e : event dom), ps_P e = 0 \/ ps_P e = 1) -> (exists (ev : event dom), 0 < ps_P ev <= 0.5). + Proof. + intros HH. + apply not_all_ex_not in HH. + destruct HH as [e nprob]. + apply not_or_and in nprob. + destruct (Rle_dec (ps_P e) 0.5). + - exists e; generalize (ps_pos e); lra. + - exists (event_complement e). + split. + + destruct (ps_pos (event_complement e)); trivial. + rewrite ps_complement in H. + lra. + + rewrite ps_complement. + lra. + Qed. + Lemma vecrvclip_max_bound (rvec : Ts -> vector R (S N)) (C : posreal) : forall a, Rvector_max_abs (vecrvclip (S N) rvec (pos_to_nneg C) a) <= C.