Theory Approximate_Model_Counting.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

(* Slicing after a family *)
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

(* TODO: generalizable to any finite output alphabet instead of just booleans *)
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

(* Lem 1.1 in IJCAI'16 paper *)
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 -

  (* The variance for i-th slice *)
  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

(* Lem 1.2 in IJCAI'16 paper *)
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)

(* Lem 2.1 in IJCAI'16 paper *)
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" (* pivot = thresh / (1 + ε/(1+ε)) *)
      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

(* Alternative Lem 2.1 in IJCAI'16 paper without bound on epsilon *)
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

(* Lem 2.2 in IJCAI'16 paper *)
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

(* Lem 2.3 in IJCAI'16 paper *)
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

(* Lem 2.4 in IJCAI'16 paper *)
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

(* Lem 3 in IJCAI'16 paper *)
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

(* Alternative Lem 3 in IJCAI'16 paper without bound on epsilon *)
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