This instance will be upgraded to Heptapod 0.23.2 on 2021-08-05 at 11:00 UTC+2 (a few minutes of down time)

Commit cde334d2 authored by Manuel Eberl's avatar Manuel Eberl
Browse files

adapted to isabelle-dev/73253:f6bb31879698

parent 3ce2153720f3
......@@ -137,7 +137,7 @@ proof -
from assms have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>P) = (\<integral>x. f x \<partial>P)"
by (intro nn_integral_eq_integral) auto
with assms show ?thesis
using nn_integral_Markov_inequality[of f P "space P" "1 / c"]
using nn_integral_Markov_inequality[of f "space P" P "1 / c"]
by (simp cong: nn_integral_cong add: emeasure_eq_measure ennreal_mult[symmetric])
qed
......
......@@ -63,7 +63,7 @@ proof -
have "(\<integral>\<^sup>+ x. ennreal (X x) \<partial>M) = (\<integral>x. X x \<partial>M)"
using assms by (intro nn_integral_eq_integral) auto
thus ?thesis
using assms nn_integral_Markov_inequality[of X M "space M" "1 / t"]
using assms nn_integral_Markov_inequality[of X "space M" M "1 / t"]
by (auto cong: nn_integral_cong simp: emeasure_eq_measure ennreal_mult[symmetric])
qed
......
......@@ -10,113 +10,12 @@ theory Geometric_PMF
"Monad_Normalisation.Monad_Normalisation"
begin
lemma geometric_sums_times_n:
fixes c::"'a::{banach,real_normed_field}"
assumes "norm c < 1"
shows "(\<lambda>n. c^n * of_nat n) sums (c / (1 - c)\<^sup>2)"
proof -
have "(\<lambda>n. c * z ^ n) sums (c / (1 - z))" if "norm z < 1" for z
using geometric_sums sums_mult that by fastforce
moreover have "((\<lambda>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 "(\<lambda>n. diffs (\<lambda>n. c) n * c ^ n) sums (c / (1 - c)\<^sup>2)"
using assms by (intro termdiffs_sums_strong)
then have "(\<lambda>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 "(\<lambda>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 \<in> {0<..1}"
shows "integrable (geometric_pmf p) real"
proof -
have "summable (\<lambda>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 (\<lambda>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)
qed
lemma expectation_geometric_pmf:
assumes "p \<in> {0<..1}"
shows "measure_pmf.expectation (geometric_pmf p) real = (1 - p) / p"
proof -
have "(\<lambda>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 "(\<lambda>n. p * ((1 - p) ^ n * n)) = (\<lambda>n. (1 - p) ^ n * p * real n)"
by auto
ultimately have *: "(\<lambda>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 =
(\<integral>n. pmf (geometric_pmf p) n * real n \<partial>count_space UNIV)"
unfolding measure_pmf_eq_density by (subst integral_density) auto
also have "integrable (count_space UNIV) (\<lambda>n. pmf (geometric_pmf p) n * real n)"
using * assms unfolding integrable_count_space_nat_iff by (simp add: sums_iff)
hence "(\<integral>n. pmf (geometric_pmf p) n * real n \<partial>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 \<in> {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 \<in> {0<..1}"
shows "geometric_pmf p =
do {b \<leftarrow> 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 \<bind>
(\<lambda>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 "\<dots> = (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 "\<dots> = measure_pmf.expectation (bernoulli_pmf p)
(\<lambda>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 "\<dots> = pmf (bernoulli_pmf p \<bind>
(\<lambda>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 \<in> {0<..<1} \<Longrightarrow> 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 \<in> {0<..1}"
shows "measure_pmf.prob (geometric_pmf p) {..n} = (1 - (1 - p)^(n + 1))"
......
......@@ -6,7 +6,6 @@
section \<open>Randomized Skip Lists\<close>
theory Skip_List
imports Geometric_PMF
Pi_pmf
Misc
"Monad_Normalisation.Monad_Normalisation"
begin
......
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