Theory Distributed_Distinct_Elements_Balls_and_Bins
section ‹Balls and Bins›
text ‹The balls and bins model describes the probability space of throwing r balls into b
bins. This section derives the expected number of bins hit by at least one ball, as well as the
variance in the case that each ball is thrown independently. Further, using an approximation
argument it is then possible to derive bounds for the same measures in the case when the balls
are being thrown only $k$-wise independently. The proofs follow the reasoning described in
\cite[\S A.1]{kane2010} but improve on the constants, as well as constraints.›
theory Distributed_Distinct_Elements_Balls_and_Bins
imports
Distributed_Distinct_Elements_Preliminary
Discrete_Summation.Factorials
"HOL-Combinatorics.Stirling"
"HOL-Computational_Algebra.Polynomial"
"HOL-Decision_Procs.Approximation"
begin
hide_fact "Henstock_Kurzweil_Integration.integral_sum"
hide_fact "Henstock_Kurzweil_Integration.integral_mult_right"
hide_fact "Henstock_Kurzweil_Integration.integral_nonneg"
hide_fact "Henstock_Kurzweil_Integration.integral_cong"
unbundle intro_cong_syntax
lemma sum_power_distrib:
fixes f :: "'a ⇒ real"
assumes "finite R"
shows "(∑i∈R. f i) ^ s = (∑xs | set xs ⊆ R ∧ length xs = s. (∏x ← xs. f x))"
proof (induction s)
case 0
have "{xs. xs = [] ∧ set xs ⊆ R} = {[]}"
by (auto simp add:set_eq_iff)
then show ?case by simp
next
case (Suc s)
have a:
"(⋃i∈R. (#) i ` {xs. set xs ⊆ R ∧ length xs = s}) = {xs. set xs ⊆ R ∧ length xs = Suc s}"
by (subst lists_length_Suc_eq) auto
have "sum f R ^ Suc s = (sum f R) * (sum f R)^s"
by simp
also have "... = (sum f R) * (∑xs | set xs ⊆ R ∧ length xs = s. (∏x ← xs. f x))"
using Suc by simp
also have "... = (∑i ∈ R. (∑xs | set xs ⊆ R ∧ length xs = s. (∏x ← i#xs. f x)))"
by (subst sum_product) simp
also have "... =
(∑i ∈ R. (∑xs ∈ (λxs. i#xs) ` {xs. set xs ⊆ R ∧ length xs = s}. (∏x ← xs. f x)))"
by (subst sum.reindex) (auto)
also have "... = (∑xs∈(⋃i∈R. (#) i ` {xs. set xs ⊆ R ∧ length xs = s}). (∏x ← xs. f x))"
by (intro sum.UNION_disjoint[symmetric] assms ballI finite_imageI finite_lists_length_eq)
auto
also have "... = (∑xs| set xs ⊆ R ∧ length xs = Suc s. (∏x ← xs. f x))"
by (intro sum.cong a) auto
finally show ?case by simp
qed
lemma sum_telescope_eq:
fixes f :: "nat ⇒ 'a :: {comm_ring_1}"
shows "(∑k∈{Suc m..n}. f k - f (k - 1)) = of_bool(m ≤ n) *(f n - f m)"
by (cases "m ≤ n", subst sum_telescope'', auto)
text ‹An improved version of @{thm [source] diff_power_eq_sum}.›
lemma power_diff_sum:
fixes a b :: "'a :: {comm_ring_1,power}"
shows "a^k - b^k = (a-b) * (∑i = 0..<k. a ^ i * b ^ (k - 1 - i))"
proof (cases "k")
case 0
then show ?thesis by simp
next
case (Suc nat)
then show ?thesis
unfolding Suc diff_power_eq_sum
using atLeast0LessThan diff_Suc_1 by presburger
qed
lemma power_diff_est:
assumes "(a :: real) ≥ b"
assumes "b ≥ 0"
shows "a^k - b^k ≤ (a-b) * k * a^(k-1)"
proof -
have "a^k - b^k = (a-b) * (∑i = 0..<k. a ^ i * b ^ (k - 1 - i))"
by (rule power_diff_sum)
also have "... ≤ (a-b) * (∑i = 0..<k. a^i * a^(k-1-i))"
using assms by (intro mult_left_mono sum_mono mult_right_mono power_mono, auto)
also have "... = (a-b) * (k * a^(k-1))"
by (simp add:power_add[symmetric])
finally show ?thesis by simp
qed
lemma power_diff_est_2:
assumes "(a :: real) ≥ b"
assumes "b ≥ 0"
shows "a^k - b^k ≥ (a-b) * k * b^(k-1)"
proof -
have "(a-b) * k * b^(k-1) = (a-b) * (∑i=0..<k. b^i * b^(k-1-i))"
by (simp add:power_add[symmetric])
also have "... ≤ (a-b)* (∑i=0..<k. a^i * b^(k-1-i))"
using assms
by (intro mult_left_mono sum_mono mult_right_mono power_mono) auto
also have "... = a^k - b^k"
by (rule power_diff_sum[symmetric])
finally show ?thesis by simp
qed
lemma of_bool_prod:
assumes "finite R"
shows "(∏ j ∈ R. of_bool(f j)) = (of_bool(∀j ∈ R. f j) :: real)"
using assms by (induction R rule:finite_induct) auto
text ‹Additional results about falling factorials:›
lemma ffact_nonneg:
fixes x :: real
assumes "k - 1 ≤ x"
shows "ffact k x ≥ 0"
using assms unfolding prod_ffact[symmetric]
by (intro prod_nonneg ballI) simp
lemma ffact_pos:
fixes x :: real
assumes "k - 1 < x"
shows "ffact k x > 0"
using assms unfolding prod_ffact[symmetric]
by (intro prod_pos ballI) simp
lemma ffact_mono:
fixes x y :: real
assumes "k-1 ≤ x" "x ≤ y"
shows "ffact k x ≤ ffact k y"
using assms
unfolding prod_ffact[symmetric]
by (intro prod_mono) auto
lemma ffact_of_nat_nonneg:
fixes x :: "'a :: {comm_ring_1, linordered_nonzero_semiring}"
assumes "x ∈ ℕ"
shows "ffact k x ≥ 0"
proof -
obtain y where y_def: "x = of_nat y"
using assms(1) Nats_cases by auto
have "(0::'a) ≤ of_nat (ffact k y)"
by simp
also have "... = ffact k x"
by (simp add:of_nat_ffact y_def)
finally show ?thesis by simp
qed
lemma ffact_suc_diff:
fixes x :: "('a :: comm_ring_1)"
shows "ffact k x - ffact k (x-1) = of_nat k * ffact (k-1) (x-1)" (is "?L = ?R")
proof (cases "k")
case 0
then show ?thesis by simp
next
case (Suc n)
hence "?L = ffact (Suc n) x - ffact (Suc n) (x-1)" by simp
also have "... = x * ffact n (x-1) - ((x-1)-of_nat n) * ffact n (x-1)"
by (subst (1) ffact_Suc, simp add: ffact_Suc_rev)
also have "... = of_nat (Suc n) * ffact n (x-1)"
by (simp add:algebra_simps)
also have "... = of_nat k * ffact (k-1) (x-1)" using Suc by simp
finally show ?thesis by simp
qed
lemma ffact_bound:
"ffact k (n::nat) ≤ n^k"
proof -
have "ffact k n = (∏i=0..<k. (n-i))"
unfolding prod_ffact_nat[symmetric]
by simp
also have "... ≤ (∏i=0..<k. n)"
by (intro prod_mono) auto
also have "... = n^k"
by simp
finally show ?thesis by simp
qed
lemma fact_moment_binomial:
fixes n :: nat and α :: real
assumes "α ∈ {0..1}"
defines "p ≡ binomial_pmf n α"
shows "(∫ω. ffact s (real ω) ∂p) = ffact s (real n) * α^s" (is "?L = ?R")
proof (cases "s ≤ n")
case True
have "?L = (∑k≤n. (real (n choose k) * α ^ k * (1 - α) ^ (n - k)) * real (ffact s k))"
unfolding p_def using assms by (subst expectation_binomial_pmf') (auto simp add:of_nat_ffact)
also have "... = (∑k ∈ {0+s..(n-s)+s}. (real (n choose k) * α ^ k * (1 - α) ^ (n - k)) * ffact s k)"
using True ffact_nat_triv by (intro sum.mono_neutral_cong_right) auto
also have "... = (∑k=0..n-s. α^s * real (n choose (k+s)) * α^k * (1-α)^(n-(k+s)) *ffact s (k+s))"
by (subst sum.atLeastAtMost_shift_bounds, simp add:algebra_simps power_add)
also have "... = α^s * (∑k≤n-s. real (n choose (k+s))*ffact s (k+s)*α^k*(1-α)^((n-s)-k))"
using atMost_atLeast0 by (simp add: sum_distrib_left algebra_simps cong:sum.cong)
also have "... = α^s * (∑k≤n-s. real (n choose (k+s))*fact (k+s) / fact k * α^k*(1-α)^((n-s)-k))"
using real_of_nat_div[OF fact_dvd[OF le_add1]]
by (subst fact_div_fact_ffact_nat[symmetric], auto)
also have "... = α^s * (∑k≤n-s.
(fact n / fact (n-s)) * fact (n-s) / (fact ((n-s)-k) * fact k) * α^k*(1-α)^((n-s)-k))"
using True by (intro arg_cong2[where f="(*)"] sum.cong)
(auto simp add: binomial_fact algebra_simps)
also have "... = α^s * (fact n / fact (n - s)) *
(∑k≤n-s. fact (n-s) / (fact ((n-s)-k) * fact k) * α^k*(1-α)^((n-s)-k))"
by (simp add:sum_distrib_left algebra_simps)
also have "... = α^s * (fact n / fact (n - s)) * (∑k≤n-s. ((n-s) choose k) * α^k*(1-α)^((n-s)-k))"
using True by (intro_cong "[σ⇩2(*)]" more: sum.cong) (auto simp add: binomial_fact)
also have "... = α^s * real (fact n div fact (n - s)) * (α+(1-α))^(n-s)"
using True real_of_nat_div[OF fact_dvd] by (subst binomial_ring, simp)
also have "... = α^s * real (ffact s n)"
by (subst fact_div_fact_ffact_nat[OF True], simp)
also have "... = ?R"
by (subst of_nat_ffact, simp)
finally show ?thesis by simp
next
case False
have "?L = (∑k≤n. (real (n choose k) * α ^ k * (1 - α) ^ (n - k)) * real (ffact s k))"
unfolding p_def using assms by (subst expectation_binomial_pmf') (auto simp add:of_nat_ffact)
also have "... = (∑k≤n. (real (n choose k) * α ^ k * (1 - α) ^ (n - k)) * real 0)"
using False
by (intro_cong "[σ⇩2(*),σ⇩1 of_nat]" more: sum.cong ffact_nat_triv) auto
also have "... = 0" by simp
also have "... = real (ffact s n) * α^s"
using False by (subst ffact_nat_triv, auto)
also have "... = ?R"
by (subst of_nat_ffact, simp)
finally show ?thesis by simp
qed
text ‹The following describes polynomials of a given maximal degree as a subset of the functions,
similar to the subsets @{term "ℤ"} or @{term "ℚ"} as subsets of larger number classes.›
definition Polynomials (‹ℙ›)
where "Polynomials k = {f. ∃p. f = poly p ∧ degree p ≤ k}"
lemma Polynomials_mono:
assumes "s ≤ t"
shows "ℙ s ⊆ ℙ t"
using assms unfolding Polynomials_def by auto
lemma Polynomials_addI:
assumes "f ∈ ℙ k" "g ∈ ℙ k"
shows "(λω. f ω + g ω) ∈ ℙ k"
proof -
obtain pf pg where fg_def: "f = poly pf" "degree pf ≤ k" "g = poly pg" "degree pg ≤ k"
using assms unfolding Polynomials_def by blast
hence "degree (pf + pg) ≤ k" "(λx. f x + g x) = poly (pf + pg)"
using degree_add_le by auto
thus ?thesis unfolding Polynomials_def by auto
qed
lemma Polynomials_diffI:
fixes f g :: "'a :: comm_ring ⇒ 'a"
assumes "f ∈ ℙ k" "g ∈ ℙ k"
shows "(λx. f x - g x) ∈ ℙ k"
proof -
obtain pf pg where fg_def: "f = poly pf" "degree pf ≤ k" "g = poly pg" "degree pg ≤ k"
using assms unfolding Polynomials_def by blast
hence "degree (pf - pg) ≤ k" "(λx. f x - g x) = poly (pf - pg)"
using degree_diff_le by auto
thus ?thesis unfolding Polynomials_def by auto
qed
lemma Polynomials_idI:
"(λx. x) ∈ (ℙ 1 :: ('a::comm_ring_1 ⇒ 'a) set)"
proof -
have "(λx. x) = poly [: 0,(1::'a) :]"
by (intro ext, auto)
also have "... ∈ ℙ 1"
unfolding Polynomials_def by auto
finally show ?thesis by simp
qed
lemma Polynomials_constI:
"(λx. c) ∈ ℙ k"
proof -
have "(λx. c) = poly [: c :]"
by (intro ext, simp)
also have "... ∈ ℙ k"
unfolding Polynomials_def by auto
finally show ?thesis by simp
qed
lemma Polynomials_multI:
fixes f g :: "'a :: {comm_ring} ⇒ 'a"
assumes "f ∈ ℙ s" "g ∈ ℙ t"
shows "(λx. f x * g x) ∈ ℙ (s+t)"
proof -
obtain pf pg where xy_def: "f = poly pf" "degree pf ≤ s" "g = poly pg" "degree pg ≤ t"
using assms unfolding Polynomials_def by blast
have "degree (pf * pg) ≤ degree pf + degree pg"
by (intro degree_mult_le)
also have "... ≤ s + t"
using xy_def by (intro add_mono) auto
finally have "degree (pf * pg) ≤ s+t" by simp
moreover have "(λx. f x * g x) = poly (pf * pg)"
using xy_def by auto
ultimately show ?thesis unfolding Polynomials_def by auto
qed
lemma Polynomials_composeI:
fixes f g :: "'a :: {comm_semiring_0, semiring_no_zero_divisors} ⇒ 'a"
assumes "f ∈ ℙ s" "g ∈ ℙ t"
shows "(λx. f (g x)) ∈ ℙ (s*t)"
proof -
obtain pf pg where xy_def: "f = poly pf" "degree pf ≤ s" "g = poly pg" "degree pg ≤ t"
using assms unfolding Polynomials_def by blast
have "degree (pf ∘⇩p pg) = degree pf * degree pg"
by (intro degree_pcompose)
also have "... ≤ s * t"
using xy_def by (intro mult_mono) auto
finally have "degree (pf ∘⇩p pg) ≤ s * t"
by simp
moreover have "(λx. f (g x)) = poly (pf ∘⇩p pg)"
unfolding xy_def
by (intro ext poly_pcompose[symmetric])
ultimately show ?thesis unfolding Polynomials_def by auto
qed
lemma Polynomials_const_left_multI:
fixes c :: "'a :: {comm_ring}"
assumes "f ∈ ℙ k"
shows "(λx. c * f x) ∈ ℙ k"
proof -
have "(λx. c * f x) ∈ ℙ (0+k)"
by (intro Polynomials_multI Polynomials_constI assms)
thus ?thesis by simp
qed
lemma Polynomials_const_right_multI:
fixes c :: "'a :: {comm_ring}"
assumes "f ∈ ℙ k"
shows "(λx. f x * c) ∈ ℙ k"
proof -
have "(λx. f x * c) ∈ ℙ (k+0)"
by (intro Polynomials_multI Polynomials_constI assms)
thus ?thesis by simp
qed
lemma Polynomials_const_divI:
fixes c :: "'a :: {field}"
assumes "f ∈ ℙ k"
shows "(λx. f x / c) ∈ ℙ k"
proof -
have "(λx. f x * (1/c)) ∈ ℙ (k+0)"
by (intro Polynomials_multI Polynomials_constI assms)
thus ?thesis by simp
qed
lemma Polynomials_ffact: "(λx. ffact s (x - y)) ∈ (ℙ s :: ('a :: comm_ring_1 ⇒ 'a) set)"
proof (induction s arbitrary: y)
case 0
then show ?case
using Polynomials_constI[where c="1"] by simp
next
case (Suc s)
have "(λ(x :: 'a). ffact (Suc s) (x-y)) = (λx. (x-y) * ffact s (x - (y+1)))"
by (simp add: ffact_Suc algebra_simps)
also have "... ∈ ℙ (1+s)"
by (intro Polynomials_multI Suc Polynomials_diffI Polynomials_idI Polynomials_constI)
finally show ?case by simp
qed
lemmas Polynomials_intros =
Polynomials_const_divI
Polynomials_composeI
Polynomials_const_left_multI
Polynomials_const_right_multI
Polynomials_multI
Polynomials_addI
Polynomials_diffI
Polynomials_idI
Polynomials_constI
Polynomials_ffact
definition C⇩2 :: real where "C⇩2 = 7.5"
definition C⇩3 :: real where "C⇩3 = 16"
text ‹A locale fixing the sets of balls and bins›
locale balls_and_bins_abs =
fixes R :: "'a set" and B :: "'b set"
assumes fin_B: "finite B" and B_ne: "B ≠ {}"
assumes fin_R: "finite R"
begin
text ‹Independent balls and bins space:›
definition Ω
where "Ω = prod_pmf R (λ_. pmf_of_set B)"
lemma set_pmf_Ω: "set_pmf Ω = R →⇩E B"
unfolding Ω_def set_prod_pmf[OF fin_R]
by (simp add:comp_def set_pmf_of_set[OF B_ne fin_B])
lemma card_B_gt_0: "card B > 0"
using B_ne fin_B by auto
lemma card_B_ge_1: "card B ≥ 1"
using card_B_gt_0 by simp
definition "Z j ω = real (card {i. i ∈ R ∧ ω i = (j::'b)})"
definition "Y ω = real (card (ω ` R))"
definition "μ = real (card B) * (1 - (1-1/real (card B))^card R)"
text ‹Factorial moments for the random variable describing the number of times a bin will be hit:›
lemma fact_moment_balls_and_bins:
assumes "J ⊆ B" "J ≠ {}"
shows "(∫ω. ffact s (∑j ∈ J. Z j ω) ∂Ω) =
ffact s (real (card R)) * (real (card J) / real (card B))^s"
(is "?L = ?R")
proof -
let ?α = "real (card J) / real (card B)"
let ?q = "binomial_pmf (card R) ?α"
let ?Y = "(λω. card {r ∈ R. ω r ∈ J})"
have fin_J: "finite J"
using finite_subset assms(1) fin_B by auto
have Z_sum_eq: "(∑j ∈ J. Z j ω) = real (?Y ω)" for ω
proof -
have "?Y ω = card (⋃j ∈ J. {r ∈ R. ω r= j})"
by (intro arg_cong[where f="card"]) auto
also have "... = (∑i∈J. card {r ∈ R. ω r = i})"
using fin_R fin_J by (intro card_UN_disjoint) auto
finally have "?Y ω = (∑j ∈ J. card {r ∈ R. ω r = j})" by simp
thus ?thesis
unfolding Z_def of_nat_sum[symmetric] by simp
qed
have card_J: "card J ≤ card B"
using assms(1) fin_B card_mono by auto
have α_range: "?α ≥ 0" "?α ≤ 1"
using card_J card_B_gt_0 by auto
have "pmf (map_pmf (λω. ω ∈ J) (pmf_of_set B)) x = pmf (bernoulli_pmf ?α) x"
(is "?L1=?R1") for x
proof -
have "?L1 = real (card (B ∩ {ω. (ω ∈ J) = x})) / real (card B)"
using B_ne fin_B
by (simp add:pmf_map measure_pmf_of_set vimage_def)
also have "... = (if x then (card J) else (card (B - J))) / real (card B)"
using Int_absorb1[OF assms(1)] by (auto simp add:Diff_eq Int_def)
also have "... = (if x then (card J) / card B else (real (card B) - card J) / real (card B))"
using card_J fin_J assms(1) by (simp add: of_nat_diff card_Diff_subset)
also have "... = (if x then ?α else (1 - ?α))"
using card_B_gt_0 by (simp add:divide_simps)
also have "... = ?R1"
using α_range by auto
finally show ?thesis by simp
qed
hence c:"map_pmf (λω. ω ∈ J) (pmf_of_set B) = bernoulli_pmf ?α"
by (intro pmf_eqI) simp
have "map_pmf (λω. λr ∈ R. ω r ∈ J) Ω = prod_pmf R (λ_. (map_pmf (λω. ω ∈ J) (pmf_of_set B)))"
unfolding map_pmf_def Ω_def restrict_def using fin_R
by (subst Pi_pmf_bind[where d'="undefined"]) auto
also have "... = prod_pmf R (λ_. bernoulli_pmf ?α)"
unfolding c by simp
finally have b:"map_pmf (λω. λr ∈ R. ω r ∈ J) Ω = prod_pmf R (λ_. bernoulli_pmf ?α)"
by simp
have "map_pmf ?Y Ω = map_pmf ((λω. card {r ∈ R. ω r}) ∘ (λω. λr∈R. ω r ∈ J)) Ω"
unfolding comp_def
by (intro map_pmf_cong arg_cong[where f="card"]) (auto simp add:comp_def)
also have "... = (map_pmf (λω. card {r ∈ R. ω r}) ∘ map_pmf (λω. λr ∈ R. ω r ∈ J)) Ω"
by (subst map_pmf_compose[symmetric]) auto
also have "... = map_pmf (λω. card {r ∈ R. ω r}) (prod_pmf R (λ_. (bernoulli_pmf ?α)))"
unfolding comp_def b by simp
also have "... = ?q"
using α_range by (intro binomial_pmf_altdef'[symmetric] fin_R) auto
finally have a:"map_pmf ?Y Ω =?q"
by simp
have "?L = (∫ω. ffact s (real (?Y ω)) ∂Ω)"
unfolding Z_sum_eq by simp
also have "... = (∫ω. ffact s (real ω) ∂(map_pmf ?Y Ω))"
by simp
also have "... = (∫ω. ffact s (real ω) ∂?q)"
unfolding a by simp
also have "... = ?R"
using α_range by (subst fact_moment_binomial, auto)
finally show ?thesis by simp
qed
text ‹Expectation and variance for the number of distinct bins that are hit by at least one ball
in the fully independent model. The result for the variance is improved by a factor of $4$ w.r.t.
the paper.›
lemma
shows exp_balls_and_bins: "measure_pmf.expectation Ω Y = μ" (is "?AL = ?AR")
and var_balls_and_bins: "measure_pmf.variance Ω Y ≤ card R * (real (card R) - 1) / card B"
(is "?BL ≤ ?BR")
proof -
let ?b = "real (card B)"
let ?r = "card R"
define Z :: "'b ⇒ ('a ⇒ 'b) ⇒ real"
where "Z = (λi ω. of_bool(i ∉ ω ` R))"
define α where "α = (1 - 1 / ?b)^?r"
define β where "β = (1 - 2 / ?b)^?r"
have "card (B × B ∩ {x. fst x = snd x}) = card ((λx. (x,x)) ` B)"
by (intro arg_cong[where f="card"]) auto
also have "... = card B"
by (intro card_image, simp add:inj_on_def)
finally have d: "card (B × B ∩ {x. fst x = snd x}) = card B"
by simp
hence count_1: "real (card (B × B ∩ {x. fst x = snd x})) = card B"
by simp
have "card B + card (B × B ∩ -{x. fst x = snd x}) =
card (B × B ∩ {x. fst x = snd x}) + card (B × B ∩ -{x. fst x = snd x})"
by (subst d) simp
also have "... = card ((B × B ∩ {x. fst x = snd x}) ∪ (B × B ∩ -{x. fst x = snd x}))"
using finite_subset[OF _ finite_cartesian_product[OF fin_B fin_B]]
by (intro card_Un_disjoint[symmetric]) auto
also have "... = card (B × B)"
by (intro arg_cong[where f="card"]) auto
also have "... = card B^2"
unfolding card_cartesian_product by (simp add:power2_eq_square)
finally have "card B + card (B × B ∩ -{x. fst x = snd x}) = card B^2" by simp
hence count_2: "real (card (B × B ∩ -{x. fst x = snd x})) = real (card B)^2 - card B"
by (simp add:algebra_simps flip: of_nat_add of_nat_power)
hence "finite (set_pmf Ω)"
unfolding set_pmf_Ω
using fin_R fin_B by (auto intro!:finite_PiE)
hence int: "integrable (measure_pmf Ω) f"
for f :: "('a ⇒ 'b) ⇒ real"
by (intro integrable_measure_pmf_finite) simp
have a:"prob_space.indep_vars (measure_pmf Ω) (λi. discrete) (λx ω. ω x) R"
unfolding Ω_def using indep_vars_Pi_pmf[OF fin_R] by metis
have b: "(∫ω. of_bool (ω ` R ⊆ A) ∂Ω) = (real (card (B ∩ A)) / real (card B))^card R"
(is "?L = ?R") for A
proof -
have "?L = (∫ω. (∏ j ∈ R. of_bool(ω j ∈ A)) ∂Ω)"
by (intro Bochner_Integration.integral_cong ext)
(auto simp add: of_bool_prod[OF fin_R])
also have "... = (∏ j ∈ R. (∫ω. of_bool(ω j ∈ A) ∂Ω))"
using fin_R
by (intro prob_space.indep_vars_lebesgue_integral[OF prob_space_measure_pmf] int
prob_space.indep_vars_compose2[OF prob_space_measure_pmf a]) auto
also have "... = (∏ j ∈ R. (∫ω. of_bool(ω ∈ A) ∂(map_pmf (λω. ω j) Ω)))"
by simp
also have "... = (∏ j ∈ R. (∫ω. of_bool(ω ∈ A) ∂(pmf_of_set B)))"
unfolding Ω_def by (subst Pi_pmf_component[OF fin_R]) simp
also have "... = ((∑ω∈B. of_bool (ω ∈ A)) / real (card B)) ^ card R"
by (simp add: integral_pmf_of_set[OF B_ne fin_B])
also have "... = ?R"
unfolding of_bool_def sum.If_cases[OF fin_B] by simp
finally show ?thesis by simp
qed
have Z_exp: "(∫ω. Z i ω ∂Ω) = α" if "i ∈ B" for i
proof -
have "real (card (B ∩ -{i})) = real (card (B - {i}))"
by (intro_cong "[σ⇩1 card,σ⇩1 of_nat]") auto
also have "... = real (card B - card {i})"
using that by (subst card_Diff_subset) auto
also have "... = real (card B) - real (card {i})"
using fin_B that by (intro of_nat_diff card_mono) auto
finally have c: "real (card (B ∩ -{i})) = real (card B) - 1"
by simp
have "(∫ω. Z i ω ∂Ω) = (∫ω. of_bool(ω ` R ⊆ - {i}) ∂Ω)"
unfolding Z_def by simp
also have "... = (real (card (B ∩ -{i})) / real (card B))^card R"
by (intro b)
also have "... = ((real (card B) -1) / real (card B))^card R"
by (subst c) simp
also have "... = α"
unfolding α_def using card_B_gt_0
by (simp add:divide_eq_eq diff_divide_distrib)
finally show ?thesis
by simp
qed
have Z_prod_exp: "(∫ω. Z i ω * Z j ω ∂Ω) = (if i = j then α else β)"
if "i ∈ B" "j ∈ B" for i j
proof -
have "real (card (B ∩ -{i,j})) = real (card (B - {i,j}))"
by (intro_cong "[σ⇩1 card,σ⇩1 of_nat]") auto
also have "... = real (card B - card {i,j})"
using that by (subst card_Diff_subset) auto
also have "... = real (card B) - real (card {i,j})"
using fin_B that by (intro of_nat_diff card_mono) auto
finally have c: "real (card (B ∩ -{i,j})) = real (card B) - card {i,j}"
by simp
have "(∫ω. Z i ω * Z j ω ∂Ω) = (∫ω. of_bool(ω ` R ⊆ - {i,j}) ∂Ω)"
unfolding Z_def of_bool_conj[symmetric]
by (intro integral_cong ext) auto
also have "... = (real (card (B ∩ -{i,j})) / real (card B))^card R"
by (intro b)
also have "... = ((real (card B) - card {i,j}) / real (card B))^card R"
by (subst c) simp
also have "... = (if i = j then α else β)"
unfolding α_def β_def using card_B_gt_0
by (simp add:divide_eq_eq diff_divide_distrib)
finally show ?thesis by simp
qed
have Y_eq: "Y ω = (∑i ∈ B. 1 - Z i ω)" if "ω ∈ set_pmf Ω" for ω
proof -
have "set_pmf Ω ⊆ Pi R (λ_. B)"
using set_pmf_Ω by (simp add:PiE_def)
hence "ω ` R ⊆ B"
using that by auto
hence "Y ω = card (B ∩ ω ` R)"
unfolding Y_def using Int_absorb1 by metis
also have "... = (∑ i ∈ B. of_bool(i ∈ ω ` R))"
unfolding of_bool_def sum.If_cases[OF fin_B] by(simp)
also have "... = (∑ i ∈ B. 1 - Z i ω)"
unfolding Z_def by (intro sum.cong) (auto simp add:of_bool_def)
finally show "Y ω = (∑i ∈ B. 1 - Z i ω)" by simp
qed
have Y_sq_eq: "(Y ω)⇧2 = (∑(i,j) ∈ B × B. 1 - Z i ω - Z j ω + Z i ω * Z j ω)"
if "ω ∈ set_pmf Ω" for ω
unfolding Y_eq[OF that] power2_eq_square sum_product sum.cartesian_product
by (intro sum.cong) (auto simp add:algebra_simps)
have "measure_pmf.expectation Ω Y = (∫ω. (∑i ∈ B. 1 - Z i ω) ∂Ω)"
using Y_eq by (intro integral_cong_AE AE_pmfI) auto
also have "... = (∑i ∈ B. 1 - (∫ω. Z i ω ∂Ω))"
using int by simp
also have "... = ?b * (1 - α)"
using Z_exp by simp
also have "... = ?AR"
unfolding α_def μ_def by simp
finally show "?AL = ?AR" by simp
have "measure_pmf.variance Ω Y = (∫ω. Y ω^2 ∂Ω) - (∫ω. Y ω ∂Ω)^2"
using int by (subst measure_pmf.variance_eq) auto
also have "... =
(∫ω. (∑i ∈ B × B. 1 - Z (fst i) ω - Z (snd i) ω + Z (fst i) ω * Z (snd i) ω) ∂Ω) -
(∫ω. (∑i ∈ B. 1 - Z i ω) ∂Ω)^2"
using Y_eq Y_sq_eq
by (intro_cong "[σ⇩2(-),σ⇩2 power]" more: integral_cong_AE AE_pmfI) (auto simp add:case_prod_beta)
also have "... =
(∑i ∈ B × B. (∫ω. (1 - Z (fst i) ω - Z (snd i) ω + Z (fst i) ω * Z (snd i) ω) ∂Ω)) -
(∑i ∈ B. (∫ω. (1 - Z i ω) ∂Ω))^2"
by (intro_cong "[σ⇩2 (-), σ⇩2 power]" more: integral_sum int)
also have "... =
(∑i ∈ B × B. (∫ω. (1 - Z (fst i) ω - Z (snd i) ω + Z (fst i) ω * Z (snd i) ω) ∂Ω)) -
(∑i ∈ B × B. (∫ω. (1 - Z (fst i) ω) ∂Ω) * (∫ω. (1 - Z (snd i) ω) ∂Ω))"
unfolding power2_eq_square sum_product sum.cartesian_product
by (simp add:case_prod_beta)
also have "... = (∑(i,j) ∈ B × B. (∫ω. (1 - Z i ω - Z j ω + Z i ω * Z j ω) ∂Ω) -
(∫ω. (1 - Z i ω) ∂Ω) * (∫ω. (1 - Z j ω) ∂Ω))"
by (subst sum_subtractf[symmetric], simp add:case_prod_beta)
also have "... = (∑(i,j) ∈ B × B. (∫ω. Z i ω * Z j ω ∂Ω) -(∫ω. Z i ω ∂Ω) * (∫ ω. Z j ω ∂Ω))"
using int by (intro sum.cong refl) (simp add:algebra_simps case_prod_beta)
also have "... = (∑i ∈ B × B. (if fst i = snd i then α - α^2 else β - α^2))"
by (intro sum.cong refl)
(simp add:Z_exp Z_prod_exp mem_Times_iff case_prod_beta power2_eq_square)
also have "... = ?b * (α - α⇧2) + (?b^2 - card B) * (β - α⇧2)"
using count_1 count_2 finite_cartesian_product fin_B by (subst sum.If_cases) auto
also have "... = ?b^2 * (β - α⇧2) + ?b * (α - β)"
by (simp add:algebra_simps)
also have "... = ?b * ((1-1/?b)^?r - (1-2/?b)^?r) - ?b^2 * (((1-1/?b)^2)^?r - (1-2/?b)^?r)"
unfolding β_def α_def
by (simp add: power_mult[symmetric] algebra_simps)
also have "... ≤ card R * (real (card R) - 1)/ card B" (is "?L ≤ ?R")
proof (cases "?b ≥ 2")
case True
have "?L ≤
?b * (((1 - 1 /?b) - (1-2 /?b)) * ?r * (1-1/?b)^(?r - 1)) -
?b^2 * ((((1-1 /?b)^2) - ((1 - 2 /?b))) * ?r * ((1-2/?b))^(?r - 1))"
using True
by (intro diff_mono mult_left_mono power_diff_est_2 power_diff_est divide_right_mono)
(auto simp add:power2_eq_square algebra_simps)
also have "... = ?b * ((1/?b) * ?r * (1-1/?b)^(?r-1)) - ?b^2*((1/?b^2)*?r*((1-2/?b))^(?r-1))"
by (intro arg_cong2[where f="(-)"] arg_cong2[where f="(*)"] refl)
(auto simp add:algebra_simps power2_eq_square)
also have "... = ?r * ((1-1/?b)^(?r - 1) - ((1-2/?b))^(?r - 1))"
by (simp add:algebra_simps)
also have "... ≤ ?r * (((1-1/?b) - (1-2/?b)) * (?r - 1) * (1-1/?b)^(?r -1 -1))"
using True by (intro mult_left_mono power_diff_est) (auto simp add:algebra_simps)
also have "... ≤ ?r * ((1/?b) * (?r - 1) * 1^(?r - 1-1))"
using True by (intro mult_left_mono mult_mono power_mono) auto
also have "... = ?R"
using card_B_gt_0 by auto
finally show "?L ≤ ?R" by simp
next
case False
hence "?b = 1" using card_B_ge_1 by simp
thus "?L ≤ ?R"
by (cases "card R =0") auto
qed
finally show "measure_pmf.variance Ω Y ≤ card R * (real (card R) - 1)/ card B"
by simp
qed
definition "lim_balls_and_bins k p = (
prob_space.k_wise_indep_vars (measure_pmf p) k (λ_. discrete) (λx ω. ω x) R ∧
(∀x. x ∈ R ⟶ map_pmf (λω. ω x) p = pmf_of_set B))"
lemma indep:
assumes "lim_balls_and_bins k p"
shows "prob_space.k_wise_indep_vars (measure_pmf p) k (λ_. discrete) (λx ω. ω x) R"
using assms lim_balls_and_bins_def by simp
lemma ran:
assumes "lim_balls_and_bins k p" "x ∈ R"
shows "map_pmf (λω. ω x) p = pmf_of_set B"
using assms lim_balls_and_bins_def by simp
lemma Z_integrable:
fixes f :: "real ⇒ real"
assumes "lim_balls_and_bins k p"
shows "integrable p (λω. f (Z i ω) )"
unfolding Z_def using fin_R card_mono
by (intro integrable_pmf_iff_bounded[where C="Max (abs ` f ` real ` {..card R})"])
fastforce+
lemma Z_any_integrable_2:
fixes f :: "real ⇒ real"
assumes "lim_balls_and_bins k p"
shows "integrable p (λω. f (Z i ω + Z j ω))"
proof -
have q:"real (card A) + real (card B) ∈ real ` {..2 * card R}" if "A ⊆ R" "B ⊆ R" for A B
proof -
have "card A + card B ≤ card R + card R"
by (intro add_mono card_mono fin_R that)
also have "... = 2 * card R" by simp
finally show ?thesis by force
qed
thus ?thesis
unfolding Z_def using fin_R card_mono abs_triangle_ineq
by (intro integrable_pmf_iff_bounded[where C="Max (abs ` f ` real ` {..2*card R})"] Max_ge
finite_imageI imageI) auto
qed
lemma hit_count_prod_exp:
assumes "j1 ∈ B" "j2 ∈ B" "s+t ≤ k"
assumes "lim_balls_and_bins k p"
defines "L ≡ {(xs,ys). set xs ⊆ R ∧ set ys ⊆ R ∧
(set xs ∩ set ys = {} ∨ j1 = j2) ∧ length xs = s ∧ length ys = t}"
shows "(∫ω. Z j1 ω^s * Z j2 ω^t ∂p) =
(∑(xs,ys) ∈ L. (1/real (card B))^(card (set xs ∪ set ys)))"
(is "?L = ?R")
proof -
define W1 :: "'a ⇒ ('a ⇒ 'b) ⇒ real"
where "W1 = (λi ω. of_bool (ω i = j1) :: real)"
define W2 :: "'a ⇒ ('a ⇒ 'b) ⇒ real"
where "W2 = (λi ω. of_bool (ω i = j2) :: real)"
define τ :: "'a list × 'a list ⇒ 'a ⇒ 'b"
where "τ = (λl x. if x ∈ set (fst l) then j1 else j2)"
have τ_check_1: "τ l x = j1" if "x ∈ set (fst l)" and "l ∈ L" for x l
using that unfolding τ_def L_def by auto
have τ_check_2: "τ l x = j2" if "x ∈ set (snd l)" and "l ∈ L" for x l
using that unfolding τ_def L_def by auto
have τ_check_3: "τ l x ∈ B" for x l
using assms(1,2) unfolding τ_def by simp
have Z1_eq: "Z j1 ω = (∑i ∈ R. W1 i ω)" for ω
using fin_R unfolding Z_def W1_def
by (simp add:of_bool_def sum.If_cases Int_def)
have Z2_eq: "Z j2 ω = (∑i ∈ R. W2 i ω)" for ω
using fin_R unfolding Z_def W2_def
by (simp add:of_bool_def sum.If_cases Int_def)
define α where "α = 1 / real (card B)"
have a: "(∫ω. (∏x←a. W1 x ω) * (∏y←b. W2 y ω) ∂p) = 0" (is "?L1 = 0")
if "x ∈ set a ∩ set b" "j1 ≠ j2" "length a = s" "length b = t" for x a b
proof -
have "(∏x←a. W1 x ω) * (∏y←b. W2 y ω) = 0" for ω
proof -
have "W1 x ω = 0 ∨ W2 x ω = 0"
unfolding W1_def W2_def using that by simp
hence "(∏x←a. W1 x ω) = 0 ∨ (∏y←b. W2 y ω) = 0"
unfolding prod_list_zero_iff using that(1) by auto
thus ?thesis by simp
qed
hence "?L1 = (∫ω. 0 ∂p)"
by (intro arg_cong2[where f="measure_pmf.expectation"]) auto
also have "... = 0"
by simp
finally show ?thesis by simp
qed
have b: "prob_space.indep_vars p (λ_. discrete) (λi ω. ω i) (set (fst x) ∪ set (snd x))"
if "x ∈ L" for x
proof -
have "card (set (fst x) ∪ set (snd x)) ≤ card (set (fst x)) + card (set (snd x))"
by (intro card_Un_le)
also have "... ≤ length (fst x) + length (snd x)"
by (intro add_mono card_length)
also have "... = s + t"
using that L_def by auto
also have "... ≤ k" using assms(3) by simp
finally have "card (set (fst x) ∪ set (snd x)) ≤ k" by simp
moreover have "set (fst x) ∪ set (snd x) ⊆ R"
using that L_def by auto
ultimately show ?thesis
by (intro prob_space.k_wise_indep_vars_subset[OF prob_space_measure_pmf indep[OF assms(4)]])
auto
qed
have c: "(∫ω. of_bool (ω x = z) ∂p) = α" (is "?L1 = _")
if "z ∈ B" "x ∈ R" for x z
proof -
have "?L1 = (∫ω. indicator {ω. ω x = z} ω ∂p)"
unfolding indicator_def by simp
also have "... = measure p {ω. ω x = z}"
by simp
also have "... = measure (map_pmf (λω. ω x) p) {z}"
by (subst measure_map_pmf) (simp add:vimage_def)
also have "... = measure (pmf_of_set B) {z}"
using that by (subst ran[OF assms(4)]) auto
also have "... = 1/card B"
using fin_B that by (subst measure_pmf_of_set) auto
also have "... = α"
unfolding α_def by simp
finally show ?thesis by simp
qed
have d: "abs x ≤ 1 ⟹ abs y ≤ 1 ⟹ abs (x*y) ≤ 1" for x y :: real
by (simp add:abs_mult mult_le_one)
have e:"(⋀x. x ∈ set xs ⟹ abs x ≤1) ⟹ abs(prod_list xs) ≤ 1 " for xs :: "real list"
using d by (induction xs, simp, simp)
have "?L = (∫ω. (∑j ∈ R. W1 j ω)^s * (∑j ∈ R. W2 j ω)^t ∂p)"
unfolding Z1_eq Z2_eq by simp
also have "... = (∫ω. (∑xs | set xs ⊆ R ∧ length xs = s. (∏x ← xs. W1 x ω)) *
(∑ys | set ys ⊆ R ∧ length ys = t. (∏y ← ys. W2 y ω)) ∂p)"
unfolding sum_power_distrib[OF fin_R] by simp
also have "... = (∫ω.
(∑l∈{xs. set xs ⊆ R ∧ length xs = s} × {ys. set ys ⊆ R ∧ length ys = t}.
(∏x←fst l. W1 x ω) * (∏y←snd l. W2 y ω)) ∂p)"
by (intro arg_cong[where f="integral⇧L p"])
(simp add: sum_product sum.cartesian_product case_prod_beta)
also have "... = (∑l∈{xs. set xs ⊆ R ∧ length xs = s} × {ys. set ys ⊆ R ∧ length ys = t}.
(∫ω. (∏x←fst l. W1 x ω) * (∏y←snd l. W2 y ω) ∂p))"
unfolding W1_def W2_def
by (intro integral_sum integrable_pmf_iff_bounded[where C="1"] d e) auto
also have "... = (∑l∈ L. (∫ω. (∏x←fst l. W1 x ω) * (∏y←snd l. W2 y ω) ∂p))"
unfolding L_def using a by (intro sum.mono_neutral_right finite_cartesian_product
finite_lists_length_eq fin_R) auto
also have "... = (∑l∈ L. (∫ω. (∏x←fst l.
of_bool(ω x = τ l x)) * (∏y←snd l. of_bool(ω y = τ l y)) ∂p))"
unfolding W1_def W2_def using τ_check_1 τ_check_2
by (intro sum.cong arg_cong[where f="integral⇧L p"] ext arg_cong2[where f="(*)"]
arg_cong[where f="prod_list"]) auto
also have "... = (∑l∈ L. (∫ω. (∏x←(fst l@snd l). of_bool(ω x = τ l x))∂ p))"
by simp
also have "... = (∑l∈ L. (∫ω. (∏x ∈ set (fst l@snd l).
of_bool(ω x = τ l x)^count_list (fst l@snd l) x) ∂ p))"
unfolding prod_list_eval by simp
also have "... = (∑l∈ L. (∫ω. (∏x ∈ set (fst l) ∪ set (snd l).
of_bool(ω x = τ l x)^count_list (fst l@snd l) x) ∂ p))"
by simp
also have "... = (∑l∈ L. (∫ω. (∏x ∈ set (fst l) ∪ set (snd l). of_bool(ω x = τ l x)) ∂ p))"
using count_list_gr_1
by (intro sum.cong arg_cong[where f="integral⇧L p"] ext prod.cong) force+
also have "... = (∑l∈ L. (∏x ∈ set (fst l) ∪ set (snd l). (∫ω. of_bool(ω x = τ l x) ∂ p)))"
by (intro sum.cong prob_space.indep_vars_lebesgue_integral[OF prob_space_measure_pmf]
integrable_pmf_iff_bounded[where C="1"]
prob_space.indep_vars_compose2[OF prob_space_measure_pmf b]) auto
also have "... = (∑l∈ L. (∏x ∈ set (fst l) ∪ set (snd l). α))"
using τ_check_3 unfolding L_def by (intro sum.cong prod.cong c) auto
also have "... = (∑l ∈ L. α^(card (set (fst l) ∪ set (snd l))))"
by simp
also have "... = ?R"
unfolding L_def α_def by (simp add:case_prod_beta)
finally show ?thesis by simp
qed
lemma hit_count_prod_pow_eq:
assumes "i ∈ B" "j ∈ B"
assumes "lim_balls_and_bins k p"
assumes "lim_balls_and_bins k q"
assumes "s+t ≤ k"
shows "(∫ω. (Z i ω)^s * (Z j ω)^t ∂p) = (∫ω. (Z i ω)^s * (Z j ω)^t ∂q)"
unfolding hit_count_prod_exp[OF assms(1,2,5,3)]
unfolding hit_count_prod_exp[OF assms(1,2,5,4)]
by simp
lemma hit_count_sum_pow_eq:
assumes "i ∈ B" "j ∈ B"
assumes "lim_balls_and_bins k p"
assumes "lim_balls_and_bins k q"
assumes "s ≤ k"
shows "(∫ω. (Z i ω + Z j ω)^s ∂p) = (∫ω. (Z i ω + Z j ω)^s ∂q)"
(is "?L = ?R")
proof -
have q2: "¦Z i x ^ l * Z j x ^ (s - l)¦ ≤ real (card R ^ s)"
if "l ∈ {..s}" for s i j l x
proof -
have "¦Z i x ^ l * Z j x ^ (s - l)¦ ≤ Z i x ^ l * Z j x ^ (s - l)"
unfolding Z_def by auto
also have "... ≤ real (card R) ^ l * real (card R) ^ (s-l)"
unfolding Z_def
by (intro mult_mono power_mono of_nat_mono card_mono fin_R) auto
also have "... = real (card R)^s" using that
by (subst power_add[symmetric]) simp
also have "... = real (card R^s)"
by simp
finally show ?thesis by simp
qed
have "?L = (∫ω. (∑l≤s. real (s choose l) * (Z i ω^l * Z j ω^(s-l))) ∂p)"
by (subst binomial_ring) (simp add:algebra_simps)
also have "... = (∑l≤s. (∫ω. real (s choose l) * (Z i ω^l * Z j ω^(s-l)) ∂p))"
by (intro integral_sum integrable_mult_right
integrable_pmf_iff_bounded[where C="card R^s"] q2) auto
also have "... = (∑l≤s. real (s choose l) * (∫ω. (Z i ω^l * Z j ω^(s-l)) ∂p))"
by (intro sum.cong integral_mult_right
integrable_pmf_iff_bounded[where C="card R^s"] q2) auto
also have "... = (∑l≤s. real (s choose l) * (∫ω. (Z i ω^l * Z j ω^(s-l)) ∂q))"
using assms(5)
by (intro_cong "[σ⇩2 (*)]" more: sum.cong hit_count_prod_pow_eq[OF assms(1-4)])
auto
also have "... = (∑l≤s. (∫ω. real (s choose l) * (Z i ω^l * Z j ω^(s-l)) ∂q))"
by (intro sum.cong integral_mult_right[symmetric]
integrable_pmf_iff_bounded[where C="card R^s"] q2) auto
also have "... = (∫ω. (∑l≤s. real (s choose l) * (Z i ω^l * Z j ω^(s-l))) ∂q)"
by (intro integral_sum[symmetric] integrable_mult_right
integrable_pmf_iff_bounded[where C="card R^s"] q2) auto
also have "... = ?R"
by (subst binomial_ring) (simp add:algebra_simps)
finally show ?thesis by simp
qed
lemma hit_count_sum_poly_eq:
assumes "i ∈ B" "j ∈ B"
assumes "lim_balls_and_bins k p"
assumes "lim_balls_and_bins k q"
assumes "f ∈ ℙ k"
shows "(∫ω. f (Z i ω + Z j ω) ∂p) = (∫ω. f (Z i ω + Z j ω) ∂q)"
(is "?L = ?R")
proof -
obtain fp where f_def: "f = poly fp" "degree fp ≤ k"
using assms(5) unfolding Polynomials_def by auto
have "?L = (∑d≤degree fp. (∫ω. poly.coeff fp d * (Z i ω + Z j ω) ^ d ∂p))"
unfolding f_def poly_altdef
by (intro integral_sum integrable_mult_right Z_any_integrable_2[OF assms(3)])
also have "... = (∑d≤degree fp. poly.coeff fp d * (∫ω. (Z i ω + Z j ω) ^ d ∂p))"
by (intro sum.cong integral_mult_right Z_any_integrable_2[OF assms(3)])
simp
also have "... = (∑d≤degree fp. poly.coeff fp d *(∫ω. (Z i ω + Z j ω) ^ d ∂q))"
using f_def
by (intro sum.cong arg_cong2[where f="(*)"] hit_count_sum_pow_eq[OF assms(1-4)]) auto
also have "... = (∑d≤degree fp. (∫ω. poly.coeff fp d * (Z i ω + Z j ω) ^ d ∂q))"
by (intro sum.cong) auto
also have "... = ?R"
unfolding f_def poly_altdef by (intro integral_sum[symmetric]
integrable_mult_right Z_any_integrable_2[OF assms(4)])
finally show ?thesis by simp
qed
lemma hit_count_poly_eq:
assumes "b ∈ B"
assumes "lim_balls_and_bins k p"
assumes "lim_balls_and_bins k q"
assumes "f ∈ ℙ k"
shows "(∫ω. f (Z b ω) ∂p) = (∫ω. f (Z b ω) ∂q)" (is "?L = ?R")
proof -
have a:"(λa. f (a / 2)) ∈ ℙ (k*1)"
by (intro Polynomials_composeI[OF assms(4)] Polynomials_intros)
have "?L = ∫ω. f ((Z b ω + Z b ω)/2) ∂p"
by simp
also have "... = ∫ω. f ((Z b ω + Z b ω)/2) ∂q"
using a by (intro hit_count_sum_poly_eq[OF assms(1,1,2,3)]) simp
also have "... = ?R" by simp
finally show ?thesis by simp
qed
lemma lim_balls_and_bins_from_ind_balls_and_bins:
"lim_balls_and_bins k Ω"
proof -
have "prob_space.indep_vars (measure_pmf Ω) (λ_. discrete) (λx ω. ω x) R"
unfolding Ω_def using indep_vars_Pi_pmf[OF fin_R] by metis
hence "prob_space.indep_vars (measure_pmf Ω) (λ_. discrete) (λx ω. ω x) J" if "J ⊆ R" for J
using prob_space.indep_vars_subset[OF prob_space_measure_pmf _ that] by auto
hence a:"prob_space.k_wise_indep_vars (measure_pmf Ω) k (λ_. discrete) (λx ω. ω x) R"
by (simp add:prob_space.k_wise_indep_vars_def[OF prob_space_measure_pmf])
have b: "map_pmf (λω. ω x) Ω = pmf_of_set B" if "x ∈ R" for x
using that unfolding Ω_def Pi_pmf_component[OF fin_R] by simp
show ?thesis
using a b fin_R fin_B unfolding lim_balls_and_bins_def by auto
qed
lemma hit_count_factorial_moments:
assumes a:"j ∈ B"
assumes "s ≤ k"
assumes "lim_balls_and_bins k p"
shows "(∫ω. ffact s (Z j ω) ∂p) = ffact s (real (card R)) * (1 / real (card B))^s"
(is "?L = ?R")
proof -
have "(λx. ffact s (x-0::real)) ∈ ℙ s"
by (intro Polynomials_intros)
hence b: "ffact s ∈ (ℙ k :: (real ⇒ real) set)"
using Polynomials_mono[OF assms(2)] by auto
have "?L = (∫ω. ffact s (Z j ω) ∂Ω)"
by (intro hit_count_poly_eq[OF a assms(3) lim_balls_and_bins_from_ind_balls_and_bins] b)
also have "... = (∫ω. ffact s (∑i ∈ {j}. Z i ω) ∂Ω)"
by simp
also have "... = ffact s (real (card R)) * (real (card {j}) / real (card B)) ^ s "
using assms(1)
by (intro fact_moment_balls_and_bins fin_R fin_B) auto
also have "... = ?R"
by simp
finally show ?thesis by simp
qed
lemma hit_count_factorial_moments_2:
assumes a:"i ∈ B" "j ∈ B"
assumes "i ≠ j" "s ≤ k" "card R ≤ card B"
assumes "lim_balls_and_bins k p"
shows "(∫ω. ffact s (Z i ω + Z j ω) ∂p) ≤ 2^s"
(is "?L ≤ ?R")
proof -
have "(λx. ffact s (x-0::real)) ∈ ℙ s"
by (intro Polynomials_intros)
hence b: "ffact s ∈ (ℙ k :: (real ⇒ real) set)"
using Polynomials_mono[OF assms(4)] by auto
have or_distrib: "(a ∧ b) ∨ (a ∧ c) ⟷ a ∧ (b ∨ c)" for a b c
by auto
have "?L = (∫ω. ffact s (Z i ω + Z j ω) ∂Ω)"
by (intro hit_count_sum_poly_eq[OF a assms(6) lim_balls_and_bins_from_ind_balls_and_bins] b)
also have "... = (∫ω. ffact s ((∑t ∈ {i,j}. Z t ω)) ∂Ω)"
using assms(3) by simp
also have "... = ffact s (real (card R)) * (real (card {i,j}) / real (card B)) ^ s "
using assms(1,2)
by (intro fact_moment_balls_and_bins fin_R fin_B) auto
also have "... = real (ffact s (card R)) * (real (card {i,j}) / real (card B)) ^ s "
by (simp add:of_nat_ffact)
also have "... ≤ (card R)^s * (real (card {i,j}) / real (card B)) ^ s "
by (intro mult_mono of_nat_mono ffact_bound, simp_all)
also have "... ≤ (card B)^s * (real (2) / real (card B)) ^ s "
using assms(3)
by (intro mult_mono of_nat_mono power_mono assms(5), simp_all)
also have "... = ?R"
using card_B_gt_0 by (simp add:divide_simps)
finally show ?thesis by simp
qed
lemma balls_and_bins_approx_helper:
fixes x :: real
assumes "x ≥ 2"
assumes "real k ≥ 5*x / ln x"
shows "k ≥ 2"
and "2^(k+3) / fact k ≤ (1/exp x)^2"
and "2 / fact k ≤ 1 / (exp 1 * exp x)"
proof -
have ln_inv: "ln x = - ln (1/ x)" if "x > 0" for x :: real
using that by (subst ln_div, auto)
have apx:
"exp 1 ≤ (5::real)"
"4 * ln 4 ≤ (2 - 2*exp 1/5)*ln (450::real)"
"ln 8 * 2 ≤ (450::real)"
"4 / 5 * 2 * exp 1 + ln (5 / 4) * exp 1 ≤ (5::real)"
"exp 1 ≤ (2::real)^4"
by (approximation 10)+
have "2 ≤ 5 * (x / (x-1))"
using assms(1) by (simp add:divide_simps)
also have "... ≤ 5 * (x / ln x)"
using assms(1)
by (intro mult_left_mono divide_left_mono ln_le_minus_one mult_pos_pos) auto
also have "... ≤ k" using assms(2) by simp
finally show k_ge_2: "k ≥ 2" by simp
have "ln x * (2 * exp 1) = ln (((4/5) * x)*(5/4)) * (2 * exp 1)"
by simp
also have "... = ln ((4/5) * x) * (2 * exp 1) + ln((5/4))*(2 * exp 1)"
using assms(1) by (subst ln_mult, simp_all add:algebra_simps)
also have "... < (4/5)* x * (2 * exp 1) + ln (5/4) * (x * exp 1)"
using assms(1) by (intro add_less_le_mono mult_strict_right_mono ln_less_self
mult_left_mono mult_right_mono) (auto simp add:algebra_simps)
also have "... = ((4/5) * 2 * exp 1 + ln(5/4) * exp 1) * x"
by (simp add:algebra_simps)
also have "... ≤ 5 * x"
using assms(1) apx(4) by (intro mult_right_mono, simp_all)
finally have 1: "ln x * (2 * exp 1) ≤ 5 * x" by simp
have "ln 8 ≤ 3 * x - 5 * x * ln(2*exp 1 /5 * ln x) / ln x"
proof (cases "x ∈ {2..450}")
case True
then show ?thesis by (approximation 10 splitting: x=10)
next
case False
hence x_ge_450: "x ≥ 450" using assms(1) by simp
have "4 * ln 4 ≤ (2 - 2*exp 1/5)*ln (450::real)"
using apx(2) by (simp)
also have "... ≤ (2 - 2*exp 1/5)* ln x"
using x_ge_450 apx(1)
by (intro mult_left_mono iffD2[OF ln_le_cancel_iff], simp_all)
finally have "(2 - 2*exp 1/5) * ln x ≥ 4 * ln 4" by simp
hence "2*exp 1/5 * ln x + 0 ≤ 2 * exp 1 / 5 * ln x + ((2 - 2*exp 1/5) * ln x - 4 * ln 4)"
by (intro add_mono) auto
also have "... = 4 * (1/2) * ln x - 4 * ln 4"
by (simp add:algebra_simps)
also have "... = 4 * (ln (x powr (1/2)) - ln 4)"
using x_ge_450 by (subst ln_powr, auto)
also have "... = 4 * (ln (x powr (1/2)/4))"
using x_ge_450 by (subst ln_div) auto
also have "... < 4 * (x powr (1/2)/4)"
using x_ge_450 by (intro mult_strict_left_mono ln_less_self) auto
also have "... = x powr (1/2)" by simp
finally have §: "2 * exp 1/ 5 * ln x ≤ x powr (1/2)" by simp
hence "ln(2* exp 1/ 5 * ln x) ≤ ln (x powr (1/2))"
using x_ge_450 by (intro ln_mono; simp)
hence 0:"ln(2* exp 1/ 5 * ln x) / ln x ≤ 1/2"
using x_ge_450 by (subst (asm) ln_powr, auto)
have "ln 8 ≤ 3 * x - 5 * x * (1/2)"
using x_ge_450 apx(3) by simp
also have "... ≤ 3 * x - 5 * x * (ln(2* exp 1/ 5 * ln x) / ln x)"
using x_ge_450 by (intro diff_left_mono mult_left_mono 0) auto
finally show ?thesis by simp
qed
hence "2 * x + ln 8 ≤ 2 * x + (3 * x - 5 * x * ln(2*exp 1 /5 * ln x) / ln x)"
by (intro add_mono, auto)
also have "... = 5 * x + 5 * x * ln(5 / (2*exp 1*ln x)) / ln x"
using assms(1) by (subst ln_inv) (auto simp add:algebra_simps)
also have "... = 5 * x * (ln x + ln(5 / (2*exp 1*ln x))) / ln x"
using assms(1) by (simp add:algebra_simps add_divide_distrib)
also have "... = 5 * x * (ln (5 * x / (2 * exp 1 * ln x))) / ln x"
using assms(1) by (simp add: ln_mult ln_div)
also have "... = (5 * x / ln x) * ln ((5 * x / ln x) / (2 * exp 1))"
by (simp add:algebra_simps)
also have "... ≤ k * ln (k / (2*exp 1))"
using assms(1,2) 1 k_ge_2
by (intro mult_mono iffD2[OF ln_le_cancel_iff] divide_right_mono)
auto
finally have "k * ln (k/(2*exp 1)) ≥ 2*x + ln 8" by simp
hence "k * ln(2*exp 1/k) ≤ -2*x - ln 8"
using k_ge_2 by (subst ln_inv, auto)
hence "ln ((2*exp 1/k) powr k) ≤ ln(exp(-2*x)) - ln 8"
using k_ge_2 by (subst ln_powr, auto)
also have "... = ln(exp(-2*x)/8)"
by (simp add:ln_div)
finally have "ln ((2*exp 1/k) powr k) ≤ ln (exp(-2*x)/8)" by simp
hence 1: "(2*exp 1/k) powr k ≤ exp(-2*x)/8"
using k_ge_2 assms(1) by (subst (asm) ln_le_cancel_iff) auto
have "2^(k+3)/fact k ≤ 2^(k+3)/(k / exp 1)^k"
using k_ge_2 by (intro divide_left_mono fact_lower_bound_1) auto
also have "... = 8 * 2^k * (exp 1 / k)^k"
by (simp add:power_add algebra_simps power_divide)
also have "... = 8 * (2*exp 1/k) powr k"
using k_ge_2 powr_realpow
by (simp add:power_mult_distrib[symmetric])
also have "... ≤ 8 * (exp(-2*x)/8)"
by (intro mult_left_mono 1) auto
also have "... = exp((-x)*2)"
by simp
also have "... = exp(-x)^2"
by (subst exp_powr[symmetric], simp)
also have "... = (1/exp x)^2"
by (simp add: exp_minus inverse_eq_divide)
finally show 2:"2^(k+3)/fact k ≤ (1/exp x)^2" by simp
have "(2::real)/fact k = (2^(k+3)/fact k)/(2^(k+2))"
by (simp add:divide_simps power_add)
also have "... ≤ (1/exp x)^2/(2^(k+2))"
by (intro divide_right_mono 2, simp)
also have "... ≤ (1/exp x)^1/(2^(k+2))"
using assms(1) by (intro divide_right_mono power_decreasing) auto
also have "... ≤ (1/exp x)^1/(2^4)"
using k_ge_2 by (intro divide_left_mono power_increasing) auto
also have "... ≤ (1/exp x)^1/exp(1)"
using k_ge_2 apx(5) by (intro divide_left_mono) auto
also have "... = 1/(exp 1 * exp x)" by simp
finally show "(2::real)/fact k ≤ 1/(exp 1 * exp x)" by simp
qed
text ‹Bounds on the expectation and variance in the k-wise independent case. Here the indepedence
assumption is improved by a factor of two compared to the result in the paper.›
lemma
assumes "card R ≤ card B"
assumes "⋀c. lim_balls_and_bins (k+1) (p c)"
assumes "ε ∈ {0<..1/exp(2)}"
assumes "k ≥ 5 * ln (card B / ε) / ln (ln (card B / ε))"
shows
exp_approx: "¦measure_pmf.expectation (p True) Y - measure_pmf.expectation (p False) Y¦ ≤
ε * real (card R)" (is "?A") and
var_approx: "¦measure_pmf.variance (p True) Y - measure_pmf.variance (p False) Y¦ ≤ ε⇧2"
(is "?B")
proof -
let ?p1 = "p False"
let ?p2 = "p True"
have "exp (2::real) = 1/ (1/exp 2)" by simp
also have "... ≤ 1/ ε"
using assms(3) by (intro divide_left_mono) auto
also have "... ≤ real (card B)/ ε"
using assms(3) card_B_gt_0 by (intro divide_right_mono) auto
finally have "exp 2 ≤ real (card B) / ε" by simp
hence k_condition_h: "2 ≤ ln (card B / ε)"
using assms(3) card_B_gt_0 by (subst ln_ge_iff) auto
have k_condition_h_2: "0 < real (card B) / ε"
using assms(3) card_B_gt_0 by (intro divide_pos_pos) auto
note k_condition = balls_and_bins_approx_helper[OF k_condition_h assms(4)]
define φ :: "real ⇒ real" where "φ = (λx. min x 1)"
define f where "f = (λx. 1 - (-1)^k / real (fact k) * ffact k (x-1))"
define g where "g = (λx. φ x - f x)"
have φ_exp: "φ x = f x + g x" for x
unfolding g_def by simp
have k_ge_2: "k ≥ 2"
using k_condition(1) by simp
define γ where "γ = 1 / real (fact k)"
have γ_nonneg: "γ ≥ 0"
unfolding γ_def by simp
have k_le_k_plus_1: "k ≤ k+1"
by simp
have "f ∈ ℙ k"
unfolding f_def by (intro Polynomials_intros)
hence f_poly: "f ∈ ℙ (k+1)"
using Polynomials_mono[OF k_le_k_plus_1] by auto
have g_diff: "¦g x - g (x-1)¦ = ffact (k-1) (x-2) / fact (k-1)"
if "x ≥ k" for x :: real
proof -
have "x ≥ 2" using k_ge_2 that by simp
hence "φ x = φ (x- 1)"
unfolding φ_def by simp
hence "¦g x - g (x-1)¦ = ¦f (x-1) - f x¦"
unfolding g_def by (simp add:algebra_simps)
also have "... = ¦(-1)^k / real (fact k) * (ffact k (x-2) - ffact k (x-1))¦"
unfolding f_def by (simp add:algebra_simps)
also have "... = 1 / real (fact k) * ¦ffact k (x-1) - ffact k ((x-1)-1)¦"
by (simp add:abs_mult)
also have "... = 1 / real (fact k) * real k * ¦ffact (k-1) (x-2)¦"
by (subst ffact_suc_diff, simp add:abs_mult)
also have "... = ¦ffact (k-1) (x-2)¦ / fact (k-1)"
using k_ge_2 by (subst fact_reduce) auto
also have "... = ffact (k-1) (x-2) / fact (k-1)"
unfolding ffact_eq_fact_mult_binomial using that k_ge_2
by (intro arg_cong2[where f="(/)"] abs_of_nonneg ffact_nonneg) auto
finally show ?thesis by simp
qed
have f_approx_φ: "f x = φ x" if f_approx_φ_1: "x ∈ real ` {0..k}" for x
proof (cases "x = 0")
case True
hence "f x = 1 - (-1)^k / real (fact k) * (∏i = 0..<k. - (real i+1))"
unfolding f_def prod_ffact[symmetric] by (simp add:algebra_simps)
also have "... = 1 - (-1)^k / real (fact k) * ((∏i = 0..<k. (- 1)::real) * (∏i = 0..<k. real i+1))"
by (subst prod.distrib[symmetric]) simp
also have "... = 1 - (-1)^k / real (fact k) * ((-1)^k * (∏i ∈ (λx. x + 1) ` {0..<k}. real i))"
by (subst prod.reindex, auto simp add:inj_on_def comp_def algebra_simps)
also have "... = 1 - (-1)^k / real (fact k) * ((-1)^k * (∏i ∈ {1..k}. real i))"
by (intro arg_cong2[where f="(-)"] arg_cong2[where f="(*)"] prod.cong refl) auto
also have "... = 0"
unfolding fact_prod by simp
also have "... = φ x"
using True φ_def by simp
finally show ?thesis by simp
next
case False
hence a: " x ≥ 1" using that by auto
obtain x' where x'_def: "x' ∈ {0..k}" "x = real x'"
using f_approx_φ_1 by auto
hence "x' - 1 ∈ {0..<k}" using k_ge_2 by simp
moreover have "x- real 1 = real (x'-1)"
using False x'_def(2) by simp
ultimately have b: "x - 1 = real (x' - 1)" "x' - 1 < k"
by auto
have "f x = 1 - (- 1) ^ k / real (fact k) * real (ffact k (x' - 1))"
unfolding f_def b of_nat_ffact by simp
also have "... = 1"
using b by (subst ffact_nat_triv, auto)
also have "... = φ x"
unfolding φ_def using a by auto
finally show ?thesis by simp
qed
have q2: "¦Z i x ^ l * Z j x ^ (s - l)¦ ≤ real (card R ^ s)"
if "l ∈ {..s}" for s i j l x
proof -
have "¦Z i x ^ l * Z j x ^ (s - l)¦ ≤ Z i x ^ l * Z j x ^ (s - l)"
unfolding Z_def by auto
also have "... ≤ real (card R) ^ l * real (card R) ^ (s-l)"
unfolding Z_def
by (intro mult_mono power_mono of_nat_mono card_mono fin_R) auto
also have "... = real (card R)^s" using that
by (subst power_add[symmetric]) simp
also have "... = real (card R^s)"
by simp
finally show ?thesis by simp
qed
have q:"real (card A) + real (card B) ∈ real ` {..2 * card R}" if "A ⊆ R" "B ⊆ R" for A B
proof -
have "card A + card B ≤ card R + card R"
by (intro add_mono card_mono fin_R that)
also have "... = 2 * card R" by simp
finally show ?thesis by force
qed
have g_eq_0_iff_2: "abs (g x) * y = 0" if "x ∈ ℤ" "x ≥ 0" "x ≤ k" for x y :: real
proof -
have "∃x'. x = real_of_int x' ∧ x' ≤ k ∧ x' ≥ 0"
using that Ints_def by fastforce
hence "∃x'. x = real x' ∧ x' ≤ k"
by (metis nat_le_iff of_nat_nat)
hence "x ∈ real ` {0..k}"
by auto
hence "g x = 0"
unfolding g_def using f_approx_φ by simp
thus ?thesis by simp
qed
have g_bound_abs: "¦∫ω. g (f ω) ∂p¦ ≤ (∫ω. ffact (k+1) (f ω) ∂p) * γ"
(is "?L ≤ ?R")
if "range f ⊆ real ` {..m}" for m and p :: "('a ⇒ 'b) pmf" and f :: "('a ⇒ 'b) ⇒ real"
proof -
have f_any_integrable:
"integrable p (λω. h (f ω))" for h :: "real ⇒ real"
using that
by (intro integrable_pmf_iff_bounded[where C="Max (abs ` h` real ` {..m})"]
Max_ge finite_imageI imageI) auto
have f_val: "f ω ∈ real ` {..m}" for ω using that by auto
hence f_nat: "f ω ∈ ℕ" for ω
unfolding Nats_def by auto
have f_int: "f ω ≥ real y + 1" if "f ω > real y" for y ω
proof -
obtain x where x_def: "f ω = real x" "x ≤ m" using f_val by auto
hence "y < x" using that by simp
hence "y + 1 ≤ x" by simp
then show ?thesis using x_def by simp
qed
have f_nonneg: "f ω ≥ 0" for ω
proof -
obtain x where x_def: "f ω = real x" "x ≤ m" using f_val by auto
hence "x ≥ 0" by simp
then show ?thesis using x_def by simp
qed
have "¬(real x ≤ f ω)" if "x > m" for x ω
proof -
obtain x where x_def: "f ω = real x" "x ≤ m" using f_val by auto
then show ?thesis using x_def that by simp
qed
hence max_Z1: "measure p {ω. real x ≤ f ω} = 0" if "x > m" for x
using that by auto
have "?L ≤ (∫ω. ¦g (f ω)¦ ∂p)"
by (intro integral_abs_bound)
also have "... = (∑y∈real ` {..m}. ¦g y¦ * measure p {ω. f ω = y})"
using that by (intro pmf_exp_of_fin_function) auto
also have "... = (∑y∈{..m}. ¦g (real y)¦ * measure p {ω. f ω = real y})"
by (subst sum.reindex) (auto simp add:comp_def)
also have "... = (∑y∈{..m}. ¦g (real y)¦ *
(measure p ({ω. f ω = real y} ∪ {ω. f ω > y}) - measure p {ω. f ω > y}))"
by (subst measure_Union) auto
also have "... = (∑y∈{..m}. ¦g (real y)¦ * (measure p {ω. f ω ≥ y} - measure p {ω. f ω > y}))"
by (intro sum.cong arg_cong2[where f="(*)"] arg_cong2[where f="(-)"]
arg_cong[where f="measure p"]) auto
also have "... = (∑y∈{..m}. ¦g (real y)¦ * measure p {ω. f ω ≥ y}) -
(∑y∈{..m}. ¦g (real y)¦ * measure p {ω. f ω > y})"
by (simp add:algebra_simps sum_subtractf)
also have "... = (∑y∈{..m}. ¦g (real y)¦ * measure p {ω. f ω ≥ y}) -
(∑y∈{..m}. ¦g (real y)¦ * measure p {ω. f ω ≥ real (y+1)})"
using f_int
by (intro sum.cong arg_cong2[where f="(-)"] arg_cong2[where f="(*)"]
arg_cong[where f="measure p"]) fastforce+
also have "... = (∑y∈{..m}. ¦g (real y) ¦ * measure p {ω. f ω ≥ real y}) -
(∑y∈Suc ` {..m}. ¦g (real y - 1)¦ * measure p {ω. f ω ≥ real y})"
by (subst sum.reindex) (auto simp add:comp_def)
also have "... = (∑y∈{..m}. ¦g (real y) ¦ * measure p {ω. f ω ≥ real y}) -
(∑y∈{1..m}. ¦g (real y - 1)¦ * measure p {ω. f ω ≥ real y})"
using max_Z1 image_Suc_atMost
by (intro arg_cong2[where f="(-)"] sum.mono_neutral_cong) auto
also have "... = (∑y∈{k+1..m}. ¦g (real y) ¦ * measure p {ω. f ω ≥ y}) -
(∑y∈{k+1..m}. ¦g (real y - 1)¦ * measure p {ω. f ω ≥ y})"
using k_ge_2
by (intro arg_cong2[where f="(-)"] sum.mono_neutral_cong_right ballI g_eq_0_iff_2)
auto
also have "... = (∑y∈{k+1..m}. (¦g (real y)¦ - ¦g (real y-1)¦) * measure p {ω. f ω ≥ y})"
by (simp add:algebra_simps sum_subtractf)
also have "... ≤ (∑y∈{k+1..m}. ¦g (real y)- g (real y-1)¦ *
measure p {ω. ffact (k+1) (f ω) ≥ ffact (k+1) (real y)})"
using ffact_mono by (intro sum_mono mult_mono pmf_mono) auto
also have "... = (∑y∈{k+1..m}. (ffact (k-1) (real y-2) / fact (k-1)) *
measure p {ω. ffact (k+1) (f ω) ≥ ffact (k+1) (real y)})"
by (intro sum.cong, simp_all add: g_diff)
also have "... ≤ (∑y∈{k+1..m}. (ffact (k-1) (real y-2) / fact (k-1)) *
((∫ω. ffact (k+1) (f ω)∂p) / ffact (k+1) (real y)))"
using k_ge_2 f_nat
by (intro sum_mono mult_left_mono pmf_markov f_any_integrable
divide_nonneg_pos ffact_of_nat_nonneg ffact_pos) auto
also have "... = (∫ω. ffact (k+1) (f ω) ∂p) / fact (k-1) * (∑y∈{k+1..m}.
ffact (k-1) (real y - 2) / ffact (Suc (Suc (k-1))) (real y))"
using k_ge_2 by (simp add:algebra_simps sum_distrib_left)
also have "... = (∫ω. ffact (k+1) (f ω) ∂p) / fact (k-1) * (∑y∈{k+1..m}.
ffact (k-1) (real y - 2) / (real y * (real y - 1) * ffact (k-1) (real y - 2)))"
by (subst ffact_Suc, subst ffact_Suc, simp)
also have "... = (∫ω. ffact (k+1) (f ω) ∂p) / fact (k-1) *
(∑y∈{k+1..m}. 1 / (real y * (real y - 1)))"
using order.strict_implies_not_eq[OF ffact_pos] k_ge_2
by (intro arg_cong2[where f="(*)"] sum.cong) auto
also have "... = (∫ω. ffact (k+1) (f ω) ∂p) / fact (k-1) *
(∑y∈{Suc k..m}. 1 / (real y - 1) - 1/(real y))"
using k_ge_2 by (intro arg_cong2[where f="(*)"] sum.cong) (auto simp add: divide_simps)
also have "... = (∫ω. ffact (k+1) (f ω) ∂p) / fact (k-1) *
(∑y∈{Suc k..m}. (-1/(real y)) - (-1 / (real (y - 1))))"
using k_ge_2 by (intro arg_cong2[where f="(*)"] sum.cong) (auto)
also have "... = (∫ω. ffact (k+1) (f ω) ∂p) / fact (k-1) *
(of_bool (k ≤ m) * (1/real k-1/real m))"
by (subst sum_telescope_eq, auto)
also have "... ≤ (∫ω. ffact (k+1) (f ω) ∂p) / fact (k-1) * (1 / real k)"
using k_ge_2 f_nat
by (intro mult_left_mono divide_nonneg_nonneg integral_nonneg
ffact_of_nat_nonneg) auto
also have "... = ?R"
using k_ge_2 unfolding γ_def by (cases k) (auto simp add:algebra_simps)
finally show ?thesis by simp
qed
have z1_g_bound: "¦∫ω. g (Z i ω) ∂p c¦ ≤ (real (card R) / real (card B)) * γ"
(is "?L1 ≤ ?R1") if "i ∈ B" for i c
proof -
have "?L1 ≤ (∫ω. ffact (k+1) (Z i ω) ∂p c) * γ"
unfolding Z_def using fin_R
by (intro g_bound_abs[where m1="card R"]) (auto intro!:imageI card_mono)
also have "... = ffact (k+1) (real (card R)) * (1 / real (card B))^(k+1) * γ"
using that by (subst hit_count_factorial_moments[OF _ _ assms(2)], simp_all)
also have "... = real (ffact (k+1) (card R)) * (1 / real (card B))^(k+1) * γ"
by (simp add:of_nat_ffact)
also have "... ≤ real (card R^(k+1)) * (1 / real (card B))^(k+1) * γ"
using γ_nonneg
by (intro mult_right_mono of_nat_mono ffact_bound, simp_all)
also have "... ≤ (real (card R) / real (card B))^(k+1) * γ"
by (simp add:divide_simps)
also have "... ≤ (real (card R) / real (card B))^1 * γ"
using assms(1) card_B_gt_0 γ_nonneg by (intro mult_right_mono power_decreasing) auto
also have "... = ?R1" by simp
finally show ?thesis by simp
qed
have g_add_bound: "¦∫ω. g (Z i ω + Z j ω) ∂p c¦ ≤ 2^(k+1) * γ"
(is "?L1 ≤ ?R1") if ij_in_B: "i ∈ B" "j ∈ B" "i ≠ j" for i j c
proof -
have "?L1 ≤ (∫ω. ffact (k+1) (Z i ω + Z j ω) ∂p c) * γ"
unfolding Z_def using assms(1)
by (intro g_bound_abs[where m1="2*card R"]) (auto intro!:imageI q)
also have "... ≤ 2^(k+1) * γ"
by (intro γ_nonneg mult_right_mono hit_count_factorial_moments_2[OF that(1,2,3) _ assms(1,2)])
auto
finally show ?thesis by simp
qed
have Z_poly_diff:
"¦(∫ω. φ (Z i ω) ∂?p1) - (∫ω. φ (Z i ω) ∂?p2)¦ ≤ 2 * ((real (card R) / card B) * γ)"
(is "?L ≤ 2 * ?R") if "i ∈ B" for i
proof -
note Z_poly_eq =
hit_count_poly_eq[OF that assms(2)[of "True"] assms(2)[of "False"] f_poly]
have "?L = ¦(∫ω. f (Z i ω) ∂?p1) + (∫ω. g (Z i ω) ∂?p1) -
(∫ω. f (Z i ω) ∂?p2) - (∫ω. g (Z i ω) ∂?p2)¦"
using Z_integrable[OF assms(2)] unfolding φ_exp by simp
also have "... = ¦(∫ω. g (Z i ω) ∂?p1) + (- (∫ω. g (Z i ω) ∂?p2))¦"
by (subst Z_poly_eq) auto
also have "... ≤ ¦(∫ω. g (Z i ω) ∂?p1)¦ + ¦(∫ω. g (Z i ω) ∂?p2)¦"
by simp
also have "... ≤ ?R + ?R"
by (intro add_mono z1_g_bound that)
also have "... = 2 * ?R"
by (simp add:algebra_simps)
finally show ?thesis by simp
qed
have Z_poly_diff_2: "¦(∫ω. φ (Z i ω) ∂?p1) - (∫ω. φ (Z i ω) ∂?p2)¦ ≤ 2 * γ"
(is "?L ≤ ?R") if "i ∈ B" for i
proof -
have "?L ≤ 2 * ((real (card R) / real (card B)) * γ)"
by (intro Z_poly_diff that)
also have "... ≤ 2 * (1 * γ)"
using assms fin_B that γ_nonneg card_gt_0_iff
by (intro mult_mono that iffD2[OF pos_divide_le_eq]) auto
also have "... = ?R" by simp
finally show ?thesis by simp
qed
have Z_poly_diff_3: "¦(∫ω. φ (Z i ω + Z j ω) ∂?p2) - (∫ω. φ (Z i ω + Z j ω) ∂?p1)¦ ≤ 2^(k+2)*γ"
(is "?L ≤ ?R") if "i ∈ B" "j ∈ B" "i ≠ j" for i j
proof -
note Z_poly_eq_2 =
hit_count_sum_poly_eq[OF that(1,2) assms(2)[of "True"] assms(2)[of "False"] f_poly]
have "?L = ¦(∫ω. f (Z i ω + Z j ω) ∂?p2) + (∫ω. g (Z i ω + Z j ω) ∂?p2) -
(∫ω. f (Z i ω + Z j ω) ∂?p1) - (∫ω. g (Z i ω + Z j ω) ∂?p1)¦"
using Z_any_integrable_2[OF assms(2)] unfolding φ_exp by simp
also have "... = ¦(∫ω. g (Z i ω + Z j ω) ∂?p2) + (- (∫ω. g (Z i ω + Z j ω) ∂?p1))¦"
by (subst Z_poly_eq_2) auto
also have "... ≤ ¦(∫ω. g (Z i ω + Z j ω) ∂?p1)¦ + ¦(∫ω. g (Z i ω + Z j ω) ∂?p2)¦"
by simp
also have "... ≤ 2^(k+1)*γ + 2^(k+1)*γ"
by (intro add_mono g_add_bound that)
also have "... = ?R"
by (simp add:algebra_simps)
finally show ?thesis by simp
qed
have Y_eq: "Y ω = (∑i ∈ B. φ (Z i ω))" if "ω ∈ set_pmf (p c)" for c ω
proof -
have "ω ` R ⊆ B"
proof (rule image_subsetI)
fix x assume a:"x ∈ R"
have "ω x ∈ set_pmf (map_pmf (λω. ω x) (p c))"
using that by (subst set_map_pmf) simp
also have "... = set_pmf (pmf_of_set B)"
by (intro arg_cong[where f="set_pmf"] assms ran[OF assms(2)] a)
also have "... = B"
by (intro set_pmf_of_set fin_B B_ne)
finally show "ω x ∈ B" by simp
qed
hence "(ω ` R) = B ∩ ω ` R"
by auto
hence "Y ω = card (B ∩ ω ` R)"
unfolding Y_def by auto
also have "... = (∑i ∈ B. of_bool (i ∈ ω ` R))"
unfolding of_bool_def using fin_B by (subst sum.If_cases) auto
also have "... = (∑i ∈ B. of_bool (card {r ∈ R. ω r = i} > 0))"
using fin_R by (intro sum.cong arg_cong[where f="of_bool"])
(auto simp add:card_gt_0_iff)
also have "... = (∑i ∈ B. φ(Z i ω))"
unfolding φ_def Z_def by (intro sum.cong) (auto simp add:of_bool_def)
finally show ?thesis by simp
qed
let ?φ2 = "(λx y. φ x + φ y - φ (x+y))"
let ?Bd = "{x ∈ B × B. fst x ≠ snd x}"
have Y_sq_eq': "Y ω^ 2 = (∑i ∈ ?Bd. ?φ2 (Z (fst i) ω) (Z (snd i) ω)) + Y ω"
(is "?L = ?R") if "ω ∈ set_pmf (p c)" for c ω
proof -
have a: "φ (Z x ω) = of_bool(card {r ∈ R. ω r = x} > 0)" for x
unfolding φ_def Z_def by auto
have b: "φ (Z x ω + Z y ω) =
of_bool( card {r ∈ R. ω r = x} > 0 ∨ card {r ∈ R. ω r = y} > 0)" for x y
unfolding φ_def Z_def by auto
have c: "φ (Z x ω) * φ(Z y ω) = ?φ2 (Z x ω) (Z y ω)" for x y
unfolding a b of_bool_def by auto
have d: "φ (Z x ω) * φ(Z x ω) = φ (Z x ω)" for x
unfolding a of_bool_def by auto
have "?L = (∑i∈B × B. φ (Z (fst i) ω) * φ (Z (snd i) ω))"
unfolding Y_eq[OF that] power2_eq_square sum_product sum.cartesian_product
by (simp add:case_prod_beta)
also have "... = (∑i∈?Bd ∪ {x ∈ B × B. fst x = snd x}. φ (Z (fst i) ω) * φ (Z (snd i) ω))"
by (intro sum.cong refl) auto
also have "... = (∑i∈?Bd. φ (Z (fst i) ω) * φ (Z (snd i) ω)) +
(∑i∈{x ∈ B × B. fst x = snd x}. φ (Z (fst i) ω) * φ (Z (snd i) ω))"
using assms fin_B by (intro sum.union_disjoint, auto)
also have "... = (∑i∈?Bd. ?φ2 (Z (fst i) ω) (Z (snd i) ω)) +
(∑i∈{x ∈ B × B. fst x = snd x}. φ (Z (fst i) ω) * φ (Z (fst i) ω))"
unfolding c by (intro arg_cong2[where f="(+)"] sum.cong) auto
also have "... = (∑i∈?Bd. ?φ2 (Z (fst i) ω) (Z (snd i) ω)) +
(∑i∈fst ` {x ∈ B × B. fst x = snd x}. φ (Z i ω) * φ (Z i ω))"
by (subst sum.reindex, auto simp add:inj_on_def)
also have "... = (∑i∈?Bd. ?φ2 (Z (fst i) ω) (Z (snd i) ω)) + (∑i ∈ B. φ (Z i ω))"
using d by (intro arg_cong2[where f="(+)"] sum.cong refl d) (auto simp add:image_iff)
also have "... = ?R"
unfolding Y_eq[OF that] by simp
finally show ?thesis by simp
qed
have "¦integral⇧L ?p1 Y - integral⇧L ?p2 Y¦ =
¦(∫ω. (∑i ∈ B. φ(Z i ω)) ∂?p1) - (∫ω. (∑i ∈ B. φ(Z i ω)) ∂?p2)¦"
by (intro arg_cong[where f="abs"] arg_cong2[where f="(-)"]
integral_cong_AE AE_pmfI Y_eq) auto
also have "... =
¦(∑i ∈ B. (∫ω. φ(Z i ω) ∂?p1)) - (∑i ∈ B. (∫ω. φ(Z i ω) ∂?p2))¦"
by (intro arg_cong[where f="abs"] arg_cong2[where f="(-)"]
integral_sum Z_integrable[OF assms(2)])
also have "... = ¦(∑i ∈ B. (∫ω. φ(Z i ω) ∂?p1) - (∫ω. φ(Z i ω) ∂?p2))¦"
by (subst sum_subtractf) simp
also have "... ≤ (∑i ∈ B. ¦(∫ω. φ(Z i ω) ∂?p1) - (∫ω. φ(Z i ω) ∂?p2)¦)"
by simp
also have "... ≤ (∑i ∈ B. 2 * ((real (card R) / real (card B)) *γ))"
by (intro sum_mono Z_poly_diff)
also have "... ≤ 2 * real (card R) *γ"
using γ_nonneg by (simp)
finally have Y_exp_diff_1: "¦integral⇧L ?p1 Y - integral⇧L ?p2 Y¦ ≤ 2 * real (card R) *γ"
by simp
have "¦integral⇧L ?p1 Y - integral⇧L ?p2 Y¦ ≤ (2 / fact k) * real (card R)"
using Y_exp_diff_1 by (simp add:algebra_simps γ_def)
also have "... ≤ 1 / (exp 1 * (real (card B) / ε)) * card R"
using k_condition(3) k_condition_h_2 by (intro mult_right_mono) auto
also have "... = ε / (exp 1 * real (card B)) * card R"
by simp
also have "... ≤ ε / (1 * 1) * card R"
using assms(3) card_B_gt_0
by (intro mult_right_mono divide_left_mono mult_mono) auto
also have "... = ε * card R"
by simp
finally show ?A
by simp
have "¦integral⇧L ?p1 Y - integral⇧L ?p2 Y¦ ≤ 2 * real (card R) *γ"
using Y_exp_diff_1 by simp
also have "... ≤ 2 * real (card B) *γ"
by (intro mult_mono of_nat_mono assms γ_nonneg) auto
finally have Y_exp_diff_2:
"¦integral⇧L ?p1 Y - integral⇧L ?p2 Y¦ ≤ 2 *γ * real (card B)"
by (simp add:algebra_simps)
have int_Y: "integrable (measure_pmf (p c)) Y" for c
using fin_R card_image_le unfolding Y_def
by (intro integrable_pmf_iff_bounded[where C="card R"]) auto
have int_Y_sq: "integrable (measure_pmf (p c)) (λω. Y ω^2)" for c
using fin_R card_image_le unfolding Y_def
by (intro integrable_pmf_iff_bounded[where C="real (card R)^2"]) auto
have "¦(∫ω. (∑i ∈ ?Bd. ?φ2 (Z (fst i) ω) (Z (snd i) ω)) ∂?p1) -
(∫ω. (∑i ∈ ?Bd. ?φ2 (Z (fst i) ω) (Z (snd i) ω)) ∂?p2)¦
≤ ¦(∑i ∈ ?Bd.
(∫ω. φ (Z (fst i) ω) ∂?p1) + (∫ω. φ(Z (snd i) ω) ∂?p1) -
(∫ω. φ (Z (fst i) ω + Z (snd i) ω) ∂?p1) - ( (∫ω. φ(Z (fst i) ω) ∂?p2) +
(∫ω. φ (Z (snd i) ω) ∂?p2) - (∫ω. φ(Z (fst i) ω + Z (snd i) ω) ∂?p2)))¦" (is "?R3 ≤ _ ")
using Z_integrable[OF assms(2)] Z_any_integrable_2[OF assms(2)]
by (simp add:integral_sum sum_subtractf)
also have "... = ¦(∑i ∈ ?Bd.
((∫ω. φ (Z (fst i) ω) ∂?p1) - (∫ω. φ(Z (fst i) ω) ∂?p2)) +
((∫ω. φ (Z (snd i) ω) ∂?p1) - (∫ω. φ(Z (snd i) ω) ∂?p2)) +
((∫ω. φ (Z (fst i) ω + Z (snd i) ω) ∂?p2) - (∫ω. φ(Z (fst i) ω + Z (snd i) ω) ∂?p1)))¦"
by (intro arg_cong[where f="abs"] sum.cong) auto
also have "... ≤ (∑i ∈ ?Bd. ¦
((∫ω. φ (Z (fst i) ω) ∂?p1) - (∫ω. φ(Z (fst i) ω) ∂?p2)) +
((∫ω. φ (Z (snd i) ω) ∂?p1) - (∫ω. φ(Z (snd i) ω) ∂?p2)) +
((∫ω. φ (Z (fst i) ω + Z (snd i) ω) ∂?p2) - (∫ω. φ(Z (fst i) ω + Z (snd i) ω) ∂?p1))¦)"
by (intro sum_abs)
also have "... ≤ (∑i ∈ ?Bd.
¦(∫ω. φ (Z (fst i) ω) ∂?p1) - (∫ω. φ(Z (fst i) ω) ∂?p2)¦ +
¦(∫ω. φ (Z (snd i) ω) ∂?p1) - (∫ω. φ(Z (snd i) ω) ∂?p2)¦ +
¦(∫ω. φ (Z (fst i) ω + Z (snd i) ω) ∂?p2) - (∫ω. φ(Z (fst i) ω + Z (snd i) ω) ∂?p1)¦)"
by (intro sum_mono) auto
also have "... ≤ (∑i ∈ ?Bd. 2*γ + 2 *γ + 2^(k+2)*γ)"
by (intro sum_mono add_mono Z_poly_diff_2 Z_poly_diff_3) auto
also have "... = (2^(k+2)+4) *γ * real (card ?Bd)"
by (simp add:algebra_simps)
finally have Y_sq_exp_diff_1:"?R3 ≤ (2^(k+2)+4) *γ * real (card ?Bd)"
by simp
have "¦(∫ω. Y ω ^2 ∂?p1) - (∫ω. Y ω^2 ∂?p2)¦ =
¦(∫ω. (∑i ∈ ?Bd. ?φ2 (Z (fst i) ω) (Z (snd i) ω)) + Y ω ∂?p1) -
(∫ω. (∑i ∈ ?Bd. ?φ2 (Z (fst i) ω) (Z (snd i) ω)) + Y ω ∂?p2)¦"
by (intro_cong "[σ⇩2 (-), σ⇩1 abs]" more: integral_cong_AE AE_pmfI Y_sq_eq') auto
also have "... ≤ ¦(∫ω. Y ω ∂?p1) - (∫ω. Y ω ∂?p2)¦ +
¦(∫ω. (∑i ∈ ?Bd. ?φ2 (Z (fst i) ω) (Z (snd i) ω)) ∂?p1) -
(∫ω. (∑i ∈ ?Bd. ?φ2 (Z (fst i) ω) (Z (snd i) ω)) ∂?p2)¦"
using Z_integrable[OF assms(2)] Z_any_integrable_2[OF assms(2)] int_Y by simp
also have "... ≤ 2 *γ * real (card B) + ?R3"
by (intro add_mono Y_exp_diff_2, simp)
also have "... ≤ (2^(k+2)+4) *γ * real (card B) + (2^(k+2)+4) *γ * real (card ?Bd)"
using γ_nonneg by (intro add_mono Y_sq_exp_diff_1 mult_right_mono) auto
also have "... = (2^(k+2)+4) *γ * (real (card B) + real (card ?Bd))"
by (simp add:algebra_simps)
also have "... = (2^(k+2)+4) * γ * real (card B)^2"
using power2_nat_le_imp_le
by (simp add:card_distinct_pairs of_nat_diff)
finally have Y_sq_exp_diff:
"¦(∫ω. Y ω ^2 ∂?p1) - (∫ω. Y ω^2 ∂?p2)¦ ≤ (2^(k+2)+4) *γ * real (card B)^2" by simp
have Y_exp_rough_bound: "¦integral⇧L (p c) Y¦ ≤ card B" (is "?L ≤ ?R") for c
proof -
have "?L ≤ (∫ω. ¦Y ω¦ ∂(p c))"
by (intro integral_abs_bound)
also have "... ≤ (∫ω. real (card R) ∂(p c))"
unfolding Y_def using card_image_le[OF fin_R]
by (intro integral_mono integrable_pmf_iff_bounded[where C="card R"])
auto
also have "... = card R" by simp
also have "... ≤ card B" using assms by simp
finally show ?thesis by simp
qed
have "¦measure_pmf.variance ?p1 Y - measure_pmf.variance ?p2 Y¦ =
¦(∫ω. Y ω ^2 ∂?p1) - (∫ω. Y ω ∂ ?p1)^2 - ((∫ω. Y ω ^2 ∂?p2) - (∫ω. Y ω ∂ ?p2)^2)¦"
by (intro_cong "[σ⇩2 (-), σ⇩1 abs]" more: measure_pmf.variance_eq int_Y int_Y_sq)
also have "... ≤ ¦(∫ω. Y ω^2 ∂?p1) - (∫ω. Y ω^2 ∂?p2)¦ + ¦(∫ω. Y ω ∂ ?p1)⇧2 - (∫ω. Y ω ∂ ?p2)⇧2¦"
by simp
also have "... = ¦(∫ω. Y ω^2 ∂?p1) - (∫ω. Y ω^2 ∂?p2)¦ +
¦(∫ω. Y ω ∂ ?p1) - (∫ω. Y ω ∂ ?p2)¦*¦(∫ω. Y ω ∂ ?p1) + (∫ω. Y ω ∂ ?p2)¦"
by (simp add:power2_eq_square algebra_simps abs_mult[symmetric])
also have "... ≤ (2^(k+2)+4) *γ * real (card B)^2 + (2*γ *real (card B)) *
(¦∫ω. Y ω ∂?p1¦ + ¦∫ω. Y ω ∂ ?p2¦)"
using γ_nonneg
by (intro add_mono mult_mono divide_left_mono Y_sq_exp_diff Y_exp_diff_2) auto
also have "... ≤ (2^(k+2)+4)*γ * real (card B)^2 + (2*γ * real (card B)) *
(real (card B) + real (card B))"
using γ_nonneg by (intro add_mono mult_left_mono Y_exp_rough_bound) auto
also have "... = (2^(k+2)+2^3) * γ * real (card B)^2"
by (simp add:algebra_simps power2_eq_square)
also have "... ≤ (2^(k+2)+2^(k+2)) * γ * real (card B)^2"
using k_ge_2 γ_nonneg
by (intro mult_right_mono add_mono power_increasing, simp_all)
also have "... = (2^(k+3) / fact k) * card B^2"
by (simp add:power_add γ_def)
also have "... ≤ (1 / (real (card B) / ε))^2 * card B^2"
using k_condition(2) k_condition_h_2
by (intro mult_right_mono) auto
also have "... = ε^2"
using card_B_gt_0 by (simp add:divide_simps)
finally show ?B
by simp
qed
lemma
assumes "card R ≤ card B"
assumes "lim_balls_and_bins (k+1) p"
assumes "k ≥ 7.5 * (ln (card B) + 2)"
shows exp_approx_2: "¦measure_pmf.expectation p Y - μ¦ ≤ card R / sqrt (card B)"
(is "?AL ≤ ?AR")
and var_approx_2: "measure_pmf.variance p Y ≤ real (card R)^2 / card B"
(is "?BL ≤ ?BR")
proof -
define q where "q = (λc. if c then Ω else p)"
have q_altdef: "q True = Ω" "q False = p"
unfolding q_def by auto
have a:"lim_balls_and_bins (k+1) (q c)" for c
unfolding q_def using assms lim_balls_and_bins_from_ind_balls_and_bins by auto
define ε :: real where "ε = min (sqrt (1/card B)) (1 / exp 2)"
have c: "ε ∈ {0<..1 / exp 2}"
using card_B_gt_0 unfolding ε_def by auto
have b: "5 * ln (card B / ε) / ln (ln (card B / ε)) ≤ real k"
proof (cases "card B ≥ exp 4")
case True
hence "sqrt(1/card B) ≤ sqrt(1/exp 4)"
using card_B_gt_0 by (intro real_sqrt_le_mono divide_left_mono) auto
also have "... = (1/exp 2)"
by (subst powr_half_sqrt[symmetric]) (auto simp add:powr_divide exp_powr)
finally have "sqrt(1/card B) ≤ (1 / exp 2)" by simp
hence ε_eq: "ε = sqrt(1 /card B)"
unfolding ε_def by simp
have "exp (6::real) = (exp 4) powr (3/2)"
by (simp add:exp_powr)
also have "...≤ card B powr (3/2)"
by (intro powr_mono2 True) auto
finally have q4:"exp 6 ≤ card B powr (3/2)" by simp
have "(2::real) ≤ exp 6"
by (approximation 5)
hence q1: "2 ≤ real (card B) powr (3 / 2)"
using q4 by argo
have "(1::real) < ln(exp 6)"
by (approximation 5)
also have "... ≤ ln (card B powr (3 / 2))"
using card_B_gt_0 by (intro iffD2[OF ln_le_cancel_iff] q4) auto
finally have q2: "1 < ln (card B powr (3 / 2))" by simp
have "exp (exp (1::real)) ≤ exp 6"
by (approximation 5)
also have "... ≤ card B powr (3/2)" using q4 by simp
finally have "exp (exp 1) ≤ card B powr (3/2)"
by simp
hence q3: "1≤ln(ln (card B powr (3/2)))"
using card_B_gt_0 q1 by (intro iffD2[OF ln_ge_iff] ln_gt_zero, auto)
have "5 * ln (card B / ε) / ln (ln (card B / ε)) =
5 * ln (card B powr (1+1/2)) / ln(ln (card B powr (1+1/2)))"
unfolding powr_add by (simp add:real_sqrt_divide powr_half_sqrt[symmetric] ε_eq)
also have "... ≤ 5 * ln (card B powr (1+1/2)) / 1"
using True q1 q2 q3 by (intro divide_left_mono mult_nonneg_nonneg mult_pos_pos
ln_ge_zero ln_gt_zero) auto
also have "... = 5 * (1+1/2) * ln(card B)"
using card_B_gt_0 by (subst ln_powr) auto
also have "... = 7.5 * ln(card B)" by simp
also have "... ≤ k" using assms(3) by simp
finally show ?thesis by simp
next
case False
have "(1::real) / exp 2 ≤ sqrt(1 / exp 4)"
by (simp add:real_sqrt_divide powr_half_sqrt[symmetric] exp_powr)
also have "...≤ sqrt(1 /card B)"
using False card_B_gt_0
by (intro real_sqrt_le_mono divide_left_mono mult_pos_pos) auto
finally have "1 / exp 2 ≤ sqrt(1/card B)"
by simp
hence ε_eq: "ε = 1/ exp 2"
unfolding ε_def by simp
have q2:"5 * (ln x + 2) / ln (ln x + 2) ≤ 7.5 * (ln x + 2)"
if "x ∈ {1..exp 4}" for x:: real
using that by (approximation 10 splitting: x=10)
have "5 * ln (card B / ε) / ln (ln (card B / ε)) =
5 * (ln (card B) +2) / ln (ln (card B) + 2)"
using card_B_gt_0 unfolding ε_eq by (simp add:ln_mult)
also have "... ≤ 7.5 * (ln (card B) + 2)"
using False card_B_gt_0 by (intro q2) auto
also have "... ≤ k" using assms(3) by simp
finally show ?thesis by simp
qed
have "?AL = ¦(∫ω. Y ω ∂(q True)) - (∫ω. Y ω ∂(q False))¦"
using exp_balls_and_bins unfolding q_def by simp
also have "... ≤ ε * card R"
by (intro exp_approx[OF assms(1) a c b])
also have "... ≤ sqrt (1 / card B) * card R"
unfolding ε_def by (intro mult_right_mono) auto
also have "... = ?AR" using real_sqrt_divide by simp
finally show "?AL ≤ ?AR" by simp
show "?BL ≤ ?BR"
proof (cases "R= {}")
case True
then show ?thesis unfolding Y_def by simp
next
case "False"
hence "card R > 0" using fin_R by auto
hence card_R_ge_1: "real (card R) ≥ 1" by simp
have "?BL ≤ measure_pmf.variance (q True) Y +
¦measure_pmf.variance (q True) Y - measure_pmf.variance (q False) Y¦"
unfolding q_def by auto
also have "... ≤ measure_pmf.variance (q True) Y + ε^2"
by (intro add_mono var_approx[OF assms(1) a c b]) auto
also have "... ≤ measure_pmf.variance (q True) Y + sqrt(1 / card B)^2"
unfolding ε_def by (intro add_mono power_mono) auto
also have "... ≤ card R * (real (card R) - 1) / card B + sqrt(1 / card B)^2"
unfolding q_altdef by (intro add_mono var_balls_and_bins) auto
also have "... = card R * (real (card R) - 1) / card B + 1 / card B"
by (auto simp add:power_divide real_sqrt_divide)
also have "... ≤ card R * (real (card R) - 1) / card B + card R / card B"
by (intro add_mono divide_right_mono card_R_ge_1) auto
also have "... = (card R * (real (card R) - 1) + card R) / card B"
by argo
also have "... = ?BR"
by (simp add:algebra_simps power2_eq_square)
finally show "?BL ≤ ?BR" by simp
qed
qed
lemma devitation_bound:
assumes "card R ≤ card B"
assumes "lim_balls_and_bins k p"
assumes "real k ≥ C⇩2 * ln (real (card B)) + C⇩3"
shows "measure p {ω. ¦Y ω - μ¦ > 9 * real (card R) / sqrt (real (card B))} ≤ 1 / 2^6"
(is "?L ≤ ?R")
proof (cases "card R > 0")
case True
define k' :: nat where "k' = k - 1"
have "(1::real) ≤ 7.5 * 0 + 16" by simp
also have "... ≤ 7.5 * ln (real (card B)) + 16"
using card_B_ge_1 by (intro add_mono mult_left_mono ln_ge_zero) auto
also have "... ≤ k" using assms(3) unfolding C⇩2_def C⇩3_def by simp
finally have k_ge_1: "k ≥ 1" by simp
have lim: "lim_balls_and_bins (k'+1) p"
using k_ge_1 assms(2) unfolding k'_def by simp
have k'_min: "real k' ≥ 7.5 * (ln (real (card B)) + 2)"
using k_ge_1 assms(3) unfolding C⇩2_def C⇩3_def k'_def by simp
let ?r = "real (card R)"
let ?b = "real (card B)"
have a: "integrable p (λω. (Y ω)⇧2)"
unfolding Y_def
by (intro integrable_pmf_iff_bounded[where C="real (card R)^2"])
(auto intro!: card_image_le[OF fin_R])
have "?L ≤ 𝒫(ω in measure_pmf p. ¦Y ω- (∫ω. Y ω ∂p)¦ ≥ 8*?r / sqrt ?b)"
proof (rule pmf_mono)
fix ω assume "ω ∈ set_pmf p"
assume a:"ω ∈ {ω. 9 * real (card R) / sqrt (real (card B)) < ¦Y ω - μ¦}"
have "8 * ?r / sqrt ?b = 9 * ?r / sqrt ?b - ?r / sqrt ?b"
by simp
also have "... ≤ ¦Y ω - μ¦ - ¦ (∫ω. Y ω ∂p) - μ¦"
using a by (intro diff_mono exp_approx_2[OF assms(1) lim k'_min]) simp
also have "... ≤ ¦Y ω - (∫ω. Y ω ∂p)¦"
by simp
finally have "8 * ?r / sqrt ?b ≤ ¦Y ω - (∫ω. Y ω ∂p)¦" by simp
thus "ω ∈ {ω ∈ space (measure_pmf p). 8 * ?r / sqrt ?b ≤ ¦Y ω - (∫ω. Y ω ∂p)¦}"
by simp
qed
also have "... ≤ measure_pmf.variance p Y / (8*?r / sqrt ?b)^2"
using True card_B_gt_0 a
by (intro measure_pmf.Chebyshev_inequality) auto
also have "... ≤ (?r^2 / ?b) / (8*?r / sqrt ?b)^2"
by (intro divide_right_mono var_approx_2[OF assms(1) lim k'_min]) simp
also have "... = 1/2^6"
using card_B_gt_0 True
by (simp add:power2_eq_square)
finally show ?thesis by simp
next
case False
hence "R = {}" "card R = 0" using fin_R by auto
thus ?thesis
unfolding Y_def μ_def by simp
qed
end
unbundle no intro_cong_syntax
end