Theory ApproxMCCoreAnalysis
section ‹ ApproxMCCore analysis ›
text ‹
This section analyzes ApproxMCCore with respect to a universal hash family.
The proof follows Lemmas 1 and 2 from Chakraborty et al.~\cite{DBLP:conf/ijcai/ChakrabortyMV16}.
›
theory ApproxMCCoreAnalysis imports
"HOL-Decision_Procs.Dense_Linear_Order"
ApproxMCCore
begin
definition Hslice :: "nat ⇒
('a assg ⇒ 'b ⇒ nat assg) ⇒ ('a assg ⇒ 'b ⇒ nat assg)"
where "Hslice i H = (λw s. aslice i (H w s))"
context prob_space
begin
lemma indep_vars_prefix:
assumes "indep_vars (λ_. count_space UNIV) H J"
shows "indep_vars (λ_. count_space UNIV) (Hslice i H) J"
proof -
have "indep_vars (λ_. count_space UNIV) (λy. (λx. aslice i x) ∘ H y) J"
by (auto intro!: indep_vars_compose[OF assms(1)])
thus ?thesis
unfolding o_def Hslice_def
by auto
qed
lemma assg_nonempty_dom:
shows "
(λx. if x < i then Some True else None) ∈
{α::nat assg. dom α = {0..<i}}"
by (auto split: if_splits)
lemma card_dom_ran_nat_assg:
shows "card {α::nat assg. dom α = {0..<n}} = 2^n"
proof -
have *: " {α::nat assg. dom α = {0..<n}} =
{w. dom w = {0..<n} ∧ ran w ⊆ {True,False}}"
by auto
have "finite {0..<n}" by auto
from card_dom_ran[OF this]
have "card {w. dom w = {0..<n} ∧ ran w ⊆ {True,False}} =
card {True,False} ^ card {0..<n}" .
thus ?thesis
unfolding *
by (auto simp add: numeral_2_eq_2)
qed
lemma card_nat_assg_le:
assumes "i ≤ n"
shows "card {α::nat assg. dom α = {0..<n}} =
2^(n-i) * card {α::nat assg. dom α = {0..<i}}"
unfolding card_dom_ran_nat_assg
by (metis assms le_add_diff_inverse mult.commute power_add)
lemma empty_nat_assg_slice_notin:
assumes "i ≤ n"
assumes "dom β ≠ {0..<i}"
shows"{α::nat assg. dom α = {0..<n} ∧ aslice i α = β} = {}"
proof (intro equals0I)
fix x
assume "x ∈ {α. dom α = {0..<n} ∧ aslice i α = β}"
then have "dom β = {0..<i}"
unfolding aslice_def
using assms(1) by force
thus False using assms(2) by blast
qed
lemma restrict_map_dom:
shows "α |` dom α = α"
unfolding restrict_map_def fun_eq_iff
by (simp add: domIff)
lemma aslice_refl:
assumes "dom α = {..<i}"
shows "aslice i α = α"
unfolding aslice_def assms[symmetric]
using restrict_map_dom by auto
lemma bij_betw_with_inverse:
assumes "f ` A ⊆ B"
assumes "⋀x. x ∈ A ⟹ g (f x) = x"
assumes "g ` B ⊆ A"
assumes "⋀x. x ∈ B ⟹ f (g x) = x"
shows "bij_betw f A B"
proof -
have "inj_on f A"
by (metis assms(2) inj_onI)
thus ?thesis
unfolding bij_betw_def
using assms
by (metis image_subset_iff subsetI subset_antisym)
qed
lemma card_nat_assg_slice:
assumes "i ≤ n"
assumes "dom β = {0..<i}"
shows"card {α::nat assg. dom α = {0..<n} ∧ aslice i α = β} =
2 ^ (n-i)"
proof -
have "dom α = {0..<i} ∧ aslice i α = β ⟷ α = β" for α
using aslice_refl
by (metis assms(2) lessThan_atLeast0)
then have r2:
"{α::nat assg. dom α = {0..<i} ∧ aslice i α = β} = {β}"
by simp
define f where "f =
(λ(α::nat assg,β::nat assg) j.
if j < i then β j else α (j-i))"
let ?lhs = "({α. dom α = {0..<n - i}} ×
{α. dom α = {0..<i} ∧ aslice i α = β})"
let ?rhs = "{α::nat assg. dom α = {0..<n} ∧ aslice i α = β}"
define finv where "finv =
(λfab::nat assg.
((λj. fab (j + i)),
fab |` {..<i})
)"
have 11: "⋀x. dom (f x) = {j. if j < i then j ∈ dom (snd x) else j - i ∈ dom (fst x)}"
unfolding f_def
by (auto simp add: fun_eq_iff split: if_splits)
have 1: " f ` ?lhs ⊆ ?rhs"
proof standard
fix x
assume x: "x ∈ f ` ({α. dom α = {0..<n - i}} × {α. dom α = {0..<i} ∧ aslice i α = β})"
obtain a b where ab: "dom a = {0..<n - i}" "dom b = {0..<i}"
"x = f (a,b)"
using x by blast
have 1: "dom x = {0..<n}"
unfolding ab 11 using assms(1)
by (auto simp add: ab)
have 2: "aslice i x = β"
using x unfolding f_def
by (auto simp add: aslice_def restrict_map_def split: if_splits)
show " x ∈ {α. dom α = {0..<n} ∧ aslice i α = β}"
using 1 2 by blast
qed
have " dom a = {0..<n - i} ⟹
dom b = {0..<i} ⟹
∀x. aslice i b x = β x ⟹
¬ x < i ⟹ None = b x" for a b :: "nat assg" and x
by (metis atLeastLessThan_iff domIff)
then have 2: "⋀x. x ∈ ?lhs ⟹ finv (f x) = x"
unfolding finv_def f_def
by (clarsimp simp add: fun_eq_iff restrict_map_def)
have 31: "⋀fab x y.
dom fab = {0..<n} ⟹
β = aslice i fab ⟹
fab (x + i) = Some y ⟹
x < n - i"
by (metis atLeastLessThan_iff domI less_diff_conv)
also have "⋀fab x.
dom fab = {0..<n} ⟹
β = aslice i fab ⟹
x < i ⟹ ∃y. fab x = Some y"
by (metis assms(1) domD dual_order.trans lessThan_atLeast0 lessThan_iff linorder_not_less)
ultimately have 3: "finv ` ?rhs ⊆ ?lhs"
unfolding finv_def
by (auto simp add: aslice_def split: if_splits)
have 4: "⋀x. x ∈ ?rhs ⟹ f (finv x) = x"
unfolding finv_def f_def
by (auto simp add: fun_eq_iff restrict_map_def)
have "bij_betw f ?lhs ?rhs"
by (auto intro: bij_betw_with_inverse[OF 1 2 3 4])
from bij_betw_same_card[OF this]
have
"card {α::nat assg. dom α = {0..<n} ∧ aslice i α = β} =
card ({α::nat assg. dom α = {0..<n-i}} ×
{α::nat assg. dom α = {0..<i} ∧ aslice i α = β})"
by auto
moreover have "... = 2^(n-i)"
using r2 card_dom_ran_nat_assg
by (simp add: card_cartesian_product)
ultimately show ?thesis by auto
qed
lemma finite_dom:
assumes "finite V"
shows "finite {w :: 'a ⇀ bool. dom w = V}"
proof -
have *: "{w :: 'a ⇀ bool. dom w = V} =
{w. dom w = V ∧ ran w ⊆ {True,False}}"
by auto
show ?thesis unfolding *
apply (intro finite_set_of_finite_maps)
using assms by auto
qed
lemma universal_prefix_family_from_hash:
assumes M: "M = measure_pmf p"
assumes kH: "k_universal k H D {α::nat assg. dom α = {0..<n}}"
assumes i: "i ≤ n"
shows "k_universal k (Hslice i H) D {α. dom α = {0..<i}}"
proof -
have "k_wise_indep_vars k (λ_. count_space UNIV) H D"
using kH unfolding k_universal_def
by auto
then have 1: "k_wise_indep_vars k (λ_. count_space UNIV) (Hslice i H) D"
unfolding k_wise_indep_vars_def
using indep_vars_prefix
by auto
have fdom: "finite {α::nat assg. dom α = {0..<i}}"
using measure_pmf.finite_dom by blast
have nempty: "{α::nat assg. dom α = {0..<i}} ≠ {}"
using assg_nonempty_dom
by (metis empty_iff)
have 2: "x ∈ D ⟹
uniform_on (Hslice i H x) {α. dom α = {0..<i}}" for x
proof -
assume "x ∈ D"
then have unif: "uniform_on (H x) {α. dom α = {0..<n}}"
by (metis kH k_universal_def)
show "uniform_on (Hslice i H x) {α. dom α = {0..<i}}"
proof (intro uniform_onI[OF M fdom nempty])
fix β
have *: "{ω ∈ space M. H x ω ∈ {α. aslice i α = β}} =
{ω. Hslice i H x ω = β}"
unfolding Hslice_def
by (auto simp add: M)
have "{α::nat assg. dom α = {0..<n}} ∩ {α. aslice i α = β} =
{α::nat assg. dom α = {0..<n} ∧ aslice i α = β}"
by auto
then have "(card ({α::nat assg. dom α = {0..<n}} ∩ {α. aslice i α = β}))
= (if dom β = {0..<i} then 2^(n-i) else 0)"
using card_nat_assg_slice[OF i]
by (simp add: empty_nat_assg_slice_notin i)
then have **: "real (card ({α::nat assg. dom α = {0..<n}} ∩ {α. aslice i α = β}))
= indicat_real {α. dom α = {0..<i}} β * 2^(n-i)"
by simp
from uniform_onD[OF unif, of "{α. aslice i α = β}"]
have "prob {ω. Hslice i H x ω = β} =
real (card ({α. dom α = {0..<n}} ∩ {α. aslice i α = β})) /
real (card {α::nat assg. dom α = {0..<n}})"
unfolding * by auto
moreover have "... =
indicat_real {α. dom α = {0..<i}} β * 2^(n-i) /
real (card {α::nat assg. dom α = {0..<n}})"
unfolding ** by auto
moreover have "... = indicat_real {α. dom α = {0..<i}} β * 2^(n-i) / 2^n"
by (simp add: card_dom_ran_nat_assg)
moreover have "... = indicat_real {α. dom α = {0..<i}} β / 2^i"
by (simp add: i power_diff)
moreover have "... = indicat_real {α. dom α = {0..<i}} β / real ((2^i)::nat)" by auto
moreover have "... = indicat_real {α. dom α = {0..<i}} β / real (card {α::nat assg. dom α = {0..<i}})"
using card_dom_ran_nat_assg
by auto
ultimately show "prob {ω. Hslice i H x ω = β} =
indicat_real {α. dom α = {0..<i}} β /
real (card {α::nat assg. dom α = {0..<i}})"
by presburger
qed
qed
show ?thesis
unfolding k_universal_def
using 1 2
by blast
qed
end
context ApproxMCCore
begin
definition pivot :: "real"
where "pivot = 9.84 * ( 1 + 1 / ε )^2"
context
assumes thresh: "thresh ≥ (1 + ε / (1 + ε)) * pivot"
begin
lemma aux_1:
assumes fin:"finite (set_pmf p)"
assumes σ: "σ > 0"
assumes exp: "μ i = measure_pmf.expectation p Y"
assumes var: "σ^2 = measure_pmf.variance p Y"
assumes var_bound: "σ^2 ≤ μ i"
shows "
measure_pmf.prob p {y. ¦ Y y - μ i ¦ ≥ ε / (1 + ε) * μ i }
≤ (1 + ε)^2 / (ε^2 * μ i) "
proof -
have pvar: "measure_pmf.variance p Y > 0"
using var σ
by (metis zero_less_power)
have kmu: "ε * (μ i) / ((1 + ε) * σ) > 0"
using σ pvar var var_bound
using ε by auto
have mupos: "μ i > 0"
using pvar var var_bound by linarith
from spec_chebyshev_inequality [OF fin pvar kmu]
have "measure_pmf.prob p
{y. (Y y - measure_pmf.expectation p Y)^2 ≥
(ε * (μ i) / ((1 + ε) * σ))^2 * measure_pmf.variance p Y} ≤ 1 / (ε * (μ i) / ((1 + ε) * σ))^2"
by simp
then have ineq1:"measure_pmf.prob p
{y. (Y y - μ i)^2 ≥
(ε * (μ i) / ((1 + ε) * σ))^2 * σ^2} ≤ 1 / (ε * (μ i) / ((1 + ε) * σ))^2"
using exp var by simp
have "(λy. (Y y - μ i)^2 ≥ (ε * (μ i) / ((1 + ε) * σ))^2 * σ^2)
= (λy. (Y y - μ i)^2 ≥ (ε * (μ i) / ((1 + ε) * σ) * σ )^2)"
by (metis power_mult_distrib)
moreover have "... = (λy. ¦ Y y - μ i ¦ ≥ ε * (μ i) / ((1 + ε) * σ) * σ)"
proof -
have "0 ≤ ε * μ i / (1 + ε)"
by (simp add: ε less_eq_real_def mupos zero_compare_simps(1))
then show ?thesis
apply clarsimp
by (metis abs_le_square_iff abs_of_nonneg)
qed
moreover have "... = (λy. ¦ Y y - μ i ¦ ≥ ε * (μ i) / (1 + ε))"
using σ by auto
ultimately have simp1:"(λy. (Y y - μ i)^2 ≥ (ε * (μ i) / ((1 + ε) * σ))^2 * σ^2)
= (λy. ¦ Y y - μ i ¦ ≥ ε / (1 + ε) * (μ i))"
by auto
have "σ^2/(μ i)^2 ≤ (μ i)/(μ i)^2"
using var_bound μ_gt_zero
by (simp add: divide_right_mono)
moreover have "... = 1 / (μ i)"
by (simp add: power2_eq_square)
ultimately have simp2: "σ^2/(μ i)^2 ≤ 1 / (μ i)" by auto
have "measure_pmf.prob p {y. ¦ Y y - μ i ¦ ≥ ε / (1 + ε) * (μ i)}
≤ 1 / (ε * (μ i) / ((1 + ε) * σ))^2"
using ineq1 simp1
by auto
moreover have "... = (1 + ε)^2 / ε^2 * σ^2/(μ i)^2"
by (simp add: power_divide power_mult_distrib)
moreover have "... ≤ (1 + ε)^2 / ε^2 * (1 / (μ i))"
using simp2
by (smt (verit, best) ε divide_pos_pos mult_left_mono times_divide_eq_right zero_less_power)
ultimately have "measure_pmf.prob p {y. ¦ Y y - μ i ¦ ≥ ε / (1 + ε) * (μ i)}
≤ (1 + ε)^2 / (ε^2 * (μ i))"
by auto
thus ?thesis by auto
qed
lemma analysis_1_1:
assumes p: "finite (set_pmf p)"
assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
{α::'a assg. dom α = S}
{α::nat assg. dom α = {0..<card S - 1}}"
assumes i: "i ≤ card S - 1"
shows "
measure_pmf.prob p
{s. ¦ card_slice ((λw. H w s)) i - μ i ¦ ≥ ε / (1 + ε) * μ i}
≤ (1 + ε)^2 / (ε^2 * μ i)"
proof -
define var where "var =
(λi. measure_pmf.variance p
(λs. real (card (proj S W ∩
{w. Hslice i H w s = aslice i α}))))"
from prob_space.universal_prefix_family_from_hash[OF _ _ ind]
have hf: "prob_space.k_universal (measure_pmf p) 2
(Hslice i H) {α::'a assg. dom α = S} {α. dom α = {0..<i}}"
using prob_space_measure_pmf
using i ind prob_space.universal_prefix_family_from_hash
by blast
have pSW: "proj S W ⊆ {α. dom α = S}"
unfolding proj_def restr_def by (auto split:if_splits)
have ain: "aslice i α ∈ {α. dom α = {0..<i}}" using α
unfolding aslice_def using i by auto
from k_universal_expectation_eq[OF p hf finite_proj_S pSW ain]
have exp:"measure_pmf.expectation p
(λs. real (card (proj S W ∩
{w. Hslice i H w s = aslice i α}))) =
real (card (proj S W)) /
real (card {α::nat assg. dom α = {0..<i}})" .
have exp_mu:"real (card (proj S W)) /
real (card {α::nat assg. dom α = {0..<i}}) = μ i"
unfolding μ_def
by (simp add: measure_pmf.card_dom_ran_nat_assg)
have "proj S W ∩
{w. Hslice i H w s = aslice i α} =
proj S W ∩ {w. hslice i (λw. H w s) w = aslice i α}" for s
unfolding proj_def Hslice_def hslice_def
by auto
then have extend_card_slice:
"⋀s. (card (proj S W ∩ {w. Hslice i H w s = aslice i α})) =
card_slice ((λw. H w s)) i"
unfolding card_slice_def by auto
have mu_exp:" μ i = measure_pmf.expectation p
(λs. real (card (proj S W ∩ {w. Hslice i H w s = aslice i α})))"
using exp exp_mu by auto
from two_universal_variance_bound[OF p hf finite_proj_S pSW ain]
have "
var i ≤
measure_pmf.expectation p
(λs. real (card (proj S W ∩
{w. Hslice i H w s = aslice i α})))"
unfolding var_def .
then have var_bound: "var i ≤ μ i" using exp exp_mu
by linarith
have "var i ≥ 0" unfolding var_def by auto
then have "var i > 0 ∨ var i = 0" by auto
moreover {
assume "var i = 0"
then have 1: "
measure_pmf.expectation p
(λs. (card_slice (λw. H w s) i - μ i)^2) = 0"
unfolding var_def extend_card_slice mu_exp by auto
have 2: "measure_pmf.expectation p
(λs. (card_slice (λw. H w s) i - μ i)^2) =
sum (λs. (card_slice (λw. H w s) i - μ i)^2 * pmf p s) (set_pmf p)"
using assms by (auto intro!: integral_measure_pmf_real)
have "∀x ∈ set_pmf p. (card_slice (λw. H w x) i - μ i)^2 * pmf p x = 0"
apply (subst sum_nonneg_eq_0_iff[symmetric])
using 1 2 p by auto
then have *: "⋀x. x ∈ set_pmf p ⟹ (card_slice (λw. H w x) i - μ i)^2 = 0"
by (meson mult_eq_0_iff set_pmf_iff)
have **: "(1 + ε)^2 / (ε^2 * μ i) > 0"
using μ_gt_zero ε by auto
have "ε / (1 + ε) * μ i > 0"
using μ_gt_zero ε by auto
then have "⋀s. s ∈ set_pmf p ⟹ ¦ card_slice ((λw. H w s)) i - μ i ¦ < ε / (1 + ε) * μ i"
using * by auto
then have "
measure_pmf.prob p
{s. ¦ card_slice ((λw. H w s)) i - μ i ¦ ≥ ε / (1 + ε) * μ i } = 0"
apply (subst measure_pmf_zero_iff)
using linorder_not_less by auto
then have "
measure_pmf.prob p
{s. ¦ card_slice ((λw. H w s)) i - μ i ¦ ≥ ε / (1 + ε) * μ i }
≤ (1 + ε)^2 / (ε^2 * μ i)"
using ** by auto
}
moreover {
define sigma where "sigma = sqrt(var i)"
assume "var i > 0"
then have sigma_gt_0: "sigma > 0"
unfolding sigma_def by simp
have extend_sigma: "sigma^2 = measure_pmf.variance p
(λs. real (card (proj S W ∩
{w. Hslice i H w s = aslice i α})))"
unfolding sigma_def var_def
using less_eq_real_def local.var_def real_sqrt_pow2 sigma_def sigma_gt_0
by fastforce
have sigma_bound: "sigma^2 ≤ μ i"
using var_bound sigma_gt_0
using sigma_def by force
from aux_1[OF p sigma_gt_0 mu_exp extend_sigma sigma_bound]
have "
measure_pmf.prob p
{s. ¦ card_slice ((λw. H w s)) i - μ i ¦ ≥ ε / (1 + ε) * μ i }
≤ (1 + ε)^2 / (ε^2 * μ i)"
using extend_card_slice by auto
}
ultimately show ?thesis by auto
qed
lemma analysis_1_2:
assumes p: "finite (set_pmf p)"
assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
{α::'a assg. dom α = S}
{α::nat assg. dom α = {0..<card S - 1}}"
assumes i: "i ≤ card S - 1"
assumes β: "β ≤ 1"
shows "measure_pmf.prob p
{s. real(card_slice ((λw. H w s)) i) ≤ β * μ i }
≤ 1 / (1 + (1 - β)^2 * μ i)"
proof -
have *: "(⋀s. (0::real) ≤ card_slice ((λw. H w s)) i)"
by simp
from spec_paley_zygmund_inequality[OF p * β]
have paley_zigmund:
"(measure_pmf.variance p (λs. real(card_slice ((λw. H w s)) i) )
+ (1-β)^2 * (measure_pmf.expectation p (λs. card_slice ((λw. H w s)) i))^2) *
measure_pmf.prob p {s. real(card_slice ((λw. H w s)) i) > β * measure_pmf.expectation p (λs. real(card_slice ((λw. H w s)) i) )} ≥
(1-β)^2 * (measure_pmf.expectation p (λs. real(card_slice ((λw. H w s)) i) ))^2"
by auto
define var where "var = (λi. measure_pmf.variance p
(λs. real (card (proj S W ∩
{w. Hslice i H w s = aslice i α}))))"
from prob_space.universal_prefix_family_from_hash[OF _ _ ind]
have hf: "prob_space.k_universal (measure_pmf p) 2
(Hslice i H) {α::'a assg. dom α = S} {α. dom α = {0..<i}}"
using prob_space_measure_pmf
using i ind prob_space.universal_prefix_family_from_hash
by blast
have pSW: "proj S W ⊆ {α. dom α = S}"
unfolding proj_def restr_def
by (auto split:if_splits)
have ain: "aslice i α ∈ {α. dom α = {0..<i}}" using α
unfolding aslice_def using i by auto
from k_universal_expectation_eq[OF p hf finite_proj_S pSW ain]
have exp:"measure_pmf.expectation p
(λs. real (card (proj S W ∩
{w. Hslice i H w s = aslice i α}))) =
real (card (proj S W)) /
real (card {α::nat assg. dom α = {0..<i}})" .
have exp_mu:"real (card (proj S W)) /
real (card {α::nat assg. dom α = {0..<i}}) = μ i"
unfolding μ_def
by (simp add: measure_pmf.card_dom_ran_nat_assg)
have "proj S W ∩
{w. Hslice i H w s = aslice i α} =
proj S W ∩ {w. hslice i (λw. H w s) w = aslice i α}" for s
unfolding proj_def Hslice_def hslice_def
by auto
then have extend_card_slice:"⋀s. (card (proj S W ∩
{w. Hslice i H w s = aslice i α})) =
card_slice ((λw. H w s)) i"
unfolding card_slice_def by auto
have mu_exp:" μ i = measure_pmf.expectation p
(λs. real (card (proj S W ∩
{w. Hslice i H w s = aslice i α})))"
using exp exp_mu by auto
from two_universal_variance_bound[OF p hf finite_proj_S pSW ain]
have "
var i ≤
measure_pmf.expectation p
(λs. real (card (proj S W ∩
{w. Hslice i H w s = aslice i α})))"
unfolding var_def .
then have var_bound: "var i ≤ μ i" using exp exp_mu
by linarith
have pos_mu: "μ i > 0"
unfolding μ_def
by (simp add: card_proj_witnesses)
have comp: "measure_pmf.prob p
{s. β * μ i < real (card_slice (λw. H w s) i)} =
(1 - measure_pmf.prob p {s. real(card_slice ((λw. H w s)) i) ≤ β * μ i})"
apply (subst measure_pmf.prob_compl[symmetric])
by (auto intro!: arg_cong[where f = "measure_pmf.prob p"])
have extend_var_bound: "measure_pmf.variance p (λs. card_slice ((λw. H w s)) i) ≤ μ i"
using var_bound
unfolding var_def
by (simp add: extend_card_slice)
then have
"(measure_pmf.variance p (λs. real(card_slice ((λw. H w s)) i))
+ (1-β)^2 * (measure_pmf.expectation p (λs. real(card_slice ((λw. H w s)) i) ) )^2)
* measure_pmf.prob p {s. real(card_slice ((λw. H w s)) i) > β * measure_pmf.expectation p (λs. real(card_slice ((λw. H w s)) i) )} ≤
(μ i + (1-β)^2 * (measure_pmf.expectation p ( λs. real(card_slice ((λw. H w s)) i) ) )^2)
* measure_pmf.prob p
{s. real(card_slice ((λw. H w s)) i) > β * measure_pmf.expectation p (λs. real(card_slice ((λw. H w s)) i) )}"
by (auto intro!: mult_right_mono)
moreover have
"... ≤ (μ i + (1-β)^2 * (measure_pmf.expectation p ( λs. real(card_slice ((λw. H w s)) i) ) )^2)
* measure_pmf.prob p
{s. real(card_slice ((λw. H w s)) i) > β * measure_pmf.expectation p (λs. real(card_slice ((λw. H w s)) i) )}"
by fastforce
ultimately have
"(μ i + (1-β)^2 * (μ i)^2) * measure_pmf.prob p {s. real(card_slice ((λw. H w s)) i) > β * μ i} ≥ (1-β)^2 * (μ i)^2"
unfolding mu_exp extend_card_slice
using paley_zigmund by linarith
then have
"(1 + (1-β)^2 * (μ i)) * (μ i) * measure_pmf.prob p {s. real(card_slice ((λw. H w s)) i) > β * μ i} ≥ (1-β)^2 * (μ i) * (μ i)"
by (smt (verit) left_diff_distrib' more_arith_simps(11) mult_cancel_right mult_cancel_right2 power2_eq_square)
then have
"(1 + (1-β)^2 * (μ i)) * measure_pmf.prob p {s. real(card_slice ((λw. H w s)) i) > β * μ i} ≥ (1-β)^2 * (μ i)"
using pos_mu by force
then have
"(1 + (1-β)^2 * (μ i)) * (1 - measure_pmf.prob p {s. real(card_slice ((λw. H w s)) i) ≤ β * μ i}) ≥ (1-β)^2 * (μ i)"
using comp by auto
then have
"(1 + (1-β)^2 * (μ i)) - (1 + (1-β)^2 * (μ i)) * measure_pmf.prob p {s. real(card_slice ((λw. H w s)) i) ≤ β * μ i} ≥ (1-β)^2 * (μ i)"
by (simp add: right_diff_distrib)
then have
"(1 + (1-β)^2 * (μ i)) * measure_pmf.prob p {s. real(card_slice ((λw. H w s)) i) ≤ β * μ i} ≤ 1"
by simp
thus ?thesis by (smt (verit, best) mult_nonneg_nonneg nonzero_mult_div_cancel_left pos_mu real_divide_pos_left zero_le_power2)
qed
lemma shift_μ:
assumes "k ≤ i"
shows"μ i * 2^k = μ (i-k)"
unfolding μ_def
by (auto simp add: assms power_diff)
lemma analysis_2_1:
assumes p: "finite (set_pmf p)"
assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
{α::'a assg. dom α = S}
{α::nat assg. dom α = {0..<card S - 1}}"
assumes ε_up: "ε ≤ 1"
shows "
measure_pmf.prob (map_pmf (λs w. H w s) p) (T (mstar-3))
≤ 1 / 62.5"
proof -
have "1 + 1 / ε > 0"
by (simp add: ε pos_add_strict)
then have pos_pivot: "pivot > 0"
unfolding pivot_def
by simp
have "mstar ≥ 4 ∨ mstar < 4" by auto
moreover {
assume "mstar < 4"
then have " measure_pmf.prob (map_pmf (λs w. H w s) p) (T (mstar-3))
≤ 1 / 62.5"
by (auto simp add: T0_empty)
}
moreover {
assume lo_mstar: "mstar ≥ 4"
have extend_mu3: "μ (mstar-1) * 2^2 = μ (mstar-3)"
apply (subst shift_μ)
subgoal using lo_mstar by linarith
using numeral_3_eq_3
using Suc_1 diff_Suc_eq_diff_pred numeral_nat(7) by presburger
have ******: "1 + ε / (1 + ε) ≤ 3 / 2"
using ε assms(3) by auto
have mu_mstar_3_gt_zero: "μ (mstar - 3) / 4 > 0"
using μ_gt_zero by simp
from mstar_prop(1)
have "thresh < μ (mstar - 1) *2^2 / 4 * (1 + ε / (1 + ε))"
by auto
also have "... = μ (mstar - 3) / 4 * (1 + ε / (1 + ε))"
unfolding extend_mu3 by auto
also have "... ≤ μ (mstar - 3) / 4 * (3 / 2)"
apply (intro mult_left_mono)
using ****** mu_mstar_3_gt_zero by auto
also have "... = 3 / 8 * μ (mstar - 3)"
by auto
finally have thresh2mu: "thresh < 3 / 8 * μ (mstar - 3)" .
have "1 + ε / (1 + ε) > 0"
by (simp add: add_nonneg_pos ε)
then have "μ (mstar-1) > pivot"
using mstar_prop(1) thresh
by (smt (verit) nonzero_mult_div_cancel_right real_divide_pos_left)
then have lo_mu_mstar_3: "μ (mstar-3) > 4*pivot"
using extend_mu3
by simp
have mstar_3: "mstar-3 ≤ card S - 1"
using lo_mstar
using diff_le_self dual_order.trans mstar_prop(3) by blast
have *: "(5 / 8)^2 = ((25 / 64)::real)"
by (auto simp add: field_simps)
have **: " 1 + 25/64 * 4*pivot ≤ 1+ 25 / 64 * μ (mstar - 3) "
using lo_mu_mstar_3
by auto
have "1 + 1/ε ≥ 2"
by (simp add: ε assms(3))
then have "(1 + 1/ε)^2 ≥ 2^2"
by (smt (verit) power_mono)
then have ***: " 1 + 25/64 * 4 * 4*9.84 ≤ 1+ 25 / 64 * 4*pivot"
unfolding pivot_def
by auto
have ****: "1 + 25/64 * 4 * 4*9.84 > (0::real)"
by simp
have "measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 3)) ≤
3 / 8 * μ (mstar - 3)}
≤ 1 / (1 + (1 - 3 / 8)⇧2 * μ (mstar - 3))"
apply(intro analysis_1_2[OF p ind mstar_3])
by auto
also have "... = 1 / (1 + (5 / 8)^2 * μ (mstar-3))"
by simp
also have "... = 1 / (1 + 25 / 64 * μ (mstar-3))"
unfolding * by auto
also have "... ≤ 1 / (1+ 25/64 * 4*pivot)"
using **
by (metis Groups.add_ac(2) add_sign_intros(3) divide_nonneg_nonneg frac_le mult_right_mono mult_zero_left of_nat_0_le_iff of_nat_numeral order_le_less pos_pivot zero_less_one)
also have "... ≤ 1 / (1+ 25/64 * 4 * 4*9.84)"
using *** ****
by (smt (verit) frac_le)
also have "... ≤ 1 / 62.5"
by simp
finally have *****: "measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 3)) ≤ 3 / 8 * μ (mstar - 3)} ≤ 1 / 62.5"
by auto
have "measure_pmf.prob (map_pmf (λs w. H w s) p) (T (mstar-3))
= measure_pmf.prob p {s. real (card_slice (λw. H w s) (mstar - 3)) < thresh}"
unfolding T_def
by auto
also have "... ≤ measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 3)) ≤ 3 / 8 * μ (mstar - 3)}"
using thresh2mu by (auto intro!: measure_pmf.finite_measure_mono)
also have "... ≤ 1 / 62.5"
using *****
by auto
finally have "measure_pmf.prob (map_pmf (λs w. H w s) p) (T (mstar-3)) ≤ 1 / 62.5" .
}
ultimately show ?thesis by auto
qed
lemma analysis_2_1':
assumes p: "finite (set_pmf p)"
assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
{α::'a assg. dom α = S}
{α::nat assg. dom α = {0..<card S - 1}}"
shows "
measure_pmf.prob (map_pmf (λs w. H w s) p) (T (mstar-3))
≤ 1 / 10.84"
proof -
have "1 + 1 / ε > 0"
by (simp add: ε pos_add_strict)
then have pos_pivot: "pivot > 0"
unfolding pivot_def
by simp
have "mstar ≥ 4 ∨ mstar < 4" by auto
moreover {
assume "mstar < 4"
then have " measure_pmf.prob (map_pmf (λs w. H w s) p) (T (mstar-3))
≤ 1 / 10.84"
by (auto simp add: T0_empty)
}
moreover {
assume lo_mstar: "mstar ≥ 4"
have extend_mu3: "μ (mstar-1) * 2^2 = μ (mstar-3)"
apply (subst shift_μ)
subgoal using lo_mstar semiring_norm(87) by linarith
using diff_Suc_eq_diff_pred eval_nat_numeral(3) by presburger
have "ε / (1 + ε) < 1"
using ε by auto
then have ******: "1 + ε / (1 + ε) < 2"
using ε by auto
have mu_mstar_3_gt_zero: "μ (mstar - 3) / 4 > 0"
using μ_gt_zero by simp
from mstar_prop(1)
have "thresh < μ (mstar - 1) * (1 + ε / (1 + ε))"
by auto
also have "... = μ (mstar - 1) *2^2 / 4 * (1 + ε / (1 + ε))"
by auto
also have "... = μ (mstar - 3) / 4 * (1 + ε / (1 + ε))"
unfolding extend_mu3 by auto
also have "... < μ (mstar - 3) / 4 * 2"
apply (intro mult_strict_left_mono)
using ****** mu_mstar_3_gt_zero by auto
also have "... = 1 / 2 * μ (mstar - 3)"
by auto
finally have thresh2mu: "thresh < 1 / 2 * μ (mstar - 3)" .
have "1 + ε / (1 + ε) > 0"
by (simp add: add_nonneg_pos ε)
then have "μ (mstar-1) * 4 > 4*pivot"
using mstar_prop(1) thresh
by (smt (verit) nonzero_mult_div_cancel_right real_divide_pos_left)
then have lo_mu_mstar_3: "μ (mstar-3) > 4*pivot"
using extend_mu3
by simp
have mstar_3: "mstar-3 ≤ card S - 1"
using lo_mstar
using diff_le_self dual_order.trans mstar_prop(3) by blast
have *: "(1 / 2)^2 = ((1 / 4)::real)"
by (auto simp add: field_simps)
have **: " 1 + 1/4 * 4*pivot ≤ 1+ 1/4 * μ (mstar - 3) "
using lo_mu_mstar_3
by auto
have "(1 + 1/ε)^2 > 1^2"
by (simp add: ε)
then have ***: " 1 + 1/4 * 4*9.84 ≤ 1+ 1/4 * 4 *pivot"
unfolding pivot_def by auto
have ****: "1 + 1/4 * 4 * 9.84 > (0::real)"
by simp
have "measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 3)) ≤
1 / 2 * μ (mstar - 3)}
≤ 1 / (1 + (1 - 1 / 2)⇧2 * μ (mstar - 3))"
apply(intro analysis_1_2[OF p ind mstar_3])
by auto
also have "... = 1 / (1 + 1 / 4 * μ (mstar-3))"
using * by force
also have "... ≤ 1 / (1+ 1/4 * 4*pivot)"
using **
by (simp add: add_nonneg_pos frac_le pos_pivot)
also have "... ≤ 1 / (1+ 1/4 * 4 *9.84)"
using *** ****
by (smt (verit) frac_le)
also have "... ≤ 1 / 10.84"
by simp
finally have *****: "measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 3)) ≤ 1/2 * μ (mstar - 3)} ≤ 1 / 10.84" .
have "measure_pmf.prob (map_pmf (λs w. H w s) p) (T (mstar-3))
= measure_pmf.prob p {s. real (card_slice (λw. H w s) (mstar - 3)) < thresh}"
unfolding T_def
by auto
also have "... ≤ measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 3)) ≤ 1 / 2 * μ (mstar - 3)}"
using thresh2mu by (auto intro!: measure_pmf.finite_measure_mono)
also have "... ≤ 1 / 10.84"
using *****
by auto
finally have "measure_pmf.prob (map_pmf (λs w. H w s) p) (T (mstar-3)) ≤ 1 / 10.84" .
}
ultimately show ?thesis by auto
qed
lemma analysis_2_2:
assumes p: "finite (set_pmf p)"
assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
{α::'a assg. dom α = S}
{α::nat assg. dom α = {0..<card S - 1}}"
shows "
measure_pmf.prob (map_pmf (λs w. H w s) p) (L (mstar-2)) ≤ 1 / 20.68"
proof -
have epos: "1 + 1 / ε > 0"
by (simp add: ε pos_add_strict)
then have pos_pivot: "pivot > 0"
unfolding pivot_def
by simp
have "mstar ≥ 3 ∨ mstar < 3" by auto
moreover {
assume "mstar < 3"
then have " measure_pmf.prob (map_pmf (λs w. H w s) p) (L (mstar-2))
≤ 1 / 20.68"
by (auto simp add: L0_empty)
}
moreover {
assume lo_mstar: "mstar ≥ 3"
have extend_mu2: "μ (mstar-1) * 2^1 = μ (mstar-2)"
apply (subst shift_μ)
subgoal using lo_mstar by linarith
by (metis diff_diff_left one_add_one)
have "1 + ε / (1 + ε) > 0"
by (simp add: add_nonneg_pos ε)
then have "μ (mstar-1) > pivot"
using mstar_prop(1) thresh
by (smt (verit) nonzero_mult_div_cancel_right real_divide_pos_left)
then have lo_mu_mstar_2: "μ (mstar-2) > 2*pivot"
using extend_mu2
by simp
have mstar_2: "mstar-2 ≤ card S - 1"
using lo_mstar
using diff_le_self dual_order.trans mstar_prop(3) by blast
have beta:"1/(1+ε) ≤ (1::real)"
using ε by auto
have pos: "(1 / (1 + 1/ε))⇧2 > 0"
using epos by auto
then have *: "1 + (1 / (1 + 1/ε))⇧2 * 2*pivot ≤ 1 + (1 / (1 + 1/ε))⇧2 * μ (mstar - 2)"
using lo_mu_mstar_2
by auto
have "1 - 1/(1+ε) = 1 / (1 + 1/ε)"
by (smt (verit, ccfv_threshold) ε conjugate_exponent_def conjugate_exponent_real(1))
then have **: "(1 - 1/(1+ε))^2 = (1 / (1 + 1/ε))^2"
by simp
have ***: "1 + (1 / (1 + 1/ε))⇧2 * 2 * 9.84 * ( 1 + 1/ε )^2
= 1 + (1 / (1 + 1/ε))⇧2 * ( 1 + 1/ε )^2 * 2 * 9.84"
by (simp add: mult.commute)
have ****: "(1 / (1 + 1/ε))⇧2 * ( 1 + 1/ε )^2 = 1"
using pos
by (simp add: power_one_over)
from analysis_1_2[OF p ind mstar_2 beta]
have "measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 2)) ≤ 1/(1+ε) * μ (mstar - 2)}
≤ 1 / (1 + (1 - 1/(1+ε))⇧2 * μ (mstar - 2))"
by auto
also have "... = 1 / (1 + (1 / (1 + 1/ε))⇧2 * μ (mstar - 2))"
unfolding ** by auto
also have "... ≤ 1 / (1 + (1 / (1 + 1/ε))⇧2 * 2 * pivot)"
using *
by (smt (verit) epos divide_pos_pos frac_le pivot_def pos_prod_le zero_less_power)
also have "... = 1 / (1 + (1 / (1 + 1/ε))⇧2 * 2 * 9.84 * ( 1 + 1/ε )^2)"
unfolding pivot_def by auto
also have "... = 1 / 20.68"
unfolding *** **** by auto
finally have *****: "measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 2)) ≤ 1/(1+ε) * μ (mstar - 2)} ≤ 1 / 20.68" .
have "measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 2)) < 1/(1+ε) * μ (mstar - 2)}
≤ measure_pmf.prob p {s. real (card_slice (λw. H w s) (mstar - 2)) ≤ 1/(1+ε) * μ (mstar - 2)}"
by (auto intro!: measure_pmf.finite_measure_mono)
then have ******: "measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 2)) < 1/(1+ε) * μ (mstar - 2)}
≤ 1 / 20.68"
using ***** by auto
have "measure_pmf.prob (map_pmf (λs w. H w s) p) (L (mstar-2))
= measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 2)) < 1/(1+ε) * μ (mstar - 2)}"
unfolding L_def
by auto
also have "... ≤ 1 / 20.68"
using ****** by auto
finally have "measure_pmf.prob (map_pmf (λs w. H w s) p) (L (mstar-2)) ≤ 1 / 20.68" .
}
ultimately show ?thesis by auto
qed
lemma analysis_2_3:
assumes p: "finite (set_pmf p)"
assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
{α::'a assg. dom α = S}
{α::nat assg. dom α = {0..<card S - 1}}"
shows "
measure_pmf.prob
(map_pmf (λs w. H w s) p) (L (mstar-1)) ≤ 1 / 10.84"
proof -
have epos: "1 + 1 / ε > 0"
by (simp add: ε pos_add_strict)
then have pos_pivot: "pivot > 0"
unfolding pivot_def
by simp
have "mstar ≥ 2 ∨ mstar < 2" by auto
moreover {
assume "mstar < 2"
then have " measure_pmf.prob (map_pmf (λs w. H w s) p) (L (mstar-2))
≤ 1 / 10.84"
by (auto simp add: L0_empty)
}
moreover {
assume lo_mstar: "mstar ≥ 2"
have "1 + ε / (1 + ε) > 0"
by (simp add: add_nonneg_pos ε)
then have lo_mu_mstar_1: "μ (mstar-1) > pivot"
using mstar_prop(1) using thresh
by (smt (verit) nonzero_mult_div_cancel_right real_divide_pos_left)
have mstar_1: "mstar-1 ≤ card S - 1"
using lo_mstar diff_le_self dual_order.trans mstar_prop(3) by blast
have beta: "1/(1+ε) ≤ (1::real)"
using ε by auto
have "(1 / (1 + 1/ε))⇧2 > 0"
using epos by auto
then have *: "1 + (1 / (1 + 1/ε))⇧2 * pivot ≤ 1 + (1 / (1 + 1/ε))⇧2 * μ (mstar - 1)"
using lo_mu_mstar_1
by auto
have "1 - 1/(1+ε) = 1 / (1 + 1/ε)"
by (smt (verit, ccfv_threshold) ε conjugate_exponent_def conjugate_exponent_real(1))
then have **: "(1 - 1/(1+ε))^2 = (1 / (1 + 1/ε))^2"
by simp
have ***: "1 + (1 / (1 + 1/ε))⇧2 * 9.84 * ( 1 + 1/ε )^2
= 1 + (1 / (1 + 1/ε))⇧2 * ( 1 + 1/ε )^2 * 9.84"
by (simp add: mult.commute)
have ****: "(1 / (1 + 1/ε))⇧2 * ( 1 + 1/ε )^2 = 1"
by (metis (mono_tags, opaque_lifting) ‹0 < 1 + 1 / ε› div_by_1 divide_divide_eq_right divide_self_if less_irrefl mult.commute power_mult_distrib power_one)
from analysis_1_2[OF p ind mstar_1 beta]
have "measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 1)) ≤ 1/(1+ε) * μ (mstar - 1)}
≤ 1 / (1 + (1 - 1/(1+ε))⇧2 * μ (mstar - 1))"
by auto
moreover have "... = 1 / (1 + (1 / (1 + 1/ε))⇧2 * μ (mstar - 1))"
unfolding ** by auto
moreover have "... ≤ 1 / (1 + (1 / (1 + 1/ε))⇧2 * pivot)"
using *
by (smt (verit) ‹0 < (1 / (1 + 1 / ε))⇧2› frac_le pos_pivot zero_le_mult_iff)
moreover have "... = 1 / (1 + (1 / (1 + 1/ε))⇧2 * 9.84 * ( 1 + 1/ε )^2)"
unfolding pivot_def by auto
moreover have "... = 1 / (1 + (1 / (1 + 1/ε))⇧2 * ( 1 + 1/ε )^2 * 9.84)"
unfolding *** by auto
moreover have "... = 1 / (1 + 9.84)"
unfolding **** by auto
moreover have "... = 1 / 10.84"
by auto
ultimately have *****: "measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 1)) ≤ 1/(1+ε) * μ (mstar - 1)} ≤ 1 / 10.84"
by linarith
have "measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 1)) < 1/(1+ε) * μ (mstar - 1)}
≤ measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 1)) ≤ 1/(1+ε) * μ (mstar - 1)}"
by (auto intro!: measure_pmf.finite_measure_mono)
then have ******: "measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 1)) < 1/(1+ε) * μ (mstar - 1)}
≤ 1 / 10.84"
using ***** by auto
have "measure_pmf.prob (map_pmf (λs w. H w s) p) (L (mstar-1))
= measure_pmf.prob p
{s. real (card_slice (λw. H w s) (mstar - 1)) < 1/(1+ε) * μ (mstar - 1)}"
unfolding L_def
by auto
moreover have "... ≤ 1 / 10.84"
using ****** by auto
ultimately have "measure_pmf.prob (map_pmf (λs w. H w s) p) (L (mstar-1)) ≤ 1 / 10.84"
by auto
}
ultimately show ?thesis by auto
qed
lemma analysis_2_4:
assumes p: "finite (set_pmf p)"
assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
{α::'a assg. dom α = S}
{α::nat assg. dom α = {0..<card S - 1}}"
shows "
measure_pmf.prob (map_pmf (λs w. H w s) p) (L mstar ∪ U mstar) ≤ 1 / 4.92"
proof -
have "1 + 1 / ε > 0"
by (simp add: ε pos_add_strict)
then have pos_pivot: "pivot > 0"
unfolding pivot_def
by simp
have "mstar ≥ 1 ∨ mstar < 1" by auto
moreover {
assume "mstar < 1"
have LU0_empty: "L mstar ∪ U mstar = {}"
using L0_empty U0_empty
using ‹mstar < 1› less_one by auto
then have "measure_pmf.prob (map_pmf (λs w. H w s) p) (L mstar ∪ U mstar)
≤ 1 / 4.92"
by auto
}
moreover {
assume lo_mstar: "mstar ≥ 1"
have extend_mu: "μ mstar * 2^1 = μ (mstar-1)"
using lo_mstar
apply (subst shift_μ)
by auto
have "1 + ε / (1 + ε) > 0"
by (simp add: add_nonneg_pos ε)
then have "μ (mstar-1) > pivot"
using mstar_prop(1) thresh
by (smt (verit) nonzero_mult_div_cancel_right real_divide_pos_left)
then have lo_mu_star: "μ mstar > pivot / 2"
using extend_mu
by auto
have mstar: "mstar ≤ card S - 1"
using lo_mstar
using diff_le_self dual_order.trans mstar_prop(3) by blast
have "ε*(1+1/ε) = 1+ε"
by (smt (verit) ε add_divide_eq_if_simps(1) divide_cancel_right divide_self_if nonzero_mult_div_cancel_left)
then have *: "9.84 * ε^2*(1+1/ε)^2 / 2 = 9.84 * (1+ε)^2 / 2"
by (metis (mono_tags, opaque_lifting) more_arith_simps(11) power_mult_distrib)
have "ε^2 * μ mstar ≥ ε^2 * pivot / 2"
using lo_mu_star
by (metis less_eq_real_def ordered_comm_semiring_class.comm_mult_left_mono times_divide_eq_right zero_le_power2)
then have **: "ε^2 * μ mstar ≥ 9.84 * (1+ε)^2 / 2"
unfolding pivot_def using * by auto
from analysis_1_1[OF p ind mstar]
have "measure_pmf.prob p
{s. ¦ card_slice ((λw. H w s)) mstar - μ mstar ¦ ≥ ε / (1 + ε) * μ mstar }
≤ (1 + ε)^2 / (ε^2 * μ mstar)"
by auto
also have "... ≤ (1 + ε)^2 / (9.84 * (1+ε)^2 / 2)"
using **
by (smt (verit) divide_cancel_left divide_le_0_iff frac_le pos_prod_le power2_less_0 zero_eq_power2)
also have "... = (1 + ε)^2 / (4.92 * (1+ε)^2)"
by simp
also have "... = 1 / 4.92"
using ε by simp
finally have *******: "measure_pmf.prob p
{s. ¦ card_slice ((λw. H w s)) mstar - μ mstar ¦ ≥ ε / (1 + ε) * μ mstar }
≤ 1 / 4.92" .
have "μ mstar / (1 + ε) - μ mstar = μ mstar * (1 / (1+ε) - 1)"
by (simp add: right_diff_distrib')
also have "... = μ mstar * (- ε / (1+ε))"
by (smt (verit) ε add_divide_distrib div_self minus_divide_left)
finally have ***: "μ mstar / (1 + ε) - μ mstar = μ mstar * (- ε / (1+ε))" .
have "{h. real (card_slice h mstar) ≤ μ mstar / (1 + ε)}
= {h. real (card_slice h mstar) - μ mstar ≤ μ mstar / (1 + ε) - μ mstar}"
by auto
also have "... = {h. real (card_slice h mstar) - μ mstar ≤ μ mstar * (- ε / (1+ε))}"
using *** by auto
finally have ****: "
{h. real (card_slice h mstar) ≤ μ mstar / (1 + ε)} =
{h. real (card_slice h mstar) - μ mstar ≤ μ mstar * (- ε / (1+ε))}" .
have "L mstar
= {h. real (card_slice h mstar) < μ mstar / (1 + ε)}"
unfolding L_def by auto
also have "...⊆ {h. real (card_slice h mstar) ≤ μ mstar / (1 + ε)}"
by auto
also have "... = {h. real (card_slice h mstar) - μ mstar ≤ μ mstar * (- ε / (1+ε))}"
unfolding **** by auto
finally have extend_L: "L mstar ⊆ {h. real (card_slice h mstar) - μ mstar ≤ μ mstar * (- ε / (1+ε))}" .
have *****: "μ mstar * (1 + ε / (1+ε)) - μ mstar = μ mstar * (ε / (1+ε))"
by (metis (no_types, opaque_lifting) add.commute diff_add_cancel group_cancel.sub1 mult.right_neutral right_diff_distrib')
have ******: "U mstar = {h. real (card_slice h mstar) ≥ μ mstar * (1 + ε / (1+ε))}"
unfolding U_def by auto
have "{h. real (card_slice h mstar) ≥ μ mstar * (1 + ε / (1+ε))}
= {h. real (card_slice h mstar) - μ mstar ≥ μ mstar * (1 + ε / (1+ε)) - μ mstar}"
by auto
also have "... = {h. real (card_slice h mstar) - μ mstar ≥ μ mstar * (ε / (1+ε))}"
unfolding ***** by auto
finally have extend_U: "U mstar = {h. real (card_slice h mstar) - μ mstar ≥ μ mstar * (ε / (1+ε))}"
using ****** by auto
have "L mstar ∪ U mstar ⊆
{h. real (card_slice h mstar) - μ mstar ≤ μ mstar * (- ε / (1+ε))}
∪ {h. real (card_slice h mstar) - μ mstar ≥ μ mstar * (ε / (1+ε))}"
unfolding extend_U
using extend_L
by auto
also have "... = {h. ¦ real (card_slice h mstar) - μ mstar ¦ ≥ μ mstar * (ε / (1+ε))}"
by auto
finally have extend_LU: "L mstar ∪ U mstar ⊆ {h. ¦ real (card_slice h mstar) - μ mstar ¦ ≥ μ mstar * (ε / (1+ε))}" .
have "measure_pmf.prob (map_pmf (λs w. H w s) p) (L mstar ∪ U mstar)
≤ measure_pmf.prob (map_pmf (λs w. H w s) p) {h. ¦ real (card_slice h mstar) - μ mstar ¦ ≥ μ mstar * (ε / (1+ε))}"
using extend_LU
by (auto intro!: measure_pmf.finite_measure_mono)
also have "... = measure_pmf.prob p
{s. ¦ real (card_slice (λw. H w s) mstar) - μ mstar ¦ ≥ ε / (1 + ε) * μ mstar }"
by (simp add: mult.commute)
also have "... ≤ 1 / 4.92"
using ******* by auto
finally have "measure_pmf.prob (map_pmf (λs w. H w s) p) (L mstar ∪ U mstar) ≤ 1 / 4.92" .
}
ultimately show ?thesis by auto
qed
lemma analysis_3:
assumes p: "finite (set_pmf p)"
assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
{α::'a assg. dom α = S}
{α::nat assg. dom α = {0..<card S - 1}}"
assumes ε_up: "ε ≤ 1"
shows "
measure_pmf.prob (map_pmf (λs w. H w s) p)
approxcore_fail ≤ 0.36"
proof -
have "measure_pmf.prob (map_pmf (λs w. H w s) p) approxcore_fail
≤ measure_pmf.prob (map_pmf (λs w. H w s) p)
(T (mstar-3) ∪
L (mstar-2) ∪
L (mstar-1) ∪
(L mstar ∪ U mstar))"
using failure_bound
by (auto intro!: measure_pmf.finite_measure_mono)
moreover have "... ≤
measure_pmf.prob (map_pmf (λs w. H w s) p) (T (mstar-3) ∪ L (mstar-2) ∪ L (mstar-1))
+ measure_pmf.prob (map_pmf (λs w. H w s) p) (L mstar ∪ U mstar)"
by (auto intro!: measure_pmf.finite_measure_subadditive)
moreover have "... ≤
measure_pmf.prob (map_pmf (λs w. H w s) p) (T (mstar-3) ∪ L (mstar-2))
+ measure_pmf.prob (map_pmf (λs w. H w s) p) (L (mstar-1))
+ measure_pmf.prob (map_pmf (λs w. H w s) p) (L mstar ∪ U mstar)"
by (auto intro!: measure_pmf.finite_measure_subadditive)
moreover have "... ≤
measure_pmf.prob (map_pmf (λs w. H w s) p) (T (mstar-3))
+ measure_pmf.prob (map_pmf (λs w. H w s) p) (L (mstar-2))
+ measure_pmf.prob (map_pmf (λs w. H w s) p) (L (mstar-1))
+ measure_pmf.prob (map_pmf (λs w. H w s) p) (L mstar ∪ U mstar)"
by (auto intro!: measure_pmf.finite_measure_subadditive)
moreover have "... ≤ 1/62.5 + 1/20.68 + 1/10.84 + 1/4.92"
using analysis_2_1[OF p ind ε_up]
using analysis_2_2[OF p ind]
using analysis_2_3[OF p ind]
using analysis_2_4[OF p ind]
by auto
ultimately show ?thesis by force
qed
lemma analysis_3':
assumes p: "finite (set_pmf p)"
assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
{α::'a assg. dom α = S}
{α::nat assg. dom α = {0..<card S - 1}}"
shows "
measure_pmf.prob (map_pmf (λs w. H w s) p)
approxcore_fail ≤ 0.44"
proof -
have "measure_pmf.prob (map_pmf (λs w. H w s) p) approxcore_fail
≤ measure_pmf.prob (map_pmf (λs w. H w s) p)
(T (mstar-3) ∪
L (mstar-2) ∪
L (mstar-1) ∪
(L mstar ∪ U mstar))"
using failure_bound
by (auto intro!: measure_pmf.finite_measure_mono)
moreover have "... ≤
measure_pmf.prob (map_pmf (λs w. H w s) p) (T (mstar-3) ∪ L (mstar-2) ∪ L (mstar-1))
+ measure_pmf.prob (map_pmf (λs w. H w s) p) (L mstar ∪ U mstar)"
by (auto intro!: measure_pmf.finite_measure_subadditive)
moreover have "... ≤
measure_pmf.prob (map_pmf (λs w. H w s) p) (T (mstar-3) ∪ L (mstar-2))
+ measure_pmf.prob (map_pmf (λs w. H w s) p) (L (mstar-1))
+ measure_pmf.prob (map_pmf (λs w. H w s) p) (L mstar ∪ U mstar)"
by (auto intro!: measure_pmf.finite_measure_subadditive)
moreover have "... ≤
measure_pmf.prob (map_pmf (λs w. H w s) p) (T (mstar-3))
+ measure_pmf.prob (map_pmf (λs w. H w s) p) (L (mstar-2))
+ measure_pmf.prob (map_pmf (λs w. H w s) p) (L (mstar-1))
+ measure_pmf.prob (map_pmf (λs w. H w s) p) (L mstar ∪ U mstar)"
by (auto intro!: measure_pmf.finite_measure_subadditive)
moreover have "... ≤ 1/10.84 + 1/20.68 + 1/10.84 + 1/4.92"
using analysis_2_1'[OF p ind]
using analysis_2_2[OF p ind]
using analysis_2_3[OF p ind]
using analysis_2_4[OF p ind]
by auto
ultimately show ?thesis by auto
qed
end
end
end