This instance will be upgraded to Heptapod 0.25.0 (final) on 2021-09-22 at 15:00 UTC+2 (a few minutes of down time)

Commit 49b43aa3 authored by hoelzl's avatar hoelzl
Browse files

add probably_innocent

parent 1618242118d6
......@@ -802,6 +802,21 @@ proof -
finally show ?thesis by (simp add: field_simps)
qed
lemma probably_innocent:
assumes approx: "1 / (2 * (H - J)) \<le> p_f" and "H \<noteq> J"
shows "\<PP>(\<omega> in \<P>. first_jondo \<omega> = last_ncoll \<omega> \<bar> hit_colls \<omega> ) \<le> 1 / 2"
unfolding P_first_jondo_eq_last_ncoll
proof -
have [simp]: "\<And>n :: nat. 1 \<le> real n \<longleftrightarrow> 1 \<le> n" by auto
have "0 \<le> J" unfolding J_def by auto
then have "1 * J \<le> H"
unfolding H_eq2[symmetric] using colls_smaller
by (intro mult_mono) (auto simp: Suc_le_eq card_Diff_subset not_le)
with `H \<noteq> J` have "J < H" by auto
with approx show "1 - (H - J) * p_f \<le> 1 / 2"
by (auto simp add: field_simps divide_le_eq split: split_if_asm)
qed
lemma P_last_ncoll:
assumes l: "l \<in> jondos - colls"
shows "\<PP>(\<omega> in \<P>. last_ncoll \<omega> = l \<bar> hit_colls \<omega> ) = J * p_f + init l * (1 - H * p_f)"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment