Theory Crowds_Protocol

(* Author: Johannes Hölzl <hoelzl@in.tum.de> *)

section ‹Formalization of the Crowds-Protocol›

theory Crowds_Protocol
  imports "../Discrete_Time_Markov_Chain"
begin

lemma cond_prob_nonneg[simp]: "0 ≤ cond_prob M A B"
  by (auto simp: cond_prob_def)

lemma (in MC_syntax) emeasure_suntil_geometric:
  assumes [measurable]: "Measurable.pred S P"
  assumes "s ∈ X" and *[simp]: "0 ≤ p" "0 ≤ r"
  assumes r: "⋀s. s ∈ X ⟹ emeasure (T s) {ω∈space (T s). P ω} = ennreal r"
  assumes p: "⋀s. s ∈ X ⟹ emeasure (K s) X = ennreal p" "p < 1"
  assumes "⋀t. AE ω in T t. ¬ (P ⊓ (HLD X ⊓ nxt (HLD X suntil P))) ω"
  shows "emeasure (T s) {ω∈space (T s). (HLD X suntil P) ω} = r / (1 - p)"
proof (subst emeasure_suntil_disj)
  let ?F = "λF s. emeasure (T s) {ω ∈ space (T s). P ω} + (∫⇧+ t. F t * indicator X t ∂K s)"
  let ?f = "λx. ennreal r + ennreal p * x"

  have "mono ?F" "mono ?f"
    by (auto intro!: monoI max.mono add_mono nn_integral_mono mult_left_mono mult_right_mono simp: le_fun_def)

  have 1: "lfp ?f ≤ lfp ?F s"
    using ‹s ∈ X›
  proof (induction arbitrary: s rule: lfp_ordinal_induct[OF ‹mono ?f›])
    case step: (1 x)
    then have "?f x ≤ ?F (λ_. x) s"
      by (auto simp: p r[simplified] nn_integral_cmult mult.commute[of _ x]
               intro!: add_mono mult_right_mono)
    also have "?F (λ_. x) ≤ ?F (lfp ?F)"
      using step
      by (intro le_funI add_mono order_refl nn_integral_mono) (auto simp: split: split_indicator)
    finally show ?case
      by (subst lfp_unfold[OF ‹mono ?F›]) (auto simp: le_fun_def)
  qed (auto intro!: Sup_least)
  also have 2: "lfp ?F s ≤ r / (1 - p)"
    using ‹s ∈ X›
  proof (induction arbitrary: s rule: lfp_ordinal_induct[OF ‹mono ?F›])
    case (1 S)
    with r have "?F S s ≤ ennreal r + (∫⇧+x. ennreal (r / (1 - p)) * indicator X x ∂K s)"
      by (intro add_mono nn_integral_mono) (auto split: split_indicator)
    also have "… ≤ ennreal r + ennreal (r * p / (1 - p))"
      using ‹s ∈ X› by (simp add: nn_integral_cmult_indicator p ennreal_mult''[symmetric])
    also have "… = ennreal (r / (1 - p))"
      using ‹p < 1› by (simp add: field_simps ennreal_plus[symmetric] del: ennreal_plus)
    finally show ?case .
  qed (auto intro!: SUP_least)
  finally obtain x where x: "lfp ?f = ennreal x" and [simp]: "0 ≤ x"
    by (cases "lfp ?f") (auto simp: top_unique)
  from ‹p < 1› have "⋀x. x = r + p * x ⟹ x = r / (1 - p)"
    by (auto simp: field_simps)
  with lfp_unfold[OF ‹mono ?f›] ‹p < 1› have "lfp ?f = r / (1 - p)"
    unfolding x by (auto simp add: ennreal_plus[symmetric] ennreal_mult[symmetric] simp del: ennreal_plus)
  with 1 2 show "lfp ?F s = ennreal (r / (1 - p))"
    by auto
qed fact+

subsection ‹Definition of the Crowds-Protocol›

datatype 'a state = Start | Init 'a | Mix 'a | End

lemma inj_Mix[simp]: "inj_on Mix A"
  by (auto intro: inj_onI)

lemma inj_Init[simp]: "inj_on Init A"
  by (auto intro: inj_onI)

lemma distinct_state_image[simp]:
  "Start ∉ Mix ` A" "Init j ∉ Mix ` A" "End ∉ Mix ` A" "Mix j ∈ Mix ` A ⟷ j ∈ A"
  "Start ∉ Init ` A" "Mix j ∉ Init ` A" "End ∉ Init ` A" "Init j ∈ Init ` A ⟷ j ∈ A"
  by auto

lemma Init_cut_Mix[simp]:
  "Init ` H ∩ Mix ` J = {}"
  by auto

abbreviation "Jondo B ≡ Init`B ∪ Mix`B"

locale Crowds_Protocol =
  fixes J :: "'a set" and C :: "'a set" and p_f :: real and p_i :: "'a ⇒ real"
  assumes J_not_empty: "J ≠ {}" and finite_J[simp]: "finite J"
  assumes C_smaller: "C ⊂ J" and C_non_empty: "C ≠ {}"
  assumes p_f: "0 < p_f" "p_f < 1"
  assumes p_i_nonneg[simp]: "⋀j. j ∈ J ⟹ 0 ≤ p_i j"
  assumes p_i_distr: "(∑j∈J. p_i j) = 1"
  assumes p_i_C: "⋀j. j ∈ C ⟹ p_i j = 0"
begin

abbreviation H :: "'a set" where
  "H ≡ J - C"

definition "p_j = 1 / card J"

lemma p_f_nonneg[simp]: "0 ≤ p_f" "p_f ≤ 1"
  using p_f by simp_all

lemma p_j_nonneg[simp]: "0 ≤ p_j"
  by (simp add: p_j_def)

definition "p_H = card H / card J"

lemma p_H_nonneg[simp]: "0 ≤ p_H" "p_H ≤ 1"
  by (auto simp: p_H_def divide_le_eq_1 card_gt_0_iff intro!: card_mono )

definition next_prob :: "'a state ⇒ 'a state ⇒ real" where
  "next_prob s t = (case (s, t) of (Start, Init j) ⇒ if j ∈ H then p_i j else 0
                                 | (Init j, Mix j') ⇒ if j' ∈ J then p_j else 0
                                 | (Mix j, Mix j') ⇒ if j' ∈ J then p_f * p_j else 0
                                 | (Mix j, End) ⇒ 1 - p_f
                                 | (End, End) ⇒ 1
                                 | _ ⇒ 0)"

definition "N s = embed_pmf (next_prob s)"

interpretation MC_syntax N .

abbreviation "𝔓 ≡ T Start"

abbreviation "E s ≡ set_pmf (N s)"

lemma finite_C[simp]: "finite C"
  using C_smaller finite_J by (blast intro: finite_subset)

lemma sum_p_i_C[simp]: "sum p_i C = 0"
  by (auto intro: sum.neutral p_i_C)

lemma sum_p_i_H[simp]: "sum p_i H = 1"
  using C_smaller by (simp add: sum_diff p_i_distr)

lemma possible_jondo:
  obtains j where "j ∈ J" "j ∉ C" "p_i j ≠ 0"
proof (atomize_elim, rule ccontr)
  assume "¬ (∃j. j ∈ J ∧ j ∉ C ∧ p_i j ≠ 0)"
  with p_i_C have "∀j∈J. p_i j = 0"
    by auto
  with p_i_distr show False
    by simp
qed

lemma C_le_J[simp]: "card C < card J"
  using C_smaller
  by (intro psubset_card_mono) auto

lemma p_H: "0 < p_H" "p_H < 1"
  using J_not_empty C_smaller C_non_empty
  by (simp_all add: p_H_def card_Diff_subset card_mono field_simps zero_less_divide_iff card_gt_0_iff)

lemma p_H_p_f_pos: "0 < p_H * p_f"
  using p_f p_H by (simp add: zero_less_mult_iff)

lemma p_H_p_f_less_1: "p_H * p_f < 1"
proof -
  have "p_H * p_f < 1 * 1"
    using p_H p_f by (intro mult_strict_mono) auto
  then show "p_H * p_f < 1" by simp
qed

lemma p_j_pos: "0 < p_j"
  unfolding p_j_def using J_not_empty by auto

lemma H_compl: "1 - p_H = real (card C) / real (card J)"
  using C_non_empty J_not_empty C_smaller
  by (simp add: p_H_def card_Diff_subset card_mono of_nat_diff divide_eq_eq field_simps)

lemma H_compl2: "1 - p_H = card C * p_j"
  unfolding H_compl p_j_def by simp

lemma H_eq2: "card H * p_j = p_H"
  unfolding p_j_def p_H_def by simp

lemma pmf_next_pmf[simp]: "pmf (N s) t = next_prob s t"
  unfolding N_def
proof (rule pmf_embed_pmf)
  show "⋀x. 0 ≤ next_prob s x"
    using p_j_pos p_f by (auto simp: next_prob_def intro: p_i_nonneg split: state.split)
  show "(∫⇧+ x. ennreal (next_prob s x) ∂count_space UNIV) = 1"
    using p_f J_not_empty
    by (subst nn_integral_count_space'[where A="Init`H ∪ Mix`J ∪ {End}"])
       (auto simp: next_prob_def sum.reindex sum.union_disjoint p_i_distr p_j_def
             split: state.split)
qed

lemma next_prob_Start[simp]: "next_prob Start (Init j) = (if j ∈ H then p_i j else 0)"
  by (auto simp: next_prob_def)

lemma next_prob_to_Init[simp]: "j ∈ H ⟹ next_prob s (Init j) =
    (case s of Start ⇒ p_i j | _ ⇒ 0)"
  by (cases s) (auto simp: next_prob_def)

lemma next_prob_to_Mix[simp]: "j ∈ J ⟹ next_prob s (Mix j) =
    (case s of Init j ⇒ p_j | Mix j ⇒ p_f * p_j | _ ⇒ 0)"
  by (cases s) (auto simp: next_prob_def)

lemma next_prob_to_End[simp]: "next_prob s End =
    (case s of Mix j ⇒ 1 - p_f | End ⇒ 1 | _ ⇒ 0)"
  by (cases s) (auto simp: next_prob_def)

lemma next_prob_from_End[simp]: "next_prob End s = 0 ⟷ s ≠ End"
  by (cases s) (auto simp: next_prob_def)

lemma next_prob_Mix_MixI: "∃j. s = Mix j ⟹ ∃j∈J. s' = Mix j ⟹ next_prob s s' = p_f * p_j"
  by (cases s) auto


lemma E_Start: "E Start = {Init j | j. j ∈ H ∧ p_i j ≠ 0 }"
  using p_i_C by (auto simp: set_pmf_iff next_prob_def split: state.splits if_split_asm)

lemma E_Init: "E (Init j) = {Mix j | j. j ∈ J }"
  using p_j_pos C_smaller by (auto simp: set_pmf_iff next_prob_def split: state.splits if_split_asm)

lemma E_Mix: "E (Mix j) = {Mix j | j. j ∈ J } ∪ {End}"
  using p_j_pos p_f by (auto simp: set_pmf_iff next_prob_def split: state.splits if_split_asm)

lemma E_End: "E End = {End}"
  by (auto simp: set_pmf_iff next_prob_def split: state.splits if_split_asm)

lemma enabled_End:
  "enabled End ω ⟷ ω = sconst End"
proof safe
  assume "enabled End ω" then show "ω = sconst End"
  proof (coinduction arbitrary: ω)
    case Eq_stream then show ?case
      by (auto simp: enabled.simps[of _ ω] E_End)
  qed
next
  show "enabled End (sconst End)"
    by coinduction (simp add: E_End)
qed

lemma AE_End: "(AE ω in T End. P ω) ⟷ P (sconst End)"
proof -
  have "(AE ω in T End. P ω) ⟷ (AE ω in T End. P ω ∧ ω = sconst End)"
    using AE_T_enabled[of End] by (simp add: enabled_End)
  also have "… = (AE ω in T End. P (sconst End) ∧ ω = sconst End)"
    by (simp add: enabled_End del: AE_conj_iff cong: rev_conj_cong)
  also have "… = (AE ω in T End. P (sconst End))"
    using AE_T_enabled[of End] by (simp add: enabled_End)
  finally show ?thesis
    by simp
qed

lemma emeasure_Init_eq_Mix:
  assumes [measurable]: "Measurable.pred S P"
  assumes AE_End: "AE x in T End. ¬ P (End ## x)"
  shows "emeasure (T (Init j)) {x∈space (T (Init j)). P x} =
    emeasure (T (Mix j)) {x∈space (T (Mix j)). P x} / p_f"
proof -
  have *: "{Mix j | j. j ∈ J } = Mix ` J"
    by auto
  show ?thesis
    using emeasure_eq_0_AE[OF AE_End] p_f
    apply (subst (1 2) emeasure_Collect_T)
    apply simp
    apply (subst (1 2) nn_integral_measure_pmf_finite)
    apply (auto simp: E_Mix E_Init * sum.reindex sum_distrib_right[symmetric] divide_ennreal
      ennreal_times_divide[symmetric])
    done
qed

text ‹

What is the probability that the server sees a specific jondo (including the initiator) as sender.

›

definition visit :: "'a set ⇒ 'a set ⇒ 'a state stream ⇒ bool" where
  "visit I L = Init`(I ∩ H) ⋅ (HLD (Mix`J) suntil (Mix`(L ∩ J) ⋅ HLD {End}))"

lemma visit_unique1:
  "visit I1 L1 ω ⟹ visit I2 L2 ω ⟹ I1 ∩ I2 ≠ {}"
  by (auto simp: visit_def HLD_iff)

lemma visit_unique2:
  assumes "visit I1 L1 ω" "visit I2 L2 ω"
  shows "L1 ∩ L2 ≠ {}"
proof -
  let ?U = "λL ω. (HLD (Mix`J) suntil ((Mix`(L∩J)) ⋅ HLD {End})) ω"
  have "?U L1 (stl ω)" "?U L2 (stl ω)"
    using assms by (auto simp: visit_def)
  then show "L1 ∩ L2 ≠ {}"
  proof (induction "stl ω" arbitrary: ω rule: suntil_induct_strong)
    case base then show ?case
      by (auto simp add: suntil.simps[of _ _ "stl (stl ω)"] suntil.simps[of _ _ "stl ω"] HLD_iff)
  next
    case step
    show ?case
    proof cases
      assume "((Mix`(L2∩J)) ⋅ HLD {End}) (stl ω)"
      with step.hyps show ?thesis
        by (auto simp: inj_Mix HLD_iff elim: suntil.cases)
    next
      assume "¬ ((Mix`(L2∩J)) ⋅ HLD {End}) (stl ω)"
      with step.prems have "?U L2 (stl (stl ω))"
        by (auto elim: suntil.cases)
      then show ?thesis
        by (rule step.hyps(4)[OF refl])
    qed
  qed
qed

lemma visit_imp_in_H: "visit {i} J ω ⟹ i ∈ H"
  by (auto simp: visit_def HLD_iff)

lemma emeasure_visit:
  assumes I: "I ⊆ H" and L: "L ⊆ J"
  shows "emeasure 𝔓 {ω∈space 𝔓. visit I L ω} = (∑i∈I. p_i i) * (card L * p_j)"
proof -
  let ?J = "HLD (Mix`J)" and ?E = "(Mix`L) ⋅ HLD {End}"
  let ?φ = "?J aand not ?E"
  let ?P = "λx P. emeasure (T x) {ω∈space (T x). P ω}"

  have [intro]: "finite L"
    using finite_J ‹L ⊆ J› by (blast intro: finite_subset)
  have [simp, intro]: "finite I"
    using finite_J ‹I ⊆ H› by (blast intro: finite_subset)

  { fix j assume j: "j ∈ H"
    have "?P (Mix j) (?J suntil ?E) = (p_f * p_j * (1 - p_f) * card L) / (1 - p_f)"
    proof (rule emeasure_suntil_geometric)
      fix s assume s: "s ∈ Mix ` J"
      then have "?P s ?E = (∫⇧+x. ennreal (1 - p_f) * indicator (Mix`L) x ∂N s)"
        by (auto simp add: emeasure_HLD_nxt emeasure_HLD AE_measure_pmf_iff emeasure_pmf_single
                 split: state.split split_indicator simp del: space_T nxt.simps
                 intro!: nn_integral_cong_AE)
      also have "… = ennreal (1 - p_f) * emeasure (N s) (Mix`L)"
        using p_f by (intro nn_integral_cmult_indicator) auto
      also have "… = ennreal ((1 - p_f) * card L * p_j * p_f)"
        using s assms
        by (subst emeasure_measure_pmf_finite)
           (auto simp: sum.reindex subset_eq ennreal_mult mult_ac)
      finally show "?P s ?E = p_f * p_j * (1 - p_f) * card L"
        by simp
    next
      show "⋀t. AE ω in T  t. ¬ (?E ⊓ (?J ⊓ nxt (?J suntil ?E))) ω"
        by (intro AE_I2) (auto simp: HLD_iff elim: suntil.cases)
    qed (insert p_f j, auto simp: emeasure_measure_pmf_finite sum.reindex p_j_def)
    then have "?P (Init j) (?J suntil ?E) = (p_f * p_j * (1 - p_f) * card L) / (1 - p_f) / p_f"
      by (subst emeasure_Init_eq_Mix) (simp_all add:  suntil.simps[of _ _ "x ## s" for x s] divide_ennreal p_f)
    then have "?P (Init j) (?J suntil ?E) = p_j * card L"
      using p_f by simp }
  note J_suntil_E = this

  have "?P Start (visit I L) = (∫⇧+x. ?P x (?J suntil ?E) * indicator (Init`I) x ∂N Start)"
    unfolding visit_def using I L by (subst emeasure_HLD_nxt) (auto simp: Int_absorb2)
  also have "… = (∫⇧+x. ennreal (p_j * card L) * indicator (Init`I) x ∂N Start)"
    using I J_suntil_E
    by (intro nn_integral_cong ennreal_mult_right_cong)
       (auto split: split_indicator_asm)
  also have "… = ennreal ((∑i∈I. p_i i) * card L * p_j)"
    using p_j_pos assms
    by (subst nn_integral_cmult_indicator)
       (auto simp: emeasure_measure_pmf_finite sum.reindex subset_eq ennreal_mult[symmetric] sum_nonneg)
  finally show ?thesis by (simp add: ac_simps)
qed

lemma measurable_visit[measurable]: "Measurable.pred S (visit I L)"
  by (simp add: visit_def)

lemma AE_visit: "AE ω in 𝔓. visit H J ω"
proof (rule T.AE_I_eq_1)
  show "emeasure 𝔓 {ω∈space 𝔓. visit H J ω} = 1"
    using J_not_empty by (subst emeasure_visit ) (simp_all add: p_j_def)
qed simp

subsection ‹Server gets no information›

lemma server_view1: "j ∈ J ⟹ 𝒫(ω in 𝔓. visit H {j} ω) = p_j"
  unfolding measure_def by (subst emeasure_visit) simp_all

lemma server_view_indep:
  "L ⊆ J ⟹ I ⊆ H ⟹ 𝒫(ω in 𝔓. visit I L ω) = 𝒫(ω in 𝔓. visit H L ω) * 𝒫(ω in 𝔓. visit I J ω)"
  unfolding measure_def
  by (subst (1 2 3) emeasure_visit) (auto simp: p_j_def sum_nonneg subset_eq)

lemma server_view: "𝒫(ω in 𝔓. ∃j∈H. visit {j} {j} ω) = p_j"
  using finite_J
proof (subst T.prob_sum[where I="H" and P="λj. visit {j} {j}"])
  show "(∑j∈H. 𝒫(ω in 𝔓. visit {j} {j} ω)) = p_j"
    by (auto simp: measure_def emeasure_visit sum_distrib_right[symmetric] simp del: space_T sets_T)
  show "AE x in 𝔓. (∀n∈H. visit {n} {n} x ⟶ (∃j∈H. visit {j} {j} x)) ∧
                ((∃j∈H. visit {j} {j} x) ⟶ (∃!n. n ∈ H ∧ visit {n} {n} x))"
    by (auto dest: visit_unique1)
qed simp_all

subsection ‹Probability that collaborators gain information›

definition "hit_C = Init`H ⋅ ev (HLD (Mix`C))"
definition "before_C B = (HLD (Jondo H)) suntil ((Jondo (B ∩ H)) ⋅ HLD (Mix ` C))"

lemma measurable_hit_C[measurable]: "Measurable.pred S hit_C"
  by (simp add: hit_C_def)

lemma measurable_before_C[measurable]: "Measurable.pred S (before_C B)"
  by (simp add: before_C_def)

lemma before_C:
  assumes ω: "enabled Start ω"
  shows "before_C B ω ⟷
    ((Init`H ⋅ (HLD (Mix`H) suntil (Mix`(B ∩ H) ⋅ HLD (Mix`C)))) or (Init`(B ∩ H) ⋅ HLD (Mix`C))) ω"
proof -
  { fix ω s assume "((HLD (Jondo H)) suntil (Jondo (B ∩ H) ⋅ HLD (Mix ` C))) ω"
      "enabled s ω" "s ∈ Jondo H"
    then have "(HLD (Mix ` H) suntil (Mix ` (B ∩ H) ⋅ (HLD (Mix ` C)))) ω"
    proof (induction arbitrary: s)
      case (base ω) then show ?case
        by (auto simp: HLD_iff enabled.simps[of _ ω] E_Init E_Mix intro!: suntil.intros(1))
    next
      case (step ω) from step.prems step.hyps step.IH[of "shd ω"] show ?case
        by (auto simp: HLD_iff enabled.simps[of _ ω] E_Init E_Mix
                       suntil.simps[of _ _ ω] enabled_End suntil_sconst)
    qed }
  note this[of "stl ω" "shd ω"]
  moreover
  { fix ω s assume "(HLD (Mix ` H) suntil (Mix ` (B ∩ H) ⋅ (HLD (Mix ` C)))) ω"
      "enabled s ω" "s ∈ Jondo H"
    then have "((HLD (Jondo H)) suntil ((Jondo (B ∩ H)) ⋅ HLD (Mix ` C))) ω"
    proof (induction arbitrary: s)
      case (step ω) from step.prems step.hyps step.IH[of "shd ω"] show ?case
        by (auto simp: HLD_iff enabled.simps[of _ ω] E_Init E_Mix
                       suntil.simps[of _ _ ω] enabled_End suntil_sconst)
    qed (auto intro: suntil.intros simp: HLD_iff) }
  note this[of "stl ω" "shd ω"]
  ultimately show ?thesis
    using assms
    using ‹enabled Start ω›
    unfolding before_C_def suntil.simps[of _ _ ω] enabled.simps[of _ ω]
    by (auto simp: E_Start HLD_iff)
qed

lemma before_C_unique:
  assumes ω: "before_C I1 ω" "before_C I2 ω" shows "I1 ∩ I2 ≠ {}"
  using ω unfolding before_C_def
proof induction
  case (base ω) then show ?case
    by (auto simp add: suntil.simps[of _ _ ω] suntil.simps[of _ _ "stl ω"] HLD_iff)
next
  case (step ω) then show ?case
    by (auto simp add: suntil.simps[of _ _ ω] suntil.simps[of _ _ "stl ω"] HLD_iff)
qed

lemma hit_C_imp_before_C:
  assumes "enabled Start ω" "hit_C ω" shows "before_C H ω"
proof -
  let ?X = "Init`H ∪ Mix`H"
  { fix ω s assume "ev (HLD (Mix`C)) ω" "s∈?X" "enabled s ω"
    then have "((HLD (Jondo H)) suntil (?X ⋅ HLD (Mix ` C))) (s ## ω)"
    proof (induction arbitrary: s rule: ev_induct_strong)
      case (step ω s) from step.IH[of "shd ω"] step.prems step.hyps show ?case
        by (auto simp: enabled.simps[of _ ω] suntil_Stream E_Init E_Mix HLD_iff
          enabled_End ev_sconst)
    qed (auto simp: suntil_Stream) }
  from this[of "stl ω" "shd ω"] assms show ?thesis
    by (auto simp: before_C_def hit_C_def enabled.simps[of _ ω] E_Start)
qed

lemma before_C_single:
  assumes "before_C I ω" shows "∃i∈I ∩ H. before_C {i} ω"
  using assms unfolding before_C_def by induction (auto simp: HLD_iff intro: suntil.intros)

lemma before_C_imp_in_H: "before_C {i} ω ⟹ i ∈ H"
  by (auto dest: before_C_single)

subsection ‹The probability that the sender hits a collaborator›

lemma Pr_hit_C: "𝒫(ω in 𝔓. hit_C ω) = (1 - p_H) / (1 - p_H * p_f)"
proof -
  let ?P = "λx P. emeasure (T x) {ω∈space (T x). P ω}"
  let ?M = "HLD (Mix ` C)" and ?I = "Init`H" and ?J = "Mix`H"
  let ?φ = "(HLD ?J) aand not ?M"

  { fix s assume s: "s ∈ Jondo J"
    have "AE ω in T s. ev ?M ω ⟷ (HLD ?J suntil ?M) ω"
      using AE_T_enabled
    proof eventually_elim
      fix ω assume ω: "enabled s ω"
      show "ev ?M ω ⟷ (HLD ?J suntil ?M) ω"
      proof
        assume "ev ?M ω"
        from this ω s show "(HLD ?J suntil ?M) ω"
        proof (induct arbitrary: s rule: ev_induct_strong)
          case (step ω) then show ?case
            by (auto simp: HLD_iff enabled.simps[of _ ω] suntil.simps[of _ _ ω] E_End E_Init E_Mix
                           enabled_End ev_sconst)
        qed (auto simp: HLD_iff E_Init intro: suntil.intros)
      qed (rule ev_suntil)
    qed }
  note ev_eq_suntil = this

  have "?P Start hit_C = (∫⇧+x. ?P x (ev ?M) * indicator ?I x ∂N Start)"
    unfolding hit_C_def by (rule emeasure_HLD_nxt) measurable
  also have "… = (∫⇧+x. ennreal ((1 - p_H) / (1 - p_f * p_H)) * indicator ?I x ∂N Start)"
  proof (intro nn_integral_cong ennreal_mult_right_cong refl)
    fix x assume "indicator (Init ` H) x ≠ 0"
    then have "x ∈ ?I"
      by (auto split: split_indicator_asm)
    { fix j assume j: "j ∈ H"
      with ev_eq_suntil[of "Mix j"] have "?P (Mix j) (ev ?M) = ?P (Mix j) ((HLD ?J) suntil ?M)"
        by (intro emeasure_eq_AE) auto
      also have "… = (((1 - p_H) * p_f)) / (1 - p_H * p_f)"
      proof (rule emeasure_suntil_geometric)
        fix s assume s: "s ∈ Mix ` H"
        from s C_smaller show "?P s ?M = ennreal ((1 - p_H) * p_f)"
          by (subst emeasure_HLD)
             (auto simp add: emeasure_measure_pmf_finite sum.reindex subset_eq p_j_def H_compl)
        from s show "emeasure (N s) (Mix`H) = p_H * p_f"
          by (auto simp: emeasure_measure_pmf_finite sum.reindex p_H_def p_j_def)
      qed (insert j, auto simp: HLD_iff p_H_p_f_less_1)
      finally have "?P (Init j) (ev ?M) = (1 - p_H) / (1 - p_H * p_f)"
        using p_f
        by (subst emeasure_Init_eq_Mix)
           (auto simp: ev_Stream AE_End ev_sconst HLD_iff mult_le_one divide_ennreal) }
    then show "?P x (ev ?M) = (1 - p_H) / (1 - p_f * p_H)"
      using ‹x ∈ ?I› by (auto simp: mult_ac)
  qed
  also have "… = ennreal ((1 - p_H) / (1 - p_H * p_f))"
    using p_j_pos p_H p_H_p_f_less_1
    by (subst nn_integral_cmult_indicator)
       (auto simp: emeasure_measure_pmf_finite sum.reindex subset_eq mult_ac
             intro!: divide_nonneg_nonneg)
  finally show ?thesis
    by (simp add: measure_def mult_le_one)
qed

lemma before_C_imp_hit_C:
  assumes "enabled Start ω" "before_C B ω"
  shows "hit_C ω"
proof -
  { fix ω j assume "((HLD (Jondo H)) suntil (Jondo (B ∩ H) ⋅ HLD (Mix ` C))) ω"
      "j ∈ H" "enabled (Mix j) ω"
    then have "ev (HLD (Mix`C)) ω"
    proof (induction arbitrary: j rule: suntil_induct_strong)
      case (step ω) then show ?case
        by (auto simp: enabled.simps[of _ ω] E_Mix enabled_End ev_sconst suntil_sconst HLD_iff)
    qed auto }
  from this[of "stl (stl ω)"] assms show "hit_C ω"
    by (force simp: before_C_def hit_C_def E_Start HLD_iff E_Init
      enabled.simps[of _ ω] ev.simps[of _ ω] suntil.simps[of _ _ ω]
      enabled.simps[of _ "stl ω"] ev.simps[of _ "stl ω"] suntil.simps[of _ _ "stl ω"])
qed

lemma negE: "¬ P ⟹ P ⟹ False"
  by blast

lemma Pr_visit_before_C:
  assumes L: "L ⊆ H" and I: "I ⊆ H"
  shows "𝒫(ω in 𝔓. visit I J ω ∧ before_C L ω ¦ hit_C ω ) =
    (∑i∈I. p_i i) * card L * p_j * p_f + (∑i∈I ∩ L. p_i i) * (1 - p_H * p_f)"
proof -
  let ?M = "Mix`H"
  let ?P = "λx P. emeasure (T x) {ω∈space (T x). P ω}"
  let ?V = "(visit I J aand before_C L) aand hit_C"
  let ?U = "HLD ?M suntil (Mix`L ⋅ HLD (Mix`C))"
  let ?L = "HLD (Mix`C)"

  have IJ: "x ∈ I ⟹ x ∈ J" for x
    using I by auto

  have [simp, intro]: "finite I" "finite L"
    using L I by (auto dest: finite_subset)

  have "?P Start ?V = ?P Start ((Init`I ⋅ ?U) or (Init`(I ∩ L) ⋅ ?L))"
  proof (rule emeasure_Collect_eq_AE)
    show "AE ω in 𝔓. ?V ω ⟷ ((Init`I ⋅ ?U) or (Init`(I ∩ L) ⋅ ?L)) ω"
      using AE_T_enabled AE_visit
    proof eventually_elim
      case (elim ω)
      then show ?case
        using before_C_imp_hit_C[of ω "L"]  before_C[of ω "L"] I L
        by (auto simp: visit_def HLD_iff Int_absorb2)
    qed
    show "Measurable.pred 𝔓 ((Init`I ⋅ ?U) or (Init`(I ∩ L) ⋅ ?L))"
      by measurable
  qed measurable
  also have "… = ?P Start (Init`I ⋅ ?U) + ?P Start (Init`(I ∩ L) ⋅ ?L)"
    using L I
    apply (subst plus_emeasure)
    apply (auto intro!: arg_cong2[where f=emeasure])
    apply (subst (asm) suntil.simps)
    apply (auto simp add: HLD_iff[abs_def] elim: suntil.cases)
    done
  also have "?P Start (Init`(I ∩ L) ⋅ ?L) = (∑i∈I∩L. p_i i * (1 - p_H))"
    using L I C_smaller p_j_pos
    apply (subst emeasure_HLD_nxt emeasure_HLD, simp)+
    apply (subst nn_integral_indicator_finite)
    apply (auto simp: emeasure_measure_pmf_finite sum.reindex next_prob_def sum.If_cases
                      Int_absorb2 H_compl2 ennreal_mult[symmetric] sum_nonneg
                      sum_distrib_left[symmetric] sum_distrib_right[symmetric]
                intro!: sum.cong sum_nonneg)
    apply (subst (asm) ennreal_inj)
    apply (auto intro!: mult_nonneg_nonneg sum_nonneg sum.mono_neutral_left elim!: negE)
    done
  also have "?P Start (Init`I ⋅ ?U) = (∑i∈I. ?P (Init i) ?U * p_i i)"
    using I
    by (subst emeasure_HLD_nxt, simp)
       (auto simp: nn_integral_indicator_finite sum.reindex emeasure_measure_pmf_finite
             intro!: sum.cong[OF refl])
  also have "… = (∑i∈I. ennreal (p_f * (1 - p_H) * p_j * card L / (1 - p_H * p_f)) * p_i i)"
  proof (intro sum.cong refl arg_cong2[where f="(*)"])
    fix i assume "i ∈ I"
    with I have i: "i ∈ H"
      by auto
    have "?P (Mix i) ?U = (p_f * p_f * (1 - p_H) * p_j * card L / (1 - p_H * p_f))"
      unfolding before_C_def
    proof (rule emeasure_suntil_geometric[where X="?M"])
      show "Mix i ∈ ?M"
        using i by auto
    next
      fix s assume "s ∈ ?M"
      with p_f p_j_pos L C_smaller[THEN less_imp_le]
      show "?P s (Mix`L ⋅ (HLD (Mix ` C))) = ennreal (p_f * p_f * (1 - p_H) * p_j * card L)"
        apply (simp add: emeasure_HLD emeasure_HLD_nxt del: nxt.simps space_T)
        apply (subst nn_integral_measure_pmf_support[of "Mix`L"])
        apply (auto simp add: subset_eq emeasure_measure_pmf_finite sum.reindex H_compl p_j_def
          ennreal_mult[symmetric] ennreal_of_nat_eq_real_of_nat)
        done
    next
      fix s assume "s ∈ ?M" then show "emeasure (N s) ?M = ennreal (p_H * p_f)"
        by (auto simp add: emeasure_measure_pmf_finite sum.reindex H_eq2)
    next
      show "AE ω in T t. ¬ ((Mix ` L ⋅ ?L) ⊓ (HLD (Mix ` H) ⊓ nxt ?U)) ω" for t
        using L
        apply (simp add: AE_T_iff[of _ t])
        apply (subst AE_T_iff; simp)
        apply (auto simp: HLD_iff suntil_Stream)
        done
    qed (insert L, auto simp: p_H_p_f_less_1 E_Mix)
    then show "?P (Init i) ?U = p_f * (1 - p_H) * p_j * card L / (1 - p_H * p_f)"
      by (subst emeasure_Init_eq_Mix)
         (auto simp: AE_End suntil_Stream divide_ennreal mult_le_one p_f)
  qed
  finally have *: "𝒫(ω in T Start. ?V ω) =
      (p_f * (1 - p_H) * p_j * (card L) / (1 - p_H * p_f)) * (∑i∈I. p_i i) +
      (∑i∈I ∩ L. p_i i) * (1 - p_H)"
    using sum_nonneg [of "I ∩ L" p_i]  sum_nonneg [of "I" p_i]
    by (simp add: mult_ac measure_def sum_distrib_right[symmetric] sum_distrib_left[symmetric]
                  sum_divide_distrib[symmetric] IJ ennreal_mult[symmetric] 
                  mult_le_one ennreal_plus[symmetric]
             del: ennreal_plus)
  show ?thesis
    unfolding cond_prob_def Pr_hit_C *
    using *
    using p_f p_H p_j_pos p_H_p_f_less_1 by (simp add: divide_simps) (simp add: field_simps)
qed

lemma Pr_visit_eq_before_C:
  "𝒫(ω in 𝔓. ∃j∈H. visit {j} J ω ∧ before_C {j} ω ¦ hit_C ω ) = 1 - (p_H - p_j) * p_f"
proof -
  let ?V = "λj. visit {j} J aand before_C {j}" and ?H = "hit_C"
  let ?J = "H"
  have "𝒫(ω in 𝔓. (∃j∈?J. ?V j ω) ∧ ?H ω) = (∑j∈?J. 𝒫(ω in 𝔓. (?V j aand ?H) ω))"
  proof (rule T.prob_sum)
    show "AE ω in 𝔓. (∀j∈?J. (?V j aand ?H) ω ⟶ ((∃j∈?J. ?V j ω) ∧ ?H ω)) ∧
      (((∃j∈?J. ?V j ω) ∧ ?H ω) ⟶ (∃!j. j∈?J ∧ (?V j aand ?H) ω))"
      by (auto intro!: AE_I2 dest: visit_unique1)
  qed auto
  then have "𝒫(ω in 𝔓. (∃j∈?J. ?V j ω) ¦ ?H ω) = (∑j∈?J. 𝒫(ω in 𝔓. ?V j ω ¦ ?H ω))"
    by (simp add: cond_prob_def sum_divide_distrib)
  also have "… = p_j * p_f + (1 - p_H * p_f)"
    by (simp add: Pr_visit_before_C sum_distrib_right[symmetric] sum.distrib)
  finally show ?thesis
    by (simp add: field_simps)
qed

lemma probably_innocent:
  assumes approx: "1 / (2 * (p_H - p_j)) ≤ p_f" and "p_H ≠ p_j"
  shows "𝒫(ω in 𝔓. ∃j∈H. visit {j} J ω ∧ before_C {j} ω ¦ hit_C ω ) ≤ 1 / 2"
  unfolding Pr_visit_eq_before_C
proof -
  have [simp]: "⋀n :: nat. 1 ≤ real n ⟷ 1 ≤ n" by auto
  have "0 ≤ p_j" unfolding p_j_def by auto
  then have "1 * p_j ≤ p_H"
    unfolding H_eq2[symmetric] using C_smaller
    by (intro mult_mono) (auto simp: Suc_le_eq card_Diff_subset not_le)
  with ‹p_H ≠ p_j› have "p_j < p_H" by auto
  with approx show "1 - (p_H - p_j) * p_f ≤ 1 / 2"
    by (auto simp add: field_simps divide_le_eq split: if_split_asm)
qed

lemma Pr_before_C:
  assumes L: "L ⊆ H"
  shows "𝒫(ω in 𝔓. before_C L ω ¦ hit_C ω ) =
    card L * p_j * p_f + (∑l∈L. p_i l) * (1 - p_H * p_f)"
proof -
  have "𝒫(ω in 𝔓. before_C L ω ¦ hit_C ω ) =
    𝒫(ω in 𝔓. visit H J ω ∧ before_C L ω ¦ hit_C ω )"
    using AE_visit by (auto intro!: T.cond_prob_eq_AE)
  also have "… = card L * p_j * p_f + (∑i∈L. p_i i) * (1 - p_H * p_f)"
    using L by (subst Pr_visit_before_C[OF L order_refl]) (auto simp: Int_absorb1)
  finally show ?thesis .
qed

lemma P_visit:
  assumes I: "I ⊆ H"
  shows "𝒫(ω in 𝔓. visit I J ω ¦ hit_C ω ) = (∑i∈I. p_i i)"
proof -
  have "𝒫(ω in 𝔓. visit I J ω ¦ hit_C ω ) =
    𝒫(ω in 𝔓. visit I J ω ∧ before_C H ω ¦ hit_C ω )"
  proof (rule T.cond_prob_eq_AE)
    show "AE x in 𝔓. hit_C x ⟶
                visit I J x = (visit I J x ∧ before_C H x)"
      using AE_T_enabled by eventually_elim (auto intro: hit_C_imp_before_C)
  qed auto
  also have "… = sum p_i I"
    using I by (subst Pr_visit_before_C[OF order_refl]) (auto simp: Int_absorb2 field_simps p_H_def p_j_def)
  finally show ?thesis .
qed

subsection ‹Probability space of hitting a collaborator›

definition "hC = uniform_measure 𝔓 {ω∈space 𝔓. hit_C ω}"

lemma emeasure_hit_C_not_0: "emeasure 𝔓 {ω ∈ space 𝔓. hit_C ω} ≠ 0"
  using p_H p_H_p_f_less_1 unfolding Pr_hit_C T.emeasure_eq_measure by auto

lemma measurable_hC[measurable (raw)]:
  "A ∈ sets S ⟹ A ∈ sets hC"
  "f ∈ measurable M S ⟹ f ∈ measurable M hC"
  "g ∈ measurable S M ⟹ g ∈ measurable hC M"
  "A ∩ space S ∈ sets S ⟹ A ∩ space hC ∈ sets S"
  unfolding hC_def uniform_measure_def
  by simp_all

lemma vimage_Int_space_C[simp]:
  "f -` {x} ∩ space hC = {ω∈space S. f ω = x}"
  by (auto simp: hC_def)

sublocale hC: information_space hC 2
proof -
  interpret hC: prob_space hC
    unfolding hC_def
    using emeasure_hit_C_not_0
    by (intro prob_space_uniform_measure) auto
  show "information_space hC 2"
    by standard simp
qed

abbreviation
  mutual_information_Pow_CP (‹ℐ'(_ ; _')›) where
  "ℐ(X ; Y) ≡ hC.mutual_information 2 (count_space (X`space hC)) (count_space (Y`space hC)) X Y"

lemma simple_functionI:
  assumes "finite (range f)"
  assumes [measurable]: "⋀x. {ω∈space S. f ω = x} ∈ sets S"
  shows "simple_function hC f"
  using assms unfolding simple_function_def hC_def
  by (simp add: vimage_def space_stream_space)

subsection ‹Estimate the information to the collaborators›

lemma measure_hC[simp]:
  assumes A[measurable]: "A ∈ sets S"
  shows "measure hC A = 𝒫(ω in 𝔓. ω ∈ A ¦ hit_C ω )"
  unfolding hC_def cond_prob_def
  using emeasure_hit_C_not_0 A
  by (subst measure_uniform_measure) (simp_all add: T.emeasure_eq_measure Int_def conj_ac)

subsubsection ‹Setup random variables for mutual information›

definition "first_J ω = (THE i. visit {i} J ω)"

lemma first_J_eq:
  "visit {i} J ω ⟹ first_J ω = i"
  unfolding first_J_def by (intro the_equality) (auto dest: visit_unique1)

lemma AE_first_J:
  "AE ω in 𝔓. visit {i} J ω ⟷ first_J ω = i"
  using AE_visit
proof eventually_elim
  fix ω assume "visit H J ω"
  then obtain j where "visit {j} J ω" "j ∈ H"
    by (auto simp: visit_def HLD_iff)
  then show "visit {i} J ω ⟷ first_J ω = i"
    by (auto dest: visit_unique1 first_J_eq)
qed

lemma measurbale_first_J[measurable]: "first_J ∈ measurable S (count_space UNIV)"
  unfolding first_J_def[abs_def]
  by (intro measurable_THE[where I=H])
     (auto dest: visit_imp_in_H visit_unique1 intro: countable_finite)

definition "last_H ω = (THE i. before_C {i} ω)"

lemma measurbale_last_H[measurable]: "last_H ∈ measurable S (count_space UNIV)"
  unfolding last_H_def[abs_def]
  by (intro measurable_THE[where I=H])
     (auto dest: before_C_single before_C_unique intro: countable_finite)

lemma last_H_eq:
  "before_C {i} ω ⟹ last_H ω = i"
  unfolding last_H_def by (intro the_equality) (auto dest: before_C_unique)

lemma last_H:
  assumes "enabled Start ω" "hit_C ω"
  shows "before_C {last_H ω} ω" "last_H ω ∈ H"
  by (metis before_C_single hit_C_imp_before_C last_H_eq Int_iff assms)+

lemma AE_last_H:
  "AE ω in 𝔓. hit_C ω ⟶ before_C {i} ω ⟷ last_H ω = i"
  using AE_T_enabled
proof eventually_elim
  fix ω assume "enabled Start ω" then show "hit_C ω ⟶ before_C {i} ω = (last_H ω = i)"
    by (auto dest: last_H last_H_eq)
qed

lemma information_flow:
  defines "h ≡ real (card H)"
  assumes init_uniform: "⋀i. i ∈ H ⟹ p_i i = 1 / h"
  shows "ℐ(first_J ; last_H) ≤ (1 - (h - 1) * p_j * p_f) * log 2 h"
proof -
  let ?il = "λi l. 𝒫(ω in 𝔓. visit {i} J ω ∧ before_C {l} ω ¦ hit_C ω )"
  let ?i = "λi. 𝒫(ω in 𝔓. visit {i} J ω ¦ hit_C ω )"
  let ?l = "λl. 𝒫(ω in 𝔓. before_C {l} ω ¦ hit_C ω )"

  from init_uniform have init_H: "⋀i. i ∈ H ⟹ p_i i = p_j / p_H"
    by (simp add: p_j_def p_H_def h_def)

  from h_def have "1/h = p_j/p_H" "h = p_H / p_j" "p_H = h * p_j"
    by (auto simp: p_H_def p_j_def field_simps)
  from C_smaller have h_pos: "0 < h"
    by (auto simp add: card_gt_0_iff h_def)

  let ?s = "(h - 1) * p_j"
  let ?f = "?s * p_f"

  from psubset_card_mono[OF _ C_smaller]
  have "1 ≤ card J - card C"
    by (simp del: C_le_J)
  then have "1 ≤ h"
    using C_smaller
    by (simp add: h_def card_Diff_subset card_mono field_simps del: C_le_J)

  have log_le_0: "?f * log 2 (p_H * p_f) ≤ ?f * log 2 1"
    using p_H_p_f_less_1 p_H_p_f_pos p_j_pos p_f ‹1 ≤ h›
    by (intro mult_left_mono log_mono mult_nonneg_nonneg) auto

  have "(h - 1) * p_j < 1"
    using ‹1 ≤ h› C_smaller
    by (auto simp: h_def p_j_def divide_less_eq card_Diff_subset card_mono)
  then have 1: "(h - 1) * p_j * p_f < 1 * 1"
    using p_f by (intro mult_strict_mono) auto

  { fix ω have "first_J ω ∈ H ∨ first_J ω = (THE x. False)"
      apply (cases "∀i. ¬ visit {i} J ω")
      apply (simp add: first_J_def)
      apply (auto dest: visit_imp_in_H first_J_eq)
      done }
  then have range_fj: "range first_J ⊆ H ∪ {THE x. False}"
    by auto

  have sf_fj: "simple_function hC first_J"
    by (rule simple_functionI) (auto intro: finite_subset[OF range_fj])

  have sd_fj: "simple_distributed hC first_J ?i"
    apply (rule hC.simple_distributedI[OF sf_fj])
    apply (auto intro!: T.cond_prob_eq_AE)
    apply (auto simp: space_stream_space)
    using AE_first_J
    apply eventually_elim
    apply auto
    done

  { fix ω have "last_H ω ∈ H ∨ last_H ω = (THE x. False)"
      apply (cases "∀i. ¬ before_C {i} ω")
      apply (simp add: last_H_def)
      apply (auto dest: before_C_imp_in_H last_H_eq)
      done }
  then have range_lnc: "range last_H ⊆ H ∪ {THE x. False}"
    by auto

  have sf_lnc: "simple_function hC last_H"
    by (rule simple_functionI) (auto intro: finite_subset[OF range_lnc])

  have sd_lnc: "simple_distributed hC last_H ?l"
    apply (rule hC.simple_distributedI[OF sf_lnc])
    apply (auto intro!: T.cond_prob_eq_AE)
    apply (auto simp: space_stream_space)
    using AE_last_H
    apply eventually_elim
    apply auto
    done

  have sd_fj_lnc: "simple_distributed hC (λω. (first_J ω, last_H ω)) (λ(i, l). ?il i l)"
    apply (rule hC.simple_distributedI)
    apply (rule simple_function_Pair[OF sf_fj sf_lnc])
    apply (auto intro!: T.cond_prob_eq_AE)
    apply (auto simp: space_stream_space)
    using AE_last_H AE_first_J
    apply eventually_elim
    apply auto
    done

  define c where "c = (SOME j. j ∈ C)"
  have c: "c ∈ C"
    using C_non_empty unfolding ex_in_conv[symmetric] c_def by (rule someI_ex)

  let ?inner = "λi. ∑l∈H. ?il i l * log 2 (?il i l / (?i i * ?l l))"
  { fix i assume i: "i ∈ H"
    with h_pos have card_idx: "real_of_nat (card (H - {i})) = p_H / p_j - 1"
      by (auto simp add: p_j_def p_H_def h_def)

    have neq0: "p_j ≠ 0" "p_H ≠ 0"
      unfolding p_j_def p_H_def
      using C_smaller i by auto

    from i have "?inner i =
      (∑l∈H - {i}. ?il i l * log 2 (?il i l / (?i i * ?l l))) +
      ?il i i * log 2 (?il i i / (?i i * ?l i))"
      by (simp add: sum_diff)
    also have "… =
      (∑l∈H - {i}. p_j/p_H * p_j * p_f * log 2 (p_j * p_f / (p_j * p_f + p_j/p_H * (1 - p_H * p_f)))) +
      p_j/p_H * (p_j * p_f + (1 - p_H * p_f)) * log 2 ((p_j * p_f + (1 - p_H * p_f)) / (p_j * p_f + p_j/p_H * (1 - p_H * p_f)))"
      using i p_f p_j_pos p_H
      apply (simp add: Pr_visit_before_C P_visit init_H Pr_before_C
                  del: sum_constant)
      apply (simp add: divide_simps distrib_left)
      apply (intro arg_cong2[where f="(*)"] refl arg_cong2[where f=log])
      apply (auto simp: field_simps)
      done
    also have "… = (?f * log 2 (h * p_j * p_f) + (1 - ?f) * log 2 ((1 - ?f) * h)) / h"
      using neq0 p_f by (simp add: card_idx field_simps ‹p_H = h * p_j›)
    finally have "?inner i = (?f * log 2 (h * p_j * p_f) + (1 - ?f) * log 2 ((1 - ?f) * h)) / h" . }
  then have "(∑i∈H. ?inner i) = ?f * log 2 (h * p_j * p_f) + (1 - ?f) * log 2 ((1 - ?f) * h)"
    using h_pos by (simp add: h_def[symmetric])
  also have "… = ?f * log 2 (p_H * p_f) + (1 - ?f) * log 2 ((1 - ?f) * h)"
    by (simp add: ‹h = p_H / p_j›)
  also have "… ≤ (1 - ?f) * log 2 ((1 - ?f) * h)"
    using log_le_0 by simp
  also have "… ≤ (1 - ?f) * log 2 h"
    using h_pos ‹1 ≤ h› 1 p_j_pos p_f
    by (intro mult_left_mono log_mono mult_pos_pos mult_nonneg_nonneg) auto
  finally have "(∑i∈H. ?inner i) ≤ (1 - ?f) * log 2 h" .
  also have "(∑i∈H. ?inner i) =
      (∑(i, l)∈(first_J`space S) × (last_H`space S). ?il i l * log 2 (?il i l / (?i i * ?l l)))"
    unfolding sum.cartesian_product
  proof (safe intro!: sum.mono_neutral_cong_left del: DiffE DiffI)
    show "finite ((first_J ` space S) × (last_H ` space S))"
      using sf_fj sf_lnc by (auto simp add: hC_def dest!: simple_functionD(1))
  next
    fix i assume "i ∈ H"
    then have "visit {i} J (Init i ## Mix i ## sconst End)"
      "before_C {i} (Init i ## Mix c ## sconst End)"
      by (auto simp: before_C_def visit_def suntil_Stream HLD_iff c)
    then show "i ∈ first_J ` space S" "i ∈ last_H ` space S"
      by (auto simp: space_stream_space image_iff eq_commute dest!: first_J_eq last_H_eq)
  next
    fix i l assume "(i, l) ∈ first_J ` space S × last_H ` space S - H × H"
    then have H: "i ∉ H ∨ l ∉ H"
      by auto
    have "𝒫(ω in 𝔓. (visit {i} J ω ∧ before_C {l} ω) ∧ hit_C ω) = 0"
      using H by (intro T.prob_eq_0_AE) (auto dest: visit_imp_in_H before_C_imp_in_H)
    then show "?il i l * log 2 (?il i l / (?i i * ?l l)) = 0"
      by (simp add: cond_prob_def)
  qed
  also have "… = ℐ(first_J ; last_H)"
    unfolding sum.cartesian_product
    apply (subst hC.mutual_information_simple_distributed[OF sd_fj sd_lnc sd_fj_lnc])
    apply (simp add: hC_def)
  proof (safe intro!: sum.mono_neutral_right imageI)
    show "finite ((first_J ` space S) × (last_H ` space S))"
      using sf_fj sf_lnc by (auto simp add: hC_def dest!: simple_functionD(1))
  next
    fix i l assume "(first_J i, last_H l) ∉ (λx. (first_J x, last_H x)) ` space S"
    moreover
    { fix i l assume "i ∈ H" "l ∈ H"
      then have "visit {i} J (Init i ## Mix l ## Mix c ## sconst End)"
        "before_C {l} (Init i ## Mix l ## Mix c ## sconst End)"
        using c C_smaller by (auto simp: before_C_def visit_def HLD_iff suntil_Stream)
      then have "first_J (Init i ## Mix l ## Mix c ## sconst End) = i"
        "last_H (Init i ## Mix l ## Mix c ## sconst End) = l"
        by (auto intro!: first_J_eq last_H_eq) }
    note this[of "first_J i" "last_H l"]
    ultimately have "(first_J i, last_H l) ∉ H×H"
      by (auto simp: space_stream_space image_iff eq_commute) metis
    then have "𝒫(ω in 𝔓. (visit {first_J i} J ω ∧ before_C {last_H l} ω) ∧ hit_C ω) = 0"
      by (intro T.prob_eq_0_AE) (auto dest: visit_imp_in_H before_C_imp_in_H)
    then show "?il (first_J i) (last_H l) *
      log 2 (?il (first_J i) (last_H l) / (?i (first_J i) * ?l (last_H l))) = 0"
      by (simp add: cond_prob_def)
  qed
  finally show ?thesis by simp
qed

end

end