Theory Distributed_Distinct_Elements_Accuracy_Without_Cutoff
section ‹Accuracy without cutoff\label{sec:accuracy_wo_cutoff}›
text ‹This section verifies that each of the $l$ estimate have the required accuracy with high
probability assuming that there was no cut-off, i.e., that $s=0$. Section~\ref{sec:accuracy} will
then show that this remains true as long as the cut-off is below @{term "t f"} the subsampling
threshold.›
theory Distributed_Distinct_Elements_Accuracy_Without_Cutoff
imports
Distributed_Distinct_Elements_Inner_Algorithm
Distributed_Distinct_Elements_Balls_and_Bins
begin
no_notation Polynomials.var ("Xı")
locale inner_algorithm_fix_A = inner_algorithm +
fixes A
assumes A_range: "A ⊆ {..<n}"
assumes A_nonempty: "{} ≠ A"
begin
definition X :: nat where "X = card A"
definition q_max where "q_max = nat (⌈log 2 X⌉ - b_exp)"
definition t :: "(nat ⇒ nat) ⇒ int"
where "t f = int (Max (f ` A)) - b_exp + 9"
definition s :: "(nat ⇒ nat) ⇒ nat"
where "s f = nat (t f)"
definition R :: "(nat ⇒ nat) ⇒ nat set"
where "R f = {a. a ∈ A ∧ f a ≥ s f}"
definition r :: "nat ⇒ (nat ⇒ nat) ⇒ nat"
where "r x f = card {a. a ∈ A ∧ f a ≥ x}"
definition p where "p = (λ(f,g,h). card {j∈ {..<b}. τ⇩1 (f,g,h) A 0 j ≥ s f})"
definition Y where "Y = (λ(f,g,h). 2 ^ s f * ρ_inv (p (f,g,h)))"
lemma fin_A: "finite A"
using A_range finite_nat_iff_bounded by auto
lemma X_le_n: "X ≤ n"
proof -
have "card A ≤ card {..<n}"
by (intro card_mono A_range) simp
thus ?thesis
unfolding X_def by simp
qed
lemma X_ge_1: "X ≥ 1"
unfolding X_def
using fin_A A_nonempty by (simp add: leI)
lemma of_bool_square: "(of_bool x)⇧2 = ((of_bool x)::real)"
by (cases x, auto)
lemma r_eq: "r x f = (∑ a ∈ A.( of_bool( x ≤ f a) :: real))"
unfolding r_def of_bool_def sum.If_cases[OF fin_A]
by (simp add: Collect_conj_eq)
lemma
shows
r_exp: "(∫ω. real (r x ω) ∂ Ψ⇩1) = real X * (of_bool (x ≤ max (nat ⌈log 2 n⌉) 1) / 2^x)" and
r_var: "measure_pmf.variance Ψ⇩1 (λω. real (r x ω)) ≤ (∫ω. real (r x ω) ∂ Ψ⇩1)"
proof -
define V :: "nat ⇒ (nat ⇒ nat) ⇒ real" where "V = (λa f. of_bool (x ≤ f a))"
have V_exp: "(∫ω. V a ω ∂Ψ⇩1) = of_bool (x ≤ max (nat ⌈log 2 n⌉) 1)/2^x"
(is "?L = ?R") if "a ∈ A" for a
proof -
have a_le_n: "a < n"
using that A_range by auto
have "?L = (∫ω. indicator {f. x ≤ f a} ω ∂ Ψ⇩1)"
unfolding V_def by (intro integral_cong_AE) auto
also have "... = measure (map_pmf (λω. ω a) (sample_pmf Ψ⇩1)) {f. x ≤ f}"
by simp
also have "... = measure (𝒢 n_exp) {f. x ≤ f}"
unfolding Ψ⇩1.single[OF a_le_n] by simp
also have "... = of_bool (x ≤ max (nat ⌈log 2 n⌉) 1)/2^x"
unfolding 𝒢_prob n_exp_def by simp
finally show ?thesis by simp
qed
have b:"(∫ω. real (r x ω) ∂ Ψ⇩1) = (∑ a ∈ A. (∫ω. V a ω ∂Ψ⇩1))"
unfolding r_eq V_def using Ψ⇩1.sample_space
by (intro Bochner_Integration.integral_sum) auto
also have "... = (∑ a ∈ A. of_bool (x ≤ max (nat ⌈log 2 n⌉) 1)/2^x)"
using V_exp by (intro sum.cong) auto
also have "... = X * (of_bool (x ≤ max (nat ⌈log 2 n⌉) 1) / 2^x)"
using X_def by simp
finally show "(∫ω. real (r x ω) ∂ Ψ⇩1) = real X * (of_bool (x ≤ max (nat ⌈log 2 n⌉) 1)/ 2^x)"
by simp
have "(∫ω. (V a ω)^2 ∂ Ψ⇩1) = (∫ω. V a ω ∂ Ψ⇩1)" for a
unfolding V_def of_bool_square by simp
hence a:"measure_pmf.variance Ψ⇩1 (V a) ≤ measure_pmf.expectation Ψ⇩1 (V a)" for a
using Ψ⇩1.sample_space by (subst measure_pmf.variance_eq) auto
have "J ⊆ A ⟹ card J = 2 ⟹ prob_space.indep_vars Ψ⇩1 (λ_. borel) V J" for J
unfolding V_def using A_range finite_subset[OF _ fin_A]
by (intro prob_space.indep_vars_compose2[where Y="λi y. of_bool(x ≤ y)" and M'="λ_. discrete"]
prob_space.k_wise_indep_vars_subset[OF _ Ψ⇩1.indep]) (auto simp:prob_space_measure_pmf)
hence "measure_pmf.variance Ψ⇩1 (λω. real (r x ω)) = (∑ a ∈ A. measure_pmf.variance Ψ⇩1 (V a))"
unfolding r_eq V_def using Ψ⇩1.sample_space
by (intro measure_pmf.var_sum_pairwise_indep_2 fin_A) (simp_all)
also have "... ≤ (∑ a ∈ A. (∫ω. V a ω ∂ Ψ⇩1))"
by (intro sum_mono a)
also have "... = (∫ω. real (r x ω) ∂ Ψ⇩1)"
unfolding b by simp
finally show "measure_pmf.variance Ψ⇩1 (λω. real (r x ω)) ≤ (∫ω. real (r x ω) ∂ Ψ⇩1)" by simp
qed
definition E⇩1 where "E⇩1 = (λ(f,g,h). 2 powr (-t f) * X ∈ {b/2^16..b/2})"
lemma t_low:
"measure Ψ⇩1 {f. of_int (t f) < log 2 (real X) + 1 - b_exp} ≤ 1/2^7" (is "?L ≤ ?R")
proof (cases "log 2 (real X) ≥ 8")
case True
define Z :: "(nat ⇒ nat) ⇒ real" where "Z = r (nat ⌈log 2 (real X) - 8⌉)"
have "log 2 (real X) ≤ log 2 (real n)"
using X_le_n X_ge_1 by (intro log_mono) auto
hence "nat ⌈log 2 (real X) - 8⌉ ≤ nat ⌈log 2 (real n)⌉"
by (intro nat_mono ceiling_mono) simp
hence a:"(nat ⌈log 2 (real X) - 8⌉ ≤ max (nat ⌈log 2 (real n)⌉) 1)"
by simp
have b:"real (nat (⌈log 2 (real X)⌉ - 8)) ≤ log 2 (real X) - 7"
using True by linarith
have "2 ^ 7 = real X / (2 powr (log 2 X) * 2 powr (-7))"
using X_ge_1 by simp
also have "... = real X / (2 powr (log 2 X - 7))"
by (subst powr_add[symmetric]) simp
also have "... ≤ real X / (2 powr (real (nat ⌈log 2 (real X) - 8⌉)))"
using b by (intro divide_left_mono powr_mono) auto
also have "... = real X / 2 ^ nat ⌈log 2 (real X) - 8⌉"
by (subst powr_realpow) auto
finally have "2 ^ 7 ≤ real X / 2 ^ nat ⌈log 2 (real X) - 8⌉"
by simp
hence exp_Z_gt_2_7: "(∫ω. Z ω ∂Ψ⇩1) ≥ 2^7"
using a unfolding Z_def r_exp by simp
have var_Z_le_exp_Z: "measure_pmf.variance Ψ⇩1 Z ≤ (∫ω. Z ω ∂Ψ⇩1)"
unfolding Z_def by (intro r_var)
have "?L ≤ measure Ψ⇩1 {f. of_nat (Max (f ` A)) < log 2 (real X) - 8}"
unfolding t_def by (intro pmf_mono) (auto simp add:int_of_nat_def)
also have "... ≤ measure Ψ⇩1 {f ∈ space Ψ⇩1. (∫ω. Z ω ∂Ψ⇩1) ≤ ¦Z f - (∫ω. Z ω ∂Ψ⇩1) ¦}"
proof (rule pmf_mono)
fix f assume "f ∈ set_pmf (sample_pmf Ψ⇩1)"
have fin_f_A: "finite (f ` A)" using fin_A finite_imageI by blast
assume " f ∈ {f. real (Max (f ` A)) < log 2 (real X) - 8}"
hence "real (Max (f ` A)) < log 2 (real X) - 8" by auto
hence "real (f a) < log 2 (real X) - 8" if "a ∈ A" for a
using Max_ge[OF fin_f_A] imageI[OF that] order_less_le_trans by fastforce
hence "of_nat (f a) < ⌈log 2 (real X) - 8⌉" if "a ∈ A" for a
using that by (subst less_ceiling_iff) auto
hence "f a < nat ⌈log 2 (real X) - 8⌉" if "a ∈ A" for a
using that True by fastforce
hence "r (nat ⌈log 2 (real X) - 8⌉) f = 0"
unfolding r_def card_eq_0_iff using not_less by auto
hence "Z f = 0"
unfolding Z_def by simp
thus "f ∈ {f ∈ space Ψ⇩1. (∫ω. Z ω ∂Ψ⇩1) ≤ ¦Z f - (∫ω. Z ω ∂Ψ⇩1)¦}"
by auto
qed
also have "... ≤ measure_pmf.variance Ψ⇩1 Z / (∫ω. Z ω ∂Ψ⇩1)^2"
using exp_Z_gt_2_7 Ψ⇩1.sample_space by (intro measure_pmf.second_moment_method) simp_all
also have "... ≤ (∫ω. Z ω ∂Ψ⇩1) / (∫ω. Z ω ∂Ψ⇩1)^2"
by (intro divide_right_mono var_Z_le_exp_Z) simp
also have "... = 1 / (∫ω. Z ω ∂Ψ⇩1)"
using exp_Z_gt_2_7 by (simp add:power2_eq_square)
also have "... ≤ ?R"
using exp_Z_gt_2_7 by (intro divide_left_mono) auto
finally show ?thesis by simp
next
case "False"
have "?L ≤ measure Ψ⇩1 {f. of_nat (Max (f ` A)) < log 2 (real X) - 8}"
unfolding t_def by (intro pmf_mono) (auto simp add:int_of_nat_def)
also have "... ≤ measure Ψ⇩1 {}"
using False by (intro pmf_mono) simp
also have "... = 0"
by simp
also have "... ≤ ?R" by simp
finally show ?thesis by simp
qed
lemma t_high:
"measure Ψ⇩1 {f. of_int (t f) > log 2 (real X) + 16 - b_exp} ≤ 1/2^7" (is "?L ≤ ?R")
proof -
define Z :: "(nat ⇒ nat) ⇒ real" where "Z = r (nat ⌊log 2 (real X) + 8⌋)"
have Z_nonneg: "Z f ≥ 0" for f
unfolding Z_def r_def by simp
have "(∫ω. Z ω ∂Ψ⇩1) ≤ real X / (2 ^ nat ⌊log 2 (real X) + 8⌋)"
unfolding Z_def r_exp by simp
also have "... ≤ real X / (2 powr (real (nat ⌊log 2 (real X) + 8⌋)))"
by (subst powr_realpow) auto
also have "... ≤ real X / (2 powr ⌊log 2 (real X) + 8⌋)"
by (intro divide_left_mono powr_mono) auto
also have "... ≤ real X / (2 powr (log 2 (real X) + 7))"
by (intro divide_left_mono powr_mono, linarith) auto
also have "... = real X / 2 powr (log 2 (real X)) / 2 powr 7"
by (subst powr_add) simp
also have "... ≤ 1/2 powr 7"
using X_ge_1 by (subst powr_log_cancel) auto
finally have Z_exp: "(∫ω. Z ω ∂Ψ⇩1) ≤ 1/2^7"
by simp
have "?L ≤ measure Ψ⇩1 {f. of_nat (Max (f ` A)) > log 2 (real X) + 7}"
unfolding t_def by (intro pmf_mono) (auto simp add:int_of_nat_def)
also have "... ≤ measure Ψ⇩1 {f. Z f ≥ 1}"
proof (rule pmf_mono)
fix f assume "f ∈ set_pmf (sample_pmf Ψ⇩1)"
assume " f ∈ {f. real (Max (f ` A)) > log 2 (real X) + 7}"
hence "real (Max (f ` A)) > log 2 (real X) + 7" by simp
hence "int (Max (f ` A)) ≥ ⌊log 2 (real X) + 8⌋"
by linarith
hence "Max (f ` A) ≥ nat ⌊log 2 (real X) + 8⌋"
by simp
moreover have "f ` A ≠ {}" "finite (f ` A)"
using fin_A finite_imageI A_nonempty by auto
ultimately obtain fa where "fa ∈ f ` A" " fa ≥ nat ⌊log 2 (real X) + 8⌋"
using Max_in by auto
then obtain ae where ae_def: "ae ∈ A" "nat ⌊log 2 (real X) + 8⌋ ≤ f ae"
by auto
hence "r (nat ⌊log 2 (real X) + 8⌋) f > 0"
unfolding r_def card_gt_0_iff using fin_A by auto
hence "Z f ≥ 1"
unfolding Z_def by simp
thus "f ∈ {f. 1 ≤ Z f}" by simp
qed
also have "... ≤ (∫ω. Z ω ∂Ψ⇩1) / 1"
using Z_nonneg using Ψ⇩1.sample_space by (intro pmf_markov) auto
also have "... ≤ ?R"
using Z_exp by simp
finally show ?thesis by simp
qed
lemma e_1: "measure Ψ {ψ. ¬E⇩1 ψ} ≤ 1/2^6"
proof -
have "measure Ψ⇩1 {f. 2 powr (of_int (-t f)) * real X ∉ {real b/2^16..real b/2}} ≤
measure Ψ⇩1 {f. 2 powr (of_int (-t f)) * real X < real b/2^16} +
measure Ψ⇩1 {f. 2 powr (of_int (-t f)) * real X > real b/2}"
by (intro pmf_add) auto
also have "... ≤ measure Ψ⇩1 {f. of_int (t f) > log 2 X + 16 - b_exp} +
measure Ψ⇩1 {f. of_int (t f) < log 2 X + 1 - b_exp}"
proof (rule add_mono)
show "measure Ψ⇩1 {f. 2 powr (of_int (-t f)) * real X < real b/2^16} ≤
measure Ψ⇩1 {f. of_int (t f) > log 2 X + 16 - b_exp}"
proof (rule pmf_mono)
fix f assume "f ∈ {f. 2 powr real_of_int (-t f) * real X < real b / 2 ^ 16}"
hence "2 powr real_of_int (-t f) * real X < real b / 2 ^ 16"
by simp
hence "log 2 (2 powr of_int (-t f) * real X) < log 2 (real b / 2^16)"
using b_min X_ge_1 by (intro iffD2[OF log_less_cancel_iff]) auto
hence "of_int (-t f) + log 2 (real X) < log 2 (real b / 2^16)"
using X_ge_1 by (subst (asm) log_mult) auto
also have "... = real b_exp - log 2 (2 powr 16)"
unfolding b_def by (subst log_divide) auto
also have "... = real b_exp - 16"
by (subst log_powr_cancel) auto
finally have "of_int (-t f) + log 2 (real X) < real b_exp - 16" by simp
thus "f ∈ {f. of_int (t f) > log 2 (real X) + 16 - b_exp}"
by simp
qed
next
show "measure Ψ⇩1 {f. 2 powr of_int (-t f) * real X > real b/2} ≤
measure Ψ⇩1 {f. of_int (t f) < log 2 X + 1 - b_exp}"
proof (rule pmf_mono)
fix f assume "f ∈ {f. 2 powr real_of_int (-t f) * real X > real b / 2}"
hence "2 powr real_of_int (-t f) * real X > real b / 2"
by simp
hence "log 2 (2 powr of_int (-t f) * real X) > log 2 (real b / 2)"
using b_min X_ge_1 by (intro iffD2[OF log_less_cancel_iff]) auto
hence "of_int (-t f) + log 2 (real X) > log 2 (real b / 2)"
using X_ge_1 by (subst (asm) log_mult) auto
hence "of_int (-t f) + log 2 (real X) > real b_exp - 1"
unfolding b_def by (subst (asm) log_divide) auto
hence "of_int (t f) < log 2 (real X) + 1 - b_exp"
by simp
thus "f ∈ {f. of_int (t f) < log 2 (real X) + 1 - b_exp}"
by simp
qed
qed
also have "... ≤ 1/2^7 + 1/2^7"
by (intro add_mono t_low t_high)
also have "... = 1/2^6" by simp
finally have "measure Ψ⇩1 {f. 2 powr of_int (-t f) * real X ∉ {real b/2^16..real b/2}} ≤ 1/2^6"
by simp
thus ?thesis
unfolding sample_pmf_Ψ E⇩1_def case_prod_beta
by (subst pair_pmf_prob_left)
qed
definition E⇩2 where "E⇩2 = (λ(f,g,h). ¦card (R f) - X / 2^(s f)¦ ≤ ε/3 * X / 2^(s f))"
lemma e_2: "measure Ψ {ψ. E⇩1 ψ ∧ ¬E⇩2 ψ} ≤ 1/2^6" (is "?L ≤ ?R")
proof -
define t⇩m :: int where "t⇩m = ⌊log 2 (real X)⌋ + 16 - b_exp"
have t_m_bound: "t⇩m ≤ ⌊log 2 (real X)⌋ - 10"
unfolding t⇩m_def using b_exp_ge_26 by simp
have "real b / 2^16 = (real X * (1/ X)) * (real b / 2^16)"
using X_ge_1 by simp
also have "... = (real X * 2 powr (-log 2 X)) * (real b / 2^16)"
using X_ge_1 by (subst powr_minus_divide) simp
also have "... ≤ (real X * 2 powr (- ⌊log 2 (real X)⌋)) * (2 powr b_exp / 2^16)"
unfolding b_def using powr_realpow
by (intro mult_mono powr_mono) auto
also have "... = real X * (2 powr (- ⌊log 2 (real X)⌋) * 2 powr(real b_exp-16))"
by (subst powr_diff) simp
also have "... = real X * 2 powr (- ⌊log 2 (real X)⌋ + (int b_exp - 16))"
by (subst powr_add[symmetric]) simp
also have "... = real X * 2 powr (-t⇩m)"
unfolding t⇩m_def by (simp add:algebra_simps)
finally have c:"real b / 2^16 ≤ real X * 2 powr (-t⇩m)" by simp
define T :: "nat set" where "T = {x. (real X / 2^x ≥ real b / 2^16)}"
have "x ∈ T ⟷ int x ≤ t⇩m" for x
proof -
have "x ∈ T ⟷ 2^ x ≤ real X * 2^16 / b"
using b_min by (simp add: field_simps T_def)
also have "... ⟷ log 2 (2^x) ≤ log 2 (real X * 2^16 / b)"
using X_ge_1 b_min by (intro log_le_cancel_iff[symmetric] divide_pos_pos) auto
also have "... ⟷ x ≤ log 2 (real X * 2^16) - log 2 b"
using X_ge_1 b_min by (subst log_divide) auto
also have "... ⟷ x ≤ log 2 (real X) + log 2 (2 powr 16) - b_exp"
unfolding b_def using X_ge_1 by (subst log_mult) auto
also have "... ⟷ x ≤ ⌊log 2 (real X) + log 2 (2 powr 16) - b_exp⌋"
by linarith
also have "... ⟷ x ≤ ⌊log 2 (real X) + 16 - real_of_int (int b_exp)⌋"
by (subst log_powr_cancel) auto
also have "... ⟷ x ≤ t⇩m"
unfolding t⇩m_def by linarith
finally show ?thesis by simp
qed
hence T_eq: "T = {x. int x ≤ t⇩m}" by auto
have "T = {x. int x < t⇩m+1}"
unfolding T_eq by simp
also have "... = {x. x < nat (t⇩m + 1)}"
unfolding zless_nat_eq_int_zless by simp
finally have T_eq_2: "T = {x. x < nat (t⇩m + 1)}"
by simp
have inj_1: "inj_on ((-) (nat t⇩m)) T"
unfolding T_eq by (intro inj_onI) simp
have fin_T: "finite T"
unfolding T_eq_2 by simp
have r_exp: "(∫ω. real (r t ω) ∂Ψ⇩1) = real X / 2^t" if "t ∈ T" for t
proof -
have "t ≤ t⇩m"
using that unfolding T_eq by simp
also have "... ≤ ⌊log 2 (real X)⌋ - 10"
using t_m_bound by simp
also have "... ≤ ⌊log 2 (real X)⌋"
by simp
also have "... ≤ ⌊log 2 (real n)⌋"
using X_le_n X_ge_1 by (intro floor_mono log_mono) auto
also have "... ≤ ⌈log 2 (real n)⌉"
by simp
finally have "t ≤ ⌈log 2 (real n)⌉" by simp
hence "t ≤ max (nat ⌈log 2 (real n)⌉) 1"by simp
thus ?thesis
unfolding r_exp by simp
qed
have r_var: "measure_pmf.variance Ψ⇩1 (λω. real (r t ω)) ≤ real X / 2^t" if "t ∈ T" for t
using r_exp[OF that] r_var by metis
have "9 = C⇩4 / ε⇧2 * ε^2/2^23"
using ε_gt_0 by (simp add:C⇩4_def)
also have "... = 2 powr (log 2 (C⇩4 / ε⇧2)) * ε^2/2^23"
using ε_gt_0 C⇩4_def by (subst powr_log_cancel) auto
also have "... ≤ 2 powr b_exp * ε^2/2^23"
unfolding b_exp_def
by (intro divide_right_mono mult_right_mono powr_mono, linarith) auto
also have "... = b * ε^2/2^23"
using powr_realpow unfolding b_def by simp
also have "... = (b/2^16) * (ε^2/2^7)"
by simp
also have "... ≤ (X * 2 powr (-t⇩m)) * (ε^2/2^7)"
by (intro mult_mono c) auto
also have "... = X * (2 powr (-t⇩m) * 2 powr (-7)) * ε^2"
using powr_realpow by simp
also have "... = 2 powr (-t⇩m-7) * (ε^2 * X)"
by (subst powr_add[symmetric]) (simp )
finally have "9 ≤ 2 powr (-t⇩m-7) * (ε^2 * X)" by simp
hence b: "9/ (ε^2 * X) ≤ 2 powr (-t⇩m -7)"
using ε_gt_0 X_ge_1
by (subst pos_divide_le_eq) auto
have a: "measure Ψ⇩1 {f.¦real (r t f)-real X/2^t¦> ε/3 *real X/2^t} ≤ 2 powr (real t-t⇩m-7)"
(is"?L1 ≤ ?R1") if "t ∈ T" for t
proof -
have "?L1 ≤ 𝒫(f in Ψ⇩1. ¦real (r t f) - real X / 2^t¦ ≥ ε/3 * real X / 2^t)"
by (intro pmf_mono) auto
also have "... = 𝒫(f in Ψ⇩1. ¦real (r t f)-(∫ω. real (r t ω) ∂ Ψ⇩1)¦ ≥ ε/3 * real X/2^t)"
by (simp add: r_exp[OF that])
also have "... ≤ measure_pmf.variance Ψ⇩1 (λω. real (r t ω)) / (ε/3 * real X / 2^t)^2"
using X_ge_1 ε_gt_0 Ψ⇩1.sample_space
by (intro measure_pmf.Chebyshev_inequality divide_pos_pos mult_pos_pos) auto
also have "... ≤ (X / 2^t) / (ε/3 * X / 2^t)^2"
by (intro divide_right_mono r_var[OF that]) simp
also have "... = 2^t*(9/ ( ε^2 * X))"
by (simp add:power2_eq_square algebra_simps)
also have "... ≤ 2^t*(2 powr (-t⇩m-7))"
by (intro mult_left_mono b) simp
also have "... = 2 powr t * 2 powr (-t⇩m-7)"
by (subst powr_realpow[symmetric]) auto
also have "... = ?R1"
by (subst powr_add[symmetric]) (simp add:algebra_simps)
finally show "?L1 ≤ ?R1" by simp
qed
have "∃y<nat (t⇩m + 1). x = nat t⇩m - y" if "x < nat (t⇩m+1)" for x
using that by (intro exI[where x="nat t⇩m - x"]) simp
hence T_reindex: "(-) (nat t⇩m) ` {x. x < nat (t⇩m + 1)} = {..<nat (t⇩m + 1)}"
by (auto simp add: set_eq_iff image_iff)
have "?L ≤ measure Ψ {ψ. (∃t ∈ T. ¦real (r t (fst ψ))-real X/2^t¦ > ε/3 * real X / 2^t)}"
proof (rule pmf_mono)
fix ψ
assume "ψ ∈ set_pmf (sample_pmf Ψ)"
obtain f g h where ψ_def: "ψ = (f,g,h)" by (metis prod_cases3)
assume "ψ ∈ {ψ. E⇩1 ψ ∧ ¬ E⇩2 ψ}"
hence a:"2 powr ( -real_of_int (t f)) * real X ∈ {real b/2^16..real b/2}" and
b:"¦card (R f) - real X / 2^(s f)¦ > ε/3 * X / 2^(s f)"
unfolding E⇩1_def E⇩2_def by (auto simp add:ψ_def)
have "¦card (R f) - X / 2^(s f)¦ = 0" if "s f= 0"
using that by (simp add:R_def X_def)
moreover have "( ε/3) * (X / 2^s f) ≥ 0"
using ε_gt_0 X_ge_1 by (intro mult_nonneg_nonneg) auto
ultimately have "False" if "s f = 0"
using b that by simp
hence "s f > 0" by auto
hence "t f = s f" unfolding s_def by simp
hence "2 powr (-real (s f)) * X ≥ b / 2^16"
using a by simp
hence "X / 2 powr (real (s f)) ≥ b / 2^16"
by (simp add: divide_powr_uminus mult.commute)
hence "real X / 2 ^ (s f) ≥ b / 2^16"
by (subst (asm) powr_realpow, auto)
hence "s f ∈ T" unfolding T_def by simp
moreover have "¦r (s f) f - X / 2^s f¦ > ε/3 * X / 2^s f"
using R_def r_def b by simp
ultimately have "∃t ∈ T. ¦r t (fst ψ) - X / 2^t¦ > ε/3 * X / 2^t"
using ψ_def by (intro bexI[where x="s f"]) simp
thus "ψ ∈ {ψ. (∃t ∈ T. ¦r t (fst ψ) - X / 2^t¦ > ε/3 * X / 2^t)}" by simp
qed
also have "... = measure Ψ⇩1 {f. (∃t ∈ T. ¦real (r t f)-real X / 2^t¦ > ε/3 * real X/2^t)}"
unfolding sample_pmf_Ψ by (intro pair_pmf_prob_left)
also have "... = measure Ψ⇩1 (⋃t ∈ T. {f. ¦real (r t f)-real X / 2^t¦ > ε/3 * real X/2^t})"
by (intro measure_pmf_cong) auto
also have "... ≤ (∑t ∈ T. measure Ψ⇩1 {f.¦real (r t f)-real X / 2^t¦ > ε/3 * real X/2^t})"
by (intro measure_UNION_le fin_T) (simp)
also have "... ≤ (∑t ∈ T. 2 powr (real t - of_int t⇩m - 7))"
by (intro sum_mono a)
also have "... = (∑t ∈ T. 2 powr (-int (nat t⇩m-t) - 7))"
unfolding T_eq
by (intro sum.cong refl arg_cong2[where f="(powr)"]) simp
also have "... = (∑x ∈ (λx. nat t⇩m - x) ` T. 2 powr (-real x - 7))"
by (subst sum.reindex[OF inj_1]) simp
also have "... = (∑x ∈ (λx. nat t⇩m - x) ` T. 2 powr (-7) * 2 powr (-real x))"
by (subst powr_add[symmetric]) (simp add:algebra_simps)
also have "... = 1/2^7 * (∑x ∈ (λx. nat t⇩m - x) ` T. 2 powr (-real x))"
by (subst sum_distrib_left) simp
also have "... = 1/2^7 * (∑x <nat (t⇩m+1). 2 powr (-real x))"
unfolding T_eq_2 T_reindex
by (intro arg_cong2[where f="(*)"] sum.cong) auto
also have "... = 1/2^7 * (∑x <nat (t⇩m+1). (2 powr (-1)) powr (real x))"
by (subst powr_powr) simp
also have "... = 1/2^7 * (∑x <nat (t⇩m+1). (1/2)^x)"
using powr_realpow by simp
also have "... ≤ 1/2^7 * 2"
by(subst geometric_sum) auto
also have "... = 1/2^6" by simp
finally show ?thesis by simp
qed
definition E⇩3 where "E⇩3 = (λ(f,g,h). inj_on g (R f))"
lemma R_bound:
fixes f g h
assumes "E⇩1 (f,g,h)"
assumes "E⇩2 (f,g,h)"
shows "card (R f) ≤ 2/3 * b"
proof -
have "real (card (R f)) ≤ ( ε / 3) * (real X / 2 ^ s f) + real X / 2 ^ s f"
using assms(2) unfolding E⇩2_def by simp
also have "... ≤ (1/3) * (real X / 2 ^ s f) + real X / 2 ^ s f"
using ε_lt_1 by (intro add_mono mult_right_mono) auto
also have "... = (4/3) * (real X / 2 powr s f)"
using powr_realpow by simp
also have "... ≤ (4/3) * (real X / 2 powr t f)"
unfolding s_def
by (intro mult_left_mono divide_left_mono powr_mono) auto
also have "... = (4/3) * (2 powr (-(of_int (t f))) * real X)"
by (subst powr_minus_divide) simp
also have "... = (4/3) * (2 powr (- t f) * real X)"
by simp
also have "... ≤ (4/3) * (b/2)"
using assms(1) unfolding E⇩1_def
by (intro mult_left_mono) auto
also have "... ≤ (2/3) * b" by simp
finally show ?thesis by simp
qed
lemma e_3: "measure Ψ {ψ. E⇩1 ψ ∧ E⇩2 ψ ∧ ¬E⇩3 ψ} ≤ 1/2^6" (is "?L ≤ ?R")
proof -
let ?α = "(λ(z,x,y) f. z < C⇩7*b^2 ∧ x ∈ R f ∧ y ∈ R f ∧ x < y)"
let ?β = "(λ(z,x,y) g. g x = z ∧ g y = z)"
have β_prob: "measure Ψ⇩2 {g. ?β ω g} ≤ (1/real (C⇩7*b^2)^2)"
if "?α ω f" for ω f
proof -
obtain x y z where ω_def: "ω = (z,x,y)" by (metis prod_cases3)
have a:"prob_space.k_wise_indep_vars Ψ⇩2 2 (λi. discrete) (λx ω. ω x = z) {..<n}"
by (intro prob_space.k_wise_indep_vars_compose[OF _ Ψ⇩2.indep])
(simp_all add:prob_space_measure_pmf)
have "u ∈ R f ⟹ u < n" for u
unfolding R_def using A_range by auto
hence b: "x < n" "y < n" "card {x, y} = 2"
using that ω_def by auto
have c: "z < C⇩7*b⇧2" using ω_def that by simp
have "measure Ψ⇩2 {g. ?β ω g} = measure Ψ⇩2 {g. (∀ξ ∈ {x,y}. g ξ = z)}"
by (simp add:ω_def)
also have "... = (∏ξ ∈ {x,y}. measure Ψ⇩2 {g. g ξ = z})"
using b by (intro measure_pmf.split_indep_events[OF refl, where I="{x,y}"]
prob_space.k_wise_indep_vars_subset[OF _ a]) (simp_all add:prob_space_measure_pmf)
also have "... = (∏ξ ∈ {x,y}. measure (map_pmf (λω. ω ξ) (sample_pmf Ψ⇩2)) {g. g = z}) "
by (simp add:vimage_def)
also have "... = (∏ξ ∈ {x,y}. measure [C⇩7 * b⇧2]⇩S {g. g=z})"
using b Ψ⇩2.single by (intro prod.cong) fastforce+
also have "... = (∏ξ ∈ {x,y}. measure (pmf_of_set {..<C⇩7 * b⇧2}) {z})"
by (subst nat_sample_pmf) simp
also have "... = (measure (pmf_of_set {..<C⇩7 * b⇧2}) {z})^2"
using b by simp
also have "... ≤ (1 /(C⇩7*b⇧2))^2"
using c by (subst measure_pmf_of_set) auto
also have "... = (1 /(C⇩7*b⇧2)^2)"
by (simp add:algebra_simps power2_eq_square)
finally show ?thesis by simp
qed
have α_card: "card {ω. ?α ω f} ≤ (C⇩7*b^2) * (card (R f) * (card (R f)-1)/2)"
(is "?TL ≤ ?TR") and fin_α: "finite {ω. ?α ω f}" (is "?T2") for f
proof -
have t1: "{ω. ?α ω f} ⊆ {..<C⇩7*b^2} × {(x,y) ∈ R f × R f. x < y}"
by (intro subsetI) auto
moreover have "card ({..<C⇩7*b^2} × {(x,y) ∈ R f × R f. x < y}) = ?TR"
using card_ordered_pairs'[where M="R f"]
by (simp add: card_cartesian_product)
moreover have "finite (R f)"
unfolding R_def using fin_A finite_subset by simp
hence "finite {(x, y). (x, y) ∈ R f × R f ∧ x < y}"
by (intro finite_subset[where B="R f × R f", OF _ finite_cartesian_product]) auto
hence t2: "finite ({..<C⇩7*b^2} × {(x,y) ∈ R f × R f. x < y})"
by (intro finite_cartesian_product) auto
ultimately show "?TL ≤ ?TR"
using card_mono of_nat_le_iff by (metis (no_types, lifting))
show ?T2
using finite_subset[OF t1 t2] by simp
qed
have "?L ≤ measure Ψ {(f,g,h). card (R f) ≤ b ∧ (∃ x y z. ?α (x,y,z) f ∧ ?β (x,y,z) g)}"
proof (rule pmf_mono)
fix ψ assume b:"ψ ∈ set_pmf (sample_pmf Ψ)"
obtain f g h where ψ_def:"ψ = (f,g,h)" by (metis prod_cases3)
have "(f,g,h) ∈ sample_set Ψ"
using sample_space_alt[OF sample_space_Ψ] b ψ_def by simp
hence c:"g x < C⇩7*b^2" for x
using g_range by simp
assume a:"ψ ∈ {ψ. E⇩1 ψ ∧ E⇩2 ψ ∧ ¬ E⇩3 ψ}"
hence "card (R f) ≤ 2/3 * b"
using R_bound ψ_def by force
moreover have "∃a b. a ∈ R f ∧ b ∈ R f ∧ a ≠ b ∧ g a = g b"
using a unfolding ψ_def E⇩3_def inj_on_def by auto
hence "∃x y. x ∈ R f ∧ y ∈ R f ∧ x < y ∧ g x = g y"
by (metis not_less_iff_gr_or_eq)
hence "∃x y z. ?α (x,y,z) f ∧ ?β (x,y,z) g"
using c by blast
ultimately show "ψ ∈ {(f, g, h). card (R f) ≤ b ∧ (∃ x y z. ?α (x,y,z) f ∧ ?β (x,y,z) g)}"
unfolding ψ_def by auto
qed
also have "... = (∫f. measure (pair_pmf Ψ⇩2 Ψ⇩3)
{g. card (R f) ≤ b ∧ (∃x y z. ?α (x,y,z) f ∧ ?β (x,y,z) (fst g))} ∂Ψ⇩1)"
unfolding sample_pmf_Ψ split_pair_pmf by (simp add: case_prod_beta)
also have
"... = (∫f. measure Ψ⇩2 {g. card (R f) ≤ b ∧ (∃x y z. ?α (x,y,z) f ∧ ?β (x,y,z) g)} ∂Ψ⇩1)"
by (subst pair_pmf_prob_left) simp
also have "... ≤ (∫f. 1/real (2*C⇩7) ∂Ψ⇩1)"
proof (rule pmf_exp_mono[OF integrable_sample_pmf[OF Ψ⇩1.sample_space]
integrable_sample_pmf[OF Ψ⇩1.sample_space]])
fix f assume "f ∈ set_pmf (sample_pmf Ψ⇩1)"
show "measure Ψ⇩2 {g. card (R f) ≤ b ∧ (∃x y z. ?α (x,y,z) f ∧ ?β (x,y,z) g)} ≤ 1 / real (2 * C⇩7)"
(is "?L1 ≤ ?R1")
proof (cases "card (R f) ≤ b")
case True
have "?L1 ≤ measure Ψ⇩2 (⋃ ω ∈ {ω. ?α ω f}. {g. ?β ω g})"
by (intro pmf_mono) auto
also have "... ≤ (∑ω ∈ {ω. ?α ω f}. measure Ψ⇩2 {g. ?β ω g})"
by (intro measure_UNION_le fin_α) auto
also have "... ≤ (∑ω ∈ {ω. ?α ω f}. (1/real (C⇩7*b^2)^2))"
by (intro sum_mono β_prob) auto
also have "... = card {ω. ?α ω f} /(C⇩7*b^2)^2"
by simp
also have "... ≤ (C⇩7*b^2) * (card (R f) * (card (R f)-1)/2) / (C⇩7*b^2)^2"
by (intro α_card divide_right_mono) simp
also have "... ≤ (C⇩7*b^2) * (b * b / 2) / (C⇩7*b^2)^2"
unfolding C⇩7_def using True
by (intro divide_right_mono Nat.of_nat_mono mult_mono) auto
also have "... = 1/(2*C⇩7)"
using b_min by (simp add:algebra_simps power2_eq_square)
finally show ?thesis by simp
next
case False
then show ?thesis by simp
qed
qed
also have "... ≤ 1/2^6"
unfolding C⇩7_def by simp
finally show ?thesis by simp
qed
definition E⇩4 where "E⇩4 = (λ(f,g,h). ¦p (f,g,h) - ρ (card (R f))¦ ≤ ε/12 * card (R f))"
lemma e_4_h: "9 / sqrt b ≤ ε / 12"
proof -
have "108 ≤ sqrt (C⇩4)"
unfolding C⇩4_def by (approximation 5)
also have "... ≤ sqrt( ε^2 * real b)"
using b_lower_bound ε_gt_0
by (intro real_sqrt_le_mono) (simp add: pos_divide_le_eq algebra_simps)
also have "... = ε * sqrt b"
using ε_gt_0 by (simp add:real_sqrt_mult)
finally have "108 ≤ ε * sqrt b" by simp
thus ?thesis
using b_min by (simp add:pos_divide_le_eq)
qed
lemma e_4: "measure Ψ {ψ. E⇩1 ψ ∧ E⇩2 ψ ∧ E⇩3 ψ ∧ ¬E⇩4 ψ} ≤ 1/2^6" (is "?L ≤ ?R")
proof -
have a: "measure Ψ⇩3 {h. E⇩1 (f,g,h) ∧ E⇩2 (f,g,h) ∧ E⇩3 (f,g,h) ∧ ¬E⇩4 (f,g,h)} ≤ 1/2^6"
(is "?L1 ≤ ?R1") if "f ∈ set_pmf (sample_pmf Ψ⇩1)" "g ∈ set_pmf(sample_pmf Ψ⇩2)"
for f g
proof (cases "card (R f) ≤ b ∧ inj_on g (R f)")
case True
have g_inj: "inj_on g (R f)"
using True by simp
have fin_R: "finite (g ` R f)"
unfolding R_def using fin_A
by (intro finite_imageI) simp
interpret B:balls_and_bins_abs "g ` R f" "{..<b}"
using fin_R b_ne by unfold_locales auto
have "range g ⊆ {..<C⇩7 * b⇧2}"
using g_range_1 that(2) unfolding sample_space_alt[OF Ψ⇩2.sample_space] by auto
hence g_ran: "g ` R f ⊆ {..<C⇩7 * b⇧2}"
by auto
have "sample_pmf [b]⇩S = pmf_of_set {..<b}"
unfolding sample_pmf_def nat_sample_space_def by simp
hence " map_pmf (λω. ω x) (sample_pmf (ℋ k (C⇩7 * b⇧2) [b]⇩S)) = pmf_of_set {..<b}"
if "x ∈ g ` R f" for x
using g_ran Ψ⇩3.single that by auto
moreover have "prob_space.k_wise_indep_vars Ψ⇩3 k (λ_. discrete) (λx ω. ω x) (g ` R f)"
by (intro prob_space.k_wise_indep_subset[OF _ _ Ψ⇩3.indep] g_ran prob_space_measure_pmf)
ultimately have lim_balls_and_bins: "B.lim_balls_and_bins k (sample_pmf (ℋ k (C⇩7 * b⇧2) [b]⇩S))"
unfolding B.lim_balls_and_bins_def by auto
have card_g_R: "card (g ` R f) = card (R f)"
using True card_image by auto
hence b_mu: "ρ (card (R f)) = B.μ"
unfolding B.μ_def ρ_def using b_min by (simp add:powr_realpow)
have card_g_le_b: "card (g ` R f) ≤ card {..<b}"
unfolding card_g_R using True by simp
have "?L1 ≤ measure Ψ⇩3 {h. ¦B.Y h - B.μ¦ > 9 * real (card (g ` R f)) / sqrt (card {..<b})}"
proof (rule pmf_mono)
fix h assume "h ∈ {h. E⇩1 (f,g,h) ∧ E⇩2 (f,g,h) ∧ E⇩3 (f,g,h) ∧ ¬E⇩4 (f,g,h)}"
hence b: "¦p (f,g,h) -ρ (card (R f))¦ > ε/12 * card (R f)"
unfolding E⇩4_def by simp
assume "h ∈ set_pmf (sample_pmf Ψ⇩3)"
hence h_range: "h x < b" for x
unfolding sample_space_alt[OF Ψ⇩3.sample_space,symmetric] using h_range_1 by simp
have "{j ∈ {..<b}. int (s f) ≤ τ⇩1 (f, g, h) A 0 j} =
{j ∈ {..<b}. int (s f) ≤ max (Max ({int (f a) |a. a ∈ A ∧ h (g a) = j} ∪ {-1})) (- 1)}"
unfolding τ⇩1_def by simp
also have "... = {j ∈ {..<b}. int (s f) ≤ Max ({int (f a) |a. a ∈ A ∧ h (g a) = j} ∪ {-1})}"
using fin_A by (subst max_absorb1) (auto intro: Max_ge)
also have "... = {j ∈ {..<b}. (∃a ∈ R f. h (g a) = j)}"
unfolding R_def using fin_A by (subst Max_ge_iff) auto
also have "... = {j. ∃a ∈ R f. h (g a) = j}"
using h_range by auto
also have "... = (h ∘ g) ` (R f)"
by (auto simp add:set_eq_iff image_iff)
also have "... = h ` (g ` (R f))"
by (simp add:image_image)
finally have c:"{j ∈ {..<b}. int (s f) ≤ τ⇩1 (f, g, h) A 0 j} = h ` (g ` R f)"
by simp
have "9 * real (card (g ` R f)) / sqrt (card {..<b}) = 9/ sqrt b * real (card (R f))"
using card_image[OF g_inj] by simp
also have "... ≤ ε/12 * card (R f)"
by (intro mult_right_mono e_4_h) simp
also have "... < ¦B.Y h - B.μ¦"
using b c unfolding B.Y_def p_def b_mu by simp
finally show "h ∈ {h. ¦B.Y h - B.μ¦ > 9 * real (card (g ` R f)) / sqrt (card {..<b})}"
by simp
qed
also have "... ≤ 1/2^6"
using k_min
by (intro B.devitation_bound[OF card_g_le_b lim_balls_and_bins]) auto
finally show ?thesis by simp
next
case False
have "?L1 ≤ measure Ψ⇩3 {}"
proof (rule pmf_mono)
fix h assume b:"h ∈ {h. E⇩1 (f, g, h) ∧ E⇩2 (f, g, h) ∧ E⇩3 (f, g, h) ∧ ¬ E⇩4 (f, g, h)}"
hence "card (R f) ≤ (2/3)*b"
by (auto intro!: R_bound[simplified])
hence "card (R f) ≤ b"
by simp
moreover have "inj_on g (R f)"
using b by (simp add:E⇩3_def)
ultimately have "False" using False by simp
thus "h ∈ {}" by simp
qed
also have "... = 0" by simp
finally show ?thesis by simp
qed
have "?L = (∫f. (∫g.
measure Ψ⇩3 {h. E⇩1 (f,g,h) ∧ E⇩2 (f,g,h) ∧ E⇩3 (f,g,h) ∧ ¬E⇩4 (f,g,h)} ∂Ψ⇩2) ∂Ψ⇩1)"
unfolding sample_pmf_Ψ split_pair_pmf by simp
also have "... ≤ (∫f. (∫g. 1/2^6 ∂Ψ⇩2) ∂Ψ⇩1)"
using a Ψ⇩1.sample_space Ψ⇩2.sample_space
by (intro integral_mono_AE AE_pmfI) simp_all
also have "... = 1/2^6"
by simp
finally show ?thesis by simp
qed
lemma ρ_inverse: "ρ_inv (ρ x) = x"
proof -
have a:"1-1/b ≠ 0"
using b_min by simp
have "ρ x = b * (1-(1-1/b) powr x)"
unfolding ρ_def by simp
hence "ρ x / real b = 1-(1-1/b) powr x" by simp
hence "ln (1 - ρ x / real b) = ln ((1-1/b) powr x)" by simp
also have "... = x * ln (1 - 1/ b)"
using a by (intro ln_powr)
finally have "ln (1 - ρ x / real b) = x * ln (1- 1/ b)"
by simp
moreover have "ln (1-1/b) < 0"
using b_min by (subst ln_less_zero_iff) auto
ultimately show ?thesis
using ρ_inv_def by simp
qed
lemma rho_mono:
assumes "x ≤ y"
shows "ρ x ≤ ρ y"
proof-
have "(1 - 1 / real b) powr y ≤ (1 - 1 / real b) powr x"
using b_min
by (intro powr_mono_rev assms) auto
thus ?thesis
unfolding ρ_def by (intro mult_left_mono) auto
qed
lemma rho_two_thirds: "ρ (2/3 * b) ≤ 3/5 *b"
proof -
have "1/3 ≤ exp ( - 13 / 12::real )"
by (approximation 8)
also have "... ≤ exp ( - 1 - 2 / real b )"
using b_min by (intro iffD2[OF exp_le_cancel_iff]) (simp add:algebra_simps)
also have "... ≤ exp ( b * (-(1/real b)-2*(1/real b)^2))"
using b_min by (simp add:algebra_simps power2_eq_square)
also have "... ≤ exp ( b * ln (1-1/real b))"
using b_min
by (intro iffD2[OF exp_le_cancel_iff] mult_left_mono ln_one_minus_pos_lower_bound) auto
also have "... = exp ( ln ( (1-1/real b) powr b))"
using b_min by (subst ln_powr) auto
also have "... = (1-1/real b) powr b"
using b_min by (subst exp_ln) auto
finally have a:"1/3 ≤ (1-1/real b) powr b" by simp
have "2/5 ≤ (1/3) powr (2/3::real)"
by (approximation 5)
also have "... ≤ ((1-1/real b) powr b) powr (2/3)"
by (intro powr_mono2 a) auto
also have "... = (1-1/real b) powr (2/3 * real b)"
by (subst powr_powr) (simp add:algebra_simps)
finally have "2/5 ≤ (1 - 1 / real b) powr (2 / 3 * real b)" by simp
hence "1 - (1 - 1 / real b) powr (2 / 3 * real b) ≤ 3/5"
by simp
hence "ρ (2/3 * b) ≤ b * (3/5)"
unfolding ρ_def by (intro mult_left_mono) auto
thus ?thesis
by simp
qed
definition ρ_inv' :: "real ⇒ real"
where "ρ_inv' x = -1 / (real b * (1-x / real b) * ln (1 - 1 / real b))"
lemma ρ_inv'_bound:
assumes "x ≥ 0"
assumes "x ≤ 59/90*b"
shows "¦ρ_inv' x¦ ≤ 4"
proof -
have c:"ln (1 - 1 / real b) < 0"
using b_min
by (subst ln_less_zero_iff) auto
hence d:"real b * (1 - x / real b) * ln (1 - 1 / real b) < 0"
using b_min assms by (intro Rings.mult_pos_neg) auto
have "(1::real) ≤ 31/30" by simp
also have "... ≤ (31/30) * (b * -(- 1 / real b))"
using b_min by simp
also have "... ≤ (31/30) * (b * -ln (1 + (- 1 / real b)))"
using b_min
by (intro mult_left_mono le_imp_neg_le ln_add_one_self_le_self2) auto
also have "... ≤ 3 * (31/90) * (- b * ln (1 - 1 / real b))"
by simp
also have "... ≤ 3 * (1 - x / real b) * (- b * ln (1 - 1 / real b))"
using assms b_min pos_divide_le_eq[where c="b"] c
by (intro mult_right_mono mult_left_mono mult_nonpos_nonpos) auto
also have "... ≤ 3 * (real b * (1 - x / real b) * (-ln (1 - 1 / real b)))"
by (simp add:algebra_simps)
finally have "3 * (real b * (1 - x / real b) * (-ln (1 - 1 / real b))) ≥ 1" by simp
hence "3 * (real b * (1 - x / real b) * ln (1 - 1 / real b)) ≤ -1" by simp
hence "ρ_inv' x ≤ 3"
unfolding ρ_inv'_def using d
by (subst neg_divide_le_eq) auto
moreover have "ρ_inv' x > 0"
unfolding ρ_inv'_def using d by (intro divide_neg_neg) auto
ultimately show ?thesis by simp
qed
lemma ρ_inv':
fixes x :: real
assumes "x < b"
shows "DERIV ρ_inv x :> ρ_inv' x"
proof -
have "DERIV (ln ∘ (λx. (1 - x / real b))) x :> 1 / (1-x / real b) * (0 -1/b)"
using assms b_min
by (intro DERIV_chain DERIV_ln_divide DERIV_cdivide derivative_intros) auto
hence "DERIV ρ_inv x :> (1 / (1-x / real b) * (-1/b)) / ln (1-1/real b)"
unfolding comp_def ρ_inv_def by (intro DERIV_cdivide) auto
thus ?thesis
by (simp add:ρ_inv'_def algebra_simps)
qed
lemma accuracy_without_cutoff:
"measure Ψ {(f,g,h). ¦Y (f,g,h) - real X¦ > ε * X ∨ s f < q_max} ≤ 1/2^4"
(is "?L ≤ ?R")
proof -
have "?L ≤ measure Ψ {ψ. ¬E⇩1 ψ ∨ ¬E⇩2 ψ ∨ ¬E⇩3 ψ ∨ ¬E⇩4 ψ}"
proof (rule pmf_rev_mono)
fix ψ assume "ψ ∈ set_pmf (sample_pmf Ψ)"
obtain f g h where ψ_def: "ψ = (f,g,h)" by (metis prod_cases3)
assume "ψ ∉ {ψ. ¬ E⇩1 ψ ∨ ¬ E⇩2 ψ ∨ ¬ E⇩3 ψ ∨ ¬ E⇩4 ψ}"
hence assms: "E⇩1 (f,g,h)" "E⇩2 (f,g,h)" "E⇩3 (f,g,h)" "E⇩4 (f,g,h)"
unfolding ψ_def by auto
define I :: "real set" where "I = {0..59/90*b}"
have "p (f,g,h) ≤ ρ (card (R f)) + ε/12 * card (R f)"
using assms(4) E⇩4_def unfolding abs_le_iff by simp
also have "... ≤ ρ(2/3*b) + 1/12* (2/3*b)"
using ε_lt_1 R_bound[OF assms(1,2)]
by (intro add_mono rho_mono mult_mono) auto
also have "... ≤ 3/5 * b + 1/18*b"
by (intro add_mono rho_two_thirds) auto
also have "... ≤ 59/90 * b"
by simp
finally have "p (f,g,h) ≤ 59/90 * b" by simp
hence p_in_I: "p (f,g,h) ∈ I"
unfolding I_def by simp
have "ρ (card (R f)) ≤ ρ(2/3 * b)"
using R_bound[OF assms(1,2)]
by (intro rho_mono) auto
also have "... ≤ 3/5 * b"
using rho_two_thirds by simp
also have "... ≤ b * 59/90" by simp
finally have "ρ (card (R f)) ≤ b * 59/90" by simp
moreover have "(1 - 1 / real b) powr (real (card (R f))) ≤ 1 powr (real (card (R f)))"
using b_min by (intro powr_mono2) auto
hence "ρ (card (R f)) ≥ 0"
unfolding ρ_def by (intro mult_nonneg_nonneg) auto
ultimately have "ρ (card (R f)) ∈ I"
unfolding I_def by simp
moreover have "interval I"
unfolding I_def interval_def by simp
moreover have "59 / 90 * b < b"
using b_min by simp
hence "DERIV ρ_inv x :> ρ_inv' x" if "x ∈ I" for x
using that I_def by (intro ρ_inv') simp
ultimately obtain ξ :: real where ξ_def: "ξ ∈ I"
"ρ_inv (p(f,g,h)) - ρ_inv (ρ (card (R f))) = (p (f,g,h) - ρ(card (R f))) * ρ_inv' ξ"
using p_in_I MVT_interval by blast
have "¦ρ_inv(p (f,g,h)) - card (R f)¦ = ¦ρ_inv(p (f,g,h)) - ρ_inv(ρ(card (R f)))¦"
by (subst ρ_inverse) simp
also have "... = ¦(p (f,g,h) - ρ (card (R f)))¦ * ¦ρ_inv' ξ ¦"
using ξ_def(2) abs_mult by simp
also have "... ≤ ¦p (f,g,h) - ρ (card (R f))¦ * 4"
using ξ_def(1) I_def
by (intro mult_left_mono ρ_inv'_bound) auto
also have "... ≤ ( ε/12 * card (R f)) * 4"
using assms(4) E⇩4_def by (intro mult_right_mono) auto
also have "... = ε/3 * card (R f)" by simp
finally have b: "¦ρ_inv(p (f,g,h)) - card (R f)¦ ≤ ε/3 * card (R f)" by simp
have "¦ρ_inv(p (f,g,h)) - X / 2 ^ (s f)¦ ≤
¦ρ_inv(p (f,g,h)) - card (R f)¦ + ¦card (R f) - X / 2 ^ (s f)¦"
by simp
also have "... ≤ ε/3 * card (R f) + ¦card (R f) - X / 2 ^ (s f)¦"
by (intro add_mono b) auto
also have "... = ε/3 * ¦X / 2 ^ (s f) + (card (R f) - X / 2 ^ (s f))¦ +
¦card (R f) - X / 2 ^ (s f)¦" by simp
also have "... ≤ ε/3 * (¦X / 2 ^ (s f)¦ + ¦card (R f) - X / 2 ^ (s f)¦) +
¦card (R f) - X / 2 ^ (s f)¦"
using ε_gt_0 by (intro mult_left_mono add_mono abs_triangle_ineq) auto
also have "... ≤ ε/3 * ¦X / 2 ^ (s f)¦ + (1+ ε/3) * ¦card (R f) - X / 2 ^ (s f)¦"
using ε_gt_0 ε_lt_1 by (simp add:algebra_simps)
also have "... ≤ ε/3 * ¦X / 2 ^ s f¦ + (4/3) * ( ε / 3 * real X / 2 ^ s f)"
using assms(2) ε_gt_0 ε_lt_1
unfolding E⇩2_def by (intro add_mono mult_mono) auto
also have "... = (7/9) * ε * real X / 2^s f"
using X_ge_1 by (subst abs_of_nonneg) auto
also have "... ≤ 1 * ε * real X / 2^s f"
using ε_gt_0 by (intro mult_mono divide_right_mono) auto
also have "... = ε * real X / 2^s f" by simp
finally have a:"¦ρ_inv(p (f,g,h)) - X / 2 ^ (s f)¦ ≤ ε * X / 2 ^ (s f)"
by simp
have "¦Y (f, g, h) - real X¦ = ¦2 ^ (s f)¦ * ¦ρ_inv(p (f,g,h)) - real X / 2 ^ (s f)¦"
unfolding Y_def by (subst abs_mult[symmetric]) (simp add:algebra_simps powr_add[symmetric])
also have "... ≤ 2 ^ (s f) * (ε * X / 2 ^ (s f))"
by (intro mult_mono a) auto
also have "... = ε * X"
by (simp add:algebra_simps powr_add[symmetric])
finally have "¦Y (f, g, h) - real X¦ ≤ ε * X" by simp
moreover have "2 powr (⌈log 2 (real X)⌉ - t f) ≤ 2 powr b_exp" (is "?L1 ≤ ?R1")
proof -
have "?L1 ≤ 2 powr (1 + log 2 (real X)- t f)"
by (intro powr_mono, linarith) auto
also have "... = 2 powr 1 * 2 powr (log 2 (real X)) * 2 powr (- t f)"
unfolding powr_add[symmetric] by simp
also have "... = 2 * (2 powr (-t f) * X)"
using X_ge_1 by simp
also have "... ≤ 2 * (b/2)"
using assms(1) unfolding E⇩1_def by (intro mult_left_mono) auto
also have "... = b" by simp
also have "... = ?R1"
unfolding b_def by (simp add: powr_realpow)
finally show ?thesis by simp
qed
hence "⌈log 2 (real X)⌉ - t f ≤ real b_exp"
unfolding not_less[symmetric] using powr_less_mono[where x="2"] by simp
hence "s f ≥ q_max" unfolding s_def q_max_def by (intro nat_mono) auto
ultimately show "ψ ∉ {(f, g, h). ε * X < ¦Y (f, g, h) - real X¦ ∨ s f < q_max}"
unfolding ψ_def by auto
qed
also have "... ≤
measure Ψ {ψ. ¬E⇩1 ψ ∨ ¬E⇩2 ψ ∨ ¬E⇩3 ψ} + measure Ψ {ψ. E⇩1 ψ ∧ E⇩2 ψ ∧ E⇩3 ψ ∧ ¬E⇩4 ψ}"
by (intro pmf_add) auto
also have "... ≤ (measure Ψ {ψ. ¬E⇩1 ψ ∨ ¬E⇩2 ψ} + measure Ψ {ψ. E⇩1 ψ ∧ E⇩2 ψ ∧ ¬E⇩3 ψ}) + 1/2^6"
by (intro add_mono e_4 pmf_add) auto
also have "... ≤ ((measure Ψ {ψ. ¬E⇩1 ψ} + measure Ψ {ψ. E⇩1 ψ ∧ ¬E⇩2 ψ}) + 1/2^6) + 1/2^6"
by (intro add_mono e_3 pmf_add) auto
also have "... ≤ ((1/2^6 + 1/2^6) + 1/2^6) + 1/2^6"
by (intro add_mono e_2 e_1) auto
also have "... = ?R" by simp
finally show ?thesis by simp
qed
end
end