diff --git a/thys/Poincare_Disc/ROOT b/thys/Poincare_Disc/ROOT --- a/thys/Poincare_Disc/ROOT +++ b/thys/Poincare_Disc/ROOT @@ -1,21 +1,21 @@ chapter AFP -session Poincare_Disc (AFP) = HOL + +session Poincare_Disc (AFP) = Complex_Geometry + options [timeout = 1200] sessions "Complex_Geometry" theories Hyperbolic_Functions Tarski Poincare_Lines Poincare_Lines_Ideal_Points Poincare_Distance Poincare_Circles Poincare_Between Poincare_Lines_Axis_Intersections Poincare_Perpendicular Poincare Poincare_Tarski document_files "root.bib" "root.tex" diff --git a/thys/Skip_Lists/Draft.thy b/thys/Skip_Lists/Draft.thy deleted file mode 100644 --- a/thys/Skip_Lists/Draft.thy +++ /dev/null @@ -1,266 +0,0 @@ -theory Draft -imports Skip_List -begin - - - -locale abstract_sl' = - fixes - val :: "'a \ 'b" and - down :: "'a \ 'a option" and - right :: "'a \ 'a option" and - V :: "'a set" - -locale abstract_sl = abstract_sl' + - assumes f: "finite V" -begin - - -function acyclic where - "acyclic visited a = (let visited' = visited \ {a} in (if visited' \ V \ a \ visited then - (case down a of Some d \ acyclic (visited \ {a}) d | None \ True) else False))" - by auto -termination - by (relation "Wellfounded.measure (\(visited, v). card V - card visited)") - (use f in \auto simp add: finite_subset intro!: psubset_card_mono diff_less_mono2\) - - - - -locale abstract_sl = abstract_sl' + - fixes wf_sl - assumes "" - - -datatype ('a::linorder) slttt = SL 'a "nat option" "nat option" - - -term "map_of [(0, SL 1 (Some 1) (Some 3)), (1, SL 1 None (Some 2)), (2, SL 8 None (Some 4))]" - -function lookup :: "'a::linorder \ 'a list list \ bool" where - "lookup x [] = False" | - "lookup x ((y#ys)#ls) = (if x = y then True else - (if y < x then lookup x (ys#(map (dropWhile (\z. z \ y)) ls)) else - lookup x ls))" | - "lookup x ([] # ls) = lookup x ls" - by pat_completeness auto -termination -proof (relation "(\(a,xs). length (concat xs)) <*mlex*> (\(a,xs). length xs) <*mlex*> {}", - goal_cases) - case 1 - then show ?case by(intro wf_mlex wf_empty) -next - case (2 a y ys ls) - have "length (concat (map (dropWhile (\z. z \ y)) ls)) \ (length (concat ls))" - by (auto simp add: length_concat length_dropWhile_le intro!: sum_list_mono) - then show ?case by (intro mlex_less) auto -next - case (3 x y ys ls) - then show ?case by (intro mlex_less) auto -next - case (4 x ls) - then show ?case by (rule mlex_leq) (auto intro!: mlex_less) -qed - -definition sl where "sl ls = (list_all distinct ls \ list_all sorted ls \ sorted_wrt subseq ls)" - - -lemma subseq_dropWhile: "subseq xs ys \ subseq (dropWhile P xs) ys" - by (induction xs ys rule: list_emb.induct) (auto) - -lemma subseq_dropWhile': "subseq xs ys \ subseq (dropWhile P xs) (dropWhile P ys)" - by (induction xs ys rule: list_emb.induct) (use subseq_dropWhile in auto) - -lemma sl_map_dropWhile: "sl ls \ sl (map (dropWhile P) ls)" - by (induction ls) (use subseq_dropWhile' in \auto simp add: sorted_dropWhile sl_def\) - -definition set_sl where "set_sl ls = \ (set ` set ls)" - -lemma set_sl_Cons: - "set xs \ set xs' \ set_sl ls \ set_sl ls' \ set_sl (xs # ls) \ set_sl (xs' # ls')" - unfolding set_sl_def by (auto) - -lemma subseq_subset: "subseq xs ys \ set xs \ set ys" - by (induction xs ys rule: list_emb.induct) (auto) - -lemma subseq_sorted: "subseq xs ys \ sorted ys \ sorted xs" - by (induction xs ys rule: list_emb.induct) (use subseq_subset in auto) - -lemma subseq_distinct: "subseq xs ys \ distinct ys \ distinct xs" - by (induction xs ys rule: list_emb.induct) (use subseq_subset in auto) - -lemma set_dropWhile: "set (dropWhile P ls) \ set ls" - by (induction ls) auto - -lemma "lookup x ls \ x \ set_sl ls" - using set_dropWhile - by (induction x ls rule: lookup.induct) (fastforce split: if_splits simp add: set_sl_def)+ - -lemma "subseq xs ys \ distinct ys \ distinct xs" - by (induction xs ys rule: list_emb.induct) (use subseq_subset in auto) - -lemma subseq_dropWhile_leq: - assumes "sorted ys" "distinct ys" "subseq xs ys" "xs = x'#xs'" - shows "subseq xs' (dropWhile (\z. z \ x') ys)" -using assms proof (induction ys arbitrary: xs x' xs') - case Nil - then show ?case by simp -next - case (Cons y ys xs x' xs') - have ?case if "x' = y" "xs' \ []" - using that Cons by (cases ys) (auto) - moreover have ?case if "x' < y" - proof - - have "subseq xs' (y # ys)" - using Cons subseq_Cons' by metis - then show ?thesis - using that Cons by (auto) - qed - ultimately show ?case using Cons by (cases "x' = y") (auto) -qed - -lemma sorted_dropWhile_filter: "sorted ls \ dropWhile (\x. x \ y) ls = filter (\x. x > y) ls" - by (induction ls) (auto simp add: less_le_trans) - -lemma sl_dropWhile_filter: "sl ls \ map (dropWhile (\x. x \ y)) ls = map (filter (\x. x > y)) ls" - by (auto simp add: sl_def list_all_iff intro!: map_cong sorted_dropWhile_filter) - -lemma "sl ls \ x \ set_sl ls \ lookup x ls" -(* TODO: clean up *) -proof (induction x ls rule: lookup.induct) - case (1 x) - then show ?case by (fastforce split: if_splits simp add: set_sl_def) -next - case (2 x y ys ls) - consider (a) "x = y" | (b) "y < x" | (c) "x < y" - by fastforce - then show ?case - proof (cases) - case b - have "sl (ys # map (dropWhile (\z. z \ y)) ls)" - proof (cases ls) - case Nil - then show ?thesis using 2 by (auto simp add: sl_def) - next - case (Cons l' ls') - have I:"sl (map (dropWhile (\z. z \ y)) ls)" - using 2 by (auto intro!: sl_map_dropWhile) (simp add: sl_def) - have "subseq ys (dropWhile (\z. z \ y) l')" - using 2 Cons by (auto simp add: sl_def intro!: subseq_dropWhile_leq) - then show ?thesis - using Cons I by (auto simp add: sl_def list_all_iff subseq_sorted subseq_distinct) - qed - moreover have "set_sl (ys # map (dropWhile (\z. z \ y)) ls) = set_sl (ys # map (filter (\z. y < z)) ls)" - using 2 by (subst sl_dropWhile_filter) (auto simp add: sl_def) - ultimately show ?thesis - using b 2 by (auto simp add: set_sl_def intro!: 2) - next - case c - then have "x \ set_sl ls" - using 2 subseq_subset by (cases ls) (auto simp add: set_sl_def sl_def) - then have "lookup x ls" - using c 2 by (auto simp add: set_sl_def sl_def intro!: 2) - then show ?thesis - using c 2 by (auto) - qed (auto) -next - case (3 x ls) - then show ?case by (fastforce split: if_splits simp add: set_sl_def sl_def) -qed - -fun sl_insert' where - "sl_insert' x (Suc n) (l#ls) = insort x l # sl_insert' x n ls" | - "sl_insert' x 0 (l#ls) = insort x l # ls" | - "sl_insert' x (Suc n) [] = [x] # sl_insert' x n []" | - "sl_insert' x 0 [] = [[x]]" - -definition sl_insert where - "sl_insert x n ls = (if lookup x ls then ls else rev (sl_insert' x n (rev ls)))" - -lemma sl_rev: - "sl (rev ls) = (list_all distinct ls \ list_all sorted ls \ sorted_wrt (\x y. subseq y x) ls)" - by (auto simp add: sl_def sorted_wrt_rev) - -lemma subseq_sorted_wrt: "sorted_wrt P xs \ subseq ys xs \ sorted_wrt P ys" -proof (induction ys) - case (Cons y ys) - then have "P y y'" if "y' \ set ys" for y' - using that subseq_subset by (induction xs) (auto split: if_splits) - then show ?case - using Cons by (auto simp add: subseq_Cons') -qed (auto) - -lemma sl_subseq_sl: "sl ls \ subseq ls' ls \ sl ls'" - using subseq_subset subseq_sorted_wrt by (fastforce simp add: sl_def list_all_iff) - -lemma subseq_rev: "subseq xs ys \ subseq (rev xs) (rev ys)" - by (induction xs ys rule: list_emb.induct) (auto) - -lemma subseq_insort_key: "subseq xs (insort_key P x xs)" - by (induction xs) (auto) - -lemma 1111: assumes "l \ set (sl_insert' x n ls)" - shows "(\l' \ set ls. l = insort x l') \ l = [x] \ l \ set ls" - using assms by (induction x n ls rule: sl_insert'.induct) (auto) - -lemma 28: "subseq xs ys \ sorted ys \ subseq (insort x xs) (insort x ys)" -proof (induction xs ys rule: list_emb.induct) - case (list_emb_Cons xs ys y) - then have "\x\set xs. y \ x" - using subseq_subset by (auto) - then have "insort x xs = x # xs" if "x \ y" - using that by (subst insort_is_Cons) (auto simp add: insort_is_Cons) - then show ?case - using list_emb_Cons by (auto) -qed (auto simp add: set_insort_key subseq_singleton_left) - - - -lemma - assumes "sl ls" - shows "sl (sl_insert x n ls)" -proof - - let ?sws = "sorted_wrt (\x y. subseq y x)" - let ?sort = "(\ls. list_all sorted ls \ sorted_wrt (\x y. subseq y x) ls)" - have "?sort (sl_insert' x n xs)" if "?sort xs" for xs - using that proof (induction x n xs rule: sl_insert'.induct) - case (1 x n y ys) - have "subseq l' (insort x y)" if "l' \ set (sl_insert' x n ys) " for l' - using 1 that apply - apply(drule 1111[of l']) apply(auto) - defer - apply(subst subseq_singleton_left) - apply (simp add: set_insort_key) - apply(subgoal_tac "subseq l' y") - using subseq_insort_key[of y] - using subseq_order.order_trans apply blast - using 1 apply(blast) - apply(rule 28) - by (auto) - then show ?case - using 1 sorted_insort by (auto) - next - case (2 x l ls) - then have "subseq l' l" if "l' \ set ls" for l' - using that by (auto) - moreover have "subseq l (insort x l)" - by (simp add: subseq_insort_key) - ultimately have "subseq l' (insort x l)" if "l' \ set ls" for l' - using that by fastforce - then show ?case - using 2 sorted_insort by (auto) - next - case (3 x n) - then show ?case - by (cases n) (auto) - qed (auto) - then show ?thesis - using assms sorry -qed - -notepad -begin - have 1: "a + b \ c" (is "?x + ?y \ ?z") for a b c::nat - sorry - let ?y = 1 - -end diff --git a/thys/Skip_Lists/Geometric_PMF.thy b/thys/Skip_Lists/Geometric_PMF.thy --- a/thys/Skip_Lists/Geometric_PMF.thy +++ b/thys/Skip_Lists/Geometric_PMF.thy @@ -1,342 +1,345 @@ (* File: Pi_pmf.thy Authors: Manuel Eberl, Max W. Haslbeck *) section \Theorems about the Geometric Distribution\ theory Geometric_PMF imports "HOL-Probability.Probability" Pi_pmf "Monad_Normalisation.Monad_Normalisation" begin lemma geometric_sums_times_n: fixes c::"'a::{banach,real_normed_field}" assumes "norm c < 1" shows "(\n. c^n * of_nat n) sums (c / (1 - c)\<^sup>2)" proof - have "(\n. c * z ^ n) sums (c / (1 - z))" if "norm z < 1" for z using geometric_sums sums_mult that by fastforce moreover have "((\z. c / (1 - z)) has_field_derivative (c / (1 - c)\<^sup>2)) (at c)" using assms by (auto intro!: derivative_eq_intros simp add: semiring_normalization_rules) ultimately have "(\n. diffs (\n. c) n * c ^ n) sums (c / (1 - c)\<^sup>2)" using assms by (intro termdiffs_sums_strong) then have "(\n. of_nat (Suc n) * c ^ (Suc n)) sums (c / (1 - c)\<^sup>2)" unfolding diffs_def by (simp add: power_eq_if mult.assoc) then show ?thesis by (subst (asm) sums_Suc_iff) (auto simp add: mult.commute) qed lemma geometric_sums_times_norm: fixes c::"'a::{banach,real_normed_field}" assumes "norm c < 1" shows "(\n. norm (c^n * of_nat n)) sums (norm c / (1 - norm c)\<^sup>2)" proof - have "norm (c^n * of_nat n) = (norm c) ^ n * of_nat n" for n::nat by (simp add: norm_power norm_mult) then show ?thesis using geometric_sums_times_n[of "norm c"] assms by force qed lemma integrable_real_geometric_pmf: assumes "p \ {0<..1}" shows "integrable (geometric_pmf p) real" proof - have "summable (\x. p * ((1 - p) ^ x * real x))" using geometric_sums_times_norm[of "1 - p"] assms by (intro summable_mult) (auto simp: sums_iff) + hence "summable (\x. (1 - p) ^ x * real x)" + by (rule summable_mult_D) (use assms in auto) thus ?thesis unfolding measure_pmf_eq_density using assms - by (subst integrable_density) (auto simp: integrable_count_space_nat_iff mult_ac) + by (subst integrable_density) + (auto simp: integrable_count_space_nat_iff mult_ac) qed lemma expectation_geometric_pmf: assumes "p \ {0<..1}" shows "measure_pmf.expectation (geometric_pmf p) real = (1 - p) / p" proof - have "(\n. p * ((1 - p) ^ n * n)) sums (p * ((1 - p) / p^2))" using assms geometric_sums_times_n[of "1-p"] by (intro sums_mult) auto moreover have "(\n. p * ((1 - p) ^ n * n)) = (\n. (1 - p) ^ n * p * real n)" by auto ultimately have *: "(\n. (1 - p) ^ n * p * real n) sums ((1 - p) / p)" using assms sums_subst by (auto simp add: power2_eq_square) have "measure_pmf.expectation (geometric_pmf p) real = (\n. pmf (geometric_pmf p) n * real n \count_space UNIV)" unfolding measure_pmf_eq_density by (subst integral_density) auto also have "integrable (count_space UNIV) (\n. pmf (geometric_pmf p) n * real n)" using * assms unfolding integrable_count_space_nat_iff by (simp add: sums_iff) hence "(\n. pmf (geometric_pmf p) n * real n \count_space UNIV) = (1 - p) / p" using * assms by (subst integral_count_space_nat) (simp_all add: sums_iff) finally show ?thesis by auto qed lemma nn_integral_geometric_pmf: assumes "p \ {0<..1}" shows "nn_integral (geometric_pmf p) real = (1 - p) / p" using assms expectation_geometric_pmf integrable_real_geometric_pmf by (subst nn_integral_eq_integral) auto lemma geometric_bind_pmf_unfold: assumes "p \ {0<..1}" shows "geometric_pmf p = do {b \ bernoulli_pmf p; if b then return_pmf 0 else map_pmf Suc (geometric_pmf p)}" proof - have *: "(Suc -` {i}) = (if i = 0 then {} else {i - 1})" for i by force have "pmf (geometric_pmf p) i = pmf (bernoulli_pmf p \ (\b. if b then return_pmf 0 else map_pmf Suc (geometric_pmf p))) i" for i proof - have "pmf (geometric_pmf p) i = (if i = 0 then p else (1 - p) * pmf (geometric_pmf p) (i - 1))" using assms by (simp add: power_eq_if) also have "\ = (if i = 0 then p else (1 - p) * pmf (map_pmf Suc (geometric_pmf p)) i)" by (simp add: pmf_map indicator_def measure_pmf_single *) also have "\ = measure_pmf.expectation (bernoulli_pmf p) (\x. pmf (if x then return_pmf 0 else map_pmf Suc (geometric_pmf p)) i)" using assms by (auto simp add: pmf_map *) also have "\ = pmf (bernoulli_pmf p \ (\b. if b then return_pmf 0 else map_pmf Suc (geometric_pmf p))) i" by (auto simp add: pmf_bind) finally show ?thesis . qed then show ?thesis using pmf_eqI by blast qed lemma "p \ {0<..<1} \ set_pmf (geometric_pmf p) = UNIV" by (auto simp add: measure_pmf_single set_pmf_def) lemma "set_pmf (geometric_pmf 1) = 0" by (auto simp add: measure_pmf_single set_pmf_def) lemma geometric_pmf_prob_atMost: assumes "p \ {0<..1}" shows "measure_pmf.prob (geometric_pmf p) {..n} = (1 - (1 - p)^(n + 1))" proof - have "(\x\n. (1 - p) ^ x * p) = 1 - (1 - p) * (1 - p) ^ n" by (induction n) (auto simp add: algebra_simps) then show ?thesis using assms by (auto simp add: measure_pmf_conv_infsetsum) qed lemma geometric_pmf_prob_lessThan: assumes "p \ {0<..1}" shows "measure_pmf.prob (geometric_pmf p) {..x {0<..1}" shows "measure_pmf.prob (geometric_pmf p) {n<..} = (1 - p)^(n + 1)" proof - have "(UNIV - {..n}) = {n<..}" by auto moreover have "measure_pmf.prob (geometric_pmf p) (UNIV - {..n}) = (1 - p) ^ (n + 1)" using assms by (subst measure_pmf.finite_measure_Diff) (auto simp add: geometric_pmf_prob_atMost) ultimately show ?thesis by auto qed lemma geometric_pmf_prob_atLeast: assumes "p \ {0<..1}" shows "measure_pmf.prob (geometric_pmf p) {n..} = (1 - p)^n" proof - have "(UNIV - {..b. {x \ A. \ b x}) (Pi_pmf A P (\_. bernoulli_pmf (1/2))) = pmf_of_set (Pow A)" proof - have *: "Pi_pmf A P (\_. pmf_of_set (UNIV :: bool set)) = pmf_of_set (PiE_dflt A P (\_. UNIV :: bool set))" using assms by (intro Pi_pmf_of_set) auto have "map_pmf (\b. {x \ A. \ b x}) (Pi_pmf A P (\_. bernoulli_pmf (1 / 2))) = map_pmf (\b. {x \ A. \ b x}) (Pi_pmf A P (\_. pmf_of_set UNIV))" using bernoulli_pmf_half_conv_pmf_of_set by auto also have "\ = map_pmf (\b. {x \ A. \ b x}) (pmf_of_set (PiE_dflt A P (\_. UNIV)))" using assms by (subst Pi_pmf_of_set) (auto) also have "\ = pmf_of_set (Pow A)" proof - have "bij_betw (\b. {x \ A. \ b x}) (PiE_dflt A P (\_. UNIV)) (Pow A)" by (rule bij_betwI[of _ _ _ "\B b. if b \ A then \ (b \ B) else P"]) (auto simp add: PiE_dflt_def) then show ?thesis using assms by (intro map_pmf_of_set_bij_betw) auto qed finally show ?thesis by simp qed lemma Pi_pmf_pmf_of_set_Suc: assumes "finite A" shows "Pi_pmf A 0 (\_. geometric_pmf (1/2)) = do { B \ pmf_of_set (Pow A); Pi_pmf B 0 (\_. map_pmf Suc (geometric_pmf (1/2))) }" proof - have "Pi_pmf A 0 (\_. geometric_pmf (1/2)) = Pi_pmf A 0 (\_. bernoulli_pmf (1/2) \ (\b. if b then return_pmf 0 else map_pmf Suc (geometric_pmf (1/2))))" using assms by (subst geometric_bind_pmf_unfold) auto also have "\ = Pi_pmf A False (\_. bernoulli_pmf (1/2)) \ (\b. Pi_pmf A 0 (\x. if b x then return_pmf 0 else map_pmf Suc (geometric_pmf (1/2))))" using assms by (subst Pi_pmf_bind[of _ _ _ _ False]) auto also have "\ = do {b \ Pi_pmf A False (\_. bernoulli_pmf (1/2)); Pi_pmf {x \ A. ~b x} 0 (\x. map_pmf Suc (geometric_pmf (1/2)))}" using assms by (subst Pi_pmf_if_set') auto also have "\ = do {B \ map_pmf (\b. {x \ A. \ b x}) (Pi_pmf A False (\_. bernoulli_pmf (1/2))); Pi_pmf B 0 (\x. map_pmf Suc (geometric_pmf (1/2)))}" unfolding map_pmf_def apply(subst bind_assoc_pmf) apply(subst bind_return_pmf) by auto also have "\ = pmf_of_set (Pow A) \ (\B. Pi_pmf B 0 (\x. map_pmf Suc (geometric_pmf (1 / 2))))" unfolding assms using assms by (subst bernoulli_pmf_of_set') auto finally show ?thesis by simp qed lemma Pi_pmf_pmf_of_set_Suc': assumes "finite A" shows "Pi_pmf A 0 (\_. geometric_pmf (1/2)) = do { B \ pmf_of_set (Pow A); Pi_pmf B 0 (\_. map_pmf Suc (geometric_pmf (1/2))) }" proof - have "Pi_pmf A 0 (\_. geometric_pmf (1/2)) = Pi_pmf A 0 (\_. bernoulli_pmf (1/2) \ (\b. if b then return_pmf 0 else map_pmf Suc (geometric_pmf (1/2))))" using assms by (subst geometric_bind_pmf_unfold) auto also have "\ = Pi_pmf A False (\_. bernoulli_pmf (1/2)) \ (\b. Pi_pmf A 0 (\x. if b x then return_pmf 0 else map_pmf Suc (geometric_pmf (1/2))))" using assms by (subst Pi_pmf_bind[of _ _ _ _ False]) auto also have "\ = do {b \ Pi_pmf A False (\_. bernoulli_pmf (1/2)); Pi_pmf {x \ A. ~b x} 0 (\x. map_pmf Suc (geometric_pmf (1/2)))}" using assms by (subst Pi_pmf_if_set') auto also have "\ = do {B \ map_pmf (\b. {x \ A. \ b x}) (Pi_pmf A False (\_. bernoulli_pmf (1/2))); Pi_pmf B 0 (\x. map_pmf Suc (geometric_pmf (1/2)))}" unfolding map_pmf_def by (auto simp add: bind_assoc_pmf bind_return_pmf) also have "\ = pmf_of_set (Pow A) \ (\B. Pi_pmf B 0 (\x. map_pmf Suc (geometric_pmf (1 / 2))))" unfolding assms using assms by (subst bernoulli_pmf_of_set') auto finally show ?thesis by simp qed lemma binomial_pmf_altdef': fixes A :: "'a set" assumes "finite A" and "card A = n" and p: "p \ {0..1}" shows "binomial_pmf n p = map_pmf (\f. card {x\A. f x}) (Pi_pmf A dflt (\_. bernoulli_pmf p))" (is "?lhs = ?rhs") proof - from assms have "?lhs = binomial_pmf (card A) p" by simp also have "\ = ?rhs" using assms(1) proof (induction rule: finite_induct) case empty with p show ?case by (simp add: binomial_pmf_0) next case (insert x A) from insert.hyps have "card (insert x A) = Suc (card A)" by simp also have "binomial_pmf \ p = do { b \ bernoulli_pmf p; f \ Pi_pmf A dflt (\_. bernoulli_pmf p); return_pmf ((if b then 1 else 0) + card {y \ A. f y}) }" using p by (simp add: binomial_pmf_Suc insert.IH bind_map_pmf) also have "\ = do { b \ bernoulli_pmf p; f \ Pi_pmf A dflt (\_. bernoulli_pmf p); return_pmf (card {y \ insert x A. (f(x := b)) y}) }" proof (intro bind_pmf_cong refl, goal_cases) case (1 b f) have "(if b then 1 else 0) + card {y\A. f y} = card ((if b then {x} else {}) \ {y\A. f y})" using insert.hyps by auto also have "(if b then {x} else {}) \ {y\A. f y} = {y\insert x A. (f(x := b)) y}" using insert.hyps by auto finally show ?case by simp qed also have "\ = map_pmf (\f. card {y\insert x A. f y}) (Pi_pmf (insert x A) dflt (\_. bernoulli_pmf p))" using insert.hyps by (subst Pi_pmf_insert) (simp_all add: pair_pmf_def map_bind_pmf) finally show ?case . qed finally show ?thesis . qed lemma bernoulli_pmf_Not: assumes "p \ {0..1}" shows "bernoulli_pmf p = map_pmf Not (bernoulli_pmf (1 - p))" proof - have *: "(Not -` {True}) = {False}" "(Not -` {False}) = {True}" by blast+ have "pmf (bernoulli_pmf p) b = pmf (map_pmf Not (bernoulli_pmf (1 - p))) b" for b using assms by (cases b) (auto simp add: pmf_map * measure_pmf_single) then show ?thesis by (rule pmf_eqI) qed lemma binomial_pmf_altdef'': assumes p: "p \ {0..1}" shows "binomial_pmf n p = map_pmf (\f. card {x. x < n \ f x}) (Pi_pmf {.._. bernoulli_pmf p))" using assms by (subst binomial_pmf_altdef'[of "{.. {0<..1}" shows "Pi_pmf A 0 (\_. geometric_pmf p) = do { fb \ Pi_pmf A dflt (\_. bernoulli_pmf p); Pi_pmf {x \ A. \ fb x} 0 (\_. map_pmf Suc (geometric_pmf p)) }" proof - have "Pi_pmf A 0 (\_. geometric_pmf p) = Pi_pmf A 0 (\_. bernoulli_pmf p \ (\b. if b then return_pmf 0 else map_pmf Suc (geometric_pmf p)))" using assms by (subst geometric_bind_pmf_unfold) auto also have "\ = Pi_pmf A dflt (\_. bernoulli_pmf p) \ (\b. Pi_pmf A 0 (\x. if b x then return_pmf 0 else map_pmf Suc (geometric_pmf p)))" using assms by (subst Pi_pmf_bind[of _ _ _ _ dflt]) auto also have "\ = do {b \ Pi_pmf A dflt (\_. bernoulli_pmf p); Pi_pmf {x \ A. \ b x} 0 (\x. map_pmf Suc (geometric_pmf p))}" using assms by (subst Pi_pmf_if_set') (auto) finally show ?thesis by simp qed lemma Pi_pmf_geometric_filter': assumes "finite A" "p \ {0<..1}" shows "Pi_pmf A 0 (\_. geometric_pmf p) = do { fb \ Pi_pmf A dflt (\_. bernoulli_pmf (1 - p)); Pi_pmf {x \ A. fb x} 0 (\_. map_pmf Suc (geometric_pmf p)) }" using assms by (auto simp add: Pi_pmf_geometric_filter[of _ _ "\ dflt"] bernoulli_pmf_Not[of p] Pi_pmf_map[of _ _ dflt] map_pmf_def[of "((\) Not)"]) end end diff --git a/thys/Skip_Lists/Skip_List.thy b/thys/Skip_Lists/Skip_List.thy --- a/thys/Skip_Lists/Skip_List.thy +++ b/thys/Skip_Lists/Skip_List.thy @@ -1,1346 +1,1346 @@ (* File: Skip_List.thy Authors: Max W. Haslbeck, Manuel Eberl *) section \Randomized Skip Lists\ theory Skip_List imports Geometric_PMF Pi_pmf Misc "Monad_Normalisation.Monad_Normalisation" begin subsection \Preliminaries\ lemma bind_pmf_if': "(do {c \ C; ab \ (if c then A else B); D ab}::'a pmf) = do {c \ C; (if c then (A \ D) else (B \ D))}" by (metis (mono_tags, lifting)) abbreviation (input) Max\<^sub>0 where "Max\<^sub>0 \ (\A. Max (A \ {0}))" subsection \Definition of a Randomised Skip List\ text \ Given a set A we assign a geometric random variable (counting the number of failed Bernoulli trials before the first success) to every element in A. That means an arbitrary element of A is on level n with probability $(1-p)^{n}p$. We define he height of the skip list as the maximum assigned level. So a skip list with only one level has height 0 but the calculation of the expected height is cleaner this way. \ locale random_skip_list = fixes p::real begin definition q where "q = 1 - p" definition SL :: "('a::linorder) set \ ('a \ nat) pmf" where "SL A = Pi_pmf A 0 (\_. geometric_pmf p)" definition SL\<^sub>N :: "nat \ (nat \ nat) pmf" where "SL\<^sub>N n = SL {..Height of Skip List\ definition H where "H A = map_pmf (\f. Max\<^sub>0 (f ` A)) (SL A)" definition H\<^sub>N :: "nat \ nat pmf" where "H\<^sub>N n = H {.. The height of a skip list is independent of the values in a set A. For simplicity we can therefore work on the skip list over the set @{term "{..< card A}"} \ lemma assumes "finite A" shows "H A = H\<^sub>N (card A)" proof - define f' where "f' = (\x. if x \ A then the_inv_into {..0 ((f \ f') ` A) = Max\<^sub>0 (f ` {.. nat" using bij_betw_imp_surj_on bij_f' image_comp by metis have "H A = map_pmf (\f. Max\<^sub>0 (f ` A)) (map_pmf (\g. g \ f') (SL\<^sub>N (card A)))" using assms bij_f' unfolding H_def SL_def SL\<^sub>N_def by (subst Pi_pmf_bij_betw[of _ f' "{.. = H\<^sub>N (card A)" unfolding H\<^sub>N_def H_def SL\<^sub>N_def using * by (auto intro!: bind_pmf_cong simp add: map_pmf_def) finally show ?thesis by simp qed text \ The cumulative distribution function (CDF) of the height is the CDF of the geometric PMF to the power of n \ lemma prob_Max_IID_geometric_atMost: assumes "p \ {0..1}" shows "measure_pmf.prob (H\<^sub>N n) {..i} = (measure_pmf.prob (geometric_pmf p) {..i}) ^ n" (is "?lhs = ?rhs") proof - note SL_def[simp] SL\<^sub>N_def[simp] H_def[simp] H\<^sub>N_def[simp] have "{f. Max\<^sub>0 (f ` {.. i} = {.. {..i}" by auto then have "?lhs = measure_pmf.prob (SL\<^sub>N n) ({.. {..i})" by (simp add: vimage_def) also have "\ = measure_pmf.prob (SL\<^sub>N n) (PiE_dflt {.._. {..i}))" by (intro measure_prob_cong_0) (auto simp add: PiE_dflt_def pmf_Pi split: if_splits) also have "\ = measure_pmf.prob (geometric_pmf p) {..i} ^ n" using assms by (auto simp add: measure_Pi_pmf_PiE_dflt) finally show ?thesis by simp qed lemma prob_Max_IID_geometric_greaterThan: assumes "p \ {0<..1}" shows "measure_pmf.prob (H\<^sub>N n) {i<..} = 1 - (1 - q ^ (i + 1)) ^ n" proof - have "UNIV - {..i} = {i<..}" by auto then have "measure_pmf.prob (H\<^sub>N n) {i<..} = measure_pmf.prob (H\<^sub>N n) (space (measure_pmf (H\<^sub>N n)) - {..i})" by (auto) also have "\ = 1 - (measure_pmf.prob (geometric_pmf p) {..i}) ^ n" using assms by (subst measure_pmf.prob_compl) (auto simp add: prob_Max_IID_geometric_atMost) also have "\ = 1 - (1 - q ^ (i + 1)) ^ n" using assms unfolding q_def by (subst geometric_pmf_prob_atMost) auto finally show ?thesis by simp qed end (* context includes monad_normalisation *) end (* locale skip_list *) text \ An alternative definition of the expected value of a non-negative random variable \footnote{\url{https://en.wikipedia.org/w/index.php?title=Expected\_value&oldid=881384346\#Formula\_for\_non-negative\_random\_variables}} \ lemma expectation_prob_atLeast: assumes "(\i. measure_pmf.prob N {i..}) abs_summable_on {1..}" shows "measure_pmf.expectation N real = infsetsum (\i. measure_pmf.prob N {i..}) {1..}" "integrable N real" proof - have "(\(x, y). pmf N y) abs_summable_on Sigma {Suc 0..} atLeast" using assms by (auto simp add: measure_pmf_conv_infsetsum abs_summable_on_Sigma_iff) then have summable: "(\(x, y). pmf N x) abs_summable_on Sigma {Suc 0..} (atLeastAtMost (Suc 0))" by (subst abs_summable_on_reindex_bij_betw[of "\(x,y). (y,x)", symmetric]) (auto intro!: bij_betw_imageI simp add: inj_on_def case_prod_beta) have "measure_pmf.expectation N real = (\\<^sub>ax. pmf N x *\<^sub>R real x)" by (auto simp add: infsetsum_def integral_density measure_pmf_eq_density) also have "\ = (\\<^sub>ax \ ({0} \ {Suc 0..}). pmf N x *\<^sub>R real x)" by (auto intro!: infsetsum_cong) also have "\ = (\\<^sub>ax\{Suc 0..}. pmf N x * real x)" proof - have "(\x. pmf N x *\<^sub>R real x) abs_summable_on {0} \ {Suc 0..}" using summable by (subst (asm) abs_summable_on_Sigma_iff) (auto simp add: mult.commute) then show ?thesis by (subst infsetsum_Un_Int) auto qed also have "\ = (\\<^sub>a(x, y)\Sigma {Suc 0..} (atLeastAtMost (Suc 0)). pmf N x)" using summable by (subst infsetsum_Sigma) (auto simp add: mult.commute) also have "\ = (\\<^sub>ax\Sigma {Suc 0..} atLeast. pmf N (snd x))" by (subst infsetsum_reindex_bij_betw[of "\(x,y). (y,x)", symmetric]) (auto intro!: bij_betw_imageI simp add: inj_on_def case_prod_beta) also have "\ = infsetsum (\i. measure_pmf.prob N {i..}) {1..}" using assms by (subst infsetsum_Sigma) (auto simp add: measure_pmf_conv_infsetsum abs_summable_on_Sigma_iff infsetsum_Sigma') finally show "measure_pmf.expectation N real = infsetsum (\i. measure_pmf.prob N {i..}) {1..}" by simp have "(\x. pmf N x *\<^sub>R real x) abs_summable_on {0} \ {Suc 0..}" using summable by (subst (asm) abs_summable_on_Sigma_iff) (auto simp add: mult.commute) then have "(\x. pmf N x *\<^sub>R real x) abs_summable_on UNIV" by (simp add: atLeast_Suc) then have "integrable (count_space UNIV) (\x. pmf N x *\<^sub>R real x)" by (subst abs_summable_on_def[symmetric]) blast then show "integrable N real" by (subst measure_pmf_eq_density, subst integrable_density) auto qed text \ The expected height of a skip list has no closed-form expression but we can approximate it. We start by showing how we can calculate an infinite sum over the natural numbers with an integral over the positive reals and the floor function. \ lemma infsetsum_set_nn_integral_reals: assumes "f abs_summable_on UNIV" "\n. f n \ 0" shows "infsetsum f UNIV = set_nn_integral lborel {0::real..} (\x. f (nat (floor x)))" proof - have "x < 1 + (floor x)"for x::real by linarith then have "\n. real n \ x \ x < 1 + real n" if "x \ 0" for x using that of_nat_floor by (intro exI[of _ "nat (floor x)"]) auto then have "{0..} = (\n. {real n..\<^sup>+x\{0::real..}. ennreal (f (nat \x\))\lborel = (\n. \\<^sup>+x\{real n..<1 + real n}. ennreal (f (nat \x\))\lborel)" by (auto simp add: disjoint_family_on_def nn_integral_disjoint_family) also have "\ = (\n. \\<^sup>+x\{real n..<1 + real n}. ennreal (f n)\lborel)" by(subst suminf_cong, rule nn_integral_cong_AE) (auto intro!: eventuallyI simp add: indicator_def floor_eq4) also have "\ = (\n. ennreal (f n))" by (auto intro!: suminf_cong simp add: nn_integral_cmult) also have "\ = infsetsum f {0..}" using assms suminf_ennreal2 abs_summable_on_nat_iff' summable_norm_cancel by (auto simp add: infsetsum_nat) finally show ?thesis by simp qed lemma nn_integral_nats_reals: shows "(\\<^sup>+ i. ennreal (f i) \count_space UNIV) = \\<^sup>+x\{0::real..}. ennreal (f (nat \x\))\lborel" proof - have "x < 1 + (floor x)"for x::real by linarith then have "\n. real n \ x \ x < 1 + real n" if "x \ 0" for x using that of_nat_floor by (intro exI[of _ "nat (floor x)"]) auto then have "{0..} = (\n. {real n..\<^sup>+x\{0::real..}. f (nat \x\)\lborel = (\n. \\<^sup>+x\{real n..<1 + real n}. ennreal (f (nat \x\))\lborel)" by (auto simp add: disjoint_family_on_def nn_integral_disjoint_family) also have "\ = (\n. \\<^sup>+x\{real n..<1 + real n}. ennreal (f n)\lborel)" by(subst suminf_cong,rule nn_integral_cong_AE) (auto intro!: eventuallyI simp add: indicator_def floor_eq4) also have "\ = (\n. ennreal (f n))" by (auto intro!: suminf_cong simp add: nn_integral_cmult) also have "\ = (\\<^sup>+ i. ennreal (f i) \count_space UNIV)" by (simp add: nn_integral_count_space_nat) finally show ?thesis by simp qed lemma nn_integral_floor_less_eq: assumes "\x y. x \ y \ f y \ f x" shows "\\<^sup>+x\{0::real..}. ennreal (f x)\lborel \ \\<^sup>+x\{0::real..}. ennreal (f (nat \x\))\lborel" using assms by (auto simp add: indicator_def intro!: nn_integral_mono ennreal_leI) lemma nn_integral_finite_imp_abs_sumable_on: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes "nn_integral (count_space A) (\x. norm (f x)) < \" shows "f abs_summable_on A" using assms unfolding abs_summable_on_def integrable_iff_bounded by auto lemma nn_integral_finite_imp_abs_sumable_on': assumes "nn_integral (count_space A) (\x. ennreal (f x)) < \" "\x. f x \ 0" shows "f abs_summable_on A" using assms unfolding abs_summable_on_def integrable_iff_bounded by auto text \ We now show that $\int_0^\infty 1 - (1 - q^x) ^ n\;dx = \frac{- H_n}{\ln q}$ if $0 < q < 1$. \ lemma harm_integral_x_raised_n: "set_integrable lborel {0::real..1} (\x. (\i\{..i\{..x. (\i\{..i\{..i\{..x. (\i\{..auto simp add: einterval_def\) moreover have "set_integrable lborel (einterval 0 1) (\x. (x ^ n))" proof - have "set_integrable lborel {0::real..1} (\x. (x ^ n))" by (rule borel_integrable_atLeastAtMost') (auto intro!: borel_integrable_atLeastAtMost' continuous_intros) then show ?thesis by (rule set_integrable_subset) (auto simp add: einterval_def) qed ultimately show ?thesis by (auto intro!: borel_integrable_atLeastAtMost' simp add: interval_lebesgue_integrable_def) qed also have "(LBINT x=0..1. x ^ n) = 1 / (1 + real n)" proof - have "(LBINT x=0..1. x ^ n) = LBINT x. x ^ n * indicator {0..1} x " proof - have "AE x in lborel. x ^ n * indicator {0..1} x = indicator (einterval 0 1) x * x ^ n" by(rule eventually_mono[OF eventually_conj[OF AE_lborel_singleton[of 1] AE_lborel_singleton[of 0]]]) (auto simp add: indicator_def einterval_def) then show ?thesis using integral_cong_AE unfolding interval_lebesgue_integral_def set_lebesgue_integral_def by (auto intro!: integral_cong_AE) qed then show ?thesis by (auto simp add: integral_power) qed finally show ?case using Suc by (auto simp add: harm_def inverse_eq_divide) qed (auto simp add: harm_def) qed lemma harm_integral_0_1_fraction: "set_integrable lborel {0::real..1} (\x. (1 - x ^ n) / (1 - x))" "(LBINT x = 0..1. ((1 - x ^ n) / (1 - x))) = harm n" proof - show "set_integrable lborel {0::real..1} (\x. (1 - x ^ n) / (1 - x))" proof - have "AE x\{0::real..1} in lborel. (1 - x ^ n) / (1 - x) = sum ((^) x) {..{0::real<..<1} in lborel. (1 - x ^ n) / (1 - x) = sum ((^) x) {.. {0<..<1}" shows "set_integrable lborel (einterval 0 \) (\x. (1 - (1 - q powr x) ^ n))" "(LBINT x=0..\. 1 - (1 - q powr x) ^ n) = - harm n / ln q" proof - have [simp]: "q powr (log q (1-x)) = 1 - x" if "x \ {0<..<1}" for x using that assms by (subst powr_log_cancel) auto have 1: "((ereal \ (\x. log q (1 - x)) \ real_of_ereal) \ 0) (at_right 0)" using assms unfolding zero_ereal_def ereal_tendsto_simps by (auto intro!: tendsto_eq_intros) have 2: "((ereal \ (\x. log q (1-x)) \ real_of_ereal) \ \) (at_left 1)" proof - have "filterlim ((-) 1) (at_right 0) (at_left (1::real))" by (intro filterlim_at_withinI eventually_at_leftI[of 0]) (auto intro!: tendsto_eq_intros) then have "LIM x at_left 1. - inverse (ln q) * - ln (1 - x) :> at_top" using assms by (intro filterlim_tendsto_pos_mult_at_top [OF tendsto_const]) (auto simp: filterlim_uminus_at_top intro!: filterlim_compose[OF ln_at_0]) then show ?thesis unfolding one_ereal_def ereal_tendsto_simps log_def by (simp add: field_simps) qed have 3: "set_integrable lborel (einterval 0 1) (\x. (1 - (1 - q powr (log q (1 - x))) ^ n) * (- 1 / (ln q * (1 - x))))" proof - have "set_integrable lborel (einterval 0 1) (\x. - (1 / ln q) * ((1 - x ^ n) / (1 - x)))" by(intro set_integrable_mult_right) (auto intro!: harm_integral_0_1_fraction intro: set_integrable_subset simp add: einterval_def) then show ?thesis by(subst set_integrable_cong_AE[where g="\x. - (1 / ln q) * ((1 - x ^ n) / (1 - x))"]) (auto intro!: eventuallyI simp add: einterval_def) qed have 4: "LBINT x=0..1. - ((1 - (1 - q powr log q (1 - x)) ^ n) / (ln q * (1 - x))) = - (harm n / ln q)" (is "?lhs = ?rhs") proof - have "?lhs = LBINT x=0..1. ((1 - x ^ n) / (1 - x)) * (- 1 / ln q)" using assms by (intro interval_integral_cong_AE) (auto intro!: eventuallyI simp add: max_def einterval_def field_simps) also have "\ = harm n * (-1 / ln q)" using harm_integral_0_1_fraction by (subst interval_lebesgue_integral_mult_left) auto finally show ?thesis by auto qed note sub = interval_integral_substitution_nonneg [where f = "(\x. (1 - (1 - q powr x) ^ n))" and g="(\x. log q (1-x))" and g'="(\x. - 1 / (ln q * (1 - x)))" and a = 0 and b = 1] show "set_integrable lborel (einterval 0 \) (\x. (1 - (1 - q powr x) ^ n))" using assms 1 2 3 4 by (intro sub) (auto intro!: derivative_eq_intros mult_nonneg_nonpos2 tendsto_intros power_le_one) show "(LBINT x=0..\. 1 - (1 - q powr x) ^ n) = - harm n / ln q" using assms 1 2 3 4 by (subst sub) (auto intro!: derivative_eq_intros mult_nonneg_nonpos2 tendsto_intros power_le_one) qed lemma one_minus_one_minus_q_x_n_nn_integral: fixes q::real assumes "q \ {0<..<1}" shows "set_nn_integral lborel {0..} (\x. (1 - (1 - q powr x) ^ n)) = LBINT x=0..\. 1 - (1 - q powr x) ^ n" proof - have "set_nn_integral lborel {0..} (\x. (1 - (1 - q powr x) ^ n)) = nn_integral lborel (\x. indicator (einterval 0 \) x * (1 - (1 - q powr x) ^ n))" using assms by (intro nn_integral_cong_AE eventually_mono[OF AE_lborel_singleton[of 0]]) (auto simp add: indicator_def einterval_def) also have "\ = ennreal (LBINT x. indicator (einterval 0 \) x * (1 - (1 - q powr x) ^ n))" using one_minus_one_minus_q_x_n_integral assms by(intro nn_integral_eq_integral) (auto simp add: indicator_def einterval_def set_integrable_def intro!: eventuallyI power_le_one powr_le1) finally show ?thesis by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def) qed text \ We can now derive bounds for the expected height. \ context random_skip_list begin definition EH\<^sub>N where "EH\<^sub>N n = measure_pmf.expectation (H\<^sub>N n) real" lemma EH\<^sub>N_bounds': fixes n::nat assumes "p \ {0<..<1}" "0 < n" shows "- harm n / ln q - 1 \ EH\<^sub>N n" "EH\<^sub>N n \ - harm n / ln q" "integrable (H\<^sub>N n) real" proof - define f where "f = (\x. 1 - (1 - q ^ x) ^ n)" define f' where "f' = (\x. 1 - (1 - q powr x) ^ n)" have q: "q \ {0<..<1}" unfolding q_def using assms by auto have f_descending: "f y \ f x" if "x \ y" for x y unfolding f_def using that q by (auto intro!: power_mono simp add: power_decreasing power_le_one_iff) have f'_descending: "f' y \ f' x" if "x \ y" "0 \ x" for x y unfolding f'_def using that q by (auto intro!: power_mono simp add: ln_powr powr_def mult_nonneg_nonpos) have [simp]: "harm n / ln q <= 0" using harm_nonneg ln_ge_zero_imp_ge_one q by (intro divide_nonneg_neg) auto have f_nn_integral_harm: "- harm n / ln q \ \\<^sup>+ x. (f x) \count_space UNIV" "(\\<^sup>+ i. f (i + 1) \count_space UNIV) \ - harm n / ln q" proof - have "(\\<^sup>+ i. f (i + 1) \count_space UNIV) = (\\<^sup>+x\{0::real..}. (f (nat \x\ + 1))\lborel)" using nn_integral_nats_reals by auto also have "\ = \\<^sup>+x\{0::real..}. ennreal (f' (nat \x\ + 1))\lborel" proof - have "0 \ x \ (1 - q * q ^ nat \x\) ^ n = (1 - q powr (1 + real_of_int \x\)) ^ n" for x::real - using q by (metis greaterThanLessThan_iff powr_int powr_mult_base zero_le_floor) + using q by (subst powr_realpow [symmetric]) (auto simp: powr_add) then show ?thesis unfolding f_def f'_def using q by (auto intro!: nn_integral_cong ennreal_cong simp add: powr_real_of_int indicator_def) qed also have "\ \ set_nn_integral lborel {0..} f'" proof - have "x \ 1 + real_of_int \x\" for x by linarith then show ?thesis by (auto simp add: indicator_def intro!: f'_descending nn_integral_mono ennreal_leI) qed also have harm_integral_f': "\ = - harm n / ln q" unfolding f'_def using q by (auto intro!: ennreal_cong simp add: one_minus_one_minus_q_x_n_nn_integral one_minus_one_minus_q_x_n_integral) finally show "(\\<^sup>+ i. f (i + 1) \count_space UNIV) \ - harm n / ln q" by simp note harm_integral_f'[symmetric] also have "set_nn_integral lborel {0..} f' \ \\<^sup>+x\{0::real..}. f' (nat \x\)\lborel" using assms f'_descending by (auto simp add: indicator_def intro!: nn_integral_mono ennreal_leI) also have "\ = \\<^sup>+x\{0::real..}. f (nat \x\)\lborel" unfolding f_def f'_def using q by (auto intro!: nn_integral_cong ennreal_cong simp add: powr_real_of_int indicator_def) also have "\ = (\\<^sup>+ x. f x \count_space UNIV)" using nn_integral_nats_reals by auto finally show "- harm n / ln q \ \\<^sup>+ x. f x \count_space UNIV" by simp qed then have f1_abs_summable_on: "(\i. f (i + 1)) abs_summable_on UNIV" unfolding f_def using q by (intro nn_integral_finite_imp_abs_sumable_on') (auto simp add: f_def le_less_trans intro!: power_le_one mult_le_one) then have f_abs_summable_on: "f abs_summable_on {1..}" using Suc_le_lessD greaterThan_0 by (subst abs_summable_on_reindex_bij_betw[symmetric, where g="\x. x + 1" and A="UNIV"]) auto also have "(f abs_summable_on {1..}) = ((\x. measure_pmf.prob (H\<^sub>N n) {x..}) abs_summable_on {1..})" proof - have "((\x. measure_pmf.prob (H\<^sub>N n) {x..}) abs_summable_on {1..}) = ((\x. measure_pmf.prob (H\<^sub>N n) {x - 1<..}) abs_summable_on {1..})" by (auto intro!: measure_prob_cong_0 abs_summable_on_cong) also have "\ = (f abs_summable_on {1..})" using assms by (intro abs_summable_on_cong) (auto simp add: f_def prob_Max_IID_geometric_greaterThan) finally show ?thesis by simp qed finally have EH\<^sub>N_sum: "EH\<^sub>N n = (\\<^sub>ai\{1..}. measure_pmf.prob (H\<^sub>N n) {i..})" "integrable (measure_pmf (H\<^sub>N n)) real" unfolding EH\<^sub>N_def using expectation_prob_atLeast by auto then show "integrable (measure_pmf (H\<^sub>N n)) real" by simp have EH\<^sub>N_sum': "EH\<^sub>N n = infsetsum f {1..}" proof - have "EH\<^sub>N n = (\\<^sub>ak\{1..}. measure_pmf.prob (H\<^sub>N n) {k - 1<..})" unfolding EH\<^sub>N_sum by (auto intro!: measure_prob_cong_0 infsetsum_cong) also have "\ = infsetsum f {1..}" using assms by (intro infsetsum_cong) (auto simp add: f_def prob_Max_IID_geometric_greaterThan) finally show ?thesis by simp qed also have "\ = (\\<^sub>ak. f (k + 1))" using Suc_le_lessD greaterThan_0 by (subst infsetsum_reindex_bij_betw[symmetric, where g="\x. x + 1" and A="UNIV"]) auto also have "ennreal \ = (\\<^sup>+x\{0::real..}. f (nat \x\ + 1)\lborel)" using f1_abs_summable_on q by (intro infsetsum_set_nn_integral_reals) (auto simp add: f_def mult_le_one power_le_one) also have "\ = (\\<^sup>+ i. f (i + 1) \count_space UNIV)" using nn_integral_nats_reals by auto also have "\ \ - harm n / ln q" using f_nn_integral_harm by auto finally show "EH\<^sub>N n \ - harm n / ln q" by (subst (asm) ennreal_le_iff) (auto) have "EH\<^sub>N n + 1 = (\\<^sub>ax\{Suc 0..}. f x) + (\\<^sub>ax\{0}. f x)" using assms by (subst EH\<^sub>N_sum') (auto simp add: f_def) also have "\ = infsetsum f UNIV" using f_abs_summable_on by (subst infsetsum_Un_disjoint[symmetric]) (auto intro!: infsetsum_cong) also have "\ = (\\<^sup>+x\{0::real..}. f (nat \x\)\lborel)" proof - have "f abs_summable_on ({0} \ {1..})" using f_abs_summable_on by (intro abs_summable_on_union) (auto) also have "{0::nat} \ {1..} = UNIV" by auto finally show ?thesis using q by (intro infsetsum_set_nn_integral_reals) (auto simp add: f_def mult_le_one power_le_one) qed also have "\ = (\\<^sup>+ x. f x \count_space UNIV)" using nn_integral_nats_reals by auto also have "... \ - harm n / ln q" using f_nn_integral_harm by auto finally have "- harm n / ln q \ EH\<^sub>N n + 1" by (subst (asm) ennreal_le_iff) (auto simp add: EH\<^sub>N_def) then show "- harm n / ln q - 1 \ EH\<^sub>N n" by simp qed theorem EH\<^sub>N_bounds: fixes n::nat assumes "p \ {0<..<1}" shows "- harm n / ln q - 1 \ EH\<^sub>N n" "EH\<^sub>N n \ - harm n / ln q" "integrable (H\<^sub>N n) real" proof - show "- harm n / ln q - 1 \ EH\<^sub>N n" using assms EH\<^sub>N_bounds' by (cases "n = 0") (auto simp add: EH\<^sub>N_def H\<^sub>N_def H_def SL_def harm_expand) show "EH\<^sub>N n \ - harm n / ln q" using assms EH\<^sub>N_bounds' by (cases "n = 0") (auto simp add: EH\<^sub>N_def H\<^sub>N_def H_def SL_def harm_expand) show "integrable (H\<^sub>N n) real" using assms EH\<^sub>N_bounds' by (cases "n = 0") (auto simp add: H\<^sub>N_def H_def SL_def intro!: integrable_measure_pmf_finite) qed end (* context random_skip_list *) subsection \Expected Length of Search Path\ text \ Let @{term "A::'a::linorder set"} and @{term "f::'a \ nat"} where f is an abstract description of a skip list (assign each value its maximum level). steps A f s u l starts on the rightmost element on level s in the skip lists. If possible it moves up, if not it moves to the left. For every step up it adds cost u and for every step to the left it adds cost l. steps A f 0 1 1 therefore walks from the bottom right corner of a skip list to the top left corner of a skip list and counts all steps. \ \ \NOTE: You could also define steps with lsteps and then prove that the following recursive definition holds\ function steps :: "'a :: linorder set \ ('a \ nat) \ nat \ nat \ nat \ nat" where "steps A f l up left = (if A = {} \ infinite A then 0 else (let m = Max A in (if f m < l then steps (A - {m}) f l up left else (if f m > l then up + steps A f (l + 1) up left else left + steps (A - {m}) f l up left))))" by pat_completeness auto termination proof (relation "(\(A,f,l,a,b). card A) <*mlex*> (\(A,f,l,a,b). Max (f ` A) - l) <*mlex*> {}", goal_cases) case 1 then show ?case by(intro wf_mlex wf_empty) next case 2 then show ?case by (intro mlex_less) (auto simp: card_gt_0_iff) next case (3 A f l a b x) then have "Max (f ` A) - Suc l < Max (f ` A) - l" by (meson Max_gr_iff Max_in diff_less_mono2 finite_imageI imageI image_is_empty lessI) with 3 have "((A, f, l + 1, a, b), A, f, l, a, b) \ (\(A, f, l, a, b). Max (f ` A) - l) <*mlex*> {}" by (intro mlex_less) (auto) with 3 show ?case apply - apply(rule mlex_leq) by auto next case 4 then show ?case by (intro mlex_less) (auto simp: card_gt_0_iff) qed declare steps.simps[simp del] text \ lsteps is similar to steps but is using lists instead of sets. This makes the proofs where we use induction easier. \ function lsteps :: "'a list \ ('a \ nat) \ nat \ nat \ nat \ nat" where "lsteps [] f l up left = 0" | "lsteps (x#xs) f l up left = (if f x < l then lsteps xs f l up left else (if f x > l then up + lsteps (x#xs) f (l + 1) up left else left + lsteps xs f l up left))" by pat_completeness auto termination proof (relation "(\(xs,f,l,a,b). length xs) <*mlex*> (\(xs,f,l,a,b). Max (f ` set xs) - l) <*mlex*> {}", goal_cases) case 1 then show ?case by(intro wf_mlex wf_empty) next case 2 then show ?case by (auto intro: mlex_less simp: card_gt_0_iff) next case (3 n f l a b) show ?case by (rule mlex_leq) (use 3 in \auto intro: mlex_less mlex_leq intro!: diff_less_mono2 simp add: Max_gr_iff\) next case 4 then show ?case by (intro mlex_less) (auto simp: card_gt_0_iff) qed declare lsteps.simps(2)[simp del] lemma steps_empty [simp]: "steps {} f l up left = 0" by (simp add: steps.simps) lemma steps_lsteps: "steps A f l u v = lsteps (rev (sorted_list_of_set A)) f l u v" proof (cases "finite A \ A \ {}") case True then show ?thesis proof(induction "(rev (sorted_list_of_set A))" f l u v arbitrary: A rule: lsteps.induct) case (2 y ys f l u v A) then have y_ys: "y = Max A" "ys = rev (sorted_list_of_set (A - {y}))" by (auto simp add: sorted_list_of_set_Max_snoc) consider (a) "l < f y" | (b) "f y < l" | (c) "f y = l" by fastforce then have "steps A f l u v = lsteps (y#ys) f l u v" proof cases case a then show ?thesis by (subst steps.simps, subst lsteps.simps) (use y_ys 2 in auto) next case b then show ?thesis using y_ys 2(1) by (cases "ys = []") (auto simp add: steps.simps lsteps.simps) next case c then have "steps (A - {Max A}) f l u v = lsteps (rev (sorted_list_of_set (A - {Max A}))) f l u v" by (cases "A = {Max A}") (use y_ys 2 in \auto intro!: 2(3) simp add: steps.simps\) then show ?thesis by (subst steps.simps, subst lsteps.simps) (use y_ys 2 in auto) qed then show ?case using 2 by simp qed (auto simp add: steps.simps) qed (auto simp add: steps.simps) lemma lsteps_comp_map: "lsteps zs (f \ g) l u v = lsteps (map g zs) f l u v" by (induction zs "f \ g" l u v rule: lsteps.induct) (auto simp add: lsteps.simps) lemma steps_image: assumes "finite A" "mono_on g A" "inj_on g A" shows "steps A (f \ g) l u v = steps (g ` A) f l u v" proof - have "(sorted_list_of_set (g ` A)) = map g (sorted_list_of_set A)" using sorted_list_of_set_image assms by auto also have "rev \ = map g (rev (sorted_list_of_set A))" using rev_map by auto finally show ?thesis by (simp add: steps_lsteps lsteps_comp_map) qed lemma lsteps_cong: assumes "ys = xs" "\x. x \ set xs \ f x = g x" "l = l'" shows "lsteps xs f l u v = lsteps ys g l' u v" using assms proof (induction xs f l u v arbitrary: ys l' rule: lsteps.induct) case (2 x xs f l up left) then show ?case by (subst \ys = x # xs\, subst lsteps.simps, subst (2) lsteps.simps) auto qed (auto) lemma steps_cong: assumes "A = B" "\x. x \ A \ f x = g x" "l = l'" shows "steps A f l u v = steps B g l' u v" using assms by (cases "A = {} \ infinite A") (auto simp add: steps_lsteps steps.simps intro!: lsteps_cong) lemma lsteps_f_add': shows "lsteps xs f l u v = lsteps xs (\x. f x + m) (l + m) u v" by (induction xs f l u v rule: lsteps.induct) (auto simp add: lsteps.simps) lemma steps_f_add': shows "steps A f l u v = steps A (\x. f x + m) (l + m) u v" by (cases "A = {} \ infinite A") (auto simp add: steps_lsteps steps.simps intro!: lsteps_f_add') lemma lsteps_smaller_set: assumes "m \ l" shows "lsteps xs f l u v = lsteps [x \ xs. m \ f x] f l u v" using assms by (induction xs f l u v rule: lsteps.induct) (auto simp add: lsteps.simps) lemma steps_smaller_set: assumes "finite A" "m \ l" shows "steps A f l u v = steps {x\A. f x \ m} f l u v" using assms by(cases "A = {} \ infinite A") (auto simp add: steps_lsteps steps.simps rev_filter sorted_list_of_set_filter intro!: lsteps_smaller_set) lemma lsteps_level_greater_fun_image: assumes "\x. x \ set xs \ f x < l" shows "lsteps xs f l u v = 0" using assms by (induction xs f l u v rule: lsteps.induct) (auto simp add: lsteps.simps) lemma lsteps_smaller_card_Max_fun': assumes "\x \ set xs. l \ f x" shows "lsteps xs f l u v + l * u \ v * length xs + u * Max ((f ` (set xs)) \ {0})" using assms proof (induction xs f l u v rule: lsteps.induct) case (1 f l up left) then show ?case by (simp) next case (2 x xs f l up left) consider "l = f x" "\y\set xs. l \ f y" | "f x = l" "\ (\y\set xs. l \ f y)" | "f x < l" | "l < f x" by fastforce then show ?case proof cases assume a: "l = f x" "\y\set xs. l \ f y" have "lsteps (x # xs) f l up left + l * up = lsteps xs f l up left + f x * up + left" using a by (auto simp add: lsteps.simps) also have "lsteps xs f l up left + f x * up \ left * length xs + up * Max (f ` set xs \ {0})" using a 2 by blast also have "up * Max (f ` set xs \ {0}) \ up * Max (insert (f x) (f ` set xs))" by simp finally show ?case by auto next assume a: "f x = l" "\ (\y\set xs. l \ f y)" have "lsteps (x # xs) f l up left + l * up = lsteps xs f l up left + f x * up + left" using a by (auto simp add: lsteps.simps) also have "lsteps xs f l up left = 0" using a by (subst lsteps_level_greater_fun_image) auto also have "f x * up \ up * Max (insert (f x) (f ` set xs))" by simp finally show ?case by simp next assume a: "f x < l" then have "lsteps (x # xs) f l up left = lsteps xs f l up left" by (auto simp add: lsteps.simps) also have "\ + l * up \ left * length (x # xs) + up * Max (insert 0 (f ` set xs))" using a 2 by auto also have "Max (insert 0 (f ` set xs)) \ Max (f ` set (x # xs) \ {0})" by simp finally show ?case by simp next assume "f x > l" then show ?case using 2 by (subst lsteps.simps) auto qed qed lemma steps_smaller_card_Max_fun': assumes "finite A" "\x\A. l \ f x" shows "steps A f l up left + l * up \ left * card A + up * Max\<^sub>0 (f ` A)" proof - let ?xs = "rev (sorted_list_of_set A)" have "steps A f l up left = lsteps (rev (sorted_list_of_set A)) f l up left" using steps_lsteps by blast also have "\ + l * up \ left * length ?xs + up * Max (f ` set ?xs \ {0})" using assms by (intro lsteps_smaller_card_Max_fun') auto also have "left * length ?xs = left * card A" using assms sorted_list_of_set_length by (auto) also have "set ?xs = A" using assms by (auto) finally show ?thesis by simp qed lemma lsteps_height: assumes "\x \ set xs. l \ f x" shows "lsteps xs f l up 0 + up * l = up * Max\<^sub>0 (f ` (set xs))" using assms proof (induction xs f l up "0::nat" rule: lsteps.induct) case (2 x xs f l up) consider "l = f x" "\y\set xs. l \ f y" | "f x = l" "\ (\y\set xs. l \ f y)" | "f x < l" | "l < f x" by fastforce then show ?case proof cases assume 0: "l = f x" "\y\set xs. l \ f y" then have 1: "set xs \ {}" using 2 by auto then have "\xa\set xs. f x \ f xa" using 0 2 by force then have "f x \ Max (f ` set xs)" using 0 2 by (subst Max_ge_iff) auto then have "max (f x) (Max (f ` set xs)) = (Max (f ` set xs))" using 0 2 by (auto intro!: simp add: max_def) then show ?case using 0 1 2 by (subst lsteps.simps) (auto) next assume 0: "f x = l" "\ (\y\set xs. l \ f y)" then have "Max (insert l (f ` set xs)) = l" by (intro Max_eqI) (auto) moreover have "lsteps xs f l up 0 = 0" using 0 by (subst lsteps_level_greater_fun_image) auto ultimately show ?case using 0 by (subst lsteps.simps) auto next assume 0: "f x < l" then have 1: "set xs \ {}" using 2 by auto then have "\xa\set xs. f x \ f xa" using 0 2 by force then have " f x \ Max (f ` set xs)" using 0 2 by (subst Max_ge_iff) auto then have "max (f x) (Max (f ` set xs)) = Max (f ` set xs)" using 0 2 by (auto intro!: simp add: max_def) then show ?case using 0 1 2 by (subst lsteps.simps) (auto) next assume "f x > l" then show ?case using 2 by (subst lsteps.simps) auto qed qed (simp) lemma steps_height: assumes "finite A" shows "steps A f 0 up 0 = up * Max\<^sub>0 (f ` A)" proof - have "steps A f 0 up 0 = lsteps (rev (sorted_list_of_set A)) f 0 up 0 + up * 0" by (subst steps_lsteps) simp also have "\ = up * Max (f ` A \ {0})" if "A \ {}" using assms that by (subst lsteps_height) auto finally show ?thesis using assms by (cases "A = {}") (auto) qed context random_skip_list begin text \ We can now define the pmf describing the length of the search path in a skip list. Like the height it only depends on the number of elements in the skip list's underlying set. \ definition R where "R A u l = map_pmf (\f. steps A f 0 u l) (SL A)" definition R\<^sub>N :: "nat \ nat \ nat \ nat pmf" where "R\<^sub>N n u l = R {..N_alt_def: "R\<^sub>N n u l = map_pmf (\f. steps {..N n)" unfolding SL\<^sub>N_def R\<^sub>N_def R_def by simp context includes monad_normalisation begin lemma R_R\<^sub>N: assumes "finite A" "p \ {0..1}" shows "R A u l = R\<^sub>N (card A) u l" proof - let ?steps = "\A f. steps A f 0 u l" let ?f' = "bij_mono_map_set_to_nat A" have "R A u l = SL A \ (\f. return_pmf (?steps A f))" unfolding R_def map_pmf_def by simp also have "\ = SL\<^sub>N (card A) \ (\f. return_pmf (?steps A (f \ ?f')))" proof - have "?f' x \ {.. A" for x using that unfolding bij_mono_map_set_to_nat_def by (auto) then show ?thesis using assms bij_mono_map_set_to_nat unfolding SL_def SL\<^sub>N_def by (subst Pi_pmf_bij_betw[of _ ?f' "{.. = SL\<^sub>N (card A) \ (\f. return_pmf (?steps {..N_def R_def SL\<^sub>N_def SL_def by (simp add: map_pmf_def) qed text \ @{const R\<^sub>N} fulfills a recurrence relation. If we move up or to the left the ``remaining'' length of the search path is again a slightly different probability distribution over the length. \ lemma R\<^sub>N_recurrence: assumes "0 < n" "p \ {0<..1}" shows "R\<^sub>N n u l = do { b \ bernoulli_pmf p; if b then \ \leftwards\ map_pmf (\n. n + l) (R\<^sub>N (n - 1) u l) else do { \ \upwards\ m \ binomial_pmf (n - 1) (1 - p); map_pmf (\n. n + u) (R\<^sub>N (m + 1) u l) } }" proof - define B where "B = (\b. insert (n-1) {x \ {.. b x})" have "R\<^sub>N n u l = map_pmf (\f. steps {..N n)" by (auto simp add: R\<^sub>N_def R_def SL\<^sub>N_def) also have "\ = map_pmf (\f. steps {..(y, f). f(n-1 := y)) (pair_pmf (geometric_pmf p) (SL\<^sub>N (n - 1))))" proof - have "{.._. geometric_pmf p)) = map_pmf (\(y, f). f(n - 1 := y)) (pair_pmf (geometric_pmf p) (Pi_pmf {.._. geometric_pmf p)))" using assms by (subst Pi_pmf_insert[of "{.._. geometric_pmf p", symmetric]) (auto) then show ?thesis by (simp add: SL\<^sub>N_def SL_def) qed also have "\ = do { g \ geometric_pmf p; f \ SL\<^sub>N (n - 1); return_pmf (steps {.. = do { b \ bernoulli_pmf p; g \ if b then return_pmf 0 else map_pmf Suc (geometric_pmf p); f \ SL\<^sub>N (n - 1); return_pmf (steps {.. = do { b \ bernoulli_pmf p; if b then do { g \ return_pmf 0; f \ SL\<^sub>N (n - 1); return_pmf (steps {.. map_pmf Suc (geometric_pmf p); f \ SL\<^sub>N (n - 1); return_pmf (steps {.. return_pmf 0; f \ SL\<^sub>N (n - 1); return_pmf (steps {.. SL\<^sub>N (n - 1); return_pmf (steps {.. = map_pmf (\n. n + l) (map_pmf (\f. steps {..N (n - 1)))" proof - have I: "{.. = map_pmf (\n. n + l) (R\<^sub>N (n - 1) u l)" unfolding R\<^sub>N_def R_def SL\<^sub>N_def by simp also have "map_pmf Suc (geometric_pmf p) \ (\g. SL\<^sub>N (n - 1) \ (\f. return_pmf (steps {.._. bernoulli_pmf p) \ (\b. map_pmf Suc (geometric_pmf p) \ (\g. Pi_pmf {x \ {.. b x} 0 (\_. map_pmf Suc (geometric_pmf p)) \ (\f. return_pmf (steps {..N_def SL_def by (subst Pi_pmf_geometric_filter) (auto) also have "\ = do { b \ Pi_pmf {.._. bernoulli_pmf p); f \ Pi_pmf (insert (n-1) {x \ {.. b x}) 0 (\_. map_pmf Suc (geometric_pmf p)); return_pmf (steps {.. = do { b \ Pi_pmf {.._. bernoulli_pmf p); f \ Pi_pmf (B b) 1 (\_. map_pmf Suc (geometric_pmf p)); return_pmf (steps {..x. if x \ (B b) then f x else 0) 0 u l)}" by (subst Pi_pmf_default_swap[symmetric, of _ _ _ 1]) (auto simp add: map_pmf_def B_def) also have "\ = do { b \ Pi_pmf {.._. bernoulli_pmf p); f \ SL (B b); return_pmf (steps {..x. if x \ (B b) then Suc (f x) else 0) 0 u l)}" proof - have *: "(Suc \ f) x = Suc (f x)" for x and f::"nat \ nat" by simp have "(\f. return_pmf (steps {..x. if x \ B b then (Suc \ f) x else 0) 0 u l)) = (\f. return_pmf (steps {..x. if x \ B b then Suc (f x) else 0) 0 u l))" for b by (subst *) (simp) then show ?thesis by (subst Pi_pmf_map[of _ _ 0]) (auto simp add: map_pmf_def B_def SL_def) qed also have "\ = do { b \ Pi_pmf {.._. bernoulli_pmf p); r \ R (B b) u l; return_pmf (u + r)}" proof - have "steps {..x. if x \ B b then Suc (f x) else 0) 0 u l = u + steps (B b) f 0 u l" for f b proof - have "Max {..x. if x \ B b then Suc (f x) else 0) 0 u l = u + (steps {..x. if x \ (B b) then Suc (f x) else 0) 1 u l)" unfolding B_def using assms by (subst steps.simps) (auto simp add: Let_def) also have "steps {..x. if x \ (B b) then Suc (f x) else 0) 1 u l = steps (B b) (\x. if x \ (B b) then Suc (f x) else 0) 1 u l" proof - have "{x \ {.. (if x \ B b then Suc (f x) else 0)} = B b" using assms unfolding B_def by force then show ?thesis by (subst steps_smaller_set[of _ 1]) auto qed also have "\ = steps (B b) (\x. f x + 1) 1 u l" by (rule steps_cong) (auto) also have "\ = steps (B b) f 0 u l" by (subst (2) steps_f_add'[of _ _ _ _ _ 1]) simp finally show ?thesis by auto qed then show ?thesis by (simp add: R_def map_pmf_def) qed also have "\ = do { b \ Pi_pmf {.._. bernoulli_pmf (1 - p)); let m = 1 + card {x. x < n - 1 \ b x}; r \ R {.. b x}) = (Suc (card {x. x < n - 1 \ b x}))" for b using assms by (auto simp add: card_insert_if) have "Pi_pmf {.._. bernoulli_pmf p) = Pi_pmf {.._. map_pmf Not (bernoulli_pmf (1 - p)))" using assms by (subst bernoulli_pmf_Not) auto also have "\ = map_pmf ((\) Not) (Pi_pmf {.._. bernoulli_pmf (1 - p)))" using assms by (subst Pi_pmf_map[of _ _ False]) auto finally show ?thesis unfolding B_def using assms * by (subst R_R\<^sub>N) (auto simp add: R_R\<^sub>N map_pmf_def) qed also have "\ = binomial_pmf (n - 1) (1 - p) \ (\m. map_pmf (\n. n + u) (R\<^sub>N (m + 1) u l))" using assms by (subst binomial_pmf_altdef'[where A = "{..N_def R_def SL_def map_pmf_def ac_simps) finally show ?thesis by simp qed end (* context includes monad_normalisation *) text \ The expected height and length of search path defined as non-negative integral. It's easier to prove the recurrence relation of the expected length of the search path using non-negative integrals. \ definition NH\<^sub>N where "NH\<^sub>N n = nn_integral (H\<^sub>N n) real" definition NR\<^sub>N where "NR\<^sub>N n u l = nn_integral (R\<^sub>N n u l) real" lemma NH\<^sub>N_EH\<^sub>N: assumes "p \ {0<..<1}" shows "NH\<^sub>N n = EH\<^sub>N n" using assms EH\<^sub>N_bounds unfolding EH\<^sub>N_def NH\<^sub>N_def by (subst nn_integral_eq_integral) (auto) lemma R\<^sub>N_0 [simp]: "R\<^sub>N 0 u l = return_pmf 0" unfolding R\<^sub>N_def R_def SL_def by (auto simp add: steps.simps) lemma NR\<^sub>N_bounds: fixes u l::nat shows "NR\<^sub>N n u l \ l * n + u * NH\<^sub>N n" proof - have "NR\<^sub>N n u l = \\<^sup>+ x. x \measure_pmf (R\<^sub>N n u l)" unfolding NR\<^sub>N_def R\<^sub>N_alt_def by (simp add: ennreal_of_nat_eq_real_of_nat) also have "\ \ \\<^sup>+ x. x \(measure_pmf (map_pmf (\f. l * n + u * Max\<^sub>0 (f ` {..N n)))" using of_nat_mono[OF steps_smaller_card_Max_fun'[of "{..N_alt_def by (cases "n = 0") (auto intro!: nn_integral_mono) also have "\ = l * n + u * NH\<^sub>N n" unfolding NH\<^sub>N_def H\<^sub>N_def H_def SL\<^sub>N_def by (auto simp add: nn_integral_add nn_integral_cmult ennreal_of_nat_eq_real_of_nat ennreal_mult) finally show "NR\<^sub>N n u l \ l * n + u * NH\<^sub>N n" by simp qed lemma NR\<^sub>N_recurrence: assumes "0 < n" "p \ {0<..<1}" shows "NR\<^sub>N n u l = (p * (l + NR\<^sub>N (n - 1) u l) + q * (u + (\kN (k + 1) u l * (pmf (binomial_pmf (n - 1) q) k)))) / (1 - (q ^ n))" proof - define B where "B = (\n k. pmf (binomial_pmf n q) k)" have q: "q \ {0<..<1}" using assms unfolding q_def by auto then have "q ^ n < 1" using assms power_Suc_less_one by (induction n) (auto) then have qn: "q ^ n \ {0<..<1}" using assms q by (auto) have "NR\<^sub>N n u l = p * (l + NR\<^sub>N (n - 1) u l) + q * (u + \\<^sup>+ k. NR\<^sub>N (k + 1) u l \measure_pmf (binomial_pmf (n - 1) q))" using assms unfolding NR\<^sub>N_def by(subst R\<^sub>N_recurrence) (auto simp add: field_simps nn_integral_add q_def ennreal_of_nat_eq_real_of_nat) also have "(\\<^sup>+ m. NR\<^sub>N (m + 1) u l \measure_pmf (binomial_pmf (n - 1) q)) = (\k\n - 1. NR\<^sub>N (k + 1) u l * B (n - 1) k)" using assms unfolding B_def q_def by (auto simp add: nn_integral_measure_pmf_finite) also have "\ = (\k\{.. {n - 1}. NR\<^sub>N (k + 1) u l * B (n - 1) k)" by (rule sum.cong) (auto) also have "\ = (\kN (k + 1) u l * B (n - 1) k) + NR\<^sub>N n u l * q ^ (n - 1)" unfolding B_def q_def using assms by (subst sum.union_disjoint) (auto) finally have "NR\<^sub>N n u l = p * (l + NR\<^sub>N (n - 1) u l) + q * ((\kN (k + 1) u l * B (n - 1) k) + u) + NR\<^sub>N n u l * (q ^ (n - 1)) * q" using assms by (auto simp add: field_simps numerals) also have "NR\<^sub>N n u l * (q ^ (n - 1)) * q = (q ^ n) * NR\<^sub>N n u l" using q power_minus_mult[of _ q] assms by (subst mult_ac, subst ennreal_mult[symmetric], auto simp add: mult_ac) finally have 1: "NR\<^sub>N n u l = p * (l + NR\<^sub>N (n - 1) u l) + q * (u + (\kN (k + 1) u l * (B (n - 1) k))) + (q ^ n) * NR\<^sub>N n u l " by (simp add: add_ac) have "x - z = y" if "x = y + z" "z \ \" for x y z::ennreal using that by (subst that) (auto) have "NR\<^sub>N n u l \ l * n + u * NH\<^sub>N n" using NR\<^sub>N_bounds by (auto simp add: ennreal_of_nat_eq_real_of_nat) also have "NH\<^sub>N n = EH\<^sub>N n" using assms NH\<^sub>N_EH\<^sub>N by auto also have "(l * n) + u * ennreal (EH\<^sub>N n) < \" by (simp add: ennreal_mult_less_top of_nat_less_top) finally have 3: "NR\<^sub>N n u l \ \" by simp have 2: "x = y / (1 - a)" if "x = y + a * x" and t: "x \ \" "a \ {0<..<1}" for x y::ennreal and a::real proof - have "y = x - a * x" using t by (subst that) (auto simp add: ennreal_mult_eq_top_iff) also have "\ = x * (ennreal 1 - ennreal a)" using that by (auto simp add: mult_ac ennreal_right_diff_distrib) also have "ennreal 1 - ennreal a = ennreal (1 - a)" using that by (subst ennreal_minus) (auto) also have "x * (1 - a) / (1 - a) = x" using that ennreal_minus_eq_0 not_less by (subst mult_divide_eq_ennreal) auto finally show ?thesis by simp qed have "NR\<^sub>N n u l = (p * (l + NR\<^sub>N (n - 1) u l) + q * (u + (\kN (k + 1) u l * (B (n - 1) k)))) / (1 - (q ^ n))" using 1 3 assms qn by (intro 2) auto then show ?thesis unfolding B_def by simp qed lemma NR\<^sub>n_NH\<^sub>N: "NR\<^sub>N n u 0 = u * NH\<^sub>N n" proof - have "NR\<^sub>N n u 0 = \\<^sup>+ f. steps {..measure_pmf (SL\<^sub>N n)" unfolding NR\<^sub>N_def R\<^sub>N_alt_def by (auto simp add: ennreal_of_nat_eq_real_of_nat) also have "\ = \\<^sup>+ f. of_nat u * of_nat (Max\<^sub>0 (f ` {..measure_pmf (SL\<^sub>N n)" by (intro nn_integral_cong) (auto simp add: steps_height) also have "\ = u * NH\<^sub>N n" by (auto simp add: NH\<^sub>N_def H\<^sub>N_def H_def SL\<^sub>N_def ennreal_of_nat_eq_real_of_nat nn_integral_cmult) finally show ?thesis by simp qed lemma NR\<^sub>N_recurrence': assumes "0 < n" "p \ {0<..<1}" shows "NR\<^sub>N n u l = (p * l + p * NR\<^sub>N (n - 1) u l + q * u + q * (\kN (k + 1) u l * (pmf (binomial_pmf (n - 1) q) k))) / (1 - (q ^ n))" unfolding NR\<^sub>N_recurrence[OF assms] by (auto simp add: field_simps ennreal_of_nat_eq_real_of_nat ennreal_mult' ennreal_mult'') lemma NR\<^sub>N_l_0: assumes "0 < n" "p \ {0<..<1}" shows "NR\<^sub>N n u 0 = (p * NR\<^sub>N (n - 1) u 0 + q * (u + (\kN (k + 1) u 0 * (pmf (binomial_pmf (n - 1) q) k)))) / (1 - (q ^ n))" unfolding NR\<^sub>N_recurrence[OF assms] by (simp) lemma NR\<^sub>N_u_0: assumes "0 < n" "p \ {0<..<1}" shows "NR\<^sub>N n 0 l = (p * (l + NR\<^sub>N (n - 1) 0 l) + q * (\kN (k + 1) 0 l * (pmf (binomial_pmf (n - 1) q) k))) / (1 - (q ^ n))" unfolding NR\<^sub>N_recurrence[OF assms] by (simp) lemma NR\<^sub>N_0[simp]: "NR\<^sub>N 0 u l = 0" unfolding NR\<^sub>N_def R\<^sub>N_def R_def by (auto) lemma NR\<^sub>N_1: assumes "p \ {0<..<1}" shows "NR\<^sub>N 1 u l = (u * q + l * p) / p" proof - have "NR\<^sub>N 1 u l = (ennreal p * of_nat l + ennreal q * of_nat u) / ennreal (1 - q)" using assms by (subst NR\<^sub>N_recurrence) auto also have "(ennreal p * of_nat l + ennreal q * of_nat u) = (u * q + l * p)" using assms q_def by (subst ennreal_plus) (auto simp add: field_simps ennreal_mult' ennreal_of_nat_eq_real_of_nat) also have "\ / ennreal (1 - q) = ennreal ((u * q + l * p) / (1 - q))" using q_def assms by (intro divide_ennreal) auto finally show ?thesis unfolding q_def by simp qed lemma NR\<^sub>N_NR\<^sub>N_l_0: assumes n: "0 < n" and p: "p \ {0<..<1}" and "u \ 1" shows "NR\<^sub>N n u 0 = (u * q / (u * q + l * p)) * NR\<^sub>N n u l" using n proof (induction n rule: less_induct) case (less i) have 1: "0 < u * q" unfolding q_def using assms by simp moreover have "0 \ l * p" using assms by auto ultimately have 2: "0 < u * q + l * p" by arith define c where "c = ennreal (u * q / (u * q + l * p))" have [simp]: "c / c = 1" proof - have "u * q / (u * q + l * p) \ 0" using assms q_def 2 by auto then show ?thesis unfolding c_def using p q_def by (auto intro!: ennreal_divide_self) qed show ?case proof (cases "i = 1") case True have "c * NR\<^sub>N i u l = c * ((u * q + l * p) / p)" unfolding c_def True by (subst NR\<^sub>N_1[OF p]) auto also have "\ = ennreal ((u * q / (u * q + l * p)) * ((u * q + l * p) / p))" unfolding c_def using assms q_def by (subst ennreal_mult'') auto also have "(u * q / (u * q + l * p)) * ((u * q + l * p) / p) = u * q / p" proof - have I: "(a / b) * (b / c) = a / c" if "0 < b" for a b c::"real" using that by (auto) show ?thesis using 2 q_def by (intro I) auto qed also have "\ = NR\<^sub>N i u 0" unfolding True c_def by (subst NR\<^sub>N_1[OF p]) (auto) finally show ?thesis unfolding c_def using True by simp next case False then have i: "i > 1" using less by auto define c where "c = ennreal (u * q / (u * q + l * p))" define B where "B = (\kN (k + 1) u l * ennreal (pmf (binomial_pmf (i - 1) q) k))" have "NR\<^sub>N i u 0 = (p * NR\<^sub>N (i - 1) u 0 + q * (u + (\kN (k + 1) u 0 * (pmf (binomial_pmf (i - 1) q) k)))) / (1 - (q ^ i))" using less assms by (subst NR\<^sub>N_l_0) auto also have "q * (u + (\kN (k + 1) u 0 * (pmf (binomial_pmf (i - 1) q) k))) = q * u + q * (\kN (k + 1) u 0 * (pmf (binomial_pmf (i - 1) q) k))" using assms q_def by (auto simp add: field_simps ennreal_of_nat_eq_real_of_nat ennreal_mult) also have "NR\<^sub>N (i - 1) u 0 = c * NR\<^sub>N (i - 1) u l" unfolding c_def using less i by (intro less) (auto) also have "(\kN (k + 1) u 0 * ennreal (pmf (binomial_pmf (i - 1) q) k)) = (\kN (k + 1) u l * ennreal (pmf (binomial_pmf (i - 1) q) k))" by (auto intro!: sum.cong simp add: less c_def) also have "\ = c * B" unfolding B_def by (subst sum_distrib_left) (auto intro!: sum.cong mult_ac) also have "q * (c * B) = c * (q * B)" by (simp add: mult_ac) also have "ennreal (q * real u) = q * u * ((u * q + l * p) / (u * q + l * p))" using assms 2 by (auto simp add: field_simps q_def) also have "\ = c * (real u * q + real l * p)" unfolding c_def using 2 by (subst ennreal_mult''[symmetric]) (auto simp add: mult_ac) also have "c * ennreal (real u * q + real l * p) + c * (ennreal q * B) = c * (ennreal (real u * q + real l * p) + (ennreal q * B))" by (auto simp add: field_simps) also have "ennreal p * (c * NR\<^sub>N (i - 1) u l) = c * (ennreal p * NR\<^sub>N (i - 1) u l)" by (simp add: mult_ac) also have "(c * (ennreal p * NR\<^sub>N (i - 1) u l) + c * (ennreal (u * q + l * p) + ennreal q * B)) = c * ((ennreal p * NR\<^sub>N (i - 1) u l) + (ennreal (u * q + l * p) + ennreal q * B))" by (auto simp add: field_simps) also have " c * (ennreal p * NR\<^sub>N (i - 1) u l + (ennreal (u * q + l * p) + ennreal q * B)) / ennreal (1 - q ^ i) = c * ((ennreal p * NR\<^sub>N (i - 1) u l + (ennreal (u * q + l * p) + ennreal q * B)) / ennreal (1 - q ^ i))" by (auto simp add: ennreal_times_divide) also have "(ennreal p * NR\<^sub>N (i - 1) u l + (ennreal (real u * q + real l * p) + ennreal q * B)) / ennreal (1 - q ^ i) = NR\<^sub>N i u l" apply(subst (2) NR\<^sub>N_recurrence') using i assms q_def by (auto simp add: field_simps B_def ennreal_of_nat_eq_real_of_nat ennreal_mult' ennreal_mult'') finally show ?thesis unfolding c_def by simp qed qed text \ Assigning 1 as the cost for going up and/or left, we can now show the relation between the expected length of the reverse search path and the expected height. \ definition EL\<^sub>N where "EL\<^sub>N n = measure_pmf.expectation (R\<^sub>N n 1 1) real" theorem EH\<^sub>N_EL\<^sub>s\<^sub>p: assumes "p \ {0<..<1}" shows "1 / q * EH\<^sub>N n = EL\<^sub>N n" proof - have 1: "ennreal (1 / y * x) = r" if "ennreal x = y * r" "x \ 0" "y > 0" for x y::real and r::ennreal proof - have "ennreal ((1 / y) * x) = ennreal (1 / y) * ennreal x" using that apply(subst ennreal_mult'') by auto also note that(1) also have "ennreal (1 / y) * (ennreal y * r) = ennreal ((1 / y) * y) * r" using that by (subst ennreal_mult'') (auto simp add: mult_ac) also have "(1 / y) * y = 1" using that by (auto) finally show ?thesis by auto qed have "EH\<^sub>N n = NH\<^sub>N n" using NH\<^sub>N_EH\<^sub>N assms by auto also have "NH\<^sub>N n = NR\<^sub>N n 1 0" using NR\<^sub>n_NH\<^sub>N by auto also have "NR\<^sub>N n 1 0 = q * NR\<^sub>N n 1 1" if "n > 0" using NR\<^sub>N_NR\<^sub>N_l_0[of _ 1 1] that assms q_def by force finally have "ennreal (EH\<^sub>N n) = q * NR\<^sub>N n 1 1" if "n > 0" using that by blast then have "1 / q * EH\<^sub>N n = NR\<^sub>N n 1 1" if "n > 0" using that assms q_def by (intro 1) (auto simp add: EH\<^sub>N_def H\<^sub>N_def H_def) moreover have "1 / q * EH\<^sub>N n = NR\<^sub>N n 1 1" if "n = 0" unfolding that by (auto simp add: EH\<^sub>N_def H\<^sub>N_def H_def) ultimately have 2: "ennreal (1 / q * EH\<^sub>N n) = NR\<^sub>N n 1 1" by blast also have "NR\<^sub>N n 1 1 = EL\<^sub>N n" using 2 assms EH\<^sub>N_bounds unfolding EL\<^sub>N_def NR\<^sub>N_def by(subst nn_integral_eq_integral) (auto intro!: integrableI_nn_integral_finite[where x="EH\<^sub>N n / q"]) finally show ?thesis using assms q_def ennreal_inj unfolding EL\<^sub>N_def EH\<^sub>N_def H\<^sub>N_def H_def SL_def by (auto) qed end (* context random_skip_list *) thm random_skip_list.EH\<^sub>N_EL\<^sub>s\<^sub>p[unfolded random_skip_list.q_def] random_skip_list.EH\<^sub>N_bounds'[unfolded random_skip_list.q_def] end